Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-25T10:16:53.113Z Has data issue: false hasContentIssue false
  • English
  • Français

Some theorems on definability and decidability

Published online by Cambridge University Press:  12 March 2014

Alonzo Church  and
W. V. Quine
Alonzo Church
Affiliation:
Princeton University
W. V. Quine
Affiliation:
Harvard University
Get access Rights & Permissions [Opens in a new window]

Extract

In this paper a theorem about numerical relations will be established and shown to have certain consequences concerning decidability in quantification theory, as well as concerning the foundation of number theory. The theorem is that relations of natural numbers are reducible in elementary fashion to symmetric ones; i.e.:

Theorem I. For every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that R is definable in terms of H plus just truth-functions and quantification over natural numbers.

To state the matter more fully, there is a (well-formed) formula ϕ of pure quantification theory, or first-order functional calculus, which meets these conditions:

(a) ϕ has ‘x’ and ‘y’ as sole free individual variables;

(b) ϕ contains just one predicate letter, and it is dyadic;

(c) for every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that, when the predicate letter in ϕ is interpreted as expressing H, ϕ comes to agree in truth-value with ‘x bears R to y’ for all values of ‘x’ and ‘y’.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 17 , Issue 3 , September 1952 , pp. 179 - 187
Copyright
Copyright © Association for Symbolic Logic 1952

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 Kalmár, László, Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären, Funktionsvariablen, Compositio mathemalica, vol. 4 (1936), pp. 137–144Google Scholar. As actually stated by him, Kalmár's method accomplishes the reduction oi a formula ψ of quantification theory to a formula ψ′ of quantification theory meeting the conditions that ψ′ contains just one predicate letter, that that letter is dyadic, and that ψ is satisfiable if and only if ψ′ is satisfiable; however, as is well known, this is easily modified to yield the reduction method described in the text by making use of the equivalence between validity of a formula and unsatisfiability of its negation. Moreover, Kalmár's procedure begins with a preliminary reduction of the given formula to a formula in prenex normal form with a prefix of specified form, and in the further reduction to a formula having a single binary predicate letter in the matrix the same form of prefix is preserved. Thus Kalmár's result is stronger than our present purpose requires. A proof of the (weaker) result stated in the text, by a reduction method which is independent of reduction of the prefix to a special form, will also appear in the forthcoming revised and enlarged edition of Church, Introduction to mathematical logic I, §47.

2 See Hilbert and Ackermann, Grundzüge der theoretischen Logik, Chapter 3, §10, or Church, op. cit., revised edition, **450.

3 Church, Alonzo, A note on the Entscheidungsproblem, this Journal, vol. 1 (1936), pp. 40–41, 101–102Google Scholar.

4 Löwenheim, Leopold, Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol. 76 (1915), pp. 447–470CrossRefGoogle Scholar. Other decision procedures for monadic quantification theory have been presented by Skolem, Thoralf, Untersuchungen über die Axiome des Klassenkalkuls, Skrifter utgit av Videnskapsselskapet i Kristiania, I. Mat.-naturvid. Klasse 1919, no. 3Google Scholar; Behmann, Heinrich, Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem, Mathematische Annalen, vol. 86 (1922), pp. 163–229CrossRefGoogle Scholar; Bernays, Paul and Schönfinkel, Moses, Zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol. 99 (1928), pp. 342–372CrossRefGoogle Scholar; Herbrand, Jacques, Recherches sur la théorie de la démonstration (Warsaw, 1930), Chapter 2, §9.2Google Scholar. For convenient expositions of these procedures and further variants, see also Hilbert and Ackermann, op. cit., Chapter 3, §12; Hilbert, and Bernays, , Grundlagen der Mathematik, vol. I, pp. 193–195Google Scholar; von Wright, G. H., Form and content in logic (Cambridge, England, 1949, 35 pp.)Google Scholar; Quine, , O sentido da nova logica (São Paulo, 1944), pp. 126–129Google Scholar; On the logic of quantification, this Journal, vol. 10 (1945), pp. 1–12Google Scholar; Methods of logic, pp. 101–117, 192–194; Church, Introduction to mathematical logic I, revised edition, §46.

5 In the opinion of one of the authors, it is only the inclusion of predicate letters within quantifiers which makes it preferable to view such letters as class variables. See Quine, Methods of Logic, §38.

6 See Löwenheim, op. cit.; or, for better accounts, Skolem, op. cit., and Behmann, op. cit.

7 Introduction to mathematical logic I, edition of 1944, and forthcoming revised edition.

8 Robinson, Julia, Definability and decision problems in arithmetic, this Journal, vol. 14 (1949), pp. 98–114Google Scholar. Her construction is geared to just the positive integers, but is easily adjusted to include 0.

9 A reduction of elementary number theory to a single non-symmetric dyadic predicate was given by Myhill, John R., A reduction in the number of primitive ideas of arithmetic, this Journal, vol. 15 (1950), p. 130Google Scholar.

10 See Goodman, Nelson, The logical simplicity of predicates, this Journal, vol. 14 (1949), pp. 32–41Google Scholar.

11 Gödel, Kurt, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, Monatshefte für Mathematik und Physik, vol. 38 (1931), pp. 173–198CrossRefGoogle Scholar.

12 Gödel, Kurt, Die Vollständigkeit der Axiome des logischen Funktionenkalküls, Monatshefte für Mathematik und Physik, vol. 37 (1930), pp. 349–360CrossRefGoogle Scholar.