Implicative algebras: a new foundation for realizability and forcing

DOI10.1017/S0960129520000079zbMath1498.03043arXiv1802.00528MaRDI QIDQ5139288

Alexandre Miquel

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1802.00528

zbMATH Keywords

forcingrealizabilitycategorical logic

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Proof theory in general (including proof-theoretic semantics) (03F03) Semilattices (06A12) Combinatory logic and lambda calculus (03B40) Other aspects of forcing and Boolean-valued models (03E40) Abstract algebraic logic (03G27)

Related Items

Triposes as a generalization of localic geometric morphisms ⋮ The category of implicative algebras and realizability ⋮ Stateful Realizers for Nonstandard Analysis ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Principal type schemes for an extended type theory
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Realizability. An introduction to its categorical side
• Minimally generated Boolean algebras
• Dependent choice, `quote' and the clock
• Realizability algebras II : new models of ZF + DC
• Specifying Peirce's law in classical realizability
• Ordered combinatory algebras and realizability
• Existential witness extraction in classical realizability and via a negative translation
• Tripos theory in retrospect
• Realizability algebras: a program to well order R
• A filter lambda model and the completeness of type assignment
• Proofs of strong normalisation for second order classical natural deduction
• The category of implicative algebras and realizability
• Krivine's classical realisability from a categorical perspective
• Intensional interpretations of functionals of finite type I
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• On the interpretation of intuitionistic number theory
• Realizability: a historical essay
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory