A Finite, Feasible, Quantifier-free Foundation for Constructive Geometry

TL;DR

This paper develops a quantifier-free, feasible axiomatic foundation for constructive geometry, enabling geometric reasoning with basic human faculties and avoiding non-feasible constructions, while capturing Euclidean and non-planar results.

Contribution

It introduces the first all-quantifier-free, feasible axiomatic system for constructive geometry, extending previous work and avoiding non-feasible assumptions like Euclid's Fifth Postulate.

Findings

Axioms are all quantifier-free and feasible

System captures Euclidean and non-planar geometry results

Avoids non-feasible constructions like Euclid's Fifth Postulate

Abstract

In this paper we will develop an axiomatic foundation for the geometric study of straight edge, protractor, and compass constructions, which while being related to previous foundations, will be the first to have all axioms written and all proofs conducted in quantifier-free first order logic. All constructions within the system will be justified to be feasible by basic human faculties. No statement in the system will refer to infinitely many objects and one can posit an interpretation of the system which is in accordance to our free, creative process of geometric constructions. We are also able to capture analogous results to Euclid's work on non-planar geometry in Book XI of The Elements. This paper primarily builds on Suppes' paper Quantifier-Free Axioms for Constructive Affine Plane Geometry and draws from Beeson's article A Constructive Version of Tarski's Geometry. By further developing Suppes' work on parallel line segments, we are able to develop analogs to most theorems about parallel lines without assuming an equivalent to Euclid's Fifth Postulate which we deem as introducing non-feasible constructions. In A Constructive Version of Tarski's Geometry, Beeson defines the characteristics such a geometric foundation should have to called constructive. This work satisfies these characteristics. Additionally this work would be considered constructive as Suppes defined it.