Nuprl Lemma : Beeson's Constructive Tarski Geometry

Tarski and his students (Szemeilew, Gupta) gave a
first order axiomatic theory for Euclidean plane geometry
that had only Points as elements and two relations.
a ternary "betweeness" relation and a quaternary "congruence" relation
(which defines a binary "same length" relation on segments).

They made the system minimal, so that the axioms were all independent
and none of them could be derived from the others (using classical logic).

Beeson has given a constructive, intuitionistic logic, version of Tarski's
system -- which we formalize here in Nuprl. We use constructive
logic and do not assume that equality of Points is decidable.
Therefore, a theorem stating that for
all points A and B satisfying some constraints P(A,B)
there exists a point C satisfying constraints Q(A,B,C)
may not be proved by cases where if A=B then C is constructed one way
and if not(A=B) then C is constructed another way.

Because of this, Beeson must add a few axioms that
were derivable (using classical logic) in Tarski's system.
Also, to make all of the constructions continuous functions of their input
points, two of the axioms (the "extend" axiom and the "inner Pasch" axiom)
that construct new points are restricted to non-degenerate cases
(only segments with distinct endpoints can be extended, and
the "inner Pasch" requires a non-colinear triangle and strict betweenness).

Finally, Beeson's axioms assume that the betweenness relation and the congruence
relation are "stable" propositions about points (a proposition P is stable
if (¬¬P) ⇒ P ).

The formal definition of a EuclideanPlane has the form
{e:EuclideanStructure| euclidean-axioms(e)} -- follow those links (right click) for
further documentation. ⋅

Latex:
Tarski and his students (Szemeilew, Gupta) gave a first order axiomatic theory for Euclidean plane geometry that had only Points as elements and two relations. a ternary "betweeness" relation and a quaternary "congruence" relation (which defines a binary "same length" relation on segments). They made the system minimal, so that the axioms were all independent and none of them could be derived from the others (using classical logic). Beeson has given a constructive, intuitionistic logic, version of Tarski's system -- which we formalize here in Nuprl. We use constructive logic and do not assume that equality of Points is decidable. Therefore, a theorem stating that for all points A and B satisfying some constraints P(A,B) there exists a point C satisfying constraints Q(A,B,C) may not be proved by cases where if A=B then C is constructed one way and if not(A=B) then C is constructed another way. Because of this, Beeson must add a few axioms that were derivable (using classical logic) in Tarski's system. Also, to make all of the constructions continuous functions of their input points, two of the axioms (the "extend" axiom and the "inner Pasch" axiom) that construct new points are restricted to non-degenerate cases (only segments with distinct endpoints can be extended, and the "inner Pasch" requires a non-colinear triangle and strict betweenness). Finally, Beeson's axioms assume that the betweenness relation and the congruence relation are "stable" propositions about points (a proposition P is stable if (\mneg{}\mneg{}P) {}\mRightarrow{} P ). The formal definition of a EuclideanPlane has the form \{e:EuclideanStructure| euclidean-axioms(e)\} -- follow those links (right click) for further documentation. \mcdot{} Date html generated: 2015_07_17-PM-06_21_37 Last ObjectModification: 2015_07_16-PM-11_47_36 Home Index