appendix sectionsignatures

Nominal, HOL, and Dialectica theorem boundaries

Dependent nominal type theory

Signature.: Cheney’s LF extension with name-type constants, ordered fresh-name declarations, name-abstraction types, abstractions, and concretion at literal names. It has no name-case, fresh-name generator, or general recursor over abstractions.
Locally reconstructed.: Restriction determinacy, substitution restriction, the concretion case of general substitution, nominal beta–eta typing, the erased algorithmic-equality route, and the decisive adequacy cases.
Imported boundary.: Soundness and completeness of algorithmic equality, decidability of the displayed judgments, canonicalization, conservativity over LF, and adequacy are the exact results of the frozen calculus. No hereditary substitution, general nominal recursion, or normalization theorem for a richer language is claimed.

Signature.: Inhabited Church simple types with $bool$ , $ind$ , arrows, equality, and choice; the ten displayed primitive inference rules; eta, selection, and infinity axioms; and conservative constant and type definitions.
Locally proved.: Semantic substitution, soundness of every frozen rule and axiom in the nonempty set model, relative consistency, conservativity of the definition principles, and LCF confinement under theorem-type abstraction.
Comparison boundary.: Jacobs–Melham predicate encoding supplies the stated derivability translation only. It does not definitionally identify HOL propositions with proof types or transfer normalization, proof relevance, or canonicity.

Signature.: Simply typed lambda terms over natural numbers with a primitive recursor at every finite result type. The source theory is first-order Heyting arithmetic; the target is quantifier-free equational System $T$ with the induction needed for those matrices.
Locally reconstructed.: Tait reducibility for the frozen lambda presentation, strong normalization, numerical canonicity, every Dialectica matrix clause, the soundness induction’s logical and arithmetic cases, and the triangular-number witness calculation.
Exact theorem.: If $HA ⊢ A$ , closed System $T$ terms $\vec{t}$ can be extracted such that the target proves $A_{D} (\vec{t}, \vec{y})$ . This is the direct first-order theorem.
Not claimed.: Full extensional $E - {HA}^{ω}$ is not directly interpreted by this induction. Classical arithmetic needs a negative translation; countable choice and classical analysis require the separately developed bar-recursive extension.