Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-28T16:19:25.320Z Has data issue: false hasContentIssue false

Relation algebra reducts of cylindric algebras and an application to proof theory

Published online by Cambridge University Press:  12 March 2014

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]

Abstract

We confirm a conjecture, about neat embeddings of cylindric algebras, made in 1969 by J. D. Monk, and a later conjecture by Maddux about relation algebras obtained from cylindric algebras. These results in algebraic logic have the following consequence for predicate logic: for every finite cardinal α ≥ 3 there is a logically valid sentence X, in a first-order language with equality and exactly one nonlogical binary relation symbol E, such that X contains only 3 variables (each of which may occur arbitrarily many times), X has a proof containing exactly α + 1 variables, but X has no proof containing only α variables. This solves a problem posed by Tarski and Givant in 1987.

Type
Research Article
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., Finite axiomatizability of SNrnCAn+1 and non-finite axiomatizability of SNrnCAn+2, Lecture notes for a series of lectures given at Algebraic Logic Meeting, Oakland, CA, 1990.Google Scholar
[2]Andréka, H., Complexity of equations valid in algebras of relations, Part I: Strong non-finitizability, Annals of Pure and Applied Logic, vol. 89 (1997), pp. 149209.CrossRefGoogle Scholar
[3]Andréka, H., Monk, J. D., and Németi, I., Algebraic logic, Colloq. Math. Soc. J. Bolyai, North-Holland, Amsterdam, 1991.Google Scholar
[4]Andréka, H., Németi, I., and Sain, I., Algebraic logic. Handbook of philosophical logic (Gabbay, D. M. and Guenthner, F., editors), Kluwer, second ed., In preparation. Draft available at http://www.math-inst.hu/pub/algebraic-logic/handbook.html.Google Scholar
[5]Chin, L. and Tarski, A., Distributive and modular laws in the arithmetic of relation algebras, University of California Publications in Mathematics, New Series, vol. 1 (1951), pp. 341384.Google Scholar
[6]Givant, S., Tarski's development of logic and mathematics based on the calculus of relations, In [3], pp. 189215.Google Scholar
[7]Greenwood, R. E. and Gleason, A. M., Combinatorial relations and chromatic graphs, Canadian Journal of Mathematics, vol. 7 (1955), pp. 17.CrossRefGoogle Scholar
[8]Henkin, L., Logic systems containing only a finite number of symbols, Séminaire de mathématiques supérieures, vol. 21, Les Press de l'Université de Montrêal, Montréal, 1967.Google Scholar
[9]Henkin, L., Relativization with respect to formulas and its use in proofs of independence, Compositio Mathematica, vol. 20 (1968), pp. 86106.Google Scholar
[10]Henkin, L., Internal semantics and algebraic logic, Truth, syntax, and modality (Leblanc, H., editor), Studies in Logic, vol. 68, North-Holland, Amsterdam, 1973, pp. 111127.CrossRefGoogle Scholar
[11]Henkin, L., Monk, J. D, and Tarski, A., Cylindric algebras, Part I, North-Holland, 1971.Google Scholar
[12]Henkin, L., Monk, J. D, and Tarski, A., Cylindric algebras, Part II, North-Holland, 1985.Google Scholar
[13]Henkin, L. and Tarski, A., Cylindric algebras, Lattice theory, proceedings of symposia in pure mathematics (Dilworth, R. R, editor), vol. 2, American Mathematical Society, Providence, 1961, pp. 83113.Google Scholar
[14]Hirsch, R. and Hodkinson, I., Relation algebras from cylindric algebras, II, Annals of Pure and Applied Logic, to appear.Google Scholar
[15]Johnson, J., Nonfinitizability of classes of representable polyadic algebras, this Journal, vol. 34 (1969), pp. 344352.Google Scholar
[16]Johnson, J., Axiom systems for logic with finitely many variables, this Journal, vol. 38 (1973), pp. 576578.Google Scholar
[17]Lyndon, R. C., The representation of relational algebras, Annals of Mathematics (series 2), vol. 51 (1950), pp. 707729.CrossRefGoogle Scholar
[18]Lyndon, R. C., Relation algebras and projective geometries, Michigan Mathematics Journal, vol. 8 (1961), pp. 2128.CrossRefGoogle Scholar
[19]Maddux, R. D., Topics in relation algebra, Ph.D. thesis, University of California, Berkeley, 1978.Google Scholar
[20]Maddux, R. D., Finite integral relation algebras, Universal algebra and lattice theory, Lecture Notes in Mathematics, vol. 1149, Springer-Verlag, 1985, pp. 175197.CrossRefGoogle Scholar
[21]Maddux, R. D., Non-finite axiomatizability results for cylindric and relation algebras, this Journal, vol. 54 (1989), pp. 951974.Google Scholar
[22]Maddux, R. D., Introductory course on relation algebras, finite-dimensional cylindric algebras, and their interconnections, In [3], pp. 361392.Google Scholar
[23]Maddux, R. D., The neat embedding problem and the number of variables required in proofs. Proceedings of the American Mathematical Society, vol. 112 (1991), pp. 195202.CrossRefGoogle Scholar
[24]McKenzie, R. N. W, The representation of integral relation algebras, Michigan Mathematical Journal, vol. 17 (1970), pp. 279287.CrossRefGoogle Scholar
[25]Monk, J. D., Studies in cylindric algebra, Ph.D. thesis, University of California, Berkeley, 1961.Google Scholar
[26]Monk, J. D., Nonfinitizability of classes of representable cylindric algebras, this Journal, vol. 34 (1969), pp. 331343.Google Scholar
[27]Monk, J. D., Provability with finitely many variables. Proceedings of the American Mathematical Society, vol. 27 (1971), pp. 353358.CrossRefGoogle Scholar
[28]Németi, I. and Simon, A., Relation algebras from cylindric and polyadic algebras, Logic Journal of IGPL, vol. 5 (1997), pp. 575588.CrossRefGoogle Scholar
[29]Simon, A., Nonrepresentable algebras of relations, Ph.D. thesis, Math. Inst. Hungar. Acad. Sci., Budapest, 1997, http:/www.renyi.hu/pub/algebraic-logic/simthes.html.Google Scholar
[30]Tarski, A., A simplified formalization of predicate logic with identity, Archive fiir Mathematische Logik und Grundlagenforschung, vol. 7 (1965), pp. 6179.CrossRefGoogle Scholar
[31]Tarski, A. and Givant, S. R, A formalization of set theory without variables, Colloquium Publications in Mathematics, vol. 41, American Mathematical Society, Providence, 1987.Google Scholar
[32]Thompson, R., Complete description of substitutions in cylindric algebras and other algebraic logics. Algebraic methods in logic and in computer science (Rauszer, C., editor), vol. 28, Banach Center publications, 1993, pp. 327342.Google Scholar