Very Weak, Essentially Undecidabile Set Theories? ?? Domenico Cantone1[0000−0002−1306−1166] , Eugenio G. Omodeo2[0000−0003−3917−1942] , and Mattia Panettiere1[0000−0002−9218−5449] 1 Dept. of Mathematics and Computer Science, University of Catania, Italy domenico.cantone@unict.it, mattia.panettiere@gmail.com 2 Dept. of Mathematics and Earth Sciences, University of Trieste, Italy eomodeo@units.it Abstract. In a first-order theory Θ, the decision problem for a class of formulae Φ is solvable if there is an algorithmic procedure that can assess whether or not the existential closure ϕ∃ of ϕ belongs to Θ, for any ϕ ∈ Φ. In 1988, Parlamento and Policriti already showed how to apply Gödel-like arguments to a very weak axiomatic set theory, with respect to the class of Σ1 -formulae with (∀∃∀)0 -matrix, i.e., existential closures of formulae that contain just restricted quantifiers of the kind (∀x ∈ y) and (∃x ∈ y) and are writeable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a ‘∀’). While revisiting their work, we show slightly stronger theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (∀∃)0 -matrices, namely formulae with at most one alternation of restricted quantifiers. Keywords: Decidability · Set Theory · Gödel Incompleteness. Introduction One often resorts to meta-level reasoning within a formal system, in order to support meta-mathematical investigations (e.g., concerning syntactic boundaries beyond which the decision problem for an axiomatic theory becomes algorith- mically unsolvable), meta-programming in declarative languages [4], or agent- based explainable AI applications (if the agents are to exhibit self-awareness of any form [2]). The resources that a first-order theory must provide to make meta-level rea- soning doable at all are surprisingly simple. In the realm of number theory, a ? Copyright c 2021 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). ?? We gratefully acknowledge partial support from project “STORAGE—Università degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, and from INdAM-GNCS 2019 and 2020 research funds. minimal arithmetic (extremely weak relative to Peano’s arithmetic) was pro- posed by Raphael M. Robinson in [11]; in the realm of set theory, an even simpler axiomatic endowment (only consisting of the null-set axiom along with an axiom enabling the adjunction of a single element to a set) was proposed by Robert L. Vaught in [13]. In either case, the proposed axiom system consti- tutes an essentially undecidable theory, i.e., a theory none of whose consistent axiomatic extensions has an algorithmically solvable derivability problem—as can be proved à la Gödel. Vaught’s result can be improved in at least two ways: (1) by making all steps needed for the so-called ‘arithmetization of syntax’ task more transparent; (2) by basing such a task on formulae of an extremely low syntactic structure. Franco Parlamento and Alberto Policriti contributed to these two amelioration goals [10,9], referring as a yardstick for measuring syntactical complexity to the number of quantifier alternations in the lowest level of Azriel Lévy’s hierarchy of set-theoretic formulae [6]. The axiom system that they exploited was still finite but slightly broader than the one by Vaught. This paper further develops the techniques by Parlamento and Policriti, by broadening the axiomatic system even further in order to achieve greater trans- parency and to reduce by one the number of quantifier alternations. The decision problem for a class of formulae Φ of the language of a given theory Θ—a consistent axiomatic set theory in the ongoing—is said to be solvable when there is an algorithmic procedure that, taken in input any ϕ ∈ Φ with n free variables x1 , x2 , . . . , xn , establishes whether or not Θ ` ∃x1 ∃x2 · · · ∃xn ϕ holds, and outputs: true if things are so, false if Θ 6` ∃x1 ∃x2 · · · ∃xn ϕ (in particular if Θ ` ¬∃x1 ∃x2 · · · ∃xn ϕ). While studying (un)decidability in fragments of set theory, it is worth considering restricted quantifiers, i.e., quantifiers of the form: Def (∀x ∈ y)ϕ ←→ ∀x(x ∈ y → ϕ) , Def (1) (∃x ∈ y)ϕ ←→ ∃x(x ∈ y ∧ ϕ) . When a formula contains only restricted quantifiers, it is called a ∆0 -formula (see [6]). Furthermore, if it is logically equivalent to some prenex formula with n alternating sequences of unbounded quantifiers in the prefix starting with uni- versal quantifiers, then it is called (∀∃∀ · · · Qn )0 (where Qi is ∀ when i is odd, and ∃ otherwise). Clearly, a complete theory is decidable; but the converse also holds when we restrict ourselves to consistent classes of existential closures of ∆0 -formulae. In [10], it has been investigated how, taking the very weak set theory T0 comprising extensionality, null-set axiom, single-element addition and removal axioms, an argument akin to the ones leading to Gödel incompleteness theorems can be applied to the class of (∀∃∀)0 -formulae. Thanks to those argu- ments, it is possible to show that every recursively axiomatizable extension Θ of T0 is incomplete with respect to the class of (∀∃∀)0 -formulae, and therefore the decision problem for that class is undecidable in every extension Θ of T0 . Since the base theory T0 is extremely elementary, the argument applies to every reasonable set theory. The limit found in [10] on the ∆0 -complexity of the class of formulae seems to be rather tight, with no room for improvement in that di- rection. Nevertheless, by slightly expanding the axiomatic core, we have found a way to lower that limit under suitable conditions. Indeed, we consider extensions of T0 that include the axiom of foundation and prove that if the concept of “be- ing a natural number” is expressible by a (∀∃)0 -formula, then the incompleteness arguments can be generalized with respect to the whole class of (∀∃)0 -formulae. At the end we will cite two examples that allow for such arguments, expanding the core theory with either the separation axiom schema or an axiom stating that every set is (hereditarily) finite. 1 A succinct axiomatic endowment for Set Theory We will consider the first-order language L∈ endowed with: – an infinite supply ν0 , ν1 , ν2 , . . . of set variables; – two dyadic relators ∈, =, designating membership and equality, respectively, as the only predicate symbols of the language; – the propositional connectives ¬ (monadic) and → (dyadic), designating re- spectively: negation and material implication; – the existential quantifier ∃ νi and the universal quantifier ∀ νi , associated with each set variable νi . The combinatorial core, dubbed T , of the axiomatic set theories we will consider consists of the following five postulates:  Extensionality (E) ∀ x ∀ y ∃ v ( v ∈ x ↔ v ∈ y ) → x = y , Null set (N) ∃ z ∀ v ¬v ∈ z ,  Adjunction (W) ∀ x ∀ y ∃ w ∀ v v ∈ w ↔ ( v ∈ x ∨ v = y ) , Removal (L) ∀ x ∀ y ∃ ` ∀ v v ∈ ` ↔ ( v ∈ x ∧ ¬v = y )  , Regularity (R) ∀ x ∃ v ∀ y y ∈ x → ( v ∈ x ∧ ¬y ∈ v ) . In the light of axiom (E), stating that distinct sets cannot have the same ele- ments, axiom (N) ensures that exactly one empty set exist. Axiom (W) and ax- with less iom (L) induce the two natural operations (x, y) 7→ x∪{y} and (x, y) 7→ x\{y}. Axiom (R) states that every non-empty set x has an element v that does not intersect x; in synergy with (N) and (W), it ensures that ‘∈’ forms no cycles. On occasions we will consider extending T with further axioms: a theory we will consider is Tf , whose intended universe encompasses no infinite sets (cf. [12]); another one is Ts , enhancing T with the separation axiom schema (cf. [5]). 2 Ordered pairs, functions, and natural numbers At the core of our definitional machinery lie the definitions of (un)ordered pair and (un)ordered functions. Indeed, most of the definitions hinge on an extensive use of these set-theoretic structures to lower their ∆0 -complexity. Consider, e.g., the variant hx, yi := {x, {x, y}} of Kuratowski’s classical ordered pair definition, which one can adopt under (N), (W), and (R). This is problematic since, while the extraction of the first component π1 (p) of such a pair p is specifiable by means of an (∃)0 -formula, the extraction of the second projection π2 (p) calls for a formula with at least one quantifier alternation: Def  y = π2 (p) ←→ (∃x ∈ p)(∃q ∈ p) x ∈ q ∧ y ∈ q ∧ (∀z ∈ q)(z = x ∨ z = y) . We rely on a definition that works under (E), (N), (W), and (L)—foundation is not required—introduced in [3]. We use the binary operator @ to construct quasi-pairs. These will be used in the formation of ordered pairs:  x@ y := x less y , x with y , hx, yi := (x@y)@ x . Definition 1. Quasi-pairs and ordered pairs are characterized by the following (∀∃)0 -conjunctions: Def QPair(q) ←→ (∃ u ∈ q)(∃ v ∈ q) ¬ u = v ∧ (∀ u, v ∈ q)(∀ t ∈ u)(∀ x ∈ v) (x ∈ u ∨ t ∈ v) ∧ (∀ u, v ∈ q)(∀ x, z ∈ v) (x ∈ u ∨ z ∈ u ∨ x = z) , Def OPair(p) ←→ QPair(p) ∧ (∃ d ∈ p)(∃ u, v ∈ d)¬ u = v ∧ (∀ d ∈ p)(∀ u, v ∈ d)(∀ t ∈ u)(∀ y ∈ v)(y ∈ u ∨ t ∈ v) ∧ (∀ d ∈ p)(∀ u, v ∈ d)(∀ y, z ∈ v)(y ∈ u ∨ z ∈ u ∨ y = z) . We use the first projection extraction on quasi-pairs to obtain the components of ordered pairs, aka 2-tuples, through these (∃)0 -specifications:3 Def x = π12 (p) ←→ (∃ u ∈ p)(∃ v ∈ p)( x ∈ v ∧ ¬ x ∈ u ) , Def y = π22 (p) ←→ (∃ d ∈ p) y = π12 (d). n-tuples and their projections πin (0 < i ≤ n), specified as usual in terms of 2-tuples for any n, can thus be captured by (∀∃)0 - and (∃)0 -formulae, resp.; e.g.: Def Triple(t) ←→ OPair(t) ∧ (∀v1 ∈ t)(∀v2 ∈ v1 )(∀s ∈ v2 )(s = π22 (t) → OPair(s)), Def x = π13 (t) ←→ x = π12 (t), Def y = π23 (t) ←→ (∃v1 ∈ t)(∃v2 ∈ v1 )(∃s ∈ v2 )(s = π22 (t) ∧ y = π12 (s)), Def z = π33 (t) ←→ (∃v1 ∈ t)(∃v2 ∈ v1 )(∃s ∈ v2 )(s = π22 (t) ∧ z = π22 (s)). Functions. Letting ∈1 ≡ ∈, it will be handy to make use of the following recursive definition of ∈n , for n ≥ 1 and for every variable y and formula ϕ: Def (∀x ∈n+1 y)ϕ ←→ (∀z ∈ y)(∀x ∈n z)ϕ . 3 In specifying projections, it would be pointless to insist that the argument must be an OPair. We can define functions in the classical way, namely as suitable sets of ordered pairs; their specification is straightforward: Def Fun(f ) ←→ (∀p ∈ f )OPair(p) ∧ (∀p1 , p2 ∈ f )(∀x ∈3 f )(x = π12 (p1 ) = π12 (p2 ) → p1 = p2 ). Often we will write (∀x ∈ dom f )ϕ in place of (∀x ∈3 f )(x ∈ dom f → ϕ) and (∀y ∈ π12 [dom f])ϕ in place of (∀p ∈ f )(∀y ∈5 f )(∀x ∈3 f ) (y = π12 (x) ∧ x ∈ dom f ) → ϕ , when f is a function and we want to quantify over the first projection of the elements of its domain. In general, to increase clarity, these compact versions of restricted quantifiers will be used, with their meanings being explicit, even though not specified. When s is a set of n-tuples, we will write πin [s] to intend the set of the i-th projections of all elements of s, namely Def x ∈ πin [s] ←→ (∃t ∈ s) x = πin (t) . We will also make use of the following function related notions, which work only under the assumption that f is a function: Def x ∈ dom f ←→ (∃p ∈ f )x = π1 (p) , (∃)0 Def d = dom f ←→ (∀x ∈ d)(x ∈ dom f ) ∧ (∀x ∈ dom f )(x ∈ d) , (∀∃)0 Def x ∈ ran f ←→ (∃p ∈ f )x = π22 (p) , (∃)0 Def y = f (x) ←→ (∃p ∈ f )(x = π12 (p) ∧ y = π22 (p)) , (∃)0 Def v ∈ f (x) ←→ (∃y ∈ ran f )(y = f (x) ∧ v ∈ y) , (∃)0 Def Fun(f (x)) ←→ (∀y ∈ ran f )(y = f (x) → Fun(y)) , (∀∃)0 Def v ∈ dom f (x) ←→ (∃y ∈ ran f )(y = f (x) ∧ v ∈ dom y) , (∃)0 Def f (x) = g(y) ←→ (∀v ∈ ran f )(∀w ∈ ran f )(v = f (x) ∧ w = g(y) → v = w). (∀)0 Similar predicates, not listed here, will be used throughout. Natural numbers are classically represented as finite ordinals. Whilst the defi- nition of ordinals is (∀)0 , hence it has a very low syntactic complexity (in the sense explained in the Introduction), expressing their finitude in weak theories requires more effort. We put: Def s = ∅ ←→ (∀x ∈ s)x 6= x, (∀)0 Def t = s+ ←→ (∀x ∈ t)(x = s ∨ x ∈ s), (∀)0 Def t = s− ←→ (s = t+ ) ∨ (t = ∅ ∧ s = ∅), (∀)0 where s+ := s ∪ {s} and s− are, resp., the successor and the predecessor of s. Under (E), (N), (W), (L), and (R), naturals are expressed by the following (∀∃∀)0 -specifications: Def Trans(X) ←→ (∀ v ∈ X) (∀ u ∈ v) u ∈ X , Def  Ord(X) ←→ Trans(X) ∧ (∀ u, v ∈ X) u ∈ v ∨ v ∈ u ∨ v = u , Def Num(X) ←→ (∀ t ∈ X) (∃ y ∈ X) (∀ u ∈ X) ( u = y ∨ u ∈ y ) ∧ (∀ y ∈ X) (∀ t ∈ y) (∃ z ∈ y) (∀ u ∈ y) ( u = z ∨ u ∈ z ) ∧ Ord(X). In Ts , namely under the separation axiom schema (Sep), the latter can be sim- plified into the following simpler (∀∃∀)0 -formula: Def Num(X) ←→ (∀ y ∈ X + ) y = ∅ ∨ (∃ z ∈ X) z + = y ∧  (∀ u, v ∈ X less ∅) ( u ∈ v ∨ v ∈ u ∨ v = u ) . Note that in Tf , Num coincides with Ord, and therefore belongs to the class (∀)0 . In other extensions of T , in order to lower the complexity of the ∆0 -specification of natural numbers, we must overload the structure of this property. We can think of natural numbers as specially constrained quadruples; specifically, we endow the classical finite ordinal with information on its predecessors and successors, allowing us to use existential formulae instead of universal ones to express them: Def Num(Q) ←→ Quadruple(Q) ∧ Fun(π4 (Q)) ∧ π1 (Q) = π2 (Q)− ∧ π3 (Q) = π2 (Q)+ ∧ (∀n ∈ π2 (Q))(Triple(π4 (Q)(n)) ∧ dom π4 (Q) = π2 (Q) ∧ (∀t ∈ ran π4 (Q))(π1 (t) = π2 (t)− ∧ π3 (t) = π2 (t)+ ) ∧  (∀y ∈ π3 (Q)) y = ∅ ∨ (∃z ∈ π2 (Q))π3 (π4 (Q)(z)) = y ∧ (∀u, v ∈ π2 (Q))(u ∈ v ∨ v ∈ u ∨ u = v). Here the definiendum requires that: (i) the second projection of a natural num- ber is a (finite) ordinal, (ii) its first and third projections are respectively the predecessor and successor of the second projection, (iii) its fourth projection is a function whose domain is the second projection mapping (finite) ordinals n to triples t such that π2 (t) = n, and (iv) the first and third projections of t are the predecessor and the successor of n respectively. Thanks to these conditions, statable with a single quantifier alternation, infinite ordinals are ruled out. All of the following definitions can be straightforwardly re-adapted to use this last (∀∃)0 -formula; however, to enhance readability we will continue to refer to our preceding characterizations of natural numbers in the definitions that follow. Given a numeral n, we can easily express the predicate x = n by means of a Σ1 -formula having a (∀)0 matrix: Vn−1 x = n ←→ (∃x0 ) · · · (∃xn−1 ) (x0 = ∅ ∧ i=1 xi = x+ Def + i−1 ∧ x = xn−1 ). The following claims are plain (cf. [10]): Lemma 1. In T , the following are provable: 1. (n)+ = n + 1, x = n ∧ y = x+ → y = n + 1, + 2. x = n + 1 → x = n, Num(x) → x 6< x, 3. Num(x) ∧ y ∈ x → Num(y), Num(x) ∧ Num(y) ∧ x 6= y → x+ 6= y + , 4. Num(x) ∧ Num(y) ∧ y ≤ x → x = y ∨ x < y, 5. Num(0), Num(n), Num(x) → Num(x+ ), ∀x(Num(x) → x 6< 0), 6. ∀x(Num(x) → x < n ∨ x = n ∨ n < x),  7. ∀x Num(x) → (x < n + 1 ↔ x = 0 ∨ · · · ∨ x = n) ; 8. if n < m, then T ` n < m; if n 6= m, then T ` n 6= m. Hereafter, we place ourselves in a generic extension T 0 of T , such as Ts , where a formal counterpart of the concept of natural number has been cast as a (∀∃)0 -formula. Provided that T 0 preserves the previous lemma (under retouched definitions), the following holds. Theorem 1 ([10]). Every total recursive n-ary function f on N := {0, 1, 2, . . . } is strongly representable in T 0 , in the sense that there is a formula ϕ such that for k1 , . . . , kn , k ∈ N: - f (k1 , . . . , kn ) = k implies T 0 ` ϕ(k 1 , .. . , k n , k), and - T 0 ` ∃ x ∀ y ϕ(k 1 , . . . , k n , y) ↔ y = x . 3 Codes We will revamp the original definition of code in [10] in order to give it a more explicit structure. Our codes are finite-length sequences that represent the syntax trees of formulae by means of a linear structure. As such, the first element is a natural number, whose presence allows us to use restricted quantifiers, while the remaining ones are triples that encode the nodes of the tree. Each triple contains the node type in the first component and either two leaves (variable nodes) or pointers to nodes previously appearing in the sequence. The last triple in the node is considered to be the root of the tree. Clearly, for each formula ϕ, there is a countable infinity of code sequences encoding ϕ. In addition, in order to be able to further simplify the definition, we will make use of unordered functions in our definitions. Definition 2 (Code sequence). Def SeqC (f ) ←→ Num(f (0)) ∧ dom(f ) ∈ f (0) ∧  (∀p ∈ f ) |p| ≤ 2 ∧ (∃x, y ∈ p)(x 6= y) ∧ (∀p ∈ f )(∀x, y ∈ p) x 6= y ∧ x 6= 0 ∧ y 6= 0  → y∈ /x ∧ x∈ / y ∧ Num(x) ∨ Num(y) . The third condition forces f to be a sequence of doubletons proper, whilst the fourth one establishes that each pair, each element of f , save 0 paired with its image, is made of a number and a non-number. The first two conjuncts state that the first element (height of the sequence) is a natural number and that the domain (length) of the sequence is bounded by it. The literal |p| ≤ 2 can plainly be expressed by (∀x, y, z ∈ p)(x = y ∨ y = z ∨ x = z). A natural specification ( for y = f x is: Def x ∈ domC f ←→ (∃p ∈ f )(∃u ∈ p)[x ∈ p ∧ x 6= u ∧ (x ∈ u ∨ 0 ∈ x)], Def ( y = f x ←→ x ∈ domC f ∧ (∃p ∈ f ) x, y ∈ p ∧ y 6= x ∧ (x ∈ y → x = 0), where x ∈ domC f means “x is in the unordered domain of the code sequence f ”. These two definitions have the desired meanings; in fact, as the length of any ( code is at least 2, its height must exceed 2. Hence 0 ∈ f 0 whenever SeqC (f ) holds. The basic principle that makes them work is that, thanks to regularity, it is always possible to prove that two naturals are comparable by membership under any definition we have considered. Combining this result with the fact that no ordered pair, and hence no triple, satisfies the predicate Num, it is always possible to distinguish the element in the range from the one in the domain. Thence, the complexity of the formula entirely depends on the complexity of Num: the formula is (∀∃)0 whenever Num is (∀∃)0 and (∀∃∀)0 when it is (∀∃∀)0 . ( We will often write fx instead of f x, and we will also make use of the following specification in the coming sections: Def y ∈ ranC f ←→ (∃p ∈ f )(∃x ∈ p)(x ∈ y ∨ 0 ∈ / y). Definition 3 (Code). Def Cod(f ) ←→ SeqC (f ) ∧ (∃p ∈ f )(∃q ∈ f )(p 6= q) ∧ (∀i ∈ domC f )[i 6= 0 → Triple(fi ) ∧ Symbol(π1 (fi )) ∧ ( ( (π2 (fi ) ∈ f 0 ∨ π2 (fi ) ∈ i) ∧ (π3 (fi ) ∈ f 0 ∨ π3 (fi ) ∈ i)]. We already noted that Triple is (∀∃)0 , and the last two conjuncts in the succedent of the implication are (∃)0 , hence it has the same ∆0 -complexity of SeqC . The first projection of a triple is a Symbol set, i.e., a set that represents a connective or a relator in L∈ . In practice, Symbol can be thought as Num, as we require just a countable amount of them. The second and third projections of the triples are either indices of variables (relative to their standard ordering ν0 , ν1 , ν2 , . . . ) or pointers to previous nodes. Pointers of previous nodes precede i, whilst we impose that the index of a variable shall be less than the height of the code. Note that this restriction does not reduce the power of codes, as it is sufficient to increase the height in order to be able to encode any variable. A total order on codes. The given definition, Cod(f ), of code implies a nat- ural total order on the class of codes. We put: Def (( (( ( ( f ≤C g ←→ [f 0 < g 0] ∨ [f 0 = g 0 ∧ domC f < domC g] ∨ f 0 = g 0 ∧ domC f = domC g ∧ (∀m ∈ domC f )([(∀i ∈ domC f )(m ∈ i → fi = gi ) ∧ ( (  f m 6= g m] → ϕless (f, g, m)) , where ϕless  (f, g, m) stands for:   π3 (fm )