Intensional models for the theory of types

DOI10.2178/JSL/1174668386zbMATH Open1116.03008arXivmath/0608571OpenAlexW2030002668MaRDI QIDQ3426565FDOQ3426565

Authors: Reinhard A. Muskens 

Publication date: 12 March 2007

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

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.

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)

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
• Cut-elimination for quantified conditional logic
• Closed structure
• Modeling abstract types in modules with open existential types
• Extensional higher-order paramodulation in Leo-III
• Selectional restrictions, types and categories
• Title not available (Why is that?)
• A Way of Making World Quantification Explicit
• Title not available (Why is that?)
• An intensional type theory: Motivation and cut-elimination
• Intensional logic and two-sorted type theory
• Intensional logic in extensional language
• When are different type-logical semantic definitions defining equivalent meanings?
• Type interaction models and the rule of six
• 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
• Title not available (Why is that?)
• Models of intuitionistic TT and NF
• Quantified multimodal logics in simple type theory
• 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)