A common axiom set for classical and intuitionistic plane geometry (Q1295418)

The intuitionistic foundation of geometry goes back to Heyting's intuitionist axiomatisation of projective geometry, to be followed by an axiomatisation of affine geometry, with simplifications and further researches by \textit{D. van Dalen} [``Heyting and intuitionistic geometry'', in: P. P. Petkov (ed.), Mathematical logic, Proc. Summer School Conf., Chaika/Bulg. 1988, 19-27 (1990; Zbl 0770.03001); `` `Outside' as a primitive notion in constructive projective geometry'', Geom. Dedicata 60, No. 1, 107-111 (1996; Zbl 0846.51001)]. None of these axiomatisations address richer geometries, with geometric notions that go beyond incidence. The intuitionistic axiomatisation of orthogonality was attempted by \textit{J. von Plato} [``The axioms of constructive geometry'', Ann. Pure Appl. Logic 76, No. 2, 169-200 (1995; Zbl 0836.03034)], but since the main interest was intuitionistic type-theoretical, the geometry it describes is weak and was not investigated for its own sake. The paper under review presents an axiomatics for plane Euclidean geometry that is inspired from \textit{A. Tarski}'s ``What is elementary geometry?'' [in: L. Henkin et al. (eds.), The axiomatic method, Stud. Logic Found. Math., 16-29 (1959; Zbl 0092.38504)], with `points' as individual variables, and with a sexternary predicate Dist, with Dist\((a,b,c,d,e,f)\) to be read as \(| ab| + | cd| > | ef| \), as its only primitive notion. It has the noteworthy property that, when the axioms (i.e. the connectives and quantifiers that appear in them) are interpreted intuitionistically, they axiomatise in intuitionistic logic a theory IEG , which is strictly weaker than the classical theory CEG, obtained by interpreting the axioms classically, and CEG is equivalent tothe theory T axiomatised by Tarski with the elementary continuity axiom included (its models are Cartesian planes over real-closed fields). To show that IEG is weaker than CEG the authors use a realisability interpretation of Dist in recursive function theory (analogous to those given by Kleene for intuitionistic arithmetic and analysis) to prove that several of Tarski's axioms are unprovable in IEG. The actual strength of IEG remains open, for although CEG is complete (since it is equivalent to Tarski's T, which he showed to be complete), and IEG proves \(\varphi^N\) whenever CEG proves \(\varphi\) (where \(\varphi^N\) is the double-negation translation of \(\varphi\)), it is not clear whether all realisable formulae are provable in IEG (the converse is true, as shown in Th. 6.10). A representation theorem connecting IEG to some intuitionistic algebraic model would also be desirable.