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

TL;DR

The paper defines a complete axiomatization of elementary plane Euclidean geometry based solely on the perpendicularity relation $O$, showing the resulting theory $SAPP$ is decidable and $PSPACE$-complete, and not finitely axiomatizable. It proves completeness by embedding models into a countable rational-line framework and analyzes several definability relations, including that $P$ and $C$ are definable from $O$ and $=$ while certain ternary predicates like $\rho$ are not. It also establishes model-theoretic properties: $SAPP$ is $ω$-categorical but not categorical in any uncountable cardinal, and it is not finitely axiomatizable. These results position the perpendicularity-based fragment as a robust, decidable foundation for plane geometry with precise complexity and categoricity characteristics.

Abstract

A. Tarski uses in his system for the elementary geometry only the primitive concept of point, and the two primitive relations betweenness and equidistance. Another approach is the relations to be on lines instead of points. W. Schwabhäuser and L. Szczerba 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, it is decidable and the complexity is PSPACE-complete. In contrast the complexity of elementary plane Euclidean geometry is exponential.

Theorems & Definitions (26)

• Remark 2.1
• Remark 2.2
• Remark 2.3
• Remark 2.4
• Remark 2.5
• Proposition 2.6
• Definition 2.7
• Proposition 2.8
• Proposition 2.9
• Corollary 2.10