A new consistency proof for intuitionistic inductive definitions using the lexicographic path ordering

Jeffrey Sarnat

Programming languages researchers routinely encounter problems that reduce to proving the consistency of a logic (e.g. the normalization of typed lambda-calculi, the decidability of equality in type theory, etc.). Although the principle of transfinite induction is routinely employed by logicians in proving consistency, its use among programming languages researchers lags considerably behind alternatives such as logical relations and model theory. Perhaps the most famous use of transfinite induction is in Gentzen's proof of the consistency of classical arithmetic, where he justifies the termination of a cut-elimination procedure by a complex assignment of ordinals to proof trees.

In this talk, we demonstrate the consistency of a formulation of Heyting arithmetic based on Martin-Lof's Intuitionistic Theory of Iterated Inductive Definitions. The proof relies on a novel cut-elimination procedure whose termination is justified by the lexicographic path ordering defined (almost) directly on the proof trees themselves. The same technique can be used on a similar logic, whose consistency can be shown, via a structural logical relation, to entail weak normalization for Godel's T. Both proofs have been formalized in a conservative extension to Twelf (whose proof-theoretic strength would otherwise be inadequate). Because the lexicographic path ordering is both well understood by computer scientists and easy to implement, we consider it a viable, off-the-shelf alternative to conventional transfinite induction that is ready for use in formal settings beyond term rewriting, where its considerable proof theoretic strength cannot be fully exploited.