Open Access

Research articles

Logics and admissible rules of constructive set theories

Rosalie Iemhoff

http://orcid.org/0000-0001-9975-9604

Department of Philosophy and Religious Studies, Utrecht University, Janskerkhof 13, 3512 BL Utrecht, The Netherlands

[email protected]

Contribution: Funding acquisition, Investigation, Methodology, Writing – original draft, Writing – review & editing

Google Scholar

Find this author on PubMed

Search for more papers by this author

and

Robert Passmann

Institute for Logic, Language and Computation, University of Amsterdam, PO Box 94242, 1090 GE Amsterdam, The Netherlands

Contribution: Funding acquisition, Investigation, Methodology, Project administration, Writing – original draft, Writing – review & editing

Google Scholar

Find this author on PubMed

Search for more papers by this author

Rosalie Iemhoff

http://orcid.org/0000-0001-9975-9604

Department of Philosophy and Religious Studies, Utrecht University, Janskerkhof 13, 3512 BL Utrecht, The Netherlands

[email protected]

Contribution: Funding acquisition, Investigation, Methodology, Writing – original draft, Writing – review & editing

Google Scholar

Find this author on PubMed

Search for more papers by this author

and

Robert Passmann

Institute for Logic, Language and Computation, University of Amsterdam, PO Box 94242, 1090 GE Amsterdam, The Netherlands

Contribution: Funding acquisition, Investigation, Methodology, Project administration, Writing – original draft, Writing – review & editing

Google Scholar

Find this author on PubMed

Search for more papers by this author

Published:10 April 2023https://doi.org/10.1098/rsta.2022.0018

Abstract

We survey the logical structure of constructive set theories and point towards directions for future research. Moreover, we analyse the consequences of being extensible for the logical structure of a given constructive set theory. We finally provide examples of a number of set theories that are extensible.

This article is part of the theme issue ‘Modern perspectives in Proof Theory’.

1. Introduction

Constructive set theories are formal systems in which we can conduct intuitionistic or constructive mathematics. Many systems of constructive set theory have strong connections to type theory and are interesting because they allow us to analyse the computational content of mathematical statements.

When a constructive mathematical theory $T$ is defined, we usually pay special attention to ensure that not all instances of the law of excluded middle,

p \lor \neg p,

are derivable in

T

. Even if an axiom looks constructive, it may happen that it entails this logical law, and if all instances of the law of excluded middle are derivable, then the axiom is constructively unacceptable.

Consider, for a well-known example, the famous theorem by Diaconescu [1] and Goodman & Myhill [2] that adding the axiom of choice to intuitionistic set theory IZF (Intuitionistic Zermelo–Fraenkel set theory) results in the classical $Z F C$ set theory. This result is often taken as evidence for rejecting the axiom of choice as constructively valid. However, showing that a certain instance of excluded middle is not constructively valid is not sufficient for ensuring that only principles of intuitionistic logic are satisfied. After all, there could be intermediate principles that are derivable in $T$ . Dick de Jongh was the first to investigate this phenomenon: in his doctoral dissertation [3], he showed that the propositional principles valid in Heyting arithmetic $(HA)$ under all substitutions are exactly those of propositional intuitionistic logic (IPC). This fact is now known as de Jongh’s theorem and has sparked fruitful investigations into the logical structure of intuitionistic arithmetic. A generalization of de Jongh’s theorem would be to consider not only the propositional principles of $HA$ but also its propositional admissible rules (see definition 2.3). Visser [4] showed that the propositional admissible rules of $HA$ are exactly those of $IPC .$ A further generalization would be to consider the two notions in the setting of predicate logic.

In this article, we survey results about the logical structure of constructive set theories and also provide a few new results in the area as well as questions for future research.

The study of the logical properties of classical and non-classical theories goes back at least several decades. Early results on the logics of theories date from the 1970s, and Rybakov’s seminal work on admissibility [5] marked the beginning of a period during which the admissible rules were investigated for many theories, see [6] for an overview. What is characteristic of that period is that the theories involved were mainly arithmetical theories, such as HA, or extensions of propositional logics, such as modal, intermediate and substructural logics. This naturally leads to the more general questions studied today, questions that ask whether the phenomena observed for arithmetic apply to other well-known constructive theories, and whether the phenomena observed for propositional logics also hold for predicate logics. Behind all this lie conceptual issues as well: What does it mean for a theory to have the same logic or rules as a given theory? Should it be required of a genuine constructive theory that it has the same admissible rules as intuitionistic propositional or predicate logics? These questions characterize the modern perspective on the area. We do not know the answers to all of them yet, but the results in this article provide some answers for constructive set theories.

(a) Overview

We will introduce what we understand as the logical structure of a theory in §2 and then survey the techniques and results obtained so far in §3. Section 4 will be dedicated to obtaining a few new results. We mention suggestions for future research throughout the article and also list some more in §5. Finally, we discuss the logics and admissible rules of the extreme case of classical theories in §6.

2. Preliminaries: the logical structure of a theory

We denote intuitionistic propositional logic by $IPC$ and intuitionistic first-order logic by $IQC$ . Classical propositional logic is denoted by $CPC$ and classical first-order logic by $CQC$ . If a logic $J$ satisfies $IPC \subseteq J \subseteq CPC$ or $IQC \subseteq J \subseteq CQC$ , then it is a (propositional or first-order) intermediate logic.

In this article, we work with first-order logics formulated in the language consisting of countably many predicate symbols $P_{i}$ for $i \in N$ in every arity. The formulas of first-order logic are recursively defined in the usual way with the connectives and quantifiers $\neg$ , $\land$ , $\lor$ , $\to$ , $\forall$ and $\exists$ . We also consider $⊥$ and $⊤$ to be part of the logical vocabulary. Note that we take constants and functions to be expressed as predicates in the usual way. The language of propositional logic is obtained by restricting to nullary predicates (i.e. the propositional letters) and forgetting the quantifiers. Finally, we assume that all first-order languages share the same set of variables ${x_{i}}_{i \in N}$ .

Definition 2.1.

Let $T$ be a theory. A map $σ$ is a $T$ -assignment if and only if it maps each predicate symbol $R$ to a $T$ -formula $σ (R)$ such that the number of free variables of $σ (R)$ is not bigger than the arity of $R$ .

For example, given a binary relation symbol $R$ , we could obtain a $T$ -assignment by setting $σ (R) = ` x_{0} \in x_{1}'$ . We denote the formulas of first-order logic by $L_{F O L}^{f o r m}$ and those of a theory $T$ by $L_{T}^{f o r m}$ . We can then obtain substitutions from assignments as follows.

Definition 2.2.

Let $T$ be a theory. A map $σ : L_{F O L}^{f o r m} \to L_{T}^{f o r m}$ is a $T$ -substitution if it obtained from a $T$ -assignment $τ$ such that $σ (R (x_{i_{1}}, \dots, x_{i_{n}})) = τ (R) (x_{i_{1}}, \dots, x_{i_{n}})$ , and, moreover, commutes with $⊥$ , $⊤$ and the logical connectives. If the range of $σ$ is ${⊤, ⊥}$ , then it is a ground substitution.

The theory $T$ is often clear from the context, and we will then speak of substitutions instead of $T$ -substitutions. As usual, a rule $Γ / Δ$ is a pair of finite sets of logical formulas.

Definition 2.3.

Let $T$ be a theory. A rule $Γ / Δ$ is admissible in $T$ , $Γ \sim_{T} Δ$ , if and only if for every substitution $σ$ , if $T ⊢ σ (A)$ for all $A \in Γ$ , then there is $B \in Δ$ such that $T ⊢ σ (B)$ .

By $\sim$ , we will denote the admissibility relation in which we consider only propositional formulas. We will consider more closely now the propositional and first-order tautologies of a theory.

Definition 2.4.

A formula $A$ of first-order logic is a tautology of $T$ if and only if $⊤ \sim_{T} A$ .

Proposition 2.5.

A formula $A$ is a tautology of $T$ if and only if $T ⊢ σ (A)$ for all substitutions $σ$ .

Proof.

Note that $⊤ \sim_{T} A$ is by definition equivalent to $T ⊢ σ (⊤)$ implying $T ⊢ σ (A)$ for all $σ$ . As the premise is true for any $T$ , the implication is equivalent to $T ⊢ σ (A)$ for every $σ$ .

Given this definition, we can define the propositional and first-order logics of a theory.

Definition 2.6.

Let $T$ be a theory. The propositional logic of $T$ , $L (T)$ , consists of all propositional tautologies of $T$ . The first-order logic of $T$ , $QL (T)$ , consists of all first-order tautologies of $T$ .

We can now ask four natural questions about the logical structure of a given theory $T$ :

(i)	What are the first-order admissible rules of $T$ ? $\sim_{T} = ?$
(ii)	What are the propositional admissible rules of $T$ ? $\sim_{T} = ?$
(iii)	What is the first-order logic of $T$ ? $QL (T) = ?$
(iv)	What is the propositional logic of $T$ ? $L (T) = ?$

Given the aforementioned definitions, it is clear that answers to some of these questions imply answers to others: If we know an answer to (i), then we know answers to (ii)–(iv). If we know an answer to (ii), then to (iv) as well. Finally, if we know an answer to (iii), then also to (iv). Still, there are several reasons to consider these questions separately. First, the following theorem shows that an informative answer—in the sense of a recursive description—to (i) is in general not possible.

Theorem 2.7. (Visser [4])

Let $T$ be a theory such that $I Δ_{0} + Exp$ can be relatively interpreted in $T$ . If $T$ has the disjunction property, then $\sim_{T}$ is $Π_{2}^{0}$ -complete.

Proof.

This is Visser’s result; however, as we are not working with relative interpretations here, one needs to add this explicitly on the logical side by replacing the quantifiers $\exists x A (x)$ and $\forall x A (x)$ with $\exists x (R (X) \land A (x))$ and $\forall x (R (x) \to A (x))$ , respectively, where $R$ is a new relation symbol.

However, one may of course still wonder whether the first-order admissible rules of any two theories are the same (question 5.1) or study the admissibility of specific interesting rules (see, e.g. van den Berg & Moerdijk [7]). Another reason to consider these questions separately is that, of course, the more complex objects require more complicated proofs than the simpler ones. In a sense, question (iv) can often be seen as a litmus test for the more difficult questions (ii) and (iii): if we conjecture that $QL (T) = IQC$ , then showing that $L (T) = IPC$ is a step in the right direction (though there are counter examples, e.g. $L (I Z F) = IPC$ but $QL (I Z F) \neq IQC$ , see §3). It may even be necessary to know an answer to (iv) before applying certain techniques for obtaining an answer to (ii), viz. the propositional admissible rules of $T$ . We will see much more detail in the remainder of this article. For now, we will dive a bit deeper into the logics and propositional admissible rules of a given theory.

We say that a theory $T$ is based on a logic $J$ if $T$ is axiomatized over $J$ . As the results discussed in this article show, if a theory $T$ is based on $IQC$ , we do not necessarily have that $QL (T) = IQC$ . Crucially, we cannot only study the logics of a theory $T$ based on intuitionistic logic but, given an intermediate logic $J$ , we can consider the theory $T (J)$ obtained as the closure of $T$ under $J$ . de Jongh et al. [8] studied these theories and defined the de Jongh property as follows.

Definition 2.8.

Let $J$ be a propositional or first-order intermediate logic. A theory $T$ has the de Jongh property for $J$ just in case $L (T (J)) = J$ if $J$ is propositional or $QL (T (J)) = J$ if $J$ is first order.

We also say that a theory $T$ satisfies de Jongh’s theorem if $L (T) = IPC$ , and that $T$ satisfies de Jongh’s theorem for first-order logic if $QL (T) = IQC$ . To illustrate research in this area, we now give an incomplete history of de Jongh’s theorem for arithmetical theories (see de Jonghet al. [8] for a more complete history). De Jongh [3] proved that $L (HA) = IPC$ —; in other words, he proved that $HA$ satisfies the de Jongh property for $IPC$ . Leivant [9] showed using proof theoretic means that $QL (HA) = IQC$ ; van Oosten later gave a model theoretic proof of the same fact. De Jongh et al. [8] proved that $HA$ has the de Jongh property for several classes of intermediate logics. The following propositions are immediate from proposition 2.5.

Proposition 2.9.

Let $T \subseteq S$ be theories in the same language. If $A$ is a tautology of $T$ , then it is a tautology of $S$ . In particular, $L (T) \subseteq L (S)$ and $QL (T) \subseteq QL (S)$ .

Proposition 2.10.

Let $J$ be a propositional or first-order intermediate logic. If $T \subseteq S$ are theories in the same language and $S$ satisfies the de Jongh property for $J$ , then so does $T$ . In particular, if $S$ satisfies de Jongh’s theorem, then so does $T$ .

A first crucial observation on the admissible rules of a theory is that these are bounded by its logic.

Theorem 2.11. (Visser [4])

Let $T$ be a theory. If $A \sim_{T} B$ , then $A \sim_{QL (T)} B$ ; i.e. $\sim_{T} \subseteq \sim_{QL (T)}$ . Similarly, if $A \sim_{T} B$ , then $A \sim_{L (T)} B$ ; i.e. $\sim_{T} \subseteq \sim_{L (T)}$ .

Not much is known about the converse direction. A counterexample could be obtained with theorem 2.7 if it turns out that the predicate admissible rules of $IQC$ are of complexity lower than $Π_{2}^{0}$ -completeness. We close these preliminaries with two particularly helpful results for studying the propositional admissible rules of a given theory. A theory $T$ is called extensible if any Kripke model of $T$ can be extended by adding a new root and corresponding domain to obtain a new model of $T$ (see also definition 4.1).

Theorem 2.12. Visser ([4], Lemma 4.1)

Let $T$ be a theory with $L (T) = IPC$ . If $T$ is extensible, then the propositional admissible rules of $T$ are exactly those of $IPC$ , $\sim_{T} = \sim_{IPC}$ .

The Visser rule $V_{n}$ is the following rule for propositional formulas $A_{i}$ , $B_{i}$ and $C$ :

\frac{(⋀_{i = 1}^{n} (A_{i} \to B_{i}) \to (A_{n + 1} \lor A_{n + 2})) \lor C}{⋁_{j = 1}^{n + 2} (⋀_{i = 1}^{n} (A_{i} \to B_{i}) \to A_{j}) \lor C} .

$V_n$

The collection of Visser rules consists of the rules

V_{n}

for every

n

Theorem 2.13.

Let $T$ be a theory with $L (T) = IPC$ . If the Visser rules are admissible in $T$ , then the admissible rules of $T$ are exactly those of $IPC$ .

Proof.

Let $A$ and $B$ be propositional formulas. By theorem 2.11, it suffices to show that if $A \sim_{IPC} B$ , then $A \sim_{T} B$ . So assume that $A \sim_{IPC} B$ . By a theorem of Iemhoff ([10], Theorem 3.9), this means that $A ⊢_{IPC}^{V} B$ , where $⊢_{IPC}^{V}$ denotes the derivability relation of $IPC$ extended with all of Visser’s rules. In other words, there is a proof tree, potentially using $A$ as a premise, all steps in which are instances of the rules of $IPC$ and $V$ , and whose conclusion is $B$ . Given that Visser’s rules are admissible in $T$ , and using the fact that $T$ is based on intuitionistic logic, it is straightforward to see that every rule application in the proof tree is admissible in $T$ . Hence, $B$ is an admissible consequence of $A$ , $A \sim_{T} B$ .

The two theorems give two routes to proving that the propositional admissible rules of a theory $T$ are exactly those of $IPC$ . We will see that theorem 2.12 can be seen as an instance of theorem 2.13 because Visser’s rules are admissible in any extensible theory (lemma 4.7). In this section, we covered the preliminaries for theories based on intuitionistic logic. There is more to say for the extreme case of theories based on classical logic, see §6.

3. Survey on techniques and results

(a) Constructive set theories

In this section, we can only give a very brief introduction to constructive set theory. As usual, the language $L_{\in}$ of set theory is a first-order language with equality and a single binary relation symbol ‘ $\in$ ’ to denote set membership. We consider the bounded quantifiers $\forall x \in a φ (x)$ and $\exists x \in a φ (x)$ to be abbreviations for $\forall x (x \in a \to φ (x))$ and $\exists x (x \in a \land φ (x))$ , respectively. The crucial aim of intuitionistic and constructive set theories is to provide a set-theoretic foundation for mathematics on the basis of intuitionistic instead of classical logic. We will now introduce the relevant systems.

In figure 1, we have spelt out all the axioms of set theory, giving rise to the following theories. Note that ‘ $z$ is full in $x$ and $y$ ’ means that every element of $z$ is a total relation between $x$ and $y$ and for every total relation $w$ between $x$ and $y$ , and there is some $u \in z$ such that $u \subseteq w$ . We can now define the relevant theories. The bounded separation consists of all instances of (separation), where $φ$ is a bounded formula (i.e. $φ$ is $Δ_{0}$ ). In a similar way, we obtain the axiom scheme of bounded collection.

Definition 3.1.

We define the following set theories on the basis of intuitionistic first-order logic.

(i)	Intuitionistic Zermelo–Fraenkel set theory (IZF) consists of the axioms and schemes of extensionality, empty set, union, pairing, infinity, separation, $\in$ -induction, collection and power set.
(ii)	Constructive Zermelo–Fraenkel set theory (CZF) consists of the axioms and schemes of extensionality, empty set, union, pairing, strong infinity, bounded separation, $\in$ -induction, strong collection and subset collection.
(iii)	Intuitionistic Kripke–Platek set theory (IKP) consists of the axioms and schemes of extensionality, empty set, union, pairing, infinity, bounded separation, $\in$ -induction and bounded collection.
(iv)	Basic constructive set theory (BCST) consists of the axioms and schemes of extensionality, empty set, union, pairing, replacement and bounded separation.
(v)	Elementary constructive set theory (ECST) consists of the axioms and schemes of extensionality, empty set, pairing, union, strong infinity, bounded separation and replacement.

The theory

IZ F_{R}

I Z F

with replacement instead of collection, and

C Z F_{E R}

C Z F

with exponentiation and replacement instead of strong collection and subset collection.

Note that $C Z F$ is usually formulated with the axiom of infinity instead of strong infinity. Obviously, the axiom of strong infinity implies infinity. The converse is also true on the basis of $C Z F$ without any infinity axioms [11, section 2.1]; so we can consider $C Z F$ to be formulated with the axiom of strong infinity instead of infinity, as this will be important later. For a detailed development of the mathematics of and in constructive set theories, we refer the reader to the notes of Aczel & Rathjen [12]. Whenever we discuss the results for an arbitrary set theory $T$ in this article, we assume that $T$ contains at least intuitionistic logic.

(b) Techniques and results

We will now survey what is known about the logical structure of constructive set theories. For many years, only the following two negative results were known.

Theorem 3.2. (Diaconescu [1]; Goodman & Myhill [2])

Let $T$ be a set theory that proves $0 \neq 1$ as well as the axioms of extensionality, pairing, and the separation scheme. If $T$ proves the axiom of choice, then $T$ proves all instances of the law of excluded middle.

Theorem 3.3. (Friedman & Ščedrov [13])

Let $T$ be a set theory containing the axioms and schemes of extensionality, separation, pairing and (finite) union. Then $IQC ⊊ QL (T)$ . In particular, $IQC ⊊ QL (I Z F) ⊊ CQC$ .

While we do not wish to spell out the proofs of these theorems in detail, we will point out here that both of them make crucial use of the separation scheme to define sets that allow to derive a logical scheme for all formulas. This observation is crucial as we will see in a while that Passmann [14] showed that both theorems fail on the basis of $C Z F$ , i.e. when the set theory does not contain the full separation scheme. Note that theorem 3.3 leads to the following open question.

Question 3.4.

Let $T$ be a set theory, based on intuitionistic logic, satisfying the conditions of theorem 3.3. What is $QL (T)$ ? In particular, what is $QL (I Z F)$ ?

Before considering more recent results, we will briefly recall some notation and results on Kripke models. A Kripke frame $(K, \leq)$ consists of a partial order $\leq$ on a set $K$ . A valuation $V$ on $(K, \leq)$ is a function $V$ assigning sets of propositional letters to nodes such that $v \leq w$ and $p \in V (v)$ entail $p \in V (w)$ . A Kripke model $(K, \leq, V)$ consists of a Kripke frame $(K, \leq)$ and a valuation $V$ on $(K, \leq)$ . The valuation $V$ can be extended to the forcing relation $⊩$ between Kripke models and valuation Kripke models and propositional formulas in the usual way. The defining property of valuations is called persistence and transfers to all propositional formulas in Kripke models, i.e. $v ⊩ φ$ and $v \leq w$ entail $w ⊩ φ$ (this property also holds for all first-order formulas in the case of first-order models, see below). We refer to the literature for the standard results about Kripke models for intuitionistic logic.

We are now ready to move to more recent results. All the results we are going to mention are obtained by model theoretic methods, i.e. a result of the form $QL (T) = J$ is usually obtained by, first, showing that $T$ proves all instances of $J$ (this is usually easy), and second, for every logical principle $A$ such that $J ⊬ A$ , one constructs a countermodel $M$ of $T$ , which also fails that principle. In other words, there is then a $T$ -substitution $σ$ such that $M ⊨ T$ but $M ⊭ σ (A)$ . We say that an intermediate logic $J$ is characterized by a class $K$ of Kripke models if and only if $J ⊢ A$ if and only if $M ⊨ A$ for every $M \in K$ . The class of finite trees consists of the finite partial orders $(P, \leq)$ such that for any $p \in P$ , the set ${q \in P | q \leq p}$ is linearly ordered.

Theorem 3.5. (Passmann [15])

Let $T \subseteq I Z F$ be a set theory. If $J$ be an intermediate propositional logic that is characterized by a class of finite trees, then $L (T (J)) = J$ . In particular, $L (T) = IPC$ .

This result was proved by using so-called blended Kripke models, and we will see an adaptation of this technique in §4. For now, we just note that Passmann’s blended models are inspired by the models that Lubarksy [16] used to show various independence results around $C Z F$ .

The next two results were proved by Iemhoff & Passmann [17]. Note that ${I K P}^{+}$ is obtained by adding weak versions of strong collection and subset collection to $I K P$ (for details see their paper). An intermediate logic $J$ is called Kripke-complete if there is a class $K$ of Kripke models such that $J$ is characterized by $K$ .

Theorem 3.6. (Iemhoff & Passmann [17])

Let $T \subseteq {I K P}^{+} + M P + A C$ be a set theory. If $J$ is a Kripke-complete intermediate propositional logic, then $L (T (J)) = J$ .

Theorem 3.7. (Iemhoff & Passmann [17])

Let $T \subseteq {I K P}^{+} + M P + A C$ be a set theory. If $J$ is a Kripke-complete intermediate first-order logic contained in the least transitive model of $Z F C + V = L$ , then $QL (T (J)) = J$ . In particular, $QL (T) = IQC$ .

For these results, Iemhoff & Passmann use (what they call) Kripke models with classical domains. These models are obtained by equipping each node of a Kripke frame with a classical model of set theory in a coherent way. An earlier result by Iemhoff [18] entails that these models will always satisfy $I K P$ . Passmann showed in his master’s thesis [19] that this result is in a certain sense optimal: there are Kripke models with classical domains that do not satisfy the exponentiation axiom (which is a consequence of $C Z F$ ). The aforementioned results could be proved for large classes of logics because the simple structure of the Kripke models with classical domains allows much control about their logical structure.

Finally, Iemhoff & Passmann also obtained the following negative result for first-order logic with equality. Note that ${QL}^{=} (T)$ is obtained just like $QL (T)$ with the additional requirement that substitutions commute with ‘ $=$ ’.

Theorem 3.8. (Iemhoff & Passmann [17], theorem 61)

Let $T$ be a set theory containing the axioms of extensionality, empty set and pairing. Then the first-order logic with equality of $T$ , ${QL}^{=} (T)$ , is strictly stronger than ${IQC}^{=}$ , i.e. ${IQC}^{=} ⊊ {QL}^{=} (T)$ .

Question 3.9.

Given any set theory $T$ , what is its first-order logic with equality ${QL}^{=} (T)$ ?

The following results were obtained by combining realizability techniques with transfinite computability. The latter is a generalization of classical computability by allowing machines to run for an infinite amount of time and/or use an infinite amount of space. For a thorough introduction, we refer the reader to Carl’s book [20].

Theorem 3.10. (Carl et al. [21])

The propositional admissible rules of $I K P$ are exactly those of $IPC$ , i.e. $\sim_{I K P} = \sim_{IPC}$ .

Theorem 3.11. (Passmann [14])

The propositional admissible rules of $C Z F$ are exactly those of $IPC$ , i.e. $\sim_{C Z F} = \sim_{IPC}$ .

Theorem 3.12. (Passmann [14])

Let $T \subseteq C Z F + P o w e r S e t + A C$ be a set theory. The first-order logic of $T$ is intuitionistic first-order logic $IQC$ , $QL (T) = IQC$ .

It is crucial to note here that the proof method of theorem 3.12 does not allow to prove the result for any intermediate logic $J$ .

Question 3.13.

Can theorem 3.12 be generalized to a class of intermediate first-order logics?

In general, all results surveyed in this section introduce assumptions on the logic $J$ under consideration. We may therefore ask the following question (table 1).

Table 1. An overview of the most important intuitionistic and constructive set theories and whether they satisfy de Jongh’s propositional and first-order theorems, and whether their admissible rules are exactly those of $IPC$ , as discussed in the survey. The question marks (‘ $?$ ’) indicate open problems. The results marked with a reference within this article are new.
Collapse
$T$	$L (T) = IPC$	$QL (T) = IQC$	$\sim_{T} = \sim_{IPC}$
$I K P$	✓	✓	✓
$B C S T$	✓	✓	✓ (corollary 4.13)
$E C S T$	✓	✓	✓ (corollary 4.13)
$C Z F_{E R}$	✓	✓	✓ (corollary 4.13)
$C Z F$	✓	✓	✓
$C Z F + A C$	✓	✓	✓
$IZ F_{R}$	✓	✗; $IQC ⊊ QL (IZ F_{R}) = ? ⊊ CQC$	✓ (corollary 4.13)
$I Z F$	✓	✗; $IQC ⊊ QL (I Z F) = ? ⊊ CQC$	✗; $\sim_{IPC} ⊊ \sim_{I Z F} = ?$
$I Z F + A C$	✗; $L (I Z F + A C) = CPC$	✗; $CQC \subseteq QL (I Z F + A C)$	✗; $\sim_{I Z F + A C} = \sim_{CPC}$

Question 3.14.

Is it possible to extend the results of this section to larger classes of logics? If not, find counterexamples for which these theorems fail if the assumptions on the logics $J$ are weakened.

4. Logics and rules of set theories

(a) Logic, rules and the extension property

In this section, we will prove a set-theoretic analogue of Visser’s [4, lemma 4.1] Main Lemma. Given a Kripke frame $K$ , we write $K^{+}$ for the frame extended with a new root. The construction of adding a new root to a Kripke model was first used by Smorynski [22] for models of $HA$ to give an alternative proof of de Jongh’s theorem for $HA$ . In the arithmetical case, it suffices to equip the new root with the standard model of arithmetic. The case of the set theory requires a more elaborate construction, as we will now see.

Definition 4.1.

Let $Γ$ be a set of sentences in the language of set theory. A set of sentences $Δ$ is $Γ$ -extensible if for every Kripke model $M ⊩ Γ \cup Δ$ of set theory with underlying frame $K$ , there is a model $M^{+}$ based on $K^{+}$ such that $M^{+} ↾ K = M$ and $M^{+} ⊩ Δ$ ; $Δ$ is extensible if it is $\emptyset$ -extensible.

To avoid cumbersome notation, we will say that a sentence $φ$ is ( $Γ$ -)extensible just in case ${φ}$ is ( $Γ$ -)extensible. We will later need the following two brief observations.

Lemma 4.2.

Let $Γ \subseteq Δ$ be sets of formulas. If $Δ$ is $Γ$ -extensible, then $Δ$ is extensible.

Proof.

Let $M ⊩ Δ$ . As $Γ \subseteq Δ$ , we have $M ⊩ Δ \cup Γ$ . By $Γ$ -extensibility, it follows that $M^{+} ⊩ Δ$ .

Lemma 4.3.

Let $Γ \subseteq Δ$ be sets of formulas. If a sentence $φ$ is $Γ$ -extensible, then it is $Δ$ -extensible.

Proof.

Let $M ⊩ {φ} \cup Δ$ . As $Γ \subseteq Δ$ , we have $M ⊩ {φ} \cup Γ$ . By $Γ$ -extensibility, $M^{+} ⊩ φ$ .

A Kripke frame $(K, \leq)$ is a finite splitting tree if $K$ is finite, connected and every $v \in K$ has either no successors or at least two immediate successors. A node $v \in K$ with no successors is also called a leaf. An easy induction on the height of finite splitting trees allows to show that every node in such a tree is uniquely determined by the set of leaves above it. A set theory $T$ is called subclassical if there is a classical model of $T$ .

The following theorem follows the same idea as Smorynski’s proof of de Jongh’s theorem for $HA$ [22]. For this reason, this proof method is also sometimes referred to as Smorynski’s trick.

Theorem 4.4.

Let $J$ be a propositional intermediate logic characterized by a class of finite splitting trees. If $T$ is a subclassical recursively enumerable extensible set theory, then $J$ is the propositional logic of $T (J)$ , i.e. $L (T (J)) = J$ .

Proof.

Let $2^{< ω}$ be the set of binary sequences of finite length, and $2^{n}$ be the set of binary sequences of length $n$ . If $T$ is a recursively enumerable theory, let $Γ_{T}$ be its Gödel sentence. Let $φ^{⟨ 0 ⟩} := Γ_{T}$ , and $φ^{⟨ 1 ⟩} := \neg Γ_{T}$ . Clearly both $T + φ^{⟨ 0 ⟩}$ and $T + φ^{⟨ 1 ⟩}$ are consistent by Gödel’s incompleteness theorem. By recursion on the length of $s \in 2^{< ω}$ , we define

φ^{s^{⌢} ⟨ 0 ⟩} := φ^{s} \land Γ_{T + φ^{s}} and

φ^{s^{⌢} ⟨ 1 ⟩} := φ^{s} \land \neg Γ_{T + φ^{s}} .

By inductively applying Gödel’s incompleteness theorem, it follows that

T + φ^{s}

is consistent for every

s \in 2^{< ω}

; so, for every

s \in 2^{< ω}

, let

M_{s}

be a classical model such that

M_{s} ⊨ T + φ^{s}

We now observe that, given $s, t \in 2^{< ω}$ of the same length with $s \neq t$ , it must be that $φ^{s}$ and $φ^{t}$ are jointly inconsistent: Let $i$ be minimal such that $s (i) \neq t (i)$ . Then $s ↾ i = t ↾ i$ , and we can assume, without loss of generality, that $s (i) = 0$ and $t (i) = 1$ . The sentences $φ^{s}$ and $φ^{t}$ are defined as conjunctions in such a way that $φ^{s}$ contains the conjunct $Γ_{T + φ^{s ↾ i}}$ , and $φ^{t}$ contains the conjunct $\neg Γ_{T + φ^{t ↾ i}}$ . Since $s ↾ i = t ↾ i$ , it follows that $φ^{s} \to \neg φ^{t}$ . We can conclude for $n < ω$ and $s \in 2^{n}$ that

M_{s} ⊨ φ^{s} \land \underset{t \in 2^{n} ∖ {s}}{⋀} \neg φ^{t} .

Let $T$ be a set theory and $J$ be a logic, as given in the statement of the theorem. To prove that $L (T (J)) = J$ , we will proceed as follows: Let $C$ be a class of finite splitting trees that characterizes the logic $J$ . It is clear that $J \subseteq L (T (J))$ . To show that $L (T (J)) \subseteq J$ , we proceed by contraposition. So assume that $J ⊬ A$ for some propositional formula $A$ , then there is a finite splitting tree $(K, \leq) \in C$ and a valuation $V$ on $K$ such that $(K, \leq, V) ⊩ J$ but $(K, \leq, V) ⊮ A$ . On the basis of this propositional Kripke model, we will construct a Kripke model $M ⊩ T$ of set theory and a propositional translation $τ$ such that $M ⊮ A^{τ}$ . As $M$ is based on the frame $(K, \leq) ⊩ J$ , it follows that $M ⊩ T (J)$ . Hence, it follows that $A \notin L (T (J))$ .

As every finite splitting tree can be constructed from its set of leaves by iterating the operation of adding a new root, we can obtain a model of $T$ on the frame $(K, \leq)$ as follows. Find $n < ω$ such that there are at least as many $s \in 2^{n}$ as there are leaves in $K$ ; let $l \mapsto s_{l}$ be an injective map assigning sequences to leaves. Assign the models $M_{s_{l}}$ to the leaves of $(K, \leq)$ and use the extensibility of $T$ to construct a Kripke model $M$ of $T$ with underlying frame $(K, \leq)$ . Given $v \in K$ , let $E_{v}$ be the set of leaves $l \geq v$ . Then consider the formula

γ_{v} := \neg \neg \underset{l \in E_{v}}{⋁} φ^{s_{l}} .

Now recall that every node

v

in the finite splitting tree

(K, \leq)

is characterized by the set

E_{v}

and that

M_{s_{l}} ⊨ φ^{s_{k}}

if and only if

l = k

. It follows that

M

w ⊩ γ_{v}

if and only if

w \geq v

We are now ready to construct the translation $τ$ . Given a propositional letter $p$ , let

τ (p) := \underset{v \in V (p)}{⋁} γ_{v} = \underset{v \in V (p)}{⋁} \neg \neg \underset{l \in E_{v}}{⋁} φ^{s_{l}} .

Moreover,

τ

commutes with the propositional connectives

\neg

\to

\lor

and

\land

To finish the proof of the theorem, it now suffices to show that $M, w ⊩ τ (p)$ if and only if $w \in V (p)$ ; it then follows by induction that $M$ , $w ⊩ A^{τ}$ if and only if $(K, \leq, V), w ⊩ A$ . So assume that $M, w ⊩ τ (p)$ . Equivalently, $M, w ⊩ γ_{v}$ for some $v \in V (p)$ . We have seen that this is equivalent to $w \geq v$ for some $v \in V (p)$ , which, by persistence, holds if and only if $w \in V (p)$ .

Note that $IPC$ is characterized by the class of finite trees [23, theorem 6.12]. To show that $IPC$ is characterized by the class of finite splitting tress, note that duplicating branches of a tree does not change the formulas satisfied at the root.

Corollary 4.5.

Let $T$ be a subclassical recursively enumerable set theory. If $T$ is extensible, then the propositional logic of $T$ is intuitionistic propositional logic $IPC$ , i.e. $L (T) = IPC$ .

Let us first observe the following helpful fact. Recall that a theory $T$ has the disjunction property whenever $T ⊢ φ \lor ψ$ implies $T ⊢ φ$ or $T ⊢ ψ$ .

Lemma 4.6.

If $T$ is an extensible set theory, then $T$ has the disjunction property.

Proof.

By contraposition. Assume that $T ⊬ φ$ and $T ⊬ ψ$ , then there are models $M_{0}$ and $M_{1}$ of $T$ such that $M_{0} ⊮ φ$ and $M_{1} ⊮ ψ$ . Let $M$ be the disjoint union of these models, then $M^{+} ⊩ T$ as $T$ is extensible. Moreover, persistence implies that $M^{+} ⊮ φ \lor ψ$ ; hence, $T ⊬ φ \lor ψ$ .

Lemma 4.7.

If $T$ is an extensible set theory, then Visser’s rules are admissible in $T$ .

Proof.

By lemma 4.6, it is sufficient to show that the following rules $V_{n}^{'}$ are admissible:

\frac{⋀_{i = 1}^{n} (A_{i} \to B_{i}) \to (A_{n + 1} \lor A_{n + 2})}{⋁_{j = 1}^{n + 2} (⋀_{i = 1}^{n} (A_{i} \to B_{i}) \to A_{j})} .

$V'_n$

The admissibility of these rules is a standard argument and proceeds as follows by contraposition. For greater readability, we write

σ A

for

σ (A)

in this proof.

Let $σ : P r o p \to L_{\in}^{s e n t}$ be any substitution and assume that $T ⊬ ⋁_{j = 1}^{n + 2} (⋀_{i = 1}^{n} (σ A_{i} \to σ B_{i}) \to σ A_{j})$ , i.e. $T ⊬ ⋀_{i = 1}^{n} (σ A_{i} \to σ B_{i}) \to σ A_{j}$ for $j = 1, \dots, n + 2$ . By Kripke completeness, let $M_{j}$ be a Kripke model of $T$ with root $r_{j}$ such that $M_{j} ⊮ ⋀_{i = 1}^{n} (σ A_{i} \to σ B_{i}) \to σ A_{j}$ . In this situation, we can assume without loss of generality that $M_{j}, r_{j} ⊩ ⋀_{i = 1}^{n} (σ A_{i} \to σ B_{i})$ , but $M_{j}, r_{j} ⊮ σ A_{j}$ .

Now, let $M$ be the disjoint union $⟨ M_{j} | j = 1, \dots, n + 2 ⟩$ of the models. As $T$ is extensible, consider a model $M^{+}$ extending $M$ with a new root $r$ such that $M^{+} ⊩ T$ . By persistence, $r ⊮ σ A_{j}$ for all $j = 1, \dots, n + 2$ . Hence, $r ⊩ σ A_{i} \to σ B_{i}$ for all $i = 1, \dots, n$ , but $r ⊮ σ A_{n + 1} \lor σ A_{n + 2}$ . Hence, $T ⊬ ⋀_{i = 1}^{n} (σ A_{i} \to σ B_{i}) \to (A_{n + 1} \lor σ A_{n + 2})$ .

We may conclude that the rule $V_{n}^{'}$ is admissible in $T$ .

The following theorem is a direct consequence of corollary 4.5, lemma 4.7 and theorem 2.13.

Theorem 4.8.

Let $T$ be a subclassical recursively enumerable set theory. If $T$ is extensible, then the admissible rules of $T$ are exactly those of $IPC$ , i.e. $\sim_{T} = \sim_{IPC}$ .

Finally, the following corollary is immediate from theorem 4.4.

Corollary 4.9.

Let $T$ be a subclassical recursively enumerable extensible set theory, and $φ$ be a sentence in the language of set theory. If $φ$ is $T$ -extensible, then $L (T + φ) = IPC$ .

In conclusion, the axiom of choice (AC) is not $IZ F_{R}$ extensible.

Question 4.10.

Is the axiom of choice $C Z F$ extensible?

(b) Extensible set theories

In this section, we assume the existence of a proper class of inaccessible cardinals (see remark 4.17). We will prove the extension property for a variety of constructive set theories by providing one particular construction for extending a given model. This construction is an adaptation of Passmann’s [15] blended models. A Kripke model for set theory is a first-order Kripke model of the form $(K, \leq, {D_{v}}_{v \in K}, {f_{v w}}_{v \leq w \in K} and {E_{v}}_{v \in K})$ , where ${D_{v}}_{v \in K}$ is a collections of domains, ${f_{v w}}_{v \leq w \in K}$ is a collection of transition functions between domains, and ${E_{v}}_{v \in K}$ is a collection of interpretations of the ‘ $\in$ ’-predicate. Note that the $D_{v}$ are assumed to be sets. Of course, the transition functions and interpretations satisfy the usual coherence conditions (for more details see, e.g. [17]).

Definition 4.11.

Let $M = (K, \leq, {D_{v}}_{v \in K}, {f_{v w}}_{v \leq w \in K}, {E_{v}}_{v \in K})$ be a Kripke model of set theory. The extended model $M^{+} = (K^{+}, \leq, {D_{v}}_{v \in K^{+}}, {f_{v w}}_{v \leq w \in K^{+}}, {E_{v}}_{v \in K^{+}})$ is defined as follows:

(i)

Let $r \notin K$ , the so-called new root. Then extend $K$ and $\leq$ as follows:

K^{+} = K \cup {r} and r \leq v for all v \in K^{+} .

(ii)

The domains $D_{v}$ for $v \in K$ are already given. The domain $D_{r}$ at the new root is defined inductively as follows:

(i)

$D_{r}^{0} = \emptyset$ ,

(ii)

$D_{r}^{α}$ consists of functions $x$ with $dom (x) = K^{+}$ such that:

(i)	$x (r) \subseteq ⋃_{β < α} D_{r}^{β}$ ,
(ii)	$x (v) \in D_{v}$ for all $v \in K$ ,
(iii)	if $y \in x (r)$ , then $y (v) E_{v} x (v)$ for all $v \in K$ ,
(iv)	if $v, w \in K$ with $v \leq w$ , then $x (w) = f_{v w} (x (v))$ .

(iii)

$D_{r} = ⋃_{α \in κ} D_{r}^{α}$ , where $κ$ is the least inaccessible cardinal $κ > | K | + \sum_{v \in K} | D_{v} |$ .

(iii)

The membership relation $E_{v}$ at $v \in K$ are already defined; at the new root $r$ , define by $y E_{r} x$ if and only if $y \in x (r)$

(iv)

The transition functions $f_{v w} : D_{v} \to D_{w}$ are already defined for $v, w \in K$ with $v \leq w$ . Given $v \in K$ , define $f_{r v} : D_{r} \to D_{v}$ by $f_{r v} (x) = x (v)$ .

To help the reader digest this construction, we will give a simple example and provide some general intuition for the construction. Let $M$ be any classical model for set theory. In other words, $M$ is a one-point Kripke model; call its single point $v$ . The extended model $M^{+}$ has then a new root $r$ . An element of the root $D_{r}$ —a set at the root—is a function $x$ with domain ${r, v}$ such that $x (r) \in D_{r}$ and $x (v) \in D_{v}$ . Moreover, if $y \in x (r)$ , then $y (v) \in x (v)$ . Intuitively, a set $x$ at node $r$ may thus already contain some elements at the root $r$ but may also collect new elements when transitioning to $v$ . Another way to think of this construction idea is as adding a new root whose elements are approximations of the sets already existing in the model we are starting from.

The next step is to observe that many set-theoretical axioms are extensible. For convenience, we abbreviate the axioms of extensionality, empty set, pairing and union with $E x t$ , $E m p$ , $P a i r$ and $U n$ , respectively.

Theorem 4.12.

The following axioms and axiom schemes are $E x t$ -extensible: extensionality, empty set, pairing, union, $\in$ -induction, separation and $Δ_{0}$ -separation, power set, replacement and exponentiation. Moreover, the axiom of strong infinity is ${E x t, E m p, P a i r, U n}$ -extensible.

Proof.

We will prove all statements of the theorem by assuming that a model $M$ satisfies the relevant axiom or scheme and then show that the extended model $M^{+}$ satisfies them as well.

For extensionality, let $x, y \in D_{r}$ . For the non-trivial direction, assume that $r ⊩ \forall z (z \in x \leftrightarrow z \in y)$ . By persistence and extensionality in $M$ , we have $v ⊩ x = y$ for every $v \in M$ ; hence, $x (v) = y (v)$ for all $v \in M$ . To see that also $x (r) = y (r)$ , observe that $z \in x (r)$ if and only if $z E_{r} x (r)$ . By assumption, the latter is equivalent to $z E_{r} y (r)$ , which holds if and only if $z \in y (r)$ . In conclusion, $y (r) = x (r)$ .

For the empty set axiom, let $e_{v}$ be the unique (by extensionality) witness for the empty set axiom at $v \in K$ . Define a function $e$ with domain $K^{+}$ such that $e (v) = e_{v}$ for $e \in K$ and $e (r) = \emptyset$ ; by uniqueness, $e$ is defined, and it follows that $e \in D_{r}$ . To see that $e$ witnesses the empty set axiom, let $x \in D_{r}$ . We have to show that $r ⊩ \neg x \in e$ . For this, it suffices to show that for all $v \geq r$ , $v ⊮ x \in e$ , but this is trivially true as $e (r)$ is empty and $e_{v}$ is the empty set for all $v \in K$ .

For the pairing axiom, let $x$ , $y \in D_{r}$ . By pairing and extensionality in $M$ , there is a unique $p_{v} \in D_{v}$ such that $v ⊩ \forall z (z \in p_{v} \leftrightarrow z = x (v) \lor z = y (v))$ for all $v \in K$ . Define $p$ to be the function with domain $K^{+}$ such that $p (r) = {x, y}$ and $p (v) = p_{v}$ for all $v \in K$ . Clearly, $p \in D_{r}$ is defined by uniqueness of the $p_{v}$ . To see that $p$ indeed witnesses the pairing axiom, observe that, clearly, $r ⊩ x \in p$ and $r ⊩ y \in p$ . Moreover, if $r ⊩ z \in p$ , then it follows by definition of $p$ that $r ⊩ z = x \lor z = y$ .

For the union axiom, let $x \in D_{r}$ . As mentioned earlier, by extensionality and the union axiom in $M$ , we can find a unique witness $u_{v}$ such that $v ⊩ u_{v} = ⋃ x (v)$ for every $v \in K$ . Then define a function $u$ with domain $K^{+}$ such that $u (v) = u_{v}$ for all $v \in K$ and $u (r) = ⋃ {y (r) | y \in x (r)}$ . To verify that indeed $u \in D_{r}$ , note that $y \in u (r)$ implies that there is some $z \in x (r)$ such that $y \in z (r)$ . Now by $y, z \in D_{r}$ , we know that $v ⊩ y (v) \in z (v) \land z (v) \in x (v)$ , so, clearly, $v ⊩ y (v) \in u (v)$ . It is now a straightforward computation to see that $u$ witnesses the union axiom at $r$ .

Regarding $\in$ -induction, suppose for contradiction that $r ⊮ \forall x (\forall y \in x φ (y) \to φ (x)) \to \forall x φ (x)$ . Then there is some $v \geq r$ such that $v ⊩ \forall x (\forall y \in x φ (y) \to φ (x))$ but $v ⊮ \forall x φ (x)$ . As $M$ satisfies $\in$ -induction, it must be that $v = r$ , and so by persistence $M^{+} ⊩ \forall x (\forall y \in x φ (y) \to φ (x))$ . By $\in$ -induction in $M$ , $M ⊩ \forall x φ (x)$ , so all failures of this instance of $\in$ -induction must happen at the new root $r$ . Thus, as $r ⊮ \forall x φ (x)$ , it follows that there is some $x_{0} \in D_{r}$ such that $r ⊮ φ (x_{0})$ . Using the antecedent of $\in$ -induction, this means that there must be some $x_{1} \in D_{r}$ such that $r ⊩ x_{1} \in x_{0}$ and $r ⊮ φ (x_{1})$ . Iterating this construction, we obtain a sequence ${x_{n}}_{n \in ω}$ such that $x_{n + 1} \in x_{n} (r)$ . This straightforwardly gives rise to an infinitely decreasing $\in$ -chain. A contradiction.

Next, we consider the separation axiom. Let $x \in D_{r}$ and $φ (y)$ be a formula, possibly with parameters. Now, for every $v \in K$ , let $s_{v}$ be the unique result of separating from $x (v)$ with $φ$ and parameters $\bar{p} (v)$ at node $v$ . With persistence and extensionality, it follows that the function $s$ with domain $K^{+}$ such that $s (v) = s_{v}$ and $s (r) = {y \in x (r) | r ⊩ φ (y, \bar{p})}$ is a well-defined element of $D_{r}$ ; if $α$ is the least such that $x \in D_{r}^{α}$ , then it is easy to see that $x \in D_{r}^{α + 1}$ . It follows straightforwardly from the definition of $s$ that it witnesses separation from $x$ with $φ$ at $r$ : $r ⊩ z \in s$ is equivalent to $z \in s (r)$ , and the latter holds by definition if and only if $r ⊩ φ (z, \bar{p})$ . Note that the proof of $Δ_{0}$ -separation schema is a special case of the proof for the separation schema.

For the power set axiom, consider $x \in D_{r}$ and let $β < κ$ such that $x \in D_{r}^{β}$ . If $y \in D_{r}$ such that $r ⊩ y \subseteq x$ , then $y (r) \subseteq x (r),$ and hence, $y \in D_{r}^{β}$ as well. Let $p (r)$ consist of those $y \in D_{r}$ such that $r ⊩ \forall z (z \in y \to z \in x)$ , then $p (r) \subseteq D_{r}^{β}$ . Moreover, let $p (v)$ be the unique element of $D_{v}$ such that $v ⊩ p (v) = P (x (v))$ (using extensionality). By persistence, $p$ is a well-defined element of $D_{r}$ . It is then straightforward to check that $p$ is the power set of $x$ at $r$ .

For replacement, let $x \in D_{r}$ and $φ$ be a formula (potentially with parameters) such that $r ⊩ \forall y \in x \exists! z φ (y, z)$ . Given this, let $a (r)$ consist of those $z \in D_{r}$ for which there exists some $y \in D_{r}$ with $r ⊩ φ (y, z)$ . Moreover, let $a (v)$ be the witness for applying replacement with $φ$ on $x (v)$ at $v$ . By inaccessibility of $κ$ and persistence in $M^{+}$ , it follows that $a \in D_{r}$ . As in the previous cases, it is now straightforward to check that $a$ witnesses replacement.

For exponentiation, let $a, b \in D_{r}$ . Let $z (r)$ be the set of functions from $a$ to $b$ at $r$ , and let $z (v)$ be the set of functions from $a (v)$ to $b (v)$ at the node $v$ . It follows that $z \in D_{r}$ , and it is easy to check that $z$ witnesses the exponentiation axiom.

Recall that the axiom of strong infinity asserts the existence of a least inductive set. So, for every $v \in K$ , let $ω_{v} \in D_{v}$ be this least inductive set. At the new root $r$ , we recursively construct sets $n_{r}$ as follows: Let $0_{r}$ be the empty set as defined from the empty set axiom. Then, given $n_{r}$ , use pairing and union, to obtain $(n + 1)_{r}$ such that $r ⊩ (n + 1)_{r} = n_{r} \cup {n_{r}}$ . As each $ω_{v}$ is the least inductive set at $v$ , it must be the case that $v ⊩ n_{r} (v) \in ω_{v}$ for all $v \in K$ . Therefore, the set $x$ , defined by $x (r) = {n_{r} | n \in ω}$ and $x (v) = ω_{v}$ for $v \in K$ , is a well-defined set at $r$ , i.e. $x \in D_{r}$ . By construction, we must have that if $r ⊩ ‘ y {is inductive}^{'}$ , then $r ⊩ x \subseteq y$ . Hence, $x$ witnesses strong infinity.

A combination of theorem 4.12 and lemmas 4.2 and 4.3 yields the next corollary. An application of theorem 4.8 then yields corollary 4.14.

Corollary 4.13.

The theories $IZ F_{R}$ , $C Z F_{E R}$ , $E C S T$ and $B C S T$ are extensible.

Corollary 4.14.

The propositional admissible rules of $IZ F_{R}$ , $C Z F_{E R}$ , $E C S T$ and $B C S T$ are exactly those of $IPC$ . In other words, if $T$ is one of these theories, then $\sim_{T} = \sim_{IPC}$ .

Remark 4.15.

It seems difficult to use the aforementioned method to prove that the axiom schemes of collection, strong collection and subset collection are extensible. The reason for this is that these axiom schemes do not require that their witnesses are unique—this is in contrast to their weakened versions, replacement and exponentiation.

Question 4.16.

Are the axiom schemes of collection, strong collection and subset collection extensible?

Remark 4.17.

It is not strictly necessary to assume the existence of a proper class of inaccessible cardinals as (at least) the following two alternatives are available: Firstly, we could work with Kripke models that have (definable) class domains. Secondly, we could apply the downwards Löwenheim–Skolem theorem (which does hold in our classical metatheory) to work, without loss of generality, only with models with countable domains. In our view, the solution with inaccessible cardinals is the most elegant as it allows us to ignore any worries about size restrictions.

5. Questions

We close with a few suggestions for future research.

Question 5.1.

Is it the case that $\sim_{HA} = \sim_{I Z F}$ ?

In general, one can ask the same question for any two constructive theories $T$ , $T^{'}$ of interest.

Question 5.2.

Are $C Z F$ and $I Z F$ extensible?

Question 5.3.

Of course, both $I Z F$ and $C Z F$ can be extended with further axioms. Natural examples of such further axioms include the so-called large set axioms—the constructive counterparts to large cardinal axioms. What are the propositional and first-order logics of extensions of $I Z F$ and $C Z F$ with further axioms? Also, what are their admissible rules?

Question 5.4.

In this article, we gave a first structural analysis of the logical structure by observing the consequences of the extension property. Are there other structural properties of set theories that determine (parts of) the logical structure of a given set theory?

Question 5.5.

Let $T$ be a theory. Given a class $Γ$ of set-theoretic formulas, we can obtain the notions of $Γ$ -propositional logic $L (T)$ and $Γ$ -first-order logic $QL (T)$ , as well as $Γ$ -admissible rules by restricting to those $T$ -substitutions that arise from $T$ -assignments with domain in $Γ$ . Natural classes to consider are, of course, the classes of the Lévy hierarchy but other cases are thinkable (such as prenex formulas). What are the logics that arise in this way?

Note, regarding the previous question, that the substitutions used to prove the results in §3 are usually of rather low complexity, e.g. $Σ_{3}$ or $Σ_{4}$ . Therefore, the question is often only interesting for classes of lower complexity. For instance, Visser [4, sections 3.7–3.9] considers $Σ_{1}$ -substitutions.

In this article, we have only considered set theories on the basis of intuitionistic logic. Of course, one can also analyse the logical structure of set theories based on other logics. Löwe et al. [24] take some first steps towards an analysis of the logical structure of certain paraconsistent set theories. Another related problem is to determine the provability logics of constructive and intuitionistic set theories.

6. The classical case

In this final section, we briefly discuss the logical structure of classical theories. Recall that a logic is post-complete if it has no consistent extension.

Theorem 6.1.

Let $T$ be a classical theory. If $T$ is consistent, then $T$ satisfies the de Jongh property for $CPC$ .

Proof.

Since $T$ is classical, it must be that $CPC \subseteq L (T)$ . As $T$ is consistent, $⊥ \notin L (T)$ . Hence, $L (T) = CPC$ as $CPC$ is post-complete.

The case for first-order logics of a given theory is more complicated as they are not post-complete; Yavorsky [25] proved that expressively strong arithmetical theories $T$ , such as $P A$ , satisfy $QL (T) = CQC$ (see Yavorsky’s paper for definitions and details). Yavorsky also shows that there are classical theories $T$ such that $CQC ⊊ QL (T)$ .

Theorem 6.2.

Let $T$ be a classical theory. Then $A \sim_{T} B$ if and only if $A \sim_{L (T)} B$ . Thus, $\sim_{T} = \sim_{L (T)} = ⊢_{CPC}$ .

Proof.

Theorem 6.1 implies that $L (T) = CPC$ . As is well known, $\sim_{CPC} = ⊢_{CPC}$ (a proof can be found in [26]). Thus, the second part of the theorem follows from the first.

For the first part, the direction from left to right has been proven in theorem 2.11. We treat the other direction. Arguing by contraposition, assume for some propositional formulas $A$ and $B$ that $⊢_{T} ρ (A)$ and $⊬_{T} ρ (B)$ for some substitution $ρ$ from the language of propositional logic to the language of $T$ . We have to show that $A ≁_{L (T)} B$ . Assumption $⊬ ρ (B)$ implies that there exists a propositional model $M$ of $T$ and a valuation $v$ such that $M, v ⊭ ρ (B)$ . Define a substitution $σ$ in propositional logic as follows:

σ (p) = {\begin{cases} ⊤ & if M, v ⊨ ρ (p), \\ ⊥ & if M, v ⊭ ρ (p) . \end{cases}

It is easy to see that for any propositional formula

C

, the formula

σ C

contains no propositional variables, which implies that

σ C

is equivalent to

⊤

or to

⊥

. Therefore,

⊢_{L (T)} σ (C) or ⊢_{L (T)} \neg σ (C) .

6.1

By using (6.1), it is easy to prove by induction on the propositional formula

C

that

⊢_{L (T)} σ (C) ⟺ M, v ⊨ ρ (C) .

6.2

Now, since

M ⊭ ρ (B)

, it follows that

⊬_{L (T)} σ (B)

from (6.2). On the other hand, since

⊢_{T} ρ (A)

, we must have that

M ⊨ ρ (A)

, thus (6.2) implies that

⊢_{L (T)} σ (A)

. Therefore,

A ≁_{L (T)} B

, which is what we had to show.

In the remainder of this section, we show that the first part of theorem 6.2 can be lifted to the predicate case, at least for theories for which $QL (T) = CQC$ , and the second part cannot. The predicate version of the first part of the previous theorem states that $\sim_{T} = \sim_{CQC}$ and the second part states that $\sim_{CQC} = ⊢_{CQC}$ . To show that the first statement is true for theories $T$ such that $QL (T) = CQC$ , we first have to prove that the second statement, while not true, is almost true; we have to show that $CQC$ is almost structurally complete.

As remarked earlier, $CPC$ is structurally complete, which means that any admissible rule is derivable: for all propositional formulas $A$ and $B$

A \sim_{CPC} B \Rightarrow A ⊢_{CPC} B .

6.3

In other words,

\sim_{CPC} = ⊢_{CPC}

(see also Iemhoff [26]).

It is easy to see that, unlike $CPC$ , $CQC$ is not structurally complete. Consider the formula $\exists x P (x) \land \exists x \neg P (x)$ and observe that for no substitution $σ$ , the formula $σ (\exists x P (x) \land \exists x \neg P (x))$ is derivable in $CQC$ . For if it were, it would hold in models consisting of one element, quod non. This implies that $\exists x P (x) \land \exists x \neg P (x) \sim_{CQC} ⊥$ . And since $\exists x P (x) \land \exists x \neg P (x) ⊬_{CQC} ⊥$ , this shows that $CQC$ is not structurally complete, i.e. that $\sim_{CQC} \neq ⊢_{CQC}$ . However, the admissible rule $\exists x P (x) \land \exists x \neg P (x) \sim_{CQC} ⊥$ has a particular property, it is passive.

Definition 6.3.

Admissible rules $A \sim_{T} B$ are called passive if the premise $A$ is not unifiable, i.e. $⊢_{T} σ (A)$ for no substitution $σ$ .

We will show that the only non-derivable admissible rules in $CQC$ are passive. In the terminology of admissibility: $CQC$ is almost structural complete. This result was first obtained by Pogorzelski and Prucnal [27]. Here, we prove a modest generalization that applies to a class of consequence relations instead of a single one. Recall that a rule $A / B$ is derivable in $CQC$ if $A ⊢ B$ , where $⊢$ is a consequence relation of $CQC$ , by which we mean a consequence relation that has the same theorems as $CQC$ : $⊢ A$ iff $A$ holds in $CQC$ . Thus, strictly speaking, the notion of derivable rule depends on the given consequence relation of $CQC$ , which is why we make it explicit in the discussion below. Since the derivability of a formula does not depend on the consequence relation (because all have the same derivable formulas), we can leave it implicit in such a setting, as in the next lemma, where $⊢_{CQC}$ denotes any consequence relation for $CQC$ .

Lemma 6.4.

A formula $A$ is unifiable if and only if there exists a ground substitution $τ$ such that $⊢_{CQC} τ (A)$ and $τ (P (\bar{s})) = τ (P (\bar{t}))$ for all predicates $P$ and sequences of terms $\bar{s}, \bar{t}$ .

Proof.

It suffices to show the direction from left to right. Since $A (\bar{x})$ is unifiable, there exists a substitution $σ$ such that $⊢_{CQC} σ (A)$ , from which it follows that $⊢_{CQC} ρ σ (A)$ for any ground substitution $ρ$ , as $CQC$ is closed under uniform substitution. Clearly, $ρ σ$ is a ground substitution too. That $ρ σ$ satisfies the second part of the lemma follows immediately from the definition of substitutions.

Theorem 6.5.

Let $⊢_{CQC}$ be a consequence relation for $CQC$ such that $C (\bar{x}) ⊢_{CQC} \forall \bar{x} C (\bar{x})$ for all formulas $C$ . Then $A \sim_{CQC} B$ implies $A ⊢_{CQC} B$ for all unifiable formulas $A$ and all formulas $B$ .

Proof.

Since $A$ is unifiable, there exists, by lemma 6.4, a ground substitution $τ$ such that $⊢ τ (A)$ and $τ (P (\bar{s})) = τ (P (\bar{t}))$ for all predicates $P$ and sequences of terms $\bar{s}, \bar{t}$ . Firstly, note that this implies that $τ (B (\bar{s})) = τ (B (\bar{t}))$ for any formula $B$ . Let $\bar{x}$ be the free variables in $A$ and define a substitution $σ$ as follows:

σ (P \bar{z}) = {\begin{cases} \forall \bar{x} A \to P (\bar{z}) & if ⊢ τ P (\bar{z}) \leftrightarrow ⊤, \\ \forall \bar{x} A \land P (\bar{z}) & if ⊢ τ P (\bar{z}) \leftrightarrow ⊥ . \end{cases}

Claim

For any formula $B$ , we have that

⊢ σ (B) \leftrightarrow {\begin{cases} \forall \bar{x} A \to B & if ⊢ τ B \leftrightarrow ⊤, \\ \forall \bar{x} A \land B & if ⊢ τ B \leftrightarrow ⊥ . \end{cases}

Proof of the Claim.

By induction on $B$ .

Case $B = P \bar{z}$ . Trivial. Case $B = C \land D$ . If $⊢ τ (C \land D) \leftrightarrow ⊤$ , then as $τ$ commutes with connectives, we must have that $⊢ τ C \leftrightarrow ⊤$ and $⊢ τ D \leftrightarrow ⊤$ , which by the induction hypothesis imply that

⊢ σ C \leftrightarrow (\forall \bar{x} A \to C) and ⊢ σ D \leftrightarrow (\forall \bar{x} A \to D) .

Thus,

σ (C \land D) ⊣⊢ (\forall \bar{x} A \to C) \land (\forall \bar{x} A \to D) ⊣⊢ \forall \bar{x} A \to (C \land D)

If $⊢ τ (C \land D) \leftrightarrow ⊥$ , then there are three cases.

Case 1.

$⊢ τ C \leftrightarrow ⊥$ and $⊢ τ D \leftrightarrow ⊥$ . By induction hypothesis, $⊢ σ C \leftrightarrow (\forall \bar{x} A \land C)$ and $⊢ σ D \leftrightarrow (\forall \bar{x} A \land D)$ . Thus, $⊢ σ (C \land D) \leftrightarrow (\forall \bar{x} A \land (C \land D))$ .

Case 2.

$⊢ τ C \leftrightarrow ⊥$ and $⊢ τ D \leftrightarrow ⊤$ . By induction hypothesis, $⊢ σ C \leftrightarrow (\forall \bar{x} A \land C)$ and $⊢ σ D \leftrightarrow (\forall \bar{x} A \to D)$ . Thus, we have that

σ C \land σ D ⊣ ⊢ (\forall \bar{x} A \land C) \land (\forall \bar{x} A \to D) ⊣ ⊢ \forall \bar{x} A \land (C \land D) .

Case 3.

$⊢ τ C \leftrightarrow ⊤$ and $⊢ τ D \leftrightarrow ⊥$ , analogous to case 2.

Case $B = \neg C$ . If $⊢ τ (\neg C) \leftrightarrow ⊤$ , then since $τ$ commutes with the connectives, we must have that $⊢ τ C \leftrightarrow ⊥$ , which by induction hypothesis implies that $σ C ⊣⊢ \forall \bar{x} A \land C$ . Thus,

σ (\neg C) ⊣ ⊢ \neg (\forall \bar{x} A \land C) ⊣ ⊢ \forall \bar{x} A \to \neg C .

⊢ τ (\neg C) \leftrightarrow ⊥

, then

⊢ τ C \leftrightarrow ⊤

since

τ

commutes with the connectives, which by induction hypothesis implies that

σ C ⊣⊢ \forall \bar{x} A \to C

. Thus,

σ (\neg C) ⊣ ⊢ \neg (\forall \bar{x} A \to C) ⊣ ⊢ \forall \bar{x} A \land \neg C .

Case

B = \forall \bar{w} C (\bar{w})

. If

⊢ τ (\forall \bar{w} C (\bar{w})) \leftrightarrow ⊤

, then

⊢ \forall \bar{w} τ (C (\bar{w})) \leftrightarrow ⊤

follows. Hence,

⊢ τ C (\bar{w}) \leftrightarrow ⊤

, which by induction hypothesis implies that

σ C (\bar{w}) ⊣⊢ \forall \bar{x} A \to C (\bar{w})

. Thus,

σ (\forall \bar{w} C (\bar{w})) ⊣ ⊢ \forall \bar{w} σ C (\bar{w}) ⊣ ⊢ \forall \bar{w} (\forall \bar{x} A (\bar{x}) \to C (\bar{w})) ⊣ ⊢ \forall \bar{x} A (\bar{x}) \to \forall \bar{w} C (\bar{w}) .

⊢ τ (\forall \bar{w} C (\bar{w})) \leftrightarrow ⊥

, then the fact that

τ

is a substitution implies that

⊢ τ (\forall \bar{w} C (\bar{w})) \leftrightarrow \forall \bar{w} τ (C (\bar{w}))

, and that it is a ground substitution that

⊢ τ C (\bar{w}) \leftrightarrow ⊥

for some

\bar{w}

. By the observation made in the first paragraph of the proof,

τ C (\bar{w})

is equivalent to

τ C (\bar{s})

for any sequence of terms

\bar{s}

. Thus,

σ C (\bar{w}) ⊣⊢ \forall \bar{x} A \land C (\bar{w})

by the induction hypothesis, which implies

σ (\forall \bar{w} C (\bar{w})) ⊣ ⊢ \forall \bar{w} (\forall \bar{x} A (\bar{x}) \land C (\bar{w})) ⊣ ⊢ \forall \bar{x} A (\bar{x}) \land \forall \bar{w} C (\bar{w}) .

This proves the claim.

Now, since $⊢ τ A \leftrightarrow ⊤$ , we know by the claim that $⊢ σ A (\bar{x}) \leftrightarrow (\forall \bar{x} A (\bar{x}) \to A)$ . But $⊢ \forall \bar{x} A (\bar{x}) \to A$ , thus $⊢ σ A$ . Since $A \sim_{CQC} B$ , we have that $⊢ σ B$ .

By the claim, it is easy to see that $\forall \bar{x} A (\bar{x}) ⊢ σ B \leftrightarrow B$ . By assumption $A ⊢_{CQC} \forall \bar{x} A (\bar{x})$ , we obtain that $A ⊢ B$ .

Corollary 6.7.

$CQC$ is almost structurally complete with respect to any consequence relation that satisfies the constraint in theorem 6.5.

Corollary 6.8.

For any classical theory $T$ such that $QL (T) = CQC$ : $A \sim_{T} B$ if and only if $A \sim_{CQC} B$ , i.e. $\sim_{T} = \sim_{CQC}$ .

Proof.

The assumption $QL (T) = CQC$ gives $A \sim_{T} B$ implies $A \sim_{CQC} B$ by theorem 2.11. For the other direction, assume that $A \sim_{CQC} B$ . If $A$ is unifiable in $CQC$ , then $A ⊢_{CQC} B$ by theorem 6.5. Hence, $A ⊢_{T} B$ and thus $A \sim_{T} B$ . If $A$ is not unifiable in $CQC$ , then it suffices to show that $A$ is not unifiable in $T$ . For this implies that $A \sim_{T} C$ for any $C$ , and thus, $A \sim_{T} B$ would follow. Arguing by contradiction, suppose $A$ is unifiable in $T$ , say $⊢_{T} σ A$ for some substitution $σ$ . Then for any ground substitution $τ$ , $⊢_{T} τ σ A$ , and as $QL (T) = CQC$ , this implies $⊢_{CQC} τ σ A$ , contradicting the assumption that $A$ is not unifiable in $CQC$ .

Data accessibility

This article has no additional data.

Authors' contributions

R.I.: funding acquisition, investigation, methodology, writing—original draft and writing—review and editing; R.P.: funding acquisition, investigation, methodology, project administration, writing—original draft and writing—review and editing.

Both authors gave final approval for publication and agreed to be held accountable for the work performed therein.

Conflict of interest declaration

We declare we have no competing interests.

Funding

The first author gratefully acknowledges support by the Netherlands Organisation for Scientific Research (grant no. 639.073.807) and by the MOSAIC project (EU H2020-MSCA-RISE-2020 Project no. 101007627). The research of the second author was partially funded by a doctoral scholarship of the Studienstiftung des deutschen Volkes (German Academic Scholarship Foundation).

Acknowledgements

We would like to thank two anonymous reviewers for their very helpful comments.

Footnotes

One contribution of 11 to a theme issue ‘Modern perspectives in Proof Theory’.

Published by the Royal Society under the terms of the Creative Commons Attribution License http://creativecommons.org/licenses/by/4.0/, which permits unrestricted use, provided the original author and source are credited.

VIEW FULL TEXT DOWNLOAD PDF

This Issue

Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences cover image

29 May 2023

Volume 381Issue 2248

Theme issue ‘Modern perspectives in Proof Theory’ compiled and edited by J. P. Aguilera, F. Pakhomov, A. Weiermann

Article Information

DOI:https://doi.org/10.1098/rsta.2022.0018
PubMed:37031696
Published by:Royal Society
Print ISSN:1364-503X
Online ISSN:1471-2962

History:

Manuscript received25/07/2022
Manuscript accepted02/12/2022
Published online10/04/2023
Published in print29/05/2023

License:

Citations and impact

Keywords

Subjects

Your password must have 8 characters or more and contain 3 of the following:

Logics and admissible rules of constructive set theories

Abstract

1. Introduction

(a) Overview

2. Preliminaries: the logical structure of a theory

Definition 2.1.

Definition 2.2.

Definition 2.3.

Definition 2.4.

Proposition 2.5.

Proof.

Definition 2.6.

Theorem 2.7. (Visser [4])

Proof.

Definition 2.8.

Proposition 2.9.

Proposition 2.10.

Theorem 2.11. (Visser [4])

Theorem 2.12. Visser ([4], Lemma 4.1)

Theorem 2.13.

Proof.

3. Survey on techniques and results

(a) Constructive set theories

Definition 3.1.

(b) Techniques and results

Theorem 3.2. (Diaconescu [1]; Goodman & Myhill [2])

Theorem 3.3. (Friedman & Ščedrov [13])

Question 3.4.

Theorem 3.5. (Passmann [15])

Theorem 3.6. (Iemhoff & Passmann [17])

Theorem 3.7. (Iemhoff & Passmann [17])

Theorem 3.8. (Iemhoff & Passmann [17], theorem 61)

Question 3.9.

Theorem 3.10. (Carl et al. [21])

Theorem 3.11. (Passmann [14])

Theorem 3.12. (Passmann [14])

Question 3.13.

Question 3.14.

4. Logics and rules of set theories

(a) Logic, rules and the extension property

Definition 4.1.

Lemma 4.2.

Proof.

Lemma 4.3.

Proof.

Theorem 4.4.

Proof.

Corollary 4.5.

Lemma 4.6.

Proof.

Lemma 4.7.

Proof.

Theorem 4.8.

Corollary 4.9.

Question 4.10.

(b) Extensible set theories

Definition 4.11.

Theorem 4.12.

Proof.

Corollary 4.13.

Corollary 4.14.

Remark 4.15.

Question 4.16.

Remark 4.17.

5. Questions

Question 5.1.

Question 5.2.

Question 5.3.

Question 5.4.

Question 5.5.

6. The classical case

Theorem 6.1.

Proof.

Theorem 6.2.

Proof.

Definition 6.3.

Lemma 6.4.

Proof.

Theorem 6.5.