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

Completeness in the Theory of Types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
A Formulation of the Simple Theory of Types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
A Theory of Propositional Types.Leon Henkin - 1963 - Fundamenta Mathematicae 52:323-334.

Add more references

Citations of this work BETA

The Seven Virtues of Simple Type Theory.William M. Farmer - 2008 - Journal of Applied Logic 6 (3):267-286.

Add more citations

Similar books and articles

A Partial Functions Version of Church's Simple Type Theory.W. A. Farmer - 1991 - Journal of Symbolic Logic 55 (1269-1291):127.
Partial Monotonic Protothetics.François Lepage - 2000 - Studia Logica 66 (1):147-163.
Partial Functions in Type Theory.François Lepage - 1992 - Notre Dame Journal of Formal Logic 33 (4):493-516.
On Almost Orthogonality in Simple Theories.Itay Ben-Yaacov & Frank O. Wagner - 2004 - Journal of Symbolic Logic 69 (2):398 - 408.
On a Hitherto Unexploited Extension of the Finitary Standpoint.Kurt Gödel - 1980 - Journal of Philosophical Logic 9 (2):133 - 142.
What is the Type-1/Type-2 Distinction?Nick Chater - 1997 - Behavioral and Brain Sciences 20 (1):68-69.


Added to PP index

Total views
18 ( #573,511 of 2,432,719 )

Recent downloads (6 months)
4 ( #170,020 of 2,432,719 )

How can I increase my downloads?


My notes