[FOM] Query: references on intuitionistic Euclidean geometry

[Vaughan Pratt]

Giovanni Sambin wrote:
 > 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.

Apropos of this question,  the equational theory of vector spaces over a 
fixed field can be axiomatized as a single-sorted theory having one 
unary operation for each element of the field, along with the language 
of groups.  While I understand the concept of intuitionistic logic as a 
first order logic, I don't know how it applies to an equationally 
axiomatized theory.  Is linear algebra when defined in this way 
considered a classical theory, an intuitionistic one, both, or neither?

This is of course not Euclidean geometry but affine (and with an origin 
but that's easily removed without leaving equational logic).   However 
the answer to the question for linear algebra (and hence affine 
geometry) might serve as a useful point of comparison for any answer to 
the corresponding question for Euclidean geometry.

Vaughan Pratt