Set comprehension in Church's type theory.

摘要

Church's simple type theory allows quantification over sets and functions. This expressive power allows a natural formalization of much of mathematics. However, searching for set instantiations has not yet been well-understood. Here we study the role of set comprehension in higher-order automated theorem proving. In particular, we introduce formulations of Church's type theory which are restricted with respect to set comprehension. We then define corresponding semantics and show soundness and completeness. Using completeness, we show that some restrictions to set comprehension are complete. That is, we can prove any theorem with restricted set comprehension that could be proven with unrestricted set comprehension. We also show some restrictions are incomplete. This methodology is used to study set comprehension both in the presence and absence of extensionality.; We also describe methods for automated theorem proving in extensional type theory with restricted set instantiations. The approach to automated proof search presented here extends mating search by including connections up to extensional and equational reasoning. Search procedures based on these ideas have been implemented as part of the TPS theorem prover. The procedures have also been augmented by including the ability to solve for certain sets using set constraints. We describe the implementation and include experimental results.