---
title: "How to Prove Higher Order Theorems in First Order Logic"
authors:
  - "Manfred Kerber"
doi: ""
url: "https://ijcai.org/proceedings/1991/21"
pdf: "https://ijcai.org/proceedings/1991/0021.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "137-141"
track: "Automated Reasoning"
keywords:
---

# How to Prove Higher Order Theorems in First Order Logic

Manfred Kerber

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 137-141.

## 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 first order logic with fiat sorts and 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.