Classical predicative logic-enriched type theories

DOI10.1016/J.APAL.2010.04.005zbMATH Open1231.03008arXiv0906.1726OpenAlexW2048875543MaRDI QIDQ636367FDOQ636367

Robin Adams, Zhaohui Luo

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTTO and LTTO*, which we claim correspond closely to the classical predicative systems of second order arithmetic ACAO and ACA. We justify this claim by translating each second-order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. The two LTTs we construct are subsystems of the logic-enriched type theory LTTW, which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system ACAO has also been claimed to correspond to Weyl's foundation. By casting ACAO and ACA as LTTs, we are able to compare them with LTTW. It is a consequence of the work in this paper that LTTW is strictly stronger than ACAO. The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work.

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

Recommendations

• Applications of type theory
• scientific article
• Constructive natural deduction and its ‘ω-set’ interpretation
• On the strength of proof-irrelevant type theories
• Weyl's predicative classical mathematics as a logic-enriched type theory
• scientific article; zbMATH DE number 3894466
• On the syntax of Martin-Löf's type theories
• On specifications, subset types and interpretation of proposition in type theory
• Reflections on the categorical foundations of mathematics

zbMATH Keywords

type theorysecond-order arithmeticpredicativismHermann Weyl's programmelogic-enriched

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25)

Cites Work

• Title not available (Why is that?)
• Which set existence axioms are needed to prove the separable Hahn-Banach theorem?
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The model-theoretic ordinal analysis of theories of predicative strength
• Title not available (Why is that?)
• Weyl's predicative classical mathematics as a logic-enriched type theory
• Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• Title not available (Why is that?)
• Title not available (Why is that?)
• The generalised type-theoretic interpretation of constructive set theory
• A relative consistency proof

Cited In (10)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Weyl's predicative classical mathematics as a logic-enriched type theory
• Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• Title not available (Why is that?)
• Type logics and pregroups
• WEYL REEXAMINED: “DAS KONTINUUM” 100 YEARS LATER
• Automata, Languages and Programming

This page was built for publication: Classical predicative logic-enriched type theories

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