Proofs in Higher-Order Logic

Expansion trees are defined as generalizations of Herbrand instances for formulas in a nonextensional form of higher-order logic based on Church\u27s simple theory of types. Such expansion trees can be defined with or without the use of skolem functions. These trees store substitution terms and either critical variables or skolem terms used to instantiate quantifiers in the original formula and those resulting from instantiations. An expansion tree is called an expansion tree proof (ET-proof) if it encodes a tautology, and, in the form not using skolem functions, an imbedding relation among the critical variables be acyclic. The relative completeness result for expansion tree proofs not using skolem functions, i.e. if A is provable in higher-order logic then A has such an expansion tree proof, is based on Andrews\u27 formulation of Takahasti\u27s proof of the cut-elimination theorem for higher-order logic. If the occurrences of skolem functions in instantiation terms are restricted appropriately, the use of skolem functions in place of critical variables is equivalent to the requirement that the imbedding relation is acyclic. This fact not only resolves the open question of what is a sound definition of skolemization in higher-order logic but also provides a direct, syntactic proof of its correctness. Since subtrees of expansion trees are also expansion trees (or their dual) and expansion trees store substitution terms and critical variables explicitly, ET-proofs can be directly converted into sequential and natural deduction proofs. A naive translation will often produce proofs which contain a lot of redunancies and will often use implicational lines in an awkward fashion. An improved translation process is presented. This process will produce only focused proofs in which much of the redunancy has been eliminated and backchaining on implicational lines was automatically selected if it was applicable. The information necessary to construct focused proofs is provided by a certain connection scheme, called a mating,of the boolean atoms within the tautology encoded by an ET-proof