The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I will stop taking part in this discussion as it is based on a
misunderstanding between our communities. In our comunity Gödel's theorems
are accepted and internalized: anyone saying "I prove consistency of Foo
using Bar" has simply proved Foo *inside* the logical system of Bar and
therefore "reduced" (or should we say "enlarge"?) consistency of Foo to
consistency of Bar. There is no misleading wording here, it is clear for
anyone in our community that Bar must be stronger than Foo (see it as a
consequence or as a prerequisite depending on the context).

If you are really looking for a logical system equivalent to PA that can be
auto-justified, I think I can speak in the name of this mailing and wish
you good luck :-).

Best  regards,
Pierre

Le jeu. 3 mai 2018 à 14:00, José Manuel Rodriguez Caballero <
josephcmac AT gmail.com>
 a écrit :

> Dear Michael,

>    First, I consider very important and interesting the opinion of a
physicist. As far as I know (discovery channel), there is not a unified
theory of physicist: for small scales you use Quantum Mechanics and for
large scales you use Relativity. Coq is like Relativity: it is very good
for traditional mathematics as such, but it is not good for foundations of
mathematics, because it is part of the problem that it presents to solve.
It is important to have another proof assistant for small scales
(foundations of mathematics and model theory).

> With respect to the universal truth, there is a consistent arithmetic
named relevant arithmetic and I think that its consistency is a kind of
universal truth or at least it satisfies Hilbert's standards of
metamathematical truth.

> Theorem. Let R# be the relevant arithmetic (defined in page 826 of [1]),
i.e. Peano axioms with first-order relevant logic in place of the classical
one. We have that R# is consistent.

> Reference: [1] Friedman, Harvey, and Robert K. Meyer. "Whither relevant
arithmetic?." The journal of symbolic logic 57.3 (1992): 824-831.
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/whither-relevant-arithmetic/C1A5D2F021B95DC9432A13C6963389DE

> In Coq you will only obtain the conditional: R# is consistent if Coq is
consistent. It is the same as: PA is consistent if Coq is consistent.
Nevertheless, the consistency of R# follows Hilbert's standards and the
consistency of PA does not follow these standards. I hope that the
consistency of R# will be interested for a physician (Roger Penrose was
interested in these kind of questions).

> Kind Regards,
> José M.



> 2018-05-03 12:42 GMT+02:00 Soegtrop, Michael 
> <michael.soegtrop AT intel.com>:

>> Dear José



>> > To say that the consistency of Peano arithmetic was verified using Coq
is misleading.

>> > This sentence promotes the idea that the consistency of arithmetic was
verified, in metamathematical way, using the software Coq as a tool



>> Probably as a physicist I shouldn’t comment on topics of foundational
mathematics, but reading the above statement I can say that even I as a
physicist wouldn’t interpret it this way. It is clear to me that Coq is
based on some axioms and/or logical foundation and that everything one can
prove in Coq is only true if this foundation is consistent. If this is
obvious to me as a physicist, I would think it is obvious to any
mathematician after the first semester, and I don’t think it is of any
value to emphasize this fact in claims. The wording “verified using Coq” is
perfectly adequate.



>> I would be astonished if the kind of absolute universal truth you are
after exists at all. I would think there is no truth without meaning and no
meaning without a foundation of common understanding. So truth always needs
a foundation. All one can do is minimize the foundation, maximize the truth
that can be derived based on it, and verify that the foundation one uses is
consistent with other foundations. As far as I can tell Coq is a fairly
good compromise in this.



>> Best regards,



>> Michael

>> Intel Deutschland GmbH
>> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
>> Tel: +49 89 99 8853-0, www.intel.de
>> Managing Directors: Christin Eisenschmid, Christian Lamprechter
>> Chairperson of the Supervisory Board: Nicole Lau
>> Registered Office: Munich
>> Commercial Register: Amtsgericht Muenchen HRB 186928