Simplifying the axiomatization for ordered affine geometry via a theorem prover

Jan von Plato proposed in 1998 an intuitionist axiomatization of ordered affine geometry consisting of 22 axioms. It is shown that axiom I.7, which is equivalent to a conjunction of four statements, two of which are redundant, can be replaced with a simpler axiom, which is von Plato’s Theorem 3.10....

Full description

Saved in:
Bibliographic Details
Published in:Journal of geometry 2023-08, Vol.114 (2), Article 9
Main Author: Li, Dafa
Format: Article
Language:English
Subjects:
Axioms
Geometry
Mathematics
Mathematics and Statistics
Theorem proving
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Jan von Plato proposed in 1998 an intuitionist axiomatization of ordered affine geometry consisting of 22 axioms. It is shown that axiom I.7, which is equivalent to a conjunction of four statements, two of which are redundant, can be replaced with a simpler axiom, which is von Plato’s Theorem 3.10.
ISSN:0047-2468
1420-8997
DOI:10.1007/s00022-023-00671-9