excellent south park reference, bro.

Pretty sure I see it, not sure if I'm supposed to give it away in the comments.

(It did not seem all that medium hard to me, so maybe I didn't get it after all, and in that case I had better not post it and embarass myself.)

Löb proved the following: for any C, Provable(Provable(C)->C)->Provable(C).

So, we may derive from PA soundness, that for any C, Provable(Provable(C)->C)->C.

Nobody proved, as you stated, that for any C (Provable(C)->C)->C.

The confusing part is this:

(C is provable -> C) -> C

I can grok the part inside the parenthases - that's what we'd all like to believe; that this system can assure us that everything it proves is true. The weird step is that this statement itself implies that C is true - I guess we either take this on faith or read the Deduction Theorem.

What I find most strange, though, is the desire to have the proof system itself distinguish between provability and truth. Isn't that impossible? A formal system only provides proofs given axioms; to it, the only me... (read more)

Tiiba: "(Smoke implies fire, therefore fire) implies (no smoke means fire)?" "therefore fire" should be left out. i) (Smoke implies fire) implies fire. ii) No smoke implies fire.

You're confused because i) is false.

Medium puzzle:

"Applying the Deduction Theorem to Löb's Theorem gives us, for all C:

((◻C)->C)->C"

Wouldn't it be: ((?C) -> C) -> ?C If the provability of C implies C's truth, then C is provable.

In other words, where you write "(X->Y)->Y", it should be "(X -> Y) -> X".

I think the error is that you didn't prove it was unprovable -- all provably unprovable statements are also provable, but unprovable statements aren't necessarily true.

In other words, I think what you get from the Deduction Theorem (which I've never seen before, so I may have it wrong) is Provable((Provable(C) -> C) -> C). I think if you want to "reach inside" that outer Provable and negate the provability of C, you have to introduce Provable(not Provable(C)).

The hypothesis was that PA proves that "if PA proves C, then C" This enabled it to be proved that "PA proves C" So I think what we actually get applying the deduction theorem is ?((◻C)->C)->?C

Peter: I THOUGHT that I'm supposed to assume that there's smoke. (DNRTFA, too hard for my little brain)

The flaw is the instant you used the deduction theorem. You used it to go from

PA |- "◻C -> C" -> PA |- "C"

to

PA |- "(◻C->C) -> C"

What the induction theorem really says is

T + X |- Y implies T |- "X -> Y"

so what you really would have needed to apply the deduction theorm would have been

PA + "◻C -> C" |- C

do I win?

oops that should be "what the deduction theorem really says"

Boiling it down to essentials, it looks to me like the key move is this:

• If we can prove X, then we can prove Y.
• Therefore, if X is true, then we can prove Y.

But this doesn't follow - X could be true but not provable.

Is that right? It's ages since I did logic, and never to a deep level, so excuse me if this is way off.

Hint: Pinpointing the exact flaw in the proof that 2=1, requires you to mention one of the steps 1-10 of the (valid) proof of Lob's Theorem.

Any supposed analysis that does not tell you to mention a particular step, is inexact at best, and more probably mistaken.

Eliezer: "Any supposed analysis that does not tell you to mention a particular step, is inexact at best, and more probably mistaken."

I'm pretty sure my answer was completely correct. Care to point out the inexactness/mistakes?

If L:ob's theorem is true, then surely we can use it without any reference to the details of its proof? Isn't the point of a proof to obtain a black box, so that we do not have to worry about all the various intermediate steps? And in this case, wouldn't it defeat the purpose of having a proof if, to explain how the proof was misapplied, we had to delve deep into the guts of the proof, rather than just pointing to the relevant features of its interface?

Opps, I made an error when I said: "It is clear that (X->Y)->X does not imply (not X)->X, so your little trick doesn't work." This is false. This implication does exist, so we get:

((not ◻C)->(◻C))

This sentence is true just in case C is in fact provable, so we don't have a problem with your 2=1 cases.

Robert: "You can only say (((◻C)->C)->(◻C))"

No that's not right. The theorem says that if PA proves "◻C -> C" then PA proves C. so that's ◻(◻C -> C) -> ◻C.

The flaw is that the deduction theorem does not cross meta levels. Eliezer says "Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C." and goes on to claim that (◻C->C)->C. But he's intentionally failed to use quotes and mixed up the meta levels here. Lob's Theorem does not give us a proof in first order logic from ((◻C)->C) to C. It gives us a proof that if there is a proof of ((◻C)->C) then there is a proof of C. Which is an entirely diffirent thing altogether.

so what you really would have needed to apply the deduction theorm would have been PA + "◻C -> C" |- C do I win?

Why doesn't the given proof of Lob's Theorem, the steps 1-10, show that PA + "◻C -> C" |- C?

Eliezer: "Why doesn't the given proof of Lob's Theorem, the steps 1-10, show that PA + "◻C -> C" |- C?"

That's just not what it says. The hypothesis in step 2 isn't "◻C -> C" it's "◻(◻C -> C)". I suppose if the Hypothesis were "◻C -> C" we could try to find where it breaks. Step 7 is the only step that depends on 2 so it has to be there. Translating the amusing cartoons, we have

1. ◻(◻C -> C)
2. ◻(◻L -> ◻C)
3. ◻(◻L -> C)

Lets say that instead we have

2'. ◻C -> C

Well what are we supposed to do with it? We're stuck. Just because ◻C -> C doesn't mean that PA can prove it.

Eliezer's password is [correct answer deleted, congratulations Douglas --EY].

Larry, interpret the smiley face as saying:

PA + (◻C -> C) |-

Then the steps 1-10 of Lob's proof would seem to take us from:

PA + (◻C -> C) |- (◻C -> C)

to

PA + (◻C -> C) |- C

If this were the case, the deduction theorem would in fact come into play and give us:

PA |- (◻C -> C) -> C

So there must be at least one step of the reasoning 1-10 that does not apply. Which one and why?

Doug S.:

What character is ◻?

Eliezer Yudkowsky:

Larry, interpret the smiley face as saying:

PA + (◻C -> C) |- I'm still struggling to completely understand this. Are you also changing the meaning of ◻ from 'derivable from PA' to 'derivable from PA + (◻C -> C)'? If so, are you additionally changing L to use provability in PA + (◻C -> C) instead of provability in PA?

As near as I can make out, the flaw is the assumption that there isn't a proof of 2=1.

There's no proof of Peano arithmetic being consistent, right? (There's a proof of that lack of proof, of course. :))

Psy-Kosh: No that isn't the problem. If there is a proof that 1=2, then 1=2. If there isn't, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a -> ◻b is the same as "a -> b".

Sebastian Hagen: no ◻X is PA |- "X". My best guess as to what Eliezer meant by "interpret the smiley face as saying.." is that he meant to interpret the cartoonproof as a proof from the assumption "(◻C -> C)" to the conclusion "C", rather than a proof from "◻(◻C -> C)" to "◻C".

Loeb's theorem shows that if PA proves "not P(C)->C", then PA proves C (using P(X) for "X is provable in PA").

It follows from that, using the Deduction Theorem, that PA proves "(not P(C)->C)->C"; it does not follow that "(not P(C)->C)->C" is a logical tautology.

From that, you obtain, similarly, that PA proves "(not P(C)) -> C". And you say "I cannot prove that 2 = 1". Sure, you cannot, but can PA? That's the real question.

There's nothing particularly surprising about PA proving &... (read more)

Larry, a simple 8 would have sufficed. :) (That's what Douglas wrote.)

I just tested and anecdotally confirmed a hypothesis made with very little data: I suspected that neither Douglas Knight nor Larry D'Anna, the two who pinpointed 8 as the critical step, would be among the objectors to my metaethics. (Either of them can torpedo this nascent theory by stating otherwise.)

"I just tested and anecdotally confirmed a hypothesis made with very little data: I suspected that neither Douglas Knight nor Larry D'Anna, the two who pinpointed 8 as the critical step, would be among the objectors to my metaethics. (Either of them can torpedo this nascent theory by stating otherwise.)"

I like your metaethics just fine.

Okay, I still don't see why we had to pinpoint the flaw in your proof by pointing to a step in someone else's valid proof.

Larry D'Anna identified the step you were looking for, but he did it by trying to transform the proof of Lob's Theorem into a different proof that said what you were pretending it said.

I think, properly speaking, the flaw is pinpointed by saying that you were misusing the theorems, not that the mean old theorem had a step that wouldn't convert into what you wanted it to be.

I've been looking more at the textual proof you linked (the cart... (read more)

How is the problem not going from 6 to 7? The false argument you gave uses PA + ((◻C)->C)|- C instead of PA |- ?((◻C)->C) when invoking the deduction theorem. In other words, the false argument is exactly the same except when it uses step 2 (which is Löb's Hypothesis). More specifically, making L doesn't depend on Löb's Hypothesis, and steps 1-6 don't depend on it either (as in they are still true in PA without the Hypothesis). Furthermore, assuming step 7 (ie PA + whatever you add |- step 7) step 8 must follow by A1.

Larry: I'm a bit confused, could you clarify what you mean? Thanks. (Incidentally, I'm pretty sure what Brain said is basically a much more detailed way of saying what I said. That is, I think Brian's right, and, further, that what I was saying was similar (though, obviously, far less detailed)

So what am I misunderstanding?

Again, thanks.

Psy-Kosh: There are two points of view of where the flaw is.

My point view is that the flaw is here:

"Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C. Applying the Deduction Theorem to Löb's Theorem gives us, for all C: ((◻C)->C)->C"

Because, in fact Lob's Theorem is: (PA |- "◻C -> C") => (PA |- "C") and the Deduction theorem says (PA + X |- Y) => (PA |- "X->Y"). We don't have PA + X proving anything for any X. The deduction theorem just doesn't apply. The flaw is that the ... (read more)

Larry D'Anna: Thanks, I think I understand the Deduction Theorem now.

We don't have PA + X proving anything for any X.

It seems to me that we do have (PA + "?(◻C -> C)" |- "?C")

from which the deduction theorem gives: (PA |- "?(◻C -> C) -> ?C") which is Löb's Theorem itself.

simon: Let me explain some of the terminology here, because that may be where the confusion lies.

A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.

A theory is a (possibly infinite) set of sentences. PA is a theory.

A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.

The notation PA + X, where X is a sentences is just the union of PA and {X}.

The notation PA |- Y means that a proof from PA that ends in Y ex... (read more)

Hmm. I was thinking that Löb's Theorem was a theorem in PA, in which case the step going from

PA + ?(?C -> C) |- ?(?L -> C)

to

PA + ?(?C -> C) |- ?(?(?L -> C))

seems legitimate given

PA |- (?X -> ?(?X))

which we ought to be able to use since PA is part of the theory before the |- symbol.

If we don't have PA on the left, can we use all the "ingredients" without adding additional assumptions?

In any case, if we do not use the deduction theorem to derive the implication in Löb's Theorem, what do we use?

simon:

I was thinking that Löb's Theorem was a theorem in PA

It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There's no contradiction there, as long as you have everything quoted properly.

in which case the step going from PA + ?(?C -> C) |- ?(?L -> C) to PA + ?(?C -> C) |- ?(?(?L -> C)) seems legitimate given PA |- (?X -> ?(?X))

That's a valid deduction, but I don't think it's a step that anyone has written down ... (read more)

I know nothing about math, and cannot even follow what's being argued (keep this in mind when programming the fAI), but it's really funny to see how one of the 2 guys that got the right answer is on this like white on rice. Is that part of the experiment?

It's not clear to me where you are going with it.

To argue that a proof is being made concluding ?C using the assumption ?(◻C -> C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- "?(◻C -> C) -> ?C") (i.e. my interpretation of Löb's Theorem)

We use 10 steps, 9 of which are proofs inside of PA

But the proof uses an additional assumption which is the antecedent of an implication, and comes to a conclusion which is the consequent of the implication. To get the implication, we must use the deduction theorem ... (read more)

simon:

To argue that a proof is being made concluding ?C using the assumption ?(◻C -> C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- "?(◻C -> C) -> ?C") (i.e. my interpretation of Löb's Theorem)

OK so the question marks are boxes right? In that case then yes, PA |- "?(?C -> C) -> ?C". This is OK. The contradiction comes if PA |- "(?C->C)->C". But morally this doesn't have anything to do with the deduction theorem. PA proves Lob because everything in the proo... (read more)

Let me try to say that clearer.

Suppose that A is false.

How the hell are you going to show that if PA proves A true then A will be true, when A is actually false?

If you can't prove what would happen if PA proved A true when A is actually false, then if you can prove that if PA proves A is true then A has to be true, it must be that A is true in the first place.

If this reasoning is correct then there isn't much mystery involved here.

One more time. If PA proves you are a werewolf, then you're really-and-truly a werewolf. PA never proves anything that isn't ac... (read more)

J Thomas:

Once more through the mill. If PA proves that 6 is a prime number, then 6 is really a prime number. Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?

If PA |- "forall x y . x y = 6 => |x|=1 || |y|=1" then N |= "forall x y . x y = 6 => |x|=1 || |y|=1" (N = the natural numbers equiped with + and ) so for all x and y in N, N |= ",x ,y = 6 => |,x|=1 || |,y|=1" (where ,x means a constant symbol for x) if xy = 6 then N |= ",x ,y = 6" so theref... (read more)

But Larry, PA does not actually say that 6 is prime, and 6 is not prime.

You could say that if PA proved that every theorem is false then every theorem would be false.

Or what would it mean if PA proved that Lob's theorem was false?

It's customary to say that any conclusion from a false premise is true. If 6 is prime then God's in his heaven, everything's right with the world and we are all muppets. Also God's in hell, everything's wrong with the world, and we are all mutant ninja turtles. It doesn't really matter what conclusions you draw from a false premis... (read more)

"But Larry, PA does not actually say that 6 is prime, and 6 is not prime."

Well of course 6 isn't prime. But if PA said it was, then it would be. There's nothing invalid about proving that A -> B if you know ~A. It's just not very useful. But for a somewhat less vacuous example, let RH be the riemann hypothesis. Then if PA |- RH then RH is true and if PA |- ~RH then RH is false. At least one of these implications has a false hypothesis, but they are both perfectly valid.

Larry, one of them is counterfactual.

If you draw implications on a false asumption then the result is useful only to show that an assumption is false.

So if PA -> 1=2 then PA -> 1<>2. How is that useful?

If PA -> 6 is prime then PA also -> 6 is not prime.

Once you assume that PA implies something that PA actually implies is false, you get a logical contradiction. Either PA is inconsistent or PA does not imply the false thing.

How can it be useful to reason about what we could prove from false premises? What good is it to pretend that PA is inconsistent?

J Thomas: "How is that useful?"

I'm just answering your question

"Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?"

I'm not stating that proving implications with false antecedent is particularly useful, just that it is valid. Also aside from 6 being prime it is true that for any sentence phi, ZF |- "if PA |- phi then phi", but that ZF cannot even say, yet alone prove that "forall phi. if PA |- phi then phi". But it can prove "forall phi. if PA |- phi then N |= phi".

Larry, you have not proven that 6 would be a prime number if PA proved 6 was a prime number, because PA does not prove that 6 is a prime number.

The theorem is only true for the phi that it's true for.

The claim that phi must be true because if it's true then it's true, and if it's false then "if PA |- phi then phi" has an officially true conclusion whenever PA does not imply phi, is bogus.

It's simply and obviously bogus, and I don't understand why there was any difficulty about seeing it.

I thought of a simpler way to say it.

If Hillary Clinton was a man, she wouldn't be Bill Clinton's wife. She'd be his husband.

Similarly, if PA proved that 6 was prime, it wouldn't be PA. It would be Bill Clinton's husband. And so ZF would not imply that 6 is actually prime.

J Thomas
Larry, you have not proven that 6 would be a prime number if PA proved 6 was a prime number, because PA does not prove that 6 is a prime number.

No I'm afraid not. You clearly do not understand the ordinary meaning of implications in mathematics. "if a then b" is equivalent (in boolean logic) to ((not a) or b). They mean the exact same thing.

The claim that phi must be true because if it's true then it's true

I said no such thing. If you think I did then you do not know what the symbols I used mean.

It's simply and obviously bogus, and I... (read more)

From the medium hard question, we have "Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C." From the cartoon, the hypothesis of Lob's theorem is, " If PA proves 'PA proves X, then X' then PA proves X", so to apply the theorem to the situation outlined in the question we would be required to write instead of "((◻C)->C)" in the first sentence the following "PA proves '((◻C)->C)' ". Then by the deduction theorem, we'd have the following conclusion: '◻('(◻C)->C')->◻C' and so the trouble with material implication wouldn't arise because the first '->' is in a quoted sentence.

Trying the puzzle, before I read the other comments:

Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.

I think this is the flaw. Löb's Theorem shows that whenever we can prove ((◻C)->C) in PA, then we can prove C in PA. So instead of ((◻C)->C)->C, it would actually be ◻((◻C)->C)->◻C.

At first I looked at ◻((◻C)->C)->◻C and thought it had a similar problem — if we let C be the statement 2 = 1, then clearly C = false, so ◻((◻C)->false)->◻C; so ◻(true)->◻C; and presumably you can prove tautologies in PA, s... (read more)

If you really want to see the truth of the theorem at a glance, I found a much simpler proof on page 7 of this writeup by Aaronson.

Posting before reading other comments...

The flaw is in the very last step: that there is no proof of 2=1. If PA is inconsistent then contradictions are provable in PA and then anything else is too, including 2=1. To prove that there is no proof of 2=1 is to prove that PA is consistent, which is impossible by Godel's theorem.

Link to http://www.sm.luth.se/%7Etorkel/eget/godel/loeb.html seems broken (gives me a 403) but the Wayback Machine has a copy : http://web.archive.org/web/20081212195540/http://www.sm.luth.se/~torkel/eget/godel/loeb.html if someone is interested.

Gur snpg gung lbh crefbanyyl pnaabg cebir 2=1 qbrf abg zrna gung vg vf hacebinoyr. Vs lbh rire cebir (va CN) gung gurer vf ab cebbs (va CN) gung 2=1, gura lbh unir vaqrrq cebirq CN vapbafvfgrag.

Gur qrqhpgvba gurberz qbrf abg fgngr gung G ∪ {◻⊥→⊥} ⊢ ⊥, orpnhfr ◻ vf n cebinovyvgl cerqvpngr sbe G. Naq, va snpg, CN ∪ {◻⊥→⊥} vf whfg CN+Pba(CN), juvpu vf bs pbhefr pbafvfgrag.

I may not removed the flaw entirely, but I have definitely changed it into a less-obviously bad flaw. And also used Loeb's Theorem to derive Goedel's, or a close analogue.

The summary statement of Loeb is wrong. It is not the case that (◻X->X) -> X, it is only the case that ◻(◻X->X) -> ◻X. That is to say, that if (a proof of X implies X) is provable, then X is provable.

Using Deduction here, we get only ◻(~◻X) -> ◻X, which in English is "If it is provable that X is unprovable, then X is provable", or in other words "If PA is proved complete, it is proved inconsistent."

The download link for the Cartoon PDF Guide is outdated, it should be: http://yudkowsky.net/assets/pdf/LobsTheorem.pdf

Yrg'f frr, V xabj sbe n snpg gung ¬(CN ⊢ (◻P → P) → P), gung vf, gung guvf fhccbfrq "nccyvpngvba" bs gur Qrqhpgvba Gurberz qb Yöo'f Gurberz vf abg n gurberz bs CN.

Yöo'f Gurberz vgfrys vf whfg gung -

Buuuu tbg vg.

Yöo'f Gurberz fnlf gung vs CN ⊢ ◻P → P, gura CN ⊢ P; be, fvzcyl, gung CN ⊢ ◻(◻P → P) → ◻P. Gur Qrqhpgvba Gurberz fnlf gung sbe "ernfbanoyr" (va n pregnva frafr) qrqhpgvir flfgrzf va svefg-beqre ybtvp naq nal frg bs nkvbzf Δ, vs vg'f gur pnfr gung, sbe fbzr N naq O, Δ ∪ {N} ⊢ O, gura Δ ⊢ N → O. Ubjrire, vg vf abg gur pnfr gung CN ... (read more)

This is best understood in terms of models.  Prove doesn't assert that something is provable in our normal sense it asserts that there are numbers encoding a proof.  So what "PA |- Prov(phi) -> phi" really asserts is that any structure that satisfies the axioms of PA must believe that phi is true iff it believes there is a number coding a proof of phi.

But there are lots of structures other than the usual non-negative integers that satisfy PA.  Including ones with infinite 'numbers.'. In fact, anything consistent with the axioms of PA is g... (read more)