[FOM] Foundational Issues: Friedman/Carneiro

[Mario Carneiro]

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 suppose you are talking about informal proofs, which are only an
approximation to the above picture, so there is some loss of objectivity
there (since different mathematicians may disagree about how "obvious" the
steps are, etc.). I will not try to give a full explanation of how this
translates to informal proof, because the story becomes much more complex;
I'll leave it to the actual philosophers.

But at least with formal proof, it really boils down to an objective
answer, unless you want to consider cosmic rays causing your computer to
malfunction and verify a false proof (and the chances of this are
astronomically low). Bugs in the verifier are also a possibility, but this
can be mitigated by having multiple verifiers, a simple kernel, and of
course independent human verification of the proofs.

Mario

On Sat, Apr 9, 2016 at 2:32 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> On Fri, 8 Apr 2016, Mario Carneiro wrote:
>
>> The rubber meets the road when you actually start writing proofs, and at
>> this stage you are limited by your short human lifetime and the limited
>> patience of your reviewers ;) . So here we certainly have an "ultrafinite"
>> constraint. But the objects themselves, the things we purport to describe,
>> can be as crazy as our imaginations can take us. Furthermore, this still
>> does not preclude the idea that math is "discovered" instead of invented,
>> because the "matters of fact" (as Baez says), of the type "is P a proof of
>> A in the theory T" are objectively true or false
>>
>
> I thought I followed you up to this point, but here I don't understand how
> you arrive at the claim that a statement such as
>
> 1. P is a proof of A in the theory T
>
> is "objectively true or false."  I can see how you could claim that
>
> 2. All working mathematicians agree that P is a proof of A in the theory T
>
> is objectively true or false.  But 2 is much closer to
>
> 3. P is *known to be* a proof of A in the theory T
>
> than to 1.  So maybe you mean that 1 is synonymous with something like
>
> 4. If presented with the appropriate sensory stimuli, the mathematical
> community would arrive at a stable consensus that P is a proof of A in the
> theory T
>
> But 4 makes assertions about a somewhat nebulous hypothetical scenario and
> so it's not quite clear to me that such a counterfactual conditional is
> necessarily "objectively true or false".
>
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160411/11cf0aff/attachment-0001.html>