# A constructive version of Tarski's geometry

@article{Beeson2015ACV, title={A constructive version of Tarski's geometry}, author={Michael Beeson}, journal={Ann. Pure Appl. Log.}, year={2015}, volume={166}, pages={1199-1273} }

Abstract Constructivity, in this context, refers to a theory of geometry whose axioms and language are closely related to ruler and compass constructions. It may also refer to the use of intuitionistic (or constructive) logic, but the reader who is interested in ruler and compass geometry but not in constructive logic will still find this work of interest. Euclid's reasoning is essentially constructive (in both senses). Tarski's elegant and concise first-order theory of Euclidean geometry, on… Expand

#### Figures and Topics from this paper

#### 21 Citations

From Hilbert to Tarski

- Mathematics
- 2016

In this paper, we describe the formal proof using the Coq proof assistant that Tarski's axioms for plane neutral geometry (excluding continuity axioms) can be derived from the corresponding Hilbert's… Expand

Constructive Geometry and the Parallel postulate

- Mathematics, Computer Science
- Bull. Symb. Log.
- 2016

This paper completely settle the questions about implications between the three versions of the parallel postulates: the strong parallel postulate easily implies Euclid 5, and in fact Euclid5 also implies the strong Parallel Postulate, although the proof is lengthy, depending on the verification that Euclid 4 suffices to define multiplication geometrically. Expand

Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq

- Mathematics, Computer Science
- Journal of Automated Reasoning
- 2017

This paper develops a large library in planar neutral geometry, including the formalization of the concept of sum of angles and the proof of the Saccheri–Legendre theorem, which states that assuming Archimedes’ axiom, the sum of the angles in a triangle is at most two right angles. Expand

A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

- Mathematics, Computer Science
- Journal of Automated Reasoning
- 2016

This paper reports on the formalization of a synthetic proof of Pappus’ theorem, which is an important milestone toward obtaining the arithmetization of geometry, which will allow to provide a connection between analytic and synthetic geometry. Expand

Brouwer and Euclid

- Mathematics
- 2017

We explore the relationship between Brouwer's intuitionistic mathematics and Euclidean geometry. Brouwer wrote a paper in 1949 called "The contradictority of elementary geometry". In that paper, he… Expand

A Finite, Feasible, Quantifier-free Foundation for Constructive Geometry

- Mathematics
- 2020

In this paper we will develop an axiomatic foundation for the geometric study of straight edge, protractor, and compass constructions, which while being related to previous foundations, will be the… Expand

A Galois connection between classical and intuitionistic logics. II: Semantics

- Mathematics
- 2013

In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper "was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a… Expand

From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry

- Mathematics, Computer Science
- SCSS
- 2016

The formalization of the arithmetization of Euclidean geometry in the Coq proof assistant is described, derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the Grobner basis method. Expand

A short note about case distinctions in Tarski's geometry

- Mathematics
- 2014

In this paper we study some decidability properties in the context of Tarski's axiom system for geometry. We removed excluded middle from our assumptions and studied how our formal proof of the first… Expand

Implementing Euclid’s straightedge and compass constructions in type theory

- Computer Science
- Annals of Mathematics and Artificial Intelligence
- 2018

This paper outlines the implementation of Euclidean geometry based on straightedge and compass constructions in the intuitionistic type theory of the Nuprl proof assistant, which enables a concise and intuitive expression of Euclid’s constructions. Expand

#### References

SHOWING 1-10 OF 57 REFERENCES

Constructive Geometry and the Parallel postulate

- Mathematics, Computer Science
- Bull. Symb. Log.
- 2016

This paper completely settle the questions about implications between the three versions of the parallel postulates: the strong parallel postulate easily implies Euclid 5, and in fact Euclid5 also implies the strong Parallel Postulate, although the proof is lengthy, depending on the verification that Euclid 4 suffices to define multiplication geometrically. Expand

Constructive Geometry

- 2009

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. A consideration of the relation of the… Expand

A further simplification of Tarski's axioms of geometry

- Mathematics
- 2013

A slight modification to one of Tarski's axioms of plane Euclidean geometry is proposed. This modification allows another of the axioms to be omitted from the set of axioms and proven as a theorem.… Expand

From Tarski to Hilbert

- Mathematics, Computer Science
- Automated Deduction in Geometry
- 2012

This paper mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski's book: Metamathematische Methoden in der Geometrie to provide clear foundations for other formalizations of geometry and implementations of decision procedures. Expand

Tarski's system of geometry

- Mathematics, Computer Science
- Bull. Symb. Log.
- 1999

This paper is an edited form of a letter written by the two authors (in the name of Tarski) to Wolfram Schwabhauser around 1978. It contains extended remarks about Tarski's system of foundations for… Expand

Proof and Computation in Geometry

- Mathematics, Computer Science
- Automated Deduction in Geometry
- 2012

A new first-order theory of “vector geometry” is given, suitable for formalizing geometry and algebra and the relations between them, and some experiments in automated deduction in these areas are reported on. Expand

Euclidean and non-Euclidean geometries

- Mathematics
- 1974

Lecture 1 April 6 2013 Euclidean and Non-Euclidean geometries The earliest written text on geometry is an Egyptian papyrus dated to the 2 millennia B.C. The geometry at that time was a collection of… Expand

Some Metamathematical Problems Concerning Elementary Hyperbolic Geometry

- Mathematics
- 1959

Publisher Summary This chapter discusses how the solutions of the metamathematical problems can be obtained by means of a familiar algorithm and the end-calculus of Hilbert. There is an illustration… Expand

Forms of the Pasch axiom in ordered geometry

- Computer Science, Mathematics
- Math. Log. Q.
- 2010

We prove that, in the framework of ordered geometry, the inner form of the Pasch axiom (IP) does not imply its outer form (OP). We also show that OP can be properly split into IP and the weak Pasch… Expand

Geometry: Euclid and Beyond

- Mathematics
- 2005

1. Euclid's Geometry.- 2. Hilbert's Axioms.- 3. Geometry over Fields.- 4. Segment Arithmetic.- 5. Area.- 6. Construction Problems and Field Extensions.- 7. Non-Euclidean Geometry.- 8. Polyhedra.-… Expand