Tarski’s “weak-continuity” elementary geometry (TWCEG) is a first-order finite axiomatization of Euclidean geometry. TWCEG is consistent and incomplete. Its universal sentences are decidable. There is no known proof of the consistency or independence of TWCEG that uses a finite-domain model. Here I show that if we replace the “segment construction” axiom of TWCEG with a slightly weaker axiom, we obtain an elementary Euclidean geometry (which I call “CCWCEG”) that is first-order, finitely axiomatized, incomplete, consistent, and independent. The proofs of the consistency and independence of CCWCEG require only finite-domain models. I further show that the universal sentences of CCWCEG are decidable.
The manuscript has two high-level parts – a ~15 pp. body, which can be read standalone, and ~150 pp. of technical appendices, which contain the detailed proof of the independence of CCWCEG.