Incompleteness

Theories and Computability

Equation form expr-0392a7f58dc6f6ba

0\Obj 0

Read as: the zero constant

Means: the zero constant

3 occurrences in this chapter

Equation form expr-0b81e6ef82ac39a9

{A:ℕ⊨A}\Setabs{!A}{ \Sat{\Nat}{!A}}

Read as: the set of sentences A such that A is true in the standard natural number interpretation

Means: the set of sentences A such that A is true in the standard natural number interpretation

1 occurrence in this chapter

Equation form expr-0e4f6664ffad3e16

T(x,x,n)T(x,x,n)

Read as: T of x, x, and n

Means: T of x, x, and n

2 occurrences in this chapter

Equation form expr-115c38bcecd4c5e8

Q={y:∃xPrfQ(x,y)}.Q = \Setabs{y}{\lexists[x][\Prf[\Th{Q}](x,y)]}.

Read as: Q equals the set of y such that there exists x with x the code of a proof in Q of the sentence with code y

Means: Q equals the set of y such that there exists x with x the code of a proof in Q of the sentence with code y

1 occurrence in this chapter

Equation form expr-11baa595827a4e0f

ω\omega

Read as: omega

Means: omega

9 occurrences in this chapter

Equation form expr-151b0405a6871bb5

T¯\Th{\bar T}

Read as: the complement of T

Means: the complement of T

1 occurrence in this chapter

Equation form expr-154c639d9e525d5c

¬R(k,k)\lnot R(k,k)

Read as: not R of k and k

Means: not R of k and k

1 occurrence in this chapter

Equation form expr-1725f50d3d8dcefd

A∈T!A \in T

Read as: sentence A belongs to theory T

Means: sentence A belongs to theory T

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

2 occurrences in this chapter

Equation form expr-1f796fa7828c1d27

C={A:T⊢E→A}.C = \Setabs{!A}{\Th{T} \Proves !E \lif !A}.

Read as: C equals the set of sentences A such that theory T proves the implication from E to A

Means: C equals the set of sentences A such that theory T proves the implication from E to A

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

1 occurrence in this chapter

Equation form expr-265fda17a34611b1

′'

Read as: the successor symbol

Means: the successor symbol

4 occurrences in this chapter

Equation form expr-2726366b3f9029a1

(B1∧…∧Bk)→A(!B_1 \land \dots \land !B_k) \lif !A

Read as: if the conjunction of B subscript one through B subscript k holds, then A

Means: if the conjunction of B subscript one through B subscript k holds, then A

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

10 occurrences 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-32ce776fa0d916ab

D(y¯)!D(\num y)

Read as: D of the numeral for y

Means: D of the numeral for y

2 occurrences in this chapter

Equation form expr-32f11b9dc837c819

Bk!B_k

Read as: B subscript k

Means: B subscript k

1 occurrence in this chapter

Equation form expr-342e35c540e50532

Source-census fragment. Read the complete source formula tr037-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-349719b1610e7ceb

R(k,k)R(k,k)

Read as: R of k and k

Means: R of k and k

1 occurrence in this chapter

Equation form expr-349ba76d907adfab

×\times

Read as: the multiplication symbol

Means: the multiplication symbol

3 occurrences in this chapter

Equation form expr-382f6f8213e1752f

{0≠0}\{ \eq/[0][0] \}

Read as: the singleton set containing the formula zero does not equal zero

Means: the singleton set containing the formula zero does not equal zero

1 occurrence in this chapter

Equation form expr-3b001107ec108500

Q⊆C\Th{Q} \subseteq C

Read as: theory Q is a subset of C

Means: theory Q is a subset of C

1 occurrence 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-3d2df79065b6f165

Q\Th{Q}

Read as: Q

Means: Q

49 occurrences in this chapter

Equation form expr-3ef8cac3fdc3e373

R(k,y)R(k,y)

Read as: R of k and y

Means: R of k and y

2 occurrences in this chapter

Equation form expr-40aa26d6f7e72e8a

K={x:Ax(x)↓}K = \Setabs{x}{!A_x(x) \downarrow}

Read as: K equals the set of x such that machine A subscript x halts on input x

Means: K equals the set of x such that machine A subscript x halts on input x

1 occurrence in this chapter

Equation form expr-46b57457636c794c

A⊆CA \subseteq C

Read as: A is a subset of C

Means: A is a subset of C

1 occurrence in this chapter

Equation form expr-497d497fc35ba36e

Q1!Q_1

Read as: Q subscript one

Means: Q subscript one

1 occurrence in this chapter

Equation form expr-4e3d79dde6e34ca2

E→¬A!E \lif \lnot !A

Read as: if E then not A

Means: if E then not A

1 occurrence in this chapter

Equation form expr-4e93ef99434cd7d0

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

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

Means: B is a subset of the complement of C

1 occurrence in this chapter

Equation form expr-534be1cd5492acea

S(n¯)→Q⊢DS(n¯)→DS(n¯)∈CS(\num n) & \lif & \Th{Q} \Proves !D_S(\num n) \\ & \lif & !D_S(\num n) \in C

Read as: If S holds of the numeral for n, then Q proves D subscript S of the numeral for n. This implies that D subscript S of the numeral for n belongs to C.

Means: If S holds of the numeral for n, then Q proves D subscript S of the numeral for n. This implies that D subscript S of the numeral for n belongs to C.

1 occurrence in this chapter

Equation form expr-559aead08264d579

AA

Read as: A

Means: A

6 occurrences in this chapter

Equation form expr-57debf3ade2d4390

Q⊢∃sAT(x¯,x¯,s)\Th{Q} \Proves \lexists[s][!A_T(\num x, \num x, s)]

Read as: Q proves that there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

Means: Q proves that there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-5fe7f9b84ca9cdcb

S(y)S(y)

Read as: S of y

Means: S of y

9 occurrences in this chapter

Equation form expr-611f25c85cfa1128

∃sAT(x¯,x¯,s)\lexists[s][!A_T(\num x, \num x, s)]

Read as: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

Means: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-6218979ca0cf36ba

∃sT(x¯,x¯,s)\lexists[s][T(\num x, \num x, s)]

Read as: there exists s such that T holds of the numeral for x, the numeral for x, and s

Means: there exists s such that T holds of the numeral for x, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-652979afe7a98d5f

L2\Lang{L_2}

Read as: L subscript two

Means: L subscript two

2 occurrences 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-675a3bf9d039e3ba

¬R(y,y)\lnot R(y,y)

Read as: not R of y and y

Means: not R of y and y

1 occurrence in this chapter

Equation form expr-67cec570ae34fc39

T∪Q\Th{T} \cup \Th{Q}

Read as: the union of theories T and Q

Means: the union of theories T and Q

3 occurrences in this chapter

Equation form expr-6a72b6dcd25f8fd1

S(k)S(k)

Read as: S of k

Means: S of k

1 occurrence in this chapter

Equation form expr-6b23c0d5f35d1b11

CC

Read as: C

Means: C

8 occurrences in this chapter

Equation form expr-6c5013f8bf6e3ccb

Q¯={A:Q⊢¬A}\Th{\bar Q} = \Setabs{!A}{\Th{Q} \Proves \lnot !A}

Read as: Q bar equals the set of sentences A whose negations are provable in Q

Means: Q bar equals the set of sentences A whose negations are provable in Q

1 occurrence in this chapter

Equation form expr-6dd8166a44d2ad05

S(n¯)→T⊢DS(n¯)→R(#DS(u)#,n)S(\num n) & \lif & T \vdash !D_S(\num n) \\ & \lif & R(\Gn{!D_S(u)}, n)

Read as: If S holds of the numeral for n, then T proves D subscript S of the numeral for n. This implies R of the Goedel number of D subscript S of u, and n.

Means: If S holds of the numeral for n, then T proves D subscript S of the numeral for n. This implies R of the Goedel number of D subscript S of u, and n.

1 occurrence in this chapter

Equation form expr-729f2cd8398e9960

∈\in

Read as: the membership relation symbol

Means: the membership relation symbol

1 occurrence in this chapter

Equation form expr-7a62d55fb411637c

T¯≤mT\Th{\bar T} \leq_m \Th{T}

Read as: the complement of T is many one reducible to T

Means: the complement of T is many one reducible to T

1 occurrence in this chapter

Equation form expr-7ad8056777e44220

¬AT(x¯,x¯,n¯)\lnot !A_T(\num x, \num x, \num n)

Read as: not A subscript T of the numeral for x, the numeral for x, and the numeral for n

Means: not A subscript T of the numeral for x, the numeral for x, and the numeral for n

1 occurrence in this chapter

Equation form expr-8077cc52bcc98e09

DS(u)!D_S(u)

Read as: D subscript S of u

Means: D subscript S of u

2 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

21 occurrences in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

2 occurrences in this chapter

Equation form expr-85ab7f168c9566f1

¬AT(x¯,x¯,1¯)\lnot !A_T(\num x, \num x, \num 1)

Read as: not A subscript T of the numeral for x, the numeral for x, and the numeral one

Means: not A subscript T of the numeral for x, the numeral for x, and the numeral one

1 occurrence in this chapter

Equation form expr-86be9a55762d316a

KK

Read as: K

Means: K

4 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

3 occurrences in this chapter

Equation form expr-8d2cacefc75ba038

∅\emptyset

Read as: the empty set

Means: the empty set

1 occurrence in this chapter

Equation form expr-8d81868389774c13

K≤mQK \leq_m Q

Read as: K is many one reducible to Q

Means: K is many one reducible to Q

1 occurrence in this chapter

Equation form expr-8de928d4788501c4

Ax(x)↓!A_x(x) \downarrow

Read as: machine A subscript x halts on input x

Means: machine A subscript x halts on input x

1 occurrence in this chapter

Equation form expr-8e30179df74cc60a

Q8!Q_8

Read as: Q subscript eight

Means: Q subscript eight

1 occurrence in this chapter

Equation form expr-8f464dce0a5a0040

R(#(DS(u¯)),y)R(\#(!D_S(\num u)),y)

Read as: R of the Goedel number of D subscript S of the numeral for u, and y

Means: R of the Goedel number of D subscript S of the numeral for u, and y

1 occurrence in this chapter

Equation form expr-90926752a5fd3d58

∃sAT(x¯,x¯,s)\lexists[s][!A_T(\num x,\num x, s)]

Read as: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

Means: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-9be8efd9853e4e3c

x∈K→∃sT(x,x,s)→∃s(Q⊢AT(x¯,x¯,s¯))→Q⊢∃sAT(x¯,x¯,s).x \in K & \lif \lexists[s][T(x,x,s)] \\ & \lif \lexists[s][(\Th{Q} \Proves !A_T(\num x,\num x, \num s))] \\ & \lif \Th{Q} \Proves \lexists[s][!A_T(\num x, \num x, s)].

Read as: If x belongs to K, then there exists s such that Kleene's T relation holds of x, x, and s. This implies that there exists s such that Q proves A subscript T of the numeral for x, the numeral for x, and the numeral for s. This in turn implies that Q proves: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s.

Means: If x belongs to K, then there exists s such that Kleene's T relation holds of x, x, and s. This implies that there exists s such that Q proves A subscript T of the numeral for x, the numeral for x, and the numeral for s. This in turn implies that Q proves: there exists s such that A subscript T holds of the numeral for x, the numeral for x, and s.

1 occurrence in this chapter

Equation form expr-9e14cb56a87abb66

L1\Lang{L_1}

Read as: L subscript one

Means: L subscript one

2 occurrences in this chapter

Equation form expr-9ef20460d50f585c

ZFC\Th{ZFC}

Read as: Z F C

Means: Z F C

5 occurrences in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

4 occurrences in this chapter

Equation form expr-a2632d37c52b9135

¬AT(x¯,x¯,0¯)\lnot !A_T(\num x, \num x, \num 0)

Read as: not A subscript T of the numeral for x, the numeral for x, and the numeral zero

Means: not A subscript T of the numeral for x, the numeral for x, and the numeral zero

1 occurrence in this chapter

Equation form expr-a318c24216defe20

++

Read as: the addition symbol

Means: the addition symbol

3 occurrences in this chapter

Equation form expr-a3466b8f618426a2

T\Th{T}

Read as: T

Means: T

48 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-a82d9e41085616de

E→A!E \lif !A

Read as: if E then A

Means: if E then A

3 occurrences in this chapter

Equation form expr-a9df23b51c1823d3

∃sT(x¯,x¯,s)\lexists[s][T(\num x,\num x,s)]

Read as: there exists s such that T holds of the numeral for x, the numeral for x, and s

Means: there exists s such that T holds of the numeral for x, the numeral for x, and s

1 occurrence in this chapter

Equation form expr-ad21ff31eb419ada

Source-census fragment. Read the complete source formula tr037-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-ae83e1213225cca6

E=Q1∧…∧Q8!E = !Q_1 \land \dots \land !Q_8

Read as: E is the conjunction of Q subscript one through Q subscript eight

Means: E is the conjunction of Q subscript one through Q subscript eight

1 occurrence in this chapter

Equation form expr-b2542285e9b32f73

C¯\Complement{C}

Read as: the complement of C

Means: the complement of C

1 occurrence in this chapter

Equation form expr-b4b2e1b50bc0c27b

x∈Kx \in K

Read as: x belongs to K

Means: x belongs to K

1 occurrence in this chapter

Equation form expr-bf55f074d4127f93

¬S(n¯)→T⊢¬DS(n¯)→T⊬DS(n¯)(since T is consistent)→¬R(#DS(u)#,n).\lnot S(\num n) & \lif & T \vdash \lnot !D_S(\num n) \\ & \lif & T \not\vdash !D_S(\num n) \quad \text{(since $\Th{T}$ is consistent)} \\ & \lif & \lnot R(\Gn{!D_S(u)}, n).

Read as: If S does not hold of the numeral for n, then T proves not D subscript S of the numeral for n. Since theory T is consistent, this implies that T does not prove D subscript S of the numeral for n. This implies that R does not hold of the Goedel number of D subscript S of u, and n.

Means: If S does not hold of the numeral for n, then T proves not D subscript S of the numeral for n. Since theory T is consistent, this implies that T does not prove D subscript S of the numeral for n. This implies that R does not hold of the Goedel number of D subscript S of u, and n.

1 occurrence in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not A

Means: not A

5 occurrences in this chapter

Equation form expr-c7e0b002595d5cf8

T={A:A⊢A}T = \Setabs{!A}{A \Proves !A}

Read as: T equals the set of sentences A that are provable from the axiom set named A

Means: T equals the set of sentences A that are provable from the axiom set named A

1 occurrence in this chapter

Equation form expr-cab917c13840b091

¬E\lnot !E

Read as: not E

Means: not E

1 occurrence in this chapter

Equation form expr-cade0c4cc96f01f9

Q¯⊆C¯\Th{\bar Q} \subseteq \Complement{C}

Read as: Q bar is a subset of the complement of C

Means: Q bar is a subset of the complement of C

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

2 occurrences in this chapter

Equation form expr-dabd3aff769f07eb

<<

Read as: the less than relation symbol

Means: the less than relation symbol

2 occurrences in this chapter

Equation form expr-db110f46a214e37e

¬S(n¯)→Q⊢¬DS(n¯)→DS(n¯)∈Q¯→DS(n¯)∉C\lnot S(\num n) & \lif & \Th{Q} \Proves \lnot !D_S(\num n) \\ & \lif & !D_S(\num n) \in \Th{\bar Q} \\ & \lif & !D_S(\num n) \not\in C

Read as: If S does not hold of the numeral for n, then Q proves not D subscript S of the numeral for n. This implies that D subscript S of the numeral for n belongs to Q bar. This in turn implies that D subscript S of the numeral for n does not belong to C.

Means: If S does not hold of the numeral for n, then Q proves not D subscript S of the numeral for n. This implies that D subscript S of the numeral for n belongs to Q bar. This in turn implies that D subscript S of the numeral for n does not belong to C.

1 occurrence in this chapter

Equation form expr-dd90fe2c42c9bea2

#A#\Gn{!A}

Read as: the Goedel number of A

Means: the Goedel number of A

1 occurrence in this chapter

Equation form expr-de821a9f13ec87f4

D(u)!D(u)

Read as: D of u

Means: D of u

2 occurrences in this chapter

Equation form expr-def9261af216c3fb

R(x,y)R(x,y)

Read as: R of x and y

Means: R of x and y

5 occurrences in this chapter

Equation form expr-df3b966b5b7ede0b

AT!A_T

Read as: A subscript T

Means: A subscript T

3 occurrences in this chapter

Equation form expr-df7e70e5021544f4

BB

Read as: B

Means: B

1 occurrence in this chapter

Equation form expr-e066055cd4f9fdb4

R(#DS(u)#,y)R(\Gn{!D_S(u)}, y)

Read as: R of the Goedel number of D subscript S of u, and y

Means: R of the Goedel number of D subscript S of u, and y

1 occurrence in this chapter

Equation form expr-e3dbf11d06b1c84e

AT(x¯,x¯,n¯)!A_T(\num x, \num x, \num n)

Read as: A subscript T of the numeral for x, the numeral for x, and the numeral for n

Means: A subscript T of the numeral for x, the numeral for x, and the numeral for n

1 occurrence in this chapter

Equation form expr-e632b7095b0bf32c

TT

Read as: T

Means: T

4 occurrences in this chapter

Equation form expr-e8bbdf6522a9a8ff

PrfQ(x,y)\Prf[\Th{Q}](x,y)

Read as: the proof coding relation for Q holds of x and y

Means: the proof coding relation for Q holds of x and y

1 occurrence in this chapter

Equation form expr-ff0ef5c23edbf7bf

B1!B_1

Read as: B subscript one

Means: B subscript one

1 occurrence in this chapter

Equation form expr-ffa444da4d73bfc1

Q¯\Th{\bar Q}

Read as: Q bar

Means: Q bar

6 occurrences in this chapter

Q is computably enumerable complete

Q is computably enumerable but not decidable. The source proves completeness by many one reduction from the diagonal halting set K, using a formula representing Kleene's T relation. The final summary changes notation from the representing formula to the relation itself; this source caveat is disclosed.

Source

Three implications reducing halting to provability in Q

Starting from x in K, obtain a halting computation witness s, then a Q proof of the representing formula at the numerals for x, x, and s, then a Q proof of its existential closure in s. The quantifier in the second step is outside provability; in the third step it is inside the proved formula.

Source

Definition of omega consistency

If T proves each negative numeral instance of a formula, at zero, one, two, and every further natural number, omega consistency requires that T not prove its positive existential closure. The infinite family is a condition on separate proofs, not a single universally quantified theorem.

Source

Omega consistent extensions of Q are undecidable

Every omega consistent theory containing Q is undecidable. The source adapts the diagonal halting reduction, replacing truth of all Q theorems with the specific omega consistency condition.

Source

There is no universal computable binary relation

No computable binary relation has a section representing every computable unary relation. The proof diagonalizes by negating the relation on equal arguments.

Source

Consistent extensions of Q are undecidable

Every consistent theory containing Q is undecidable. Assuming a decision procedure would make the relation expressing provability of numeral instances into a universal computable relation, contradicting the preceding lemma.

Source

Positive direction of universality

A positive instance of S implies provability of the corresponding numeral instance of its representative, which implies membership in the proposed universal relation. The source puts a numeral in the external relation S; its type notation is retained and noted.

Source

Negative direction using consistency

A negative instance of S gives a proof of the negated representing formula. Consistency then rules out a proof of the positive formula, so the proposed universal relation fails on this input. The negation of provability is not the provability of a negation; consistency connects these separate steps.

Source

True arithmetic is undecidable

The complete theory consisting of the true arithmetic sentences in the standard natural number interpretation is not decidable.

Source

Computably axiomatizable theories are computably enumerable

With a computable axiom set, theorems can be enumerated by searching finite derivations. A positive search terminates when it finds a proof; the source does not supply a decision procedure for nonmembers.

Source

Complete computably axiomatizable theories are decidable

An inconsistent theory is trivial. For the consistent case, search simultaneously for a proof of a sentence and a proof of its negation. Completeness ensures one search succeeds, and consistency makes its answer decisive.

Source

First incompleteness theorem from undecidability

Q has no extension that is simultaneously complete, consistent, and computably axiomatizable. Such an extension would be decidable by the preceding lemma, contradicting the earlier undecidability theorem.

Source

Provable and refutable sentences of Q are computably inseparable

Q and Q bar, the set of sentences refutable in Q, cannot be separated by a computable set. Q bar here is not the whole complement of Q. A separator would again yield a universal computable relation.

Source

Positive instances enter a proposed separator

If S holds, Q proves the corresponding representing instance, which therefore lies in C because C contains Q.

Source

Negative instances fall outside a proposed separator

If S fails, Q proves the negation of the representing instance. That instance therefore lies in Q bar, and hence outside C. The formula itself, not its negation, belongs to Q bar.

Source

Theories consistent with Q are undecidable

A theory need not contain Q for the result: it suffices that its union with Q is consistent. The finite conjunction E of the eight Q axioms produces the proposed separator through provability of implications from E.

Source

Undecidability of first order logic in the arithmetic language

The set of sentences provable in first order logic in the language of arithmetic is undecidable. These are the consequences of the empty premise set, which is consistent with Q.

Source

Undecidability through interpretation of arithmetic

If arithmetic is interpretable in the language of T and T is consistent with the interpretation of Q, T is undecidable. If T proves the interpreted axioms of Q, every consistent extension of T is undecidable. The proof is described as a modification of the preceding separation argument, not supplied in full.

Source

Source corollary concerning extensions of Z F C

The source states that there is no decidable extension of Z F C without repeating the necessary consistency qualifier. This omission is explicitly disclosed; the unqualified source sentence is retained rather than certified as a correct consequence.

Source

Incompleteness for computably axiomatizable extensions of Z F C

No extension of Z F C can be simultaneously complete, consistent, and computably axiomatizable.

Source

Undecidability with a binary relation symbol

First order logic for any language with a binary relation symbol is undecidable. The surrounding source discusses simulation by two unary functions and contrasts the stated decidable unary case.

Source

Cross-reference reference-000738

the definition of representability of a function in Q

Source occurrence

Cross-reference reference-000739

the definition of representability of a relation in Q

Source occurrence

Cross-reference reference-000740

the theorem that a function is representable in Q exactly when it is computable

Source occurrence

Cross-reference reference-000741

the theorem characterizing computable relations by representability in Q

Source occurrence

Cross-reference reference-000742

the introduction to representability in Q and its eight axioms

Source occurrence

Cross-reference reference-000743

the preceding definition of omega consistency

Source occurrence

Source disclosures

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

{A:A is provable in first-order logic}\Setabs{!A}{\text{$!A$ is provable in first-order logic}}

Read as: the set of sentences A such that A is provable in first order logic

Read in context source