Incompleteness

Incompleteness and Provability

Equation form expr-01a4acad621b4081

¬(x<n¯)\lnot(x < \num{n})

Read as: it is not the case that x is less than the numeral for n

Means: it is not the case that x is less than the numeral for n

1 occurrence in this chapter

Equation form expr-01d9c9487dee9dee

Q⊢¬RT\Th{Q} \Proves \lnot !R_{\Th{T}}

Read as: Q proves not R subscript T

Means: Q proves not R subscript T

1 occurrence in this chapter

Equation form expr-03f73897018b01e3

Q⊢A↔¬D(⌜A⌝)\Th{Q} \Proves !A \liff \lnot !D(\gn{!A})

Read as: Q proves that A is equivalent to not D of the numeral naming A

Means: Q proves that A is equivalent to not D of the numeral naming A

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: s

1 occurrence in this chapter

Equation form expr-051ef9392c1bafe5

Ddiag(⌜E(x)⌝,⌜A⌝)∀y(Ddiag(⌜E(x)⌝,y)→y=⌜A⌝).& !D_{\fn{diag}}(\gn{!E(x)}, \gn{!A}) \ollabel{repdiag1} \\ & \lforall[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \lif \eq[y][\gn{!A}])]. \ollabel{repdiag2}

Read as: First fact, diagonal representation one: D subscript diagonal holds of the numeral naming E of x and the numeral naming A. Second fact, diagonal representation two: for every y, if D subscript diagonal holds of the numeral naming E of x and y, then y equals the numeral naming A.

Means: First fact, diagonal representation one: D subscript diagonal holds of the numeral naming E of x and the numeral naming A. Second fact, diagonal representation two: for every y, if D subscript diagonal holds of the numeral naming E of x and y, then y equals the numeral naming A.

1 occurrence in this chapter

Equation form expr-067b51ca2dcf75b6

xByx B y

Read as: x B y

Means: x B y

2 occurrences in this chapter

Equation form expr-07fe2c64bb2b65e2

∃y(Ddiag(⌜E(x)⌝,y)∧B(y)).\lexists[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \land !B(y))].

Read as: there exists y such that D subscript diagonal holds of the numeral naming E of x and y, and B holds of y

Means: there exists y such that D subscript diagonal holds of the numeral naming E of x and y, and B holds of y

1 occurrence in this chapter

Equation form expr-088452eec157155c

T⊢A\Th{T} \Proves !A

Read as: T proves A

Means: T proves A

1 occurrence in this chapter

Equation form expr-095df5c5bb70f7b5

PrfT(x,y)\OPrf[\Th{T}](x,y)

Read as: the arithmetic proof formula for T applied to x and y

Means: the arithmetic proof formula for T applied to x and y

1 occurrence in this chapter

Equation form expr-09aaa5de3a74135c

T⊬ProvT(⌜⊥⌝)→⊥\Th{T} \Proves/ \OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse

Read as: T does not prove the implication: if the arithmetic provability formula for T holds of the numeral naming falsity, then falsity

Means: T does not prove the implication: if the arithmetic provability formula for T holds of the numeral naming falsity, then falsity

1 occurrence in this chapter

Equation form expr-09ef420258c72675

x≠n¯\eq/[x][\num{n}]

Read as: x is not equal to the numeral for n

Means: x is not equal to the numeral for n

1 occurrence in this chapter

Equation form expr-0a1fc396f621a67c

N⊨D(⌜A⌝)\Sat{N}{!D(\gn{!A})}

Read as: D of the numeral naming A is true in the standard natural number structure N

Means: D of the numeral naming A is true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-0b85416a66e796ed

T⊢⊥\Th{T} \Proves \lfalse

Read as: T proves falsity

Means: T proves falsity

1 occurrence in this chapter

Equation form expr-0e5a8f4729edac64

B⊆X¯B \subseteq \Complement{X}

Read as: B is a subset of the complement of X

Means: B is a subset of the complement of X

1 occurrence in this chapter

Equation form expr-1088bfc03a6c5877

ConPA→¬ProvPA(⌜GPA⌝).\OCon[\Th{PA}] \lif \lnot \OProv[\Th{PA}](\gn{!G_\Th{PA}}).

Read as: if the arithmetic consistency sentence for P A holds, then the arithmetic provability formula for P A does not hold of the numeral naming G subscript P A

Means: if the arithmetic consistency sentence for P A holds, then the arithmetic provability formula for P A does not hold of the numeral naming G subscript P A

1 occurrence in this chapter

Equation form expr-1165c59bb9054e7b

T(x)T(x)

Read as: T of x

Means: T of x

1 occurrence in this chapter

Equation form expr-11baa595827a4e0f

ω\omega

Read as: omega

Means: omega

18 occurrences in this chapter

Equation form expr-13bcf9d25c75255b

G!G

Read as: G

Means: G

1 occurrence in this chapter

Equation form expr-1693aa02ef04531f

n¯<x∧RefT(n¯,⌜RT⌝)\num{n} < x \land \ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})

Read as: the numeral for n is less than x, and the arithmetic refutation formula for T holds of the numeral for n and the numeral naming R subscript T

Means: the numeral for n is less than x, and the arithmetic refutation formula for T holds of the numeral for n and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-182f11c211a4c8b2

PrfT(x,y)\Prf[\Th{T}](x, y)

Read as: the external proof coding relation for T applied to x and y

Means: the external proof coding relation for T applied to x and y

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

5 occurrences in this chapter

Equation form expr-1cdad80140794880

∃xPrfT(x,y)\lexists[x][\OPrf[\Th{T}](x,y)]

Read as: there exists x such that the arithmetic proof formula for T holds of x and y

Means: there exists x such that the arithmetic proof formula for T holds of x and y

1 occurrence in this chapter

Equation form expr-1ce52cdbbfbc4db3

E(⌜E(x)⌝)!E(\gn{!E(x)})

Read as: E applied to the numeral naming the formula E of x

Means: E applied to the numeral naming the formula E of x

6 occurrences in this chapter

Equation form expr-1e870888f28149ec

¬PrfT(0¯,⌜GT⌝),¬PrfT(1¯,⌜GT⌝),¬PrfT(2¯,⌜GT⌝),…\lnot \OPrf[\Th{T}](\num 0, \gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 1, \gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 2, \gn{!G_\Th{T}}), \dots

Read as: the arithmetic proof formula for T does not hold of the numeral zero and the numeral naming G subscript T; does not hold of the numeral one and the numeral naming G subscript T; does not hold of the numeral two and the numeral naming G subscript T; and likewise for every further natural number

Means: the arithmetic proof formula for T does not hold of the numeral zero and the numeral naming G subscript T; does not hold of the numeral one and the numeral naming G subscript T; does not hold of the numeral two and the numeral naming G subscript T; and likewise for every further natural number

1 occurrence in this chapter

Equation form expr-1f57909a98830662

PrfT(x,y)\Prf[\Th{T}](x,y)

Read as: the external proof coding relation for T applied to x and y

Means: the external proof coding relation for T applied to x and y

4 occurrences in this chapter

Equation form expr-247683706aa86ece

ConPA→GPA\OCon[\Th{PA}] \lif !G_\Th{PA}

Read as: if the arithmetic consistency sentence for P A holds, then G subscript P A

Means: if the arithmetic consistency sentence for P A holds, then G subscript P A

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

1 occurrence in this chapter

Equation form expr-2531406eac454cb4

Q⊢PrfT(n¯,⌜RT⌝)\Th{Q} \Proves \OPrf[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})

Read as: Q proves that the arithmetic proof formula for T holds of the numeral for n and the numeral naming R subscript T

Means: Q proves that the arithmetic proof formula for T holds of the numeral for n and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-257b58b97ec39266

¬GT\lnot !G_\Th{T}

Read as: not G subscript T

Means: not G subscript T

6 occurrences in this chapter

Equation form expr-259072e6c653cc56

f(x)f(x)

Read as: f of x

Means: f of x

1 occurrence in this chapter

Equation form expr-25deb7ee1dccfd65

Ddiag(x,y)!D_{\fn{diag}}(x,y)

Read as: D subscript diagonal of x and y

Means: D subscript diagonal of x and y

1 occurrence in this chapter

Equation form expr-278d6de731f4e487

RefT(x,y)\Refut[\Th{T}](x, y)

Read as: the external refutation coding relation for T applied to x and y

Means: the external refutation coding relation for T applied to x and y

1 occurrence in this chapter

Equation form expr-27b062f213c21201

¬ProvT(y)\lnot \OProv[\Th{T}](y)

Read as: the negation of the arithmetic provability formula for T at y

Means: the negation of the arithmetic provability formula for T at y

1 occurrence in this chapter

Equation form expr-28e8ca6f819f726b

k<nk < n

Read as: k is less than n

Means: k is less than n

2 occurrences in this chapter

Equation form expr-28f3d698fa6e03a9

Q⊢RT↔¬RProvT(⌜RT⌝).\Th{Q} \Proves !R_\Th{T} \liff \lnot \ORProv[\Th{T}](\gn{!R_\Th{T}}). \ollabel{RT}

Read as: Q proves that R subscript T is equivalent to the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T

Means: Q proves that R subscript T is equivalent to the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-2b55d4329be47f77

RT!R_{\Th{T}}

Read as: R subscript T

Means: R subscript T

2 occurrences in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

10 occurrences in this chapter

Equation form expr-3173379adfb672b6

RefT\Refut[\Th{T}]

Read as: the external refutation coding relation for T

Means: the external refutation coding relation for T

1 occurrence in this chapter

Equation form expr-317b05c9c7f09b17

T⊬ConT\Th{T} \Proves/ \OCon[\Th{T}]

Read as: T does not prove its arithmetic consistency sentence

Means: T does not prove its arithmetic consistency sentence

1 occurrence in this chapter

Equation form expr-31cb57483f878acc

PA⊢0=1\Th{PA} \Proves \eq[0][1]

Read as: P A proves that zero equals one

Means: P A proves that zero equals one

1 occurrence in this chapter

Equation form expr-32bf26f266ac3169

¬A(1¯)\lnot !A(\num 1)

Read as: not A of the numeral one

Means: not A of the numeral one

1 occurrence in this chapter

Equation form expr-32f1d5d41e9d25a8

diag(#E(x)#)=#A#\fn{diag}(\Gn{!E(x)}) = \Gn{!A}

Read as: the diagonal function applied to the Goedel number of E of x equals the Goedel number of A

Means: the diagonal function applied to the Goedel number of E of x equals the Goedel number of A

1 occurrence in this chapter

Equation form expr-35ad5b7ab055aabd

ConPA\OCon[\Th{PA}]

Read as: the arithmetic consistency sentence for P A

Means: the arithmetic consistency sentence for P A

6 occurrences in this chapter

Equation form expr-3b397d4a86559ab8

∃xPrfT(x,⌜GT⌝)\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]

Read as: there exists x such that the arithmetic proof formula for T holds of x and the numeral naming G subscript T

Means: there exists x such that the arithmetic proof formula for T holds of x and the numeral naming G subscript T

2 occurrences in this chapter

Equation form expr-3bf1c7fe7b8af6ec

¬A(0¯)\lnot !A(\num 0)

Read as: not A of the numeral zero

Means: not A of the numeral zero

1 occurrence in this chapter

Equation form expr-3c5eac973e56bff0

Q⊢RefT(⌜δ⌝,⌜A⌝)\Th{Q} \Proves \ORefut[\Th{T}](\gn{\delta}, \gn{!A})

Read as: Q proves that the arithmetic refutation formula for T holds of the numeral naming derivation delta and the numeral naming A

Means: Q proves that the arithmetic refutation formula for T holds of the numeral naming derivation delta and the numeral naming A

1 occurrence in this chapter

Equation form expr-3d2df79065b6f165

Q\Th{Q}

Read as: Q

Means: Q

43 occurrences in this chapter

Equation form expr-3f79bb7b435b0532

ee

Read as: e

Means: e

1 occurrence in this chapter

Equation form expr-4026b49cee6e3826

RProvT(y)\ORProv_T(y)

Read as: the arithmetic Rosser provability formula subscript T applied to y

Means: the arithmetic Rosser provability formula subscript T applied to y

1 occurrence in this chapter

Equation form expr-4229d41b9cd49550

N⊨A(n¯1,…,n¯k)\Sat{N}{!A(\num n_1,\dots,\num n_k)}

Read as: A of the numerals for n subscript one through n subscript k is true in the standard natural number structure N

Means: A of the numerals for n subscript one through n subscript k is true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-425040f7e127e267

Q⊢¬PrfT(k¯,⌜RT⌝)\Th{Q} \Proves \lnot \OPrf[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})

Read as: Q proves that the arithmetic proof formula for T does not hold of the numeral for k and the numeral naming R subscript T

Means: Q proves that the arithmetic proof formula for T does not hold of the numeral for k and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-434e68b9e3e31cc8

n1,…,nkn_1,\dots,n_k

Read as: n subscript one through n subscript k

Means: n subscript one through n subscript k

1 occurrence in this chapter

Equation form expr-43679b0ce7790e4e

T⊢¬ProvT(⌜G⌝)\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G})

Read as: T proves the negation of its arithmetic provability formula at the numeral naming G

Means: T proves the negation of its arithmetic provability formula at the numeral naming G

1 occurrence in this chapter

Equation form expr-438055240a892193

¬RProvT(⌜RT⌝)\lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}})

Read as: the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T

Means: the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-4392b7176357df2d

#E(x)#¯\num{\Gn{!E(x)}}

Read as: the numeral for the Goedel number of the formula E of x

Means: the numeral for the Goedel number of the formula E of x

2 occurrences in this chapter

Equation form expr-44bd7ae60f478fae

HH

Read as: H

Means: H

2 occurrences in this chapter

Equation form expr-458830ddc1a31be3

Q∪{¬GQ}\Th{Q} \cup \{\lnot !G_\Th{Q}\}

Read as: Q together with the sentence not G subscript Q

Means: Q together with the sentence not G subscript Q

1 occurrence in this chapter

Equation form expr-45f80f1bb02ff5da

GT!G_\Th{T}

Read as: G subscript T

Means: G subscript T

8 occurrences in this chapter

Equation form expr-4834eb200f3543c0

T⊢A↔B(⌜A⌝)\Th{T} \Proves!A \liff !B(\gn{!A})

Read as: T proves that A is equivalent to B of the numeral naming A

Means: T proves that A is equivalent to B of the numeral naming A

1 occurrence in this chapter

Equation form expr-4902d0ed1938bce7

∃z(z<x∧RefT(z,⌜RT⌝))\lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))]

Read as: there exists z such that z is less than x and the arithmetic refutation formula for T holds of z and the numeral naming R subscript T

Means: there exists z such that z is less than x and the arithmetic refutation formula for T holds of z and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-494983d0a3746f00

P\Th{P}

Read as: theory P

Means: theory P

1 occurrence in this chapter

Equation form expr-4a3fc4ac2ca25c0f

PA⊢ProvPA(⌜A⌝)\Th{PA} \Proves \OProv[\Th{PA}](\gn{!A})

Read as: P A proves that its arithmetic provability formula holds of the numeral naming A

Means: P A proves that its arithmetic provability formula holds of the numeral naming A

2 occurrences in this chapter

Equation form expr-4a7d03de256e59a9

¬RT\lnot !R_\Th{T}

Read as: not R subscript T

Means: not R subscript T

1 occurrence in this chapter

Equation form expr-4b4a02834fefdcef

T⊢ProvT(⌜⊥⌝)→⊥\Th{T} \Proves \OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse

Read as: T proves the implication: if its arithmetic provability formula holds of the numeral naming falsity, then falsity

Means: T proves the implication: if its arithmetic provability formula holds of the numeral naming falsity, then falsity

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: X

Means: X

17 occurrences in this chapter

Equation form expr-4d9e454879188f69

T⊬⊥\Th{T} \Proves/ \lfalse

Read as: T does not prove falsity

Means: T does not prove falsity

1 occurrence in this chapter

Equation form expr-4f508a460886d5a5

B(diag(x))!B(\Obj{diag}(x))

Read as: B of the value of the object language diagonal function symbol at x

Means: B of the value of the object language diagonal function symbol at x

2 occurrences in this chapter

Equation form expr-4f8646cdbfa68bec

diag(#B(diag(x))#)=#B(diag(⌜B(diag(x))⌝))#=#A#.\fn{diag}(\Gn{!B(\Obj{diag}(x))}) & = \Gn{!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))} \\ & = \Gn{!A}.

Read as: The diagonal function applied to the Goedel number of the formula B of diagonal of x equals the Goedel number of the following formula: B of diagonal of the numeral naming B of diagonal of x. End formula. This equals the Goedel number of A.

Means: The diagonal function applied to the Goedel number of the formula B of diagonal of x equals the Goedel number of the following formula: B of diagonal of the numeral naming B of diagonal of x. End formula. This equals the Goedel number of A.

1 occurrence in this chapter

Equation form expr-502aee465bebc80f

ProvPA(y)\OProv[\Th{PA}](y)

Read as: the arithmetic provability formula for P A applied to y

Means: the arithmetic provability formula for P A applied to y

5 occurrences in this chapter

Equation form expr-50bf4008855e1923

T⊬¬RT\Th{T} \Proves/ \lnot !R_{\Th{T}}

Read as: T does not prove the negation of R subscript T

Means: T does not prove the negation of R subscript T

1 occurrence in this chapter

Equation form expr-5151f6167204b906

Ddiag(⌜E(x)⌝,⌜A⌝)∧B(⌜A⌝).It follows that∃y(Ddiag(⌜E(x)⌝,y)∧B(y)).& !D_{\fn{diag}}(\gn{!E(x)}, \gn{!A}) \land !B(\gn{!A}). \intertext{It follows that} & \lexists[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \land !B(y))].

Read as: D subscript diagonal holds of the numeral naming E of x and the numeral naming A, and B holds of the numeral naming A. It follows that there exists y such that D subscript diagonal holds of the numeral naming E of x and y, and B holds of y.

Means: D subscript diagonal holds of the numeral naming E of x and the numeral naming A, and B holds of the numeral naming A. It follows that there exists y such that D subscript diagonal holds of the numeral naming E of x and y, and B holds of y.

1 occurrence in this chapter

Equation form expr-54afe41b5accae0c

T⊢¬RT\Th{T} \Proves \lnot !R_{\Th{T}}

Read as: T proves the negation of R subscript T

Means: T proves the negation of R subscript T

1 occurrence in this chapter

Equation form expr-54c2704ad08b2451

A→(B→C),A→B⊢A→C!A \lif (!B \lif !C), !A \lif !B \Proves !A \lif !C

Read as: from the premises if A then if B then C, and if A then B, one can derive if A then C

Means: from the premises if A then if B then C, and if A then B, one can derive if A then C

1 occurrence in this chapter

Equation form expr-559aead08264d579

AA

Read as: A

Means: A

3 occurrences in this chapter

Equation form expr-55fac4ccbde9168f

ProvT(x)\OProv[\Th{T}](x)

Read as: the arithmetic provability formula for T applied to x

Means: the arithmetic provability formula for T applied to x

1 occurrence in this chapter

Equation form expr-56b59a3b3dc11eaf

H!H

Read as: H

Means: H

3 occurrences in this chapter

Equation form expr-57781442869db01a

PrfT(x,not(y))\Prf[\Th{T}](x, \fn{not}(y))

Read as: the external proof coding relation for T applied to x and the result of the negation coding function at y

Means: the external proof coding relation for T applied to x and the result of the negation coding function at y

1 occurrence in this chapter

Equation form expr-5b63a60fdb499c3a

N\Struct{N}

Read as: the standard natural number structure N

Means: the standard natural number structure N

9 occurrences in this chapter

Equation form expr-5ba10bcb5519da63

ProvT(⌜H⌝)→H\OProv[\Th{T}](\gn{!H}) \lif !H

Read as: if the arithmetic provability formula for T holds of the numeral naming H, then H

Means: if the arithmetic provability formula for T holds of the numeral naming H, then H

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

1 occurrence in this chapter

Equation form expr-5f089873be7cb173

G↔¬Prov(⌜G⌝)G is a Gödel sentenceG→¬Prov(⌜G⌝)from step G two, oneG→(Prov(⌜G⌝)→⊥)from step G two, two by logicProv(⌜G→(Prov(⌜G⌝)→⊥)⌝)by from step G two, three by condition P1Prov(⌜G⌝)→Prov(⌜(Prov(⌜G⌝)→⊥)⌝)from step G two, four by condition P2Prov(⌜G⌝)→(Prov(⌜Prov(⌜G⌝)⌝)→Prov(⌜⊥⌝))from step G two, five by condition P2 and logicProv(⌜G⌝)→Prov(⌜Prov(⌜G⌝)⌝)by P3Prov(⌜G⌝)→Prov(⌜⊥⌝)from step G two, six and step G two, seven by logicCon→¬Prov(⌜G⌝)contraposition of step G two, eight and Con≡¬Prov(⌜⊥⌝)Con→Gfrom step G two, one and step G two, nine by logic& !G \liff \lnot \OProv(\gn{!G}) \ollabel{G2-1}\\ & \qquad\text{$!G$ is a G\"odel sentence}\notag \\ & !G \lif \lnot \OProv(\gn{!G}) \ollabel{G2-2}\\ & \qquad\text{from \olref{G2-1}} \notag\\ & !G \lif (\OProv(\gn{!G}) \lif \lfalse) \ollabel{G2-3}\\ & \qquad\text{from \olref{G2-2} by logic}\notag\\ & \OProv(\gn{ !G \lif (\OProv(\gn{!G}) \lif \lfalse) }) \ollabel{G2-4}\\ & \qquad\text{by from \olref{G2-3} by condition P1} \notag\\ & \OProv(\gn{!G}) \lif \OProv(\gn{ (\OProv(\gn{!G}) \lif \lfalse) }) \ollabel{G2-5}\\ & \qquad\text{from \olref{G2-4} by condition P2} \notag\\ & \OProv(\gn{!G}) \lif (\OProv(\gn{\OProv(\gn{!G})}) \lif \OProv(\gn{\lfalse})) \ollabel{G2-6}\\ & \qquad\text{from \olref{G2-5} by condition P2 and logic} \notag\\ & \OProv(\gn{!G}) \lif \OProv(\gn{\OProv(\gn{!G})}) \ollabel{G2-7}\\ & \qquad\text{by P3} \notag\\ & \OProv(\gn{!G}) \lif \OProv(\gn{\lfalse}) \ollabel{G2-8}\\ & \qquad \text{from \olref{G2-6} and \olref{G2-7} by logic}\notag\\ & \OCon \lif \lnot \OProv(\gn{!G}) \ollabel{G2-9}\\ & \qquad\text{contraposition of \olref{G2-8} and $\OCon \ident \lnot \OProv(\gn{\lfalse})$}\notag \\ & \OCon \lif !G \notag\\ & \qquad\text{from \olref{G2-1} and \olref{G2-9} by logic}\notag

Read as: Derivation inside P A. Prov denotes the arithmetic provability formula for P A, and Con its arithmetic consistency sentence; the source suppresses the P A subscripts. Line G two, one. G is equivalent to not Prov of the numeral naming G. Reason: G is a Goedel sentence. Line G two, two. If G then not Prov of the numeral naming G. From step G two, one. Line G two, three. If G then, if Prov holds of the numeral naming G, falsity. From step G two, two by logic. Line G two, four. Prov holds of the numeral naming this entire formula: if G then, if Prov holds of the numeral naming G, falsity. End named formula. From step G two, three by condition P one. Line G two, five. If Prov holds of the numeral naming G, then Prov holds of the numeral naming this formula: if Prov holds of the numeral naming G, then falsity. End named formula. From step G two, four by condition P two. Line G two, six. If Prov holds of the numeral naming G, then, if Prov holds of the numeral naming the formula Prov of the numeral naming G, then Prov holds of the numeral naming falsity. From step G two, five by condition P two and logic. Line G two, seven. If Prov holds of the numeral naming G, then Prov holds of the numeral naming the formula Prov of the numeral naming G. By condition P three. Line G two, eight. If Prov holds of the numeral naming G, then Prov holds of the numeral naming falsity. From step G two, six and step G two, seven by logic. Line G two, nine. If Con then not Prov of the numeral naming G. By contraposition of step G two, eight, using the definition of Con as not Prov of the numeral naming falsity. Final step. If Con then G. From step G two, one and step G two, nine by logic. End derivation.

Means: Derivation inside P A. Prov denotes the arithmetic provability formula for P A, and Con its arithmetic consistency sentence; the source suppresses the P A subscripts. Line G two, one. G is equivalent to not Prov of the numeral naming G. Reason: G is a Goedel sentence. Line G two, two. If G then not Prov of the numeral naming G. From step G two, one. Line G two, three. If G then, if Prov holds of the numeral naming G, falsity. From step G two, two by logic. Line G two, four. Prov holds of the numeral naming this entire formula: if G then, if Prov holds of the numeral naming G, falsity. End named formula. From step G two, three by condition P one. Line G two, five. If Prov holds of the numeral naming G, then Prov holds of the numeral naming this formula: if Prov holds of the numeral naming G, then falsity. End named formula. From step G two, four by condition P two. Line G two, six. If Prov holds of the numeral naming G, then, if Prov holds of the numeral naming the formula Prov of the numeral naming G, then Prov holds of the numeral naming falsity. From step G two, five by condition P two and logic. Line G two, seven. If Prov holds of the numeral naming G, then Prov holds of the numeral naming the formula Prov of the numeral naming G. By condition P three. Line G two, eight. If Prov holds of the numeral naming G, then Prov holds of the numeral naming falsity. From step G two, six and step G two, seven by logic. Line G two, nine. If Con then not Prov of the numeral naming G. By contraposition of step G two, eight, using the definition of Con as not Prov of the numeral naming falsity. Final step. If Con then G. From step G two, one and step G two, nine by logic. End derivation.

1 occurrence in this chapter

Equation form expr-6193864491e4d7b1

N⊨A\Sat{N}{!A}

Read as: A is true in the standard natural number structure N

Means: A is true in the standard natural number structure N

3 occurrences in this chapter

Equation form expr-6211fc6de8737bd4

Q⊢RT↔¬RProvT(⌜RT⌝),and since T extends Q, it suffices to show thatQ⊢¬RProvT(⌜RT⌝).\Th{Q} & \Proves !R_{\Th{T}} \liff \lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}}), \intertext{and since $\Th{T}$ extends~$\Th{Q}$, it suffices to show that} \Th{Q} & \Proves \lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}}).

Read as: Q proves that R subscript T is equivalent to the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T. And since T extends Q, it suffices to show that Q proves the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T.

Means: Q proves that R subscript T is equivalent to the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T. And since T extends Q, it suffices to show that Q proves the negation of the arithmetic Rosser provability formula for T at the numeral naming R subscript T.

1 occurrence in this chapter

Equation form expr-625644a4cbf2f7ac

B(⌜A⌝)!B(\gn{!A})

Read as: B of the numeral naming A

Means: B of the numeral naming A

2 occurrences in this chapter

Equation form expr-628a097f108c4bcd

Q⊢∀z(z<n¯→¬RefT(z,⌜RT⌝))\Th{Q} \Proves \lforall[z][(z < \num{n} \lif \lnot \ORefut[\Th{T}](z, \gn{!R_{\Th{T}}}))]

Read as: Q proves that for every z, if z is less than the numeral for n, then the arithmetic refutation formula for T does not hold of z and the numeral naming R subscript T

Means: Q proves that for every z, if z is less than the numeral for n, then the arithmetic refutation formula for T does not hold of z and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: m

1 occurrence in this chapter

Equation form expr-64e1d9b6e1a58e62

not(x)\fn{not}(x)

Read as: the negation coding function applied to x

Means: the negation coding function applied to x

2 occurrences in this chapter

Equation form expr-652365313fd3049c

E(n¯)!E(\num{n})

Read as: E of the numeral for n

Means: E of the numeral for n

1 occurrence in this chapter

Equation form expr-65e250c2f2829fd8

T(e,x,s)T(e,x,s)

Read as: T of e, x, and s

Means: T of e, x, and s

1 occurrence in this chapter

Equation form expr-673d9af278073bf5

N⊨A↔¬D(⌜A⌝)\Sat{N}{!A \liff \lnot !D(\gn{!A})}

Read as: the equivalence between A and not D of the numeral naming A is true in the standard natural number structure N

Means: the equivalence between A and not D of the numeral naming A is true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-67d1828b5b9fb5e1

PA⊢ProvPA(⌜A→B⌝)→(ProvPA(⌜A⌝)→ProvPA(⌜B⌝)).\Th{PA} \Proves \OProv[\Th{PA}](\gn{!A \lif !B}) \lif (\OProv[\Th{PA}](\gn{!A}) \lif \OProv[\Th{PA}](\gn{!B})).

Read as: P A proves the following implication. If its arithmetic provability formula holds of the numeral naming the implication from A to B, then, if that provability formula holds of the numeral naming A, it also holds of the numeral naming B. End implication.

Means: P A proves the following implication. If its arithmetic provability formula holds of the numeral naming the implication from A to B, then, if that provability formula holds of the numeral naming A, it also holds of the numeral naming B. End implication.

1 occurrence in this chapter

Equation form expr-68a990b9fde35c0e

X¯\Complement{X}

Read as: the complement of X

Means: the complement of X

1 occurrence in this chapter

Equation form expr-692dc9a1552174fa

x∈ℕx \in \Nat

Read as: x is a natural number

Means: x is a natural number

1 occurrence in this chapter

Equation form expr-6932ad1ef5bf7d96

¬RT\lnot !R_{\Th{T}}

Read as: not R subscript T

Means: not R subscript T

2 occurrences in this chapter

Equation form expr-6a5cba0f14471f03

R(n1,…,nk)R(n_1,\dots,n_k)

Read as: R of n subscript one through n subscript k

Means: R of n subscript one through n subscript k

1 occurrence in this chapter

Equation form expr-6ae99f2c728136b3

(A(0)∧∀x(A(x)→A(x′)))→∀xA(x)(!A(0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)]

Read as: if A holds of zero and, for every x, A of x implies A of the successor of x, then A holds of every x

Means: if A holds of zero and, for every x, A of x implies A of the successor of x, then A holds of every x

1 occurrence in this chapter

Equation form expr-6b383bdb20d3c220

T⊬GT\Th{T} \Proves/ !G_\Th{T}

Read as: T does not prove G subscript T

Means: T does not prove G subscript T

2 occurrences in this chapter

Equation form expr-6cd2bedca3cc927c

¬(x=0¯∨x=1¯∨…∨x=n−1¯)\lnot(\eq[x][\num{0}] \lor \eq[x][\num{1}] \lor \dots \lor \eq[x][\num{n-1}])

Read as: it is not the case that x equals the numeral zero, or the numeral one, or any of the successive numerals through the numeral for n minus one

Means: it is not the case that x equals the numeral zero, or the numeral one, or any of the successive numerals through the numeral for n minus one

1 occurrence in this chapter

Equation form expr-6eef739850924c44

Q⊢¬RefT(k¯,⌜RT⌝)\Th{Q} \Proves \lnot \ORefut[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})

Read as: Q proves that the arithmetic refutation formula for T does not hold of the numeral for k and the numeral naming R subscript T

Means: Q proves that the arithmetic refutation formula for T does not hold of the numeral for k and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-725852a72a62e51b

⌜A⌝\gn{!A}

Read as: the numeral naming A

Means: the numeral naming A

4 occurrences in this chapter

Equation form expr-72dfcfb0c470ac25

LL

Read as: L

Means: L

2 occurrences in this chapter

Equation form expr-76f5a09f92082e90

PrfPA(x,y)\OPrf[\Th{PA}](x,y)

Read as: the arithmetic proof formula for P A applied to x and y

Means: the arithmetic proof formula for P A applied to x and y

1 occurrence in this chapter

Equation form expr-770598d31dafe8d2

D(y)!D(y)

Read as: D of y

Means: D of y

1 occurrence in this chapter

Equation form expr-7882d4102bf25566

B(diag(⌜B(diag(x))⌝))!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))

Read as: B of diagonal of the numeral naming the formula B of diagonal of x

Means: B of diagonal of the numeral naming the formula B of diagonal of x

2 occurrences in this chapter

Equation form expr-78e82f106e192900

T⊢ProvT(⌜A⌝)→AT \Proves \OProv[\Th{T}](\gn{!A}) \lif !A

Read as: T proves the implication: if its arithmetic provability formula holds of the numeral naming A, then A

Means: T proves the implication: if its arithmetic provability formula holds of the numeral naming A, then A

1 occurrence in this chapter

Equation form expr-79d4c7f9c8579543

ℕ\Nat

Read as: the natural numbers

Means: the natural numbers

1 occurrence in this chapter

Equation form expr-7a0ae23759d98097

DT!D_T

Read as: D subscript T

Means: D subscript T

1 occurrence in this chapter

Equation form expr-7a10064bdd4bb243

RefT(x,y)\ORefut[\Th{T}](x, y)

Read as: the arithmetic refutation formula for T applied to x and y

Means: the arithmetic refutation formula for T applied to x and y

1 occurrence in this chapter

Equation form expr-7a465cca1b87f2b2

PrfT(x,⌜RT⌝)\OPrf[\Th{T}](x, \gn{!R_{\Th{T}}})

Read as: the arithmetic proof formula for T applied to x and the numeral naming R subscript T

Means: the arithmetic proof formula for T applied to x and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-7b597906c930922e

PrfPA(x,y)\Prf[\Th{PA}](x,y)

Read as: the external proof coding relation for P A applied to x and y

Means: the external proof coding relation for P A applied to x and y

1 occurrence in this chapter

Equation form expr-7c8c4b127e21d1e7

∃y(Ddiag(x,y)∧B(y))\lexists[y][(!D_{\fn{diag}}(x,y) \land !B(y))]

Read as: there exists y such that D subscript diagonal holds of x and y, and B holds of y

Means: there exists y such that D subscript diagonal holds of x and y, and B holds of y

2 occurrences in this chapter

Equation form expr-7d2d7f2c3e783596

∀x(PrfT(x,⌜RT⌝)→∃z(z<x∧RefT(z,⌜RT⌝))).\lforall[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \lif \lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])].

Read as: for every x, if the arithmetic proof formula for T holds of x and the numeral naming R subscript T, then there exists z less than x such that the arithmetic refutation formula for T holds of z and the numeral naming R subscript T

Means: for every x, if the arithmetic proof formula for T holds of x and the numeral naming R subscript T, then there exists z less than x such that the arithmetic refutation formula for T holds of z and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-7e0d610f4d4eb867

D↔B(⌜D⌝)!D \liff !B(\gn{!D})

Read as: D is equivalent to B of the numeral naming D

Means: D is equivalent to B of the numeral naming D

1 occurrence in this chapter

Equation form expr-7e8d9ddb1a4c9286

n=#E(x)#n = \Gn{!E(x)}

Read as: n equals the Goedel number of the formula E of x

Means: n equals the Goedel number of the formula E of x

1 occurrence in this chapter

Equation form expr-7f0e64e1cce77e7c

A≡G!A \ident !G

Read as: A is syntactically identical to G

Means: A is syntactically identical to G

1 occurrence in this chapter

Equation form expr-7f2dcd759f041fd9

T⊢ProvT(⌜H⌝)↔H.\Th{T} \Proves \OProv[\Th{T}](\gn{!H}) \liff !H.

Read as: T proves that its arithmetic provability formula at the numeral naming H is equivalent to H

Means: T proves that its arithmetic provability formula at the numeral naming H is equivalent to H

1 occurrence in this chapter

Equation form expr-819391d2f4afc66b

N⊨¬D(⌜A⌝)\Sat{N}{\lnot !D(\gn{!A})}

Read as: not D of the numeral naming A is true in the standard natural number structure N

Means: not D of the numeral naming A is true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-81aa5a490db29cc9

A(x)!A(x)

Read as: A of x

Means: A of x

1 occurrence in this chapter

Equation form expr-8203022b3a39d71a

y=⌜A⌝y = \gn{!A}

Read as: y equals the numeral naming A

Means: y equals the numeral naming A

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

28 occurrences in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

3 occurrences in this chapter

Equation form expr-87f0ba94ea1a94d4

⊢¬A↔(A→⊥)\Proves \lnot!A \liff (!A\lif \lfalse)

Read as: logic proves that not A is equivalent to the implication from A to falsity

Means: logic proves that not A is equivalent to the implication from A to falsity

1 occurrence in this chapter

Equation form expr-8870f3b9517f01a8

ProvT(y)→A\OProv[\Th{T}](y) \lif !A

Read as: if the arithmetic provability formula for T holds of y, then A

Means: if the arithmetic provability formula for T holds of y, then A

2 occurrences in this chapter

Equation form expr-89801fb4bf128952

B≡⊥!B \ident \lfalse

Read as: B is syntactically identical to falsity

Means: B is syntactically identical to falsity

1 occurrence in this chapter

Equation form expr-89906b1475218964

ProvT\OProv[\Th{T}]

Read as: the arithmetic provability formula for T

Means: the arithmetic provability formula for T

1 occurrence in this chapter

Equation form expr-89a2522c1609426c

Q⊢RefT(n¯,⌜RT⌝)\Th{Q} \Proves \ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})

Read as: Q proves that the arithmetic refutation formula for T holds of the numeral for n and the numeral naming R subscript T

Means: Q proves that the arithmetic refutation formula for T holds of the numeral for n and the numeral naming R subscript T

2 occurrences in this chapter

Equation form expr-8c1856c0bd3610dd

T⊢AT \Proves !A

Read as: T proves A

Means: T proves A

2 occurrences in this chapter

Equation form expr-8d56f4158b0c9a30

ProvT(⌜GT⌝)\OProv[\Th{T}](\gn{!G_\Th{T}})

Read as: the arithmetic provability formula for T at the numeral naming G subscript T

Means: the arithmetic provability formula for T at the numeral naming G subscript T

1 occurrence in this chapter

Equation form expr-8da51c116dcd62bf

B(y)!B(y)

Read as: B of y

Means: B of y

2 occurrences in this chapter

Equation form expr-8e1d660cc8cb601c

PrfT\OPrf[\Th{T}]

Read as: the arithmetic proof formula for T

Means: the arithmetic proof formula for T

1 occurrence in this chapter

Equation form expr-8faa1b82ee1be916

RT!R_\Th{T}

Read as: R subscript T

Means: R subscript T

2 occurrences in this chapter

Equation form expr-90112d5a01eab86d

A⊆XA \subseteq X

Read as: A is a subset of X

Means: A is a subset of X

1 occurrence in this chapter

Equation form expr-91f92997b806bb77

Q⊢A↔B(⌜A⌝)\Th{Q} \Proves !A \liff !B(\gn{!A})

Read as: Q proves that A is equivalent to B of the numeral naming A

Means: Q proves that A is equivalent to B of the numeral naming A

2 occurrences in this chapter

Equation form expr-924eb9fa8620a34f

GPA!G_\Th{PA}

Read as: G subscript P A

Means: G subscript P A

7 occurrences in this chapter

Equation form expr-927b31ab643b6045

Ddiag!D_{\fn{diag}}

Read as: D subscript diagonal

Means: D subscript diagonal

1 occurrence in this chapter

Equation form expr-9497c70d26fff743

PrfT\Prf[\Th{T}]

Read as: the external proof coding relation for T

Means: the external proof coding relation for T

1 occurrence in this chapter

Equation form expr-95e396d54f31d77a

T⊢¬ProvT(⌜G⌝)↔G.\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G}) \liff !G.

Read as: T proves that the negation of its arithmetic provability formula at the numeral naming G is equivalent to G

Means: T proves that the negation of its arithmetic provability formula at the numeral naming G is equivalent to G

1 occurrence in this chapter

Equation form expr-966c13ac7323b83a

f(x)=U(μsT(e,x,s))f(x) = U(\umin{s}{T(e,x,s)})

Read as: f of x equals U applied to the least s such that Kleene's T relation holds of e, x, and s

Means: f of x equals U applied to the least s such that Kleene's T relation holds of e, x, and s

1 occurrence in this chapter

Equation form expr-97a4b59f2faaeb88

∃x(PrfT(x,y)∧∀z(z<x→¬RefT(z,y))).\lexists[x][(\OPrf[\Th{T}](x,y) \land \lforall[z][(z < x \lif \lnot \ORefut[\Th{T}](z,y))])].

Read as: there exists x such that the arithmetic proof formula for T holds of x and y, and for every z less than x the arithmetic refutation formula for T does not hold of z and y

Means: there exists x such that the arithmetic proof formula for T holds of x and y, and for every z less than x the arithmetic refutation formula for T does not hold of z and y

1 occurrence in this chapter

Equation form expr-9b10ea990f650fd4

∃xPrfT(x,y)\lexists[x][\OPrf[\Th{T}](x, y)]

Read as: there exists x such that the arithmetic proof formula for T holds of x and y

Means: there exists x such that the arithmetic proof formula for T holds of x and y

1 occurrence in this chapter

Equation form expr-9b620e53b96ef344

PrfT(x,y)\OPrf[\Th{T}](x, y)

Read as: the arithmetic proof formula for T applied to x and y

Means: the arithmetic proof formula for T applied to x and y

2 occurrences in this chapter

Equation form expr-9e37543b179e2edd

R(x1,…,xk)R(x_1,\dots,x_k)

Read as: R of x subscript one through x subscript k

Means: R of x subscript one through x subscript k

1 occurrence in this chapter

Equation form expr-9ef20460d50f585c

ZFC\Th{ZFC}

Read as: Z F C

Means: Z F C

1 occurrence in this chapter

Equation form expr-9fbc4a2ee3060c16

RefT(n,#RT#)\Refut[\Th{T}](n, \Gn{!R_{\Th{T}}})

Read as: the external refutation coding relation for T applied to n and the Goedel number of R subscript T

Means: the external refutation coding relation for T applied to n and the Goedel number of R subscript T

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

10 occurrences in this chapter

Equation form expr-a23c76e06c4f9132

Q⊢∃x(PrfT(x,⌜RT⌝)∧∀z(z<x→¬RefT(z,⌜RT⌝))),\Th{Q} \Proves \lexists[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \land \lforall[z][(z < x \lif \lnot \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])],

Read as: Q proves that there exists x such that the arithmetic proof formula for T holds of x and the numeral naming R subscript T, and for every z less than x the arithmetic refutation formula for T does not hold of z and the numeral naming R subscript T

Means: Q proves that there exists x such that the arithmetic proof formula for T holds of x and the numeral naming R subscript T, and for every z less than x the arithmetic refutation formula for T does not hold of z and the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-a25513c7e0f6eaa8

UU

Read as: U

Means: U

1 occurrence in this chapter

Equation form expr-a269ad3980fe0822

H={⟨e,x⟩:∃sT(e,x,s)}.H = \Setabs{\tuple{e,x}}{\lexists[s][T(e, x, s)]}.

Read as: H equals the set of ordered pairs e, x such that there exists s with Kleene's T relation holding of e, x, and s

Means: H equals the set of ordered pairs e, x such that there exists s with Kleene's T relation holding of e, x, and s

1 occurrence in this chapter

Equation form expr-a3466b8f618426a2

T\Th{T}

Read as: T

Means: T

83 occurrences in this chapter

Equation form expr-a60f9b20bd2671fd

¬A(2¯)\lnot !A(\num 2)

Read as: not A of the numeral two

Means: not A of the numeral two

1 occurrence in this chapter

Equation form expr-a617dd9308ce9ba2

T⊬ProvT(⌜A⌝)→A\Th{T} \Proves/ \OProv[\Th{T}](\gn{!A}) \lif !A

Read as: T does not prove the implication: if its arithmetic provability formula holds of the numeral naming A, then A

Means: T does not prove the implication: if its arithmetic provability formula holds of the numeral naming A, then A

1 occurrence in this chapter

Equation form expr-a62608c10cf4e579

T⊢¬A\Th{T} \Proves \lnot !A

Read as: T proves not A

Means: T proves not A

1 occurrence in this chapter

Equation form expr-a6a0bb17aa6fd55e

diag(⌜B(diag(x))⌝)=⌜A⌝,\Obj{diag}(\gn{!B(\Obj{diag}(x))}) = \gn{!A},

Read as: the value of the object language diagonal function at the numeral naming B of diagonal of x equals the numeral naming A

Means: the value of the object language diagonal function at the numeral naming B of diagonal of x equals the numeral naming A

1 occurrence in this chapter

Equation form expr-a853be42d49299ca

ProvT(y)\OProv[\Th{T}](y)

Read as: the arithmetic provability formula for T applied to y

Means: the arithmetic provability formula for T applied to y

8 occurrences in this chapter

Equation form expr-a88804146736aca0

T⊢G\Th{T} \Proves !G

Read as: T proves G

Means: T proves G

2 occurrences in this chapter

Equation form expr-a89bebd8d7de3401

⌜E(x)⌝\gn{!E(x)}

Read as: the numeral naming the formula E of x

Means: the numeral naming the formula E of x

2 occurrences in this chapter

Equation form expr-aae09569465854a0

D(x)!D(x)

Read as: D of x

Means: D of x

1 occurrence in this chapter

Equation form expr-ad00ddaf8268b155

Bew(y)\fn{Bew}(y)

Read as: Bew of y

Means: Bew of y

1 occurrence in this chapter

Equation form expr-aee22c5b1c8a8367

T⊢H\Th{T} \Proves !H

Read as: T proves H

Means: T proves H

1 occurrence in this chapter

Equation form expr-aee455608e4cfb38

T⊢ProvT(⌜A⌝)T \Proves \OProv[\Th{T}](\gn{!A})

Read as: T proves that its arithmetic provability formula holds of the numeral naming A

Means: T proves that its arithmetic provability formula holds of the numeral naming A

2 occurrences in this chapter

Equation form expr-afdcb58e20ae5027

T⊢A→ProvT(⌜A⌝)T \Proves !A \lif \OProv[\Th{T}](\gn{!A})

Read as: T proves the implication: if A then its arithmetic provability formula holds of the numeral naming A

Means: T proves the implication: if A then its arithmetic provability formula holds of the numeral naming A

1 occurrence in this chapter

Equation form expr-afffbb653fe6cd4b

T⊬RT\Th{T} \Proves/ !R_{\Th{T}}

Read as: T does not prove R subscript T

Means: T does not prove R subscript T

2 occurrences in this chapter

Equation form expr-b0dbbf9111dfb375

n¯<x\num{n} < x

Read as: the numeral for n is less than x

Means: the numeral for n is less than x

1 occurrence in this chapter

Equation form expr-b256184873054297

T⊢ProvT(⌜G⌝)\Th{T} \Proves \OProv[\Th{T}](\gn{!G})

Read as: T proves that its arithmetic provability formula holds of the numeral naming G

Means: T proves that its arithmetic provability formula holds of the numeral naming G

1 occurrence in this chapter

Equation form expr-b4d6f2e8f2d6162e

E(x)!E(x)

Read as: E of x

Means: E of x

7 occurrences in this chapter

Equation form expr-bac9c1c74ecbbfd7

RefT\ORefut[\Th{T}]

Read as: the arithmetic refutation formula for T

Means: the arithmetic refutation formula for T

1 occurrence in this chapter

Equation form expr-bc297bffaa769119

D↔(ProvT(⌜D⌝)→A)D is a fixed point of B(y)D→(ProvT(⌜D⌝)→A)from step L oneProvT(⌜D→(ProvT(⌜D⌝)→A)⌝)from step L two by condition P1ProvT(⌜D⌝)→ProvT(⌜ProvT(⌜D⌝)→A⌝)from step L three using condition P2ProvT(⌜D⌝)→(ProvT(⌜ProvT(⌜D⌝)⌝)→ProvT(⌜A⌝))from step L four using P2 againProvT(⌜D⌝)→ProvT(⌜ProvT(⌜D⌝)⌝)by derivability condition P3ProvT(⌜D⌝)→ProvT(⌜A⌝)from step L five and step L sixProvT(⌜A⌝)→Aby assumption of the theoremProvT(⌜D⌝)→Afrom step L seven and step L eight(ProvT(⌜D⌝)→A)→Dfrom step L oneDfrom step L nine and step L tenProvT(⌜D⌝)from step L eleven by condition P1Afrom step L eight and step L twelve& !D \liff (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-1}\\ & \qquad \text{$!D$ is a fixed point of~$!B(y)$}\notag \\ & !D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-2}\\ & \qquad\text{from \olref{L-1}}\notag\\ & \OProv[\Th{T}](\gn{!D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A)}) \ollabel{L-3}\\ & \qquad \text{from \olref{L-2} by condition P1}\notag \\ & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D}) \lif !A}) \ollabel{L-4}\\ &\qquad \text{from \olref{L-3} using condition P2}\notag \\ & \OProv[\Th{T}](\gn{!D}) \lif (\OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \lif \OProv[\Th{T}](\gn{!A})) \ollabel{L-5}\\ &\qquad \text{from \olref{L-4} using P2 again} \notag\\ & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \ollabel{L-6}\\ & \qquad\text{by !!{derivability} condition P3} \notag\\ & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{!A}) \ollabel{L-7} \\ &\qquad\text{from \olref{L-5} and \olref{L-6}}\notag\\ & \OProv[\Th{T}](\gn{!A}) \lif !A \ollabel{L-8}\\ &\qquad\text{by assumption of the theorem} \notag\\ & \OProv[\Th{T}](\gn{!D}) \lif !A \ollabel{L-9}\\ &\qquad\text{from \olref{L-7} and \olref{L-8}}\notag\\ & (\OProv[\Th{T}](\gn{!D}) \lif !A) \lif !D \ollabel{L-10}\\ & \qquad \text{from \olref{L-1}}\notag \\ & !D \ollabel{L-11}\\ & \qquad\text{from \olref{L-9} and \olref{L-10}}\notag \\ & \OProv[\Th{T}](\gn{!D}) \ollabel{L-12}\\ & \qquad\text{from \olref{L-11} by condition~P1}\notag \\ & !A \qquad\qquad\text{from \olref{L-8} and \olref{L-12}}\notag

Read as: Derivation inside theory T. In this reading, Prov denotes the arithmetic provability formula for T. Line L one. D is equivalent to the implication: if Prov holds of the numeral naming D, then A. Reason: D is a fixed point of B of y. Line L two. If D then, if Prov holds of the numeral naming D, then A. From step L one. Line L three. Prov holds of the numeral naming this whole formula: if D then, if Prov holds of the numeral naming D, then A. End named formula. From step L two by condition P one. Line L four. If Prov holds of the numeral naming D, then Prov holds of the numeral naming this formula: if Prov holds of the numeral naming D, then A. End named formula. From step L three by condition P two. Line L five. If Prov holds of the numeral naming D, then, if Prov holds of the numeral naming the formula Prov of the numeral naming D, then Prov holds of the numeral naming A. From step L four using P two again. Line L six. If Prov holds of the numeral naming D, then Prov holds of the numeral naming the formula Prov of the numeral naming D. By derivability condition P three. Line L seven. If Prov holds of the numeral naming D, then Prov holds of the numeral naming A. From step L five and step L six. Line L eight. If Prov holds of the numeral naming A, then A. By the assumption of the theorem. Line L nine. If Prov holds of the numeral naming D, then A. From step L seven and step L eight. Line L ten. If the implication from Prov of the numeral naming D to A holds, then D. From step L one. Line L eleven. D. From step L nine and step L ten. Line L twelve. Prov holds of the numeral naming D. From step L eleven by condition P one. Final step. A. The source cites step L eight and step L twelve. End derivation.

Means: Derivation inside theory T. In this reading, Prov denotes the arithmetic provability formula for T. Line L one. D is equivalent to the implication: if Prov holds of the numeral naming D, then A. Reason: D is a fixed point of B of y. Line L two. If D then, if Prov holds of the numeral naming D, then A. From step L one. Line L three. Prov holds of the numeral naming this whole formula: if D then, if Prov holds of the numeral naming D, then A. End named formula. From step L two by condition P one. Line L four. If Prov holds of the numeral naming D, then Prov holds of the numeral naming this formula: if Prov holds of the numeral naming D, then A. End named formula. From step L three by condition P two. Line L five. If Prov holds of the numeral naming D, then, if Prov holds of the numeral naming the formula Prov of the numeral naming D, then Prov holds of the numeral naming A. From step L four using P two again. Line L six. If Prov holds of the numeral naming D, then Prov holds of the numeral naming the formula Prov of the numeral naming D. By derivability condition P three. Line L seven. If Prov holds of the numeral naming D, then Prov holds of the numeral naming A. From step L five and step L six. Line L eight. If Prov holds of the numeral naming A, then A. By the assumption of the theorem. Line L nine. If Prov holds of the numeral naming D, then A. From step L seven and step L eight. Line L ten. If the implication from Prov of the numeral naming D to A holds, then D. From step L one. Line L eleven. D. From step L nine and step L ten. Line L twelve. Prov holds of the numeral naming D. From step L eleven by condition P one. Final step. A. The source cites step L eight and step L twelve. End derivation.

1 occurrence in this chapter

Equation form expr-bca5ed895ceeecf9

PA⊢A\Th{PA} \Proves !A

Read as: P A proves A

Means: P A proves A

2 occurrences in this chapter

Equation form expr-c0c9e624593101c9

diag(n)\fn{diag}(n)

Read as: the diagonal function applied to n

Means: the diagonal function applied to n

3 occurrences in this chapter

Equation form expr-c1e524fe9bea8cf9

RProvT(⌜RT⌝)\ORProv[\Th{T}](\gn{!R_{\Th{T}}})

Read as: the arithmetic Rosser provability formula for T at the numeral naming R subscript T

Means: the arithmetic Rosser provability formula for T at the numeral naming R subscript T

1 occurrence in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not A

Means: not A

1 occurrence in this chapter

Equation form expr-c6ac28037112f1e5

T⊬A\Th{T} \Proves/ !A

Read as: T does not prove A

Means: T does not prove A

1 occurrence in this chapter

Equation form expr-c9889aa1225024e1

¬ProvPA(⌜GPA⌝)\lnot \Prov[\Th{PA}](\gn{!G_\Th{PA}})

Read as: the negation of the external provability relation for P A at the numeral naming G subscript P A

Means: the negation of the external provability relation for P A at the numeral naming G subscript P A

1 occurrence in this chapter

Equation form expr-cb54e6364b5db3af

PrfT(m,#GT#)\Prf[\Th{T}](m, \Gn{!G_\Th{T}})

Read as: the external proof coding relation for T applied to m and the Goedel number of G subscript T

Means: the external proof coding relation for T applied to m and the Goedel number of G subscript T

1 occurrence in this chapter

Equation form expr-cb9cb1021abe75c9

ProvT(⌜A⌝)→A\OProv[\Th{T}](\gn{!A}) \lif !A

Read as: if the arithmetic provability formula for T holds of the numeral naming A, then A

Means: if the arithmetic provability formula for T holds of the numeral naming A, then A

3 occurrences in this chapter

Equation form expr-cc15b5465a9c2743

x≠k¯\eq/[x][\num{k}]

Read as: x is not equal to the numeral for k

Means: x is not equal to the numeral for k

1 occurrence in this chapter

Equation form expr-ccbf98e5fc5a7541

∃xPrfPA(x,y)\lexists[x][\Prf[\Th{PA}](x,y)]

Read as: there exists x such that the external proof coding relation for P A holds of x and y

Means: there exists x such that the external proof coding relation for P A holds of x and y

1 occurrence in this chapter

Equation form expr-cd3d61f5dad4e6b6

diag\Obj{diag}

Read as: the object language diagonal function symbol

Means: the object language diagonal function symbol

3 occurrences in this chapter

Equation form expr-ce1c9d4ee73ea6be

B(diag(⌜B(diag(x))⌝))↔B(⌜A⌝)!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))})) \liff !B(\gn{!A})

Read as: B of diagonal of the numeral naming the formula B of diagonal of x is equivalent to B of the numeral naming A

Means: B of diagonal of the numeral naming the formula B of diagonal of x is equivalent to B of the numeral naming A

1 occurrence in this chapter

Equation form expr-ce7808f70ee2abca

A(x1,…,xk)!A(x_1,\dots,x_k)

Read as: A of x subscript one through x subscript k

Means: A of x subscript one through x subscript k

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: B

Means: B

2 occurrences in this chapter

Equation form expr-d1b4757eae616923

GPA→ConPA!G_{\Th{PA}} \lif \OCon[\Th{PA}]

Read as: if G subscript P A then the arithmetic consistency sentence for P A

Means: if G subscript P A then the arithmetic consistency sentence for P A

1 occurrence in this chapter

Equation form expr-d203ba01eef4198c

δ\delta

Read as: delta

Means: delta

1 occurrence in this chapter

Equation form expr-d475527c5abd77f4

∃xA(x)\lexists[x][!A(x)]

Read as: the formula there exists x such that A of x

Means: the formula there exists x such that A of x

3 occurrences in this chapter

Equation form expr-d6ed30707586ef06

∃sDT(z,x,s)\lexists[s][!D_T(z, x, s)]

Read as: the formula: there exists s such that D subscript T holds of z, x, and s. End formula.

Means: the formula: there exists s such that D subscript T holds of z, x, and s. End formula.

1 occurrence in this chapter

Equation form expr-d704227c365c1301

PrfT(m¯,⌜GT⌝)\OPrf[\Th{T}](\num m, \gn{!G_\Th{T}})

Read as: the arithmetic proof formula for T applied to the numeral for m and the numeral naming G subscript T

Means: the arithmetic proof formula for T applied to the numeral for m and the numeral naming G subscript T

1 occurrence in this chapter

Equation form expr-d891e212f8a2a2ff

GT↔¬ProvT(⌜GT⌝).\ollabel{eqn:qpf} !G_\Th{T} \liff \lnot \OProv[\Th{T}](\gn{!G_\Th{T}}).

Read as: G subscript T is equivalent to the negation of the arithmetic provability formula for T at the numeral naming G subscript T

Means: G subscript T is equivalent to the negation of the arithmetic provability formula for T at the numeral naming G subscript T

1 occurrence in this chapter

Equation form expr-d89ad7af62404a57

PA\Th{PA}

Read as: P A

Means: P A

28 occurrences in this chapter

Equation form expr-daa35700f4bd10c2

diag\fn{diag}

Read as: the diagonal function

Means: the diagonal function

4 occurrences in this chapter

Equation form expr-dd90fe2c42c9bea2

#A#\Gn{!A}

Read as: the Goedel number of A

Means: the Goedel number of A

3 occurrences in this chapter

Equation form expr-df7e70e5021544f4

BB

Read as: B

Means: B

3 occurrences in this chapter

Equation form expr-e0f517c1e00b26c7

H={⟨e,x⟩:N⊨∃sDT(e¯,x¯,s)},H = \Setabs{\tuple{e,x}}{\Sat{N}{\lexists[s][!D_T(\num e, \num x, s)]}},

Read as: H equals the set of ordered pairs e, x such that the following sentence is true in the standard natural number structure N: there exists s such that D subscript T holds of the numeral for e, the numeral for x, and s

Means: H equals the set of ordered pairs e, x such that the following sentence is true in the standard natural number structure N: there exists s such that D subscript T holds of the numeral for e, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-e321c65dc6d1efcd

T⊢A↔B(⌜A⌝)\Th{T} \Proves !A \liff !B(\gn{!A})

Read as: T proves that A is equivalent to B of the numeral naming A

Means: T proves that A is equivalent to B of the numeral naming A

1 occurrence in this chapter

Equation form expr-e36fea235d951da5

ConT\OCon[T]

Read as: the arithmetic consistency sentence for T

Means: the arithmetic consistency sentence for T

1 occurrence in this chapter

Equation form expr-e60383591ce7998c

Prov(⌜A→B⌝)→(Prov(⌜A⌝)→Prov(⌜B⌝))\OProv(\gn{!A \lif !B}) \lif (\OProv(\gn{!A}) \lif \OProv(\gn{!B}))

Read as: if the arithmetic provability formula holds of the numeral naming the implication from A to B, then, if it holds of the numeral naming A, it also holds of the numeral naming B

Means: if the arithmetic provability formula holds of the numeral naming the implication from A to B, then, if it holds of the numeral naming A, it also holds of the numeral naming B

1 occurrence in this chapter

Equation form expr-e632b7095b0bf32c

TT

Read as: T

Means: T

3 occurrences in this chapter

Equation form expr-e6aa658a5b12a84c

T⊢¬ProvT(⌜G⌝)↔G\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G}) \liff !G

Read as: T proves that the negation of its arithmetic provability formula at the numeral naming G is equivalent to G

Means: T proves that the negation of its arithmetic provability formula at the numeral naming G is equivalent to G

1 occurrence in this chapter

Equation form expr-e702022763e41de5

¬A(n¯)\lnot !A(\num n)

Read as: not A of the numeral for n

Means: not A of the numeral for n

1 occurrence in this chapter

Equation form expr-e92ccebb64085e8c

T⊢ProvT(⌜H⌝)↔Hin particularT⊢ProvT(⌜H⌝)→H\Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \liff !H\\ \intertext{in particular} \Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \lif !H

Read as: T proves that its arithmetic provability formula at the numeral naming H is equivalent to H. In particular, T proves that if its arithmetic provability formula holds of the numeral naming H, then H.

Means: T proves that its arithmetic provability formula at the numeral naming H is equivalent to H. In particular, T proves that if its arithmetic provability formula holds of the numeral naming H, then H.

1 occurrence in this chapter

Equation form expr-eb29cbe6badd68df

{#A#:N⊨A}\Setabs{\Gn{!A}}{\Sat{N}{!A}}

Read as: the set of Goedel numbers of sentences A that are true in the standard natural number structure N

Means: the set of Goedel numbers of sentences A that are true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-eb56b2300ad56d34

Source-census fragment. Read the complete source formula tr038-reader-composite-math-0001. The original fragment is preserved as forensic source evidence, not as a complete reader equation.

1 occurrence in this chapter

Equation form expr-ebae624d86fb2037

T⊢ProvT(⌜H⌝)\Th{T} \Proves \OProv[\Th{T}](\gn{!H})

Read as: T proves that its arithmetic provability formula holds of the numeral naming H

Means: T proves that its arithmetic provability formula holds of the numeral naming H

1 occurrence in this chapter

Equation form expr-ec7b50c0c99f3425

Ddiag(⌜E(x)⌝,y)!D_{\fn{diag}}(\gn{!E(x)},y)

Read as: D subscript diagonal of the numeral naming E of x, and y

Means: D subscript diagonal of the numeral naming E of x, and y

1 occurrence in this chapter

Equation form expr-eee1c230c6f27590

TA\Th{TA}

Read as: true arithmetic

Means: true arithmetic

2 occurrences in this chapter

Equation form expr-ef1827c01ee30529

ℕ∖X\Nat \setminus X

Read as: the natural numbers outside X

Means: the natural numbers outside X

1 occurrence in this chapter

Equation form expr-f0b022c1f249a0a8

¬∃x(PrfT(x,⌜RT⌝)∧∀z(z<x→¬RefT(z,⌜RT⌝))),is logically equivalent to∀x(PrfT(x,⌜RT⌝)→∃z(z<x∧RefT(z,⌜RT⌝))).\lnot & \lexists[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \land \lforall[z][(z < x \lif \lnot \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])], \intertext{is logically equivalent to} & \lforall[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \lif \lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])].

Read as: It is not the case that there exists x for which the arithmetic proof formula for T holds of x and the numeral naming R subscript T, and no z less than x satisfies the arithmetic refutation formula for T at z and that same numeral. This is logically equivalent to the following: for every x, if the arithmetic proof formula for T holds of x and the numeral naming R subscript T, then there exists z less than x such that the arithmetic refutation formula for T holds of z and the numeral naming R subscript T.

Means: It is not the case that there exists x for which the arithmetic proof formula for T holds of x and the numeral naming R subscript T, and no z less than x satisfies the arithmetic refutation formula for T at z and that same numeral. This is logically equivalent to the following: for every x, if the arithmetic proof formula for T holds of x and the numeral naming R subscript T, then there exists z less than x such that the arithmetic refutation formula for T holds of z and the numeral naming R subscript T.

1 occurrence in this chapter

Equation form expr-f24501cd355c999c

TA={A:N⊨A}\Th{TA} = \Setabs{!A}{\Sat{N}{!A}}

Read as: true arithmetic equals the set of sentences A that are true in the standard natural number structure N

Means: true arithmetic equals the set of sentences A that are true in the standard natural number structure N

1 occurrence in this chapter

Equation form expr-f3c33399d278002f

RProvT(y)\ORProv[\Th{T}](y)

Read as: the arithmetic Rosser provability formula for T applied to y

Means: the arithmetic Rosser provability formula for T applied to y

4 occurrences in this chapter

Equation form expr-f3f3804480e8551a

β\beta

Read as: beta

Means: beta

1 occurrence in this chapter

Equation form expr-f498864f9c464a35

T⊢RT\Th{T} \Proves !R_{\Th{T}}

Read as: T proves R subscript T

Means: T proves R subscript T

1 occurrence in this chapter

Equation form expr-f4a7eb519730ae63

T⊬¬GT\Th{T} \Proves/ \lnot !G_\Th{T}

Read as: T does not prove not G subscript T

Means: T does not prove not G subscript T

2 occurrences in this chapter

Equation form expr-f4f206f5148979e1

A≡Prov(⌜G⌝)!A \ident \OProv(\gn{G})

Read as: A is syntactically identical to the arithmetic provability formula at the numeral naming G

Means: A is syntactically identical to the arithmetic provability formula at the numeral naming G

1 occurrence in this chapter

Equation form expr-f4fd7f5ee62c4c18

Source-census fragment. Read the complete source formula tr038-reader-composite-math-0001. The original fragment is preserved as forensic source evidence, not as a complete reader equation.

1 occurrence in this chapter

Equation form expr-f5a8cce5cb491c78

PA⊢ProvPA(⌜A⌝)→ProvPA(⌜ProvPA(⌜A⌝)⌝).\Th{PA} \Proves \OProv[\Th{PA}](\gn{!A}) \lif \OProv[\Th{PA}](\gn{\OProv[\Th{PA}](\gn{!A})}).

Read as: P A proves the following implication. If its arithmetic provability formula holds of the numeral naming A, then that provability formula holds of the numeral naming the following formula: the arithmetic provability formula for P A at the numeral naming A. End named formula. End implication.

Means: P A proves the following implication. If its arithmetic provability formula holds of the numeral naming A, then that provability formula holds of the numeral naming the following formula: the arithmetic provability formula for P A at the numeral naming A. End named formula. End implication.

1 occurrence in this chapter

Equation form expr-f5eeaf6f9ba05577

Q⊢B↔A(⌜B⌝)\Th{Q} \Proves !B \liff !A(\gn{!B})

Read as: Q proves that B is equivalent to A of the numeral naming B

Means: Q proves that B is equivalent to A of the numeral naming B

1 occurrence in this chapter

Equation form expr-f888d2e33b66d0c5

D!D

Read as: D

Means: D

1 occurrence in this chapter

Equation form expr-f8c3828a4c9b00c9

B(x)!B(x)

Read as: B of x

Means: B of x

9 occurrences in this chapter

Equation form expr-f9f119879291e79b

Q(n)⇔n∈{#A#:Q⊢A}Q(n) \defiff n \in \Setabs{\Gn{!A}}{\Th{Q} \Proves !A}

Read as: the numerical relation Q of n, defined by the following equivalence: Q of n if and only if n belongs to the set of Goedel numbers of sentences A such that theory Q proves A. End of defining equivalence.

Means: the numerical relation Q of n, defined by the following equivalence: Q of n if and only if n belongs to the set of Goedel numbers of sentences A such that theory Q proves A. End of defining equivalence.

1 occurrence in this chapter

Equation form expr-fadefb2f36b04638

¬ProvPA(⌜0=1⌝)\lnot \OProv[\Th{PA}](\gn{\eq[0][1]})

Read as: the arithmetic provability formula for P A does not hold of the numeral naming the formula zero equals one

Means: the arithmetic provability formula for P A does not hold of the numeral naming the formula zero equals one

1 occurrence in this chapter

Equation form expr-ff7db6935561aeca

B≡Prov(⌜G⌝)→⊥!B \ident \OProv(\gn{!G}) \lif \lfalse

Read as: B is syntactically identical to the implication from the arithmetic provability formula at the numeral naming G to falsity

Means: B is syntactically identical to the implication from the arithmetic provability formula at the numeral naming G to falsity

1 occurrence in this chapter

Fixed point lemma in a theory extending Q

For every formula B with just x free, there is a sentence A such that T proves that A is equivalent to B applied to the numeral naming A. This is provable equivalence, not syntactic identity.

Source

Diagonalization produces the code of the intended fixed point

Two equalities first expand the diagonal function on the code of B of diagonal of x, then identify the resulting code with the Goedel number of A. The inner naming expressions are numerals; the outer Goedel brackets denote natural numbers.

Source

Fixed point lemma already provable in Q

For any formula B with one free variable, Q proves an equivalence between a sentence A and B of the numeral naming A. The proof represents the computable diagonal function by a formula with an input and a uniquely determined output.

Source

Existence and uniqueness facts for diagonal representation

The first fact supplies the represented diagonal value. The second says that every output satisfying that same representation equals the numeral naming A. Both are derivable in Q; uniqueness is not merely asserted in the external natural numbers.

Source

Reverse implication in the fixed point proof

Combine the represented diagonal value with the assumed B of the numeral naming A, then existentially quantify the common output. The result is the defining formula E at its own name, which is A.

Source

Exercise ruling out a provable truth definition

The exercise defines a truth definition by requiring Q to prove the truth equivalence for every sentence, and asks the reader to rule it out using the fixed point lemma. No solution is supplied.

Source

Defining equivalence of the Goedel sentence

G subscript T is equivalent to the negation of the arithmetic provability formula at its own name. The surrounding text states that Q, and hence T, derives this equivalence.

Source

Consistency makes the Goedel sentence unprovable

A consistent computably axiomatizable theory extending Q does not prove its Goedel sentence. The proof assumes such a proof, represents its code inside Q, and uses the defining equivalence to obtain the opposite sentence.

Source

Definition of omega consistency

When every negative numeral instance of a formula is provable, omega consistency rules out a proof of its positive existential closure. These are separate individual numeral proofs; no universal closure is substituted for the infinite family.

Source

Omega consistency makes the Goedel sentence irrefutable

An omega consistent computably axiomatizable extension of Q cannot prove the negation of its Goedel sentence. The proof combines absence of each individual proof code with the existential assertion that a proof exists, obtaining omega inconsistency if the negation were provable.

Source

Exercise separating consistency from omega consistency

The reader is asked to show that Q together with the negation of its Goedel sentence is consistent but omega inconsistent. This requested argument is not supplied as an added solution.

Source

Goedel first incompleteness theorem

Every omega consistent computably axiomatizable extension of Q is incomplete. Its Goedel sentence is neither provable nor refutable, by the preceding two lemmas.

Source

Rosser incompleteness theorem

Every consistent computably axiomatizable extension of Q is incomplete; omega consistency is no longer needed. The proof modifies the provability formula by requiring that a proof code have no smaller refutation code.

Source

Defining equivalence of the Rosser sentence

Q proves that R subscript T is equivalent to the negation of the arithmetic Rosser provability formula at its own numeral name.

Source

Reduction of Rosser irrefutability to a statement in Q

The defining fixed point equivalence is a theorem of Q. Because T extends Q, it suffices to prove in Q the negation of Rosser provability of the Rosser sentence.

Source

Negating the Rosser provability formula

The negation of an existential proof code with no smaller refutation becomes a universal statement: every proof code has some smaller refutation code. The strict inequality and the nesting of universal and existential quantifiers are retained.

Source

Exercise on computable inseparability of provable and refutable sentences

For a consistent computably axiomatizable extension T of Q, the reader must prove that the sets of codes of provable and refutable sentences are computably inseparable. The separator definition and natural number complement are retained. No solution is supplied.

Source

Second incompleteness theorem for Peano arithmetic

Assuming P A is consistent, it does not derive its arithmetic consistency sentence for the stated provability representation. The surrounding text emphasizes the dependence on the chosen representation and derivability conditions.

Source

Ten step internal derivation from consistency to the Goedel sentence

Nine labeled steps and an unlabeled conclusion inside P A establish that Con implies G. They use the Goedel fixed point, derivability conditions P one, P two, and P three, propositional reasoning, and contraposition. Full formula and dependency speech accompanies the display; nested provability levels remain distinct.

Source

General second incompleteness theorem

For a consistent computably axiomatized extension T of Q, any arithmetic provability formula satisfying conditions P one through P three gives a consistency sentence that T cannot derive.

Source

Exercise deriving consistency from the Goedel sentence

Show inside P A that its Goedel sentence implies its consistency sentence. The exercise reverses the implication established in the source proof, and remains unsolved.

Source

Loeb theorem

For a computably axiomatizable extension T of Q whose provability formula satisfies the derivability conditions, if T proves the reflection implication for A, then T already proves A. The statement is about a particular instance, not a universally available reflection schema.

Source

Thirteen step internal derivation for Loeb theorem

Twelve labeled steps and a final A use a fixed point D of the reflection-shaped formula. The proof derives provability of D implying A, then D, then provability of D, and finally A. The source final citation gives L eight and L twelve rather than L nine and L twelve; this citation defect is disclosed without deleting the original dependency labels.

Source

The positive provability fixed point is derivable

The equivalence between provability of H and H yields its left to right reflection implication. Loeb theorem then establishes H. The displayed equivalence and its consequence are both theorems of T.

Source

Exercise comparing four reflection and provability claims

The four numbered claims distinguish external implications about what T proves from implications proved inside T. They also distinguish the direction from A to its provability from the converse reflection direction. The requested conditions are not answered in the edition.

Source

Definition of definability in the standard natural numbers

A numerical relation is definable if an arithmetic formula agrees with it on every tuple of natural numbers when the corresponding numerals are substituted and truth is evaluated in the standard natural number structure N.

Source

Every computable relation is definable

A formula representing a relation in Q defines the same relation in the standard natural number structure N.

Source

The halting relation is definable

Kleene normal form expresses halting by existence of a computation witness. Since the T relation is primitive recursive, its arithmetic definition yields a definition of the halting relation, despite that relation not being computable.

Source

Exercise defining Q theorem codes in arithmetic

The reader is asked to show that the set of Goedel numbers of sentences provable in Q is definable in arithmetic. No solution is added.

Source

Tarski undefinability theorem

The set of true arithmetic sentences, coded by their Goedel numbers, is not definable in arithmetic. The proof assumes a defining formula and diagonalizes against it, producing a contradiction in the standard interpretation rather than confusing truth with formal provability.

Source

Cross-reference reference-000744

the second diagonal representation fact, uniqueness of the output

Source occurrence

Cross-reference reference-000745

the first diagonal representation fact, the represented value

Source occurrence

Cross-reference reference-000746

the defining equivalence of the Goedel sentence

Source occurrence

Cross-reference reference-000747

the lemma that consistency makes the Goedel sentence unprovable

Source occurrence

Cross-reference reference-000748

the defining equivalence of the Goedel sentence

Source occurrence

Cross-reference reference-000749

the lemma that consistency makes the Goedel sentence unprovable

Source occurrence

Cross-reference reference-000750

the lemma that omega consistency makes the Goedel sentence irrefutable

Source occurrence

Cross-reference reference-000751

the first incompleteness theorem

Source occurrence

Cross-reference reference-000752

the lemma describing the finitely many numbers below a numeral

Source occurrence

Cross-reference reference-000753

the defining equivalence of the Rosser sentence

Source occurrence

Cross-reference reference-000754

the lemma describing the finitely many numbers below a numeral

Source occurrence

Cross-reference reference-000755

the trichotomy lemma for comparison with a numeral

Source occurrence

Cross-reference reference-000756

the first incompleteness theorem

Source occurrence

Cross-reference reference-000757

step G two, one

Source occurrence

Cross-reference reference-000758

step G two, two

Source occurrence

Cross-reference reference-000759

step G two, three

Source occurrence

Cross-reference reference-000760

step G two, four

Source occurrence

Cross-reference reference-000761

step G two, five

Source occurrence

Cross-reference reference-000762

step G two, six

Source occurrence

Cross-reference reference-000763

step G two, seven

Source occurrence

Cross-reference reference-000764

step G two, eight

Source occurrence

Cross-reference reference-000765

step G two, one

Source occurrence

Cross-reference reference-000766

step G two, nine

Source occurrence

Cross-reference reference-000767

step G two, three

Source occurrence

Cross-reference reference-000768

step G two, eight

Source occurrence

Cross-reference reference-000769

step G two, five

Source occurrence

Cross-reference reference-000770

step G two, six

Source occurrence

Cross-reference reference-000771

the section on the second incompleteness theorem

Source occurrence

Cross-reference reference-000772

Loeb theorem

Source occurrence

Cross-reference reference-000773

step L one

Source occurrence

Cross-reference reference-000774

step L two

Source occurrence

Cross-reference reference-000775

step L three

Source occurrence

Cross-reference reference-000776

step L four

Source occurrence

Cross-reference reference-000777

step L five

Source occurrence

Cross-reference reference-000778

step L six

Source occurrence

Cross-reference reference-000779

step L seven

Source occurrence

Cross-reference reference-000780

step L eight

Source occurrence

Cross-reference reference-000781

step L one

Source occurrence

Cross-reference reference-000782

step L nine

Source occurrence

Cross-reference reference-000783

step L ten

Source occurrence

Cross-reference reference-000784

step L eleven

Source occurrence

Cross-reference reference-000785

step L eight

Source occurrence

Cross-reference reference-000786

step L twelve

Source occurrence

Source disclosures

Complete source formula tr038-reader-composite-math-0001

T(`X')T(\text{`$X$'})

Read as: T applied to the quotation of the sentence X

Read in context source