A constructive version of Tarski's geometry

DOI10.1016/J.APAL.2015.07.006zbMath1392.03059arXiv1407.4399OpenAlexW1479730010MaRDI QIDQ490871

Michael J. Beeson

Publication date: 21 August 2015

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

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

zbMATH Keywords

geometryTarskiconstructive mathematicsEuclid

Mathematics Subject Classification ID

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

Related Items (11)

A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Proof-checking Euclid ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Brouwer and Euclid ⋮ Negation-free and contradiction-free proof of the Steiner-Lehmus theorem ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Axiomatizing origami planes ⋮ Quantifier-free axioms for constructive affine plane geometry

Cites Work

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

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