From Hilbert's 10th Problem to slim, Undecidable Fragments of Set Theory?

Abstract

We revisit, deepen, and make more systematic, the study| undertaken ca. 1990|of reductions of Hilbert's tenth problem to fragments of set theory, whereby sublanguages of the Zermelo-Fraenkel axiomatic theory are shown to have an undecidable satis ability problem.

Keywords

• Hilbert's 10th problem
• Undecidability
• ZF set theory
• Satis ability problem
• Cartesian product
• (89)0 formulas
• Proof-checkers

-

Introduction We show that the satis ability problems for various fragments of ZF|the Zermelo-Fraenkel rst-order set theory with regularity axiom|are undecidable. To wit, if is among those sublanguages of ZF, no algorithm can establish whether or not any given formula in becomes true under suitable assignments of sets to its free variables.

For each taken into account, the undecidability result stems from a uniform

translation method which turns every instance D = 0 (with D 2 Z[x1; : : : ; xm]) of Hilbert's 10th problem into a formula of so that is satis able if and only if the polynomial equation D(x1; : : : ; xm) = 0 has natural solutions. Through this translation, the algorithmic unsolvability of Hilbert's 10th problem carries over to the satis ability problem for .

Some of the undecidable 's are slight extensions of a core language consisting of all conjunctions of literals of the forms x = y [ z, x = y z, x \ y = ?, and jxj = jyj, where x; y; z stand for variables, y z is a variant of Cartesian product consisting of singletons and unordered doubletons, and jxj = jyj designates equinumerosity between x and y. Additional conjuncts entering into play can be, e.g.: one literal of the form Finite(x), stating that x has nitely many elements, ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). We gratefully acknowledge partial support from project \STORAGE|Universita degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2", and from INdAM-GNCS 2019 and 2020 research funds. taken along with one literal of the form x 6= ?. Another option would be to extend the said syntactic core by allowing three negated equinumerosity literals of the form jxj 6= jyj to appear in the conjunction. Our interest in these, and similar, slim undecidable set-theoretic languages is increased by the fact that they lie extremely close to fragments of ZF which are either known [3, Sec.11.1], or conjectured [4, p. 239], to be decidable.

One can recast the undecidable fragments of ZF under study in a set-theoretic language entirely devoid of function symbols (such as [; , etc.), which only involves the relators 2 and =, propositional connectives, and also the constructs 8 x 2 y ' and 9 x 2 y ' involving bounded quanti ers, subject to a very restrained use. The fact that somewhat sophisticated notions like \being an ordinal", \being the rst limit ordinal !", \having a nite cardinality", \being a hereditarily nite set", can be speci ed inside this collection of formulas, dubbed (89)0 formulas, gives evidence of the high expressive power of bounded quanti cation in the context of ZF.

In a full- edged language for set theory, (89)0 speci cations are only seldom used in order to de ne mathematical notions. Hence, to support the correctness of the proposed (89)0-speci cations of !, equinumerosity, and nitude, we have proved that they are equivalent to more direct and practical characterizations of the same notions. As we document at the http://aetnanova.units. it/scenarios/SetTheoreticH10/, this formal accomplishment was carried out with the aid of a proof-checker embodying a computational version of ZF. 1

From Hilbert's 10th problem to unsolvable satis ability problems in set theory 1.1

How to

atten instances of Hilbert's 10th problem

Consider a polynomial Diophantine equation

D(x1; : : : ; xm) = 0 to be solved in N. By pulling out subterms of the polynomial D, we can atten this equation into a system (viz., a conjunction) of equations of the forms x = y + z ; x = y z ; x = 1 ; x = y ; where x; y; z stand for variables, to be regarded|the new ones as well as the original ones, x1; : : : ; xm|as unknowns in N (cf. [10,1]). We can then eliminate each equation of the form x = y by rewriting it as x = y + , where is forced to assume the value 0 (see equations ( 5 ) below).

The attening process can easily enforce that x; y; z are distinct variables when they appear together in the same equation x = y ? z (with ? 2 f`+'; ` 'g); moreover, we will keep a sole equation, o = 1, involving 1. The equi-solvability between the system so obtained and the original equation will be obvious.

= 1 + 2 ; o = 1 ; u1 = o + ; Px11 = x1 + ; Px12 = x2 + ; Px13 = x3 + ;

1 = 2 + ; u2 = u1 + o ; u3 = u2 + o ; Px21 = Px11 Px22 = Px12 Px23 = Px13 x1 ; x2 ; x3 ; M11 = u4 Px31 ; M1 = M11 x2 ; M21 = u2 Px21 ; M2 = M21 Px33 ; M31 = u3 Px22 ; M3 = M31 x1 ;

2 = + 1 ; u4 = u3 + o ; u5 = u4 + o ; Px31 = Px21 Px33 = Px23 x1 ; x3 ; M4 = u5 x3 ;

L = M1 + M4 ; L = M2 + M3 : By then replacing the equation o = 1 in 1 by the constraints o 6= o = o o0 ; o0 = o + ; ( 1 ) and ( 2 ) ( 3 ) ( 4 )

a ( 5 ) (which are equisatis able with o = o2 & o 6= ), we get a system which is equisolvable|in N|with the initial equation ( 1 ) and consists of: 28 equations in 29 unknowns, of the forms (where all compound terms y ? z involve distinct variables) and one inequality x = y + z ; x = y z ; o 6=

: Example 1. The equation (from [8, p. 4]) 4 x13 x2 2 x12 x33 3 x22 x1 + 5 x3 = 0 can be attened into the following system 1 consisting of 26 equations in 28 unknowns, 3 of which are x1; x2; x3, namely the original unknowns of ( 1 ): De nition 1. Systems that consist of at equations of the forms ( 3 ) conjoined with the equations = 1 + 2 ; 1 = 2 + ; 2 = + 1 and ( 2 ) and with the inequality ( 4 ), and inside which all terms of type y + z and y z involve distinct variables, are named canonical Diophantine systems. Remark 1. One can also express multiplication in terms of the squaring operation (see [6, p. 230]). Notice, in fact, that any equation of the form x = y z is equisolvable in N with the attened system of equations p = y + z ; x0 = x + ; q = p2 ; f = y2 ; g = z2 ; k = x + x0 ; h = f + g ; q = k + h ; as can be seen from the identity q k h (z y +}|z ){2 = zy z }+| y z{ + zy2 }+| z2{ : | {pz } |{xz} |{xz0} |{fz} |{gz} a

From a canonical Diophantine systems of set-theoretic constraints of the forms: , we will next get a conjunction b = = union (ternary relation) Cartesian product (ternary relation) disjointness (dyadic relation) equinumerosity (dyadic relation) finitude (property) singleton formation (dyadic relation) non-emptyness (property) non-equinumerosity (dyadic relation) Here, in light of the replaceability of multiplication by the squaring operation (as pointed out in Remark 1), we might only employ Cartesian square y y, without ever resorting to the product y z with y distinct from z. 1.2 Let

How to translate a canonical Diophantine system unquanti ed fragments of set theory into

be a Diophantine canonical system.

We translate each conjunct of according to the following rules: x = y + z x = y z o 6= uy;z = y [ z & where each uy;z and each wy;z is a new variable. By also adding, for each variable u in , the conjunct Finite(u) (meaning that j u j 2 N), we obtain the set-theoretic counterpart b of .

Next we prove that the canonical system is satis able in N if and only if its set-theoretic counterpart b is satis able in the universe of all sets. In view of the unsolvability of Hilbert's Tenth problem (see [8, Chapter 5]), we readily obtain the algorithmic unsolvability of the satis ability problem for set-theoretic conjunctions of positive literals of the forms plus a single inequality of the form x 6= ? .

To carry out the rst half of the proof, we observe that any set-assignment

v 7! M v over the variables of b that satis es b induces naturally the corresponding N-assignment

v 7! jM vj over the variables of , and it is a simple matter to check that ( 6 ) satis es For instance, if x = y + z is in , then the following conjuncts are in b ( 6 ) . uy;z = y [ z ;

We prove that the set-assignment M so de ned over the variables of b satis es all of the conjuncts of b .

{ Let x = y + z be in . By the de nition of M , we have

M uy;z = M y [ M z ; so that M satis es the conjunct uy;z = y [ z.

Let y and z be the variables vi and vj , respectively, where without loss of

generality we are assuming i < j. Also, let x be the variable vh. Preliminarily, we show that

M vi \ M vj = ; : ( 7 )

If ; 2 fM vi ; M vj g, then (7) plainly holds. Otherwise, recalling that

M vi := ki + [vi] and

M vj := kj + [vj ] ; we get max M vi = ki + vi = i 1 X vr + vi = r=1

i X vr 6 r=1 j 1 X vr < min M vj ; r=1 whence ( 7 ) follows in this case too.

From ( 7 ), it follows that j M uy;z j = j M y [ M z j = j M y j + j M z j = j M vi j + j M vj j = vi + vj = vh = j M vh j = j M x j ; proving that the set-assignment M satis es the conjunct j M uy;z j = j M x j. { It is even easier to prove that M satis es also the literals in b of the forms resulting from the translation of equations of the form x = y z, and the only literal of the form x 6= ? in b . { To end, for each variable u in , the assignment M also satis es Finite(u) .

We have thus obtained that the set-assignment M satis es the conjunction

b, and hence conclude that the translation 7! b is satis ability-preserving, namely: Theorem 1. A canonical Diophantine system is solvable in N if and only if the corresponding conjunction b is satis ed by some set-assignment.

Consequently, from the undecidability of Hilbert's tenth problem we get:

Lemma 1. The satis ability problem for set-theoretic conjunctions of any number of positive literals of the forms and of the form Finite(x), plus one negative literal of the form x 6= ? , is algorithmically unsolvable.

Since nitude is -hereditary, any conjunction Vi2I Finite(xi) of nitude constraints can be replaced, without a ecting satis ability, by the conjunction Finite(F ) & Vi2I F = F [ xi containing a single nitude constraint, where F is a newly introduced variable. The preceding undecidability result can hence be slightly strengthened into: Lemma 2. The satis ability problem for set-theoretic conjunctions of any number of positive literals of the forms (z), plus one positive nitude literal, Finite(x) , and one negative literal of the form x 6= ? is algorithmically unsolvable.

A fortiori, we also have the following negative result:

Lemma 3. The satis ability problem for set-theoretic conjunctions of any number of positive literals of the forms (z), plus one positive nitude literal, Finite(x) , and one negative literal of the form j x j 6= j y j is algorithmically unsolvable.

The following claim gives us a way of expressing the nitude of sets:

Proposition 1. A set with at least two members is nite if and only if it is the union of two sets whose cardinalities di er from its own cardinality. Proof. It su ces to note that, for an in nite set s and any decomposition s = s1[ s2, we have (independently of whether s1 \s2 = ? or not) j s j = max(j s1 j ; j s2 j).

Thus, without a ecting satis ability, any conjunction nitude literals can be replaced by the conjunction

Vi2I Finite(xi) of F = F1 [ F2 & j F1 j 6= j F j & j F2 j 6= j F j & ^ F = F [ xi i2I containing no nitude literal, where F; F1; F2 are newly introduced variables.

In view of the preceding remark, Lemma 3 can be restated as follows.

Lemma 4. The satis ability problem for set-theoretic conjunctions of any number of positive literals of the forms (z), plus at most three negative literals of the form j x j 6= j y j , is algorithmically unsolvable.

One can express nitude also in the following way:

Proposition 2. A nonempty set is nite if and only if, by removing a member from it, one obtains a set of di erent cardinality.

Therefore, we have:

Lemma 5. The satis ability problem for set-theoretic conjunctions of any number of positive literals of the forms (z), plus two positive literals of the form x = f y g , and one negative literal of the form j x j 6= j y j , is unsolvable.

Proof. In view of Lemma 2, it is enough to observe that:

{ a negative literal of the form x 6= ? can be expressed via a conjunction of the form y0 = f x0 g & x = x [ y0 where x0; y0 are brand new variables; { any conjunction Vi2I Finite(xi) of nitude literals can be expressed by means of the conjunction F = f f g & F = F [F & F = F nF &

F 6= j F j & ^ F = F [xi i2I containing no nitude literal, where F; F ; F are new variables; { a literal of the form x = y n z can be expressed by means of the conjunction y = x [ x0 & x \ x0 = ? & x \ z = ? & x0 \ y = ? : 1.3

Undecidability results regarding unordered Cartesian product

Much the same reductions can be carried out when the operation de ned by

s t :=

fu; vg : u 2 s; v 2 t : (for sets s; t whatsoever) supersedes the standard Cartesian product operator .

In order that Lemmas 1, 2, 3, 4, and 5 retain their validity with this unordered product operator in place of , it su ces that the above-proposed translation rule for arithmetical constraints of the form x = y z gets retouched as follows: x = y z

z & y \ z = ? & j wy;z j = j x j : 2

Undecidability of a restrained collection of bounded-quanti er formulas in set theory So far we have been designating various set-theoretic operations (e.g., dyadic union, Cartesian product, cardinality) and properties and relations ( nitude, disjointness, etc.) by means of ad hoc signs ( [ , , Finite( ), \ = ? , etc.) which, if adopted beforehand as primitives in the language supporting set theory, would make the undecidable fragments reviewed in Sec. 1 devoid of quanti ers.

Most often, set theories get formalized in a rst-order language devoid of

constants and function symbols, whose only relators are 2 and =. How complex then becomes the syntactic structure of the formulas lying in the undecidable fragments? As we will see next, a very modest usage of quanti cation is needed to state them: only bounded quanti ers, and just one quanti er alternation are needed, with (bounded) universal quanti ers in leading position. 2.1

The syntax of (89)0 formulas

Consider the rst-order language L2 endowed with:

{ an in nite supply 0; 1; 2; : : : of set variables; { dyadic relators 2; = designating membership and equality; { the familiar propositional connectives : (monadic) and & ; _ ; !; $ (dyadic); { associated with each set variable i , the familiar quanti ers 8 i and 9 i.

We enhance the usual syntax of formulas with two handy shortening devices: De nition 2. Universal and existential bounded quantifiers are introduced as follows:

(8 x 2 y)' $Def (8 x)(x 2 y ! ') ; (9 x 2 y)' $Def (9 x)(x 2 y & ') :

De nition 3. We dub (89)0-formula any conjunction

of the form where, for each j, the formula 'j is devoid of quanti ers and either pj > 0, qj > 0 or pj = qj = 0 holds. De nition 4. We dub (89)0 specification of an m-place relationship R over sets a (89)0 formula with free variables a1; : : : ; am; x1; : : : ; x (where > 0) such that, under the axioms of set theory (see below), one can prove: R(a1; : : : ; am) $ (9 x1 ; : : : ; x ) :

E.g., the right-hand sides of

a = b n c $ (8t 2 a)(t 2 b & t 2= c) & (8t 2 b)(t 2 c _ t 2 a) ;

Sngl(a) $ (9 x) x 2 a & (8y 2 a)(y = x) are (89)0 speci cations of the 3-place relationship a = b n c and, respectively, of the property \being a singleton set".

In the ongoing, our set-theoretic framework will be the theory ZF, axiom of

regularity included. First, in order to design a (89)0 speci cation of the property \being a nite set" (see Sec. 2.4), we will extend temporarily the signature of L2 with a constant ! which is meant to designate the rst limit ordinal; then we will gure out a (89)0 speci cation of the property \being the rst limit ordinal" (see Sec. 2.5), thus ending in an impeccable (89)0 speci cation of nitude. Along the way, we will also specify the important equinumerosity predicate, which relates two sets when they have the same cardinality (see Sec. 2.4). (89)0 speci cations referring to disjointness, unionset, and weak Cartesian product x \ y = ? $ (8 v 2 x) v 2= y ; x [y $ (8 x0 2 x)(9 y0 2 y) x0 2 y0 ;

v $ (8p 2 f )(8w 2 p)(w 2 v) ; [f Mapw(f ) $ (8p 2 f )(8x1; x2; x3 2 p) x1 = x2 _ x2 = x3 _ x3 = x1 ; f x y $ Mapw(f ) (8p 2 f )(9x0 2 x)(9y0 2 y) x0 2 p & y0 2 p ) (8p 2 f )(8w 2 p) w 2 x _ w 2 y ) : & &

The explanation of the last of these is straightforward; here it is:

No member of f has more than two members:

where (8p 2 f ) jpj 6 2 ; jpj 6 2 $ (8x1; x2; x3 2 p) x1 = x2 _ x2 = x3 _ x3 = x1 : Each member of f has the form fx0; y0g with x0 2 x and y0 2 y: (8p 2 f )(9x0 2 x)(9y0 2 y) x0 2 p & y0 2 p ) : No member of a member of f lies outside x [ y: [f x [ y : 2.4 (89)0 speci cations of equinumerosity, squaring, and nitude 1-1w(x; f; y) $ x \ y = ? & f x y & x [f & y [f & (8p ; q 2 f )(8v 2 p) v 2 q ! p = q : Meaning: 1-1w(x; f; y) can only hold if x and y are disjoint sets, in which case f models a one-to-one mapping between x and y by means of unordered pairs, in the sense that: f consists of doubletons proper; each doubleton in f pairs up a member of x with one of y; f pairs up exactly one member of y with each member of x; f pairs up exactly one member of x with each member of y.

Stating that sets x; y are of the same cardinality amounts to the statement that there is a set y0 such that y0 can be put in one-to-one correspondence with x, y0 can be put in one-to-one correspondence with y, y0 and x are disjoint, and y0 and y are disjoint.

Summing up, we have:

jxj = jyj $ (9 y0 ; g ; h ) 1-1w(x; g; y0) & 1-1w(y; h; y0) : Clue: One way of concretizing y0, here, is by putting y0 = y fy [ xg.

Likewise, stating that the cardinalities jxj ; jyj are such that jxj = jyj2 amounts to the statement that there are sets y0; x0 such that y0 can be put in one-to-one correspondence with y, x0 = y y0 and x0 can be put in one-to-one correspondence with x, x0 and x are disjoint, and y0 and y are disjoint. Summing up, we have: jxj = jyj2 $ (9 x0 ; y0 ; g ; h ) Mapw(x0) Clue: The equality x0 = y y0 follows from the conjunction of Mapw(x0) with the last two conditions, thanks to the disjointness constraint y0 \y = ? hidden inside 1-1w(y0; h; y). A convenient way to instantiate y0 is, again, to put y0 = y fy [xg.

A nite set is one that can be put in one-to-one correspondence with a cardinal preceding (i.e., belonging to) the rst in nite ordinal, ! :

Finite(x) $ (9 o) o 2 ! & jxj = joj :

More explicitly:

Finite(x) $ (9 o ; x0 ; g ; h) o 2 ! & 1-1w(x0; g; x) & 1-1w(x0; h; o) : (89)0 speci cation of ordinals and of the rst limit ordinal A set t is said to be transitive if t P(t); equivalently, if [ t t . After John von Neumann and Raphael M. Robinson, ordinal numbers are those transitive sets within which any two di erent elements can be compared by membership: Ord(o) $ (8y 2 o)(8y0 2 y) y0 2 o &

(8o1 2 o)(8o2 2 o)(o1 = o2 _ o1 2 o2 _ o2 2 o1)

Those ordinal numbers o such that o 6= ; and o = [o are called limit ordinals.

Plainly, the property \being a limit ordinal" is (89)0-speci able.

To characterize uniquely the rst limit ordinal, !, among all sets, it will

su ce to conjoin together the following conditions, where Z; a, and s are meant to represent, respectively: ! itself, an element of !, and the successor function (modeled as a set of doubletons, each one implicitly ordered by membership): Z is a non-null ordinal:

No member of s has more than two members:

a 2 Z & Ord(Z)

Mapw(s) Each member of s is a doubleton fx; yg with x 2 y 2 Z: (8p 2 s)(9x; y 2 p) x 2 y & y 2 Z ( 8 ) ( 9 ) The domain of s includes Z: (8p; q 2 s)(8x; y 2 p)(8y0 2 q) (x 2 y & x 2 y0 & x 2 q) ! p = q (11) (12) (13) The multi-image of s includes Z n f;g:

(8x 2 Z)(9p 2 s)(9y 2 p) x 2 p & x 2 y (8y 2 Z)(8e 2 y)(9p 2 s)(9x 2 p) y 2 p & x 2 y

Thus, one can prove (in ZF with regularity):

(8Z) Z = ! $ (9a)(9s) ( 8 ) & & (13)

Concluding remarks and open problems We have revisited, deepened, and made more systematic, the study undertaken long ago with [2] (see also [3, pp. 161{165]).

Can we do more along the directions envisioned in the following excerpt from a historical paper?

[ ]the translation of a theorem of the appropriate form in some part of mathematics shows that the corresponding Diophantine equation has no solution. Hence whatever methods went into proving the theorem can in fact be used to show that a particular Diophantine equation has no solution. It is possible that the same methods can be used to show that a class of equations including perhaps an equation of interest in itself are unsolvable. Such an example providing a new tool for solving Diophantine equations would be a considerable breakthrough. In any case, any mathematical method that has been used to prove a theorem of the appropriate form has in fact been used to show that a particular Diophantine equation has no solution. Thus all mathematical methods can be tools in the theory of Diophantine equations and perhaps we should consciously attempt to exploit them. " [5, pp. 338{339]

The quest is open. . . It may be rewarding to:

{ translate back into number theory decidability results regarding fragments of set theory; { mimic the proofs of the theorems, dubbed DPR and DPRM in [7], concerning the exponential Diophantine representability and the polynomial Diophantine representability of any r.e. set, directly inside set theory (possibly making some technical aspects of those proofs more transparent).

Open problems

Let BSTC (Boolean Set Theory with Cardinality comparison and the unordered Cartesian product) be the collection of conjunctions of any number of positive literals of the forms

x = y [ z ; x = y z ; x \ y = ? ; j x j = j y j :

In sight of the still in progress decidability result for MLS (multilevel syllogistic with the unordered Cartesian product), concerning a positive solution to the satis ability problem for conjunctions of literals of the forms x = y [ z ; x = y z ; x \ y = ? ; x 2 y ; to precisely locate the boundary between decidability and undecidability, one should attempt to nd the decidability status of the satis ability problem for the following collections of equalities: { BSTC -conjunctions plus one negative literal of the form x 6= ? , { BSTC -conjunctions plus two literals of any of the following forms: j x j 6= j y j and x = f y g :

Acknowledgements

We are grateful to Martin Davis for his encouragement. We thank the anonymous referees for their careful comments.

References

1. J.L. Britton . Integer solutions of systems of quadratic equations . Mathematical Proceedings of the Cambridge Philosophical Society , 86 ( 3 ): 385 { 389 , 1979 .

2. D. Cantone , Vincenzo Cutello, and Alberto Policriti . Set-theoretic reductions of Hilbert's tenth problem . In Egon Borger, Hans Kleine Buning, and Michael M. Richter, editors, CSL '89 , 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2- 6 , 1989 , Proceedings, volume 440 of Lecture Notes in Computer Science, pages 65 { 75 . Springer, 1990 .

3. D. Cantone , E. G. Omodeo , and A. Policriti . Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets . Monographs in Computer Science . Springer, 2001 .

4. Domenico Cantone and Pietro Ursino . Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, niteness predicate . Information and Computation , 237 : 215 { 242 , 2014 .

5. Martin Davis , Yuri Matijasevic, and Julia Robinson . Hilbert's tenth problem. Diophantine equations: positive aspects of a negative solution . In Mathematical Developments Arising From Hilbert Problems , volume 28 of Proceedings of Symposia in Pure Mathematics , pages 323 { 378 , Providence, RI, 1976 . American Mathematical Society. Reprinted in [9 , p. 269 .].

6. Yu . Matiyasevich. Existential arithmetization of Diophantine equations . Annals of Pure and Applied Logic , 253 ( 2-3 ): 225 { 233 , 2009 .

7. Yu . V. Matiyasevich . Martin Davis and Hilbert's tenth problem . In Eugenio G. Omodeo and Alberto Policriti, editors, Martin Davis on Computability, Computational Logic, and Mathematical Foundations , volume 10 of Outstanding Contributions to Logic, pages 35 { 54 . Springer, 2016 .

8. Yuri Vladimirovich Matiyasevich. Hilbert's tenth problem . The MIT Press, Cambridge (MA) and London, 1993 .

9. Julia Robinson . The collected works of Julia Robinson , volume 6 of Collected Works. American Mathematical Society , Providence, RI, 1996 . ISBN 0-8218- 0575-4. With an introduction by Constance Reid. Edited and with a foreword by Solomon Feferman . xliv+338 pp.

10. Thoralf Skolem . Uber die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzahlbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen . Fundamenta Mathematicae , 23 : 150 { 161 , 1934 .