2018/02/02 by Alexandre Miquel · 1 voice · 9 citations
Computer Science · Mathematics · #Advanced Algebra and Logic #Algebra over a field #Class (philosophy) #Forcing (mathematics) #Foundation (evidence) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical proof #Realizability #Salient #Simple (philosophy) #math.LO
paper · pdf · doi:10.1017/s0960129520000079
published in Mathematical Structures in Computer Science 30(5), 458-510 (Cambridge University Press) · 56 pages. Revised version (after reviewers' comments)
arxiv published 2018/02/02 · openalex created_date 2018/02/23 · arxiv created 2020/02/20 · openalex publication_date 2020/05/01 · arxiv updated 2020/07/15 · openalex updated_date 2026/08/05
Abstract We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model-theoretic constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a ( Set -based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompasses all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine), and all intuitionistic realizability triposes built from partial combinatory algebras.