FOM: 79:Axioms for geometry -- A question and a program

[Vaughan Pratt]

Harvey Friedman:
HF>AN AXIOMATIZATION OF EUCLIDEAN PLANE GEOMETRY BASED ON DISTANCE COMPARISON
HF>We can define the field of real numbers in (R^2,E). This is done by
HF>equivalence classes of pairs of elements of R^2.

In other words, the field structure of R is definable from a certain
eight-dimensional variety E over R, presented as its characteristic
function on R^8.

(E is a variety because the equation d((a,b),(c,d)) = d((e,f),(g,h))
defining E is expressible as (a-c)^2+(b-d)^2 = (e-g)^2+(f-h)^2.)

This prompts the following question and program.

1.  What is the least dimension of variety over R from which the field
structure of R is definable in Friedman's sense?

2.  Characterize the class of all such varieties.

Vaughan Pratt