[FOM] What is a proof?

[Tjark Weber]

On Fri, 2009-01-23 at 17:08 +1300, Bill Taylor wrote:
> The key to clarifying debates about this, is the recognition that the word
> "proof" has two closely related yet starkly distinct meanings, when used
> in math, or more precisely in meta-mathematics.
> 
> Proof-1 is a very formal object; a sequences of lines in a strict formal
> language, usually FOL(=) with a few extra symbols and a shortish list
> of axioms (and schemas).  It must follow certain precise and simple rules.
> [...]
>
> Proof-2.  This is a somewhat more informal object, containing a lot of
> ordinary natural language as well as a fair amount of proof-1 material,
> though even this is usually in a highly modified and abbreviated form.
> Proof-2's are what typically appear in math journals.
> [...]

Checking the correctness of a Proof-2 is much harder than checking the
correctness of a Proof-1; the latter is purely mechanical and can be
done by a computer.

However, what Chow calls the "Euthyphro dilemma" applies to Proof-1
objects nevertheless.  They quickly become too large to be reliably
checked by humans.  If a computer checks a purported Proof-1 and outputs
"correct", can we be absolutely certain that the computer did the right
thing?

Whether the mathematical community accepts a proof (of any kind) is
inevitably a social process.

Regards,
Tjark