A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Technical Summary: A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Problem and Context
The paper addresses the challenges of mechanizing type theory, specifically focusing on the meta-theoretical properties of Pure Type Systems (PTS). A central difficulty in formalizing substitution and $\beta$-reduction lies in handling variable renaming to prevent name capture. Traditional definitions (e.g., Curry-Feys) require well-founded induction on term length due to non-primitive recursive renaming steps, making mechanization difficult. Alternative approaches such as de Bruijn indices (dBI), locally nameless syntax, and Higher-Order Abstract Syntax (HOAS) offer solutions but introduce their own drawbacks: dBI is cumbersome for human readability; locally nameless syntax requires well-formedness predicates that "pollute" meta-theoretical results; and HOAS often prevents the generation of executable code or the formulation of decidability questions.

The authors aim to assess the feasibility of an approach that retains classical syntax (using named variables) while utilizing Stoughton's simultaneous substitutions. This method performs renaming of bound variables simultaneously with substitution via a single structural recursion, avoiding the need for well-founded induction on term length for most proofs.

Methodology
The development is fully machine-checked using Agda (v2.6.2.2) and the standard library. The methodology relies on the following core components:

1. Stoughton's Simultaneous Substitutions: Substitutions are defined as functions from variables to $\lambda$-terms ($Sub = V \to \Lambda$). The operation $M \bullet \sigma$ is defined by structural recursion. For $\lambda$-abstractions and $\Pi$-types, the bound variable is renamed to a fresh name $y$ chosen by a function $X$, and the substitution is updated to map the old bound variable to this new name. This ensures that only one recursive call is needed per abstraction, maintaining primitive recursiveness.
2. $\alpha$-Commutative Relations: The authors develop a theory of relations that commute with $\alpha$-conversion. A relation $S$ is $\alpha$-commutative if $M \sim_\alpha N$ and $N S P$ implies the existence of a $Q$ such that $M S Q$ and $Q \sim_\alpha P$. This framework allows the authors to treat confluence up to $\alpha$-conversion cleanly, avoiding the duplication of lemmas often seen in other formalizations.
3. Takahashi's Revision of the Confluence Proof: Instead of the original Tait and Martin-Löf proof, the paper employs Takahashi's revision using parallel reduction ($\Rightarrow$). The authors define parallel reduction without explicit $\alpha$-conversion rules in the reduction steps, relying instead on the pentagon property (a generalization of the diamond property up to $\alpha$-conversion) to prove confluence.
4. Normalization Assumption: The proof of consistency assumes that the specific PTS under consideration is normalizing (every well-typed term is weakly normalizing). The authors note that proving normalization for impredicative systems within Agda is likely impossible due to Agda's lack of impredicativity in the meta-language.

Key Contributions
The paper presents formal proofs for three major meta-theoretical properties:

1. Confluence of $\beta$-reduction: The authors prove the Church-Rosser theorem for the underlying syntax of PTS. By utilizing the theory of $\alpha$-commutative relations and Takahashi's parallel reduction, they establish that the star closure of parallel reduction coincides with many-step $\beta$-reduction and satisfies the pentagon property.
2. Subject Reduction (SR): The paper formalizes the preservation of typing under reduction. Following ideas from McKinna and Pollack, the authors extend reductions to contexts and prove a simultaneous theorem regarding the validity of contexts and the preservation of typing for subjects. This includes proving product injectivity, a crucial lemma for inversion.
3. Consistency for Impredicative PTS: The authors prove that for a specific subclass of impredicative PTS (those satisfying specific axioms and rules, such as $(\ast, \square) \in \mathcal{A}$ and $(\square, \ast, \ast) \in \mathcal{R}$), the type $\Pi[x : s]x$ (representing falsehood under Curry-Howard) is uninhabited in the empty context. The proof extends Coquand's pen-and-paper proof for the Calculus of Constructions (CC). It relies on the soundness and completeness of inductively defined normal and neutral forms, inversion lemmas, and the assumed normalization property.

Results and Evaluation

• Formalization Size: The entire development comprises approximately 4,300 lines of code (LoC), with 3,000 LoC attributed to the underlying framework of Stoughton's substitutions and PTS syntax from previous work.
• Comparison: The authors compare their work to formalizations using de Bruijn indices (Barras and Werner, ~2,900 LoC) and locally nameless syntax (Aydemir et al., ~4,800 LoC). They argue their approach is comparable in size but offers superior transparency regarding the syntax used, as it closely mirrors informal mathematical presentations (e.g., the weakening lemma looks nearly identical to the classical notation).
• Feasibility: The results suggest that the approach using classical syntax and simultaneous substitutions is feasible for dependent type theories. The authors note that only a couple of lemmas required well-founded induction, and the code size did not "explode."

Significance and Claims
The paper claims that the approach using Stoughton's substitutions offers a "clearer presentation and treatment" of meta-theoretical problems compared to similar developments, particularly regarding the handling of $\alpha$-conversion. The authors assert that their solution is more transparent to human readers than locally nameless or de Bruijn approaches, as it avoids the "notational clutter" of opening terms and managing fresh parameters manually.

The significance of the work lies in demonstrating that a machine-checked proof of consistency for impredicative systems is achievable without abandoning classical syntax, provided that normalization is assumed. The authors modestly acknowledge that a full mechanization of normalization for impredicative theories is likely impossible in Agda due to proof-theoretic strength limitations (Gödel's incompleteness theorem implications), but the consistency proof itself remains a substantial step toward correct-by-construction type-checking algorithms for such systems. The work serves as a validation of the framework's utility for future formalizations of dependent type theories.