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 © 2019 by
Christoph Benzmüller <>
Peter Andrews

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing this directive]