2.4.1.1. Term

Define T_C as follows.

\begin{align*} u \in T_C &\iff && (\exists z)[u = \widehat{\#z}] \lor {} \\ & && (\exists x) [u = \widehat{\&x}] \lor {} \\ & && (\exists k, f, v) [\mathrm{Func}_k(f) \land \mathrm{Seq}(v) \land k = \mathrm{lh}(v) \land (\forall i, z)[\braket{i, z} \in v \to z \in C] \land u = \widehat{f^k(v)}] \\ \end{align*}

\widehat{\bullet} is a quasi-quotation..

\begin{align*} \text{bounded variable: }&& \widehat{\#z} &\coloneqq \braket{0, z} + 1 \\ \text{free variable: }&&\widehat{\&x} &\coloneqq \braket{1, x} + 1 \\ \text{function: }&&\widehat{f^k(v)} &\coloneqq \braket{2, f, k, v} + 1 \\ \end{align*}

T_C is \Delta_1 (if C is a finite set) and monotone. Let \mathrm{UTerm}(t) be a fixedpoint of T_C. It is \Delta_1 since T_C satisfies strong finiteness. Define the function \mathrm{termBV}(t) inductively on \mathrm{UTerm} meaning the largest bounded variable +1 that appears in the term. Define \mathrm{Semiterm}(n, t) := \mathrm{UTerm}(t) \land \mathrm{termBV}(t) \le n.

LO.ISigma1.Metamath.IsSemiterm.{u_1, u_2} {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (n t : V) :
  Prop
LO.ISigma1.Metamath.IsSemiterm.{u_1, u_2}
  {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable]
  [L.LORDefinable] (n t : V) : Prop

2.4.1.2. Formula

Similarly, Define F_C:

\begin{align*} u \in F_C &\iff && (\exists k, R, v)[\mathrm{Rel}_k(R) \land \text{$v$ is a list of $\mathrm{UTerm}$ of length $k$} \land u = \widehat{R^k (v)}] \lor {} \\ & && (\exists k, R, v)[\mathrm{Rel}_k(R) \land \text{$v$ is a list of $\mathrm{UTerm}$ of length $k$} \land u = \widehat{\lnot R^k (v)}] \lor {} \\ & && [u = \widehat{\top}] \lor {} \\ & && [u = \widehat{\bot}] \lor {} \\ & && (\exists p \in C, q \in C) [u = \widehat{p \land q}] \lor {} \\ & && (\exists p \in C, q \in C) [u = \widehat{p \lor q}] \lor {} \\ & && (\exists p \in C) [u = \widehat{\forall p}] \lor {} \\ & && (\exists p \in C) [u = \widehat{\exists p}] \end{align*}

\begin{align*} \widehat{R^k(v)} &\coloneqq \braket{0, R, k, v} + 1\\ \widehat{\lnot R^k(v)} &\coloneqq \braket{1, R, k, v} + 1 \\ \widehat{\top} &\coloneqq \braket{2, 0} + 1\\ \widehat{\bot} &\coloneqq \braket{3, 0} + 1\\ \widehat{p \land q} &\coloneqq \braket{4, p, q} + 1\\ \widehat{p \lor q} &\coloneqq \braket{5, p, q} + 1\\ \widehat{\forall p} &\coloneqq \braket{6, p} + 1\\ \widehat{\exists p} &\coloneqq \braket{7, p} + 1\\ \end{align*}

F_C is \Delta_1 and monotone. Let \mathrm{UFormula}(p) be a fixedpoint of F_C and define

\mathrm{Semiformula}(n, p) \iff \mathrm{UFormula}(p) \land \mathrm{bv}(p) \le n

LO.ISigma1.Metamath.IsSemiformula.{u_1, u_2} {V : Type u_1}
  [ORingStruc V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable]
  [L.LORDefinable] (n p : V) : Prop
LO.ISigma1.Metamath.IsSemiformula.{u_1,
    u_2}
  {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable]
  [L.LORDefinable] (n p : V) : Prop

LO.ISigma1.Metamath.IsSemiformula.mk.{u_1, u_2}

isUFormula : IsUFormula L p

bv_le : bv L p ≤ n

The function \mathrm{bv}(p) is defined inductively on \mathrm{UFormula} meaning the largest bounded variable +1 that appears in the formula.

\mathrm{UFormula}(p) and \mathrm{Semiormula}(n, p) are again \Delta_1 since F_C satisfies strong finiteness.

LO.ISigma1.Metamath.IsUFormula.{u_1, u_2} {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : V → Prop
LO.ISigma1.Metamath.IsUFormula.{u_1, u_2}
  {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable]
  [L.LORDefinable] : V → Prop

2.4.3.1. Fixed-point Lemma

Since the substitution is \Sigma_1, There is a formula \mathrm{ssnum}(y, p, x) such that, for all formula \varphi with only one variable and x, y \in V,

\mathrm{ssnum}(y, {\ulcorner \varphi \urcorner}, x) \iff y = \ulcorner \varphi(\overline{x}) \urcorner

holds. (overline \overline{\bullet} denotes the (formalized) numeral of x)

Define a sentence \mathrm{fixedpoint}_\theta for formula (with one variable) \theta as follows.

\begin{align*} \mathrm{fixedpoint}_\theta &\coloneqq \mathrm{diag}_\theta(\overline{\ulcorner \mathrm{diag}_\theta \urcorner}) \\ \mathrm{diag}_\theta(x) &\coloneqq (\forall y)[\mathrm{ssnum}(y, x, x) \to \theta (y)] \end{align*}

By simple reasoning, it can be checked that f satisfies the following:

T \vdash \mathrm{fixedpoint}_\theta \leftrightarrow \theta({\ulcorner \mathrm{fixedpoint}_\theta \urcorner})

2.4.3.2. Main Theorem

Let T be a \Delta_1-theory, which is stronger than \mathsf{I}\Sigma_1.

We will use \square \varphi to denote \mathrm{Provable}(\ulcorner\varphi\urcorner). Define Gödel sentence \mathsf{G}, as \mathrm{fixedpoint}_{\lnot\mathrm{Provable}_T(x)} using fixed-point theorem, satisfies

T \vdash \mathsf{G} \leftrightarrow \lnot \mathrm{Provable}(\ulcorner\mathsf{G}\urcorner)

Gödel sentence is undecidable, i.e., T \nvdash \mathsf{G} if T is consistent,

And T \nvdash \lnot\mathsf{G} if \mathbb{N} \models T.

Define formalized consistent statement \mathrm{Con}_T as \lnot\mathrm{Provable}_T(\ulcorner \bot \urcorner):

And, surprisingly enough, it can be proved that Gödel sentence \mathsf{G} is equivalent to the consistency statement.

Finally, combined with the fact that \mathsf{G} is independent, we can prove that the consistency statement is also independent.

LO.FirstOrder.Arithmetic.consistent_unprovable (T : Theory ℒₒᵣ) [T.Δ₁]
  [𝗜𝚺₁ ⪯ T] [Consistent T] : T ⊬ ↑T.consistent
LO.FirstOrder.Arithmetic.consistent_unprovable
  (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T]
  [Consistent T] : T ⊬ ↑T.consistent

LO.FirstOrder.Arithmetic.inconsistent_independent (T : Theory ℒₒᵣ)
  [T.Δ₁] [𝗜𝚺₁ ⪯ T] [ArithmeticTheory.SoundOnHierarchy T 𝚺 1] :
  Independent T ↑T.consistent
LO.FirstOrder.Arithmetic.inconsistent_independent
  (T : Theory ℒₒᵣ) [T.Δ₁] [𝗜𝚺₁ ⪯ T]
  [ArithmeticTheory.SoundOnHierarchy T 𝚺
      1] :
  Independent T ↑T.consistent