Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

# Benja comments on An angle of attack on Open Problem #1 - Less Wrong

28 18 August 2012 12:08PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Sort By: Best

Comment author: 18 August 2012 12:05:42PM *  5 points [-]

Ok, first note that here I'm applying what I proved in the whole previous paragraph, so it's not as easy to explain as one single step of reasoning. That said, the short answer is that what I've actually done is to pass from "PA_K proves that PA_K proves that p is K-step safe" to "PA_K proves that p is (K-1)-step safe": note that inst(K-1, 'p is safe for K steps') means that K-1 is substituted for K in the thing in quotes...

...except, there is a problem with that, namely that inst(n,x) was supposed to be a meta-level function that substitutes the numeral corresponding to n for each occurrence of K in x. On the meta-level, (K-1) is just an expression, not a definite value, so this doesn't work. Argh, I had thought about that problem, but I thought I'd fixed it... I'll have to think about it & update the post. Thanks!

Comment author: 18 August 2012 01:02:19PM 6 points [-]

I'm applying what I proved in the whole previous paragraph, so it's not as easy to explain as one single step of reasoning

OK

Formalizing the above argument in Peano Arithmetic, and writing instPA(n,x) for the object-level encoding of the meta-level function, we can prove: "For all extended-language sentences 'C', if PAK proves 'C', then for all n, PA(n+1) proves instPA(n,'C')."

Oh, this is the place that I should have pointed out. Sorry.

If I understand this correctly, "PA_K proves that if PA_K proves 'C', PA(1) proves instPA(0, 'C')". Also, PA_K should prove all simple things from PA(2), like PA(1) being consistent. Let us consider 'C' being plain "falsehood". Then we shall get "PA_K proves that PA(1) is not contradictory and if PA_K is contradictory, PA(1) is contradictory". For the benefit of casual reader: this would imply that PA_K contains PA and proves its own consistency, which implies that PA_K is contradictory.

This means I missed something very basic about what goes on here. Could you point out what exactly, please?

Comment author: 18 August 2012 10:44:42PM 1 point [-]

Thanks for digging deeper! This is much easier to answer: PA_K does not prove PA(1) consistent. As I noted at the end of the post, it's conservative over PA(1), which means that it proves a sentence in the base language only if PA(1) does. The reason is that if C is a sentence in the base language and x is a proof of it, then inst(1,x) is a proof of inst(1,C), but since C doesn't contain any occurrences of K, inst(1,C) = C.

Does that help?

Comment author: 19 August 2012 08:08:53AM 2 points [-]

Not much yet.

At the very least, it looks like your third note should be removed.

It is easy to prove that PA(n) is monotonically growing in strength.

By induction, PA(0) is inside PA(K). It is even obvious in PA_K.

PA_K proves "PA(K) proves 'falsehood' implies 'falsehood'", as 'falsehood' is a constant falsehood without reference to K, and is in the base language.

PA_K proves "PA(0) proves 'falsehood' implies PA(K) proves 'falsehood', which implies 'falsehood", by provable monotonicity.

PA_K proves "PA(0) is consistent", because I just collapse the logical steps in the previous statement.

PA_K proves "K=0 or PA(1) is consistent", by analogy.

PA_K proves:

"For all extended-language sentences 'C', if PA_K proves 'C', then for all n, PA(n+1) proves instPA(n,'C')."

(direct quote, hopefully understood correctly)

'falsehood' is a formula and it doesn't change under substitutions. So, "PA_K proves 'falsehood' implies PA(1) proves 'falsehood'"

So we can combine PA_K-PA(1) relation and PA(1) conditional consistency and get:

PA_K proves: "K=0 or PA_K is consistent"

So if PA_K says K>10, we have a huge problem here.

Comment author: 19 August 2012 08:54:01AM *  1 point [-]

At the very least, it looks like your third note should be removed.

From the rest of your comment, I think that's probably a typo and it's the second note you're concerned about? Or I'm misunderstanding?

PA_K proves "K=0 or PA(1) is consistent", by analogy.

I agree with this and with your proof of it.

PA_K proves: "For all extended-language sentences 'C', if PA_K proves 'C', then for all n, PA(n+1) proves instPA(n,'C')."

...

So if PA_K says K>10, we have a huge problem here.

Right, the assertion you quote would fail in the system proposed in the second note -- let's call it PA_K[2] for short. (And in PA_K itself, you do not have K>10.) Instead, I believe you have

PA_K[2] proves: "For all extended-languange sentences 'C', if PA_K[2] proves 'C', then there is an m such that for all n>=m, PA(n+1) proves instPA(n,'C')."

(In the proof, we fix a proof of 'C' and choose m such that if the axiom "K>k" is used in the proof of 'C', then m>k.)

It's quite possible that something else in my proof idea fails if you replace PA_K by PA_K[2], but I'd like to table that question for now while I'm working on trying to fix the proof. (I'm happy to continue talking about the consistency of PA_K[2], if you're interested in that, I just don't want to get into whether the proof about AI_K can be modified into a proof for "AI_K[2]" before I've figured out whether I can fix the first one.)

Please keep the questions coming, it's very good to have someone thinking about these things in technical detail.

[ETA: fixed a typo; in the thing that I conjecture PA_K[2] proves, I accidentally wrote 'PA_K' instead of 'PA_K[2]'.]

Comment author: 19 August 2012 09:45:06AM 0 points [-]

Yes, I meant that the comment introducing PA_K[2] should be weakened somehow because it is easily understood as something introducing contradictory system.

Comment author: 19 August 2012 10:09:17AM 0 points [-]

Ok, included a warning with a link to our discussion for now.