The fragment of elementary plane Euclidean geometry based on perpendicularity alone with complexity PSPACE-complete

Ivanova, Tatyana; Tinchev, Tinko

doi:10.1090/tran/9302

The fragment of elementary plane Euclidean geometry based on perpendicularity alone with complexity PSPACE-complete
HTML articles powered by AMS MathViewer

by Tatyana Ivanova and Tinko Tinchev;

Trans. Amer. Math. Soc. 378 (2025), 1433-1447

DOI: https://doi.org/10.1090/tran/9302

Published electronically: November 19, 2024

HTML | PDF | Request permission

Abstract:

A. Tarski uses in his system for elementary Euclidean geometry only the primitive concept of point, and the two primitive relations betweenness and equidistance. Another approach is for the relations to be on lines instead of points. W. Schwabhäuser and L. Szczerba [Fund. Math. 82 (1974/75), pp. 347–355] showed that perpendicularity together with the ternary relation of co-punctuality are sufficient for dimension two, i.e. they may be used as a system of primitive relations for elementary plane Euclidean geometry. In this paper we give a complete axiomatization for the fragment of elementary plane Euclidean geometry based on perpendicularity alone. We show that this theory is not finitely axiomatizable, that it is decidable and that the complexity is PSPACE-complete. In contrast the complexity of elementary plane Euclidean geometry is exponential.

References

Philippe Balbiani and Tinko Tinchev, Line-based affine reasoning in Euclidean plane, J. Appl. Log. 5 (2007), no. 3, 421–434. MR 2328189, DOI 10.1016/j.jal.2006.03.003
Saugata Basu, New results on quantifier elimination over real closed fields and applications to constraint databases, J. ACM 46 (1999), no. 4, 537–555. MR 1812131, DOI 10.1145/320211.320240
Saugata Basu, Richard Pollack, and Marie-Françoise Roy, On the combinatorial and algebraic complexity of quantifier elimination, J. ACM 43 (1996), no. 6, 1002–1045. MR 1434910, DOI 10.1145/235809.235813
Evert W. Beth and Alfred Tarski, Equilaterality as the only primitive notion of Euclidean geometry, Indag. Math. 18 (1956), 462–467. Nederl. Akad. Wetensch. Proc. Ser. A 59. MR 80922, DOI 10.1016/S1385-7258(56)50062-5
G. E. Collins, Quantifier elimination by cylindrical algebraic decomposition—twenty years of progress, In Caviness, B. F. and Johnson, J. R., editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer-Verlag, New York, 1998, pp. 8–23.
H. N. Gupta, Contributions to the axiomatic foundations of geometry, Doctoral dissertation, University of California, Berkeley, 1965, p. 407.
Joos Heintz, Marie-Françoise Roy, and Pablo Solernó, Sur la complexité du principe de Tarski-Seidenberg, Bull. Soc. Math. France 118 (1990), no. 1, 101–126 (French, with English summary). MR 1077090, DOI 10.24033/bsmf.2138
D. Hilbert, Foundations of Geometry, La Salle, Illinois, 1950.
L. Monk, Elementary recursive decision procedures, Ph.D. thesis, University of California, Berkeley, 1974.
M. Pasch, Vorlesungen über neuere Geometrie, B.G.Teubner, Leipzig, 1882.
M. Pieri, La geometria elementare istituita sulle nozioni ’punto’ é ’sfera’, Memorie di Matematica e di Fisica della Società Italiana delle Scienze, 15 (1908), 345–450.
J. Renegar, On the computational complexity and geometry of the first-order theory of the reals, J. Symb. Comput. 13 (1992), no. 3, 255–352.
W. Schwabhäuser and L. W. Szczerba, Relations on lines as primitive notions for Euclidean geometry, Fund. Math. 82 (1974/75), 347–355. MR 360247, DOI 10.4064/fm-82-4-347-355
W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, Hochschultext, Springer-Verlag, Berlin, 1983, pp. viii+482.
D. Scott, Dimension in elementary Euclidean geometry, In Henkin et al., 1959, pp. 53–67.
L. W. Szczerba and A. Tarski, Metamathematical properties of some affine geometries, Logic, Methodology and Philos. Sci. (Proc. 1964 Internat. Congr.), North-Holland, Amsterdam, 1965, pp. 166–178. MR 209948
L. W. Szczerba and A. Tarski, Metamathematical discussion of some affine geometries, Fund. Math. 104 (1979), no. 3, 155–192. MR 559172, DOI 10.4064/fm-104-3-155-192
A. Tarski, A decision method for elementary algebra and geometry, prepared for publication by J.C.C. McKinsey, U.S. Air Force Project RAND, R-109, the RAND Corporation, Santa Monica, 1948, pp. iv+60; a second, revised edition was published by the University of California Press, Berkeley and Los Angeles, CA, 1951, pp. iii+63.
Alfred Tarski, A general theorem concerning primitive notions of Euclidean geometry, Indag. Math. 18 (1956), 468–474. Nederl. Akad. Wetensch. Proc. Ser. A 59. MR 80923, DOI 10.1016/S1385-7258(56)50063-7
Alfred Tarski, What is elementary geometry?, Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958, Stud. Logic Found. Math., North-Holland, Amsterdam, 1959, pp. 16–29. The axiomatic method; With special reference to geometry and Physics; Edited by L. Henkin, P. Suppes and A. Tarski. MR 106185
A. Tarski, The completeness of elementary algebra and geometry, Institut Blaise Pascal, Paris, 1967, pp. iv+50.
Alfred Tarski and Steven Givant, Tarski’s system of geometry, Bull. Symbolic Logic 5 (1999), no. 2, 175–214. MR 1791303, DOI 10.2307/421089
Oswald Veblen, A system of axioms for geometry, Trans. Amer. Math. Soc. 5 (1904), no. 3, 343–384. MR 1500678, DOI 10.1090/S0002-9947-1904-1500678-X
O. Veblen, The foundations of geometry, In Young, J., editor, Monographs on topics of modern mathematics, relevant to the elementary field, pp. 1–51. Longsman, Green, and Company, New York, (1914).

AMS Website Down

Transactions of the American Mathematical Society

The fragment of elementary plane Euclidean geometry based on perpendicularity alone with complexity PSPACE-complete
HTML articles powered by AMS MathViewer

Abstract: