Ordered combinatory algebras and realizability

DOI10.1017/S0960129515000432zbMATH Open1423.03053arXiv1410.5034OpenAlexW2963271462MaRDI QIDQ2973254FDOQ2973254

Jonas Frey, Alexandre Miquel, Walter Ricardo Ferrer Santos, Octavio Malherbe, Mauricio German Guillermo

Publication date: 3 April 2017

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

Abstract: We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are equivalent for the purpose of modeling higher-order logic. We center our attentions in the role of a special kind of Ordered Combinatory Algebras-- that we call the "Krivine ordered combinatory algebras" ($mathcalKOCA$s)-- that we propose as the foundational pillars for the categorical perspective of Krivine's classical realizability as presented by Streicher. Our procedure is the following: we show that each of the considered combinatory structures gives rise to an indexed preorder, and describe a way to transform the different structures into each other that preserves the associated indexed preorders up to equivalence. Since all structures give rise to the same indexed preorders, we only prove that they are triposes once: for the class of $mathcalKOCA$s. We finish showing that in $mathcalKOCA$s, one can define realizability in every higher-order language and in particular in higher-order arithmetic.

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Intuitionistic mathematics (03F55)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tripos theory
• Continuous Lattices and Domains
• Lectures on the Curry-Howard isomorphism
• On the interpretation of intuitionistic number theory
• Realizability. An introduction to its categorical side
• Dependent choice, `quote' and the clock
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Adjointness in Foundations
• A 2-Categories Companion
• All realizability is relative
• Ordered partial combinatory algebras
• Iterated realizability as a comma construction
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Krivine's classical realisability from a categorical perspective

Cited In (3)

• On categorical structures arising from implicative algebras: from topology to assemblies
• Realized higher-order comoments
• Implicative algebras: a new foundation for realizability and forcing

This page was built for publication: Ordered combinatory algebras and realizability

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