Classical Simple Type Theory and HOL

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Curry–Howard type theories identify a proposition with a type of its proofs. HOL does something deliberately different. It uses the simply typed lambda calculus as a language of mathematical objects, reserves one type for truth values, and puts proofs behind an abstract theorem interface. Classical reasoning, extensionality, and choice are principles of that logic; a theorem is not definitionally a program of its proposition, as it is in the propositions-as-types reading of chapter 2. The control-operator account of classical proofs in chapter 17 is another system, not an operational semantics for this HOL kernel.

This chapter fixes one HOL family member closely enough to prove things about it. The logical core is a compact Church-style presentation of the HOL rules documented by Gordon and in the HOL4 teaching packet [Gor85, Tue19]; slides 29–36 of the latter display the selected kernel. The definition principles and model follow the machine-checked account of Kumar, Arthan, Myreen, and Owens [KAMO14]. Historical LCF supplies the kernel architecture [Mil79]. Other HOL implementations make different small choices, so every theorem below is scoped to this frozen core.

The Church signature

Types and terms are $$\tau ,\sigma ::=\alpha \mid \mathsf{bool}\mid \mathsf{ind}\mid \tau \to \sigma ,t,u::=x_{\tau }\mid c_{\tau }\mid tu\mid \lambda x_{\tau }.t.$$ Type variables are schematic. The type operator $\to$ associates to the right, and application to the left. Every type is inhabited. A term of type $\mathsf{bool}$ is a formula; a sequent $\mathrm{\Gamma }⊢p$ has a finite set of Boolean assumptions and a Boolean conclusion.

The primitive logical constants are polymorphic equality and choice: $$(={)}_{\alpha }:\alpha \to \alpha \to \mathsf{bool},(@{)}_{\alpha }:(\alpha \to \mathsf{bool})\to \alpha .$$ Truth, connectives, and quantifiers are definitions. One convenient basis is Negation, disjunction, implication, and existential quantification can then be defined classically. These encodings are not intended as a pleasant surface syntax. They show that equality plus the lambda calculus is a complete logical basis.

The primitive inference rules are as follows. Substitutions in INST are capture-avoiding simultaneous term substitutions; those in INST-TYPE substitute types throughout a theorem. $$\frac{\phantom{X}}{⊢t=t}\mathrm{REFL}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢s=t\\ \mathrm{\Delta }⊢t=u\end{array}}{\mathrm{\Gamma }\cup \mathrm{\Delta }⊢s=u}\mathrm{TRANS}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢f=g\\ \mathrm{\Delta }⊢x=y\end{array}}{\mathrm{\Gamma }\cup \mathrm{\Delta }⊢fx=gy}\mathrm{COMB}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢s=t\\ x\notin \mathrm{FV}(\mathrm{\Gamma })\end{array}}{\mathrm{\Gamma }⊢(\lambda x.s)=(\lambda x.t)}\mathrm{ABS}\frac{\phantom{X}}{⊢(\lambda x.t)x=t}\mathrm{BETA}$$ General beta conversion at an argument $u$ is derived by first choosing the bound variable fresh and then applying INST. $$\frac{\phantom{X}}{\{p\}⊢p}\mathrm{ASSUME}\frac{\begin{array}{c}\mathrm{\Gamma }⊢p=q\\ \mathrm{\Delta }⊢p\end{array}}{\mathrm{\Gamma }\cup \mathrm{\Delta }⊢q}\mathrm{EQ}-\mathrm{MP}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢p\\ \mathrm{\Delta }⊢q\end{array}}{(\mathrm{\Gamma }\setminus \{q\})\cup (\mathrm{\Delta }\setminus \{p\})⊢p=q}\mathrm{DEDUCT}-\mathrm{ANTISYM}$$ $$\frac{\mathrm{\Gamma }⊢p}{\theta \mathrm{\Gamma }⊢\theta p}\mathrm{INST}$$ $$\frac{\mathrm{\Gamma }⊢p}{\rho \mathrm{\Gamma }⊢\rho p}\mathrm{INST}-\mathrm{TYPE}.$$ In DEDUCT-ANTISYM, the first premise is understood to use $q$ as a possible assumption and the second to use $p$. Writing the set differences in the conclusion makes assumption discharge explicit.

Three closed axioms complete the selected signature: $$\mathsf{ETA}:⊢(\lambda x.fx)=f(x\notin \mathrm{FV}(f)),$$ $$\mathsf{SELECT}:⊢Px\Rightarrow P(@P),$$ $$\mathsf{INFINITY}:⊢\mathrm{\exists }f:\mathsf{ind}\to \mathsf{ind}.\mathsf{inj}(f)\wedge \mathrm{\neg }\mathsf{surj}(f).$$ The last formula is one common infinity axiom; equivalent HOL presentations may instead postulate an injective non-surjective successor directly.

Which principles enter where?

The following ledger prevents several common conflations. Beta is a primitive inference rule, justified by function application. Eta is a closed axiom, valid because functions are extensional. Propositional extensionality and classical logic are derived theorems of the Boolean encoding, whose model interprets $\mathsf{bool}$ by exactly $\{0,1\}$. Choice is a closed axiom using $@$, interpreted by a choice function on every nonempty type. Infinity is a closed axiom, interpreted by choosing $\mathsf{ind}$ infinite. Equality is primitive at every type. Functional extensionality follows from $\eta$ and congruence. Propositional extensionality is stronger than merely having equality at $\mathsf{bool}$: the Boolean encoding proves that logically equivalent formulas denote the same Boolean. Classical excluded middle is a theorem of this logical basis, not a normalization consequence of the term calculus.

A set model

Fix a set-theoretic universe containing a two-element set and a countably infinite set. A valuation $\nu$ assigns every type variable a nonempty set. Interpret types by $$[[\mathsf{bool}{]]}_{\nu }=\{0,1\},[[\mathsf{ind}{]]}_{\nu }=\mathbb{N},[[\sigma \to \tau {]]}_{\nu }=[[\tau {]]}_{\nu }^{[[\sigma {]]}_{\nu }}.$$ Constants receive elements of their denoted sets. Application and abstraction are interpreted by application and set-theoretic function formation. Equality denotes the diagonal characteristic function.

Because every type denotes a nonempty set, fix a global choice operation ${\chi }_X:(X\to \{0,1\})\to X$ with $$(\mathrm{\exists }x\in X.P(x)=1)⟹P({\chi }_X(P))=1.$$ Interpret $(@{)}_{\tau }$ by ${\chi }_{[[\tau ]]}$. This is the semantic strength used by $\mathsf{SELECT}$; it is not smuggled into the lambda-calculus clauses. Interpret $\mathsf{ind}$ by $\mathbb{N}$, with successor witnessing $\mathsf{INFINITY}$.

Proof of Lemma 65.1 — Semantic substitution

Proof. Induct on $t$. Variables are the definition of ${\eta }_{\theta }$; constants are fixed by the interpretation. Application uses the two induction hypotheses. For abstraction, rename its binder fresh for $\theta$, apply the induction hypothesis to the body in an extended environment, and use extensional equality of set-theoretic functions. ◻

Write $(\nu ,\eta )\vDash \mathrm{\Gamma }$ when every member of $\mathrm{\Gamma }$ denotes $1$, and $\mathrm{\Gamma }{\vDash }_{\mathsf{all}}p$ when this implies $[[p{]]}_{\nu ,\eta }=1$ for every valuation and environment.

Proof of Theorem 65.2 — Kernel soundness

Proof. Induct on the theorem object. REFL, TRANS, and COMB are reflexivity, transitivity, and congruence of set equality. ABS uses function extensionality; its freshness condition keeps the assumption interpretations fixed. BETA is the semantic substitution lemma. For ASSUME, satisfaction of $\{p\}$ gives $[[p]]=1$. Rule EQ-MP replaces equal Boolean values. For DEDUCT-ANTISYM, inspect the four possible truth-value pairs for $p,q$: the premises exclude $(1,0)$ and $(0,1)$ under the undischarged assumptions, hence the values agree. The substitution rules use lemma 65.1. Finally $\mathsf{ETA}$ holds for functions, $\mathsf{SELECT}$ by $\chi$, and $\mathsf{INFINITY}$ in $\mathbb{N}$. ◻

Proof of Corollary 65.3

Proof. The model gives $[[\mathrm{\perp }]]=0$. Soundness would give value $1$ to any closed theorem. ◻

This is a relative consistency argument in the stated set theory. It neither proves that an arbitrary implementation is bug-free nor covers later oracle axioms. Kumar et al. prove a corresponding soundness and consistency theorem for their formal HOL semantics [KAMO14].

Definitions, new types, and quotients

A constant definition introduces fresh $c:\tau$ with equation $⊢c=t$, where $t:\tau$ is closed and contains no type variable absent from $\tau$. Its model interpretation is forced to be $[[t]]$, so it creates notation, not a new axiom about old constants.

A type definition starts with an old-type predicate $P:\sigma \to \mathsf{bool}$ and a theorem $⊢\mathrm{\exists }x.Px$. It introduces fresh $\alpha$, $\mathsf{abs}:\sigma \to \alpha$, and $\mathsf{rep}:\alpha \to \sigma$, with characteristic equations $$⊢\mathsf{abs}(\mathsf{rep}a)=a,⊢Pr⟺\mathsf{rep}(\mathsf{abs}r)=r.$$ Semantically, take $[[\alpha ]]=\{x\in [[\sigma ]]\mid P(x)=1\}$. Nonemptiness is exactly what HOL’s inhabited-type discipline needs. Let $\mathsf{rep}$ be inclusion and let $\mathsf{abs}$ map members to themselves and nonmembers to one fixed witness. The equations follow. Extending every old model in this way proves conservativity for formulas in the old signature.

For a concrete quotient, let $\mathsf{List}(A)$ be an already defined HOL type and put $$xs\approx ys⟺\mathrm{\forall }a:A.\mathsf{count}(a,xs)=\mathsf{count}(a,ys).$$ This is an equivalence relation, and concatenation respects it: $$xs\approx x{s}^{\prime }\wedge ys\approx y{s}^{\prime }⟹xs++ys\approx x{s}^{\prime }++y{s}^{\prime }.$$ A quotient package first constructs a nonempty representation of equivalence classes, then uses the type-definition principle to introduce $\mathsf{Bag}(A)$. Lift $[]$ and $(++)$ to $\varnothing$ and $\uplus$. The representative equations give $$B\uplus \varnothing =B,(A\uplus B)\uplus C=A\uplus (B\uplus C),A\uplus B=B\uplus A.$$ Only the last law is new relative to lists; its proof is pointwise commutativity of natural-number addition. The package automates respectfulness and lifting, but its theorems still pass through the same kernel.

The LCF trust boundary

An LCF implementation makes the host-language type $\mathsf{thm}$ abstract. Only kernel functions construct values of that type. A tactic has shape $$\mathsf{goal}⟶({\mathsf{goal}}_1,\dots ,{\mathsf{goal}}_n,{\mathsf{thm}}^n⟶\mathsf{thm}).$$ The validation function must rebuild the promised theorem from subtheorems. A buggy tactic can fail, loop, or choose a poor proof; absent an unsafe escape hatch, it cannot forge a $\mathsf{thm}$. This is the central LCF separation between a small trusted kernel and untrusted proof search.

For an exact tactic-to-kernel trace, consider the goal $$⊢(\lambda x.(\lambda y.y)y)=(\lambda x.y).$$ A derived abstraction tactic replaces it by the subgoal $⊢(\lambda y.y)y=y$ and stores a validation that calls ABS on the returned theorem. A beta tactic closes that subgoal by the primitive BETA constructor. Composing the validations yields the complete primitive trace $$\frac{{\displaystyle \frac{\phantom{X}}{⊢(\lambda y.y)y=y}}\mathrm{BETA}}{⊢(\lambda x.(\lambda y.y)y)=(\lambda x.y)}\mathrm{ABS}.$$ The empty assumption set discharges ABS’s freshness condition. The HOL4 course’s longer forward trace for $⊢\mathrm{\forall }p.p\Rightarrow p$ uses derived DISCH and GEN at the interface [Tue19]; replaying that trace in the frozen core must additionally expand the connective definitions and record all type and term instantiations.

Proof of Theorem 65.4 — LCF confinement

Proof. By representation independence, a tactic can obtain a theorem value only as an input or as the result of an exported constructor. Induction on the finite constructor trace reduces validity to theorem 65.2. ◻

The premise is operational, not ornamental. Unsafe casts, mutable corruption, or an oracle constructor enlarge the trusted base and require a new soundness argument.

Comparison with proof-relevant type theory

Under Curry–Howard, a judgment $p:P$ exposes a proof term whose type is the proposition. In HOL, $P:\mathsf{bool}$, while a kernel theorem asserting $⊢P$ lives at the implementation level. HOL proof objects may be recorded and replayed, but $\mathsf{bool}$ is not definitionally the host type $\mathsf{thm}$, and arbitrary inhabitants of a HOL type are not proofs.

Jacobs and Melham encode dependent types in HOL by predicates. A dependent type over $A$ becomes a predicate on an underlying HOL type; dependent functions carry closure obligations saying that admissible inputs are sent to admissible outputs. Their Theorem 4.8 gives a translation of derivable judgments of the selected dependent type theory into HOL [JM93]. The paper also says that a full formal metatheoretic treatment is future work. We therefore use its stated derivability translation as a comparison, not as a claim that HOL and dependent type theory are definitionally equivalent or that every HOL axiom has computational proof content.

Seminar and practical

Suggested first pass.

Begin with exercise 65.5; then replay exercise 65.7.

Exercise 65.5¶

★★☆ For each of $\beta$, $\eta$, choice, infinity, functional extensionality, and propositional extensionality, classify it as syntax, rule, axiom, derived theorem, or semantic construction. Defend every answer with one exact rule or model clause. (One page.)

Referenced from 4 locations

• Classical Simple Type Theory and HOL
• Solutions for Chapters 64–66

Exercise 65.6¶

★★☆ An implementation adds $\mathsf{oracle}:\mathsf{string}\to \mathsf{thm}$. Draw the new trust boundary. State the weakest specification of $\mathsf{oracle}$ that makes theorem 65.4 true again. (Ten lines and one diagram.)

Referenced from 3 locations

• Classical Simple Type Theory and HOL
• Solutions for Chapters 64–66

Exercise 65.7¶

★★★ Practical project.hol-kernel-trace-checker The companion artifact hol-kernel-trace-checker represents formulas by a small equality fragment and theorem values by replayable kernel traces. Add the missing side-condition check for ABS; then extend the valid equality-symmetry trace and one mutation that illegally abstracts over a free assumption. Record the Kappa commands and explain why rejection is a kernel property rather than a tactic property. (One page plus code.)

Referenced from 5 locations

• Classical Simple Type Theory and HOL
• Object calculus checker and evaluator
• ch:hol: theorem-constructor side conditions

Sources and theorem boundary

The kernel presentation and set-model picture are drawn from Gordon’s report, the HOL4 course packet, and the formal semantics of Kumar et al. [Gor85, Tue19, KAMO14]. The course’s slides 29–36 display the kernel and definition boundary; Kumar et al.’s Theorems 2–3 state soundness and consistency. The abstract theorem type and validation architecture originate in LCF [Mil79]. The predicate encoding is bounded by Jacobs and Melham’s stated translation theorem [JM93]. No claim here transfers normalization, proof relevance, or computational canonicity from a dependent type theory into classical HOL.