Notes on Undecidability and Incompleteness

Stephen G. Simpson Department of Mathematics Pennsylvania State University http://www.math.psu.edu/simpson/

First Draft: November 18, 2008 This Draft: December 10, 2013

Abstract

Let Q be Robinson’s weak theory of arithmetic. We use recursiontheoretical methods to show that Q is essentially undecidable. Consequently, any recursively axiomatizable theory in which Q is interpretable is undecidable and incomplete. This is a strengthening of theorems of Gödel, Rosser and Tarski. We also present proofs of Gödel’s First and Second Incompleteness Theorems. In these proofs, the role of Q is perhaps a bit unusual.

1 Undecidable Theories

This section is based on a talk which I gave on November 18, 2008 in the Penn State Logic Seminar. Sankha Basu took notes, and this section is essentially a polished version of those notes.

*  *  *

Recall Chapter 2 of my Math 558 notes [1], where we proved that all recursive functions are definable over (ℕ, +, ·, 0, 1, =). We now begin with a refinement of that result.

Definition 1.1. The Δ_{0} formulas are the smallest class of number-theoretical formulas containing all atomic formulas (i.e., of the form t_{1} = t_{2} where t_{1}, t_{2} are polynomials with coefficients from ℕ) and closed under ∧, ∨, ¬, ⇒, ⇔ and bounded quantifiers (∀x < t), (∃x < t) where t is a term not involving x. Note that (∀x < t) Φ ≡ ∀x (x < t ⇒ Φ) and (∃x < t) Φ ≡ ∃x (x < t ∧ Φ).

Definition 1.2. A Δ_{0} predicate is a number-theoretical predicate P ⊆ ℕ^{k} which is defined over (ℕ, +, ·, 0, 1, =, <) by a Δ_{0} formula.

Remark 1.3. Obviously all Δ_{0} predicates are primitive recursive. It can be shown that the Δ_{0} predicates are a small subclass of the primitive recursive predicates. Trivially, the class of Δ_{0} predicates is closed under ∧, ∨, ¬, ⇒, ⇔ and bounded quantification.

Definition 1.4. A Σ_{1} formula is a formula of the form ∃x Φ where x is a number variable and Φ is a Δ_{0} formula. A generalized Σ_{1} formula is a formula of the form ∃x_{1} ⋯ ∃x_{k} Φ where x_{1}, …, x_{k} are number variables and Φ is a Δ_{0} formula. A Σ_{1} predicate is a number-theoretical predicate which is defined over ℕ by a Σ_{1} formula. Equivalently, it is defined over ℕ by a generalized Σ_{1} formula.

Lemma 1.5. The class of Σ_{1} predicates is closed under ∧, ∨, ∃x, ∃x < t, ∀x < t. Proof.

\begin{aligned}∃x ∃y \underbrace{P (x, y, −)}_{Δ_{0}} & ≡ & ∃z \underbrace{(∃x < z) (∃y < z) P (x, y, −).}_{Δ_{0}} \\ (∃x P (x, −)) ∧ (∃y Q(y, −)) & ≡ & ∃x ∃y (P (x, −) ∧ Q(y, −)). \\ (∀x < t) ∃y … & ≡ & ∃z (∀x < t) (∃y < z) …. \end{aligned}

Theorem 1.6. For every recursive function f : ℕ^{k} → ℕ, the graph of f is a Σ_{1} predicate.

Proof. We use the familiar characterization of recursive functions in terms of composition, primitive recursion and minimization.

Composition:

For example, suppose f = g ∘ h. Then

f(x) = y ≡ ∃z (\underbrace{h(x) = z}_{Σ_{1}} ∧ \underbrace{g(z) = y}_{Σ_{1}})

so this is Σ_{1}.

Minimization:

Suppose f(−) = least y such that R(−, y), where R is recursive. Then

f(−) = y ≡ \underbrace{χ_{R}(−, y) = 1}_{Σ_{1}} ∧(∀z < y) \underbrace{(χ_{R}(−, z) = 1)}_{Σ_{1}}

so this is Σ_{1}.

Primitive Recursion:

Recall the Gödel beta-function, β(a, r, i) = Rem(r, a · (i + 1) + 1). We have

β(a, r, i) = v ≡ ∃u ((r = u · (a · (i + 1) + 1) + v) ∧ (v < a · (i + 1) + 1)) so the graph of the beta-function is Σ_{1}. Now suppose f is obtained by primitive recursion, f(0, −) = g(−) and f(x + 1, −) = h(x, f(x, −), −) where the graphs of g and h are Σ_{1}. Then

\begin{aligned}f(x, −) = w & ≡ & ∃a ∃r (β(a, r, 0) = g(−) ∧ β(a, r, x) = w \\ & & ∧ (∀i < x) β(a, r, i + 1) = h(i, β(a, r, i), −)) \end{aligned}

so the graph of f is Σ_{1}. Corollary 1.7. The Σ_{1} predicates are the same as the Σ_{1}^{0} predicates. Proof. Clearly Σ_{1} implies Σ_{1}^{0}. Conversely, given a Σ_{1}^{0} predicate P (−) ≡ ∃x R(x, −) where R is recursive, we have

P (−) ≡ ∃x \underbrace{(χ_{R}(x, −) = 1)}_{Σ_{1}}

and this is Σ_{1}. Definition 1.8. We consider theories T = (L, S) where L is a finite language, the language of T, and S is a set of L-sentences, the axioms of T. Recall that an L-sentence is an L-formula with no free variables. Let B range over L-sentences.

1. T ⊢ B means that B is a theorem of T.

2. T is consistent if T ⊬ Φ ∧ ¬ Φ.

3. T is complete if for all B either T ⊢ B or T ⊢ ¬ B.

4. T is decidable if Thm_{T} = {#(B) | T ⊢ B} is recursive.

5. T is recursively axiomatizable if Ax_{T} := {#(B) | B ∈ S} is recursive. Examples 1.9.

1. Th(ℕ, +, ·, 0, 1, =), the complete theory of the natural numbers, is not decidable and not recursively axiomatizable. In this case L = {+, ·, 0, 1, =} and S = TrueSnt_{ℕ}.

2. Th(ℝ, +, ·, 0, 1, =), the complete theory of the real numbers, is decidable.

This is a consequence of quantifier elimination. In this case S = TrueSnt_{ℝ}. Theorem 1.10. If T is recursively axiomatizable, then Thm_{T} is recursively enumerable, i.e., Σ_{1}^{0}. Sketch of proof. Use the tableau method or some other proof system. Given an L-sentence B, search for a finite proof of B from the axioms of T. Theorem 1.11. If T is recursively axiomatizable and complete, then T is decidable.

Proof. Let B range over L-sentences. By Theorem 1.10 we have that {#(B) | T ⊢ B} is Σ_{1}^{0}. But then, by completeness of T, we also have that {#(B) | T ⊬ B} = {#(B) | T ⊢ ¬ B} is Σ_{1}^{0}. Hence {#(B) | T ⊢ B} is Δ_{1}^{0}, i.e., recursive. Thus T is decidable. Definition 1.12. Consider the particular theory Q. Roughly speaking, Q is first-order arithmetic minus the induction scheme. Formally, the language of Q is {+, ·, 0, =, S} where, + and · are binary operations, S is a unary operation, 0 is a constant, and = is a binary predicate. The axioms of Q are:

• ∀x ∀y (Sx = Sy ⇒ x = y)

• ∀x (Sx ≠ 0)

• ∀y (y ≠ 0 ⇒ ∃x (Sx = y))

• ∀x (x + 0 = x)

• ∀x ∀y (x + Sy = S(x + y))

• ∀x (x · 0 = 0)

• ∀x ∀y (x · Sy = x · y + x) The idea of using Q is due to Tarski/Mostowski/Robinson [2]. Remark 1.13. Q is a very weak fragment of first-order arithmetic. For instance Q ⊬ ∀x (0 + x = x), etc. Notation 1.14.

1. We write \underline{n} = \underbrace{S ⋯ S}_{n times} 0. Or, inductively, \underline{0} = 0 and \underline{n + 1} = S\underline{n} for each n ∈ ℕ.

2. We introduce a 2-place predicate ≤ by x ≤ y ≡ ∃z (z + x = y). Lemma 1.15. For each m, n ∈ ℕ the following are provable in Q:

1. \underline{m} + \underline{n} = \underline{m + n}

2. \underline{m} · \underline{n} = \underline{m · n}

3. ∀x (x ≤ \underline{n} ⇔ (x = \underline{0} ∨ x = \underline{1} ∨ ⋯ ∨ x = \underline{n − 1} ∨ x = \underline{n}))

4. \underline{m} ≠ \underline{n} if m ≠ n

5. \underline{m} ≤ \underline{n} if m ≤ n

6. ∀x (x ≤ \underline{n} ∨ \underline{n} ≤ x) Proof. By external induction on n.

1. E.g., \underline{3}+\underline{2} = SSS0+SS0 = S(SSS0+S0) = SS(SSS0+0) = SSSSS0 = \underline{5}.

2. Similar.

3. We prove this by external induction on n.

Base step, n = 0: x ≤ \underline{0}. So ∃w (w + x = 0). This implies, x = 0 because otherwise x = Su for some u. Then 0 = w + Su = S(w + u) which is a contradiction.

Induction step: Suppose the claim holds for all n ≤ k where, k ≥ 0. We now prove it for n = k + 1. Suppose x ≤ \underline{k + 1}. Then w + x = \underline{k + 1} for some w. If x = 0, we are done. If x ≠ 0, x = Su for some u, so w + x = w + Su = \underline{k + 1}. Now w + Su = S(w + u), so w + u = \underline{k}. Then by induction hypothesis u = \underline{0} ∨ u = \underline{1} ∨ ⋯ ∨ u = \underline{n} which implies x = \underline{1} ∨ x = \underline{2} ∨ ⋯ ∨ x = \underline{k + 1}, Q.E.D.

4. E.g., we prove \underline{2} ≠ \underline{3}. Suppose \underline{2} = \underline{3}, i.e., SS0 = SSS0. This implies S0 = SS0 which in turn implies 0 = S0, a contradiction.

5. Similar.

6. Suppose, x ≰ \underline{n}. Then by part 3, x ≠ \underline{0}, \underline{1}, …, \underline{n}, so we can deduce from the axioms of Q that x = \underbrace{SS ⋯ S}_{n+1} w for some w. Then x = \underbrace{SS ⋯ S}_{n+1} w =

Sw + \underbrace{SS ⋯ S}_{n} 0 = Sw + \underline{n}, hence \underline{n} ≤ x.

Theorem 1.16. For all Δ_{0} sentences Φ we have:

1. Q ⊢ Φ if and only if Φ is true.

2. Q ⊢ ¬ Φ if and only if Φ is not true.

Proof. The proof is by induction on the number of connectives and quantifiers in Φ. Suppose for instance that Φ ≡ (∀x ≤ t) Ψ where t is a variable-free term. By inductive hypothesis, Q ⊢ Ψ[x/\underline{n}] for all n ≤ t. Using part 3 of Lemma 1.15, we have Q ⊢ ∀x (x ≤ t ⇒ Ψ), i.e., Q ⊢ Φ, Q.E.D. Next, suppose Φ ≡ (∃x ≤ t) Ψ. By inductive hypothesis, there is n ≤ t such that Q ⊢ Ψ[x/\underline{n}]. Also, Q ⊢ \underline{n} ≤ t, so Q ⊢ (∃x ≤ t)Ψ, i.e., Q ⊢ Φ, Q.E.D.

Theorem 1.17. For all generalized Σ_{1} sentences S, Q ⊢ S if and only if S is true.

Proof. Since the axioms of Q are true, all sentences provable in Q are true. For the converse, let S ≡ ∃x_{1} ⋯ ∃x_{k} Φ where Φ is Δ_{0}. If S is true, let m_{1}, …, m_{k} ∈ ℕ be such that Φ[x_{1}/\underline{m_{1}}, …, x_{k}/\underline{m_{k}}] is true. Then, by the previous theorem, Q ⊢ Φ[x_{1}/\underline{m_{1}}, …, x_{k}/\underline{m_{k}}]. It follows that Q ⊢ ∃x_{1} ⋯ ∃x_{k} Φ, i.e., Q ⊢ S, Q.E.D.

Theorem 1.18. Q is undecidable.

Proof. Let H = the Halting Problem. Recall that H is Σ_{1}^{0} but not recursive. Let Halt be a Σ_{1} formula defining H. Then

H = \{n | Halt[x/\underline{n}] is true\}
= \{n | Q ⊢ Halt[x/\underline{n}]\}
= \{n | Q ⊢ ∃x (x = \underline{n} ∧ Halt)\}.

Now f(n) := #(∃x (x = \underline{n} ∧ Halt)) is a primitive recursive function. Moreover H is reducible to Thm_{Q} = {#(B) | Q ⊢ B} via f. In other words, n ∈ H ⇔ f(n) ∈ Thm_{Q}. Since H is nonrecursive, it follows that Thm_{Q} is nonrecursive, i.e., Q is undecidable.

Remark 1.19. It follows from Theorems 1.18 and 1.11 that Q is incomplete, but this was obvious anyway. We are now going to show that any consistent theory which contains Q is incomplete.

Definition 1.20. Two sets A, B ⊆ ℕ are said to be recursively inseparable if there is no recursive set X such that A ⊆ X and X ∩ B = ∅.

Remark 1.21. Let A, B ⊆ ℕ be recursively enumerable (i.e., Σ_{1}^{0}), and disjoint and recursively inseparable. It is well known that such a pair of sets exists. Let A, B be defined by Σ_{1} formulas ∃y Φ and ∃z Ψ be Σ_{1} respectively. Thus A = \{m | ∃y Φ[x/\underline{m}]\} and B = \{m | ∃z Ψ[x/\underline{m}]\} where Φ and Ψ are Δ_{0} formulas. Let Φ^{∗} ≡ Φ ∧ ¬ (∃z ≤ y) Ψ. This is again a Δ_{0} formula. Note that A = \{m | ∃y Φ^{∗}[x/\underline{m}]\}. The passage from Φ to Φ^{∗} is known as Rosser’s Trick.

Theorem 1.22. Let T be a consistent theory which contains Q. Then T is undecidable.

Proof. Let A, B, Φ, Ψ, Φ^{∗} be as in Remark 1.21. Let

A^{∗} = \{m ∈ ℕ | T ⊢ ∃y Φ^{∗}[x/\underline{m}]\}.

As before, A^{∗} is reducible to Thm_{T}. Thus, it will suffice to show that A^{∗} is not recursive.

Obviously A^{∗} ⊇ A, because for all m ∈ A we have Q ⊢ ∃y Φ^{∗}[x/\underline{m}], hence T ⊢ ∃y Φ^{∗}[x/\underline{m}], hence m ∈ A^{∗}.

We claim that A^{∗} ∩ B = ∅. To see this, suppose m ∈ A^{∗} ∩ B. Because m ∈ A^{∗} we have T ⊢ ∃y Φ^{∗}[x/\underline{m}], i.e.,

T ⊢ ∃y (Φ[x/\underline{m}] ∧ ¬ (∃z ≤ y) Ψ[x/\underline{m}]).  (1)

At the same time, because m ∈ B we have ∃z Ψ[x/\underline{m}] so let n ∈ ℕ be such that Ψ[x/\underline{m}, z/\underline{n}] holds. Then Q ⊢ Ψ[x/\underline{m}, z/\underline{n}], hence

T ⊢ Ψ[x/\underline{m}, z/\underline{n}].  (2)

Combining (1) and (2) we obtain

T ⊢ ∃y (Φ[x/\underline{m}] ∧ \underline{n} ≰ y)  (3)

and from (3) and Lemma 1.15 it follows that

T ⊢ ∃y (Φ[x/\underline{m}] ∧ (y = \underline{0} ∨ ⋯ ∨ y = \underline{n})),

i.e.,

T ⊢ Φ[x/\underline{m}, y/\underline{0}] ∨ ⋯ ∨ Φ[x/\underline{m}, y/\underline{n}].  (4)

On the other hand, because m ∈ B and A ∩ B = ∅ we have m ∉ A, hence ¬ ∃y Φ[x/\underline{m}] holds, hence for all k ∈ ℕ we have ¬ Φ[x/\underline{m}, y/\underline{k}] hence Q ⊢ ¬ Φ[x/\underline{m}, y/\underline{k}] hence T ⊢ ¬ Φ[x/\underline{m}, y/\underline{k}] so in particular

T ⊢ ¬ (Φ[x/\underline{m}, y/\underline{0}] ∨ ⋯ ∨ Φ[x/\underline{m}, y/\underline{n}]).  (5)

Now (4) and (5) contradict our assumption that T is consistent. This proves our claim.

We have seen that A^{∗} ⊇ A and A ∩ B = ∅. Since A and B are recursively inseparable, it follows that A^{∗} is nonrecursive. Hence Thm_{T} is nonrecursive, i.e., T is undecidable.

Theorem 1.23. Let T be a recursively axiomatizable, consistent theory which contains Q. Then T is undecidable and incomplete.

Proof. Immediate from Theorems 1.11 and 1.22.

Corollary 1.24. Each of the theories Z_{1}, Z_{2}, ZFC, … is undecidable and incomplete.

Proof. Let T be any of these recursively axiomatizable theories. Clearly Q is interpretable in T, i.e., we can find a definitional extension T′ of T which contains Q. Then, by Theorems 1.22 and 1.23, T′ is undecidable and incomplete. Using known results on definitional extensions, it follows that T is undecidable and incomplete.

2 The Incompleteness Theorems of Gödel

In this section we sketch a proof of Gödel’s First and Second Incompleteness Theorems. I presented this proof in December 2009 in a course at Penn State. In this presentation, the role of Robinson’s theory Q is perhaps a bit unusual.

Lemma 2.1. Let f : ℕ → ℕ be a recursive function. Then, we can find a Σ_{1} formula F in the language of Q which represents f in the sense that

Q ⊢ ∀x (x = \underline{f(m)} ⇔ F [w/\underline{m}])

for each m ∈ ℕ. The free variables of F are w and x.

Proof. Since f is recursive, the graph of f is Σ_{1}-definable over the natural numbers. Let ∃y_{1} ⋯ ∃y_{k} Φ be a Σ_{1} formula with free variables w and x which defines f over ℕ. Thus for all m, n ∈ ℕ we have that f(m) = n if and only if ∃y_{1} ⋯ ∃y_{k} Φ[w/\underline{m}, x/\underline{n}] holds in ℕ. Let F be the following Σ_{1} formula:

There exists z such that

1. z = the least z such that (∃x, y_{1}, …, y_{k} ≤ z) Φ,

2. x = the least x ≤ z such that (∃y_{1}, …, y_{k} ≤ z) Φ.

Note that the free variables of F are w and x. We can use our lemmas concerning Q to show that F has the desired property.

Lemma 2.2 (Self-Reference Lemma). Let L be a recursive language which includes the language of Q. Let A be an L-formula. Let T be an L-theory which includes Q. Let x be a number variable. Then, we can find an L-formula B such that

T ⊢ B ⇔ A[x/\underline{#(B)}].

Remark 2.3. The free variables of B are those of A except for x. In particular, if x is the only free variable of A, then B is an L-sentence.

Proof of Lemma 2.2. Let w be a number variable different from x and which does not occur in A. For all m ∈ ℕ let d(m) = sub(m, #(w), num(m)). Note that d : ℕ → ℕ is a primitive recursive function and for all L-formulas C we have d(#(C)) = #(C[w/\underline{#(C)}]). Let D be a Σ_{1} formula which represents d as in Lemma 2.1. The free variables of D are w and x and for each m ∈ ℕ we have

Q ⊢ ∀x (x = \underline{d(m)} ⇔ D[w/\underline{m}]).

Let A^{∗} be the formula ∀x (D ⇒ A), and let B be the formula A^{∗}[w/\underline{#(A^{∗})}]. Since d(#(A^{∗})) = #(B), we have

Q ⊢ ∀x (x = \underline{#(B)} ⇔ D[w/\underline{#(A^{∗})}]).

It follows that

T ⊢ A[x/\underline{#(B)}] ⇔ ∀x (D[w/\underline{#(A^{∗})}] ⇒ A),

i.e.,

T ⊢ A[x/\underline{#(B)}] ⇔ A^{∗}[w/\underline{#(A^{∗})}],

i.e.,

T ⊢ A[x/\underline{#(B)}] ⇔ B.

This completes the proof.

Definition 2.4 (the provability predicate). Let L be a recursive language, and let T be a recursively axiomatizable L-theory. By Theorem 1.10 the set Thm_{T} = {#(B) | T ⊢ B} is recursively enumerable, i.e., Σ_{1}^{0}. By Corollary 1.7 let Pvbl_{T} be a Σ_{1} formula which defines Thm_{T} over ℕ. Thus Thm_{T} = {m ∈ ℕ | Pvbl_{T} [x/\underline{m}]\}. Here x is number variable, the only free variable of Pvbl_{T}. The Σ_{1} formula Pvbl_{T} is called the provability predicate for T.

Lemma 2.5. Let L be a recursive language which includes the language of Q. Let T be a recursively axiomatizable L-theory. Then, we can find a sentence G = G_{T} such that

Q ⊢ G ⇔ ¬ Pvbl_{T} [x/\underline{#(G)}].

Moreover G is of the form ¬ S where S is a generalized Σ_{1} sentence.

Proof. This is essentially the special case of Lemma 2.2 with T = Q and A = ¬ Pvbl_{T}. However, we have to slightly modify the proof of Lemma 2.2. Instead of A^{∗} use the logically equivalent formula ¬ S^{∗} where S^{∗} is generalized Σ_{1}. Explicitly, S^{∗} is ∃x ∃y ∃z (Φ ∧ Ψ) where D is ∃y Φ and Pvbl_{T} is ∃z Ψ and Φ and Ψ are Δ_{0} formulas. Then G is (¬ S^{∗})[w/\underline{#(¬ S^{∗})}] and the proof goes through as before. Note that G is identical to ¬ S where S is the generalized Σ_{1} sentence S^{∗}[w/\underline{#(¬ S^{∗})}].

Theorem 2.6 (The First Incompleteness Theorem). Let L be a recursive language which includes the language of Q. Let T be a recursively axiomatizable L-theory which includes Q. If T is consistent, then T ⊬ G_{T}.

Proof. Let G = G_{T} and suppose T ⊢ G. Then Pvbl_{T} [x/\underline{#(G)}] is true. Since the axioms of Q are true, it follows by Lemma 2.5 that ¬ G is true. Moreover ¬ G is logically equivalent to a generalized Σ_{1} sentence, so by Theorem 1.17 we have Q ⊢ ¬ G. Since T ⊇ Q it follows that T ⊢ ¬ G. Thus T is inconsistent.

Remark 2.7. Theorem 2.6 is a refinement of Gödel’s First Incompleteness Theorem. The sentence G_{T} is known as the Gödel sentence for T. Note that G_{T}, although not provable in T, is true. This is because, by Lemma 2.5, G_{T} is equivalent to T ⊬ G_{T}, and the latter statement is true in view of Theorem 2.6.

Remark 2.8. Next we turn to Gödel’s Second Incompleteness Theorem. In order to prove the Second Incompleteness Theorem, we need an additonal condition on T. The condition that we need is adequacy as formulated in the following definition. It can be shown that each of the theories Z_{1}, Z_{2}, ZFC, etc., is adequate. It is not clear whether Q is adequate. It is conceivable that the adequacy of Q may depend on the choice of the provability predicate Pvbl_{Q}.

Definition 2.9 (adequacy). Let L be a recursive language which includes the language of Q. Let T be a recursively axiomatizable L-theory which includes Q. We say that T is adequate if

T ⊢ S ⇒ Pvbl_{T} [x/\underline{#(S)}]

for all generalized Σ_{1} sentences S. Note that, in view of Theorem 1.17, all sentences of the form S ⇒ Pvbl_{T} [x/\underline{#(S)}] where S is a generalized Σ_{1} sentence are true. Hence, it is reasonable to expect these sentences to be provable in T.

Definition 2.10 (the consistency sentence). Let L be a recursive language which includes the language of Q. Let T be a recursively axiomatizable Ltheory which includes Q. Let G = G_{T} be the Gödel sentence for T. Recall that G is of the form ¬ S where S is a generalized Σ_{1} sentence. Let Con_{T} be the sentence ¬ (Pvbl_{T} [x/\underline{#(S)}]∧Pvbl_{T} [x/\underline{#(¬ S)}]). Note that T is consistent if and only if Con_{T} is true. The sentence Con_{T} is known as the consistency sentence for T.

Theorem 2.11 (the Second Incompleteness Theorem). Let L be a recursive language which includes the language of Q. Let T be a recursively axiomatizable L-theory which includes Q and is adequate. If T is consistent, then T ⊬ Con_{T}.

Proof. Write G = G_{T}. By Theorem 2.6 we have T ⊬ G. Therefore, it suffices to show that T ⊢ Con_{T} ⇒ G, i.e., T ⊢ S ⇒ ¬ Con_{T}. Here G = ¬ S where S is a generalized Σ_{1} sentence. By adequacy of T we have

T ⊢ S ⇒ Pvbl_{T} [x/[\underline{#(S)}].  (6)

On the other hand, by Lemma 2.5 we have

T ⊢ G ⇔ ¬ Pvbl_{T} [x/\underline{#(G)}],

i.e.,

T ⊢ S ⇔ Pvbl_{T} [x/\underline{#(¬ S)}].  (7)

Combining (6) and (7) we have

T ⊢ S ⇒ (Pvbl_{T} [x/[\underline{#(S)}] ∧ Pvbl_{T} [x/\underline{#(¬ S)}]),

i.e., T ⊢ S ⇒ ¬ Con_{T}, Q.E.D.

References

[1] Stephen G. Simpson. Foundations of Mathematics. Unpublished lecture notes, Department of Mathematics, Pennsylvania State University, 123 pages, 1995–2009.

[2] Alfred Tarski, Andrzej Mostowski, and Raphael M. Robinson. Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North-Holland, 1953. IX + 98 pages.