Lindenbaum algebras of intuitionistic theories and free categories

DOI10.1016/0168-0072(87)90061-3zbMath0624.03045OpenAlexW2091067796MaRDI QIDQ1092043

Harvey M. Friedman, Peter J. Freyd, Andrej Scedrov

Publication date: 1987

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

Full work available at URL: https://doi.org/10.1016/0168-0072(87)90061-3

zbMATH Keywords

Heyting arithmetictopoicomprehensionexcluded middlefree Heyting algebrasecond order arithmeticclosed instancesconsistent sentenceextension of Kleene slashLindenbaum algebraslogoi

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Intuitionistic mathematics (03F55)

Related Items (3)

Introduction: A personal tribute to Peter Freyd and Bill Lawvere ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ Independent axiomatizability of sets of sentences

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Choice and well-ordering
• Amalgamation and interpolation in the category of Heyting algebras
• An application of open maps to categorical logic
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Arithmetic transfinite induction and recursive well-orderings
• On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis
• Completeness results for intuitionistic and modal logic in a categorical setting
• An extension of the Galois theory of Grothendieck
• La logique des topos
• The disjunction property implies the numerical existence property

This page was built for publication: Lindenbaum algebras of intuitionistic theories and free categories