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)

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

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)