Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-24T22:34:14.480Z Has data issue: false hasContentIssue false
  • English
  • Français

The unsolvability of the Gödel class with identity

Published online by Cambridge University Press:  12 March 2014

Warren D. Goldfarb
Warren D. Goldfarb*
Affiliation:
Harvard University Cambridge, Massachusetts 02138
Get access Rights & Permissions [Opens in a new window]

Extract

The Gödel class with identity (GCI) is the class of closed, prenex quantificational formulas whose prefixes have the form ∀∀∃ … ∃ and whose matrices contain arbitrary predicate letters and the identity sign “ = ”, but do not contain function signs or individual constants. The ∀∀∃ … ∃ class without identity was shown solvable over fifty years ago ([4], [12], [17]); slightly later, that class was shown to possess the stronger property of finite controllability ([5], [18]). (A class of formulas is solvable iff it is decidable for satisfiability; it is finitely controllable iff every satisfiable formula in it has a finite model.) At the end of [5], Gödel claims that the finite controllability of the GCI can be shown “by the same method” as he employed to show this for the class without identity. This claim has been questioned for nearly twenty years; in §1 below we give a brief history of investigations into it. The major result of this paper shows Gödel to have been mistaken: the GCI is unsolvable. §2 contains the basic construction, which yields a satisfiable formula in the GCI that lacks finite models. This formula may easily be exploited to encode undecidable problems into the GCI.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 49 , Issue 4 , December 1984 , pp. 1237 - 1252
Copyright
Copyright © Association for Symbolic Logic 1984

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

REFERENCES

[1]Ackermann, W., Solvable cases of the decision problem, North-Holland, Amsterdam, 1954.Google Scholar
[2]Denton, J., Applications of the Herbrand theorem, Ph.D. thesis, Harvard University, Cambridge, Massachusetts, 1963.Google Scholar
[3]Dreben, B. and Goldfarb, W., The decision problem, Addison-Wesley, Reading, Massachusetts, 1979.Google Scholar
[4]Gödel, K., Ein Spezialfall des Entscheidungsproblems der theoretischen Logik, Ergebnisse eines Mathematischen Kolloquiums, vol. 2 (1932), pp. 27–28.Google Scholar
[5]Gödel, K., Zum Entscheidungsproblem des logischen Funktionenkalkiils, Monatshefte für Mathtmatik und Physik, vol. 40 (1933), pp. 433–443.CrossRefGoogle Scholar
[6]Goldfarb, W., On the Gödel class with identity, this Journal, vol. 46 (1981), pp. 354–364.Google Scholar
[7]Goldfarb, W., Gurevich, Y. and Shelah, S., A decidable subclass of the minimal Gödel class with identity, this Journal, vol. 49 (1984), pp. 1253–1261.Google Scholar
[8]Gurevich, Y., On the effective recognizing of satisfiability of predicate formulas, Algebra i Lofika, vol. 5 (1966), no. 2, pp. 25–55. (Russian)Google Scholar
[9]Gurevich, Y., The decision problem for standard classes, this Journal, vol. 41 (1976), pp. 460–464.Google Scholar
[10]Kahr, A., Improved reductions of the Entscheidungsproblem to subclasses of AEA formulas, Proceedings of a Symposium on the Mathematical Theory of Automata, Brooklyn Polytechnic Institute, Brooklyn, New York, 1962, pp. 57–70.Google Scholar
[11]Kahr, A., Moore, E. and Wang, H., Entscheidungsproblem reduced to the ∀∃∀ case, Proceedings of the National Academy of Sciences of the United States of America, vol. 48 (1962), pp. 364–377.Google Scholar
[12]Kalmar, L., Über die Erfüllbarkeit derjenigen Zählausdrücke, welche in der Normalform zwei benachbarte Allzeichen enthalten, Mathematische Annalen, vol. 108 (1933), pp. 466–484.CrossRefGoogle Scholar
[13]Kalmár, L. and Surányi, J., On the reduction of the decision problem, second paper, this Journal, vol. 12 (1947), pp. 65–73.Google Scholar
[14]Kalmár, L. and Surányi, J., On the reduction of the decision problem, third paper, this Journal, vol. 15 (1950), pp. 161–173.Google Scholar
[15]Kostyrko, V., The reduction class ∀∃n∀, Algebra i Logika, vol. 3 (1964), no. 516 pp. 45–65. (Russian)Google Scholar
[16]Ramsey, F., On a problem of formal logic, Proceedings of the London Mathematical Society, ser. 2, vol. 30 (1930), pp. 264–286.CrossRefGoogle Scholar
[17]Schütte, K., Untersuchungen zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol. 109 (1934), pp. 572–603.CrossRefGoogle Scholar
[18]Schütte, K., Über die Erfüllbarkeit einer Klasse von logischen Formeln, Mathematische Annalen, vol. 110 (1934), pp. 161–194.CrossRefGoogle Scholar
[19]Surányi, J., Contributions to the reduction theory of the decision problem, second paper, Acta Mathematica Academiae Scientiarum Hungaricae, vol. 1 (1950), pp. 261–270.CrossRefGoogle Scholar
[20]Surányi, J., Reduktionstheorie des Entscheidungsproblems im Prädikatenkalkül der ersten Stufe, Verlag der Ungarischen Akademie der Wissenschaften, Budapest, 1959.Google Scholar
[21]Trakhtenbrot, B., On recursive separability, Doklady Akademii Nauk SSSR, vol. 88 (1953), pp. 953–955. (Russian)Google Scholar
[22]Wang, H., Dominoes and the AEA case of the decision problem, Proceedings of a Symposium on the Mathematical Theory of Automata, Brooklyn Polytechnic Institute, Brooklyn, New York, 1962, pp. 23–55.Google Scholar