[FOM] Foundational Issues: Friedman/Carneiro

[tchow]

On 2016-04-11 20:14, Mario Carneiro wrote:
> Your reaction is very interesting. I suppose I should observe that my
> background is in computer mathematics, so when I say "proof" I really
> mean "formal proof". Given a formal proof P of a statement A in some
> formalization software, it is generally a trivial matter to run the
> software, to check that all the steps in the proof are valid. If this
> is true, then it is a proof, otherwise not. It's very clear cut when
> you have data of this quality.

I do not believe that "formal proof" is so clear-cut if "string" is not
clear-cut.  Doesn't a formal proof consist of strings?  There is some
kind of platonistic abstraction going on.  The formal proof cannot be
identified with a particular section of your disk drive because it is
still the same formal proof when it is copied to a different disk drive,
right?  There is some platonistic notion of a "formal proof in Coq" that
lets you make the identification between different physical realizations
of it.

It only *seems* clear-cut because you have been seduced by the behavior
of the community of human beings around you that behave in a coherent
manner, according to your expectations.  But if we allow ourselves to be
so seduced then why not allow ourselves to be seduced into thinking that
the number 3 is also a clear-cut platonically existing entity?  I 
suspect
that until the 20th century, there was much more consensus about how
clear-cut '3' was than about what a 'string' was.

Tim Chow