[FOM] Query: references on intuitionistic Euclidean geometry

[Sara Negri]

Dear Giovanni,

Intuitionistic geometry was the topic of Heyting's doctoral thesis of  
1927, but the axioms were not the right ones. Richard Vesley gave in  
1998 an intuitionistic version of Euclidean geometry, the latter from  
Tarski's classical formulation:

Lombard, Melinda; Vesley, Richard
A common axiom set for classical and intuitionistic plane geometry.
Ann. Pure Appl. Logic 95 (1998), no. 1-3, 229--255.

It was based on an earlier intuitionistic axiomatics of projective and  
affine geometry that corrected Heyting's "mistake," namely, Heyting  
had incidence as a basic notion when he should have had "point outside  
a line," in analogy to the apartness relations for points and for  
lines that he used:

Jan von Plato
The axioms of constructive geometry.
Ann. Pure Appl. Logic 76 (1995), no. 2, 169--200.


Computer implementations of the latter exist, starting with the late  
Gilles Kahn. I don't know if these are extended to Vesley's work now.  
You can look at:

Narboux, Julien
A decision procedure for geometry in Coq.
Theorem proving in higher order logics, 225--240,
Lecture Notes in Comput. Sci., 3223, Springer, Berlin, 2004.

best regards, Jan von Plato

(visiting FOMmer through Sara Negri)

Quoting "Giovanni Sambin" <sambin at math.unipd.it>:

> Dear FOMers,
> a student of mine plans to write a thesis on Euclidean geometry
> developed over intuitionistic logic. I would appreciate any reference to
> books, papers, or  any other source on this topic.
> Thank you very much in advance for collaboration
> Giovanni Sambin
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>



Sara Negri

Academy Research Fellow,
Ph.D., Docent of Logic,
Department of Philosophy,
University of Helsinki,
http://www.helsinki.fi/~negri/