A constructive theory of ordered affine geometry

DOI10.1016/S0019-3577(98)80034-7MaRDI QIDQ1279729zbMATH OpenOpenAlexFDO

Authors Jan von Plato

Publication date 21 November 1999

Published in Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0019-3577(98)80034-7

zbMATH Keywords

affine geometryAnother Logical Frameworkapartness geometryconstructive geometryprojective geometry

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Intuitionistic mathematics (03F55) Other constructive mathematics (03F65) Ordered geometries (ordered incidence structures, etc.) (51G05)

Review text

The inclusion of some notion of orientation (or ordering) into the axiomatics for Euclidean geometry is necessary (although missing in Euclid's ``Elements), as we know since Pasch's ``Vorlesungen über neuere Geometrie (1882). The author extends his attempts towards a constructive axiomatization of elementary geometry [begun in the author's paper, Ann. Pure Appl. Logic 76, No. 2, 169-200 (1995; Zbl 0836.03034)], including a notion of ``unequally directed lines. These axioms allow to deduce Pasch's axiom, and to introduce a betweenness relation (or a pair of orders) on each line. Desargues' property (or embeddability into a space of higher dimension) is not discussed.

Recommendations

• scientific article; zbMATH DE number 3901538
• The axiomatics of ordered geometry: I. Ordered incidence spaces
• Weakly ordered plane geometry
• scientific article; zbMATH DE number 69210
• scientific article; zbMATH DE number 3866068

Cites work

• `Outside' as a primitive notion in constructive projective geometry
• scientific article; zbMATH DE number 3150814 (Why is no real title available?)
• Organization and development of a constructive axiomatization
• The axioms of constructive geometry

Cited in

(14)

• A proof of Pasch's axiom in the absolute theory of oriented parallelity
• On the simplicity of ordered geometry
• Axiomatizing geometric constructions
• Implementing Euclid's straightedge and compass constructions in type theory
• A constructive real projective plane
• scientific article; zbMATH DE number 3866068 (Why is no real title available?)
• scientific article; zbMATH DE number 3901538 (Why is no real title available?)
• scientific article; zbMATH DE number 27291 (Why is no real title available?)
• scientific article; zbMATH DE number 727656 (Why is no real title available?)
• The axiomatics of ordered geometry: I. Ordered incidence spaces
• Constructive geometry and the parallel postulate
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Simplifying the axiomatization for ordered affine geometry via a theorem prover
• Winkelmessung und Orientierung. (Measurement of angles and orientation)

Describes a project that uses

Uses Software

• ALF

This page was built for publication: A constructive theory of ordered affine geometry

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