Formalising Gödel's incompleteness theorems, III: Coding and Bound Variables
[incompleteness nominal package Kurt Gödel Gödel’s proof uses arithmetic (or in our case, hereditarily finite sets) to encode logical syntax, rules of inference, and therefore theorems of the internal calculus. Analogous coding techniques are ubiquitous in computation theory, complexity theory and elsewhere in logic under the general heading of problem reduction: showing that something is impossible because it could otherwise be used to solve another problem already known to be impossible. A complication is that our calculus involves variable binding, with the attendant horrors of name clashes and renaming. As described in a previous post, the Isabelle/HOL formalisation of HF deals with variable binding through the nominal package, but when coding HF in itself we shall be forced to use a simpler technique, due to de Bruijn.
Overview of de Bruijn indices
Briefly, de Bruijn’s technique is to eliminate bound variable names altogether. Bound variables become nonnegative integers, where 0 refers to the innermost binder and greater integers refer to binders further out. It destroys readability, but that is no problem for coding. De Bruijn’s own exposition include remarks on the application of his technique to AUTOMATH, and today it is ubiquitous in proof assistants.
The definition of coding is via an intermediate representation of HF terms and formulas, which uses de Bruijn indices rather than nominal for variable binding. Even these definitions must be done using the nominal package, as they involve the type name. Proving the fidelity of the translation between the two representations is nontrivial.
Isabelle definitions terms and formulas, using de Bruijn indices
We begin with terms. Free variables are identified by their names, as before, while bound variables are identified by their de Bruijn index.
nominal_datatype dbtm = DBZero | DBVar name | DBInd nat | DBEats dbtm dbtm
The datatype for de Bruijn formulas is different only in the last constructor, because existential quantification no longer mentions a variable name.
nominal_datatype dbfm = DBMem dbtm dbtm | DBEq dbtm dbtm | DBDisj dbfm dbfm | DBNeg dbfm | DBEx dbfm
The translation from nominal terms to de Bruijn terms has at its heart the following function, which looks up a name in an environment of distinct names (representing the variable binding context), returning the appropriate index if the name is found.
fun lookup :: "name list ⇒ nat ⇒ name ⇒ dbtm" where "lookup [] n x = DBVar x" | "lookup (y # ys) n x = (if x = y then DBInd n else (lookup ys (Suc n) x))"
The translation itself is the obvious recursive traversal, calling the lookup function above.
The argument e is the environment in which variables are interpreted.
nominal_function trans_tm :: "name list ⇒ tm ⇒ dbtm" where "trans_tm e Zero = DBZero" | "trans_tm e (Var k) = lookup e 0 k" | "trans_tm e (Eats t u) = DBEats (trans_tm e t) (trans_tm e u)"
The translation of formulas involves a little trickery that I would rather gloss over
(Christian Urban did this, and only he properly understands it).
Note that the condition in the last line requires the quantified variable to be fresh with respect to the environment e, which it then extends in the recursive call for translating the body of the quantification.
nominal_function (invariant "λ(xs, _) y. atom ` set xs ♯* y") trans_fm :: "name list ⇒ fm ⇒ dbfm" where "trans_fm e (Mem t u) = DBMem (trans_tm e t) (trans_tm e u)" | "trans_fm e (Eq t u) = DBEq (trans_tm e t) (trans_tm e u)" | "trans_fm e (Disj A B) = DBDisj (trans_fm e A) (trans_fm e B)" | "trans_fm e (Neg A) = DBNeg (trans_fm e A)" | "atom k ♯ e ⟹ trans_fm e (Ex k A) = DBEx (trans_fm (k#e) A)"
These translations turn out to be injective. The proof is a simple induction on t followed by case analysis on u.
lemma trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) ⟷ t = u"
Translations of formulas are also injective, by a mostly similar proof. The existential case requires about 20 lines of reasoning, referring to nominal primitives, to show that the translation yields the same result regardless of whether or not the bound variables are identical.
lemma trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) ⟷ A = B"
Abstraction and substitution on de Bruijn formulas
Abstraction and substitution are key operations in the de Bruijn representation. Abstraction takes a name, an index number and a term, replacing every occurrence of the named variable by the given index. Here is the version for terms:
nominal_function abst_dbtm :: "name ⇒ nat ⇒ dbtm ⇒ dbtm" where "abst_dbtm name i DBZero = DBZero" | "abst_dbtm name i (DBVar name') = (if name = name' then DBInd i else DBVar name')" | "abst_dbtm name i (DBInd j) = DBInd j" | "abst_dbtm name i (DBEats t1 t2) = DBEats (abst_dbtm name i t1) (abst_dbtm name i t2)"
Substitution replaces a (necessarily free) occurrence of a named variable by a term. The term version looks almost the same as abstraction, but wait until we get to formulas.
nominal_function subst_dbtm :: "dbtm ⇒ name ⇒ dbtm ⇒ dbtm" where "subst_dbtm u x DBZero = DBZero" | "subst_dbtm u x (DBVar name) = (if x = name then u else DBVar name)" | "subst_dbtm u x (DBInd j) = DBInd j" | "subst_dbtm u x (DBEats t1 t2) = DBEats (subst_dbtm u x t1) (subst_dbtm u x t2)"
The following fact relates the translation of the term in an extended environment with translating the same term without the extension, then abstracting over an additional name. The proof is another trivial induction.
lemma trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)" by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append)
Abstraction over formulas satisfies the corresponding property. Its definition is the obvious structural recursion except for the last line, which increments the index. The point is that a quantifier binds a new variable.
nominal_function abst_dbfm :: "name ⇒ nat ⇒ dbfm ⇒ dbfm" where "abst_dbfm name i (DBMem t1 t2) = DBMem (abst_dbtm name i t1) (abst_dbtm name i t2)" | "abst_dbfm name i (DBEq t1 t2) = DBEq (abst_dbtm name i t1) (abst_dbtm name i t2)" | "abst_dbfm name i (DBDisj A1 A2) = DBDisj (abst_dbfm name i A1) (abst_dbfm name i A2)" | "abst_dbfm name i (DBNeg A) = DBNeg (abst_dbfm name i A)" | "abst_dbfm name i (DBEx A) = DBEx (abst_dbfm name (i+1) A)"
Substitution for free variables in a formula is different from abstraction, because the quantifier case is treated exactly like all the others.
nominal_function subst_dbfm :: "dbtm ⇒ name ⇒ dbfm ⇒ dbfm" where "subst_dbfm u x (DBMem t1 t2) = DBMem (subst_dbtm u x t1) (subst_dbtm u x t2)" | "subst_dbfm u x (DBEq t1 t2) = DBEq (subst_dbtm u x t1) (subst_dbtm u x t2)" | "subst_dbfm u x (DBDisj A1 A2) = DBDisj (subst_dbfm u x A1) (subst_dbfm u x A2)" | "subst_dbfm u x (DBNeg A) = DBNeg (subst_dbfm u x A)" | "subst_dbfm u x (DBEx A) = DBEx (subst_dbfm u x A)"
The term being substituted must be entirely without the DBInd constructor.
The time has come to talk about the concept of a de Bruijn term or formula being well-formed.
Well-formed de Bruijn terms and formulas
A de Bruijn index requires a matching binder, and we’ve a problem if it doesn’t exist. The notion of de Bruijn terms and formulas being well-formed is straightforward to formalise. As always, we begin with the terms:
inductive wf_dbtm :: "dbtm ⇒ bool" where Zero: "wf_dbtm DBZero" | Var: "wf_dbtm (DBVar name)" | Eats: "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ wf_dbtm (DBEats t1 t2)"
This may look strange, because the index constructor (DBInd) is simply prohibited.
But this is correct because terms have no binding construct.
The proof that every well formed de Bruijn term is equal to the translation of a nominal term is an elementary induction:
lemma wf_dbtm_imp_is_tm: assumes "wf_dbtm x" shows "∃t::tm. x = trans_tm [] t" using assms proof (induct rule: wf_dbtm.induct) case Zero thus ?case by (metis trans_tm.simps(1)) next case (Var i) thus ?case by (metis lookup.simps(1) trans_tm.simps(2)) next case (Eats dt1 dt2) thus ?case by (metis trans_tm.simps(3)) qed
The opposite direction, that the translation of a term is always well formed, is an even simpler induction:
lemma wf_dbtm_trans_tm: "wf_dbtm (trans_tm [] t)" by (induct t rule: tm.induct) auto
And so we can characterise the well-formed de Bruijn terms precisely as the translations of nominal terms.
theorem wf_dbtm_iff_is_tm: "wf_dbtm x ⟷ (∃t::tm. x = trans_tm [] t)" by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm)
A well formed de Bruijn formula is defined in terms of abstraction in the last line, which handles the existential quantifier. The abstraction operation is called with the name of the quantified variable, substituting a de Bruijn index of 0. The abstraction operation will increase this index as it passes through other quantifiers. A lot is going on, and yet the definition is simple.
inductive wf_dbfm :: "dbfm ⇒ bool" where Mem: "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ wf_dbfm (DBMem t1 t2)" | Eq: "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ wf_dbfm (DBEq t1 t2)" | Disj: "wf_dbfm A1 ⟹ wf_dbfm A2 ⟹ wf_dbfm (DBDisj A1 A2)" | Neg: "wf_dbfm A ⟹ wf_dbfm (DBNeg A)" | Ex: "wf_dbfm A ⟹ wf_dbfm (DBEx (abst_dbfm name 0 A))"
Application of similar techniques gives us a characterisation of well-formed de Bruijn formulas.
lemma wf_dbfm_iff_is_fm: "wf_dbfm x ⟷ (∃A::fm. x = trans_fm [] A)" by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm)
It’s impressive that two absolutely different treatments of variable binding turn out to be exactly equivalent, and with so little effort in the proofs. The formal specification of well-founded terms and formulas will be needed later in the incompleteness development.
A few commutativity properties
The development requires a great many facts relating substitution, abstraction, freshness and the translations between the nominal and de Bruijn levels. Here are just a couple. Thankfully, most of these are easy to prove.
If you have a formula and two distinct names, one of which is fresh for the term u, then substitution and abstraction actually commute.
And the proof is a single line!
lemma dbfm_abst_swap_subst: "name ≠ name' ⟹ atom name' ♯ u ⟹ subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)" by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst)
Here, substitution on de Bruijn terms corresponds to substitution on the original nominal terms. The same property holds for formulas. The proof is again easy.
lemma subst_trans_commute [simp]: "atom i ♯ e ⟹ subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)" apply (induct t rule: tm.induct) apply (auto simp: lookup_notin fresh_imp_notin_env) apply (metis abst_dbtm_fresh_ignore dbtm_subst_ignore lookup_fresh lookup_notin subst_dbtm.simps(2)) done
I imagine that readers have had enough of Gödel for the moment, so I shall have to think of something else for next week!