POUR-EL’S LANDSCAPE

Abstract

We study the effective versions of several notions related to incompleteness, undecidability, and inseparability along the lines of Pour-El’s insights. Firstly, we strengthen Pour-El’s theorem on the equivalence between effective essential incompleteness and effective inseparability. Secondly, we compare the notions obtained by restricting that of effective essential incompleteness to intensional finite extensions and extensional finite extensions. Finally, we study the combination of effectiveness and hereditariness, and prove an adapted version of Pour-El’s result for this combination.

1 Introduction

Reflection on the meaning of incompleteness and undecidability results gave rise to notions like essential undecidability of theories and computable inseparability of theories: a consistent c.e. theory U is essentially undecidable iff all its consistent extensions V (in the same language) are undecidable, and a consistent c.e. theory U is computably inseparable iff its theorems and its refutable sentences are computably inseparable. We note that these notions have different flavours: essential undecidability looks at the relation of the given theory with other theories and computable inseparability looks at the relation of the theory with c.e. sets.

Such notions were studied in the period 1950–1970 (see, e.g., [16, 18]). Their various relations and non-relations were established. See the schema at the end of Section 2.4.

Marian Boykan Pour-El, in her ground-breaking paper [1], made an interesting discovery. Where there are examples of essentially incomplete theories that are not computably inseparable, the effective versions of these notions coincide. The present paper is a study of results along the lines of Pour-El’s insight. We study effective versions of notions connected to incompleteness and undecidability and establish their interrelationships. See the schema at the end of Section 5 for an overview of our results.

In the usual statements of incompleteness results, there is often a restriction to some specific formula class. For example: for all c.e. extensions U of the Tarski–Mostowski–Robinson theory R, we can effectively find a $\Sigma ^0_1$ -sentence $\sigma $ that is independent of U from an index of U. The Pour-El style results in this paper will reflect the possibility of such restrictions: we will add a parameter for the formula class from which the witnesses of, e.g., incompleteness or creativity may be chosen.

Effective versions of incompleteness and undecidability results have unavoidably an intensional component. For example, a theory U is effectively essentially incomplete iff there is a partial computable function $\varPhi $ such that, for all indices i, if the c.e. set $\mathsf {W}_i$ is a consistent extension of U, then $\varPhi (i)$ converges to a sentence that is independent of $\mathsf {W}_i$ . We see that the function that provides the independent sentences operates on presentations rather than directly on the extensions of the given theory itself. Thus, our paper is as much a study of the consequences of intensionality as it is of effectiveness. In the case of finite extensions, we can operate more extensionally, since we can consider these as given not by an index but rather by a sentence. This fact enables us, in the special case of finite extensions, to compare the intensional and the extensional. In Section 4, we study the extensional finite case.

1.1 Overview of the paper

In Section 2, we introduce the basic notions. We present an analysis of what the effectivisation of a notion is in Section 2.5. Section 3 gives our presentation and extension of Pour-El’s work. Then, in Section 4, we study the extensional case for finite extensions. Section 5 is concerned with the combination of effectiveness and hereditariness. Among other things, we prove that for any consistent c.e. theory, effective essential hereditary creativity and strong effective inseparability are equivalent. The section is a sequel to the paper [28], where the non-effective case of hereditariness is studied.

Apart from reading the paper from A to Z, there are several other paths the reader may beneficially follow. Section 2 is more or less obligatory in order to understand the rest, but, e.g., Section 2.2 can be read lightly to return to when the relevant notions are needed. Of Section 3, the presentation of Pour-El’s original result in Section 3.1 should not be skipped, but the reader could cherry-pick from the rest. Then, the reader can choose between Section 4 and Section 5.

2 Notions and basic facts

In this section, we introduce the various notions that we employ in this paper and present some basic facts.

2.1 Theories

A theory is given as a set of axioms in a given signature. We take the signature to be part of the data of the theory. Note that we do not take a formula representing the axiom set or an index of the axiom set as part of the data. The same theory can have different enumerations. Moreover, these enumerations are enumerations of the axiom set and not of the theorems.

We write $U_{{\mathfrak {p}}}$ for the set of theorems of U and $U_{{\mathfrak {r}}}$ for the U-refutable sentences or anti-theorems of U, i.e., $U_{{\mathfrak {r}}} = \{ \varphi \mid U \vdash \neg \, \varphi \}$ .

We will also consider mono-consequence: $U \vdash _{{\mathfrak {m}}} \varphi $ iff there is a $\psi \in U$ such that $\psi \vdash \varphi $ . We have the corresponding notion of mono-consistency, which was developed by Lindström (cf. [10]). We write $U_{{\mathfrak {m}}}$ for the set of mono-theorems of U and $U_{{\mathfrak {n}}}$ for the set of mono-refutable sentences.

Strictly speaking, there is no disjoint notion of mono-theory. A mono-theory is just a theory. However, sometimes we will still use the word to indicate that we intend to use the given set of sentences of the given signature with the notion of mono-consequence.

The notion of mono-theory plays a role in Theorem 2.9. Below we show the notion of mono-theory is connected to the idea of computable sequence of c.e. theories. There are heuristic differences between the notions. Sometimes it is better to think in terms of the ‘flatter’ notion of mono-theory, sometimes it is pleasant to visualise a sequence of theories.

We define $\widehat U$ as the set of all non-empty finite conjunctions of elements of U. We have the following convenient insight.

Theorem 2.1. We have: $U\vdash \varphi $ iff $\widehat U \vdash _{{\mathfrak {m}}} \varphi $ . As a consequence, $U_{{\mathfrak {p}}} = \widehat U_{{\mathfrak {m}}}$ and $U_{{\mathfrak {r}}} = \widehat U_{{\mathfrak {n}}}$ .

We note that we have $V \dashv U$ iff $V \dashv _{{\mathfrak {m}}} \widehat U$ . So, $\widehat {(\cdot )}$ is the right adjoint of the projection functor of theories (of a given signature) with $\dashv $ into theories (of the given signature) with $\dashv _{{\mathfrak {m}}}$ . We also note that, of course, $(\cdot )_{{\mathfrak {p}}}$ gives us an isomorphic functor. The advantage of $\widehat {(\cdot )}$ is the fact that it does not raise the complexity of the given set for most measures of complexity.

A computable sequence $(T_i)_{i\in \omega }$ of c.e. theories is given by a c.e. relation $\mathcal {T}(i,\varphi )$ . Here, of course, $T_i := \{ \varphi \mid \mathcal {T}(i,\varphi ) \}$ . We demand that all $T_i$ are in the same signature. We take this signature as part of the data of the sequence. A sequence of theories is consistent if each of its theories is.

Consider a computable sequence of c.e. theories, given by $\mathcal {T}(i,\varphi )$ . We define $\mathcal {T}^{{\mathfrak {m}}} := \bigcup _{i\in \omega } \widehat T_i$ . Clearly, $\mathcal {T}^{{\mathfrak {m}}}$ is a c.e. mono-theory. It is easy to see that $\mathcal {T}^{{\mathfrak {m}}} \vdash _{{\mathfrak {m}}}\varphi $ iff $T_i \vdash \varphi $ , for some i.

Conversely, given a c.e. mono-theory U we can associate a computable sequence $(T_i)_{i\in \omega }$ of c.e. theories as follows. Enumerate U in stages and, if, at stage i, a sentence $\varphi $ is enumerated, put $\varphi $ in $T_i$ . Clearly, $U \vdash _{{\mathfrak {m}}}\varphi $ iff $T_i \vdash \varphi $ , for some i.

Since metamathematical results on sequences of theories are mostly concerned with the relation $\exists i\in \omega \;T_i \vdash \varphi $ , we can usually replace sequences of theories given by $\mathcal {T}$ by mono-theories U and study $U \vdash _{{\mathfrak {m}}}\varphi $ .

2.2 Theory-extension

We may define various notions of theory-extension. The basic notion is simply $U\subseteq V$ : the V-axioms extend the U-axioms. Here the V-language may extend the U-language. We have three ‘dimensions’ of variation.

1. i. We can put restrictions on the V-language. We consider two possibilities. We use a superscript ${\mathfrak {s}}$ , for ‘same’ or for ‘signature’, to indicate that the U- and the V-language coincide. We use a superscript ${\mathfrak {c}}$ to indicate that the V-language extends the U-language by at most finitely many constants.

2. ii. We do not compare the axiom sets but appropriate closures of the axioms sets. When we compare the theorems, we indicate this by a subscript ${\mathfrak {p}}$ . We can also compare the mono-theorems. We indicate this by a subscript ${\mathfrak {m}}$ .

3. iii. We may put constraints on the cardinality of the extension. We use the subscript ${\mathfrak {f}}$ for finite extensions.

So we will use, e.g., $U\subseteq ^{{\mathfrak {s}}}_{{\mathfrak {f}}}V$ , for: V is a finite extension of U in the same language. If we use, e.g., $U\subseteq ^{{\mathfrak {s}}}_{{\mathfrak {pf}}}V$ , this is of course intended to mean that the theorems of V are theorems of a finite extension of U. We will use $U\dashv V$ for $U \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {p}}} V$ and $U\dashv _{{\mathfrak {m}}} V$ for $U \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} V$ .

We note that if $U_{{\mathfrak {p}}} = U^{\prime }_{{\mathfrak {p}}}$ and $V_{{\mathfrak {p}}} = V^{\prime }_{{\mathfrak {p}}}$ , then $U\subseteq ^{{\mathfrak {s}}}_{{\mathfrak {pf}}}V$ iff $U'\subseteq ^{{\mathfrak {s}}}_{{\mathfrak {pf}}}V'$ .

We will be looking at mono-extensions of non-mono theories. For this case the following notion of extension is a relevant one.

• • $U \Cup V := \{ \varphi \wedge \psi \mid \varphi \in U \text { and } \psi \in V \}$ .

• • $U \Subset V$ iff $U\Cup V \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} V$ .

Let $\mathcal {X}$ and $\mathcal {Y}$ be disjoint c.e. sets. Two sets $\mathcal {Z}$ and $\mathcal {W}$ weakly biseparate $\mathcal {X}$ and $\mathcal {Y}$ iff $\mathcal {X} \subseteq \mathcal {Z}$ , $\mathcal {Y} \subseteq \mathcal {W}$ , $\mathcal {Z} \cap \mathcal {Y} = \emptyset $ , and $\mathcal {W} \cap \mathcal {X} = \emptyset $ . We say that $\mathcal {Z}$ and $\mathcal {W}$ biseparate $\mathcal {X}$ and $\mathcal {Y}$ iff they weakly biseparate $\mathcal {X}$ and $\mathcal {Y}$ and $\mathcal {Z} \cap \mathcal {W} = \emptyset $ . We will not use the following theorem later, but we state it for the sake of understanding.

Theorem 2.2.

1. a. If $U \Subset V$ , then $\widehat U \subseteq ^{{\mathfrak {s}}} U_{{\mathfrak {p}}} \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} U_{{\mathfrak {p}}} \Cup V \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} V$ .

2. b. If $U \Subset V$ and V is mono-consistent, then $V_{{\mathfrak {m}}}$ and $V_{{\mathfrak {n}}}$ weakly biseparate $U_{\mathsf {p}}$ and $U_{{\mathfrak {r}}}$ .

3. c. $U\Subset U$ iff $U_{{\mathfrak {m}}} = U_{{\mathfrak {p}}}$ .

Proof (a). Suppose $U \Subset V$ . The inclusions $\widehat U \subseteq ^{{\mathfrak {s}}} U_{{\mathfrak {p}}} \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} U_{{\mathfrak {p}}} \Cup V$ are obvious. To prove $U_{{\mathfrak {p}}} \Cup V \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} V$ , it suffices to show that for any k, $\varphi _0, \ldots , \varphi _k \in U$ , and $\psi \in V$ , there exists a $\rho \in V$ such that

$$\begin{align*}\rho \vdash \varphi _0 \land \cdots \land \varphi _k \land \psi.\end{align*}$$

We prove the statement by induction on k, and the case of $k = 0$ is immediate from $U \Subset V$ . Assume that the statement holds for k and let $\varphi _0, \ldots , \varphi _k, \varphi _{k+1} \in U$ and $\psi \in V$ . By the induction hypothesis, there exists a $\rho \in V$ such that $\rho \vdash \varphi _0 \land \cdots \land \varphi _k \land \psi $ . Since $U \Subset V$ , there exists a $\rho ' \in V$ such that $\rho ' \vdash \varphi _{k+1} \land \rho $ . We obtain $\rho ' \vdash \varphi _0 \land \cdots \land \varphi _k \land \varphi _{k+1} \land \psi $ .

(b). Suppose $U \Subset V$ and V is mono-consistent. Since $U_{{\mathfrak {p}}} \subseteq _{{\mathfrak {m}}} V$ by (a), we have $U_{{\mathfrak {p}}} \subseteq V_{{\mathfrak {m}}}$ and $U_{{\mathfrak {r}}} \subseteq V_{{\mathfrak {n}}}$ . If $\xi \in U_{{\mathfrak {p}}} \cap V_{{\mathfrak {n}}}$ for some sentence $\xi $ , then there would be a $\psi \in V$ such that $\psi \vdash \neg \xi $ . Since $U_{{\mathfrak {p}}} \Cup V \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} V$ , there would be a $\rho \in V$ such that $\rho \vdash \xi \land \psi $ . Then, $\rho $ is inconsistent. This contradicts the mono-consistency of V. Therefore, $U_{{\mathfrak {p}}} \cap V_{{\mathfrak {n}}} = \emptyset $ . In a similar way, we can prove $U_{{\mathfrak {r}}} \cap V_{{\mathfrak {m}}} = \emptyset $ .

(c). By (a), $U \Subset U$ is equivalent to $U_{{\mathfrak {p}}} \Cup U \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} U$ , and to $U_{{\mathfrak {p}}} \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} U$ . Also, $U_{{\mathfrak {p}}} \subseteq ^{{\mathfrak {s}}}_{{\mathfrak {m}}} U$ is equivalent to $U_{{\mathfrak {m}}} = U_{{\mathfrak {p}}}$ .

2.3 Interpretability

An interpretation K of a theory U in a theory V is based on a translation of the U-language into the V-language. This translation commutes with the propositional connectives. In some broad sense, it also commutes with the quantifiers but here there are a number of extra features.

• • Translations may be more-dimensional: we allow a variable to be translated to an appropriate sequence of variables.

• • We may have domain relativisation: we allow the range of the translated quantifiers to be some domain definable in the V-language.

• • We may even allow the new domain to be built up from pieces of, possibly, different dimensions.

A further feature is that identity need not be translated to identity but can be translated to a congruence relation. Finally, we may also allow parameters in an interpretation. To handle these the translation may specify a parameter-domain. For details on the various kinds of translation, we refer the reader to [26].

We can define the obvious identity translation of a language in itself and composition of translations.

An interpretation is a triple ${\langle U,\tau ,V \rangle }$ , where $\tau $ is a translation of the U-language in the V-language such that, for all $\varphi $ , if $U \vdash \varphi $ , then $V \vdash \varphi ^\tau $ . ¹

We write:

• • $K:U \lhd V$ for: K is an interpretation of U in V.

• • $U \lhd V$ for: there is a K such that $K:U \lhd V$ . We also write $V\rhd U$ for: $U \lhd V$ .

• • $U \lhd _{\mathsf {loc}} V$ for: for every finitely axiomatisable sub-theory $U_0$ of U, we have $U_0 \lhd V$ .

• • $U \lhd _{\mathsf {mod}} V$ for: for every V-model $\mathcal {M}$ , there is a translation $\tau $ from the U-language in the V-language, such that $\tau $ defines an internal U-model $\mathcal {N} = \widetilde \tau (\mathcal {M})$ of U in $\mathcal {M}$ .

In Appendix B, we will have a brief look at effective versions of local interpretability, essentially concluding that all such versions collapse either to ordinary local interpretability or, somewhat surprisingly, to global interpretability.

In [28], the relation of essential tolerance was studied since it has backwards preservation of essential hereditary undecidability. In Appendix C, we briefly consider effective essential tolerance. This relation has backwards preservation of effective essential hereditary undecidability.

2.4 The non-effective notions

In this subsection, we introduce the non-effective notions. We will then discuss what the appropriate corresponding effective versions should be in the next subsection.

Our first building blocks are decidability, completeness, and separability.

• • A theory U is decidable if there is an algorithm that decides provability in U. In other words, U is decidable iff $U_{{\mathfrak {p}}}$ is computable. A theory is undecidable if it is not decidable.

• • A theory U is complete if, for every U-sentence $\varphi $ , we have $U\vdash \varphi $ or $U \vdash \neg \,\varphi $ . In other words, U is complete iff $U_{{\mathfrak {p}}} \cup U_{{\mathfrak {r}}}= \mathsf {Sent}_U$ . A theory is incomplete if it is not complete.

Suppose $\mathcal P$ is a property of theories. We say that U is essentially $\mathcal P$ if all consistent c.e. extensions (in the same language) of U are $\mathcal P$ . We say that U is hereditarily $\mathcal P$ if all consistent c.e. sub-theories of U (in the same language) are $\mathcal P$ . We say that U is potentially $\mathcal P$ if some consistent c.e. extension (in the same language) of U is $\mathcal P$ .

We defined essential and potential and hereditary with respect to $\subseteq ^{{\mathfrak {s}}}$ . In this paper we also will consider these notions with respect to $\subseteq ^{{\mathfrak {s}}}_{{\mathfrak {f}}}$ .

If $\mathcal R$ is a relation between theories the use of essential and hereditary and potential always concerns the first component aka the subject. Thus, e.g., we say that U essentially tolerates V meaning that U essentially has the property of tolerating V. Tolerance itself is defined as potential interpretation. So U essentially tolerates V if U essentially potentially interprets V. We will have a closer look at essential tolerance in Appendix C.

An important recursion theoretic notion is computable (in)separability. Two c.e. sets $\mathcal {X}$ and $\mathcal {Y}$ are computably separable iff, there is a computable $\mathcal {Z}$ such that $\mathcal {X}\subseteq \mathcal {Z}$ and $\mathcal {Y} \subseteq \mathcal {Z}^{\mathsf {c}}$ . Two sets are computably inseparable iff they are not computably separable. We want to apply computable (in)separability to theories and pairs of theories by designating certain sets of sentences associated with the theories as candidates for computable (in)separability.

Let us say that a pair of theories $(U,V)$ is acceptable iff U and V have the same signature and are jointly consistent. Let $(U,V)$ be acceptable. We define:

• • $(U,V)$ is computably (in)separable iff $U_{{\mathfrak {p}}}$ and $V_{{\mathfrak {r}}}$ are computably (in)separable.

• • U is computably (in)separable iff $(U,U)$ is computably (in)separable.

• • U is strongly computably (in)separable iff $(U, 0_U)$ is computably (in)separable.

Here, $0_U$ denotes the pure predicate calculus in the language of U.

We define: $(\mathcal {X},\mathcal {Y}) \leq _1 (\mathcal {Z},\mathcal {W})$ iff there is an injective computable function f, such that $n\in \mathcal {X}$ iff $f(n) \in \mathcal {Z}$ , and $n\in \mathcal {Y}$ iff $f(n) \in \mathcal {W}$ . Our definition generalises [20, Definition 2.4.9, p. 40], which coincides with our definition when we restrict ourselves to disjoint pairs of sets. We have $(\mathcal {X},\mathcal {X}) \leq _1 (\mathcal {Y},\mathcal {Y})$ iff $\mathcal {X}\leq _1\mathcal {Y}$ . Clearly, if $(\mathcal {X},\mathcal {Y})$ and $(\mathcal {Z},\mathcal {W})$ are disjoint pairs and if $(\mathcal {X},\mathcal {Y})$ is computably inseparable and $(\mathcal {X},\mathcal {Y}) \leq _1(\mathcal {Z},\mathcal {W})$ , then $(\mathcal {Z},\,\mathcal {W})$ is computably inseparable.

We have the following simple insights:

Theorem 2.3. $(U,V)$ is computably inseparable iff $(V,U)$ is computably inseparable.

Proof We note that negation witnesses that $(U_{{\mathfrak {p}}},V_{{\mathfrak {r}}}) \leq _1 (U_{{\mathfrak {r}}},V_{{\mathfrak {p}}})$ . So if $(U_{{\mathfrak {p}}},V_{{\mathfrak {r}}})$ is computably inseparable, then so is $(V_{{\mathfrak {p}}},U_{{\mathfrak {r}}})$ .

Theorem 2.4 (Subtraction Theorem).

If $(U+\varphi ,V+\varphi )$ is computably inseparable, then so is $(U+\varphi ,V)$ .

Proof The function $\psi \mapsto (\varphi \wedge \psi )$ witnesses that

$$\begin{align*}((U+\varphi)_{{\mathfrak {p}}},(V+\varphi)_{{\mathfrak {r}}})\leq_1 ((U+\varphi)_{{\mathfrak {p}}},V_{{\mathfrak {r}}}).\\[-37pt]\end{align*}$$

The computable inseparability of a theory is closely related to the undecidability and the incompleteness of the theory. Indeed, the computable inseparability of a theory U implies the essential undecidability of U. For example, the computable inseparability of the theory $\mathsf {R}$ of weak arithmetic follows from the work by Smullyan [14], and then the essential undecidability of $\mathsf {R}$ that was first established by Tarski, Mostowski, and Robinson [21] immediately follows. It is well-known that, for any consistent c.e. theory, essential incompleteness and essential undecidability are equivalent, and so the computable inseparability of $\mathsf {R}$ also yields the essential incompleteness of $\mathsf {R}$ . Here, the essential incompleteness of $\mathsf {R}$ is also strengthened. Mostowski [11] proved that $\mathsf {R}$ is uniformly essentially incomplete, that is, for any computable sequence $(T_i)_{i \in \omega }$ of consistent c.e. extensions of $\mathsf {R}$ , there exists a sentence simultaneously independent of all theories in the sequence. Interestingly, Ehrenfeucht [4] proved that Mostowski’s theorem is equivalent to the computable inseparability of $\mathsf {R}$ , namely, he proved that, for any consistent c.e. theory U, U is computably inseparable if and only if U is uniformly essentially incomplete.

Finitely axiomatisable theories sometimes behave well. Tarski, Mostowski, and Robinson [21] showed that for a finitely axiomatisable theory, essential undecidability is equivalent to essential hereditary undecidability. Also, it follows from the Subtraction Theorem (Theorem 2.4) that for a finitely axiomatised theory, computable inseparability is equivalent to strong computable inseparability. Note that strong effective inseparability implies essential hereditary undecidability. So, the finitely axiomatised theory $\mathsf {Q}$ which is an extension of $\mathsf {R}$ is strongly computably inseparable and essentially hereditarily undecidable. Here, since $\mathsf {R}$ is not finitely axiomatisable, the essential hereditary undecidability of $\mathsf {R}$ is non-trivial. This was proved by Cobham, but his proof of the result was not published. Vaught [22] gave a proof of Cobham’s theorem by proving the strong computable inseparability of $\mathsf {R}$ . For a detailed study of the notion of essential hereditary undecidability, see [28]. See [26] and [9] for new proofs of Cobham and Vaught’s theorems.

Relating to these notions, we also introduce the following two notions:

• • U is f-essentially incomplete iff, for any U-sentence $\varphi $ , if $U \cup \{\varphi \}$ is consistent, then $U \cup \{\varphi \}$ is incomplete.

• • U is f-uniformly essentially incomplete iff, for any $k \in \omega $ , whenever $U_0$ , …, $U_{k-1}$ are consistent c.e. extensions of U in the same language, then there is a sentence independent of each of the $U_0, \ldots , U_{k-1}$ .

It is easy to see that a theory U is f-essentially incomplete iff the Lindenbaum algebra of U is atomless. For f-uniform essential incompleteness, we have the following:

Proposition 2.5. Every essentially incomplete theory is f-uniformly essentially incomplete.

Proof We prove, by induction on k, that, if $U_0 \ldots , U_{k-1}$ are consistent c.e. extensions of U in the same language, then there is a sentence $\rho _k$ independent of each of the $U_0, \ldots , U_{k-1}$ . We set $\rho _0 := \top $ . In case $U_i \cup U_k$ is consistent for some $i<k$ , we replace both $U_i$ and $U_k$ with $U_i \cup U_k$ , and apply the induction hypothesis to the reduced sequence. Suppose all the $U_i \cup U_k$ , for $i<k$ , are inconsistent. We define $\rho _{k+1}$ . For each $i<k$ , there is a $\varphi _i$ , such that $U_k \vdash \varphi _i$ and $U_i \vdash \neg \, \varphi _i$ . Let $\varphi $ be the conjunction of the $\varphi _i$ . So, $U_k \vdash \varphi $ and, for each of the $U_i$ , where $i<k$ , we have $U_i \vdash \neg \,\varphi $ . Suppose $\rho $ is independent of $U_k$ . We define $\rho _{k+1} := (\rho \wedge \varphi ) \vee (\rho _k \wedge \neg \,\varphi )$ . It is immediate that this does as promised.

The relationships between these non-effective notions are visualised in Figure 1. In [12], the existence of a decidable f-essentially incomplete theory was proved. Also, essential hereditary undecidability and computable inseparability are incomparable in general (cf. [28, Example 6]). Therefore, none of the implications in Figure 1 are reversible. Related to this figure, one could consider the notions such as f-essential undecidability and f-essential hereditary undecidability etc., but we will not deal with these notions, as they are beside the main subject of this paper.

Figure 1 Implications between non-effective notions.

In what follows, we explore the effectivisations of these notions of incompleteness, undecidability, and inseparability.

2.5 What is effective?

Notions like essential and hereditary operate extensionally on the notions they modify. The situation is not so simple for adding effective. Adding “effective” in front of an expression operates intensionally on the definition of the concept.

Suppose the definition of $\mathcal {P}$ has the form $\forall \vec {x}\,\exists \vec {y}\, \varphi (\vec {x},\vec {y})$ , where $\varphi $ does not start with an existential quantifier. We propose to say that effectively $\mathcal {P}$ means that there are computable functions $\vec {\varPhi }$ such that $\forall \vec {x}\, \varphi (\vec {x},\vec {\varPhi }(\vec {x}))$ . If the given definition of $\mathcal {P}$ has the form $\forall \vec {x}\,(\psi (\vec {x}) \to \exists \vec {y}\, \varphi (\vec {x},\vec {y}))$ , where $\varphi $ does not start with an existential quantifier, then, effectively $\mathcal {P}$ means that there are partial computable functions $\vec {\varPhi }$ such that

$$\begin{align*}\forall \vec{x}\, (\psi(\vec{x}) \to \exists \vec{z}\, (\vec{\varPhi}(\vec{x})\simeq \vec{z} \wedge \varphi(\vec{x},\vec{z}))).\end{align*}$$

Remark 2.6. An alternative proposal would be to suggest that effectively $\mathcal {P}$ simply means the Kleene realisability of the salient definition of $\mathcal {P}$ . However, this does not always deliver the desired outcomes.

2.5.1 Effective undecidability

A c.e. set $\mathcal {X}$ is decidable iff

$$\begin{align*}\exists i \, ((\mathcal {X} \cap \mathsf {W}_i) = \emptyset \wedge (\mathcal {X} \cup \mathsf {W}_i) = \omega ).\end{align*}$$

So, $\mathcal {X}$ is undecidable means:

$$\begin{align*}\forall i\, (\exists y\, (y \in \mathcal {X} \wedge y\in \mathsf{W}_i) \vee \exists x\, (x\not\in \mathcal {X} \wedge x \not\in \mathsf{W}_i)).\end{align*}$$

Equivalently,

$$\begin{align*}\forall i\, \exists x\, ((x \in \mathcal {X} \wedge x\in \mathsf{W}_i) \vee (x\not\in \mathcal {X} \wedge x \not\in \mathsf{W}_i)).\end{align*}$$

The constructivisation of this is: there is a computable $\varPhi $ such that

$$\begin{align*}\forall i\, ((\varPhi(i) \in \mathcal {X} \wedge \varPhi(i)\in \mathsf{W}_i) \vee (\varPhi(i)\not\in \mathcal {X} \wedge \varPhi(i) \not\in \mathsf{W}_i)).\end{align*}$$

So this is the notion of being constructively non-computable (see [13, p. 162]).

Alternatively, $\mathcal {X}$ is undecidable also means:

$$\begin{align*}\forall i\, \exists y\, ((\mathcal {X} \cap \mathsf{W}_i) = \emptyset \Rightarrow (y \not \in \mathcal {X} \wedge y \not \in \mathsf{W}_i)).\end{align*}$$

So, the effectivisation of this is: there is a computable $\varPhi $ such that

$$\begin{align*}\forall i\, ((\mathcal {X} \cap \mathsf{W}_i) = \emptyset \Rightarrow (\varPhi(i) \not \in \mathcal {X} \wedge \varPhi(i) \not \in \mathsf{W}_i)).\end{align*}$$

This is exactly the notion of being creative.

Every constructively non-computable set is exactly a c.e. set whose complement is completely productive, which is a notion introduced by Dekker [3]. It is proved in [13, p. 183, Theorem VI] that productivity and complete productivity coincide, and hence creativity and constructive non-computability also coincide. So, these notions serve stable effectivisation of the notion of undecidability.

2.5.2 Effective essential undecidability

Let us assume the definition of the essential undecidability of U is

$$ \begin{align*} \forall i\,\forall j \, \Big(\big(\mathsf{W}_{i} \vdash U\text{ and } &\mathsf{con}(\mathsf{W}_i)\big)\; \Rightarrow \\ & \exists x\, \big((x\not\in \mathsf{W}_{i{\mathfrak {p}}} \wedge x \not\in \mathsf{W}_j) \vee (x \in \mathsf{W}_{i{\mathfrak {p}}} \wedge x\in \mathsf{W}_j)\big)\Big). \end{align*} $$

Here $\mathsf {con}(\mathsf {W}_i)$ is an abbreviation of the statement ‘ $\mathsf {W}_i$ is consistent’. So our recipe gives: there is a partial computable $\varPsi $ such that

$$ \begin{align*} & \forall i\,\forall j \, \Big(\big(\mathsf{W}_{i} \vdash U\text{ and } \mathsf{con}(\mathsf{W}_i)\big) \Rightarrow \\ & \big(\varPsi(i,j) {\downarrow} \wedge \big((\varPsi(i,j)\not\in \mathsf{W}_{i{\mathfrak {p}}} \wedge \varPsi(i,j) \not\in \mathsf{W}_j) \vee (\varPsi(i,j) \in \mathsf{W}_{i{\mathfrak {p}}} \wedge \varPsi(i,j)\in \mathsf{W}_j)\big)\big)\Big). \end{align*} $$

By the usual argument, we can always choose $\varPsi $ total. Moreover, our definition is equivalent to: there is a total computable $\varTheta $ such that

$$\begin{align*}\forall i \, \big((\mathsf{W}_{i} \vdash U\text{ and } \mathsf{con}(\mathsf{W}_i)\big) \Rightarrow \big( \lambda j.\varTheta(i,j) \text{ witnesses that}\ \mathsf{W}_{i{\mathfrak {p}}}\ \text{is creative)}\big). \end{align*}$$

So this gives us that effective essential undecidability is the same thing as effective essential creativity. We will work with the last notion. This notion was suggested in Feferman’s paper [5, Footnote 11] and investigated by Smullyan [15].

In the rest of the paper, we will simply stipulate the effective versions of the relevant notions. The reader may amuse herself by deriving the definitions following our recipe. We briefly discuss why there is not separate notion of effective local interpretability in Appendix B.

2.5.3 Constraining the witness

Effective notions usually have a partial computable function $\varPhi $ that chooses some (counter)example. In many cases, it is interesting to put a constraint on the (counter)examples, i.e., on the range of witness providing function $\varPhi $ . For example, consider effective essential incompleteness. One usually specifies that the witnesses can be chosen to be $\Sigma ^0_1$ (or, equivalently, $\Pi ^0_1$ ). In this case we will speak of effective essential $\Sigma ^0_1$ -incompleteness. We will see that there are other interesting restriction than this familiar one.

More generally, if the constraint $\mathcal {X}$ is a set of numbers coding sentences-of-the-given-signature, and $\mathcal {P}$ is the property of theories under consideration, we will speak about effective $\mathcal {X}$ - $\mathcal {P}$ . Note that we do not demand that $\mathcal {X}$ is c.e..

We can make this even more general. Let $\mathcal {F}$ be a function from sets of sentences to sets of sentences (all of the given signature). We do not put any effectivity constrains on $\mathcal {F}$ . Moreover, we allow $\mathcal {F}$ to be empty on some arguments. For example, U is effectively essentially $\mathcal {F}$ -incomplete iff, for every i such that $\mathsf {W}_i$ axiomatizes a consistent extension of U, there is a $\varphi \in \mathcal {F}(\mathsf {W}_i)$ , such that $\varphi $ is independent of $\mathsf {W}_i$ . We note that if $\mathcal {F}$ has constant value $\mathcal {X}$ , we are back in the simpler case.

2.6 Effective inseparability

Two disjoint c.e. sets $\mathcal {X}$ and $\mathcal {Y}$ are said to be effectively inseparable iff, there exists a partial computable function $\varPhi $ such that for any c.e. sets $\mathsf {W}_i$ and $\mathsf {W}_j$ , if $\mathsf {W}_i$ and $\mathsf {W}_j$ weakly bi-separate $\mathcal {X}$ and $\mathcal {Y}$ , then $\varPhi (i, j)$ converges and $\varPhi (i, j) \notin \mathsf {W}_i \cup \mathsf {W}_j$ . Let $(U,V)$ be acceptable pair of theories. We define:

• • $(U,V)$ is effectively inseparable iff $U_{{\mathfrak {p}}}$ and $V_{{\mathfrak {r}}}$ are effectively inseparable.

• • U is effectively inseparable iff $(U,U)$ is effectively inseparable.

• • U is strongly effectively inseparable iff $(U, 0_U)$ is effectively inseparable.

We define witness comparison notation. For every c.e. relation $R(\vec {x})$ , we can effectively find a primitive computable relation $R^\star (\vec {x}, y)$ such that $R(\vec {x})$ iff $\exists y\, R^\star (\vec {x}, y)$ . For all pairs of c.e. relations $R_0(\vec {x})$ and $R_1(\vec {x})$ , we define:

• • $R_0(\vec {x}) \leq R_1(\vec {x}) :\leftrightarrow \exists y\, (R_0^\star (\vec {x}, y) \wedge \forall z < y\, \neg \,R_1^\star (\vec {x}, z))$ ,

• • $R_0(\vec {x}) < R_1(\vec {x}) :\leftrightarrow \exists y\, (R_0^\star (\vec {x}, y) \wedge \forall z \leq y\, \neg \,R_1^\star (\vec {x}, z))$ .

We note that the witness comparison notation is intensional. The procedure to find $R^\star $ given R operates on a presentation of R and gives a presentation of $R^\star $ as output.

Proposition 2.7. In the definition of effective inseparability, restricting weakly bi-separating sets to bi-separating sets yields an equivalent notion.

Proof This is because if $\mathsf {W}_i$ and $\mathsf {W}_j$ weakly bi-separate $\mathcal {X}$ and $\mathcal {Y}$ , then we can effectively find $k_0$ and $k_1$ such that $\mathsf {W}_{k_0} \cup \mathsf {W}_{k_1} = \mathsf {W}_i \cup \mathsf {W}_j$ , and $\mathsf {W}_{k_0}$ and $\mathsf {W}_{k_1}$ bi-separate $\mathcal {X}$ and $\mathcal {Y}$ . Such $k_0$ and $k_1$ are obtained by letting:

• • $\mathsf {W}_{k_0} = \{n \mid (n \in \mathsf {W}_i) \leq (n \in \mathsf {W}_j)\}$ and

• • $\mathsf {W}_{k_1} = \{n \mid (n \in \mathsf {W}_j) < (n \in \mathsf {W}_i)\}$ .

Smullyan analyzed the notion of effective inseparability extensively, and in particular various notions related to effective inseparability are discussed in his [17, 18]. For more information on this topic, see the recent paper by Yong Cheng [2].

The effective inseparability of the theory $\mathsf {R}$ follows from a result established by Smullyan [15]. Smullyan mentioned that effective inseparability implies effective essential creativity. Also, for any consistent c.e. theory, effective essential creativity clearly implies effective essential incompleteness. Ehrenfeucht [4] provided an essentially incomplete theory that is not computably inseparable, but, in the effective case, such an example cannot exist. Namely, for any consistent c.e. theory, effective essential incompleteness implies effective inseparability. This result was established by Pour-El. Actually, Pour-El proved more. We say that a theory U is effectively if-essentially $\mathcal {F}$ -incomplete iff there is a partial computable function $\varPhi $ such that for any i, if $\mathsf {W}_i$ is a consistent finite extension of U, then $\varPhi (i)$ converges, $\varPhi (i) \in \mathcal {F}(\mathsf {W}_i)$ , and $\varPhi (i)$ is independent of $\mathsf {W}_i$ . Here, ‘if’ stands for ‘intensional finite extensions’. The notion of effective ef-essential $\mathcal {F}$ -incompleteness is studied in Section 4, where ‘ef’ stands for ‘extensional finite extensions’. Pour-El called effective essential incompleteness effective extensibility. She called effective if-essential incompleteness weak effective extensibility. Pour-El’s theorem is stated as follows:

Theorem 2.8 (Pour-El [1, Theorem 1]).

For any consistent c.e. theory U, the following are equivalent:

1. a. U is effectively inseparable.

2. b. U is effectively essentially creative.

3. c. U is effectively essentially incomplete.

4. d. U is effectively if-essentially incomplete.

In the next section, we prove a slightly strengthened version of Pour-El’s theorem (Theorem 3.1). Furthermore, our proof is slightly simpler than the original one. For completeness, we describe Pour-El’s original argument in Appendix A.

We say that a theory U is effectively uniformly essentially $\mathcal {X}$ -incomplete iff, there is a partial computable function $\varPhi $ such that for any j, if j is the index of a computable sequence of consistent c.e. extensions $(T_i)_{i \in \omega }$ of U, then we have that $\varPhi (j)$ converges, $\varPhi (j)\in \mathcal {X}$ , and $\varPhi (j)$ is independent of $T_i$ for all $i \in \omega $ . For any consistent c.e. theory, effective inseparability easily implies effective uniform essential incompleteness. So, one could say that, in the effective case, Ehrenfeucht’s result on the equivalence between computable inseparability and uniform essential incompleteness is superseded by Pour-El’s work. However, we do think it is instructive to include the effective analogues of Ehrenfeucht’s theorem here, also since these results have entirely self-reference free proofs. We also present the effective version of Ehrenfeucht’s results from the mono-perspective.

Theorem 2.9. Let U be a consistent c.e. theory. Let $\mathcal {X}$ be a set of sentences. The following are equivalent.

1. a. U is effectively $\mathcal {X}$ -inseparable, i.e., there is a partial computable function $\varPhi $ , such that for all pairs of sets $\mathsf {W}_i$ , $\mathsf {W}_j$ that weakly bi-separate $U_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ , we have $\varPhi (i,j)$ converges, $\varPhi (i,j) \in \mathcal {X}$ , and $\varPhi (i,j) \not \in \mathsf W_i \cup \mathsf W_j$ .

2. b. U is effectively uniformly essentially $\mathcal {X}$ -incomplete, i.e., there is a partial computable function $\varPsi _0$ , such that, for every computable sequence of consistent c.e. extensions $U^{\prime }_i$ of U with index j, we have that $\varPsi _0(j)$ converges, $\varPsi _0(j)\in \mathcal {X}$ , and, for all i, $U^{\prime }_i \nvdash \varPsi _0(j)$ and $U^{\prime }_i \nvdash \neg \, \varPsi _0(j)$ .

3. c. There is a partial computable function $\varPsi _1$ , such that, for every computable sequence of U-sentences $\nu _0,\nu _1,\dots $ with index j, such that each $\nu _i$ is consistent with U, $\varPsi _1(j)$ converges, $\varPsi _1(j) \in \mathcal {X}$ , and, for all i, we have $U \nvdash \nu _i \to \varPsi _1(j) $ and $U \nvdash \nu _i \to \neg \, \varPsi _1(j)$ .

4. d. There is a partial computable function $\varPsi _2$ , such that, for every computable sequence of U-sentences $\chi _0,\chi _1,\dots $ with index j, such that each $\chi _i$ is consistent with U, we have $\varPsi _2(j)$ converges, $\varPsi _2(j)\in \mathcal {X}$ , and, for all i, we have $0_U \nvdash \chi _i \to \varPsi _2(j)$ and $0_U \nvdash \chi _i \to \neg \, \varPsi _2(j)$ .

5. e. U is effectively $\Subset $ -essentially $\mathcal {X}$ - ${\mathfrak {m}}$ -incomplete, i.e., there is a partial computable function $\varPsi _3$ , such that for every mono-consistent $\mathsf {W}_j\Supset U$ , we have $\varPsi _3(j)$ converges, $\varPsi _3(j)\in \mathcal {X}$ , and, $ \varPsi _3(j)\not \in \mathsf {W}_{j{\mathfrak {m}}}\cup \mathsf {W}_{j{\mathfrak {n}}}$ .

6. f. There is a partial computable function $\varPsi _4$ such that, for any $\mathsf {W}_j$ such that $\widehat U \Cup \mathsf {W}_j$ is mono-consistent, we have $\varPsi _4(j)$ converges, $\varPsi _4(j)\in \mathcal {X}$ , and, $ \varPsi _4(j)\not \in \mathsf {W}_{j{\mathfrak {m}}}\cup \mathsf {W}_{j{\mathfrak {n}}}$ .

Moreover, each of (a), (b), (c), (d), (e), (f) is equivalent to a version, say (a $'$ ), (b $'$ ), (c $'$ ), (d $'$ ), (e $'$ ), (f $'$ ) where the witnessing function is total.

Proof “(a) to (b)”. Consider a computable sequence $(U^{\prime }_i)_{i\in \omega }$ of consistent c.e. extensions of U. Say our sequence has index j. Let $V:= \bigcup _{i\in \omega } U^{\prime }_{i{\mathfrak {p}}}$ and let $W := \bigcup _{i\in \omega } U^{\prime }_{i{\mathfrak {r}}}$ . We can find indices k and $\ell $ for V and W effectively from j. Clearly, V and W weakly bi-separate $U_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ . We take $ \varPsi _0(j) := \varPhi (k,\ell )$ . It follows that $ \varPsi _0(j)$ is in $\mathcal {X}$ and is independent of each $U^{\prime }_i$ .

“(b) to (c)”. We can effectively transform an index j of the sequence $(\nu _i)_{i\in \omega }$ into an index $j'$ of the sequence of theories $(U+\nu _i)_{i\in \omega }$ . We set $\varPsi _1(j) := \varPsi _0(j')$ .

“(c) to (d)”. We can take $\varPsi _2:= \varPsi _1$ .

“(d) to (e)”. Suppose $\mathsf {W}_j \Supset U$ and $\mathsf {W}_j$ is mono-consistent. We can effectively find an index k of an enumeration $(\chi _s)_{s\in \omega }$ of the elements of $\mathsf {W}_j$ from j. Since $\mathsf {W}_j$ and $U_{{\mathfrak {r}}}$ are disjoint, we have that $\chi _s$ is consistent with U for each $s \in \omega $ . We obtain that $\varPsi _2(k)$ converges, $\varPsi _2(k) \in \mathcal {X}$ , and for all s, $0_U \nvdash \chi _s \to \varPsi _2(k)$ and $0_U \nvdash \chi _s \to \neg \, \varPsi _2(k)$ . We then have $\varPsi _2(k) \notin \mathsf {W}_{j {\mathfrak {m}}} \cup \mathsf {W}_{j {\mathfrak {n}}}$ . We take $\varPsi _3(j) := \varPsi _2(k)$ .

“(e) to (f)”. Consider any c.e. $\mathsf {W}_j$ such that $W:=\widehat U \Cup \mathsf {W}_j$ is mono-consistent. It is easy to see that $W \Supset U$ . We can easily find an index k of W from j. We take $\varPsi _4(j) := \varPsi _3(k)$ .

“(f) to (a)”. Suppose $\mathsf {W}_i$ and $\mathsf {W}_j$ weakly bi-separate $U_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ . Let

$$\begin{align*}V := \mathsf{W}_i \cup \{ \chi \mid (\neg\,\chi) \in \mathsf{W}_j \}.\end{align*}$$

If $\widehat U \Cup V$ were mono-inconsistent, there would be a $\nu \in V$ and $U \vdash \neg \, \nu $ . The second conjunct tells us that $ \nu \not \in \mathsf {W}_i$ and $(\neg \,\nu )\not \in \mathsf {W}_j$ . A contradiction. So, $\widehat U \Cup V$ is mono-consistent. We clearly can find an index k of V effectively from i and j. We take $\varPhi (i,j) := \varPsi _4(k)$ .

We prove the equivalence between (a) and (a $'$ ). The (a $'$ )-to-(a) direction is trivial. We assume (a). Consider any pair of indices $i,j$ . We define $\varPhi ^\ast $ . We can effectively find indices $i',j'$ of $U_{{\mathfrak {p}}} \cup \mathsf {W}_i$ and $U_{{\mathfrak {r}}} \cup \mathsf {W}_j$ . We compute $\varPhi (i',j')$ and, simultaneously, we seek a counterexample to the claim that $\mathsf {W}_{i'},\mathsf {W}_{j'}$ weakly biseparate $\mathsf {U}_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ . If we find a value of $\varPhi (i',j')$ first then we give that as output of $\varPhi ^\ast (i,j)$ . If we find a counterexample first, we give that as output (or, alternatively, we give some fixed chosen sentence as output). It is easy to see that $\varPhi ^\ast $ is total and satisfies our specification.

The equivalences of (b) and (b $'$ ), (c) and (c $'$ ), (d) and (d $'$ ), (e) and (e $'$ ), and (f) and (f $'$ ) are proved in an analogous way.

3 Pour-El’s Theorem

In this section, we prove Pour-El’s Theorem in a slightly stronger version (Section 3.1). We give a variant (Section 3.2) and describe some sample applications (Sections 3.3 and 3.4). In Section 5, we present an adaptation of the argument that applies to effective hereditary creativity.

3.1 The Theorem

In this subsection, we give our version of Pour-El’s result.

Theorem 3.1. Suppose U is effectively if-essentially $\mathcal {F}$ -incomplete. Then, U is effectively $\mathcal {F}(U)$ -inseparable.

Proof Let U be effectively if-essentially $\mathcal {F}$ -incomplete with partial computable witness $\varPhi $ . Suppose $\mathsf {W}_i$ and $\mathsf {W}_j$ weakly biseparate $U_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ .

Using the Recursion Theorem with parameters (cf. [19, Theorem 3.5]), we effectively find a $k^\ast $ (depending of i and j) such that

$$ \begin{align*} & \mathsf{W}_{k^\ast} = U \cup \{ \varphi \mid \varPhi(k^\ast)\simeq \varphi \text{ and }\varphi \in \mathsf{W}_i \}\; \cup \\ & \{ \psi \mid \exists \varphi \,(\varPhi(k^\ast)\simeq \varphi \text{ and }\varphi \in \mathsf{W}_j \text{ and } \psi = \neg\,\varphi) \}. \end{align*} $$

We note that we have

$$\begin{align*}\mathsf{W}_{k^\ast} = \begin{cases} U \cup \{\varPhi(k^\ast)\}, & \ \text{if}\ \varPhi(k^\ast)\ \text{converges and}\ \varPhi(k^\ast) \in \mathsf{W}_i,\\ U \cup \{\neg\, \varPhi(k^\ast)\}, & \ \ \text{if}\ \varPhi(k^\ast)\ \text{converges and}\ \varPhi(k^\ast) \in \mathsf{W}_j, \\ U, & \ \text{otherwise}. \end{cases} \end{align*}$$

Let $U^\ast :=\mathsf {W}_{k^\ast }$ .

• • Suppose $\varPhi (k^\ast )$ converges to, say, $\varphi ^\ast $ and $\varphi ^\ast \in \mathsf {W}_i$ . It follows that $U^\ast = U\cup \{ \varphi ^\ast \}$ . Since $\varphi ^\ast \not \in U_{{\mathfrak {r}}}$ , we have that $U^\ast $ is consistent and, hence, $\varphi ^\ast $ is independent of $U^\ast $ . A contradiction.

• • Suppose $\varPhi (k^\ast )$ converges to, say, $\varphi ^\ast $ and $\varphi ^\ast \in \mathsf {W}_j$ . It follows that $U^\ast = U\cup \{ \neg \,\varphi ^\ast \}$ . Since $\varphi ^\ast \not \in U_{{\mathfrak {p}}}$ , we have that $U^\ast $ is consistent, and, hence, $\varphi ^\ast $ is independent of $U^\ast $ . A contradiction.

We may conclude that $U^\ast = U$ . Hence, $\varPhi (k^\ast )$ converges, say to $\varphi ^\ast $ . We have $\varphi ^\ast \not \in \mathsf {W}_i\cup \mathsf {W}_j$ .

Clearly, our argument delivers a total computable $\varPsi $ , such that, whenever $\mathsf {W}_i$ and $\mathsf {W}_j$ weakly biseparate $U_{{\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ , we have $\varPsi (i,j) \not \in \mathsf {W}_i\cup \mathsf {W}_j$ .

Finally, we note that the $\mathsf {W}_{k^\ast }$ are all equal to U and, thus $\varPsi (i,j)= \varPhi (k^\ast ) \in \mathcal {F}(U)$ .

As a consequence of Theorem 3.1, we obtain the following corollary showing the equivalence of several relating notions. For each formula class $\mathcal {X}$ and theory U, let $[\mathcal {X}]_U$ be the closure of $\mathcal {X}$ under U-provable equivalence.

Corollary 3.2. For any consistent c.e. theory U and set of sentences $\mathcal {X}$ , the following are equivalent:

1. a. U is effectively $\mathcal {X}$ -inseparable.

2. b. U is effectively essentially $\mathcal {X}$ -creative.

3. c. U is effectively essentially $\mathcal {X}$ -incomplete.

4. d. U is effectively if-essentially $\mathcal {X}$ -incomplete.

Moreover, in case $\mathcal {X}$ is c.e., each of (a), (b), (c), (d) is equivalent to a version, say (a $'$ ), (b $'$ ), (c $'$ ), (d $\,'$ ) where $\mathcal {X}$ is replaced by $[\mathcal {X}]_U$ .

Proof The implications “(a) to (b)”, “(b) to (c)”, and “(c) to (d)” are obvious.

“(d) to (a)”. Immediate from Theorem 3.1 by letting $\mathcal {F}$ to be the function having the constant value $\mathcal {X}$ .

Suppose $\mathcal {X}$ is c.e. It suffices to show the equivalence of (c) and (c $'$ ). The implication “(c) to (c $'$ )” is trivial because $\mathcal {X} \subseteq [\mathcal {X}]_U$ . We treat “(c $'$ ) to (c)”. Suppose that U is effectively essentially $[\mathcal {X}]_U$ -incomplete, as witnessed by a partial computable function $\varPhi $ . Note that if T is a consistent extension of U and $\varphi $ is independent of T, then each element of $[\{\varphi \}]_U$ is also independent of T. Let $\varPsi $ be a partial computable function such that for each i, if $\varPhi (i)$ converges, then $\varPsi (i)$ is in $[\{\varPhi (i)\}]_U \cap \mathcal {X}$ . Then, it is shown that $\varPsi $ witnesses the effective $\mathcal {X}$ -incompleteness of U.

Corollary 3.3. If U is effectively if-essentially $\mathcal {F}$ -incomplete, then U is effectively $\mathcal {F}(U)$ -inseparable and effectively if-essentially $\mathcal {F}(U)$ -incomplete

3.2 A variant: double generativity

In Smullyan’s book [18], many notions that are equivalent to effective inseparability were introduced (see also [2]). As a sample of variants of the argument in Section 3.1, we focus on double generativity among them as the double analogue of constructive non-computability, and discuss its witness constraining version.

We say that a theory U is doubly $\mathcal {X}$ -generative iff there exists a total computable function $\varPhi $ such that for any $i, j \in \omega $ , if $\mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ , then:

• • $\varPhi (i, j) \in U_{{\mathfrak {p}}}$ iff $\varPhi (i, j) \in \mathsf {W}_j$ ,

• • $\varPhi (i, j) \in U_{{\mathfrak {r}}}$ iff $\varPhi (i, j) \in \mathsf {W}_i$ ,

• • if $\varPhi (i, j) \notin \mathsf {W}_i \cup \mathsf {W}_j$ , then $\varPhi (i, j) \in \mathcal {X}$ .

We obtain a prima facie less constrictive notion if we demand that the $\mathsf {W}_i$ , $\mathsf {W}_j$ are the $V_{{\mathfrak {p}}}$ , $V_{{\mathfrak {r}}}$ of some theory V. A consistent c.e. theory U is $\mathcal {X}$ -theory-generative iff, there is a total computable function $\varPsi $ , such for every consistent theory V in the U-language with index i, we have:

• • $\varPsi (i) \in U_{{\mathfrak {p}}}$ iff $\varPsi (i) \in V_{{\mathfrak {r}}}$ ,

• • $\varPsi (i) \in U_{{\mathfrak {r}}}$ iff $\varPsi (i) \in V_{{\mathfrak {p}}}$ ,

• • if $\varPsi (i) \notin V_{{\mathfrak {p}}} \cup V_{{\mathfrak {r}}}$ , then $\varPsi (i) \in \mathcal {X}$ .

Theorem 3.4. For any consistent c.e. theory U and set of sentences $\mathcal {X}$ , the following are equivalent:

1. a. U is doubly $\mathcal {X}$ -generative.

2. b. U is $\mathcal {X}$ -theory-generative.

3. c. U is effectively if-essentially $\mathcal {X}$ -incomplete.

Proof “(a) to (b)”. Suppose that a total computable function $\varPhi $ witnesses the double $\mathcal {X}$ -generativity of U. Let V be any consistent c.e. theory with index i. We can effectively find $k_0$ and $k_1$ from i such that $\mathsf {W}_{k_0} =V_{{\mathfrak {p}}}$ and $\mathsf {W}_{k_1} = V_{{\mathfrak {r}}}$ . Let $\varPsi (i) := \varPhi (k_0,k_1)$ . It is immediate that $\varPhi $ witnesses that U is $\mathcal {X}$ -theory-generative.

“(b) to (c)”. Suppose $\varPhi $ witnesses that U is $\mathcal {X}$ -theory-generative and let V be a consistent c.e. theory that if-extends U with index i. Since the first two cases of $\mathcal {X}$ -theory-generativity cannot be active, it follows that $\varPhi (i)\not \in V_{{\mathfrak {p}}} \cup V_{{\mathfrak {r}}}$ and $\varPhi (i) \in \mathcal {X}$ .

“(c) to (a)”. Suppose that U is effectively if-essentially $\mathcal {X}$ -incomplete. Let $\varPhi $ be a partial computable function that witnesses the effective if-essential $\mathcal {X}$ -incompleteness of U. We may assume that $\varPhi (k)$ converges if $\mathsf {W}_k$ is an if-extension of U, whether $\mathsf {W}_k$ is consistent or not. By the Recursion Theorem with parameters, there exists a computable function $\varPsi (x, y)$ such that, setting $\varPhi ^*(x, y) : = \varPhi (\varPsi (x, y))$ , we have

$$\begin{align*}\mathsf{W}_{\varPsi(x, y)} = \begin{cases} U \cup \{\varPhi^*(x, y)\}, & \ \text{if}\ \big(\varPhi^*(x, y) \in (U_{{\mathfrak {p}}} \cup \mathsf{W}_{x}) \big) \leq \big(\varPhi^*(x, y) \in (U_{{\mathfrak {r}}} \cup \mathsf{W}_{y}) \big),\\ U \cup \{\neg \,\varPhi^*(x, y)\}, & \ \text{if}\ \big(\varPhi^*(x, y) \in (U_{{\mathfrak {r}}} \cup \mathsf{W}_{y}) \big) < \big(\varPhi^*(x, y) \in (U_{{\mathfrak {p}}} \cup \mathsf{W}_{x}) \big), \\ U, & \ \text{otherwise}. \end{cases} \end{align*}$$

Since $\mathsf {W}_{\varPsi (i, j)}$ is an if-essential extension of U for all i and j, we find that $\varPhi ^*(i, j)$ is a total computable function.

We show that $\varPhi ^*$ witnesses the double $\mathcal {X}$ -generativity of U. Let i and j be such that $\mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ and let $\varphi ^\ast := \varPhi ^\ast (i,j).$

• • Suppose $\big (\varphi ^* \in (U_{{\mathfrak {p}}} \cup \mathsf {W}_{i}) \big ) \leq \big (\varphi ^* \in (U_{{\mathfrak {r}}} \cup \mathsf {W}_{j}) \big )$ holds. Then, $\mathsf {W}_{\varPsi (i, j)} = U \cup \{\varphi ^*\}$ . Since $\mathsf {W}_{\varPsi (i, j)} \vdash \varPhi (\varPsi (i, j))$ , we have that $\mathsf {W}_{\varPsi (i, j)} = U \cup \{\varphi ^*\}$ is inconsistent. So, $\varphi ^* \in U_{{\mathfrak {r}}}$ . Since $U_{{\mathfrak {p}}} \cap U_{{\mathfrak {r}}} = \emptyset $ and $\varphi ^* \in U_{{\mathfrak {p}}} \cup \mathsf {W}_i$ , we obtain $\varphi ^* \in U_{{\mathfrak {r}}} \cap \mathsf {W}_i$ .

• • Suppose $\big (\varphi ^* \in (U_{{\mathfrak {r}}} \cup \mathsf {W}_{j}) \big ) < \big (\varphi ^* \in (U_{{\mathfrak {p}}} \cup \mathsf {W}_{i}) \big )$ holds. As above, it is shown that $\varphi ^* \in U_{{\mathfrak {p}}} \cap \mathsf {W}_j$ .

• • Otherwise, $\varphi ^* \notin U_{{\mathfrak {p}}} \cup \mathsf {W}_j$ and $\varphi ^* \notin U_{{\mathfrak {r}}} \cup \mathsf {W}_i$ . Since $\mathsf {W}_{\varPsi (i, j)} = U$ is a consistent if-essential extension of U, we have $\varphi ^* = \varPhi (\varPsi (i, j)) \in \mathcal {X}$ .

A simple exercise in propositional logic now shows that $\varPhi ^*$ witnesses the double $\mathcal {X}$ -generativity of U.

3.3 Orey-sentences of extensions of Peano Arithmetic

In this subsection we treat Orey-sentences for extensions of PA. The results of Section 3.4 will extend these results, but it is nice to see the simple case first.

Let U be any consistent c.e. extension of Peano Arithmetic. An Orey-sentence of U is a sentence O, such that $U \rhd (U+O)$ and $U \rhd (U+ \neg \, O)$ . Clearly, an Orey sentence O of U is independent of U. We also note that the Orey property is extensional in the sense that it only depends on the theorems of the given theory.

Here is one way to construct an Orey-sentence for U. Let $\mathsf {W}_i$ be an enumeration of the axioms of U. We define $\mathsf {W}_{i,n}$ as the theory axiomatised by the first n axioms enumerated in $\mathsf {W}_i$ . We define

Here stands for provability in $\mathsf {W}_{i,x}$ and stands for , so, arithmetizes the consistency of $\mathsf {W}_{i,n}$ . We write ${\triangledown }$ for $\neg {\vartriangle }\neg $ . We find that ${\vartriangle }_i$ satisfies the modal laws of K. Moreover, we have the seriality axiom D, i.e., ${\triangledown }_i\top $ . Finally, we can prove ${\triangledown }_i\varphi \rhd _U \varphi $ (see [6] or [27]).

We find $\gamma _i$ with $\mathsf {PA} \vdash \gamma _i \leftrightarrow \neg \, {\vartriangle }_i \gamma _i$ . We claim that $\gamma _i$ is an Orey-sentence of U. We have, temporarily omitting the subscripts i and U:

$$ \begin{align*} \gamma & \vdash \neg\,{\vartriangle} \gamma \\ & \vdash {\triangledown} \neg\, \gamma \\ & \rhd \neg\, \gamma \\ \neg \, \gamma & \vdash {\vartriangle} \gamma \\ & \vdash {\triangledown} \gamma \\ & \rhd \gamma. \end{align*} $$

Since, we have $\gamma \rhd \neg \, \gamma $ and $\neg \,\gamma \rhd \neg \, \gamma $ , we find, using a disjunctive interpretation, $\top \rhd \neg \, \gamma $ . Similarly, we find $\top \rhd \gamma $ . Thus, $\gamma _i$ is an Orey-sentence of U as promised.

Remark 3.5. The Orey-sentences $\gamma _i$ produced in our example are all known to be true. We can also use ${\vartriangle }_i$ to build U-internally a Henkin interpretation of U. This interpretation comes with a truth predicate $\mathsf {H}_i$ . The Liar sentence $\lambda _i$ of $\mathsf {H}_i$ is also an Orey-sentence of U. However, in this case, it is unknown whether $\lambda _i$ or $\neg \,\lambda _i$ is true.

We note that, in the real world, the Henkin construction just depends on the theorems of the given theory, not on the axiomatisation. It does depend on the chosen enumeration of sentences. Thus, as long as we keep the enumeration fixed, the truth-value of $\lambda _i$ remains the same when we run through i that enumerates axiom sets of PA.

Let $\mathbb O$ be the function that assigns to sets of sentences $\mathcal {A}$ in the signature of arithmetic the Orey-sentences of the theory axiomatised by $\mathcal {A}$ . Note that it is possible that there are no such Orey-sentences, so the empty set will be in the range of this function. We have shown the following:

Theorem 3.6. $\mathsf {PA}$ is effectively essentially $\mathbb O$ -incomplete.

Applying Corollary 3.3, we find the following:

Theorem 3.7. PA is effectively $\mathbb O(\mathsf {PA})$ -inseparable and, thus, effectively essentially $\mathbb O(\mathsf {PA})$ -incomplete.

Theorem 3.7 illustrates the important insight that independence,per se, has nothing to do with strength. Of course, we are familiar with this point, e.g., from the well-known results on, e.g., the continuum hypothesis which is an Orey-sentence of ZF that is independent of many extensions that have to do with strength. However, Theorem 3.7 has a somewhat different flavor in that it presents a systematic construction of such sentences for a wide range of theories.

3.4 Consistency and conservativity

We say a formula $\alpha (x)$ is a binumeration of a theory U iff for any U-sentence $\varphi $ , if $\varphi \in U$ , then $U \vdash \alpha (\ulcorner {\varphi }\urcorner )$ ; and if $\varphi \notin U$ , then $U \vdash \neg \, \alpha (\ulcorner {\varphi }\urcorner )$ . For each binumeration $\alpha (x)$ of U, we can naturally construct a formula $\mathsf {Prf}_{\alpha }(x, y)$ saying that y is the code of a proof of a formula with the code x in the theory defined by $\alpha $ (cf. [6]). Let $\mathsf {Con}_\alpha $ be the consistency statement $\neg \, \exists y\, \mathsf {Prf}_\alpha (\ulcorner {\bot }\urcorner , y)$ of U, where $\bot $ is some U-refutable sentence. Let $\mathbb C$ be the function that assigns to sets of sentences $\mathcal {A}$ in the signature of arithmetic the set of all sentences of the form $\mathsf {Con}_\alpha $ , where $\alpha $ is a binumeration of some computable axiomatisation of an extension A of $\mathsf {PA}$ axiomatised by $\mathcal {A}$ . It is known that $\mathsf {PA}$ is effectively essentially $\mathbb {C}$ -incomplete (cf. Lindström [10, Theorem 2.8]). Thus, $\mathsf {PA}$ is effectively $\mathbb {C}(\mathsf {PA})$ -inseparable and effectively essentially $\mathbb {C}(\mathsf {PA})$ -incomplete.

For each $n \geq 1$ , let $\mathbb D_n$ be the function that assigns to sets of sentences $\mathcal {A}$ in the signature of arithmetic the set of all sentences $\varphi $ such that $\varphi $ and $\neg \, \varphi $ are both $\Pi _n$ -conservative over the theory axiomatised by $\mathcal {A}$ . It is well-known that for any consistent c.e. extension U of $\mathsf {PA}$ , $\mathbb D_1(U) = \mathbb {O}(U)$ (cf. [10, Theorem 6.6]). For every pair of functions $\mathcal {F}$ and $\mathcal {G}$ from sets of sentences to sets of sentences, let $\mathcal {F} \cap \mathcal {G}$ be the function defined by $(\mathcal {F} \cap \mathcal {G})(\mathcal {A}) = \mathcal {F}(\mathcal {A}) \cap \mathcal {G}(\mathcal {A})$ .

For each binumeration $\alpha $ of an extension U of $\mathsf {PA}$ , the formula $\mathsf {Prf}_{\alpha }^{\Sigma _n}(x, y)$ is defined as

$$\begin{align*}\exists u \leq y\, (\Sigma_n(u) \land \mathsf{true}_{\Sigma_n}(u) \land \mathsf{Prf}_\alpha(u \dot{\to} x, y)). \end{align*}$$

Then, we have the following:

Proposition 3.8 (The small reflection principle (cf. [10, Lemma 5.1(ii)])).

Let U be any computable extension of $\mathsf {PA}$ and $\alpha $ be a binumeration of U. Then, for any sentence $\varphi $ and natural number m, we have

$$\begin{align*}U \vdash \exists y < \underline{m}\, \mathsf{Prf}_{\alpha}^{\Sigma_n}(\ulcorner{\varphi}\urcorner, y) \to \varphi.\end{align*}$$

Theorem 3.9. For each $n \geq 1$ , $\mathsf {PA}$ is effectively essentially $\mathbb {C} \cap \mathbb {D}_n$ -incomplete.

Proof Suppose that $\mathsf {W}_i$ is a consistent c.e. extension of $\mathsf {PA}$ . By Craig’s trick, we can effectively find a k from i such that $\mathsf {W}_k$ is a primitive computable axiomatisation of $\mathsf {W}_i$ . Let $\beta (x)$ be an effectively found primitive computable binumeration of $\mathsf {W}_k$ . We can effectively find a formula $\alpha (x)$ such that

$$\begin{align*}\mathsf{PA} \vdash \alpha(x) \leftrightarrow \Big( \big(\beta(x) \lor \exists y < x\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\mathsf{Con}_\alpha}\urcorner, y) \big) \land \forall z < x\, \neg\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\neg\, \mathsf{Con}_\alpha}\urcorner, z) \Big). \end{align*}$$

We show that $\mathsf {Con}_\alpha $ is $\Pi _n$ -conservative over $\mathsf {W}_k$ . Let $\pi $ be any $\Pi _n$ sentence such that $\mathsf {W}_k \cup \{\mathsf {Con}_\alpha \} \vdash \pi $ . Then, $\mathsf {W}_k \cup \{\neg \, \pi \} \vdash \neg \, \mathsf {Con}_\alpha $ . There exists a number q such that $\mathsf {PA} \cup \{\neg \, \pi \} \vdash \mathsf {Prf}_{\beta }^{\Sigma _n}(\ulcorner {\neg \, \mathsf {Con}_\alpha }\urcorner , \underline {q})$ . Thus, $\mathsf {PA} \cup \{\neg \, \pi \} \vdash \alpha (x) \to x \leq \underline {q}$ . We have

$$ \begin{align*} \mathsf{PA} \cup \{\neg\, \pi\} \vdash \forall y < \underline{q}\, \neg\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\mathsf{Con}_\alpha}\urcorner, y) & \to \Big (\alpha(x) \to \big( x\leq \underline{q} \;\wedge \\ & \hspace{1cm} \forall y < x\, \neg\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\mathsf{Con}_\alpha}\urcorner, y) \big)\kern-1pt\Big) \\ & \to \big(\alpha(x) \to (\beta(x) \land x \leq \underline{q})\big) \\ & \to (\mathsf{Con}_{\beta \leq \underline{q}} \to \mathsf{Con}_\alpha). \\ & \to \mathsf{Con}_\alpha. \end{align*} $$

The last step uses the fact that $\beta (x)$ a is binumeration of $\mathsf {W}_k$ in combination with the essential reflexiveness of $\mathsf {PA}$ . By combining this with the small reflection principle, we obtain $\mathsf {W}_k \cup \{\neg \, \pi \} \vdash \mathsf {Con}_\alpha $ . Since $\mathsf {W}_k \cup \{\mathsf {Con}_\alpha \} \vdash \pi $ , we conclude $\mathsf {W}_k \vdash \pi $ .

We show that $\neg \, \mathsf {Con}_\alpha $ is also $\Pi _n$ -conservative over $\mathsf {W}_k$ . Let $\pi $ be any $\Pi _n$ sentence such that $\mathsf {W}_k \cup \{\neg \, \mathsf {Con}_\alpha \} \vdash \pi $ . Then, $\mathsf {W}_k \cup \{\neg \, \pi \} \vdash \mathsf {Con}_\alpha $ . There exists a number p such that $\mathsf {PA} \cup \{\neg \, \pi \} \vdash \mathsf {Prf}_{\beta }^{\Sigma _n}(\ulcorner {\mathsf {Con}_\alpha }\urcorner , \underline {p})$ . For each $q> p$ , we have $\mathsf {PA} \cup \{\neg \, \pi \} \vdash \exists y < \underline {q}\, \mathsf {Prf}_{\beta }^{\Sigma _n}(\ulcorner {\mathsf {Con}_\alpha }\urcorner , y)$ . We obtain

$$\begin{align*}\mathsf{PA} \cup \{\neg\, \pi\} \vdash \forall z < \underline{q}\, \neg\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\neg\, \mathsf{Con}_\alpha}\urcorner, z) \to \alpha(\underline{q}). \end{align*}$$

So, for a sufficiently large $q> p$ , we have

$$\begin{align*}\mathsf{PA} \cup \{\neg\, \pi\} \vdash \forall z < \underline{q}\, \neg\, \mathsf{Prf}_{\beta}^{\Sigma_n}(\ulcorner{\neg\, \mathsf{Con}_\alpha}\urcorner, z) \to \neg\, \mathsf{Con}_\alpha. \end{align*}$$

By combining this with the small reflection principle, we have $\mathsf {W}_k \cup \{\neg \, \pi \} \vdash \neg \, \mathsf {Con}_\alpha $ . Since $\mathsf {W}_k \cup \{\neg \, \mathsf {Con}_\alpha \} \vdash \pi $ , we conclude $\mathsf {W}_k \vdash \pi $ .

We have proved that $\mathsf {Con}_\alpha \in \mathbb {D}_n(\mathsf {W}_i)$ . Consequently, we have that $\mathsf {Con}_{\alpha }$ is independent of $\mathsf {W}_i$ .

By $\Pi _n$ -conservativity, we obtain that for each $m \in \omega $ ,

• • $\mathsf {W}_k \vdash \forall y < \underline {m}\, \neg \, \mathsf {Prf}_{\beta }^{\Sigma _n}(\ulcorner {\mathsf {Con}_\alpha }\urcorner , y)$ and

• • $\mathsf {W}_k \vdash \forall z < \underline {m}\, \neg \, \mathsf {Prf}_{\beta }^{\Sigma _n}(\ulcorner {\neg \, \mathsf {Con}_\alpha }\urcorner , z)$ .

Hence, we have $\mathsf {W}_k \vdash \alpha (\underline {m}) \leftrightarrow \beta (\underline {m})$ . This means that $\alpha (x)$ is also a binumeration of $\mathsf {W}_k$ , and, thus, $\mathsf {Con}_{\alpha } \in \mathbb C(\mathsf {W}_i)$ . We take $\varPhi (i) : = \mathsf {Con}_\alpha $ . Then, $\varPhi $ witnesses the effective essential $\mathbb {C} \cap \mathbb {D}_n$ -incompleteness of $\mathsf {PA}$ .

Corollary 3.10. $\mathsf {PA}$ is effectively $(\mathbb {C} \cap \mathbb {D}_n)(\mathsf {PA})$ -inseparable and effectively essentially $(\mathbb {C} \cap \mathbb {D}_n)(\mathsf {PA})$ -incomplete.

4 Effective ef-essential incompleteness

Effective forms of incompleteness employ presentations of the extensions considered. This is necessitated by the fact that our witnessing partial computable functions need finite objects to operate on. In the finite case, we do have an alternative available to presenting an extension by a c.e. index. We can simply specify the sentence we extend with. In this section, we study this notion of effective incompleteness for finite extensions and a variant. We consider the relation of these two notions to if-essential incompleteness.

Definition 4.1. Consider a c.e. theory U. We define:

• • U is effectively ef-essentially $\mathcal {F}$ -incomplete iff there exists a computable function $\varPhi $ , such that, for any sentence $\varphi $ , if $U \cup \{\varphi \}$ is consistent, then $\varPhi (\varphi )$ is independent of $U \cup \{\varphi \}$ and $\varPhi (\varphi ) \in \mathcal {F}(U \cup \{\varphi \})$ .

• • U is effectively ef-essentially $\mathcal {F}$ -incomplete w.r.t. N and $\xi $ iff N is an interpretation of $\mathsf {R}$ in U and, for any sentence $\varphi $ , if $U \cup \{\varphi \}$ is consistent, then $\xi (\ulcorner {\varphi }\urcorner )$ is independent of $U \cup \{\varphi \}$ and $\xi (\ulcorner {\varphi }\urcorner ) \in \mathcal {F}(U \cup \{\varphi \})$ . Here the numerals are the numerals provided by N. To avoid heavy notation, we pretend that N is one-dimensional. Of course, this is inessential.

The notion of effective ef-essential incompleteness was studied by Jones [7] as the name effective nonfinite completability. We have the following simple insight.

Theorem 4.2. Every effectively if-essentially $\mathcal {F}$ -incomplete theory is effectively ef-essentially $\mathcal {F}$ -incomplete.

Proof This is immediate seeing that, given $\varphi $ , we can effectively find an index of $U \cup \{\varphi \}$ .

However, an effectively ef-essentially incomplete theory can be decidable as we show in the following example. So, the converse of Theorem 4.2 does not generally hold.

Example 4.3. We consider the theory $\mathsf {Succ}^\circ $ in the language of zero and successor. The theory is axiomatised by: zero is not a successor; successor is injective; every number is either zero or a successor; for every n, there is at most one successor-cycle of size n.

One can show that $\mathsf {Succ}^\circ $ is decidable and that every sentence is equivalent to a Boolean combination of sentences $\mathsf {C}_n$ saying ‘there is a cycle of size n’ (see, e.g., [12, Appendix A]). We note that, over $\mathsf {Succ}^\circ $ , the $\mathsf {C}_n$ are mutually independent.

Let $\varphi $ be any $\mathsf {Succ}^\circ $ -sentence. We can effectively find a sentence $\psi $ , equivalent to $\varphi $ , which is a Boolean combination of the $\mathsf {C}_n$ . Let k be the smallest number so that $\mathsf {C}_k$ does not occur in $\psi $ . We set $\varPhi (\varphi ) := \mathsf {C}_k$ . It is easily seen that $\varPhi $ witnesses the effective ef-essential incompleteness of $\mathsf {Succ}^\circ $ .

We can say more about the difference of the two notions. The following two theorems reveal an intrinsic difference between if- and ef-.

Theorem 4.4. Suppose $\mathcal {X}$ is c.e. and $\varPhi $ is a partial computable witness that U is an effectively if-essentially $\mathcal {X}$ -incomplete c.e. theory. Then, we can find, effectively from an index of $\varPhi $ , a $\varphi \in \mathcal {X}$ , such that $U \cup \{\varphi \}$ is inconsistent. In particular, $U_{{\mathfrak {p}}} \cup \mathcal {X}$ is not mono-consistent.

Proof By the Recursion Theorem, we find an i such that

$$\begin{align*}\mathsf{W}_{i} = \begin{cases} U \cup \{\varPhi(i)\}, & \text{if}\ \varPhi(i)\ \text{converges and}\ \varPhi(i) \in \mathcal {X}, \\ U, & \text{otherwise}. \end{cases} \end{align*}$$

If the second clause would obtain, $\mathsf {W}_i$ would be a consistent if-extension of U. So, $\varPhi (i)$ would converge to an element of $\mathcal {X}$ . Quod non. Thus, only the first clause can be active. Hence, $\varPhi (i)$ converges to an element $\varphi $ of  $\mathcal {X}$ . Then, $\mathsf {W}_i = U \cup \{\varphi \}$ and $\mathsf {W}_i \vdash \varPhi (i)$ . By the effective if-essential $\mathcal {X}$ -incompleteness of U, we have that $U \cup \{\varphi \}$ is inconsistent.

Theorem 4.5. Suppose U is a consistent effectively ef-essentially incomplete c.e. theory. Then, there is a c.e. set $\mathcal {X}$ such that U is effectively ef-essentially $\mathcal {X}$ -incomplete and every $\varphi $ in $\mathcal {X}$ is consistent with U, i.o.w., $U_{{\mathfrak {p}}} \cup \mathcal {X}$ is mono-consistent.

Proof Suppose U is effectively ef-essentially incomplete as witnessed by $\varPhi $ . We take

$$\begin{align*}\varPsi(\varphi) := \begin{cases} (\varphi \to \varPhi(\varphi)), & \text{if}\ \varPhi(\varphi)\ \text{converges}, \\ \text{undefined,} & \text{otherwise}. \end{cases} \end{align*}$$

Let $\mathcal {X}$ be the range of $\varPsi $ .

If $\varphi $ is inconsistent with U and $\varPhi (\varphi )$ converges, then $U\vdash \varphi \to \varPhi (\varphi )$ and, thus, $\varPsi (\varphi )$ is consistent with U. If $\varphi $ is consistent with U, then $\varPhi (\varphi )$ converges and $\varPhi (\varphi )$ is independent of $U \cup \{\varphi \}$ and, a fortiori, consistent with U.

Combining Theorems 4.4 and 4.5, we immediately find the following corollary:

Corollary 4.6. Suppose U is a consistent effectively ef-essentially incomplete c.e. theory. Then, there is a c.e. set $\mathcal {X}$ such that U is effectively ef-essentially $\mathcal {X}$ -incomplete but not effectively if-essentially $\mathcal {X}$ -incomplete.

The next theorem gives a condition under which effective ef-essential $\mathcal {X}$ -incompleteness w.r.t. some N and $\xi $ implies effective essential $\mathcal {X}$ -incompleteness.

Theorem 4.7. Let U be a consistent c.e. theory and suppose U is effectively ef-essentially $\mathcal {X}$ -incomplete w.r.t. N and $\xi $ . Then, U is effectively essentially $\mathcal {X}$ -incomplete via a witnessing function $\varPhi $ , where $\varPhi (i)$ is of the form $\xi (\ulcorner {\sigma }\urcorner )$ .

Proof We assume the conditions of the theorem. Suppose that $\mathsf {W}_{i}$ is a consistent extension of U. We construct formulas $\gamma _0$ and $\gamma _1$ with some desired properties as follows. Our construction is an adaptation of a solution to [10, Exercise 3.4].

1. Stage 1. We start with $\Sigma _1$ -formulas $\alpha _0$ and $\alpha _1$ , where $\alpha _0$ represents $\mathsf {W}_{i{\mathfrak {p}}}$ and $\alpha _1$ represents $\mathsf {W}_{i{\mathfrak {r}}}$ . We arrange it so that the $\alpha _i$ start with a single existential quantifier followed by a $\Delta _0$ -formula.

2. Stage 2. Let $\beta _0 := \alpha _0 \leq \alpha _1$ and $\beta _1 := \alpha _1 < \alpha _0$ . We note that the $\beta _i$ represent the same sets as the $\alpha _i$ . Moreover, if $n \in \mathsf {W}_{i {\mathfrak {p}}}$ , then $\beta _0(\underline {n})$ is true, and, hence $\mathsf {R} \vdash \beta _{0}(\underline {n}) \wedge \neg \, \beta _{1}(\underline {n})$ . Also, if $n \in \mathsf {W}_{i {\mathfrak {r}}}$ , then $\mathsf {R} \vdash \beta _{1}(\underline {n}) \wedge \neg \, \beta _{0}(\underline {n})$ .

3. Stage 3. Let $\eta (x)$ be a $\Sigma _1$ -formula with one existential quantifier followed by a $\Delta _0$ -formula that is equivalent in predicate logic with $(\beta _0(x) \vee \beta _1(x))$ . By the Fixed Point Lemma, we find a $\rho $ , such that, for every n, we have $\mathsf {R} \vdash \rho (\underline {n}) \leftrightarrow \eta (\underline {n}) \leq \alpha _0(\ulcorner {\rho ^N(\underline {n})}\urcorner ) $ . By the reasoning of the FGH Theorem (see, e.g., [24, Section 3] or [8]), we have: $\mathsf {W}_i \vdash \rho ^N(\underline {n})$ iff $\rho (\underline {n})$ is true iff $n \in \mathsf {W}_{i {\mathfrak {p}}} \cup \mathsf {W}_{i{\mathfrak {r}}}$ . We define $\gamma _i(x) := (\beta _i(x) \wedge \rho (x))$ . We find:

   1. A. The $\gamma _0$ and $\gamma _1$ represent $\mathsf {W}_{i {\mathfrak {p}}}$ and $\mathsf {W}_{i {\mathfrak {r}}}$ , respectively.

   2. B. If $\mathsf {W}_i \vdash (\gamma _0(\underline {n}) \vee \gamma _1(\underline {n}))^N$ , then $n \in \mathsf {W}_{i{\mathfrak {p}}}\cup \mathsf {W}_{i{\mathfrak {r}}}$ .

   3. C. If $n\in \mathsf {W}_{i{\mathfrak {p}}}$ , then $\mathsf {R} \vdash \gamma _0(\underline {n}) \wedge \neg \, \gamma _{1}(\underline {n})$ .

   4. D. If $n\in \mathsf {W}_{i{\mathfrak {r}}}$ , then $\mathsf {R} \vdash \gamma _1(\underline {n}) \wedge \neg \, \gamma _{0}(\underline {n})$ .

We can effectively find a sentence $\sigma $ from i satisfying the following equivalence:

$$\begin{align*}U \vdash \sigma \leftrightarrow \Big(\big(\gamma_0(\ulcorner{\xi(\ulcorner{\sigma}\urcorner)}\urcorner)^N \to \xi(\ulcorner{\sigma}\urcorner) \big) \land \big( \gamma_1(\ulcorner{\xi(\ulcorner{\sigma}\urcorner)}\urcorner)^N \to \neg\, \xi(\ulcorner{\sigma}\urcorner)\big) \Big). \end{align*}$$

Suppose, towards a contradiction, that $\xi (\ulcorner {\sigma }\urcorner ) \in \mathsf {W}_{i {\mathfrak {p}}} \cup \mathsf {W}_{i {\mathfrak {r}}}$ .

• • Suppose $\xi (\ulcorner {\sigma }\urcorner ) \in \mathsf {W}_{i {\mathfrak {p}}}$ . Then, by (C), we obtain $U \vdash \sigma \leftrightarrow \xi (\ulcorner {\sigma }\urcorner )$ . Since $U \cup \{\sigma \} \vdash \xi (\ulcorner {\sigma }\urcorner )$ , we have that $U \cup \{\sigma \}$ is inconsistent because U is ef-essentially $\mathcal {X}$ -incomplete w.r.t. N and $\xi $ . Thus, $U \vdash \neg \, \sigma $ , and, hence, $U \vdash \neg \, \xi (\ulcorner {\sigma }\urcorner )$ . This contradicts the consistency of $\mathsf {W}_i$ .

• • Suppose $\xi (\ulcorner {\sigma }\urcorner ) \in \mathsf {W}_{i {\mathfrak {r}}}$ . Then, by (D), we obtain $U \vdash \sigma \leftrightarrow \neg \, \xi (\ulcorner {\sigma }\urcorner )$ . Since $U \cup \{\sigma \} \vdash \neg \, \xi (\ulcorner {\sigma }\urcorner )$ , we have that $U \cup \{\sigma \}$ is inconsistent. Thus, $U \vdash \xi (\ulcorner {\sigma }\urcorner )$ . This contradicts the consistency of $\mathsf {W}_{i}$ .

We have shown that $\xi (\ulcorner {\sigma }\urcorner )$ is independent of $\mathsf {W}_{i}$ . By (B), we find that $U \nvdash (\gamma _0(\ulcorner {\xi (\ulcorner {\sigma }\urcorner )}\urcorner ) \lor \gamma _1(\ulcorner {\xi (\ulcorner {\sigma }\urcorner )}\urcorner ))^N$ . Since

$$\begin{align*}U\vdash \neg\, \sigma \to \big (\gamma_0(\ulcorner{\xi(\ulcorner{\sigma}\urcorner)}\urcorner) \lor \gamma_1(\ulcorner{\xi(\ulcorner{\sigma}\urcorner)}\urcorner)\big)^N,\end{align*}$$

we have that $U \cup \{\sigma \}$ is consistent. Hence, $\xi (\ulcorner {\sigma }\urcorner ) \in \mathcal {X}$ . We take $\varPhi (i) : = \xi (\ulcorner {\sigma }\urcorner )$ . Thus, $\varPhi $ witnesses the effective essential $\mathcal {X}$ -incompleteness of U.

We show that the converse of Theorem 4.7 does not generally hold. For this, as compared with Corollary 3.2, we prove the following proposition stating that the notion of effective ef-essential $\mathcal {X}$ -incompleteness w.r.t. N and $\xi $ is not equivalent to the one obtained by replacing $\mathcal {X}$ with $[\mathcal {X}]_U$ .

Proposition 4.8. If U is effectively ef-essentially incomplete w.r.t. N and $\xi $ , then there exists a computable set $\mathcal {X}$ of formulas such that U is effectively ef-essentially $[\mathcal {X}]_U$ -incomplete w.r.t. N and $\xi $ , but U is not effectively ef-essentially $\mathcal {X}$ -incomplete w.r.t. N and $\eta $ for all $\eta $ .

Proof Suppose that U is effectively ef-essentially incomplete w.r.t. N and $\xi $ . Let $\mathcal {X}$ be the computable set defined by

$$\begin{align*}\mathcal {X} : = \{\xi(\ulcorner{\varphi}\urcorner) \land \bigwedge_{i = 1}^{\ulcorner{\varphi}\urcorner} (0=0)^N \mid \varphi\ \text{is a}\ U\text{-sentence}\}. \end{align*}$$

Since each $\xi (\ulcorner {\varphi }\urcorner )$ is U-provably equivalent to some element of $\mathcal {X}$ , we have that U is effectively ef-essentially $[\mathcal {X}]_U$ -incomplete w.r.t. N and $\xi $ . On the other hand, since there are unboundedly many U-sentences $\varphi $ in the sense of Gödel numbers such that $U \cup \{\varphi \}$ is consistent, it is shown that there is no single formula $\eta $ such that U is effectively ef-essentially $\mathcal {X}$ -incomplete w.r.t. N and $\eta $ .

Remark 4.9. Suppose U is a c.e. theory that interprets R via N. Then, we can find a $\rho $ such that U is essentially ef-incomplete w.r.t. N and $\rho $ . This is a variant of Rosser’s Theorem. It follows, by Theorem 4.7, that U is effectively if-essentially incomplete. Moreover, this can be relativised to $\mathcal {X}$ , for any $\mathcal {X}$ that contains all the $\rho (\ulcorner {\varphi }\urcorner )$ ’s. From the results presented in this section, we have the following observations.

• • By Theorem 4.4, we can effectively find a $\sigma $ , such that $U \cup \{\rho (\sigma )\}$ is inconsistent.

• • By Corollary 4.6, we can find a c.e. set $\mathcal {Y}$ , such that U is effectively ef-essentially $\mathcal {Y}$ -incomplete, but not effectively if-essentially $\mathcal {Y}$ -incomplete.

• • Finally, by Theorem 4.8, we can find a computable $\mathcal {Z}$ such that U is effectively ef-essentially $[\mathcal {Z}]_U$ -incomplete w.r.t. N and $\rho $ , but not effectively ef-essentially $\mathcal {Z}$ -incomplete w.r.t. N and $\eta $ for all $\eta $ . By Theorem 4.7, U is effectively if-essentially $[\mathcal {Z}]_U$ -incomplete, and so by Corollary 3.2, we find that U is effectively if-essentially $\mathcal {Z}$ -incomplete.

We provide some versions of the converses of Theorems 4.2 and 4.7 when U and $\mathcal {X}$ satisfy a certain condition.

Theorem 4.10. Let U be a consistent c.e. theory and let N be an interpretation of $\mathsf {R}$ in U. Let $\mathcal {X}$ be a c.e. set of sentences. Suppose that we have a U-formula true such that $U \vdash \mathsf {true}(\ulcorner {\varphi }\urcorner ) \leftrightarrow \varphi $ , for all $\varphi \in \mathcal {X}$ . Then, the following are equivalent:

1. a. U is effectively ef-essentially $[\mathcal {X}]_U$ -incomplete w.r.t. N and $\xi $ for some $\xi $ .

2. b. U is effectively if-essentially $\mathcal {X}$ -incomplete.

3. c. U is effectively ef-essentially $\mathcal {X}$ -incomplete.

Proof “(a) to (b)”. This follows from Theorem 4.7 and Corollary 3.2.

“(b) to (c)”. By Theorem 4.2.

“(c) to (a)”. Let $\varPhi $ witness the effective ef-essential $\mathcal {X}$ -incompleteness of U. By the representability theorem, we find a formula $\mathsf {G}_\varPhi (x, y)$ representing $\varPhi $ in $\mathsf {R}$ . Define

$$\begin{align*}\xi(x):= \exists y\in \delta_N \, \big(\mathsf{G}^N_\varPhi(x, y) \land \mathsf{true}(y) \big).\end{align*}$$

We show that U is effectively ef-essentially $[\mathcal {X}]_U$ -incomplete w.r.t. N and $\xi $ . Suppose that $U \cup \{\varphi \}$ is consistent and, thus, $\varPhi (\varphi ) \in \mathcal {X}$ and $\varPhi (\varphi )$ is independent of $U \cup \{\varphi \}$ . We get

$$ \begin{align*} U \vdash \xi(\ulcorner{\varphi}\urcorner) & \leftrightarrow \exists y\in \delta_N \, \big(\mathsf{G}^N_\varPhi(\ulcorner{\varphi}\urcorner, y) \land \mathsf{true}(y) \big) \\ & \leftrightarrow \mathsf{true}(\ulcorner{\varPhi(\varphi)}\urcorner) \\ & \leftrightarrow \varPhi(\varphi). \end{align*} $$

Thus, $\xi (\ulcorner {\varphi }\urcorner )$ is also independent of $U \cup \{\varphi \}$ and we find $\xi (\ulcorner {\varphi }\urcorner ) \in [\mathcal {X}]_U$ .

Remark 4.11. One might wonder whether there is an infinitary version for the ef-notions. It seems that this will be non-trivial to attain. The reason is that we can use Craig’s trick to transform every index i effectively to an index $i^\ast $ , so that $(U+\mathsf {W}_i)_{{\mathfrak {p}}} = (U+\mathsf {W}_{i^\ast })_{{\mathfrak {p}}}$ and $\mathsf {W}_{i^\ast }$ is computable. We can even make $\mathsf {W}_{i^\ast }$ p-time decidable. In case U is a pair theory, we can even make $\mathsf {W}_{i^\ast }$ a scheme (see [23] or [25]). So, we would have to look for some really different notion of extension.

5 Heredity

In this section, we study what happens when we consider effective notions combined with hereditariness. Our main insight here is that an adapted version of Pour-El’s result also holds in this case.

Definition 5.1. A consistent c.e. theory U is effectively essentially hereditarily $\mathcal {X}$ -creative iff there exists a partial computable function $\varPhi $ such that for any $i, j, k \in \omega $ , if $\mathsf {W}_k$ is a consistent extension of U, $\mathsf {W}_{i}$ is a subtheory of $\mathsf {W}_k$ , and $\mathsf {W}_{i {\mathfrak {p}}} \cap \mathsf {W}_{j} = \emptyset $ , then $\varPhi (i, j, k)$ converges, $\varPhi (i, j, k) \in \mathcal {X}$ , and $\varPhi (i, j, k) \notin \mathsf {W}_{i {\mathfrak {p}}} \cup \mathsf {W}_j$ .

Lemma 5.2. For any consistent c.e. theory U, the following are equivalent:

1. i. U is effectively essentially hereditarily $\mathcal {X}$ -creative.

2. ii. There exists a partial computable function $\varPsi $ such that for any $i, j \in \omega $ , if $\mathsf {W}_{i}$ is a theory consistent with U and $\mathsf {W}_{i {\mathfrak {p}}} \cap \mathsf {W}_{j} = \emptyset $ , then $\varPsi (i, j)$ converges, $\varPsi (i, j) \in \mathcal {X}$ , and $\varPsi (i, j) \notin \mathsf {W}_{i {\mathfrak {p}}} \cup \mathsf {W}_{j}$ .

Proof “(i) to (ii)”. Let $\varPhi (i, j, k)$ be a partial computable function witnessing the effective essential hereditary creativity of U. We define a partial computable function $\varPsi $ by $\varPsi (i, j) : = \varPhi (i, j, k)$ , where k is an effectively found index of $(U \cup \mathsf {W}_{i})_{{\mathfrak {p}}}$ . It is easy to see that $\varPsi $ witnesses condition (ii).

“(ii) to (i)”. Let $\varPsi $ be a partial computable function that witnesses condition (ii). We define a partial computable function $\varPhi $ by $\varPhi (i, j, k) : = \varPsi (i, j)$ for all k. It is easy to see that $\varPhi $ witnesses the effective essential hereditary $\mathcal {X}$ -creativity of U.

Theorem 5.3. For any consistent c.e. theory U and set $\mathcal {X}$ of sentences, the following are equivalent:

1. a. U is strongly effectively $\mathcal {X}$ -inseparable.

2. b. U is effectively essentially hereditarily $\mathcal {X}$ -creative.

Proof “(a) to (b)”. Let $\varPhi $ be a partial computable function that witnesses the strong effective $\mathcal {X}$ -inseparability of U. Suppose that $U \cup \mathsf {W}_i$ is consistent and $\mathsf {W}_{i {\mathfrak {p}}} \cap \mathsf {W}_j = \emptyset $ . we can effectively find numbers $k_0$ and $k_1$ from i and j such that $\mathsf {W}_{k_0} = \mathsf {W}_{i {\mathfrak {p}}}$ and $\mathsf {W}_{k_1} = U_{{\mathfrak {r}}} \cup \mathsf {W}_j$ . Clearly, $\mathsf {W}_{k_0}$ and $\mathsf {W}_{k_1}$ biseparate $0_{U {\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ . By strong effective $\mathcal {X}$ -inseparability, $\varPhi (k_0, k_1)$ converges, $\varPhi (k_0, k_1) \in \mathcal {X}$ , and $\varPhi (k_0, k_1) \notin \mathsf {W}_{k_0} \cup \mathsf {W}_{k_1}$ . We take $\varPsi (i, j) : = \varPhi (k_0, k_1)$ . Then, $\varPsi $ satisfies Condition (ii) of Lemma 5.2, and, hence, U is effectively essentially hereditarily $\mathcal {X}$ -creative.

“(b) to (a)”. Suppose that U is effectively essentially hereditarily $\mathcal {X}$ -creative. Let $\varPsi $ be a partial computable function that witnesses Condition (ii) of Lemma 5.2. Suppose that $\mathsf {W}_{i}$ and $\mathsf {W}_{j}$ biseparate $0_{U {\mathfrak {p}}}$ and $U_{{\mathfrak {r}}}$ . By the Double Recursion Theorem with parameters (cf. [19, Exercise 3.15(b)]), we can effectively find numbers $k_0$ and $k_1$ from i and j such that:

• • $\mathsf {W}_{k_0} = \begin {cases} \{\varphi \}, & \text {if}\ \varPsi (k_0, k_1) \simeq \varphi \ \text {and}\ \varphi \in \mathsf {W}_{i}, \\ \emptyset , & \text {otherwise.}\end {cases}$

• • $\mathsf {W}_{k_1} = \begin {cases} \{\neg \, \varphi \}_{{\mathfrak {r}}}, & \text {if}\ \varPsi (k_0, k_1) \simeq \varphi \ \text {and}\ \varphi \in \mathsf {W}_{j},\\ 0_{U {\mathfrak {r}}}, & \text {otherwise.}\end {cases}$

Suppose, towards a contradiction, we have that $\varPsi (k_0, k_1) \simeq \varphi $ and $\varphi \in \mathsf {W}_{i} \cup \mathsf {W}_{j}$ .

• • If $\varphi \in \mathsf {W}_{i}$ , then $\mathsf {W}_{k_0} = \{\varphi \}$ and $\mathsf {W}_{k_1} = 0_{U {\mathfrak {r}}}$ . Since $\mathsf {W}_i \cap U_{{\mathfrak {r}}} = \emptyset $ , we have $\varphi \notin U_{{\mathfrak {r}}}$ , and hence $U \cup \mathsf {W}_{k_0}$ is consistent. If $\xi \in \mathsf {W}_{k_0 {\mathfrak {p}}} \cap \mathsf {W}_{k_1}$ for some $\xi $ , then $\varphi \vdash \xi $ and $0_U \vdash \neg \, \xi $ . This contradicts $\varphi \notin U_{{\mathfrak {r}}}$ . So, we find $\mathsf {W}_{k_0 {\mathfrak {p}}} \cap \mathsf {W}_{k_1} = \emptyset $ , and we obtain $\varphi = \varPsi (k_0, k_1) \notin \mathsf {W}_{k_0 {\mathfrak {p}}} \cup \mathsf {W}_{k_1}$ . This contradicts $\varphi \in \mathsf {W}_{k_0 {\mathfrak {p}}}$ .

• • If $\varphi \in \mathsf {W}_{j}$ , then $\mathsf {W}_{k_0} = \emptyset $ and $\mathsf {W}_{k_1} = \{\neg \, \varphi \}_{{\mathfrak {r}}}$ . If $\xi \in \mathsf {W}_{k_0 {\mathfrak {p}}} \cap \mathsf {W}_{k_1}$ for some $\xi $ , then $0_U \vdash \xi $ and $\neg \, \varphi \vdash \neg \, \xi $ . We obtain $\varphi \in 0_{U{\mathfrak {p}}}$ , and this contradicts $\mathsf {W}_j \cap 0_{U{\mathfrak {p}}} = \emptyset $ . Thus, we have $\mathsf {W}_{k_0 {\mathfrak {p}}} \cap \mathsf {W}_{k_1} = \emptyset $ . Since the theory $U \cup \mathsf {W}_{k_0} = U$ is consistent, we obtain $\varphi \notin \mathsf {W}_{k_0 {\mathfrak {p}}} \cup \mathsf {W}_{k_1}$ . This contradicts $\varphi \in \mathsf {W}_{k_1}$ .

We have shown $\mathsf {W}_{k_0} = \emptyset $ and $\mathsf {W}_{k_1} = 0_{U {\mathfrak {r}}}$ . Since $U \cup \mathsf {W}_{k_0}$ is consistent and $\mathsf {W}_{k_0 {\mathfrak {p}}} \cap \mathsf {W}_{k_1} = \emptyset $ , we obtain that $\varPsi (k_0, k_1)$ converges and $\varPsi (k_0, k_1) \in \mathcal {X}$ . We have also shown $\varPsi (k_0, k_1) \notin \mathsf {W}_i \cup \mathsf {W}_j$ . We take $\varPhi (i, j) : = \varPsi (k_0, k_1)$ . Thus, $\varPhi $ witnesses the strong effective $\mathcal {X}$ -inseparability of U.

We note that the proof in the (b) to (a) direction only employs finitely axiomatised theories.

We also study an adapted version of the result established in Section 3.2. We say that a theory U is strongly doubly $\mathcal {X}$ -generative iff there exists a total computable function $\varPhi $ such that for any $i, j \in \omega $ , if $\mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ , then:

• • $\varPhi (i, j) \in 0_{U {\mathfrak {p}}}$ iff $\varPhi (i, j) \in \mathsf {W}_j$ ,

• • $\varPhi (i, j) \in U_{{\mathfrak {r}}}$ iff $\varPhi (i, j) \in \mathsf {W}_i$ ,

• • if $\varPhi (i, j) \notin \mathsf {W}_i \cup \mathsf {W}_j$ , then $\varPhi (i, j) \in \mathcal {X}$ .

Theorem 5.4. For any consistent c.e. theory U, the following are equivalent:

1. a. U is strongly doubly $\mathcal {X}$ -generative.

2. b. U is effectively essentially hereditarily $\mathcal {X}$ -creative.

Proof “(a) to (b)”. Suppose that a total computable function $\varPhi $ witnesses the strong double $\mathcal {X}$ -generativity of U. Suppose that $\mathsf {W}_i$ is a theory consistent with U and $\mathsf {W}_{i {\mathfrak {p}}} \cap \mathsf {W}_j = \emptyset $ . We can effectively find k from i such that $\mathsf {W}_{k} =\mathsf {W}_{i {\mathfrak {p}}}$ . Since $\mathsf {W}_{k} \cap \mathsf {W}_{j} = \emptyset $ , we have that $\varPhi (k, j) \in 0_{U {\mathfrak {p}}}$ iff $\varPhi (k, j) \in \mathsf {W}_{j}$ ; and $\varPhi (k, j) \in U_{{\mathfrak {r}}}$ iff $\varPhi (k, j) \in \mathsf { W}_{i {\mathfrak {p}}}$ . Since $0_{U {\mathfrak {p}}} \cap \mathsf {W}_{j} = U_{{\mathfrak {r}}} \cap \mathsf {W}_{i {\mathfrak {p}}} = \emptyset $ , we obtain $\varPhi (k, j) \notin \mathsf {W}_{i {\mathfrak {p}}} \cup \mathsf {W}_{j}$ and $\varPhi (k, j) \in \mathcal {X}$ . We take $\varPsi (i, j) : = \varPhi (k, j)$ . Thus, $\varPsi $ satisfies Condition (ii) of Lemma 5.2. So, U is effectively essentially hereditarily $\mathcal {X}$ -creative.

“(b) to (a)”. Suppose that U is effectively essentially hereditarily $\mathcal {X}$ -creative. Let $\varPsi $ be a partial computable function that witnesses Condition (ii) of Lemma 5.2. We may assume that $\varPsi $ is a total function. By the Recursion Theorem with parameters, there exist total computable functions $\varTheta _0$ and $\varTheta _1$ such that, setting $\varPhi ^*(x, y) : = \varPsi (\varTheta _0(x, y), \varTheta _1(x, y))$ , we have:

$$\begin{align*}\mathsf{W}_{\varTheta_0(x, y)} = \begin{cases} \{\varPhi^*(x, y)\}, & \ \text{if}\ \big(\varPhi^*(x, y) \in (0_{U {\mathfrak {p}}} \cup \mathsf{W}_{x}) \big) \leq \big(\varPhi^*(x, y) \in (U_{{\mathfrak {r}}} \cup \mathsf{W}_{y}) \big),\\ \emptyset, & \ \text{otherwise}. \end{cases} \end{align*}$$

$$\begin{align*}\mathsf{W}_{\varTheta_1(x, y)} = \begin{cases} \{\neg\, \varPhi^*(x, y)\}_{{\mathfrak {r}}}, & \ \text{if}\ \big(\varPhi^*(x, y) \in (U_{{\mathfrak {r}}} \cup \mathsf{W}_{y}) \big) < \big(\varPhi^*(x, y) \in (0_{U {\mathfrak {p}}} \cup \mathsf{W}_{x}) \big), \\ 0_{U {\mathfrak {r}}}, & \ \text{otherwise}. \end{cases} \end{align*}$$

We show that $\varPhi ^*$ witnesses the strong double $\mathcal {X}$ -generativity of U. Let i and j be such that $\mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ . We set $\varphi ^\ast :=\varPhi ^*(i, j)$ .

• • Suppose $\big (\varphi ^\ast \in (0_{U {\mathfrak {p}}} \cup \mathsf {W}_{i}) \big ) \leq \big (\varphi ^\ast \in (U_{{\mathfrak {r}}} \cup \mathsf {W}_{j}) \big )$ holds. Then, $\mathsf {W}_{\varTheta _0(i, j)} = \{\varphi ^\ast \}$ and $\mathsf {W}_{\varTheta _1(i, j)} = 0_{U {\mathfrak {r}}}$ . Since,

  $$\begin{align*}\varPsi(\varTheta_0(i, j), \varTheta_1(i, j)) = \varphi^\ast \in \mathsf{W}_{\varTheta_0(i, j) {\mathfrak {p}}} \subseteq \mathsf{W}_{\varTheta_0(i, j) {\mathfrak {p}}} \cup \mathsf{W}_{\varTheta_1(i, j)},\end{align*}$$
  by Condition (ii) of Lemma 5.2, we have that (I) $\mathsf {W}_{\varTheta _0(i, j)}$ is inconsistent with U or (II) $\mathsf {W}_{\varTheta _0(i, j) {\mathfrak {p}}} \cap \mathsf {W}_{\varTheta _1(i, j)} \neq \emptyset $ . If (I) holds, then $\varphi ^\ast \in U_{{\mathfrak {r}}}$ . If (II) holds, then $\varphi ^\ast \vdash \xi $ and $0_U \vdash \neg \, \xi $ , for some $\xi $ , and hence $\varphi ^\ast \in 0_{U {\mathfrak {r}}} \subseteq U_{{\mathfrak {r}}}$ . Therefore, in either case, $\varphi ^\ast \in U_{{\mathfrak {r}}}$ . Since, $0_{U {\mathfrak {p}}} \cap U_{{\mathfrak {r}}} = \mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ and $\varphi ^\ast \in \mathsf {W}_i \cup 0_{U {\mathfrak {p}}}$ , we obtain $\varphi ^\ast \notin 0_{U {\mathfrak {p}}} \cup \mathsf {W}_j$ and $\varphi ^\ast \in U_{{\mathfrak {r}}} \cap \mathsf {W}_i$ .

• • Suppose $\big (\varphi ^\ast \in (U_{{\mathfrak {r}}} \cup \mathsf {W}_{j}) \big ) < \big (\varphi ^\ast \in (0_{U {\mathfrak {p}}} \cup \mathsf {W}_{i}) \big )$ holds. Then, $\mathsf {W}_{\varTheta _0(i, j)} = \emptyset $ and $\mathsf {W}_{\varTheta _1(i, j)} = \{\neg \, \varphi ^\ast \}_{{\mathfrak {r}}}$ . Since $\mathsf {W}_{\varTheta _0(i, j)}$ is consistent with U and

  $$\begin{align*}\varPsi(\varTheta_0(i, j), \varTheta_1(i, j)) = \varphi^\ast \in \mathsf{W}_{\varTheta_1(i, j)} \subseteq \mathsf{W}_{\varTheta_0(i, j) {\mathfrak {p}}} \cup \mathsf{W}_{\varTheta_1(i, j)},\end{align*}$$
  by Condition (ii) of Lemma 5.2, we have that $\xi \in \mathsf {W}_{\varTheta _0(i, j) {\mathfrak {p}}} \cap \mathsf {W}_{\varTheta _1(i, j)}$ for some $\xi $ . Then $0_U \vdash \xi $ and $\neg \, \varphi ^\ast \vdash \neg \, \xi $ , and hence $\varphi ^\ast \in 0_{U {\mathfrak {p}}}$ . Since, $0_{U {\mathfrak {p}}} \cap U_{{\mathfrak {r}}} = \mathsf {W}_i \cap \mathsf {W}_j = \emptyset $ and $\varphi ^\ast \in U_{{\mathfrak {r}}}\cup \mathsf {W}_j$ , we obtain that ${\varphi ^\ast \in 0_{U {\mathfrak {p}}} \cap \mathsf {W}_j}$ and $\varphi ^\ast \notin U_{{\mathfrak {r}}} \cup \mathsf {W}_i$ .

• • Otherwise, $\varphi ^\ast \notin 0_{U {\mathfrak {p}}} \cup \mathsf {W}_j$ and $\varphi ^\ast \notin U_{{\mathfrak {r}}} \cup \mathsf {W}_i$ . In this case, $\mathsf {W}_{\varTheta _0(i, j)} = \emptyset $ and $\mathsf {W}_{\varTheta _1(i, j)} = 0_{U {\mathfrak {r}}}$ . Since $\mathsf {W}_{\varTheta _0(i, j)}$ is consistent both with U and $\mathsf {W}_{\varTheta _0(i, j) {\mathfrak {p}}} \cap \mathsf {W}_{\varTheta _1(i, j)} = \emptyset $ , we obtain $\varphi ^\ast = \varPsi (\varTheta _0(i, j), \varTheta _1(i, j)) \in \mathcal {X}$ .

Thus, $\varPhi ^*$ witnesses the strong double $\mathcal {X}$ -generativity of U.

We prove a closure property for strong effective inseparability. For a theory U and formula classes $\mathcal {X}$ and $\mathcal {Y}$ , we write:

• • $\mathcal {X} \wedge \mathcal {Y}$ for $\{ (\varphi \wedge \psi )\mid \varphi \in \mathcal {X}\text { and } \psi \in \mathcal {Y} \}$ .

• • iff, for all $\varphi \in \mathcal {X}$ , we have $\varphi \vdash U$ .

Theorem 5.5. Suppose . Suppose further that U is $\mathcal {X}$ -creative and effectively $\mathcal {Y}$ -inseparable. Then, U is strongly effectively $\mathcal {X}\wedge \mathcal {Y}$ -inseparable.

Proof Suppose . Let U be $\mathcal {X}$ -creative and effectively $\mathcal {Y}$ -inseparable. Suppose $\mathsf {W}_i$ and $\mathsf {W}_j$ bi-separate $U_{{\mathfrak {p}}}$ and $0_{U{\mathfrak {r}}}$ .

Let $\mathcal {W} := \{ \psi \mid \exists \varphi \in \mathsf {W}_j\; U \cup \{\psi \} \vdash \varphi \}$ . Suppose $\psi \in U_{{\mathfrak {p}}}\cap \mathcal {W}$ . Then, for some $\varphi \in \mathsf {W}_j$ , we have $U \cup \{\psi \} \vdash \varphi $ and $U \vdash \psi $ . So, $U \vdash \varphi $ . Quod non. By $\mathcal {X}$ -creativity, we can effectively find a $\varphi ^\ast \in \mathcal {X}$ such that $\varphi ^\ast \not \in U_{{\mathfrak {p}}} \cup \mathcal {W}$ . We claim that (†) $\{ \varphi ^\ast \}_{{\mathfrak {p}}} \cap \mathsf {W}_j = \emptyset $ . If not, $\varphi ^\ast \vdash \chi $ , for some $\chi \in \mathsf {W}_j$ . So, a fortiori, $\varphi ^\ast \in \mathcal {W}$ . Quod non.

Let $\mathsf {W}_{i^\ast } := \{ \psi \mid (\varphi ^\ast \wedge \psi ) \in \mathsf {W}_i \}\cup \{ \varphi ^\ast \}_{{\mathfrak {p}}}$ and

$$ \begin{align*} \mathsf {W}_{j^\ast } := \{ \psi \mid (\varphi ^\ast \wedge \psi ) \in \mathsf {W}_j \}.\ \textrm{Suppose}\ \psi \in \mathsf {W}_{i^\ast } \cap \mathsf {W}_{j^\ast }.\end{align*} $$

Then $\varphi ^\ast \vdash \psi $ and $(\varphi ^\ast \wedge \psi ) \in \mathsf {W}_j$ . It follows that $(\varphi ^\ast \wedge \psi ) \in \{ \varphi ^\ast \}_{{\mathfrak {p}}} \cap \mathsf {W}_j $ . Quod non, by (†). Since $\varphi ^\ast \in \mathcal {X}$ , we find that $U_{{\mathfrak {p}}} \subseteq \{ \varphi ^\ast \}_{{\mathfrak {p}}} \subseteq \mathsf {W}_{i^\ast }$ . We have

$$ \begin{align*} \varphi \in U_{{\mathfrak {r}}} & \Rightarrow \varphi^\ast \vdash \neg\,\varphi \\ & \Rightarrow 0_U \vdash \neg \,(\varphi^\ast \wedge \varphi) \\ & \Rightarrow (\varphi^\ast \wedge \varphi)\in 0_{U{\mathfrak {r}}} \\ & \Rightarrow (\varphi^\ast \wedge \varphi)\in \mathsf{W}_j \\ & \Rightarrow \varphi\in \mathsf{W}_{j^\ast}. \end{align*} $$

So $U_{{\mathfrak {r}}} \subseteq \mathsf {W}_{j^\ast }$ .

We can effectively find a $\psi ^\ast \in \mathcal {Y}$ , such that $\psi ^\ast \not \in \mathsf {W}_{i^\ast }\cup \mathsf {W}_{j^\ast }$ . So, we have $(\varphi ^\ast \wedge \psi ^\ast ) \not \in \mathsf {W}_i \cup \mathsf {W}_j$ and $(\varphi ^\ast \wedge \psi ^\ast )\in \mathcal {X} \wedge \mathcal {Y}$ .

Example 5.6. The strong effective inseparability of the theory $\mathsf {R}$ was proved by Vaught [22, 5.2]. In [9, Theorem 2.4], the authors provided new proofs of this fact. Here, we give a proof of this fact in terms of Theorem 5.5, based on the method developed in [9]. In [9, Generalised Certified Extension Theorem], it is proved that for any $\Sigma _1$ -sentence $\sigma $ , we can effectively find a sentence $[\sigma ]$ satisfying the following conditions:

1. i. $[\sigma ] \vdash \sigma $ ,

2. ii. if $\sigma $ is true, then $\mathsf {R} \vdash [\sigma ]$ ,

3. iii. if $\sigma $ is false, then $[\sigma ] \vdash \mathsf {R}$ .

Let $\mathcal {X} = \{\varphi \mid \varphi \vdash \mathsf {R}\}$ , then . Since $\mathsf {R}$ is not finitely axiomatisable, we have $\mathsf {R}_{{\mathfrak {p}}} \cap \mathcal {X} = \emptyset $ . We show that $\mathsf {R}$ is $\mathcal {X}$ -creative. Let $\mathsf {W}_i$ be any c.e. set disjoint from $\mathsf {R}_{{\mathfrak {p}}}$ . From i, we effectively find a $\Sigma _1$ sentence $\rho $ satisfying

$$\begin{align*}\mathsf{R} \vdash \rho \leftrightarrow [\rho] \in \mathsf{W}_i. \end{align*}$$

If $\rho $ were true, then $[\rho ] \in \mathsf {W}_i$ . Also by (ii), $[\rho ] \in \mathsf {R}_{{\mathfrak {p}}}$ , a contradiction. Thus, $\rho $ is false, which implies $[\rho ] \notin \mathsf {W}_i$ . By (iii), we get $[\rho ] \vdash \mathsf {R}$ , and so we find $[\rho ] \in \mathcal {X}$ . Since $\mathsf {R}_{{\mathfrak {p}}} \cap \mathcal {X} = \emptyset $ , we also have $[\rho ] \notin \mathsf {R}_{{\mathfrak {p}}}$ . Then, the partial computable function $\varPhi $ defined by $\varPhi (i) : = [\sigma ]$ witnesses the $\mathcal {X}$ -creativity of $\mathsf {R}$ .

Since $\mathsf {R}$ is effectively $\mathsf {sent}$ -inseparable, by Theorem 5.5, we have that $\mathsf {R}$ is strongly effectively $(\mathcal {X} \land \mathsf {sent})$ -inseparable.

It is known that there exists a consistent c.e. theory which is effectively inseparable but is not essentially hereditarily undecidable (see [28, Example 6]). Relating to this example, we propose the following problem.

Figure 2 Implications between effective notions.

Problem 5.7. For any effectively inseparable consistent c.e. theory U, can we find a formula class $\mathcal {X}$ such that U is effectively $\mathcal {X}$ -inseparable but not strongly effectively $\mathcal {X}$ -inseparable?

The relationships between effective notions we have considered so far are visualised in Figure 2.