Simplifying the axiomatization for the ordered affine geometry via a theorem prover

TL;DR

This paper simplifies the axiomatization of ordered affine geometry by replacing a complex, redundant axiom with a more intuitive one, using a theorem prover to ensure equivalence.

Contribution

It identifies redundancy in a key axiom and introduces a simpler, equivalent axiom for ordered affine geometry through automated theorem proving.

Findings

Redundancy found in the original axiom I.7.

A new, simpler axiom is proposed and verified as equivalent.

Enhanced understanding of the axiomatization process.

Abstract

Based on an ordering with directed lines and using constructions instead of existential axioms, von Plato proposed a constructive axiomatization of the ordered affine geometry. There are 22 axioms for the ordered affine geometry, of which the axiom I.7 is about the convergence of three lines (ignoring their directions). In this paper, we indicate that the axiom I.7 includes much redundancy, and demonstrate that the complicated axiom I.7 can be replaced equivalently with a simpler and more intuitive new axiom via a theorem prover.