Safe Proof Checking in Type Theory with Y

Abstract

We present an extension of type theory with a fixed point combinator Y .We are particularly interested in using this Y for doing unbounded proof search in the proof system. Therefore we treat in some detail a typed λ-calculus for higher order predicate logic with inductive types (a reasonable subsystem of the theory implemented in [Dowek e.a. 1991]) and show how bounded proof search can be done in this system, and how unbounded proof search can be done if we add Y . Of course, proof search can also be implemented (as a tactic) in the meta language. This may give faster results, but asks from the user to be able to program the implementation. In our approach the user works completely in the proof system itself. We also provide the meta theory of type theory with Y that allows to use the fixed point combinator in a safe way. Most importantly, we prove a kind of conservativity result, showing that, if we can generate a proof term M of formula ϕ in the extended system, and M does not contain Y , then M is already a proof of ϕ in the original system.