[FOM] Undecidability in geometry

[José Félix Costa]

Dear friends,

I am asking Francisco to send the draft of the paper (he is still asleep).

The idea is to have the 'line' of natural numbers and

     commands COMPASS[a,b] -- center in a and radius b --,

     and RULER[a,b] -- line through points a and b.

New lines and points are drawn and added during computations (like the
computable real sqrt(2) in a glance, but pi can be approximated successively
like in classical computability).

This abstract computer has the full power of Turing machines (and not more).

Some Euclidean proofs are immediately translated into programs.

This is similar, but not the same as the theory of real closed fields.

Regards,

Félix

+++++++++++++++++++++++++++++++++++++++++++++++
J. Felix Costa
Departamento de Matematica
Instituto Superior Tecnico
Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL
tel:      351 - 21 - 841 71 45
fax:     351 - 21 - 841 75 98
e-mail:   fgc at math.ist.utl.pt
www:    http://fgc.math.ist.utl.pt/jfc.htm
+++++++++++++++++++++++++++++++++++++++++++++++