Andrews' type theory with undefinedness

zbMATH Open1226.03017arXiv1406.7492MaRDI QIDQ3086780FDOQ3086780

Authors: William M. Farmer 

Publication date: 30 March 2011

Abstract: ${calQ}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${calQ}_0$ does not admit undefined terms. The "traditional approach to undefinedness" in mathematical practice is to treat undefined terms as legitimate, nondenoting terms that can be components of meaningful statements. ${calQ}_0^{mu}$ is a modification of Andrews' type theory ${calQ}_0$ that directly formalizes the traditional approach to undefinedness. This paper presents ${calQ}_0^{mu}$ and proves that the proof system of ${calQ}_0^{mu}$ is sound and complete with respect to its semantics which is based on Henkin-style general models. The paper's development of ${calQ}_0^{mu}$ closely follows Andrews' development of ${calQ}_0$ to clearly delineate the differences between the two systems.

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

Recommendations

• A partial functions version of Church's simple theory of types
• Automated Reasoning
• Theory morphisms in Church's type theory with quotation and evaluation
• Fuzzy type theory with partial functions
• A simple type theory with partial functions and subtypes

zbMATH Keywords

undefinednessChurch's type theoryAndrews' type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (5)

• Automated Reasoning
• Incorporating quotation and evaluation into Church's type theory
• Theory morphisms in Church's type theory with quotation and evaluation
• Propositional type theory of indeterminacy
• Mathematics of Program Construction

This page was built for publication: Andrews' type theory with undefinedness

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