A Finite-Domain-Based Automated Proof of the Consistency of a “Segment-Construction” Variant of Tarski’s Elementary Geometry
摘要
Tarski’s “weak-continuity” elementary geometry (TWCEG) is a consistent, first-order, finite axiomatization of Euclidean geometry. All proofs of the consistency of TWCEG require infinite-domain-size models. Experimentation reveals that the “segment-construction” axiom (“A4”) of TWCEG can be considered at least part of a cause of our inability to prove the consistency of TWCEG using finite-domain-size models. Here I show that if we replace A4 with an axiom that does nothing but remove a null case of A4, we obtain an elementary Euclidean geometry whose consistency can be shown using a finite-domain model. The resulting theory, which I call “substantive-segment-constructive weak continuity elementary geometry” (SSCWCEG), has the same consequences as TWCEG except for the null case of A4. The proof described here appears to be the first fully automated, finite-domain-based proof of the consistency of SSCWCEG.