[FOM] Foundational Issues: Friedman/Carneiro

[Mario Carneiro]

On Tue, Apr 12, 2016 at 8:39 AM, tchow <tchow at alum.mit.edu> wrote:

> 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.


In the case of "formal proof" (as well as of "string"), when the length is
not too long, we are physically capable of realizing it as bits in a
computer or words on a page. In this case I don't believe its "reality" can
meaningfully be questioned. This is also true for small numbers like 1 or
3. These might be seen as a physical realization of a more abstract notion
of "1" or "string" or "formal proof", which does not have the unpleasant
properties of being limited by size, and it is this latter thing, existing
in a platonic realm, whose existence I question.


> 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.
>

I suppose it is also a possibility to identify the things that "exist" in
the platonic realm with a sort of equivalence class of physical objects
under a similarity measure, which is what you seem to be suggesting here.
If I were to accept that, though, that would make me a true ultrafinitist,
since only finite things that are small enough to exist in the universe
will have representatives. Insofar as it is a convenient abstraction for
reasoning about mathematics, I like to keep my platonic realm unfettered by
the constraints of reality, and allow large finite objects and infinite
objects inside it.

I am fully aware that there is a "philosophy rabbit hole" to go down if one
pursues this topic too far. Ultimately, nothing in reality is absolutely
clear cut, but I am confident that (feasible) formal proofs (along with
small strings and small numbers) is the closest humanity has come to such
an ideal (which is why I got into formal proof in the first place).

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160412/154d95ac/attachment.html>