Intensional models for the theory of types

Journal of Symbolic Logic 72 (1):98-118 (2007)
Download Edit this record How to cite View on PhilPapers
In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up
(categorize this paper)
PhilPapers/Archive ID
Revision history
Archival date: 2018-08-27
View upload history
References found in this work BETA
General Semantics.Lewis, David K.
Handbook of Modal Logic.Blackburn, Patrick; van Benthem, Johan & Wolter, Frank (eds.)

View all 18 references / Add more references

Citations of this work BETA
Mechanizing Principia Logico-Metaphysica in Functional Type-Theory.Kirchner, Daniel; Benzmüller, Christoph & Zalta, Edward N.
Quantified Multimodal Logics in Simple Type Theory.Benzmüller, Christoph & Paulson, Lawrence C.

View all 10 citations / Add more citations

Added to PP index

Total views
98 ( #33,500 of 50,155 )

Recent downloads (6 months)
10 ( #41,049 of 50,155 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.