arXiv 1007.08252010-07math.LOcs.LO

Realizability algebras II : new models of ZF + DC

Jean-Louis Krivine

备注：: 28 p
发表信息：: Logical Methods in Computer Science, Volume 8, Issue 1 (February 27, 2012) lmcs:1072
DOI：: 10.2168/LMCS-8(1:10)2012

英文摘要：

Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of ZF and relative consistency results in set theory. We show the relative consistency of ZF + DC + there exists a sequence of subsets of R the cardinals of which are strictly decreasing + other similar properties of R. These results seem not to have been previously obtained by forcing.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

A first-order completeness result about characteristic Boolean algebras in classical realizability

We prove the following completeness result about classical realizability: given any Boolean algebra with at least two elements, there exists a Krivine-style classical realizability model whose characteristic Boolean algebra is elementarily equivalent to it. This is done by controlling precisely which combinations of so-called "angelic" (or "may") and "demonic" (or "must") nondeterminism exist in the underlying model of computation.

2022-09-19cs.LOmath.LO

Realizability algebras III: some examples

We use the technique of "classical realizability" to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, probably not obtainable by forcing. This gives also a new method to get programs from proofs of arithmetical formulas with dependent choice.

2013-10-02cs.LOmath.LO

The category of implicative algebras and realizability

In this paper we continue with the algebraic study of Krivine's realizability, refining some of the authors' previous constructions by introducing two categories, with objects the abstract Krivine structures and the implicative algebras respectively. These categories are related by an adjunction whose existence clarifies many aspects of the theory previously established.

2019-04-18math.LO

Implicative algebras: a new foundation for realizability and forcing

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 constructi…

2020-02-20math.LO

Ordered combinatory algebras and realizability

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…

2014-10-19math.LO

A Report on Realizability

Besides recalling the basic definitions of Realizability Lattices, Abstract Krivine Structures, Ordered Combinatory Algebras and Tripos and reviewing its relationships, we propose a new foundational framework for realizability. Motivated by Streicher's paper "Krivine's Classical Realizability from a Categorical Perspective" [9], we define the concept of Krivine's Ordered Combinatory Algebras (kOKA) as a common platform that is strong enough to do both: categorical and computational semantics. The OCAs produced by Streicher from AKSs in [9] are particular cases of kOKAs.

2013-09-30math.LO

更多相关论文收起更多论文

一类用于修正可实现性的箭头代数

A category of arrow algebras for modified realizability

该研究定义箭头代数的态射概念以对应关联tripos的态射，用底层代数的核刻画箭头tripos的子tripos，还将修正可实现性拓展至箭头代数并证明其函子性，推进了相关代数与topos理论研究。

2025-01-13math.CTmath.LO

完全选择公理的一个程序

A program for the full axiom of choice

本文在经典可实现性框架下，提出了完全选择公理（AC）的第一个显式程序，填补了此前仅有依赖选择公理（DC）程序的空白。

2021-08-31cs.LOmath.LO

Partial Combinatory Algebras of Functions

We employ the notions of `sequential function' and `interrogation' (dialogue) in order to define new partial combinatory algebra structures on sets of functions. These structures are analyzed using J. Longley's preorder-enriched category of partial combinatory algebras and decidable applicative structures. We also investigate total combinatory algebras of partial functions. One of the results is, that every realizability topos is a quotient of a realizability topos on a total combinatory algebra.

2009-05-16math.LO

Arrow 代数

Arrow algebras

本文引入 Arrow 代数，一种简单代数结构，通过 tripos-to-topos 构造诱导初等 topos，涵盖局部化与可实现性 topos，并为 Kreisel 修正可实现性提供构造 topos 的通用工具。

2025-10-09math.CTmath.LO

编码逻辑对应：通过超图Heyting代数将信息和通信网络转化为逻辑公式

Coding-Logic Correspondence: Turning Information and Communication Networks into Logical Formulae via Hypergraph Heyting Algebra

The Chinese University of Hong Kong（香港中文大学）

通过超图Heyting代数将信息和通信网络转化为逻辑公式，实现编码设置与逻辑公式的对应关系。

2026-09-18cs.ITmath.ITmath.LO