A formalization of Brouwer's argument for bar induction

DOI10.1007/978-3-662-57669-4_4MaRDI QIDQ1799271zbMATH OpenOpenAlexFDO

Authors 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)

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

Cited in

(3)

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

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)