[FOM] proof assistants and foundations of mathematics

[Franck Slama]

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/20180809/55577bc5/attachment-0001.html>