[FOM] Are Proofs in mathematics based on sufficient evidence?

[Monroe Eskew]

On Thu, Jul 15, 2010 at 2:21 PM, Vaughan Pratt <pratt at cs.stanford.edu> wrote:
>
> The problem comes at the step "join FC".  Postulate 5 ruled out
> hyperbolic geometry but not elliptical.  On the sphere, if the distance
> from F to C is more than half the circumference the segment FC will be
> the complete line FC less the segment drawn by Euclid in the diagram.
> This screws up the angles in the rest of the argument.

This can be viewed as an instance of a hidden assumption.  Hilbert's
axioms for plane geometry provide the needed assumptions-- the
incidence axiom which says that two lines meet only in one point.  One
can use Hilbert's axioms to perfect Euclid's proofs, without
introducing formal rules of derivation.  If we wish, we can take them
into formal FOL and use a standard formal proof system for FOL.  Or we
can work informally but rigorously as we do in ordinary mathematics.
The problem is not a lack of formal derivation rules; it is a lack of
ordinary validity because of the use of hidden assumptions.

Monroe