Intensional models for the theory of types

DOI10.2178/JSL/1174668386MaRDI QIDQ3426565zbMATH OpenOpenAlexFDO

Authors Reinhard A. Muskens

Publication date 12 March 2007

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0608571

zbMATH Keywords

modal logicpossible worldscut-free sequent calculusmodel existence theoremfragment of Englishpropositional attitudeintensional models for classical theory of typesintensional type logicITL semantics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic of natural languages (03B65) Cut-elimination and normal-form theorems (03F05)

Abstract: 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.

Recommendations

• scientific article; zbMATH DE number 2070194
• Intensional logic in extensional language
• Intensional logic and two-sorted type theory
• scientific article; zbMATH DE number 3843727
• ON THE THEORY OF MODELS FOR INTUITIONISTIC LOGIC

Cited in

(27)

• Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
• Dialectica models of type theory
• Representing model theory in a type-theoretical logical framework
• Selectional restrictions, types and categories
• Cut-elimination for quantified conditional logic
• Closed structure
• Extensional higher-order paramodulation in Leo-III
• Modeling abstract types in modules with open existential types
• scientific article; zbMATH DE number 6680163 (Why is no real title available?)
• A Way of Making World Quantification Explicit
• An intensional type theory: Motivation and cut-elimination
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• Intensional logic and two-sorted type theory
• When are different type-logical semantic definitions defining equivalent meanings?
• Type interaction models and the rule of six
• Intensional logic in extensional language
• Extensional and Intensional Semantic Universes
• Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
• Intensional completeness in an extension of Gödel/Dummett logic
• scientific article; zbMATH DE number 2070194 (Why is no real title available?)
• Quantified multimodal logics in simple type theory
• Models of intuitionistic TT and NF
• A theory of necessities
• Type-theoretic logic with an operational account of intensionality
• CERES in higher-order logic
• Constructing possible worlds*
• A very modal model of a modern, major, general type system

This page was built for publication: Intensional models for the theory of types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3426565)