Intoduction

Formalized Formal Logic is aim to formalize some various results of mathematical logic in Lean Theorem Prover.

Kites

Visualization for sublogic/subtheory relations.

Modal Logics

First-Order Arithmetics

Import Graph

Generated by import-graph

PDF version

Viasualization

References and

References

• J. Han, F. van Doorn, "A formalization of forcing and the unprovability of the continuum hypothesis"
• W. Pohlers, "Proof Theory: The First Step into Impredicativity"
• P. Hájek, P. Pudlák, "Metamathematics of First-Order Arithmetic"
• R. Kaye, "Models of Peano arithmetic"
• 田中 一之 (編), 『ゲーデルと 20 世紀の論理学』
• 菊池 誠 (編), 『数学における証明と真理 ─ 様相論理と数学基礎論』
• P. Blackburn, M. de Rijke, Y. Venema, "Modal Logic"
• Open Logic Project, "The Open Logic Text"
• R. Hakli, S. Negri, "Does the deduction theorem fail for modal logic?"
• G. Boolos, "The Logic of Provability"
• M. C. Fitting, V. W. Marek, and M. Truszczynski, "The Pure Logic of Necessitation"
• T. Kurahashi, "The provability logic of all provability predicates"
• W. Carnielli, C. Pizzi, "Modalities and Multimodalities"
• A. Chagrov, M. Zakharyaschev, "Modal Logic"
• G. E. Hughes, M. J. Cresswell, "A New Introduction to Modal Logic"
• K. Segerberg, "An Essay in Classical Modal Logic"

Related Works

Here is the list of project particularly formalize mathematical logics. If you find something missing from this list or add, report via issues.

Lean 4

m4lvin/lean4-pdl

Propositional dynamic logics.

alexoltean61/hybrid_logic_lean

Hybrid logic. Syntax and semantics for hybrid logic are provided, and some facts and soundness have been proven. However completeness seems to have been not yet formalized.

• Andrei-Alexandru Oltean, "A Formalization of Hybrid Logic in Lean"

leanprover-community/con-nf

Formalizing the consistency of Quine's set theory "New Foundations": $\mathrm{Con}(\mathbf{NF})$.

• Website

Lean 3

flypitch

Independence of the continuum hypothesis.

• Jesse Michael Han and Floris van Doorn, "A Formal Proof of the Independence of the Continuum Hypothesis"

bbentzen/ipl

Intuitionistic propositional logic.

Hilbert-style deduction system, Kripke semantics and Henkin-style (constructing maximal prime set and canonical model) completeness proof.

• Huayo Guo, Dongheng Chen, Bruno Bentzen, "Verified completeness in Henkin-style for intuitionistic propositional logic"

bbentzen/mpl

Normal modal logic.

Hilbert-style deduction system, Kripke semantics and Henkin-style (constructing maximal consistent set and canonical model) completeness proof for $S5$.

• Bruno Bentzen, "A Henkin-style completeness proof for the modal logic S5"

paulaneeley/modal

Formalization of modal logic $S5$ and public announcement logic.

• Paula Neeley, "A Formalization of Dynamic Epistemic Logic"

minchaowu/ModalTab

Tableaux system for modal logic $\mathbf{K},\mathbf{KT},S4$.

• Minchao Wu, Rajeev Goré, "Verified Decision Procedures for Modal Logics"

ljt12138/Formalization-PAL

$S5$ and public announcement logic (PAL). Main result are recursion theorem (reducing public announce modality for any PAL formula) and completeness of $S5$.

• Jiatu Li, "Formalization of PAL⋅S5 in Proof Assistant"

Isabelle

Lawrence C. Paulson, "Gödel's Incompleteness Theorems"

Formalized Gödel's first and second incompleteness theorems. Remark the second incompleteness theorem is proved on hereditarily finite sets.

• paper: Lawrence C. Paulson, "A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets"

Christoph Benzmüller, Woltzenlogel Paleo, "Gödel's God in Isabelle/HOL"

Gödel's ontological argument of God's existence.

jrh13/hol-light/GL

Completeness of Gödel-Löb (provability) modal logic $\mathbf{GL}$ in HOL/Light.

• Marco Maggesi, Cosimo Perini Brogi, "Mechanising Gödel–Löb Provability Logic in HOL Light"

u5943321/Modal-Logic

Modal Logic, based on textbook "Modal Logic" by P. Blackburn, M. de Rijke, Y. Venema in HOL.

• Yiming Xu, "Formalizing Modal Logic in HOL"

Coq

ianshil/PhD_thesis

Coq formalization of several modal logics (related provability logic and etc.) and their caliculi.

• Ian Shillito, New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq.

hferee/UIML

Uniform interpolants for basic modal logic $\mathbf{K}$, Gödel-Löb provability logic $\mathbf{GL}$, intuitionistic strong Löb logic $\mathbf{iSL}$.

• demo
• Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito, "Mechanised uniform interpolation for modal logics K, GL and iSL"

ana-borges/QRC1-Coq

Quantified modal logic called Quantified Reflection Calculus with one modality $\mathsf{QR}{\mathsf{C}}_1$.

Christian Doczkal, Gert Smolka, "Completeness and decidability of converse PDL in the constructive type theory of Coq"

Propositional Dynamic Logic.

Christian Doczkal, Gert Smolka, "Constructive Formalization of Hybrid Logic with Eventualities"

Hybrid Logic.

Russell O'Connor's continuous works on Incompleteness Theorem

• Russell O’Connor, "Essential Incompleteness of Arithmetic Verified by Coq"

fondefjobn/S5-Formalization-in-Coq

Modal logic $S5$, its Kripke completeness.

• Lubor Budaj, "Formalization of modal logic $S5$ in the Coq proof assistant"

Floris van Doorn, "Propositional Calculus in Coq"

Hilbert deduction system, natural deduction system, and sequent calculus for classical propositional logic. Formalized completeness of natural deduction system, the provability equivalence of three calculi, cut-elimination for sequent calculus.

Christoph Benzmüller, Bruno Woltzenlogel Paleo, "Interacting with Modal Logics in the Coq Proof Assistant"

Modal logic and Gödel's ontological argument of existence of God.

mphilipse/coq-multi-agent-systems

Multi-agent epistemic modal logic ${S5}^n$.

• Michiel Philipse, "Distributed Knowledge Proofs in the Coq Proof Assistant"

Iris Project

Framework for concurrent saparation logic. Verified in Coq.

First-Order Logic

TODO:

Term and Formula

Notation

Quantification of formulae are defined using de Bruijn index, but we can write terms and formulae by usual binder notation using macro.

variables x y z is just an example and can take any number of idents. e is an expression of term/formula.

Binder Notation

Binder notation of term takes either form:

• Term: ‘x y z. e’, Formula: “x y z. e”
  • x y z is the symbol for the bound variables, k:num-variables denotes the terms in Semiterm L ξ (n + $k)/Semiformula L ξ (n + $k). (n can be variable)
• Term: ‘x y z | e’, Formula: “x y z | e”
  • x y z is the symbol for the free variables, k:num-variables denotes the terms in Semiterm L ξ n/Semiformula L ξ n. (n can be variable)
• Term: ‘e’, Formula: “e”
  • An abbreviation of ‘ . e’/“ . e”

Expression of term/formula

Deduction System for First-Order Logic

Semantics for First-Order Logic

Completeness Theorem

Arithmetics

In this formalization, we prefer developing arithmetic model theoretic, i.e. show $T\models \sigma$ instead of $T⊢\sigma$ (They are equivalent thanks to the completeness theorem.). This approach has several advantages:

1. In general, writing a formalized proof (in formalized system!) is very tedious. Meta-proofs, on the other hand, tend to be relatively concise.
2. Many definitions and proofs of logic and algebra in Mathlib can be used.
3. Metaprogramming can streamline the proof process (especially definability).
4. It is easy to extend predicates and functions. When adding predicates or functions, it is necessary to extend its language by extension by definition in case of formalized proof, but not in model theoretic approach.

This procedure is done as follows. Suppose we wish to prove that the totality of an exponential function can be proved in $\mathsf{I}{\Sigma }_1$. First, the graph of the exponential function must be defined. This is achieved by the following two definitions.

1. Semantic definition.

   def Exponential {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] :
       M → M → Prop
   

2. Syntactic definition that expresses the semantic definition.

   def exponentialDef : 𝚺₀-Semisentence 2
   
       lemma Exponential.defined :
           𝚺₀-Relation (Exponential : M → M → Prop) via exponentialDef
       ```
   
   Then prove the totality.
   

theorem Exponential.total  {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] (x : M) : ∃ y, Exponential x y

Since Exponential and Exponential.total are defined in all the model of $\mathsf{I}{\Sigma }_1$, 𝐈𝚺₁ ⊢! ∀' ∃' exponentialDef is obtained by the completeness theorem. This was the result we wanted to achieve.

Defined Predicates and Functions

Theories of Arithmetics

Theory $\mathsf{I}{\Sigma }_0$

Exponential

The graph of exponential $\mathrm{Exp}(x,y)$ is definable by ${\Sigma }_0$-fomrula, and its inductive properties are proved in $\mathsf{I}{\Sigma }_0$.

instance exponential_definable [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)

• LO.Arith.exponential_definable

lemma exponential_zero_one [M ⊧ₘ* 𝐈𝚺₀] :
    Exponential 0 1

• LO.Arith.Exponential.exponential_zero_one

lemma exponential_succ_mul_two [M ⊧ₘ* 𝐈𝚺₀] {x y : M} :
    Exponential (x + 1) (2 * y) ↔ Exponential x y

• LO.Arith.Exponential.exponential_succ_mul_two

Other basic functions, such as $\log x,|x|$ are defined by using exponential.

Theory $\mathsf{I}{\Sigma }_1$

Exponential

It is proved that the graph of exponential is definable by ${\Sigma }_0$-formula, and their inductive properties are provable in $\mathsf{I}{\Sigma }_0$. In $\mathsf{I}{\Sigma }_1$, we can further prove their entireness.

Theory of Hereditary Finite Sets in $\mathsf{I}{\Sigma }_1$

Weak theory of sets in $V_{\omega }$ (Hereditary Finite Sets) can be developed inside $\mathsf{I}{\Sigma }_1$ using Ackermann coding and bit predicate. Hereafter, we will use the notation $i\in a$ in the sense of bit predicate:

lemma mem_iff_bit [M ⊧ₘ* 𝐈𝚺₁] {i a : M} : i ∈ a ↔ Bit i a

• LO.Arith.mem_iff_bit

The following comprehension holds.

theorem finset_comprehension₁ [M ⊧ₘ* 𝐈𝚺₁]
    {P : M → Prop} (hP : (Γ, 1)-Predicate P) (a : M) :
    ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

• LO.Arith.finset_comprehension₁

The basic concepts of set theory, such as union, inter, cartesian product, and mapping, etc. are defined.

Seq

$\mathrm{Seq}(s)$ iff $s$ is a mapping and its domain is $[0,l)$ for some $l$.

def Seq [M ⊧ₘ* 𝐈𝚺₁] (s : M) : Prop := IsMapping s ∧ ∃ l, domain s = under l

• LO.Arith.Seq

Primitive Recursion

Let $f(\vec{v})$, $g(\vec{v},x,z)$ be a ${\Sigma }_1$-function. There is a ${\Sigma }_1$-function ${\mathsf{PR}}_{f,g}(\vec{v},u)$ such that:

$$\begin{array}{rl}{\mathsf{PR}}_{f,g}(\vec{v},0)& =f(\vec{v})\\ {\mathsf{PR}}_{f,g}(\vec{v},u+1)& =g(\vec{v},u,{\mathsf{PR}}_{f,g}(\vec{v},u))\end{array}$$

structure Formulae (k : ℕ) where
  zero : 𝚺₁-Semisentence (k + 1)
  succ : 𝚺₁-Semisentence (k + 3)

structure Construction {k : ℕ} (p : Formulae k) where
  zero : (Fin k → M) → M
  succ : (Fin k → M) → M → M → M
  zero_defined : DefinedFunction zero p.zero
  succ_defined : DefinedFunction (fun v ↦ succ (v ·.succ.succ) (v 1) (v 0)) p.succ

variable {k : ℕ} {p : Formulae k} (c : Construction M p) (v : Fin k → M)

def Construction.result (u : M) : M

theorem Construction.result_zero :
    c.result v 0 = c.zero v

theorem Construction.result_succ (u : M) :
    c.result v (u + 1) = c.succ v u (c.result v u)

• Formulae, Construction, Construction.result, Construction.result_zero, Construction.result_succ

Fixpoint

Let ${\Phi }_C(\vec{v},x)$ be a predicate, which takes a class $C$ as a parameter. Then there is a ${\Sigma }_1$-predicate ${\mathsf{Fix}}_{\Phi }(\vec{v},x)$ such that

$${\mathsf{Fix}}_{\Phi }(\vec{v},x)⟺{\Phi }_{\{z\mid {\mathsf{Fix}}_{\Phi }(\vec{v},z)\}}(\vec{v},x)$$

if $\Phi$ satisfies following conditions:

1. $\Phi$ is ${\Delta }_1$-definable if $C$ is a set. i.e., a predicate $(c,\vec{v},x)\mapsto {\Phi }_{\{z\mid \mathrm{Bit}(z,c)\}}(\vec{v},x)$ is ${\Delta }_1$-definable.
2. Monotone: $C\subseteq C^{\prime }$ and ${\Phi }_C(\vec{v},x)$ implies ${\Phi }_{C^{\prime }}(\vec{v},x)$.
3. Finite: ${\Phi }_C(\vec{v},x)$ implies the existence of a $m$ s.t. ${\Phi }_{\{z\in C\mid z<m\}}(\vec{v},x)$.

structure Blueprint (k : ℕ) where
  core : 𝚫₁-Semisentence (k + 2)

structure Construction (φ : Blueprint k) where
  Φ : (Fin k → M) → Set M → M → Prop
  defined : Arith.Defined (fun v ↦ Φ (v ·.succ.succ) {x | x ∈ v 1} (v 0)) φ.core
  monotone {C C' : Set M} (h : C ⊆ C') {v x} : Φ v C x → Φ v C' x

class Construction.Finite (c : Construction M φ) where
  finite {C : Set M} {v x} : c.Φ v C x → ∃ m, c.Φ v {y ∈ C | y < m} x

variable {k : ℕ} {φ : Blueprint k} (c : Construction M φ) [Finite c] (v : Fin k → M)

def Construction.Fixpoint (x : M) : Prop

theorem Construction.case :
    c.Fixpoint v x ↔ c.Φ v {z | c.Fixpoint v z} x

• Blueprint, Construction, Construction.Finite, Construction.Fixpoint, Construction.case

${\mathsf{Fix}}_{\Phi }(\vec{v},x)$ is ${\Delta }_1$ if $\Phi$ satisfies strong finiteness:

class Construction.StrongFinite (c : Construction M φ) where
  strong_finite {C : Set M} {v x} : c.Φ v C x → c.Φ v {y ∈ C | y < x} x

• StrongFinite

Also structural induction holds.

theorem Construction.induction [c.StrongFinite]
    {P : M → Prop} (hP : (Γ, 1)-Predicate P)
    (H : ∀ C : Set M, (∀ x ∈ C, c.Fixpoint v x ∧ P x) → ∀ x, c.Φ v C x → P x) :
    ∀ x, c.Fixpoint v x → P x

• LO.Arith.Fixpoint.Construction.induction

Gödel's First Incompleteness Theorem

A deduction system $\mathcal{S}$ is complete iff it can prove or refute every sentence $\sigma$. Otherwise, $\mathcal{S}$ is incomplete.

def System.Complete {F S} [System F S] [LogicalConnective F] (𝓢 : S) : Prop :=
    ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f

• System.Complete

Theorem

Let $T$ be a ${\Delta }_1$-definable arithmetic theory, stronger than ${\mathsf{R}}_0$ and ${\Sigma }_1$-sound.

Representeation Theorem

Theorem: Let $S$ be a r.e. set. Then, there exists a formula ${\phi }_S(x)$ such that $n\in S⟺T⊢{\phi }_S(\overline{n})$ for all $n\in \mathbb{N}$.

lemma re_complete
    [𝐑₀ ≼ T] [Sigma1Sound T]
    {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
    p x ↔ T ⊢! ↑((codeOfRePred p)/[‘↑x’] : Sentence ℒₒᵣ) 

• re_complete

Main Theorem

Theorem: ${\Sigma }_1$-sound and ${\Delta }_1$-definable first-order theory, which is stronger than ${\mathsf{R}}_0$, is incomplete.

• Proof.

  Define a set of formulae with one variable. $$D:=\{\phi \mid T⊢\neg \phi (┌\phi ┐)\}$$ $D$ is r.e. since $T$ is ${\Delta }_1$-definable. (one could use Craig's trick to weaken this condition to ${\Sigma }_1$, but I will not do that here.)

  By the representation theorem, there exists a ${\Sigma }_1$ formula $\rho (x)$ that represents $D$. i.e.,

  $$T⊢\rho (┌\phi ┐)⟺T⊢\neg \phi (┌\phi ┐)$$

  Let $\gamma :=\rho (┌\rho ┐)$. The next follows immediately.

  $$T⊢\gamma ⟺T⊢\neg \gamma$$

  Thus, as $T$ is consistent, $\gamma$ is undecidable from $T$. ∎

theorem goedel_first_incompleteness
  (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] :
  ¬System.Complete T

• goedel_first_incompleteness

Gödel's Second Incompleteness Theorem

Recall that inside $\mathsf{I}{\Sigma }_1$ we can do basic set theory and primitive recursion. Many inductive notions and functions on them are defined in ${\Delta }_1$ or ${\Sigma }_1$ using the fixpoint construction.

We work inside an arbitrary model $V$ of $\mathsf{I}{\Sigma }_1$.

Coding of Terms and Formulae

Term

Define $T_C$ as follows.

$$\begin{array}{rlrl}u\in T_C& ⟺& & (\exists z)[u=\widehat{\#z}]\vee \\ & & & (\exists x)[u=\widehat{\&x}]\vee \\ & & & (\exists k,f,v)[{\mathrm{Func}}_k(f)\wedge \mathrm{Seq}(v)\wedge k=\mathrm{lh}(v)\wedge (\forall i,z)[⟨i,z⟩\in v\to z\in C]\wedge u=\widehat{f^k(v)}]\end{array}$$

$\hat{\bullet }$ is a quasi-quotation. $$\begin{array}{rlrl}\text{bounded variable: }& & \widehat{\#z}& :=⟨0,z⟩+1\\ \text{free variable: }& & \widehat{\&x}& :=⟨1,x⟩+1\\ \text{function: }& & \widehat{f^k(v)}& :=⟨2,f,k,v⟩+1\end{array}$$

$T_C$ is ${\Delta }_1$ (if $C$ is a finite set) and monotone. Let $\mathrm{UTerm}(t)$ be a fixpoint 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)\wedge \mathrm{termBV}(t)\le n$.

Formula

Similarly, Define $F_C$:

$$\begin{array}{rlrl}u\in F_C& ⟺& & (\exists k,R,v)[{\mathrm{Rel}}_k(R)\wedge \text{v is a list of UTerm of length k}\wedge u=\widehat{R^k(v)}]\vee \\ & & & (\exists k,R,v)[{\mathrm{Rel}}_k(R)\wedge \text{v is a list of UTerm of length k}\wedge u=\widehat{\neg R^k(v)}]\vee \\ & & & [u=\hat{\top }]\vee \\ & & & [u=\hat{\perp }]\vee \\ & & & (\exists p\in C,q\in C)[u=\widehat{p\wedge q}]\vee \\ & & & (\exists p\in C,q\in C)[u=\widehat{p\vee q}]\vee \\ & & & (\exists p\in C)[u=\widehat{\forall p}]\vee \\ & & & (\exists p\in C)[u=\widehat{\exists p}]\end{array}$$

$$\begin{array}{rl}\widehat{R^k(v)}& :=⟨0,R,k,v⟩+1\\ \widehat{\neg R^k(v)}& :=⟨1,R,k,v⟩+1\\ \hat{\top }& :=⟨2,0⟩+1\\ \hat{\perp }& :=⟨3,0⟩+1\\ \widehat{p\wedge q}& :=⟨4,p,q⟩+1\\ \widehat{p\vee q}& :=⟨5,p,q⟩+1\\ \widehat{\forall p}& :=⟨6,p⟩+1\\ \widehat{\exists p}& :=⟨7,p⟩+1\end{array}$$

$F_C$ is ${\Delta }_1$ and monotone. Let $\mathrm{UFormula}(p)$ be a fixpoint of $F_C$ and define

$$\mathrm{Semiformula}(n,p)⟺\mathrm{UFormula}(p)\wedge \mathrm{bv}(p)\le 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.

Formalized Provability

Let $T$ be ${\Delta }_1$-definable theory. Define $D_C$:

$$\begin{array}{rlrl}d\in D_C& ⟺& & (\forall p\in \mathrm{sqt}(d))[\mathrm{Semiformula}(0,p)]\wedge \\ & & [& (\exists s,p)[d=\widehat{\text{AXL}(s,p)}\wedge p\in s\wedge \hat{\neg }p\in s]\vee \\ & & & (\exists s)[d=\widehat{\top \text{-INTRO}(s)}\wedge \hat{\top }\in s]\vee \\ & & & (\exists s,p,q)(\exists d_p,d_q\in C)[d=\widehat{\wedge \text{-INTRO}(s,p,q,d_p,d_q)}\wedge \widehat{p\wedge q}\in s\wedge \mathrm{sqt}(d_p)=s\cup \{p\}\wedge \mathrm{sqt}(d_q)=s\cup \{q\}]\vee \\ & & & (\exists s,p,q)(\exists d\in C)[d=\widehat{\vee \text{-INTRO}(s,p,q,d)}\wedge \widehat{p\vee q}\in s\wedge \mathrm{sqt}(d)=s\cup \{p,q\}]\vee \\ & & & (\exists s,p)(\exists d\in C)[d=\widehat{\forall \text{-INTRO}(s,p,d)}\wedge \widehat{\forall p}\in s\wedge \mathrm{sqt}(d)=s^{+}\cup \{p^{+}[\&0]\}]\vee \\ & & & (\exists s,p,t)(\exists d\in C)[d=\widehat{\exists \text{-INTRO}(s,p,t,d)}\wedge \widehat{\exists p}\in s\wedge \mathrm{sqt}(d)=s\cup \{p(t)\}]\vee \\ & & & (\exists s)(\exists d^{\prime }\in C)[d=\widehat{\mathrm{WK}(s,d^{\prime })}\wedge s\supseteq \mathrm{sqt}(d^{\prime })]\\ & & & (\exists s)(\exists d^{\prime }\in C)[d=\widehat{\mathrm{SHIFT}(s,d^{\prime })}\wedge s=\mathrm{sqt}(d^{\prime }{)}^{+}]\\ & & & (\exists s,p)(\exists d_1,d_2\in C)[d=\widehat{\mathrm{CUT}(s,p,d_1,d_2)}\wedge \mathrm{sqt}(d_1)=s\cup \{p\}\wedge \mathrm{sqt}(d_2)=s\cup \{\neg p\}]\\ & & & (\exists s,p)[d=\widehat{\mathrm{ROOT}(s,p)}\wedge p\in s\wedge p\in T]]\end{array}$$

$$\begin{array}{rl}\widehat{\text{AXL}(s,p)}& :=⟨s,0,p⟩+1\\ \widehat{\top \text{-INTRO}(s)}& :=⟨s,1,0⟩+1\\ \widehat{\wedge \text{-INTRO}(s,p,q,d_p,d_q)}& :=⟨s,2,p,q,d_p,d_q⟩+1\\ \widehat{\vee \text{-INTRO}(s,p,q,d)}& :=⟨s,3,p,q,d⟩+1\\ \widehat{\forall \text{-INTRO}(s,p,d)}& :=⟨s,4,p,d⟩+1\\ \widehat{\exists \text{-INTRO}(s,p,t,d)}& :=⟨s,5,p,t,d⟩+1\\ \widehat{\text{WK}(s,d)}& :=⟨s,6,d⟩+1\\ \widehat{\text{SHIFT}(s,d)}& :=⟨s,7,d⟩+1\\ \widehat{\text{CUT}(s,p,d_1,d_2)}& :=⟨s,8,p,d_1,d_2⟩+1\\ \widehat{\text{ROOT}(s,p)}& :=⟨s,9,p⟩+1\\ \mathrm{sqt}(d)& :={\pi }_1(d-1)\end{array}$$

$p^{+}$ is a shift of a formula $p$. $s^{+}$ is a image of shift of $s$. Take fixpoint ${\mathrm{Derivation}}_T(d)$.

$$\begin{array}{rl}{\mathrm{Derivable}}_T(\Gamma )& :=(\exists d)[{\mathrm{Derivation}}_T(d)\wedge \mathrm{sqt}(d)=\Gamma ]\\ {\mathrm{Bew}}_T(p)& :={\mathrm{Derivable}}_T(\{p\})\end{array}$$

Following holds for all formula (not coded one) $\phi$ and finite set $\Gamma$.

• Sound: $\mathbb{N}\models {\mathrm{Bew}}_T(┌\phi ┐)⟹T⊢\phi$

  lemma LO.Arith.Language.Theory.Provable.sound :
      (T.codeIn ℕ).Provable ⌜p⌝ → T ⊢! p 
  

  • LO.Arith.Language.Theory.Provable.sound
• D1: $T⊢\phi ⟹V\models {\mathrm{Bew}}_T(┌\phi ┐)$

  theorem LO.Arith.provable_of_provable :
      T ⊢! p → (T.codeIn V).Provable ⌜p⌝ 
  

  • LO.Arith.provable_of_provable
• D2: ${\mathrm{Bew}}_T(┌\phi \to \psi ┐)\&{\mathrm{Bew}}_T(┌\phi ┐)⟹{\mathrm{Bew}}_T(┌\psi ┐)$
• Formalized ${\Sigma }_1$-completeness: Let $\sigma$ be a ${\Sigma }_1$-sentence. $V\models \sigma ⟹V\models {\mathrm{Bew}}_{T+{\mathsf{R}}_0}(┌\sigma ┐)$

  theorem LO.Arith.sigma₁_complete (hσ : Hierarchy 𝚺 1 σ) :
      V ⊧ₘ₀ σ → T.Provableₐ (⌜σ⌝ : V)
  

  • LO.Arith.sigma₁_complete

Now assume that $U$ is a theory of arithmetic stronger than ${\mathsf{R}}_0$ and $T$ be a theory of arithmetic stronger than $\mathsf{I}{\Sigma }_1$. The following holds, thanks to the completeness theorem.

• $U⊢\sigma ⟺T⊢{\mathrm{Bew}}_U(┌\sigma ┐)$
  • LO.FirstOrder.Arith.provableₐ_complete
• $T⊢{\mathrm{Bew}}_U(┌\sigma \to \pi ┐)\to {\mathrm{Bew}}_U(┌\sigma ┐)\to {\mathrm{Bew}}_U(┌\pi ┐)$
  • LO.FirstOrder.Arith.provableₐ_D2
• $T⊢{\mathrm{Bew}}_U(┌\sigma ┐)\to {\mathrm{Bew}}_U(┌{\mathrm{Bew}}_U(┌\sigma ┐)┐)$
  • LO.FirstOrder.Arith.provableₐ_D3

Second Incompleteness Theorem

Assume that $T$ is ${\Delta }_1$-definable and stronger than $\mathsf{I}{\Sigma }_1$.

Fixpoint Lemma

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

$$\mathrm{ssnum}(y,┌\phi ┐,x)⟺y=┌\phi (\overline{x})┐$$

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

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

$$\begin{array}{rl}{\mathrm{fixpoint}}_{\theta }& :={\mathrm{diag}}_{\theta }(\overline{┌{\mathrm{diag}}_{\theta }┐})\\ {\mathrm{diag}}_{\theta }(x)& :=(\forall y)[\mathrm{ssnum}(y,x,x)\to \theta (y)]\end{array}$$

Lemma: $T⊢{\mathrm{fixpoint}}_{\theta }\leftrightarrow \theta (┌{\mathrm{fixpoint}}_{\theta }┐)$

• Proof. $$\begin{array}{rl}{\mathrm{fixpoint}}_{\theta }& \equiv (\forall x)[\mathrm{ssnum}(x,┌{\mathrm{diag}}_{\theta }┐,┌{\mathrm{diag}}_{\theta }┐)\to \theta (x)]\\ & \leftrightarrow \theta (┌{\mathrm{diag}}_{\theta }(\overline{┌{\mathrm{diag}}_{\theta }┐})┐)\\ & \equiv \theta (┌{\mathrm{fixpoint}}_{\theta }┐)\end{array}$$ ∎

theorem LO.FirstOrder.Arith.diagonal (θ : Semisentence ℒₒᵣ 1) :
    T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝]

• LO.FirstOrder.Arith.diagonal

Main Theorem

Define Gödel sentence ${\mathrm{G}}_T$: $${\mathrm{G}}_T:={\mathrm{fixpoint}}_{\neg {\mathrm{Bew}}_T(x)}$$

Lemma: Gödel sentence is undecidable, i.e., $T⊬\mathrm{G}$ if $T$ is consistent, and $T⊬\neg \mathrm{G}$ if $\mathbb{N}\models T$.

lemma goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗚

lemma not_goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    T ⊬ ∼↑𝗚

• goedel_unprovable
• not_goedel_unprovable

Define formalized incompleteness sentence ${\mathrm{Con}}_T$: $${\mathrm{Con}}_T:=\neg {\mathrm{Bew}}_T(┌\perp ┐)$$

Lemma: $T⊢{\mathrm{Con}}_T\leftrightarrow G_T$

lemma consistent_iff_goedel
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] :
    T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚

• consistent_iff_goedel

Theorem: $T$ cannot prove its own consistency, i.e., $T⊬{\mathrm{Con}}_T$ if $T$ is consistent. Moreover, ${\mathrm{Con}}_T$ is undecidable from $T$ if $\mathbb{N}\models T$.

theorem goedel_second_incompleteness
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗖𝗼𝗻 

theorem inconsistent_undecidable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    System.Undecidable T ↑𝗖𝗼𝗻

• goedel_second_incompleteness
• inconsistent_undecidable

Interpretation