Names, HOL, and finite-type interpretation

Chapter 64: dependent nominal type theory

Contexts extend by variables or by fresh literal names. Restriction removes the selected name and every later variable, while retaining later fresh-name declarations: $$\frac{\phantom{X}}{\mathrm{\Gamma };\mathsf{fresh}a:\alpha \mathsf{restrict}a:\alpha \Rightarrow \mathrm{\Gamma }}\mathrm{R}-\mathrm{Here}$$ $$\frac{\mathrm{\Gamma }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}{\mathrm{\Gamma };\mathsf{fresh}b:\beta \mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime };\mathsf{fresh}b:\beta }\mathrm{R}-\mathrm{Name}$$ $$\frac{\mathrm{\Gamma }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}{\mathrm{\Gamma },x:A\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}\mathrm{R}-\mathrm{Var}.$$ The name type, fresh-name type former, and literal-name variable rule are

$\alpha :\mathsf{name}\in \mathrm{\Sigma }$

$\mathrm{\Gamma }⊢\alpha :\mathsf{type}$

$\alpha :\mathsf{name}\in \mathrm{\Sigma }$$\mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢B:\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{N}a:\alpha .B:\mathsf{type}$

$a:\alpha \in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢a:\alpha$

Name abstraction and concretion are $$\frac{\mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢M:B}{\mathrm{\Gamma }⊢⟨a:\alpha ⟩M:\mathsf{N}a:\alpha .B}\mathrm{Name}-\mathrm{Abs}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }\mathsf{restrict}b:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }\\ {\mathrm{\Gamma }}^{\prime }⊢M:\mathsf{N}a:\alpha .B\end{array}}{\mathrm{\Gamma }⊢M@b:B[b/a]}\mathrm{Concretion}.$$ Name substitutions retain the restriction premise:

$\mathrm{\Delta }\mathsf{restrict}b:\alpha \Rightarrow {\mathrm{\Delta }}^{\prime }$${\mathrm{\Delta }}^{\prime }⊢\theta :\mathrm{\Gamma }$

$\mathrm{\Delta }⊢(\theta ,b/a):\mathrm{\Gamma };\mathsf{fresh}a:\alpha$

Their definitional equations are name beta and fresh-name eta; the latter has the full form

$\mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢M@a=N@a:B$

$\mathrm{\Gamma }⊢M=N:\mathsf{N}a:\alpha .B$

Algorithmic equality erases $\mathrm{\Pi }$ to arrows and $\mathsf{N}$ to name-abstraction simple types. Its name-specific rules are

$a:\alpha \in \mathrm{\Delta }$

$\mathrm{\Delta }⊢a\leftrightarrow a:\alpha$

$\mathrm{\Delta }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Delta }}^{\prime }$${\mathrm{\Delta }}^{\prime }⊢M\leftrightarrow N:[\alpha ]\tau$

$\mathrm{\Delta }⊢M@a\leftrightarrow N@a:\tau$

$\mathrm{\Delta };\mathsf{fresh}a:\alpha ⊢M@a⟺N@a:\tau$

$\mathrm{\Delta }⊢M⟺N:[\alpha ]\tau$

Its completeness proof uses the chapter’s Kripke logical relation.

Chapter 65: classical simple type theory

The frozen HOL core has inhabited types generated by $\alpha ,\mathsf{bool},\mathsf{ind},\to$, simply typed lambda terms, polymorphic equality and choice. Its primitive theorem rules are

$⊢t=t$

$\mathrm{\Gamma }⊢s=t$$\mathrm{\Delta }⊢t=u$

$\mathrm{\Gamma }\cup \mathrm{\Delta }⊢s=u$

$\mathrm{\Gamma }⊢f=g$$\mathrm{\Delta }⊢x=y$

$\mathrm{\Gamma }\cup \mathrm{\Delta }⊢fx=gy$

$\mathrm{\Gamma }⊢s=t$$x\notin \mathrm{FV}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢(\lambda x.s)=(\lambda x.t)$

$⊢(\lambda x.t)x=t$

$\{p\}⊢p$

$\mathrm{\Gamma }⊢p=q$$\mathrm{\Delta }⊢p$

$\mathrm{\Gamma }\cup \mathrm{\Delta }⊢q$

$\mathrm{\Gamma }⊢p$$\mathrm{\Delta }⊢q$

$(\mathrm{\Gamma }\setminus \{q\})\cup (\mathrm{\Delta }\setminus \{p\})⊢p=q$

$\mathrm{\Gamma }⊢p$

$\theta \mathrm{\Gamma }⊢\theta p$

$\mathrm{\Gamma }⊢p$

$\rho \mathrm{\Gamma }⊢\rho p$

The selected closed axioms are eta, selection, and infinity. Classical connectives, quantifiers, functional extensionality, and propositional extensionality are derived at this signature; they are not extra unlisted kernel constructors.

Constant definition requires a fresh name, a closed right-hand side, and no right-hand-side type variable absent from the declared type. Type definition requires a theorem that the representing predicate is nonempty. Its abstraction and representation equations characterize precisely that nonempty subset.

Chapter 66: System T and Dialectica

System $T$ has finite types $\mathbb{N}$ and $\sigma \to \tau$, with $${\mathsf{R}}_{\sigma }:\sigma \to (\mathbb{N}\to \sigma \to \sigma )\to \mathbb{N}\to \sigma ,$$ $${\mathsf{R}}_{\sigma }ag0⟶a,{\mathsf{R}}_{\sigma }ag(\mathsf{S}n)⟶gn({\mathsf{R}}_{\sigma }agn).$$ For $A^{\mathsf{D}}=\mathrm{\exists }\overrightarrow{x}\mathrm{\forall }\overrightarrow{y}.A_{\mathsf{D}}$ and $B^{\mathsf{D}}=\mathrm{\exists }\overrightarrow{u}\mathrm{\forall }\overrightarrow{v}.B_{\mathsf{D}}$, the critical clause is $$(A\to B{)}^{\mathsf{D}}=\mathrm{\exists }U,Y\mathrm{\forall }\overrightarrow{x},\overrightarrow{v}.(A_{\mathsf{D}}(\overrightarrow{x},Y\overrightarrow{x}\overrightarrow{v})\to B_{\mathsf{D}}(U\overrightarrow{x},\overrightarrow{v})).$$ Conjunction concatenates witness and challenge tuples; a disjunction adds a numerical tag; universal quantification extracts a witness function; and existential quantification extracts the quantified object with its matrix witness.