[FOM] Query: references on intuitionistic Euclidean geometry
negri at mappi.helsinki.fi
Fri Nov 20 07:40:58 EST 2009
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:
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
Academy Research Fellow,
Ph.D., Docent of Logic,
Department of Philosophy,
University of Helsinki,
More information about the FOM