Ordinal analysis and the set existence property for intuitionistic set theories

• 全文链接
• 请求原文

作   者：

Rathjen, Michael; 

作者机构：

Univ Leeds; 

关键词：

ordinal analysis;  existence property;  intuitionistic set theory;  realizability; 

期刊名称：

Philosophical transactions of the Royal Society. Mathematical, physical, and engineering sciences

i s s n：

1364-503X

年卷期：

2023 年 381 卷 2248 期

页   码：

ARTN 20220019-

页   码：

摘   要：

On account of being governed by constructive logic, intuitionistic theories T often enjoy various existence properties. The most common is the numerical existence property (NEP). It entails that an existential theorem of T of the form (there exists x is an element of N)A(x) can be witnessed by a numeral (n) over bar such that T proves A((n) over bar). While NEP holds almost universally for natural intuitionistic set theories, the general existence property (EP), i.e. the property of a theory that for every existential theorem, a provably definable witness can be found, is known to fail for some prominent intuitionistic set theories such as Intuitionistic Zermelo-Fraenkel set theory (IZF) and constructive Zermelo-Fraenkel set theory (CZF). Both of these theories are formalized with collection rather than replacement as the latter is often difficult to apply in an intuitionistic context because of the uniqueness requirement. In light of this, one is clearly tempted to single out collection as the culprit that stymies the EP in such theories. Beeson stated the following open problem: `Does any reasonable set theory with collection have the existence property? and added in proof: The problem is still open for IZF with only bounded separation.' (Beeson. 1985 Foundations of constructive mathematics, p. 203. Berlin, Germany: Springer.) In this article, it is shown that IZF with bounded separation, that is, separation for formulas in which only bounded quantifiers of the forms (for all x is an element of a), (for all x subset of a), (there exists x subset of a) are allowed, indeed has the EP. Moreover, it is also shown that CZF with the exponentiation axiom in place of the subset collection axiom has the EP. Crucially, in both cases, the proof involves a detour through ordinal analyses of infinitary systems of intuitionistic set theory, i.e. advanced techniques from proof theory. This article is part of the theme issue 'Modern perspectives in Proof Theory'.