Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid

Roland Coghetto 📧

January 31, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The GeoCoq library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high school. We port a part of the GeoCoq 2.4.0 library to Isabelle/HOL: more precisely, the files Chap02.v to Chap13_3.v, suma.v as well as the associated definitions and some useful files for the demonstration of certain parallel postulates. The synthetic approach of the demonstrations is directly inspired by those contained in GeoCoq. The names of the lemmas and theorems used are kept as far as possible as well as the definitions.

It should be noted that T.J.M. Makarios has done some proofs in Tarski's Geometry. It uses a definition that does not quite coincide with the definition used in Geocoq and here. Furthermore, corresponding definitions in the Poincaré Disc Model development are not identical to those defined in GeoCoq.

In the last part, it is formalized that, in the neutral/absolute space, the axiom of the parallels of Tarski's system implies the Playfair axiom, the 5th postulate of Euclid and Euclid's original parallel postulate. These proofs, which are not constructive, are directly inspired by Pierre Boutry, Charly Gries, Julien Narboux and Pascal Schreck.

License

GNU Lesser General Public License (LGPL)

History

April 18, 2025
Split Tarski_Neutral.thy into 3 files: Tarski_Neutral.thy Tarski_Neutral_2D.thy Tarski_Postulate_Parallels.thy Modify ROOT Move locale Tarski_neutral_2D and 2D-lemma to Tarski_Neutral_2D.thy Move 2D-lemma to Tarski_Neutral_2D.thy Move postulate-lemma to Tarski_postulate_Parallels.thy (revision 90b76ef4bc10)
January 31, 2021
Initial Version INITIAL: CREATE: Tarski_Neutral.thy ========================== locale Tarski_neutral_dimensionless locale Tarski_2D context Tarski_neutral_dimensionless Definitions (with arity left,right) ----------------------------------- WARNING: Perp2(1,4): GeoCoq Perp2 A B C D E :: IsaGeoCoq E Perp2 A B C D OFSC(4,4) Cong3(3,3) Col(0,3) Bet4(0,4) BetS(0,3) FSC(4,4) IFSC(4,4) Le(2,2) Lt(2,2) Ge(2,2) Gt(2,2) Out(1,2) Midpoint(1,2) Per(0,3) PerpAt(1,4) Perp(2,2) Coplanar(0,4) TS(2,2) ReflectL(2,2) Reflect(2,2) InAngle(1,3) ParStrict(2,2) Par(2,2) Plg(0,4) ParallelogramStrict(0,4) ParallelogramFlat(0,4) Parallelogram(0,4) Rhombus(0,4) Rectangle(0,4) Square(0,4) Lambert(0,4) OS(0,4) TSP(3,2) OSP(3,2) Saccheri(0,4) ReflectLAt(1,4) ReflectAt(1,4) upper_dim_axiom[UpperDimAxiom](0,0) all_coplanar_axiom[AllCoplanarAxiom](0,0) CongA(3,3) LeA(3,3) LtA(3,3) GtA(3,3) Acute(0,3) Obtuse(0,3) OrthAt(1,4) Orth(3,3) SuppA(3,3) SumA(6,3) TriSumA(3,3) SAMS(0,6) Inter(1,4) Perp2(1,4) QCong(0,1) TarskiLen(0,3) QCongNull(0,1) QCongA(0,1) Ang(3,1) QCongAAcute(0,1) AngAcute(3,1) QCongANullAcute(0,1) QCongAnNull(0,1) QCongAnFlat(0,1) IsNullAngaP(0,1) QCongANull(0,1) AngFlat(0,1) tarski_s_parallel_postulate[TarskiParallelPostulate](0,0) euclid_5[Euclid5](0,0) euclid_s_parallel_postulate[EuclidSParallelPostulate](0,0) playfair_s_postulate[PlayFairSPostulate](0,0) Porting Files ------------- theories/Main/Tarski_dev/Ch02_cong.v theories/Main/Tarski_dev/Ch03_bet.v theories/Main/Tarski_dev/Ch04_col.v theories/Main/Tarski_dev/Ch04_cong_bet.v theories/Main/Tarski_dev/Ch05_bet_le.v theories/Main/Tarski_dev/Ch06_out_lines.v theories/Main/Tarski_dev/Ch07_midpoint.v theories/Main/Tarski_dev/Ch08_orthogonality.v theories/Main/Tarski_dev/Ch09_plane.v theories/Main/Tarski_dev/Ch10_line_reflexivity.v theories/Main/Tarski_dev/Ch10_line_reflexivity_2.v theories/Main/Tarski_dev/Ch11_angles.v theories/Main/Annexes/suma.v theories/Main/Tarski_dev/Ch12_parallel.v theories/Main/Tarski_dev/Ch12_parallel_inter_dec.v theories/Main/Tarski_dev/Ch13_1.v theories/Main/Tarski_dev/Ch13_2_length.v theories/Main/Tarski_dev/Ch13_3_angles.v theories/Main/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v theories/Main/Meta_theory/Parallel_postulates/tarski_euclid.v theories/Main/Meta_theory/Parallel_postulates/tarski_playfair.v (revision f5710bbb2d80)

Topics

Session IsaGeoCoq