Classical predicative logic-enriched type theories
From MaRDI portal
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.
Recommendations
- Applications of type theory
- scientific article; zbMATH DE number 65743
- 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
Cites work
- scientific article; zbMATH DE number 3825796 (Why is no real title available?)
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- scientific article; zbMATH DE number 1226875 (Why is no real title available?)
- scientific article; zbMATH DE number 1273299 (Why is no real title available?)
- scientific article; zbMATH DE number 2085163 (Why is no real title available?)
- scientific article; zbMATH DE number 1867338 (Why is no real title available?)
- scientific article; zbMATH DE number 226803 (Why is no real title available?)
- A relative consistency proof
- The generalised type-theoretic interpretation of constructive set theory
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- The model-theoretic ordinal analysis of theories of predicative strength
- Weyl's predicative classical mathematics as a logic-enriched type theory
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
- Which set existence axioms are needed to prove the separable Hahn-Banach theorem?
Cited in
(11)- A pluralist approach to the formalisation of mathematics
- Weyl's predicative classical mathematics as a logic-enriched type theory
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
- Type logics and pregroups
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
- scientific article; zbMATH DE number 1870414 (Why is no real title available?)
- scientific article; zbMATH DE number 5360215 (Why is no real title available?)
- Automata, Languages and Programming
- scientific article; zbMATH DE number 823591 (Why is no real title available?)
- scientific article; zbMATH DE number 1342281 (Why is no real title available?)
- Weyl reexamined: ``Das Kontinuum 100 years later
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)
