A formalization of Brouwer's argument for bar induction

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

Authors: Ryota Akiyoshi 

Publication date: 18 October 2018

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

Recommendations

• Bar induction and restricted classical logic
• Extended bar induction in applicative theories
• The bounded functional interpretation of bar induction
• A note on Bar Induction in Constructive Set Theory
• Gentzen's original consistency proof and the bar theorem
• Bar induction is compatible with constructive type theory
• Principles of bar induction and continuity on Baire space
• Well-ordering principles and bar induction
• Justifying induction on modal \(\mu\)-formulae
• scientific article; zbMATH DE number 1163362

zbMATH Keywords

infinitary proof theoryintuitionismBrouwer's bar induction

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

Cited In (3)

• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• Bar induction. The good, the bad, and the ugly
• Contingent objects and the Barcan formula

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)