Theorem bj-babygodel 37306

Description: See the section header comments for the context.

The first hypothesis reads "𝜑 is true if and only if it is not provable in T" (and having this first hypothesis means that we can prove this fact in T). The wff 𝜑 is a formal version of the sentence "This sentence is not provable". The hard part of the proof of Gödel's theorem is to construct such a 𝜑, called a "Gödel–Rosser sentence", for a first-order theory T which is effectively axiomatizable and contains Robinson arithmetic, through Gödel diagonalization (this can be done in primitive recursive arithmetic). The second hypothesis means that ⊥ is not provable in T, that is, that the theory T is consistent (and having this second hypothesis means that we can prove in T that the theory T is consistent). The conclusion is the falsity, so having the conclusion means that T can prove the falsity, that is, T is inconsistent.

Therefore, taking the contrapositive, this theorem expresses that if a first-order theory is consistent (and one can prove in it that some formula is true if and only if it is not provable in it), then this theory does not prove its own consistency.

This proof is due to George Boolos, Gödel's Second Incompleteness Theorem Explained in Words of One Syllable, Mind, New Series, Vol. 103, No. 409 (January 1994), pp. 1--3.

(Contributed by BJ, 3-Apr-2019.)

Hypotheses

Ref	Expression
bj-babygodel.s	⊢ (𝜑 ↔ ¬ Prv 𝜑)
bj-babygodel.1	⊢ ¬ Prv ⊥

Assertion

Ref	Expression
bj-babygodel	⊢ ⊥

Proof of Theorem bj-babygodel

Step	Hyp	Ref	Expression
1		bj-babygodel.1	. . . 4 ⊢ ¬ Prv ⊥
2	1	ax-prv1 37301	. . 3 ⊢ Prv ¬ Prv ⊥
3		bj-babygodel.s	. . . . . . . . 9 ⊢ (𝜑 ↔ ¬ Prv 𝜑)
4	3	biimpi 219	. . . . . . . 8 ⊢ (𝜑 → ¬ Prv 𝜑)
5	4	prvlem1 37304	. . . . . . 7 ⊢ (Prv 𝜑 → Prv ¬ Prv 𝜑)
6		ax-prv3 37303	. . . . . . 7 ⊢ (Prv 𝜑 → Prv Prv 𝜑)
7		pm2.21 124	. . . . . . . 8 ⊢ (¬ Prv 𝜑 → (Prv 𝜑 → ⊥))
8	7	prvlem2 37305	. . . . . . 7 ⊢ (Prv ¬ Prv 𝜑 → (Prv Prv 𝜑 → Prv ⊥))
9	5, 6, 8	sylc 66	. . . . . 6 ⊢ (Prv 𝜑 → Prv ⊥)
10	9	con3i 155	. . . . 5 ⊢ (¬ Prv ⊥ → ¬ Prv 𝜑)
11	10, 3	sylibr 237	. . . 4 ⊢ (¬ Prv ⊥ → 𝜑)
12	11	prvlem1 37304	. . 3 ⊢ (Prv ¬ Prv ⊥ → Prv 𝜑)
13	2, 12, 9	mp2b 10	. 2 ⊢ Prv ⊥
14	13, 1	pm2.24ii 121	1 ⊢ ⊥

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ⊥wfal 1582  Prv cprvb 37300

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-prv1 37301  ax-prv2 37302  ax-prv3 37303

This proof depends on definitions:  df-bi 210

This theorem is used by: (None)