Investigations into proof-search in a system of first-order dependent function types

Abstract

We present a series of proof systems for λII-calculus: a theory of first-order dependent function types. The systems are complete for the judgement of interest but differ substantially as bases for algorithmic proof-search. Each calculus in the series induces a search space that is properly contained within that of its predecessor. The λII-calculus is a candidate general logic in that it provides a metalanguage suitable for the encoding of logical systems and mathematics. Proof procedures formulated for the metalanguage extend to suitably encoded object logics, thus removing the need to develop procedures for each logic independently. This work is also an exploration of a systematic approach to the design of proof procedures. It is our contention that the task of designing a computationally efficient proof procedure for a given logic can be approached by formulating a series of calculi that possess specific proof-theoretic properties. These properties indicate that standard computational techniques such as unification are applicable, sometimes in novel ways. The study below is an application of this design method to an intuitionistic type theory.

Our methods exploit certain forms of subformula property and reduction ordering — a notion introduced by Bibel for classical logic, and extended by Wallen to various non-classical logics — to obtain a search calculus for which we are able to define notions of compatibility and intrinsic well-typing between a derivation ψ and a substitution σ calculated by unification which closes ψ (a derivation is closed when all of its leaves are axioms). Compatibility is an acyclicity test, a generalization of the occurs-check which, subject to intrinsic well-typing, determines whether the derivation ψ and substitution σ together constitute a proof.

Our work yields the (operational) foundations for a study of logic programming in this general setting. This potential is not explored here.