Andrews' type theory with undefinedness

MaRDI QIDQ3086780zbMATHFDO

Authors William M. Farmer

Publication date 30 March 2011

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

zbMATH Keywords

undefinednessChurch's type theoryAndrews' type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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.

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

Cited in

(5)

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

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)