[FOM] Certificates are Fully Practical

[Harvey Friedman]

When I talked about certificates in formalisms for the foundations of
mathematics, I am talking about actual proofs of actual mathematics, given
by actual mathematicians - of course expanded so that they become fully
rigorous.

Because of the extensive work on "proof assistants", we know from
experience (although I an many other people were convinced much earlier)
that this expansion process to fully rigorous proofs of actual mathematical
theorems by actual mathematicians is well under control and can be and has
been carried out in reality.

Granted, this has not been done for really big sophisticated proofs yet,
such as FLT and classification of finite simple groups. But there is now
little doubt that the certificates have completely feasible size, and will
be actually constructed, say by 2150.

This is in sharp contrast to non first order "foundations for mathematics"
without certificates. Before they become any sort of "foundations for
mathematics" one must pass to first order associates, where there are
certificates.

I view the work from proof assistants as strengthening the already
overwhelming case for the role of certificates, as proof assistants have
shown that they are entirely practical. There is even good data on the
actual size of the relevant certificates.

Harvey Friedman

On Fri, Sep 13, 2013 at 5:12 PM, Alan Weir <Alan.Weir at glasgow.ac.uk> wrote:

> One assumption which seems to be accepted by all so far, in the debate on
> 'What is second-order ZFC', is that a derivation, a 'certificate', must be
> finite. Indeed one usually requires that there be an algorithm for deciding
> whether a given formal structure is a proof, and if so of what sentence.
>
> But of course in the formal languages and systems which are our
> idealisations of informal mathematical practice, all but a tiny fragment of
> the constructions contain more parts than the estimated number of neutrinos
> in the observable universe. Perhaps more telling: we know from speed-up
> considerations (in reverse, as it were) that no matter what formal system
> we work with, there will be provable formulae which are  of 'feasible'
> length- their tokens can be grasped by us or at least by machines we can in
> some decent sense comprehend- but whose shortest proof will be unfeasibly
> long. This will be true even for polynomially decidable logic, a logic
> which is surely far too restricted to act as a formalisation of actual
> mathematical practice.
>
> Given all this, and assuming (as I think we should) that we nonetheless
> must idealise beyond the patchy fragment of our formal systems which we can
> feasibly digest, what is the rationale for idealising to systems, such as
> first-order logic, in which the theorems are recursively enumerable  but
> the anti-theorems are not, and in which the derivations are of lengths
> vastly beyond anything we can grasp? Why is omega-logic not a candidate for
> an idealisation of our informal practice; or more powerful infinitary
> logics? And if they are, does the fact that (full, non-Henkin) 2nd order
> logic is not complete tell against it any more than the fact that
> first-order logic is not decidable or propositional  logic is not
> polynomial-time decidable (if P is not NP)?
>
> I suggest there is no non-ad hoc limit on the power of the abstract
> idealisations which are formal systems, if they are to count as legitimate
> idealisations of informal proof.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130913/eeacd3a4/attachment-0001.html>