Notes to Church’s Type Theory

1. They, e.g., do not entail the saturation and reflexivity properties given below.

2. The calculus in Kohlhase 1998 is technically still flawed; e.g., to guarantee soundness Skolemization must be used in rule \(\textit{SIM}(\textit{fun})\).

3. RUE stands for resolution by unification and equality.

4. Different to what is claimed, the presented rules fail to capture an exhaustive extensionality treatment, and so did their implementation in the prover HOT (Konrad 1998); see the respective comment on this in Benzmüller 1997; there are also some soundness issues.

Copyright © 2024 by
Christoph Benzmüller <>
Peter Andrews

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free