Formalising Gödel's incompleteness theorems, II: Σ-formulas
[Isar incompleteness nominal package Kurt Gödel Gödel’s theorem, more than other deep results, is burdened with numerous tiresome definitions and lemmas. It’s necessary to codify in full the axioms and inference rules of HF, the internal logic, as well as a toolbox of derived syntactic primitives needed for expressing and proving HF statements. (It’s also necessary to prove that the primitives actually work, a particularly tiresome step that most authors omit.) Here, let’s look at something a bit more interesting: Świerczkowski’s Theorem 2.5, which states that every true Σ-sentence is a theorem. This turns out to be vital once we set up Gödel encodings of formulas and define a provability predicate, Pf. It will be possible to show that φ is a theorem if and only if Pf⌜φ⌝ is true, for any HF formula φ. The point is that all of these syntactic predicates can be defined as Σ-formulas. Therefore, if Pf⌜φ⌝ is true, we get—for free—that Pf⌜φ⌝ is formally provable. To get started, we first need to define Σ-formulas.
Σ-formulas and the main result, informally
Świerczkowski defines the strict Σ-formulas syntactically:
- all formulas of the form $x\in y$, where $x$ and $y$ are variables
- all formulas of the form $\phi\land\psi$ and $\phi\lor\psi$, where $\phi$ and $\psi$ are strict Σ-formulas
- all formulas of the form $\forall x\in y.\, \phi$, where $\phi$ is a strict Σ-formula and $y$ is a variable
- all formulas of the form $\exists x.\, \phi$, where $\phi$ is a strict Σ-formula
Now a Σ-formula is any formula provably equivalent in HF to a strict Σ-formula. With a little work, it’s possible to show that all atomic formulas are Σ-formulas, including those of the form $t=u$ and $t\subseteq u$. In particular, the syntactic requirements for variables in (1) and (3) above can be relaxed to any terms.
Intuitively, such formulas are positive. Negation isn’t available and universal quantifiers must be bounded. However, existential quantifiers can be unbounded. This class of formulas is expressive enough to simulate recursion and thereby specify the syntactic structure of well-formed terms, formulas and proofs.
The proof of the main theorem is then by induction on the structure of a (generalised) Σ-sentence.
- Atomic formulas can essentially be evaluated in the logic, because they have no variables.
- If $\phi\lor\psi$ is true then either $\phi$ or $\psi$ must be true, and by the induction hypothesis, provable in HF. Therefore, $\phi\lor\psi$ itself is provable. Similarly for $\phi\land\psi$.
- If $\forall x\in t.\, \phi$ is true then the term $t$ denotes a specific HF set and we are dealing with a conjunction.
- If $\exists x.\, \phi(x)$ is true then $\phi(t)$ is a true Σ-sentence and therefore a theorem by the induction hypothesis. Using the value of $t$ as a witness, the conclusion follows.
Dead simple really. Let’s formalise it.
Formalising the set of Σ-formulas
The strict Σ-formulas are defined as follows.
This definition references the formal definition of HF from the previous post,
as well as some derived syntactic constructions (AND and All2) that I have left to the imagination. Occurrences of the Var constructor agree with the original text, which permitted variables only.
inductive ss_fm :: "fm ⇒ bool" where MemI: "ss_fm (Var i IN Var j)" | DisjI: "ss_fm A ⟹ ss_fm B ⟹ ss_fm (A OR B)" | ConjI: "ss_fm A ⟹ ss_fm B ⟹ ss_fm (A AND B)" | ExI: "ss_fm A ⟹ ss_fm (Ex i A)" | All2I: "ss_fm A ⟹ atom j ♯ (i,A) ⟹ ss_fm (All2 i (Var j) A)
The definition of a Σ-formula echoes Świerczkowski’s except for a technical condition involving the function supp (meaning “support”). The support of an entity is, roughly speaking, its set of free variables. So formally, a Σ-formula is anything provably equivalent to a strict Σ-formula containing no additional free variables.
definition Sigma_fm :: "fm ⇒ bool" where "Sigma_fm A ⟷ (∃B. ss_fm B ∧ supp B ⊆ supp A ∧ {} ⊢ A IFF B)"
It is straightforward to show that the Σ-formulas are closed according to the same rules as the strict Σ-formulas, and moreover Fls (the falsity symbol, $\bot$) is also a Σ-formula (being provably equivalent to $\exists x.\, x\in x$).
All atomic formulas are Σ-formulas
Our next task is to demonstrate that all atomic formulas are Σ-formulas. This involves a series of fairly elementary proofs, relating various atomic formulas to strict Σ-formulas. We begin with the terms restricted to variables and gradually strengthen the results to other terms. The subset relation, applied to variables, is a Σ-formula simply by its syntactic structure: $x\subseteq y \leftrightarrow (\forall j\in x.\, j\in y)$. The following is a representative example, where $x\subseteq 0 \longleftrightarrow(\forall j\in x.\, \bot)$ is proved in the HF calculus. Another theorem handles the case $x\subseteq y\lhd z$, and on we go, step by tedious step.
lemma Subset_Zero_sf: "Sigma_fm (Var i SUBS Zero)" proof - obtain j::name where j: "atom j ♯ i" by (rule obtain_fresh) hence Subset_Zero_Iff: "{} ⊢ Var i SUBS Zero IFF (All2 j (Var i) Fls)" by (auto intro!: Subset_I [of j] intro: Eq_Zero_D Subset_Zero_D All2_E [THEN rotate2]) thus ?thesis using j by (auto simp: supp_conv_fresh intro!: Sigma_fm_Iff [OF Subset_Zero_Iff] Sigma_fm_All2_Var) qed
Perhaps surprising is that every HF theorem is automatically a Σ-formula. That simply because every theorem is provably equivalent to $\exists x.\, \exists y.\, x\in y$, which is a valid Σ-formula. The Isabelle proof isn’t especially clear and is shown simply to give an impression of what’s involved in proving theorems in the HF calculus. The Isabelle proof begins by grabbing a pair of fresh variable names, then does the HF proof, giving as existential witnesses $0$ and $0\lhd 0$.
lemma theorem_sf: assumes "{} ⊢ A" shows "Sigma_fm A" proof - obtain i::name and j::name where ij: "atom i ♯ (j,A)" "atom j ♯ A" by (metis obtain_fresh) show ?thesis apply (rule Sigma_fm_Iff [where A = "Ex i (Ex j (Var i IN Var j))"]) using ij apply auto apply (rule Ex_I [where x=Zero], simp) apply (rule Ex_I [where x="Eats Zero"]) apply (auto intro: Mem_Eats_I2 assms thin0) done qed
Once we have assembled a collection of results for atomic formulas with all the different combinations of term constructors, we can prove a key lemma: that all atomic formulas, with arbitrarily large terms, are Σ-formulas. The 50 line proof is by complete induction on the combined sizes of the terms.
lemma Subset_Mem_sf_lemma: "size t + size u < n ⟹ Sigma_fm (t SUBS u) ∧ Sigma_fm (t IN u)"
As a trivial corollary, equality is also a Σ-formula:
lemma Equality_sf: "Sigma_fm (t EQ u)" by (auto intro: Sigma_fm_Iff [OF Extensionality] simp: supp_conv_fresh)
Some results connecting quantification and ground terms
Bounded universal quantifiers will be interpreted as finite conjunctions, while existentially quantified formulas will be proved by exhibiting a specific witness. For both of these, we need to reason about the terms that denote sets.
Every hereditary finite set $x$ is the denotation of some HF term, $t$, and that term is ground (i.e., variable free):
lemma obtain_const_tm: obtains t where "⟦t⟧e = x" "ground t" proof (induct x rule: hf_induct) case 0 thus ?case by (metis ground_aux_simps(1) eval_tm.simps(1)) next case (hinsert y x) thus ?case by (metis ground_aux_simps(3) eval_tm.simps(3)) qed
An existential HF formula evaluates to true if and only if there exists a specific ground term, $t$, which yields a true formula if it is substituted for the quantified variable:
lemma ex_eval_fm_iff_exists_tm: "eval_fm e (Ex k A) ⟷ (∃t. eval_fm e (A(k::=t)) ∧ ground t)" by (auto simp: eval_subst_fm) (metis obtain_const_tm)
The following function returns the elements of any HF set. Note that both the set and its elements take the form of HF terms.
nominal_function elts :: "tm ⇒ tm set" where "elts Zero = {}" | "elts (Var k) = {}" | "elts (Eats t u) = insert u (elts t)"
if $t$ is a ground term, and $A(u)$ is an HF theorem for each $u\in t$, then the formula $\forall x\in t.\,A(x)$ is also an HF theorem. The proof, given in full below, is by induction on HF terms. The only nontrivial case is for Eats terms, $t\lhd u$ when the induction hypothesis gives us $A(u)$ and $\forall x\in t.\,A(x)$ as HF theorems.
The inductive step, $\forall x\in t\lhd u.\,A(x)$,
follows by a couple of applications of low-level HF inference rules.
lemma prove_elts_imp_prove_All2: "ground t ⟹ (⋀u. u ∈ elts t ⟹ {} ⊢ A(i::=u)) ⟹ {} ⊢ All2 i t A" proof (induct t rule: tm.induct) case (Eats t u) hence pt: "{} ⊢ All2 i t A" and pu: "{} ⊢ A(i::=u)" by auto have "{} ⊢ ((Var i IN t) IMP A)(i ::= Var i)" by (rule All_D [OF pt]) hence "{} ⊢ ((Var i IN t) IMP A)" by simp thus ?case using pu by (auto intro: anti_deduction) (metis Iff_MP_same Var_Eq_subst_Iff thin1) qed auto
Every true Σ-sentence is a theorem
We finally have all the ingredients for the main theorem in this post.
The previous definition of a Σ-formula did not allow nontrivial terms, only variables. With a little effort, some of it shown above, we can lift the restriction and allow arbitrary terms in atomic formulas and as the bounds of universal quantifiers. The following definition (of the so-called Σ-eats-formulas) codifies this more general class:
inductive se_fm :: "fm ⇒ bool" where MemI: "se_fm (t IN u)" | DisjI: "se_fm A ⟹ se_fm B ⟹ se_fm (A OR B)" | ConjI: "se_fm A ⟹ se_fm B ⟹ se_fm (A AND B)" | ExI: "se_fm A ⟹ se_fm (Ex i A)" | All2I: "se_fm A ⟹ atom i ♯ t ⟹ se_fm (All2 i t A)"
For illustration, here’s one of the many facts proved about this definition. The class of Σ-eats-formulas is closed under substitutions for variables. The proof is a trivial induction.
lemma subst_fm_in_se_fm: "se_fm A ⟹ se_fm (A(k::=x))" by (nominal_induct avoiding: k x rule: se_fm.strong_induct) (auto)
Here is our main theorem for the case of atomic formulas. It can be seen as a mutual induction, which turns out to be a key feature of HF reasoning: the cases for the subset and membership relation are treated simultaneously, each used in the proof of the other. The proof is by the complete induction on the size of the ground formula (or rather its arguments, $t$ and $u$).
First, we prove that if $t\subseteq u$ evaluates to true then that formula is an HF theorem, by case analysis on the term $t$, because if it equals 0 then the result is trivial and if it has the form $x\lhd y$ then the induction hypothesis can be used. Second, the induction hypothesis is rephrased in terms of set equality, and then the claim for formulas of the form $t\in u$ is proved by case analysis on $u$.
lemma ground_prove: "⟦size t + size u < n; ground t; ground u⟧ ⟹ (⟦t⟧e ≤ ⟦u⟧e ⟶ {} ⊢ t SUBS u) ∧ (⟦t⟧e ❙∈ ⟦u⟧e ⟶ {} ⊢ t IN u)" proof (induction n arbitrary: t u rule: less_induct) case (less n t u) show ?case proof show "⟦t⟧e ≤ ⟦u⟧e ⟶ {} ⊢ t SUBS u" using less by (cases t rule: tm.exhaust) auto next { fix y t u have "⟦y < n; size t + size u < y; ground t; ground u; ⟦t⟧e = ⟦u⟧e⟧ ⟹ {} ⊢ t EQ u" by (metis Equality_I less.IH add.commute order_refl) } thus "⟦t⟧e ❙∈ ⟦u⟧e ⟶ {} ⊢ t IN u" using less.prems by (cases u rule: tm.exhaust) (auto simp: Mem_Eats_I1 Mem_Eats_I2 less.IH) qed qed
The main result is by complete induction on the size of the formula $\alpha$ (and apologies for calling it $\alpha$; I was following Świerczkowski).
The base case, $t\in u$, follows immediately by the previous result.
The cases for $\lor$ and $\land$ are trivial despite requiring reasoning in the HF calculus.
The existential case finds the required witness using the lemma ex_eval_fm_iff_exists_tm, which was proved above.
The universal case is slightly more difficult, but uses two lemmas proved above: subst_fm_in_se_fm and prove_elts_imp_prove_All2.
lemma ground_se_fm_induction: "ground_fm α ⟹ size α < n ⟹ se_fm α ⟹ eval_fm e α ⟹ {} ⊢ α" proof (induction n arbitrary: α rule: less_induct) case (less n α) show ?case using ‹se_fm α› proof (cases rule: se_fm.cases) case (MemI t u) thus "{} ⊢ α" using less by (auto intro: ground_prove_IN) next case (DisjI A B) thus "{} ⊢ α" using less by (auto intro: Disj_I1 Disj_I2) next case (ConjI A B) thus "{} ⊢ α" using less by auto next case (ExI A i) thus "{} ⊢ α" using less.prems apply (auto simp: ex_eval_fm_iff_exists_tm simp del: better_ex_eval_fm) apply (auto intro!: Ex_I less.IH subst_fm_in_se_fm ground_subst_fm) done next case (All2I A i t) hence t: "ground t" using less.prems by (auto simp: ground_aux_def fresh_def) hence "(∀u∈elts t. eval_fm e (A(i::=u)))" by (metis All2I(1) t eval_fm_All2_Iff_elts less(5)) thus "{} ⊢ α" using less.prems All2I t apply (auto del: Neg_I intro!: prove_elts_imp_prove_All2 less.IH) apply (auto intro: subst_fm_in_se_fm ground_subst_fm elts_imp_ground) done qed qed
The main theorem simply repackages the inductive proposition above. Every Σ-sentence (ground formula) that evaluates to true in the standard HF model is a formal HF theorem.
theorem Sigma_fm_imp_thm: "⟦Sigma_fm A; ground_fm A; eval_fm e0 A⟧ ⟹ {} ⊢ A" by (metis Iff_MP2_same ss_imp_se_fm empty_iff Sigma_fm_def eval_fm_Iff ground_fm_aux_def hfthm_sound se_fm_imp_thm subset_empty)
These proofs are remarkably simple. And the final theorem is worth the effort: it is invoked 10 times in the formal incompleteness development. That’s 10 occasions when the alternative would be tedious strings of HF steps, each of them hundreds of lines long and absolutely opaque.