A Mechanical Verification of the Independence of Tarski's Euclidean Axiom

10.26686/wgtn.16999462 ◽

2021 ◽

Author(s):

◽

Timothy James McKenzie Makarios

Keyword(s):

Projective Plane ◽

Hyperbolic Plane ◽

Axiom System ◽

Plane Geometry ◽

Mechanical Verification ◽

The Real ◽

Cartesian Plane ◽

Proof Verification

<p>This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.</p>

Download Full-text

An Easy Proof for Some Classical Theorems in Plane Geometry

Canadian Mathematical Bulletin ◽

10.4153/cmb-1992-073-8 ◽

1992 ◽

Vol 35 (4) ◽

pp. 560-568 ◽

Cited By ~ 1

Author(s):

C. Thas

Keyword(s):

Projective Plane ◽

Projective Geometry ◽

The Other ◽

Plane Geometry ◽

The Real ◽

Easy Proof ◽

Special Cases ◽

Euclidean Planes ◽

Straight Lines ◽

Short Method

AbstractThe main result of this paper is a theorem about three conies in the complex or the real complexified projective plane. Is this theorem new? We have never seen it anywhere before. But since the golden age of projective geometry so much has been published about conies that it is unlikely that no one noticed this result. On the other hand, why does it not appear in the literature? Anyway, it seems interesting to "repeat" this property, because several theorems in connection with straight lines and (or) conies in projective, affine or euclidean planes are in fact special cases of this theorem. We give a few classical examples: the theorems of Pappus-Pascal, Desargues, Pascal (or its converse), the Brocard points, the point of Miquel. Finally, we have never seen in the literature a proof of these theorems using the same short method see the proof of the main theorem).

Download Full-text

Gilles Deleuze's Luminous Philosophy

10.3366/edinburgh/9781474450713.001.0001 ◽

2020 ◽

Author(s):

Hanjo Berressem

Keyword(s):

Projective Plane ◽

Visual Arts ◽

Whole Body ◽

Literary Studies ◽

Chronological Order ◽

Real Projective Plane ◽

Cinema Studies ◽

The Real

Providing a comprehensive reading of Deleuzian philosophy, Gilles Deleuze’s Luminous Philosophy argues that this philosophy’s most consistent conceptual spine and figure of thought is its inherent luminism. When Deleuze notes in Cinema 1 that ‘the plane of immanence is entirely made up of light’, he ties this philosophical luminism directly to the notion of the complementarity of the photon in its aspects of both particle and wave. Engaging, in chronological order, the whole body and range of Deleuze’s and Deleuze and Guattari’s writing, the book traces the ‘line of light’ that runs through Deleuze’s work, and it considers the implications of Deleuze’s luminism for the fields of literary studies, historical studies, the visual arts and cinema studies. It contours Deleuze’s luminism both against recent studies that promote a ‘dark Deleuze’ and against the prevalent view that Deleuzian philosophy is a philosophy of difference. Instead, it argues, it is a philosophy of the complementarity of difference and diversity, considered as two reciprocally determining fields that are, in Deleuze’s view, formally distinct but ontologically one. The book, which is the companion volume toFélix Guattari’s Schizoanalytic Ecology, argues that the ‘real projective plane’ is the ‘surface of thought’ of Deleuze’s philosophical luminism.

Download Full-text