:: Tarski Geometry Axioms :: by William Richter , Adam Grabowski and Jesse Alama :: :: Received June 16, 2014 :: Copyright (c) 2014-2021 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, XREAL_0, METRIC_1, ORDINAL1, STRUCT_0, ZFMISC_1; requirements 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) TarskiGeometryStruct (# 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 TarskiGeometryStruct; mode POINT of S is Element of S; end; definition let S be TarskiGeometryStruct; 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 TarskiGeometryStruct; 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 TarskiGeometryStruct; 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 TarskiGeometryStruct; 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 TarskiGeometryStruct; 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 TarskiGeometryStruct; 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,TarskiGeometryStruct) 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 TarskiGeometryStruct; end; registration cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch -> satisfying_Tarski-model for TarskiGeometryStruct; cluster satisfying_Tarski-model -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch for TarskiGeometryStruct; end; begin :: Proving Properties reserve S for satisfying_Tarski-model TarskiGeometryStruct; 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 be TarskiGeometryStruct; let a,b,c be POINT of S; 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;