How to Prove Higher Order Theorems in First Order Logic

Abstract

In this paper we are interested in using a first order theorem prover to prove theorems that are formulated in some higher order logic. To this end we present translations of higher order logics into many sorted first order logic with equality and give a sufficient criterion for the soundness of these translations. In addition translations are introduced that are sound and complete with respect to L. Henkin’s general model semantics. Our higher order logics are based on a restricted type structure in the sense of A. Church, they have typed function symbols and predicate symbols, but no sorts. The translation results are finally generalized to handle such a logic with equality.