[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

>
> Franck said:
> 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


We don't need to consider such a generalization of the problem in order to
make sense to my particular statement: Q0 has greater consistency strength
than CIC. If we prefer to use just type theories, we can say
that:  simply-typed lambda calculus has greater consistency strength than
Calculus of Inductive Constructions. For this reason, Mathematics should be
formalized in simply-typed lambda calculus in a first attempt. If this is
impossible, then the remaining theorems should be formalized in an stronger
type theory and so on. Calculus of Inductive Constructions should be one of
the last resources to use.

Which famous theorems could be formalized in Calculus of Inductive
Constructions which cannot be formalized in Simple Type Theory? I think
that this question is fundamental.

Jose M.


Message: 5
> Date: Thu, 9 Aug 2018 10:30:29 +0200
> From: Franck Slama <franck.slama.pro at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc: tchow at math.princeton.edu
> Subject: Re: [FOM] proof assistants and foundations of mathematics
> Message-ID:
>         <CAO+630Kh+YLEfYy8MTyS6-uoXxZU_uyUj-0jDJUYXD=XgE7dFg@
> mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Hi,
>
> On Wed, Aug 8, 2018 at 8:43 PM, Jos? Manuel Rodriguez Caballero <
> josephcmac at gmail.com> wrote:
>
> >
> > "X could be used for foundations of mathematics if the foundations of X
> > are strictly less doubtful than the foundations of traditional
> mathematics"
> >
>
> 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?
> 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. 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. 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.
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180810/c4828022/attachment-0001.html>