A common axiom set for classical and intuitionistic plane geometry

DOI10.1016/S0168-0072(98)00017-7zbMath0922.03082OpenAlexW2062971860WikidataQ114012779 ScholiaQ114012779MaRDI QIDQ1295418

Melinda Lombard, Richard E. Vesley

Publication date: 11 October 1999

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

Full work available at URL: https://doi.org/10.1016/s0168-0072(98)00017-7

zbMATH Keywords

intuitionistic logicaxiomatics for plane Euclidean geometryintuitionistic foundation of geometry

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Foundations of classical theories (including reverse mathematics) (03B30) Metamathematics of constructive systems (03F50) Euclidean geometries (general) and generalizations (51M05) Intuitionistic mathematics (03F55)

Related Items (9)

A constructive real projective plane ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Constructive geometrical reasoning and diagrams ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Brouwer and Euclid ⋮ Negation-free and contradiction-free proof of the Steiner-Lehmus theorem ⋮ Constructivity in Geometry ⋮ Axiomatizing geometric constructions ⋮ Constructibility and Geometry

Cites Work

• Automated development of Tarski's geometry
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• Realizing Brouwer's sequences
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Tarski and geometry
• Ternary Operations as Primitive Notions for Constructive Plane Geometry
• Ternary Operations as Primitive Notions for Constructive Plane Geometry V
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A common axiom set for classical and intuitionistic plane geometry