A constructive version of Tarski's geometry

DOI10.1016/J.APAL.2015.07.006zbMATH Open1392.03059arXiv1407.4399OpenAlexW1479730010MaRDI QIDQ490871FDOQ490871

Authors: Michael Beeson 

Publication date: 21 August 2015

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: Euclid's reasoning is essentially constructive. Tarski's elegant and concise first-order theory of Euclidean geometry, on the other hand, is essentially non-constructive, even if we restrict attention (as we do here) to the theory with line-circle and circle-circle continuity in place of first-order Dedekind completeness. Here we exhibit three constructive versions of Tarski's theory. One, like Tarski's theory, has existential axioms and no function symbols. We then consider a version in which function symbols are used instead of existential quantifiers. The third version has a function symbol for the intersection point of two non-parallel, non-coincident lines, instead of only for intersection points produced by Pasch's axiom and the parallel axiom; this choice of function symbols connects directly to ruler-and-compass constructions. All three versions have this in common: the axioms have been modified so that the points they assert to exist are unique and depend continuously on parameters. This modification of Tarski's axioms, with classical logic, has the same theorems as Tarski's theory, but we obtain results connecting it with ruler-and-compass constructions as well. In particular, points constructively proved to exist can be constructed with ruler and compass, uniformly in parameters; the same is true with non-constructive proofs if several constructions are allowed for different cases.

Full work available at URL: https://arxiv.org/abs/1407.4399

Recommendations

• Axiomatizing geometric constructions
• Constructive geometry
• Tarski geometry axioms
• The axioms of constructive geometry
• Constructibility and Geometry
• A further simplification of Tarski's axioms of geometry
• Finding proofs in Tarskian geometry
• On Tarski's foundations of the geometry of solids
• Constructive Axiomatizations of Plane Absolute, Euclidean and Hyperbolic Geometry

zbMATH Keywords

geometryconstructive mathematicsEuclidTarski

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Other constructive mathematics (03F65) Euclidean geometries (general) and generalizations (51M05) Geometric constructions in real or complex geometry (51M15)

Cites Work

• Title not available (Why is that?)
• Constructive geometry
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• From Tarski to Hilbert
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Title not available (Why is that?)
• Title not available (Why is that?)
• Über die Kreisaxiome
• Title not available (Why is that?)
• Tarski's System of Geometry
• Title not available (Why is that?)
• Foundations of geometry (Festschrift 1899). Edited and commented by Klaus Volkert
• Proof and Computation in Geometry
• Title not available (Why is that?)
• Forms of the Pasch axiom in ordered geometry
• Title not available (Why is that?)
• CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
• A further simplification of Tarski's axioms of geometry
• Title not available (Why is that?)

Cited In (18)

• A synthetic proof of Pappus' theorem in Tarski's geometry
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Proof-checking Euclid
• Formalization of the Poincaré disc model of hyperbolic geometry
• Constructive geometry
• Negation-free and contradiction-free proof of the Steiner-Lehmus theorem
• The axioms of constructive geometry
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Axiomatizing origami planes
• Brouwer and Euclid
• Full Development of Tarski's Geometry of Solids
• Implementing Euclid's straightedge and compass constructions in type theory
• Interpretations of Euclidean Geometry
• Title not available (Why is that?)
• CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
• Tarski geometry axioms
• Ternary Operations as Primitive Notions for Constructive Plane Geometry V
• Quantifier-free axioms for constructive affine plane geometry

This page was built for publication: A constructive version of Tarski's geometry

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q490871)