Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-26T15:25:29.837Z Has data issue: false hasContentIssue false
  • English
  • Français

On the reduction of the decision problem. First paper. Ackermann prefix, a single binary predicate

Published online by Cambridge University Press:  12 March 2014

László Kalmár
László Kalmár*
Affiliation:
The Bolyai Institute, University Of Szeged
Get access Rights & Permissions [Opens in a new window]

Extract

1. Although the decision problem of the first order predicate calculus has been proved by Church to be unsolvable by any (general) recursive process, perhaps it is not superfluous to investigate the possible reductions of the general problem to simple special cases of it. Indeed, the situation after Church's discovery seems to be analogous to that in algebra after the Ruffini-Abel theorem; and investigations on the reduction of the decision problem might prepare the way for a theory in logic, analogous to that of Galois.

It has been proved by Ackermann that any first order formula is equivalent to another having a prefix of the form

(1) (Ex1)(x2)(Ex3)(x4)…(xm).

On the other hand, I have proved that any first order formula is equivalent to some first order formula containing a single, binary, predicate variable. In the present paper, I shall show that both results can be combined; more explicitly, I shall prove the

Theorem. To any given first order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.

2. Of course, this theorem cannot be proved by a mere application of the Ackermann reduction method and mine, one after the other. Indeed, Ackermann's method requires the introduction of three auxiliary predicate variables, two of them being ternary variables; on the other hand, my reduction process leads to a more complicated prefix, viz.,

(2) (Ex1)…(Exm)(xm+1)(xm+2)(Exm+3)(Exm+4).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 4 , Issue 1 , March 1939 , pp. 1 - 9
Copyright
Copyright © Association for Symbolic Logic 1939

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

1 See, for instance, Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. 1 (Berlin 1924), pp. 129–131Google Scholar. We eball adopt bere tbe point of view called “set-theoretic” in that book, pp. 125-128. Also, we ehall use the notations of that book.

2 Church, Alonzo, A note on the Entseheidungsproblem, The journal of symbolic logic, vol. 1 (1936), pp. 40–41CrossRefGoogle Scholar; Correction, ibid., pp. 101-102. See also Church, Alonzo, An unsolvable problem of elementary number theory, American journal of mathematics, vol. 58 (1936), pp. 345–363CrossRefGoogle Scholar, and Turing, A. M., On computable numbers, with an application to the Entseheidungsproblem, Proceedings of the London Mathematical Society, ser. 2, vol. 42 (1937), pp. 230–265CrossRefGoogle Scholar.

3 See Church, Alonzo, An unsolvable problem etc. (loc. cit.), pp. 350–351Google Scholar; Kleene, S. C., General recursive functions of natural numbers, Mathematische Annalen, vol. 112 (1936), pp. 727–742CrossRefGoogle Scholar. The notion of “general recursiveness” introduced in these papers (due to Herbrand and Gödel) is probably equivalent to that of “effectiveness.” To prove the equivalence of the two notions, an exact definition of the latter is evidently needed. Alternative forms of such definitions together with equivalence proofs have been given by Church (An unsolvable problem etc., loc. cit., pp. 356–358) and by Turing (loc. cit.); see also Kleene, S. C., λ-definability and recursiveness, Duke mathematical journal, vol. 2 (1936), pp. 340–353CrossRefGoogle Scholar. On the other hand, each exact definition of “effectiveness” gives rise to the doubt that it may involve restriction and to the hope that the decision problem can yet be solved by an effective process in the unrestricted sense; see Pepis, Józef, Untersuchungen über das Entseheidungsproblem der mathematischen Logik, Fundamenta mathematicae, vol. 30 (1938), pp. 257–348CrossRefGoogle Scholar, especially pp. 257–258. As a matter of fact, neither an instance nor a possible form of a process ever has been given which could be accepted as effective but was not (or could not, after the cited paradigms, be readily proved to be) general recursive.

4 Ackermann, Wilhelm, Beiträge sum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol. 112 (1936), pp. 419–432CrossRefGoogle Scholar.

5 Two first order formulas are called equivalent, if either both can be satisfied or neither. A statement expressing that any first order formula is equivalent to another of a special kind is always meant in the constructive sense, viz., that to any given first order formula we can effectively find an equivalent one of the kind in question.

6 Kalmár, László, Zum Entseheidungsproblem der mathematischen Logik, Verhandlungen des internationalen Mathematiker-Kongresses Zürich 1932, vol. 2, pp. 337–338Google Scholar; Zurilck-führung des Entsekeidungsproblem auf den Fall von Formeln mit einer einzigen, bindren, Funktionsvariablen, Compositio mathematica, vol. 4 (1936), pp. 137–144Google Scholar.

7 One of the ternary auxiliary predicate variables can be eaaily replaced by a binary one (see footnote 8 of my paper Zurückführung etc., loc. cit., p. 138). By an improvement of the Ackermann method, Pepis (loc. cit.) has proved that any first order formula is equivalent to another with a prefix of the form (1) which contains only one unary and three binary predicate variables.

8 Pepis has proved (loc. cit.) that one can reach m=3. Of course, the theorem of the present paper implies more, viz., that one can secure m=1.

9 Skolem, Th., Über einige Grundlagenfragen der Mathematik, Skrifter utgitt av det Nortke Videnskaps-Akademi i Oslo, mat.-naturv. klasse, 1929, no. 4, pp. 1–49Google Scholar, especially §4.

10 For similar reasons, Pepis (loc. cit.) uses the function 2i−1,(2j+1). It does not matter that the equations (3) do not form a “primitive” recursion. w(i, j) can be defined explicitly by

w(i,j) = i + (i+j−2)(i+j−1)/2,

but we shall make no use of this equation.

11 In my paper Zurückfükrung etc. (loc. cit.), I represented the elements x of I by the corresponding “diagonal” pairs (x, x); but this device can be avoided by using the set J − I+I 2+{Φ1,…,Φ1}.

12 See Kalmár, László, Ein Beitrag zum Entseheidungsproblem, Acta scientiarum mathematicarum, vol. 5 (1932), pp. 222–236Google Scholar and Über einen Löwenheimschen Satz, ibid., vol. 7 (1935), pp. 112–121, especially footnote 5, p. 113.

13 If m <l, we insert (Ey m+1) … (Eyι) between (Exm) and (xm+1) with variables y m+1, …, yι not occurring in A. By using the result of my paper Zurückfükrung etc. (loc. cit.), we could suppose l=1; but this would not essentially simplify the subsequent reasoning.

14 Compare Skolem, loc. cit., and Ackermann, loc. cit., especially pp. 421–422.

15 For simplicity, we omit “(mod 3)” after congruences.

16 To spare brackets, we agree that a disjunction sign separates more strongly than a conjunction sign, i.e., we do not put conjunctions in brackets when they are members of a disjunction.

17 For simplicity, we omit the conjunction sign.

18 The sign Π stands for conjunction.

19 We observe that 1 enters in (5)–(9) not only explicitly but also through the abbreviations Γ and Ω.

20 See Hilbert-Bernays, loc. cit., especially p. 141.

21 We introduced (4) only to be able to carry out these simplifications by means of the rules of the propositional calculus only. By means of the rules of tbe predicate calculus, we can infer (4) from (5) and (6).