Theory Footprint_Checks
theory Footprint_Checks
imports Consistency
begin
section ‹Footprint of the consistency proof›
text ‹A footprint audit for the consistency result ‹nk_consistent›; nothing new is proved
here. The instances ‹consistency_bool_params› and ‹consistency_unit_params› instantiate
the parameter type ‹'p› (BKK's typed constants) --- not the individuals ‹ι›, which the
model makes a singleton --- with the finite types ‹bool› and ‹unit›; they would fail to
type-check if the proof required ‹'p :: infinite›, so no infinite supply of parameters is
needed.
The result is what the introduction calls an @{emph ‹outright›} consistency proof, relative
only to plain Isabelle/HOL: the meta-logic certifies the embedded object logic --- which
carries no axiom of infinity --- by a standard model with finite domains at every type,
using no set theory. The model construction uses no Hilbert choice: its description
operator selects by definite description (‹THE›, locale @{locale lambda_universe} in
theory ‹Semantics›). The soundness proof that the argument relies on uses Isabelle's
choice operator in one place, to name a canonical assignment (‹xi0› in theory
‹Semantics›).
The type \<^typ>‹ival› that hosts the model is infinite, as every recursive HOL datatype is.
For the object logic this does not matter: its quantifiers range over the domains
‹cD 1 σ› of the size-one instance ‹k = 1› of the model family of ‹Consistency›, and
each of these is a finite set. The domain of individuals has a single element:
@{lemma ‹en 1 ι = [VI 0]› by (simp add: upt_rec)}. The model therefore refutes every
axiom of infinity, which by definition has no finite models; concretely, a Dedekind-style
axiom demands an injective, non-surjective self-map of the individuals, and a one-element
domain has none. Nor can the model keep two individual constants apart. This is why the
consistency proof needs neither an infinite model nor a stronger meta-theory.
Finally, the kind of statement this is. The meta-logic Isabelle/HOL has an axiom of
infinity; the object logic has none. The meta-level infinity is needed only for the
syntax, and there only in the form of the natural numbers: the term type, the names of free
variables and the inductively defined set of derivations are infinite, as they must be in
any meta-theory that speaks about derivations. The argument itself is finitary ---
evaluation in a finite model is decidable, and soundness is an induction over derivations
--- and would go through in primitive recursive arithmetic, which needs no infinite object
at all (a metatheoretic remark, not formalised). Inside HOL there seems no lighter route:
the term type itself exists only by the axiom of infinity, and that axiom states exactly
that some type is Dedekind-infinite, which is all the natural numbers need. The datatype
\<^typ>‹ival› that hosts the model is infinite only because every HOL datatype is; its
domains are finite. So the consistency proof is carried out in a logic with an axiom of
infinity, about a logic without one; it is not a logic proving its own consistency.
G\"odel's second incompleteness theorem does not apply to the object logic: a theory with a
one-element model interprets no arithmetic. For many applications this is no restriction: where HOL
serves as a representation language, as in the LogiKEy embeddings of object logics
\<^cite>‹LogiKEy›, arithmetic at the object level is optional; the introduction's paragraph
on the two tiers of consistency says which core of the logic in use is the one certified
here.›
theorem : "¬ (⊢ (❙⊥ :: bool tm))"
by (rule nk_consistent)
theorem : "¬ (⊢ (❙⊥ :: unit tm))"
by (rule nk_consistent)
end