:: Tarski Geometry Axioms
:: by William Richter , Adam Grabowski and Jesse Alama
::
:: Received June 16, 2014
:: Copyright (c) 2014-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GTARSKI1, RELAT_1, XBOOLE_0, INCSP_1, SUBSET_1, ZFMISC_1,
STRUCT_0, METRIC_1, FUNCT_1, NUMBERS, RELAT_2, CARD_1, ARYTM_3, XREAL_0,
COMPLEX1, ARYTM_1, XXREAL_0, XXREAL_1, ROUGHS_4;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, NUMBERS, XXREAL_0, XXREAL_1,
XXREAL_2, XCMPLX_0, XREAL_0, COMPLEX1, SUBSET_1, DOMAIN_1, RELAT_1,
RELSET_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0, METRIC_1, ORDINAL1,
FUNCT_4, ARYTM_2, ARYTM_0;
constructors RELSET_1, DOMAIN_1, ZFMISC_1, STRUCT_0, NUMBERS, XREAL_0,
FUNCT_1, FUNCT_2, METRIC_1, XXREAL_0, XCMPLX_0, SUBSET_1, BINOP_1,
SQUARE_1, COMPLEX1, XXREAL_1, XXREAL_2, FUNCT_4, ARYTM_1, ARYTM_0;
registrations XBOOLE_0, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, METRIC_1,
RELAT_1, FUNCT_1, BINOP_1, XXREAL_1, XXREAL_2, ARYTM_2, ORDINAL1,
STRUCT_0, ZFMISC_1;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
begin :: Tarski Axioms
:: Here are readable Mizar proofs of some axiomatic geometry theorems due
:: to the great Polish mathematician Alfred Tarski (born Teitelbaum), and
:: we hope to continue this work. The first author ported the code to
:: HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/), which can be
:: found in any recent subversion of HOL Light as
:: hol_light/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
:: This is largely a Mizar port of Julien Narboux's Coq pseudo-code
:: http://dpt-info.u-strasbg.fr/~narboux/tarski.html. We partially
:: prove the theorem of the 1983 book Metamathematische Methoden in
:: der Geometrie by Schwabh\"auser, Szmielew, and Tarski, that Tarski's
:: (extremely weak!) plane geometry axioms imply Hilbert's axioms. We
:: get about as far as Narboux, with Gupta's amazing proof which
:: implies Hilbert's axiom I1 that two points determine a line.
:: Tarski's axioms are easy to find, but the first Tarski proofs we
:: ever learned were on wikiproofs's port of Narboux's results
:: http://www.wikiproofs.de/w/index.php?title=Interface:Tarski%27s_geometry_axioms
:: Our Mizar proofs are much more readable than either Narboux's Coq
:: pseudo-code or wikiproof's JHilbert code.
:: Our Mizar coding was heavily influenced by Wojciech A. Trybulec's
:: incsp_1.miz in the MML library on axioms of incidence geometry.
:: S will be a Tarski plane, a set of points which is a model of the
:: first 7 of Tarski's Geometry axioms A1--A7. There are two binary
:: relations (predicates) defined on S, between and ≡, for
:: betweenness of points and equidistance of segments.
:: We carry the axioms A1--A7 around as part of the statements of the
:: theorems. To avoid this minor clutter one has to define a Mizar type of
:: planes satisfying axioms A1--A7, as Trybulec does with by
:: `mode IncSpace is IncSpace-like IncStruct;'
:: In Mizar it isn't possible to define such a type (or model) without
:: proving that some model exists. Trybulec's existence proofs runs
:: over 450 lines. So we define a predicate `S Tarski-model' which
:: means that the plane S satisfies the axioms A1--A7, and then prove
:: trivial theorems A1--A7 which say that if S Tarski-model, then S
:: satisfies an axiom A1--A7. The extra clutter involving the
:: predicate Tarski-model, and the label TarskiModel which stands for
:: the statement `S Tarski-model' could be avoided by loading all our
:: results into one gigantic theorem. Our approach seems preferable.
:: Our axioms have descriptive names, largely the names Narboux used,
:: CongruenceSymmetry (A1), CongruenceEquivalenceRelation (A2),
:: CongruenceIdentity (A3), SegmentConstruction (A4), SAS (A5),
:: BetweennessIdentity (A6), and Pasch (A7).
:: Our theorems are EquivReflexive, EquivSymmetric, EquivTransitive,
:: Baaa, Bqaa, C1 (for Hilbert's axiom C1), Bsymmetry, Baaq,
:: BEquality, B124and234then123, BTransitivity, BTransitivityOrdered,
:: B124and234Ordered, B124and234Ordered, SegmentAddition,
:: CongruenceDoubleSymmetry, C1prime, SegmentSubtraction,
:: EasyAngleTransport, B123and134Ordered, BextendToLine, GuptaEasy,
:: Inner5Segments, RhombusDiagBisect, FlatNormal,
:: EqDist2PointsBetween, EqDist2PointsInnerBetween, Gupta, I1part1,
:: I1part2, LineEqRefl, LineEqA1, LineEqSymmetric, LineEqTrans,
:: onlineEq, I1part2Reverse, and I1.
definition
struct (1-sorted) TarskiPlane (# carrier -> set,
Betweenness -> Relation of [:the carrier, the carrier:], the carrier,
Equidistance -> Relation of
[:the carrier, the carrier:], [:the carrier, the carrier:] #);
end;
definition
let S be TarskiPlane;
mode POINT of S is Element of S;
end;
definition
let S be TarskiPlane;
let a, b, c be POINT of S;
pred between a,b,c means
:: GTARSKI1:def 1
[[a,b],c] in the Betweenness of S;
end;
definition
let S be TarskiPlane;
let a, b, c, d be POINT of S;
pred a,b equiv c,d means
:: GTARSKI1:def 2
[[a,b],[c,d]] in the Equidistance of S;
end;
:: Two triangles are congruent if they satisfy the SSS criterion
definition
let S be TarskiPlane;
let a, b, c, x, y, z be POINT of S;
pred a,b,c cong x,y,z means
:: GTARSKI1:def 3 ::: :Def4:
a,b equiv x,y & a,c equiv x,z & b,c equiv y,z;
end;
definition
let S be TarskiPlane;
let a, b, c, d be POINT of S;
pred a,b,c,d are_ordered means
:: GTARSKI1:def 4 ::: :Def5:
between a,b,c & between a,b,d & between a,c,d & between b,c,d;
end;
definition let S be TarskiPlane;
attr S is satisfying_CongruenceSymmetry means
:: GTARSKI1:def 5 ::: :Axiom1:
for a, b being POINT of S holds a,b equiv b,a;
attr S is satisfying_CongruenceEquivalenceRelation means
:: GTARSKI1:def 6 ::: :Axiom2:
for a, b, p, q, r, s being POINT of S holds
a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s;
attr S is satisfying_CongruenceIdentity means
:: GTARSKI1:def 7 ::: :Axiom3:
for a, b, c being POINT of S holds
a,b equiv c,c implies a = b;
attr S is satisfying_SegmentConstruction means
:: GTARSKI1:def 8 ::: :Axiom4:
for a, q, b, c being POINT of S holds
ex x being POINT of S st between q,a,x & a,x equiv b,c;
attr S is satisfying_SAS means
:: GTARSKI1:def 9 ::: :Axiom5:
for a, b, c, x, a1, b1, c1, x1 being POINT of S holds
a <> b & a,b,c cong a1,b1,c1 &
between a,b,x & between a1,b1,x1 & b,x equiv b1,x1
implies c,x equiv c1,x1;
attr S is satisfying_BetweennessIdentity means
:: GTARSKI1:def 10 ::: :Axiom6:
for a, b being POINT of S holds between a,b,a implies a = b;
attr S is satisfying_Pasch means
:: GTARSKI1:def 11 ::: :Axiom7:
for a, b, p, q, z being POINT of S holds
between a,p,z & between b,q,z implies
ex x being POINT of S st between p,x,b & between q,x,a;
end;
definition
let S be TarskiPlane;
attr S is satisfying_Tarski-model means
:: GTARSKI1:def 12 ::: :TarskiAxioms:
S is satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch;
end;
begin :: Existence Proofs for Tarski Plane
definition
struct (MetrStruct,TarskiPlane) MetrTarskiStr
(# carrier -> set,
distance -> Function of [:the carrier,the carrier:], REAL,
Betweenness -> Relation of [:the carrier, the carrier:], the carrier,
Equidistance -> Relation of
[:the carrier, the carrier:], [:the carrier, the carrier:]
#);
end;
definition let M be MetrStruct;
mode TarskiExtension of M -> MetrTarskiStr means
:: GTARSKI1:def 13
the MetrStruct of it = the MetrStruct of M;
end;
registration let M be non empty MetrStruct;
cluster -> non empty for TarskiExtension of M;
end;
registration let M be non empty Reflexive MetrStruct;
cluster -> Reflexive for TarskiExtension of M;
end;
registration let M be non empty discerning MetrStruct;
cluster -> discerning for TarskiExtension of M;
end;
registration let M be non empty symmetric MetrStruct;
cluster -> symmetric for TarskiExtension of M;
end;
registration let M be non empty triangle MetrStruct;
cluster -> triangle for TarskiExtension of M;
end;
definition ::: is_between taken from METRIC_1
let S be MetrStruct, p,q,r be Element of S;
pred q is_Between p,r means
:: GTARSKI1:def 14
dist(p,r) = dist(p,q) + dist(q,r);
end;
definition let M be MetrTarskiStr;
attr M is naturally_generated means
:: GTARSKI1:def 15
(for a, b, c being POINT of M holds
between a,b,c iff b is_Between a,c) &
(for a, b, c, d being POINT of M holds
a,b equiv c,d iff dist (a,b) = dist (c,d));
end;
theorem :: GTARSKI1:1
for M, N being MetrStruct,
x, y being Element of M,
a, b being Element of N st
the MetrStruct of M = the MetrStruct of N & x = a & y = b holds
dist (x,y) = dist (a,b);
registration let N be non empty MetrStruct;
cluster naturally_generated for TarskiExtension of N;
end;
registration
cluster trivial non empty for MetrSpace;
end;
definition
func TrivialTarskiSpace -> MetrTarskiStr equals
:: GTARSKI1:def 16
the naturally_generated TarskiExtension of
the trivial non empty MetrSpace;
end;
registration
cluster TrivialTarskiSpace -> trivial non empty;
end;
theorem :: GTARSKI1:2
for M being trivial non empty MetrSpace,
a, b, c being Element of M holds
a is_Between b,c;
registration
cluster TrivialTarskiSpace -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch;
end;
registration
cluster TrivialTarskiSpace -> satisfying_Tarski-model;
end;
registration
cluster satisfying_Tarski-model non empty for TarskiPlane;
end;
registration
cluster satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch -> satisfying_Tarski-model for TarskiPlane;
cluster satisfying_Tarski-model -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch for TarskiPlane;
end;
begin :: Proving Properties
reserve S for satisfying_Tarski-model TarskiPlane;
reserve a, b, c, d, e, f, o, p, q, r, s,
v, w, u, x, y, z, a9, b9, c9, d9, x9, y9, z for POINT of S;
theorem :: GTARSKI1:3
a,b equiv b,a;
theorem :: GTARSKI1:4
a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s;
theorem :: GTARSKI1:5
a,b equiv c,c implies a = b;
theorem :: GTARSKI1:6
ex x st between q,a,x & a,x equiv b,c;
theorem :: GTARSKI1:7
a <> b & a,b,c cong a9,b9,c9 &
between a,b,x & between a9,b9,x9 & b,x equiv b9,x9
implies c,x equiv c9,x9;
theorem :: GTARSKI1:8
between a,b,a implies a = b;
theorem :: GTARSKI1:9
between a,p,z & between b,q,z implies
ex x st between p,x,b & between q,x,a;
:: Now we can prove results referring to the axioms as A1--A7.
theorem :: GTARSKI1:10
a,b equiv a,b;
theorem :: GTARSKI1:11
a,b equiv c,d implies c,d equiv a,b;
theorem :: GTARSKI1:12
a,b equiv p,q & p,q equiv r,s implies a,b equiv r,s;
theorem :: GTARSKI1:13
between a,a,a & a,a equiv b,b;
theorem :: GTARSKI1:14
between q,a,a;
theorem :: GTARSKI1:15
a <> b & between a,b,x & between a,b,y & b,x equiv b,y
implies x = y;
theorem :: GTARSKI1:16
between a,p,z implies between z,p,a;
theorem :: GTARSKI1:17
between a,a,q;
theorem :: GTARSKI1:18
between a,b,c & between b,a,c implies a = b;
theorem :: GTARSKI1:19
between a,b,d & between b,c,d implies between a,b,c;
theorem :: GTARSKI1:20
b <> c & between a,b,c & between b,c,d implies between a,c,d;
theorem :: GTARSKI1:21
b <> c & between a,b,c & between b,c,d implies a,b,c,d are_ordered;
theorem :: GTARSKI1:22 ::: B124and234Ordered:
between a,b,d & between b,c,d implies a,b,c,d are_ordered;
theorem :: GTARSKI1:23
between a,b,d & between b,c,d implies a,b,c,d are_ordered;
theorem :: GTARSKI1:24
between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9
implies a,c equiv a9,c9;
theorem :: GTARSKI1:25
a,b equiv c,d implies b,a equiv d,c;
theorem :: GTARSKI1:26
a <> b & between a,b,x & between a,b,y & a,x equiv a,y
implies x = y;
theorem :: GTARSKI1:27 ::: SegmentSubtraction:
between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9
implies b,c equiv b9,c9;
theorem :: GTARSKI1:28
o <> a implies
ex x,y st between b,o,x & between a,o,y & x,y,o cong a,b,o;
theorem :: GTARSKI1:29
between a,b,c & between a,c,d implies a,b,c,d are_ordered;
:: We now port Narboux's Coq proof of Gupta's result
:: a <> b & Babc & Babd -> Bacd or Badc.
:: with this one simplification: we isolate some lemmas. We begin
:: with two results that are not actually needed, but shed some light.
theorem :: GTARSKI1:30
a <> b & between a,b,c & between a,b,d
implies ex x st a,b,c,x are_ordered & a,b,d,x are_ordered;
:: We don't use this result, but there ought to be an easy proof of
:: it, and there is. The proof is largely due to Benjamin Kordesh.
theorem :: GTARSKI1:31 ::: GuptaEasy:
a <> b & between a,b,c & between a,b,d &
b <> c & b <> d implies not between c,b,d;
:: The next result is like SAS: there are 5 pairs of segments, 4
:: equivalent. We say we apply Inner5Segments to abc-x and a9b9c9-x9
theorem :: GTARSKI1:32
a,b,c cong a9,b9,c9 &
between a,x,c & between a9,x9,c9 & c,x equiv c9,x9
implies b,x equiv b9,x9;
theorem :: GTARSKI1:33
between b,c,d9 & between b,d,c9 &
c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d implies
ex e st between c,e,c9 & between d,e,d9 &
c,e equiv c9,e & d,e equiv d9,e;
theorem :: GTARSKI1:34
between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e &
c <> d & e <> d implies
ex p,r,q st between p,r,q & between r,c,d9 & between e,c,p &
r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e;
theorem :: GTARSKI1:35
a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q
implies c,p equiv c,q;
theorem :: GTARSKI1:36
between a,x,c & a,p equiv a,q & c,p equiv c,q
implies x,p equiv x,q;
theorem :: GTARSKI1:37
a <> b & between a,b,c & between a,b,d
implies between b,d,c or between b,c,d;
definition
let S, a, b, c;
pred Collinear a,b,c means
:: GTARSKI1:def 17 ::: :DefCollinear:
between a,b,c or between b,c,a or between c,a,b;
end;
definition
let S, a, b, x;
pred x on_line a,b means
:: GTARSKI1:def 18 ::: :DefLine:
a <> b & (between a,b,x or between b,x,a or between x,a,b);
end;
definition
let S, a, b, x, y;
pred a,b equal_line x,y means
:: GTARSKI1:def 19 ::: :DefLineEq:
a <> b & x <> y & for c holds c on_line a,b iff c on_line x,y;
end;
:: Using Gupta's theorem, we prove Hilbert's axiom I3, a line is
:: determined by two points.
theorem :: GTARSKI1:38
a <> b & a <> x & x on_line a,b &
c on_line a,b implies c on_line a,x;
theorem :: GTARSKI1:39
a <> b & a <> x & x on_line a,b implies
a,b equal_line a,x;
theorem :: GTARSKI1:40 :::LineEqRefl:
a <> b implies a,b equal_line a,b; :::NS
theorem :: GTARSKI1:41
a <> b implies a,b equal_line b,a;
theorem :: GTARSKI1:42 ::: LineEqSymmetric:
a <> b & c <> d & a,b equal_line c,d implies c,d equal_line a,b; :::NS
theorem :: GTARSKI1:43 ::: LineEqTrans:
a <> b & c <> d & e <> f & a,b equal_line c,d & c,d equal_line e,f
implies a,b equal_line e,f; :::NS
theorem :: GTARSKI1:44 ::: onlineEq:
x on_line a,b & a,b equal_line c,d implies x on_line c,d; :::NS
theorem :: GTARSKI1:45
a <> b & b <> y & y on_line a,b
implies a,b equal_line y,b;
theorem :: GTARSKI1:46 ::: I1:
a <> b & x <> y & a on_line x,y & b on_line x,y
implies x,y equal_line a,b;
begin :: Construction of the Euclidean Example
definition
func Tarski0Space -> MetrTarskiStr equals
:: GTARSKI1:def 20
the naturally_generated TarskiExtension of ZeroSpace;
end;
registration
cluster Tarski0Space -> Reflexive symmetric non empty;
end;
definition let M be non empty MetrStruct;
attr M is close-everywhere means
:: GTARSKI1:def 21
for a,b being Element of M holds
dist (a,b) = 0;
end;
registration
cluster Tarski0Space -> close-everywhere;
end;
registration
cluster Tarski0Space -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_SAS
satisfying_Pasch;
end;
definition
func TarskiSpace -> MetrTarskiStr equals
:: GTARSKI1:def 22
the naturally_generated TarskiExtension of RealSpace;
end;
registration
cluster TarskiSpace -> non empty;
end;
registration
cluster TarskiSpace -> Reflexive symmetric discerning;
end;
registration
cluster -> real for Element of TarskiSpace;
end;
registration
cluster -> real for Element of RealSpace;
end;
theorem :: GTARSKI1:47
for a, b, c being Element of RealSpace st
b in [.a,c.] holds b is_Between a,c;
registration
cluster TarskiSpace -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity;
end;