Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-25T02:08:12.676Z Has data issue: false hasContentIssue false
  • English
  • Français

Provability with Finitely Many Variables

Published online by Cambridge University Press:  15 January 2014

Robin Hirsch ,
Ian Hodkinson  and
Roger D. Maddux
Robin Hirsch
Affiliation:
Department of Computer Science, University College, Gower Street, London WC1E 6BT, UK, E-mail: [email protected]
Ian Hodkinson
Affiliation:
Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK, E-mail: [email protected]
Roger D. Maddux
Affiliation:
Department of Mathematics, 400 Carver Hall, Iowa State University, Ames, Iowa 50011-2066, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

For every finite n ≥ 4 there is a logically valid sentence φn with the following properties: φn contains only 3 variables (each of which occurs many times); φn contains exactly one nonlogical binary relation symbol (no function symbols, no constants, and no equality symbol); φn has a proof in first-order logic with equality that contains exactly n variables, but no proof containing only n − 1 variables. This result was first proved using the machinery of algebraic logic developed in several research monographs and papers. Here we replicate the result and its proof entirely within the realm of (elementary) first-order binary predicate logic with equality. We need the usual syntax, axioms, and rules of inference to show that φn has a proof with only n variables. To show that φn has no proof with only n − 1 variables we use alternative semantics in place of the usual, standard, set-theoretical semantics of first-order logic.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 8 , Issue 3 , September 2002 , pp. 348 - 379
Copyright
Copyright © Association for Symbolic Logic 2002

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] Andréka, H., Maddux, R. D., and Németi, I., Splitting in relation algebras, Proceedings of the American Mathematical Society, vol. 111 (1991), no. 4, pp. 1085–1093.Google Scholar
[2] Berge, C., Graphs and hypergraphs, North-Holland Publishing Co., Amsterdam, 1973, Translated from the French by Edward Minieka, North-Holland Mathematical Library, vol. 6.Google Scholar
[3] Comer, S. D., Color schemes forbidding monochrome triangles, Proceedings of the Fourteenth Southeastern conference on combinatorics, graph theory and computing (Boca Raton, Fla., 1983), vol. 39, 1983, pp. 231–236.Google Scholar
[4] Givant, S., Tarski's development of logic and mathematics based on the calculus of relations, Algebraic Logic (Budapest, 1988) (Andréka, H., Monk, J., and Németi, I., editors), Colloquia Mathematica Societatis Janos Bolyai, vol. 54, North-Holland, Amsterdam, 1991, pp. 189–215.Google Scholar
[5] Gordeev, L., Combinatorial principles relevant to finite variable logic, RelMiCS 2000 (Desharnais, J., editor), Département d'Informatique, Université Laval, 2000, pp. 95–111.Google Scholar
[6] Graham, R. L., Rudiments of Ramsey theory, CBMS, American Mathematical Society, Providence, RI, 1981.CrossRefGoogle Scholar
[7] Graham, R. L., Rothschild, B. L., and Spencer, J. H., Ramsey theory, Wiley, New York, 1980.Google Scholar
[8] Greenwood, R. E. and Gleason, A. M., Combinatorial relations and chromatic graphs, Canadian Journal of Mathematics, vol. 7 (1955), pp. 1–7.CrossRefGoogle Scholar
[9] Henkin, L., Internal semantics and algebraic logic, Truth, syntax and modality (Proc. Conf. Alternative Semantics, Temple Univ., Philadelphia, Pa., 1970), Studies in Logic and the Foundations of Mathematics, vol. 68, North-Holland, Amsterdam, 1973, pp. 111–127.Google Scholar
[10] Hirsch, R., Hodkinson, I., and Maddux, R. D., Relation algebra reducts of cylindric algebras and an application to proof theory, The Journal of Symbolic Logic, vol. 67 (2002), no. 1, pp. 197–213.CrossRefGoogle Scholar
[11] Johnson, J., Nonfinitizability of classes of representable polyadic algebras, The Journal of Symbolic Logic, vol. 34 (1969), pp. 344–352.Google Scholar
[12] Löwenheim, L., Über Möglichkeiten im Relativkalkul, Mathematische Annalen, vol. 76 (1915), pp. 447–470.CrossRefGoogle Scholar
[13] Lyndon, R. C., Relation algebras and projective geometries, The Michigan Mathematical Journal, vol. 8 (1961), pp. 21–28.Google Scholar
[14] Maddux, R. D., Topics in relation algebras, Ph.D. thesis , University of California, Berkeley, 1978, pp. iii + 241.Google Scholar
[15] Maddux, R. D., Some varieties containing relation algebras, Transactions of the American Mathematical Society, vol. 272 (1982), no. 2, pp. 501–526.CrossRefGoogle Scholar
[16] Maddux, R. D., A sequent calculus for relation algebras, Annals of Pure and Applied Logic, vol. 25 (1983), no. 1, pp. 73–101.Google Scholar
[17] Maddux, R. D., Nonfinite axiomatizability results for cylindric and relation algebras, The Journal of Symbolic Logic, vol. 54 (1989), no. 3, pp. 951–974.CrossRefGoogle Scholar
[18] McKenzie, R. N., Representations of integral relation algebras, The Michigan Mathematical Journal, vol. 17 (1970), pp. 279–287.CrossRefGoogle Scholar
[19] Monk, J. D., On representable relation algebras, The Michigan Mathematical Journal, vol. 11 (1964), pp. 207–210.Google Scholar
[20] Maddux, R. D., Model-theoretic methods and results in the theory of cylindric algebras, The Theory of Models (Proc. 1963 Internat. Sympos. Berkeley) (Addison, J., Henkin, L., and Tarski, A., editors), North-Holland, Amsterdam, 1965, pp. 238–250.Google Scholar
[21] Maddux, R. D., Nonfinitizability of classes of representable cylindric algebras, The Journal of Symbolic Logic, vol. 34 (1969), pp. 331–343.Google Scholar
[22] Maddux, R. D., Provability with finitely many variables, Proceedings of the American Mathematical Society, vol. 27 (1971), pp. 353–358.Google Scholar
[23] Participants, Open problems, Algebraic Logic (Budapest, 1988) (Andréka, H., Monk, J., and Németi, I., editors), Colloquia Mathematica Societatis János Bolyai, vol. 54, North-Holland, Amsterdam, 1991, pp. 727–746.Google Scholar
[24] Peirce, C. S., Note B: the logic of relatives, Studies in Logic by Members of the Johns Hopkins University (Peirce, C. S., editor), Little, Brown, and Co., Boston, 1883, pp. 187–203.Google Scholar
[25] Schröder, F. W. K. E., Vorlesungen über die Algebra der Logik (exacte Logik), Volume 3, “Algebra und Logik der Relative” Part I, second ed., Chelsea, Bronx, New York, 1966, first published in Leipzig, 1895.Google Scholar
[26] Tarski, A., On the calculus of relations, The Journal of Symbolic Logic, vol. 6 (1941), pp. 73–89.Google Scholar
[27] Tarski, A., A simplified formalization of predicate logic with identity, Arch. Math. Logik Grundlag., vol. 7 (1965), pp. 61–79.Google Scholar
[28] Tarski, A. and Givant, S., A formalization of set theory without variables, American Mathematical Society, Providence, RI, 1987.Google Scholar