Showing 1–6 of 6 results for author: Miquel, A

Implicative models of set theory

Authors: Samuele Maschio, Alexandre Miquel

Abstract: In this paper we show that using implicative algebras one can produce models of set theory generalizing Heyting/Boolean-valued models and realizability models of (I)ZF, both in intuitionistic and classical logic. This has as consequence that any topos which is obtained from a Set-based tripos as the result of the tripos-to-topos construction hosts a model of intuitionistic or classical set theory,… ▽ More In this paper we show that using implicative algebras one can produce models of set theory generalizing Heyting/Boolean-valued models and realizability models of (I)ZF, both in intuitionistic and classical logic. This has as consequence that any topos which is obtained from a Set-based tripos as the result of the tripos-to-topos construction hosts a model of intuitionistic or classical set theory, provided a large enough strongly inaccessible cardinal exists. △ Less

Submitted 18 November, 2023; v1 submitted 16 October, 2023; originally announced October 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2301.11740

MSC Class: 03B40; 03C62

Journal ref: Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX (November 23, 2023) entics:12426

Completions of Implicative Assemblies

Authors: Alexandre Miquel, Krzysztof Worytkiewicz

Abstract: We continue our work on implicative assemblies by investigating under which circumstances a subset $M \subseteq \mathscr{S}$ gives rise to a lex full subcategory $\mathbf{Asm}_M$ of the quasitopos $\mathbf{Asm}_{\mathcal{A}}$ of all assemblies such that $(\mathbf{Asm}_M)_{reg/lex} \simeq \mathbf{Asm}_{\mathcal{A}}$. We establish a characterisation. Furthermore, this latter is relevant to the study… ▽ More We continue our work on implicative assemblies by investigating under which circumstances a subset $M \subseteq \mathscr{S}$ gives rise to a lex full subcategory $\mathbf{Asm}_M$ of the quasitopos $\mathbf{Asm}_{\mathcal{A}}$ of all assemblies such that $(\mathbf{Asm}_M)_{reg/lex} \simeq \mathbf{Asm}_{\mathcal{A}}$. We establish a characterisation. Furthermore, this latter is relevant to the study of $\mathbf{Asm}_M$'s ex/lex-completion. △ Less

Submitted 10 July, 2023; v1 submitted 16 June, 2023; originally announced June 2023.

Implicative Assemblies

Authors: Félix Castro, Alexandre Miquel, Krzysztof Worytkiewicz

Abstract: Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this paper we introduce implicative assemblies as sets valued in the separator of an underlying implicative algebra. Given a fixed implicative algebra A, implicative assemblies over A organise themselves in a category Asm with tracked set-theo… ▽ More Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this paper we introduce implicative assemblies as sets valued in the separator of an underlying implicative algebra. Given a fixed implicative algebra A, implicative assemblies over A organise themselves in a category Asm with tracked set-theoretical functions as morphisms. We show that Asm is a quasitopos with NNO. △ Less

Submitted 20 April, 2023; originally announced April 2023.

Implicative algebras II: completeness w.r.t. Set-based triposes

Authors: Alexandre Miquel

Abstract: We prove that all Set-based triposes are implicative triposes. We prove that all Set-based triposes are implicative triposes. △ Less

Submitted 17 November, 2020; originally announced November 2020.

Comments: 14 pages

Implicative algebras: a new foundation for realizability and forcing

Authors: Alexandre Miquel

Abstract: We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model 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… ▽ More We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model 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 encompass 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. △ Less

Submitted 20 February, 2020; v1 submitted 1 February, 2018; originally announced February 2018.

Comments: 56 pages. Revised version (after reviewers' comments)

Journal ref: Math. Struct. Comp. Sci. 30 (2020) 458-510

Ordered combinatory algebras and realizability

Authors: Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, Alexandre Miquel

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" (… ▽ More 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" ($\mathcal{KOCA}$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 $\mathcal{KOCA}$s. We finish showing that in $\mathcal{KOCA}$s, one can define realizability in every higher-order language and in particular in higher-order arithmetic. △ Less

Submitted 19 October, 2014; originally announced October 2014.