In a rst-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 '9 of ' belongs to , for any ' 2 . In 1988, Parlamento and Policriti already showed how to apply Godel-like arguments to a very weak axiomatic set theory, with respect to the class of 1-formulae with (898)0-matrix, i.e., existential closures of formulae that contain just restricted quanti ers of the kind (8x 2 y) and (9x 2 y) and are writeable in prenex form with at most two alternations of restricted quanti ers (the outermost quanti er being a `8'). While revisiting their work, we show slightly stronger theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (89)0-matrices, namely formulae with at most one alternation of restricted quanti ers.
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 algorithmically unsolvable), meta-programming in declarative languages [4], or agentbased explainable AI applications (if the agents are to exhibit self-awareness of any form [2]).
The resources that a rst-order theory must provide to make meta-level reasoning doable at all are surprisingly simple. In the realm of number theory, a minimal arithmetic (extremely weak relative to Peano's arithmetic) was proposed 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 constitutes an essentially undecidable theory, i.e., a theory none of whose consistent axiomatic extensions has an algorithmically solvable derivability problem|as can be proved a la Godel.
Vaught's result can be improved in at least two ways: (
This paper further develops the techniques by Parlamento and Policriti, by broadening the axiomatic system even further in order to achieve greater transparency and to reduce by one the number of quanti er 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 ' 2 with n free variables x1; x2; : : : ; xn, establishes whether or not ` 9x19x2 9xn ' holds, and outputs: true if things are so, false if 6` 9x19x2 9xn ' (in particular if ` :9x19x2 9xn '). While studying (un)decidability in fragments of set theory, it is worth considering restricted quanti ers, i.e., quanti ers of the form: (8x 2 y)' (9x 2 y)'
D!ef 8x(x 2 y ! ') ;
D!ef 9x(x 2 y ^ ') :
(
We will consider the rst-order language L2 endowed with: { an in nite supply 0; 1; 2; : : : of set variables; { two dyadic relators 2; =, designating membership and equality, respectively, as the only predicate symbols of the language; { the propositional connectives : (monadic) and ! (dyadic), designating respectively: negation and material implication; { the existential quanti er 9 i and the universal quanti er 8 i, associated with each set variable i .
The combinatorial core, dubbed T , of the axiomatic set theories we will consider consists of the following ve postulates:
8 x 8 y 9 v ( v 2 x $ v 2 y ) ! x = y ;
9 z 8 v :v 2 z ; 8 x 8 y 9 w 8 v v 2 w $ ( v 2 x _ v = y ) ; 8 x 8 y 9 ` 8 v v 2 ` $ ( v 2 x ^ :v = y ) ;
8 x 9 v 8 y y 2 x ! ( v 2 x ^ :y 2 v ) : In the light of axiom (E), stating that distinct sets cannot have the same elements, axiom (N) ensures that exactly one empty set exist. Axiom (W) and axiom (L) induce the two natural operations (x; y) w7 !ith x[fyg and (x; y) l7 !ess xnfyg. 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 `2' 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 in nite sets (cf. [12]); another one is Ts, enhancing T with the separation axiom schema (cf. [5]). 2
At the core of our de nitional machinery lie the de nitions of (un)ordered pair
and (un)ordered functions. Indeed, most of the de nitions hinge on an extensive
use of these set-theoretic structures to lower their 0-complexity. Consider, e.g.,
the variant hx; yi := fx; fx; ygg of Kuratowski's classical ordered pair de nition,
which one can adopt under (N), (W), and (R). This is problematic since, while
the extraction of the rst component 1(p) of such a pair p is speci able by
means of an (
Def !
(9x 2 p)(9q 2 p) x 2 q ^ y 2 q ^ (8z 2 q)(z = x _ z = y) : We rely on a de nition 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:
(89)0-conjunctions:
QPair(q) OPair(p)
D!ef (9 u 2 q)(9 v 2 q) : u = v ^
(8 u; v 2 q)(8 t 2 u)(8 x 2 v) (x 2 u _ t 2 v) ^
(8 u; v 2 q)(8 x; z 2 v) (x 2 u _ z 2 u _ x = z) ;
D!ef QPair(p) ^ (9 d 2 p)(9 u; v 2 d): u = v ^
(8 d 2 p)(8 u; v 2 d)(8 t 2 u)(8 y 2 v)(y 2 u _ t 2 v) ^
(8 d 2 p)(8 u; v 2 d)(8 y; z 2 v)(y 2 u _ z 2 u _ y = z) :
We use the rst projection extraction on quasi-pairs to obtain the components
of ordered pairs, aka 2-tuples, through these (
Def
!
Def
!
(9 u 2 p)(9 v 2 p)( x 2 v ^ : x 2 u ) ;
(9 d 2 p) y = 12(d):
n-tuples and their projections in (0 < i n), speci ed as usual in terms of
2-tuples for any n, can thus be captured by (89)0- and (
Triple(t) D!ef OPair(t) ^ (8v1 2 t)(8v2 2 v1)(8s 2 v2)(s = 22(t) ! OPair(s)); x = 13(t) D!ef x = 12(t); y = 23(t) D!ef (9v1 2 t)(9v2 2 v1)(9s 2 v2)(s = 22(t) ^ y = 12(s)); z = 33(t) D!ef (9v1 2 t)(9v2 2 v1)(9s 2 v2)(s = 22(t) ^ z = 22(s)): Functions. Letting 21 2, it will be handy to make use of the following recursive de nition of 2n, for n 1 and for every variable y and formula ': (8x 2n+1 y)'
D!ef (8z 2 y)(8x 2n z)' : 3 In specifying projections, it would be pointless to insist that the argument must be an OPair.
We can de ne functions in the classical way, namely as suitable sets of ordered pairs; their speci cation is straightforward:
Fun(f )
D!ef (8p 2 f )OPair(p) ^ (8p1; p2 2 f )(8x 23 f )(x = 12(p1) = 12(p2) ! p1 = p2): Often we will write (8x 2 dom f )' in place of (8x 23 f )(x 2 dom f ! ') and (8y 2 12[dom f ])' in place of (8p 2 f )(8y 25 f )(8x 23 f ) (y = 12(x) ^ x 2 dom f ) ! ' , when f is a function and we want to quantify over the rst projection of the elements of its domain. In general, to increase clarity, these compact versions of restricted quanti ers will be used, with their meanings being explicit, even though not speci ed. 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 x 2 in[s]
Def
!
(9t 2 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:
x 2 dom f D!ef (9p 2 f )x = 1(p) ; (
Natural numbers are classically represented as nite ordinals. Whilst the de
nition of ordinals is (
D!ef (8x 2 s)x 6= x;
D!ef (8x 2 t)(x = s _ x 2 s);
D!ef (s = t+) _ (t = ? ^ s = ?);
(
Ord(X) Num(X)
D!ef (8 v 2 X) (8 u 2 v) u 2 X ; D!ef Trans(X) ^ (8 u; v 2 X) u 2 v _ v 2 u _ v = u ; D!ef (8 t 2 X) (9 y 2 X) (8 u 2 X) ( u = y _ u 2 y ) ^
(8 y 2 X) (8 t 2 y) (9 z 2 y) (8 u 2 y) ( u = z _ u 2 z ) ^ Ord(X): In Ts, namely under the separation axiom schema (Sep), the latter can be simpli ed into the following simpler (898)0-formula:
Num(X) D!ef (8 y 2 X+) y = ? _ (9 z 2 X) z+ = y ^
(8 u; v 2 X less ?) ( u 2 v _ v 2 u _ v = u ) :
Note that in Tf , Num coincides with Ord, and therefore belongs to the class (
D!ef (9x0) (9xn 1) (x0 = ? ^
Vin=11 xi = xi+ 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 2 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+), 8x(Num(x) ! x 6< 0), 6. 8x(Num(x) ! x < n _ x = n _ n < x), 7. 8x 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 (89)0-formula.
Provided that T 0 preserves the previous lemma (under retouched de nitions), the following holds.
Theorem 1 ([10]). Every total recursive n-ary function f on N := f0; 1; 2; : : : g is strongly representable in T 0, in the sense that there is a formula ' such that for k1; : : : ; kn; k 2 N: - f (k1; : : : ; kn) = k implies T 0 ` '(k1; : : : ; kn; k), and - T 0 ` 9 x 8 y '(k1; : : : ; kn; y) $ y = x . 3
We will revamp the original de nition of code in [10] in order to give it a more explicit structure. Our codes are nite-length sequences that represent the syntax trees of formulae by means of a linear structure. As such, the rst element is a natural number, whose presence allows us to use restricted quanti ers, while the remaining ones are triples that encode the nodes of the tree. Each triple contains the node type in the rst 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 in nity of code sequences encoding '.
In addition, in order to be able to further simplify the de nition, we will make use of unordered functions in our de nitions.
SeqC (f ) D!ef Num(f (0)) ^ dom(f ) 2 f (0) ^ (8p 2 f ) jpj 2 ^ (9x; y 2 p)(x 6= y) ^ (8p 2 f )(8x; y 2 p) x 6= y ^ x 6= 0 ^ y 6= 0 !
y 2= x ^ x 2= 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 rst two conjuncts state that the rst element (height of the sequence) is a natural number and that the domain (length) of the sequence is bounded by it. The literal jpj 2 can plainly be expressed by (8x; y; z 2 p)(x = y _ y = z _ x = z). A natural speci cation ( for y = f x is: x 2 domC f D!ef (9p 2 f )(9u 2 p)[x 2 p ^ x 6= u ^ (x 2 u _ 0 2 x)]; y = f(x D!ef x 2 domC f ^ (9p 2 f ) x; y 2 p ^ y 6= x ^ (x 2 y ! x = 0); where x 2 domC f means \x is in the unordered domain of the code sequence f ". These two de nitions have the desired meanings; in fact, as the length of any code is at least 2, its height must exceed 2. Hence 0 2 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 de nition we have considered. Combining this result with the fact that no ordered pair, and hence no triple, satis es 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 (89)0 whenever Num is (89)0 and (898)0 when it is (898)0. We will often write fx instead of f(x, and we will also make use of the following speci cation in the coming sections:
y 2 ranC f D!ef (9p 2 f )(9x 2 p)(x 2 y _ 0 2= y):
Cod(f )
D!ef SeqC (f ) ^ (9p 2 f )(9q 2 f )(p 6= q) ^ (8i 2 domC f()[i 6= 0 ! Triple(fi) ^ Symbo(l( 1(fi)) ^
( 2(fi) 2 f 0 _ 2(fi) 2 i) ^ ( 3(fi) 2 f 0 _ 3(fi) 2 i)]:
We already noted that Triple is (89)0, and the last two conjuncts in the succedent
of the implication are (
f m 6= g m] ! 'less(f; g; m)) ; 3(fm) = 3(gm) ^ 2(fm) < 2(gm) _ where 'less(f; g; m) stands for: 3(fm) <S 3(gm) _
3(fm) = 3(gm) ^ 2(fm) = 2(gm) ^ 1(fm) < 1(gm) :
By <S , we denote a strict total order on the class of symbols. Since the
projections of f can be extracted with (
The following proposition is trivially proved by contradiction:
C .
We can also explicitly de ne the strict variant of C with a (89)0-formula: f <C g D!ef f C g ^ (9p 2 g)(p 2= f ): We will now specify a successor function which allows us to enumerate the class of all the code sequences. To achieve simpler speci cations, we will consider ( natural numbers below f 0 as symbols. We have three cases: 1. There is some triple in which one of the values is not f(0 1: in this case, ( we interpret the sequence of all triples as a base f 0 {number and take its successor. 2. None of the triples can be increased, but the domain of the code is smaller than its height: in this case, the successor is the code which has the same height, one more triple, and whose triples are made up of zeroes. 3. Neither of the previous cases holds: in this case the successor has the height increased by one, and has just one triple of zeroes.
This informal de nition can be written as: g = NextC (f ) D!ef (C1) _(C2) _ (C3):
Condition (C1): We de ne two utility predicates. The rst one, y = NextT (x; c; v),
is true when y is the successor triple of x, thinking of x as a number in base
c. The variable v is conveniently used in the antecedent of the implications in
order to be able to write a (
CarryT (f; c; i) D!ef (8j 2 i)(8v1 2 1(ranC f ))(8v2 2 2(ranC f ))(8v3 2 3(ranC f )) (8u1 2 1(ranC f ))(8u2 2 2(ranC f ))(8u3 2 3(ranC f )) [j 6= 0 ^ v1 = 1(fj) ^ v2 = 2(fj) ^ v3 = 3(fj) ^
u1 = 1(fi) ^ u2 = 2(fi) ^ u3 = 3(fi) ! v1 = c ^ v2 = c ^ v3 = c ^ (u1 6= c _ u2 6= c _ u3 6= c)]: Now we are ready to produce a compact (89)0-speci cation of Condition (C1).
( (9m 2 domC f )(9y 2 f 0)[m 6= 0 ^ (( 1(fm+) 2 y _ 2(fm) 2 y _ 3(fm) 2 y)] ^ (8m 2 domC f )(8c 2 f(0)(8i 2 m)[f 0 = c ^ CarryT (f; c; m) ^
(8j 2 m)CarryT (f; c; j) ! fi = (0; 0; 0)] ^
(8(m 2 domC f )(8c 2 f(0)(8v1 2 1(ranC g))(8v2 2 2(ranC g))(8v3 2 3(ranC g)))
[f 0 = c+ ^ CarryT (f; c; m) ! gm = NextT (fm; c; v1) _ gm = NextT (fm; c; v2) _
gm = NextT (fm; c; v3)];
3(fi) = 0.
where fi = (0; 0; 0) is syntactic sugar for 1(fi) = 0 ^
2(fi) = 0 ^
Condition (C2): (C2) is a (89)0-formula:
(8x 2 domC(f )(8y 2(f(0)((f(0 = y+ ^ x 6= 0 ! fx = (y; y; y)) ^
domC f < f 0 ^ g 0 = f 0 ^ (domC f )+ = domC g ^
(8i 2 domC g)(i 6= 0 ! gi = (0; 0; 0)):
Condition (C3): With this last (89)0-condition, we cover every possible case:
(8x 2 domC f )(8y 2 f(0)(f(0 = y+ ^ x 6= 0 ! fx = (y; y; y)) ^
domC f = f(0 ^ g(0 = f(0+ ^ domC g = 2 ^ g(
The previous discussion readily yields Lemma 3. NextC (f ) is a (89)0-formula.
It is clear that starting from the code ff0; 3g; f1; h0; 0; 0igg, through successive application of NextC , we can enumerate all the codes, as, given a length and a height, there is a nite amount of codes with that length and height. The bottom code, 0C , is characterized by the (89)0-formula f = 0C
D!ef Cod(f ) ^ f0 = 2 ^ Triple(f1) ^
1(f1) = 0 ^ 2(f1) = 0 ^ 3(f1) = 0: Throughout the rest of the section, we will state some useful facts about codes that will be essential in developing an argument a la Godel within the weak set theories we are considering. As most of these facts admit proofs very similar to the ones available in [10], we will not provide details.
(a) 8x8y Cod(x) ^ NextC (x) = y ! Cod(y) ; (b) 8x8y8z Cod(x) ^ Cod(y) ^ Cod(z) ^ x C z ^ z C y ^ y = NextC (x) ! z = x _ z = y ; (c) 8x8y Cod(x) ^ Cod(y) ^ NextC (x) = y ! x <C y ; (d) 8x8y8z Cod(y) ^ NextC (y) = x ^ NextC (y) = z ! x = z . For every natural number k, by x = (k)C we mean: (9x0; : : : ; xk 1) x0 = 0C ^
Vik=01 xi+1 = NextC (xi) ^ x = xk :
(a) (k + 1)C = NextC ((k)C ); (b) x = (k)C ^ y = NextC (x) ! = (k)C ; (c) 8x(Cod(x) ^ (k + 1)C = NextC (x) ! x = (k)C ; (d) Cod((k)C ); (e) 8x Cod(x) ! : <C 0C ; (f ) 8x Cod(x) ! (x C (k)C $ x <C (k + 1)C ) ; (g) 8x Cod(x) ! (x <C (k + 1)C $ x = 0C _ : : : _ x = (k)C ) ; (h) 8x Cod(x) ! (x <C (k)C _ x = (k)C _ (k)C <C x) .
Corollary 1. For all natural numbers h and k, we have that if h = k, then T ` (h)C = (k)C ; if h < k, then T ` (h)C <C (k)C . 4
We require the following symbols (and the related identifying predicates): Symbol , ) Symbol8, Symbol2, Symbol=, and a renaming symbol for each variable vi, SymbolRi . The intent of the last predicate is to integrate a rename operator for each variable in the language. Each one of the symbols has two parameters, either variables or subformulae, thus we add predicates to recognize the type (the symbol on top of the syntax tree of the formula) of code sequences. Remember that the topmost node of the generation tree is the last element of a code sequence. We start by de ning predicates that recognize the function of a triple t of index i inside a code f of height c: impl(f; t; i; c) D!ef Symbol)( 1(t)) ^ 2(t) 2 i ^ 2(t) 6= 0 ^ 3(t) 2 i ^ 3(t) 6= 0; forall(f; t; i; c) D!ef Symbol8( 1(t)) ^ 2(t) < c ^ 3(t) < i ^ 3(t) 6= 0; rename(f; t; i; c) D!ef SymbolR ( 1(t)) ^ 2(t) < c ^ 3(t) < i ^ 3(t) 6= 0; equals(f; t; i; c) D!ef Symbol=( 1(t)) ^ 2(t) < c ^ 3(t) < c: in(f; t; i; c) D!ef Symbol2( 1(t)) ^ 2(t) < c ^ 3(t) < c:
All of these formulae are (
Form(f )
D!ef (8c 2 ranC f )(8i 2 domC f )(8t 2 ranC f )[c = f 0 ^ t = fi ! ( impl(f; t; i; c) _ forall(f; t; i; c) _ rename(f; t; i; c) _
equals(f; t; i; c) _ in(f; t; i; c)] ^ Cod(f ): The formula is clearly (89)0. We can also straightforwardly de ne predicate symbols for derived connectives and quanti ers as we can express ? as 8 v0(v0 2 v0) and thus :' as ' ! ?; accordingly, 9v' will stand for 8v(' ! ?) ! ?. Consider now the following axiomatization of rst-order logic with axioms: (A1) (((((' ! ) ! (( ! ?) ! ( ! ?))) ! ) ! ) ! (( ! ') ! ( ! '))) ; (A2) 8vi (' ! ) ! (' ! 8vi( )) (vi not free in ') ; (A3) 8vi('(vi) ! '(vj)) ; (A4) 8vi (' ! (8vi' ! ?)) ! ? ! ? ; (A5) x = x ; (A6) x = y ! ('(x) ! '(y)) : For each such schema, we can write a (89)0-formula that recognizes whether the code of a formula is in the schema. As the reader can check, most of these speci cations are rather trivial. However, the speci cations of (A2), (A3), and (A6) are more problematic. Formulae that are instances of the schema (A3) are captured by the following predicate A3: A3(f ) D!ef (8x 2 domC f )(8u 24 f )(8v 25 f )(8i 24 f )(8t 25 f ) x+ = domC f ^ 2(fx) = u ^ im3p(fl(xf); =fx;vx;^f(02)(f^u) f=oraill^(f; fu; u; f(0) ^ 3(fu) = t ! (9j 2 f(0)[renamei(f; fv; v; f(0) ^ t = 3(fi)] ^ Cod(f ): One can proceed similarly with (A6). As for (A2), we also need means to express whether a variable has free occurrences in a formula. While this problem is particularly hard to solve in general, it will be easy in the context in which it will be needed.
We are now able to de ne
LAxiom(f ) D!ef A1(f ) _ A2(f ) _ A3(f ) _ A4(f ) _ A5(f ) _ A6(f ); which recognizes whether the code of a formula is a rst-order logic axiom. Depending on the theory we are considering, we also have several theory axioms that are usually trivial to express. Using similar speci cations, one can de ne the TAxiom that holds whenever a formula code is an axiom in the theory. We also put:
Axiom(f ) D!ef LAxiom(f ) _ TAxiom(f ): We de ne next the two predicates that hold when f is a left or a right copy of g:
CLCopy(f; g) D!ef (8i 2 domf )(8x 2 2(ranf ))[x = 2(lastf ) ! (fi 2 ran g $
(9j 2 domf )(j x ^ PtBy(i; fj)) _ i = x)];
CRCopy(f; g) D!ef (8i 2 domf )(8x 2 2(ranf ))[x = 3(lastf ) ! (fi 2 ran g $
(9j 2 domf )(j x ^ PtBy(i; fj)) _ i = x)]:
The formula PtBy(i; t) holds when the triple t has a pointer to the ith node.
This is clearly an (
PtBy(i; t) Def !
Symbol)( 1(t)) ^ (i = 2(t) _ i = 3(t)) _ (Symbol8( 1(t)) ^ i = 3(t)) _ (SymbolR ( 1(t)) ^ i = 3(t)) : The temporary notation last f can be eliminated by means of the rewriting rules explained below: { add (8n 2 dom f ), involving a new n, in front of the quanti cational pre x; { conjoin n+ = dom f with the antecedent of the matrix; { replace every occurrence of last f by the term fn.
The added complexity depends on the complexity of checking n+ = dom f that
normally has a 89-pre x. Although this would yield a (898)0-formula, we will
use it in a context in which we will be able to rewrite it as an (98)0-formula,
hence we will be able to write the two predicates with (89)0-formulae.
Given a code c, in order to recognize bound variables, we will consider a sequence
of the same length that contains the bound variables in each triple (subformula).
The following (89)0-predicate establishes that b is the bound list of a code c:
BoundList(b; c) D!ef Fun(b) ^ dom b = domC c ^
(8i 2 domC c)(8j 2 domC c)(PtBy(i; bj) ! bj
bi) ^
(8i 2 domC c)(8v 24 b) v 2 bi $
(9j 2 domC c)(PtBy(i; bj) ^ v 2 bj) _
(Symbol8( 1(fi)) ^
2(fi) = v) ;
where bi bj is a shorthand for (8x 2 bi)x 2 bj , so that BoundList(b; c) is clearly
(89)0. When BoundList(b; c) holds and we encounter a variable v in some triple
ci, it is su cient to check if v 2 bi holds in order to know whether v is bound.
Proofs. Accessing the domain and the predecessor of a natural number can be
done with a (89)0- and a (
The idea is that a proof is a sequence composed of three parts: (i) a value at index 0 that contains the point in the sequence that separates the other two parts; (ii) a list of triples, one for each one of the subformulae of the formulae that occur in the proof, that contain the subformula in the rst projection, a copy of the left child in the second, and a copy of the right child in the third ( ( (between index 1 and f 0 - 1); and (iii) a list of indices between 1 and f 0 that point to the formulae that are supposed to be the steps of the proof. We also ll a list of bound variables for each of the subformulae in order to be able to always tell which variables are bound in a given formula.
Proof0(f; x; p; d; df ; b) Def
! Fun(f ) ^ Num(domf ) ^ Num(f (0)) ^ f (0) 2 domf ^ df = domf Fun(p) ^ dom p = domf ^ (8i 2 dom p)(i 6= 0 ! pi = i ) ^ Fun(d) ^ dom d = domf ^ (8i 2 dom d)(f (0) 2 i ! di = dom fi) ^ (8i 2 f (0))[Triple(fi) ^ Form( 1(fi)) ^ Form( 2(fi)) ^ Form( 3(fi)) ^ (NotAtom(fi) ! (9j1; j2 2 i)( 1(fj1 ) = 2(fi) ^ 1(fj2 ) = 3(fi)))] ^ (8i 2 f (0))[i 2 f (0) ^ NotAtom( 1(fi)) ^ i 6= 0 !
CLCopy( 1(fi); 2(fi)) ^ CRCopy( 1(fi); 3(fi))] ^
(8i 2 domf )(f (0) i ! fi 2 f (0) ^ fi 6= 0) ^
Fun(b) ^ dom b = f (0) ^ (8i 2 f (0))(BoundList(bi; 1(fi))) ^
(8i; n; j 2 domf )[df = n+ ^ f (0) i ! 1(f (f (n)) = x ^ ];
where the formula will be de ned below. Clearly, NotAtom is easily de nable
starting from last and the Symbol predicates. This is the point in the formula in
which d is implicitly used in order to be able to express last as an (
The formula is the disjunction of the following four formulae: Axiom(fi). Clearly, to recognize axiom (A6), we have to use the bound variables list properly. This clearly does not raise the 0-complexity, as it is su cient to access the list that comes with just existential quanti ers.
Modus Ponens: (9j1; j2 2 i)(f (0) ^ f (0) j2 ^ Symbol)( 1(last( 1f (fj1 ))) ^
1(f (fi)) = 3(f (fj1 )) ^ 1(f (fj2 )) = 2(f (fj1 ))): Universal Generalization:
(9j1 2 i)[f (0) ^ 1(f (fj1 )) = 3(f (fi)) ^ Symbol8( 1(last( 1(f (fi)))]:
Rename Resolution:
(8k 2 dom 3(f (fpi )))(8t 2 ran 3(f (fpi )))(8j 2 f (0))
j = rfrom(lastf (fi)) ^ t = 3(f (fpi ))(k) ! ^ f (0) pi;
where rfrom extracts the variable that has to be renamed from a rename node
(depending on the encoding, with natural numbers it is (
Clearly the entire formula is (89)0.
Thus and also Proof0 are (89)0. Finally, we have the (89)0-speci cation: Proof(p; x) D!ef Quintuple(p) ^ Proof0 1(p); x; 2(p); 3(p); 4(p); 5(p) : 5
What follows presupposes that an essential preliminary step for an arithmetization of the syntax, namely a map ' 7! d'e sending every formula into a natural number whence one can retrieve a formula '0 such that '0 a` ', has been implemented (cf. [7]). Our next lemma will be useful in exploiting such a \Godel numbering".
representable in T 0 through the existential closure of a (89)0-formula 'ind(c; k).
d results from the formula with code c through substitution of the lowest-index variable by the code of a term t is strongly represented in T 0 by a 1-formula with a (89)0-matrix 'sub(c; t; d). More speci cally, we have that for each formula ' and term code t:
T 0 ` 8d( Subst(d'e; t; d) $ d = d8x(x = t ! ')e ):
In practice, we will write 'sub(c; t; d; w), where w is an n-tuple containing all the existentially quanti ed variables, to intend the same formula after dropping its external existential quanti ers.
T 0 ` $ 8c c = d e ! '(c) ; where d e is some code for the formula . that has the Proof. Let D(c; d; w) 'sub(c; c; d; w) and assume, without loss of generality, that w and d are not free in '. By the previous lemma, we have that for every formula , 8c c = d e ! 9d; wD(c; d; w) , and 8c c = d e ! 8d; w D(c; d; w) ! d = d8c(c = d e ! ')e . Putting = 8d; w(D(c; d; w) ! '(d)), we have: 8c c = d8d; w(D(c; d; w) ! '(d))e ! 8d; w D(c; d; w) ! d = d8c(c = d8d; w(D(c; d; w) ! '(d))e ! ')e . Let = 8c(c = d8d; w(D(c; d; w) ! '(d))e ! 8d; w(D(c; d; w) ! '(d))). Then: 8c8d8w c = d8d; w(D(c; d; w) ! '(d))e ^ D(c; d; w) ! d = d e : Since 8c c = d e ! 9d; wD(c; d; w) , we have 9d; w c = d8d; w(D(c; d; w) ! '(d))e ^ D(c; d; w) for any c such that c = d e. Thus, as c, d, w are not free in ', we have: 8c c = d8d; w(D(c; d; w) ! '(d))e ! 8d; w(D(c; d; w) ! '(d)) $ '(d e): In general, c = (k)C is a 1-formula with a (89)0-matrix, whilst can be seen as the universal closure of the formula obtained from ' by eliminating its unbounded quanti ers. In general, c = (k)C is a 1-formula with a (89)0-matrix, whilst can be seen as the universal closure of the formula obtained from ' by eliminating its unbounded quanti ers. When we take '(x) 8p(:Proof(p; x)), which is a 1-formula with a (98)0 matrix, then also is a 1-formula with (98)0-matrix. This fact can be exploited to apply a Godel incompleteness theoremlike argument.
(@ 2 L2) T ` 9x Cod(x) ^ ^ (8c 2 Cod) T ` : (c) ; then it is incomplete with respect to the class of 1-formulae with a (89)0-matrix. Proof. By applying the xpoint lemma on the formula '(x) = 8p(:Proof(p; x)), we obtain a formula such that:
T 0 ` $ 8p(:Proof(p; d e)): As T 0 is Cod -consistent, it neither proves nor disproves . Therefore, since : is a 1-formula with a (89)0-matrix, then T 0 is incomplete with respect to this class of formulae. tu The usual computability notions on functions over natural numbers can naturally be extended on codes thanks to the fact that their index can be computed. If we take a recursively axiomatizable theory on L2, the collection of the indices of its axioms is a recursive set. Therefore, as computable functions are strongly representable, also the collection of code indices C0 is faithfully representable in T 0, i.e., there is a formula 'C0 such that n 2 C0 , T 0 ` 'C0 (n). We saw that also the correspondence between codes and their indices is strongly representable through the formula 'ind. Thus, the collection C of codes of the axioms of the theory is faithfully representable through the following formula 'C (x) 9y('ind(x; y) ^ 'C0 (y)). Clearly, for every formula ' of L2, assuming Codconsistency, we have: T 0 ` ' , T 0 ` 9y Proof('; y); and, in particular, when we instantiate ' with 'C (c): T 0 ` 'C (c) , T 0 ` 9y Proof('C (c); y): Thence:
C(x) = 9z; u; y; w z = d'C e ^ 'sub(z; x; u; w) ^ Proof(u; y) is 1-formula with a (89)0-matrix that faithfully represents the collection of codes C.
From the previous discussion, we have the following result:
is faithfully representable through a 1-formula C with a (89)0-matrix. Hence, we can state our main result:
the theory T 0. Then with a (89)0-matrix.
be a recursively axiomatizable, Cod -consistent extension of is incomplete with respect to the collection of 1-formulae Proof. Let C be the r.e. collection of codes of the theorems in refer the xpoint lemma to '(c) :C(c). . It su ces to tu
To resume the discussion on decidability in the Introduction, we state:
ther Ts or Tf , the decision problem for the collection of (89)0-formulae is algorithmically unsolvable. 6
The claim just made is closely akin to a result in [1, Sec. 2], but the framework in which this paper has cast Corollary 2 is much broader. Instead of referring the undecidability of (89)0-formulae to a full- edged set theory, we have been working under very weak, explicit axiomatic assumptions; moreover, our limiting results contribute to a general investigation on essential (set-theoretic) undecidability.
We have striven, while revisiting the material of [10], to balance transparency of the encodings with complexity of the undecidable collection of formulae; and yet, we expect that further work along the lines of this paper|possibly calling into play also the milestone result [8]|can improve this tradeo .