Annals of Pure and Applied Logic 64 (3):211-240 (1993)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of, an Interactive Mathematical Proof System developed at The MITRE Corporation.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(93)90144-3
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,827
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Partial Monotonic Protothetics.François Lepage - 2000 - Studia Logica 66 (1):147-163.
A Partial Functions Version of Church's Simple Type Theory.W. A. Farmer - 1991 - Journal of Symbolic Logic 55 (1269-1291):127.
Probabilistic Canonical Models for Partial Logics.François Lepage & Charles Morgan - 2003 - Notre Dame Journal of Formal Logic 44 (3):125-138.
Higher Order Modal Logic.Reinhard Muskens - 2006 - In Patrick Blackburn, Johan Van Benthem & Frank Wolter (eds.), Handbook of Modal Logic. Elsevier. pp. 621-653.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
On Almost Orthogonality in Simple Theories.Itay Ben-Yaacov & Frank O. Wagner - 2004 - Journal of Symbolic Logic 69 (2):398-408.


Added to PP index

Total views
11 ( #810,132 of 2,432,721 )

Recent downloads (6 months)
1 ( #464,418 of 2,432,721 )

How can I increase my downloads?


My notes