I went to the carnival and I met a fortune-teller. Everything she says comes true. Not only that, she told me that everything she says always comes true.
I said, "George Washington is my mother" and she said it wasn't true.
I said, "Well, if George Washington was my mother would you tell me so?" and she refused to say she would. She said she won't talk about what would be true if George Washingto was my mother, because George Washington is not my mother.
She says that everything she says comes true. She looked outside her little tent, and saw the sky was clear. She said, "If I tell you the sky is clear, then the sky is clear."
"But what if it was raining right now? If you told me it was raining, would it be raining?"
"I won't say what I'd tell you if it was raining right here right now, because it isn't raining."
"But if the sky is clear right now you'll tell me the sky is clear."
"Yes. Because it's true."
"So you'll only tell me that (if you say the sky is clear then the sky really is clear), when the sky really is clear?"
"Yes. I only tell you about true things. I don't tell you what I'd do if the world was some other way."
"Oh."
You can tell that J_Thomas2's "if" (which is the counterfactual "if") is not the "if" of material implication (which is what appears in Loeb's theorem) from the grammar: "if George Washington was my mother" rather than "if George Washington is my mother".
Lo! A cartoon proof of Löb's Theorem!
Löb's Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent. Marcello and I wanted to be able to see the truth of Löb's Theorem at a glance, so we doodled it out in the form of a cartoon. (An inability to trust assertions made by a proof system isomorphic to yourself, may be an issue for self-modifying AIs.)
It was while learning mathematical logic that I first learned to rigorously distinguish between X, the truth of X, the quotation of X, a proof of X, and a proof that X's quotation was provable.
The cartoon guide follows as an embedded Scribd document after the jump, or you can download as a PDF file. Afterward I offer a medium-hard puzzle to test your skill at drawing logical distinctions.
Cartoon Guide to Löb's ... by on Scribd
Cartoon Guide to Löb's Theorem - Upload a Document to Scribd
And now for your medium-hard puzzle:
The Deduction Theorem (look it up) states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F) is a theorem in classical logic.
Let ◻Z stand for the proposition "Z is provable". 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:
However, those familiar with the logic of material implication will realize that:
Applied to the above, this yields (not ◻C)->C.
That is, all statements which lack proofs are true.
I cannot prove that 2 = 1.
Therefore 2 = 1.
Can you exactly pinpoint the flaw?