A formalization of Brouwer's argument for bar induction

DOI10.1007/978-3-662-57669-4_4OpenAlexW2810746708MaRDI QIDQ1799271

Ryota Akiyoshi

Publication date: 18 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-662-57669-4_4

zbMATH Keywords

infinitary proof theoryintuitionismBrouwer's bar induction

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

Related Items (1)

Contingent objects and the Barcan formula

Recommendations

• Title not available (Why is that?) 👍 👎
• The bounded functional interpretation of bar induction 👍 👎
• Extended bar induction in applicative theories 👍 👎
• Bar induction and restricted classical logic 👍 👎
• Justifying induction on modal  -formulae 👍 👎
• Principles of bar induction and continuity on Baire space 👍 👎
• Bar Induction is Compatible with Constructive Type Theory 👍 👎
• Gentzen’s Original Consistency Proof and the Bar Theorem 👍 👎
• Well-Ordering Principles and Bar Induction 👍 👎
• A note on Bar Induction in Constructive Set Theory 👍 👎

This page was built for publication: A formalization of Brouwer's argument for bar induction

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