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

cut-free sequent calculusfragment of Englishintensional models for classical theory of typesintensional type logicITL semanticsmodal logicmodel existence theorempossible worldspropositional attitude

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

(29)

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

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)