Reseña: Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski’s system of geometry

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski’s system of geometry.

Sus autores son Pierre Boutry, Julien Narboux y Pascal Schreck (del Équipe Informatique Géométrique et Graphique en la Universidad de Estrasburgo, Francia)

Su resumen es

In this paper we focus on the formalization of the proof of equivalence between different versions of Euclid’s 5 th postulate. This postulate is of historical importance because for centuries many mathematicians believed that this statement was rather a theorem which could be derived from the first four of Euclid’s postulates and history is rich of incorrect proofs of Euclid’s 5 th postulate. These proofs are incorrect because they assume more or less implicitly a statement which is equivalent to Euclid’s 5 th postulate and whose validity is taken for granted. Even though these proofs are incorrect the attempt was not pointless because the flawed proof can be turned into a proof that the unjustified statement implies the parallel postulate. In this paper we provide formal proofs verified using the Coq proof assistant that 10 different statements are equivalent to Euclid’s 5 th postulate. We work in the context of Tarski’s neutral geometry without continuity nor Archimedes’ axiom. The formalization provide a clarification of the hypotheses used for the proofs. Following Beeson, we study the impact of the choice of a particular version of the parallel postulate on the decidability issues.

El código de las correspondientes teorías en Coq se encuentra aquí.