The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

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