I am stuck at part 2.2:
“So in particular, if we could prove that mathematics would never prove a contradiction,
then in fact mathematics would prove that contradiction”
I’ve spend 15 minutes on this, but still cannot see relation to löb’s theorem. Even though it seems like it should be obvious to attentive reader.
Could anyone please explain or link me to an explanation?
Suppose “mathemathics would never prove a contradiction”. We can write it out as ¬Provable(⊥). This is logically equivalent to Provable(⊥) → ⊥, and it also implies Provable(Provable(⊥) → ⊥) by the rules of provability. But Löb’s theorem expresses ∀ A (Provable(Provable(A) → A) → Provable(A)), which we can instantiate to Provable(Provable(⊥) → ⊥)→ Provable(⊥), and now we can apply modus ponens and our assumption to get a Provable(⊥).
Wasn’t Löb’s theorem ∀ A (Provable(Provable(A) → A) → Provable(A))? So you get Provable(⊥) directly, rather than passing through ⊥ first. This is good, as, of course, ⊥ is always false, even if it is provable.
Thanks for asking! I should add another sentence in that paragraph; the key step, as Kutta and Quill noted, is that “not A” is logically equivalent to “if A, then False”, and in particular the statement “2+2=5 is not provable” is logically equivalent to “if 2+2=5 were provable, then 2+2=5″, and then we can then run Löb’s Theorem.
I am stuck at part 2.2: “So in particular, if we could prove that mathematics would never prove a contradiction, then in fact mathematics would prove that contradiction”
I’ve spend 15 minutes on this, but still cannot see relation to löb’s theorem. Even though it seems like it should be obvious to attentive reader.
Could anyone please explain or link me to an explanation?
Suppose “mathemathics would never prove a contradiction”. We can write it out as ¬Provable(⊥). This is logically equivalent to Provable(⊥) → ⊥, and it also implies Provable(Provable(⊥) → ⊥) by the rules of provability. But Löb’s theorem expresses ∀ A (Provable(Provable(A) → A) → Provable(A)), which we can instantiate to Provable(Provable(⊥) → ⊥)→ Provable(⊥), and now we can apply modus ponens and our assumption to get a Provable(⊥).
Wasn’t Löb’s theorem ∀ A (Provable(Provable(A) → A) → Provable(A))? So you get Provable(⊥) directly, rather than passing through ⊥ first. This is good, as, of course, ⊥ is always false, even if it is provable.
You’re right, I mixed it up. Edited the comment.
Thanks for asking! I should add another sentence in that paragraph; the key step, as Kutta and Quill noted, is that “not A” is logically equivalent to “if A, then False”, and in particular the statement “2+2=5 is not provable” is logically equivalent to “if 2+2=5 were provable, then 2+2=5″, and then we can then run Löb’s Theorem.
Unless I have completely got something wrong, it should go like this:
I can’t prove a contradiction. I.e. I can’t prove false statements.
For all X: If I find a proof of X, X is true. I.e. For all X: L(X)
or all X: X (Löb’s Theorem).