[FOM] proof assistants and foundations of mathematics

[Harvey Friedman]

On Thu, Aug 9, 2018 at 4:30 AM, Franck Slama <franck.slama.pro at gmail.com> wrote:
> Hi,

> What is *the* foundation of traditional mathematics? I don't think there is
> such *a* foundation of "traditional" mathematics. If you're thinking about
> set theory, is it ZF? ZFC? General set theory? Kripke-Platek set theory?
> Something else?

The foundation of mathematics is currently and has been for some time
given by ZFC. E.g., Charles Fefferman, when he was acting as an Editor
of Annals of Mathematics, stated explicitly that the reference
standard for acceptable mathematical proof is currently ZFC. If you
want some special purpose foundations, then you will want to modify
ZFC in various ways, depending on the special purposes you have mind.
But for general purpose mathematics, this is ZFC.

> Many mathematicians (in fact, probably all that are not in the area of
> formal logic) work in an unspecified theory, and it's not a problem at all
> for them.

 For normal mathematical purposes, intuition is enough to avoid
actually consulting the "rule book". There is a little bit of an
analogy with say playing in professional bridge or go or chess
tournaments. The actual rule books are rather imposing documents,
which are, in some sense, more complicated than ZFC. Yet probably few
professional players have seriously read the rule books, but know that
it is definitive if on the rare occasion some serious issue arises.
Probably all professional bridge or go or chess players know and
appreciate that there really is an official rule book even if they do
not really look at it seriously.

> They work in something of the flavour of naive set theory, which,
> even if known to be inconsistent, is perfectly reasonable for doing everyday
> maths on the paper. And anyway, they very rarely need the "low level"
> machinery of the internal theory. They do maths in a naive theory as
> computer scientists do algorithmics in a high-level pseudo-code, without
> worrying about the assembly language and the needed transformation.

Theoretical Computer Science also has a very substantial and totally
accepted foundation.

> Of
> course, this could potentially lead to false proofs, but they are just
> careful to avoid using known paradoxes. It's only when one studies logic
> itself or tries to formalize things on a machine and to automatically verify
> proofs that working in such a naive and imprecise systems doesn't work any
> more. For such purposes, we have many formal systems, but I don't think
> there is a consensus on *the* foundation of "traditional" mathematics.

The situation is changing radically in several respects with regard to
mathematicians being able to rely on there being no point in becoming
familiar with ZFC and variants, and foundations of mathematics,
generally. This seems to be unfolding in a vivid way this year.
>
> On Wed, Aug 8, 2018 at 8:43 PM, José Manuel Rodriguez Caballero
> <josephcmac at gmail.com> wrote:
>>
>>
>> Does a proof of the incompleteness of Peano arithmetic in CIC is good as a
>> proof of the same result in Peter Andrews' Q0? Maybe this question is
>> trivial, but for someone like me, outside the world of foundations of
>> mathematics, it is a fundamental question. My intuition is that such a proof
>> in Q0 is better than the corresponding proof in CIC.
>
>
> Defining such an ordering between formal systems seems far from obvious to
> me. Of course, for two formal theories T1 and T2 sharing the same language,
> if the axioms of T1 are a strict subset of the axioms of T2, then indeed a
> proof of X in the theory T1 is better/stronger than a proof of X in T2. But
> how should we compare and rank two theories that don't follow this strict
> inclusion, with different axioms (that are independent from each other)? And
> how should we compare and rank theories that don't even share the same
> language? (for instance, type versus set, categories versus types, etc).
>
> Kind regards,
>
> Franck
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>