The Coq mailing list

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

Russell said:

"I also want to point out that proving that PA is consistent doesn't by itself mean that there isn't a proof that PA is inconsistent”

Ok, we are not talking the same language. In my world: PA is consistent means that there isn't a proof that PA is inconsistent (a proof that 1=0 formalized inside PA). I’m following Hilbert’s metamathematical standards: https://plato.stanford.edu/entries/hilbert-program/

Pierre said:

So IMHO to refute O'Connor's claim you need to chose between

these two points:
Refutation 1) you show that CIC is inconsistent.
Or:
Refutation 2) you show that his encoding of PA is not correct by showing
that some formula is provable in his encoding and not in the "real" one, or
the reverse.

I propose the following mental experiment:

X: Unicorns exist.

Y: Why?

X: Because a unicorn told me that unicorns exist and unicorns don’t lie.

Y: This is begging the question.

Z: To refute X you should prove that unicorns could lie.

Let’s study a more complex situation:

X: PA is consistent

Y: Why?

X: Because the natural numbers from Coq are a model of PA. The consistency of CiC is stronger than the consistency of PA.

Y: This is begging the question.

Z: To refute X you should prove that either CiC is inconsistent or that there is a problem in the encoding of PA in Coq made by X.

On May 2, 2018, at 5:56 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi,

But it is still just a matter of being careful right? You can
always reencode a logical system (say S) inside your preferred
one (say T, more expressive than S) as a regular first class
definition. And then you can use the whole power of T to prove
things about S, right? Nothing wrong with that, or do I miss
something? If you have defined in T what provability in S means
you can't be wrong by using the whole power of T. So pointing at
the T itself (CIC here) used to prove things about S (PA) is not a
valid objection IMHO.

The only things I see that can go wrong are:
1) T is inconsistent, but that is Gödel's curse, you can't remove
   this assumption.
2) S is not correctly encoded in T, which you seem to suggest by
   saying that defining PA in a recursion aware framework is bad.

So IMHO to refute O'Connor's claim you need to chose between
these two points:

Refutation 1) you show that CIC is inconsistent.

Or:

Refutation 2) you show that his encoding of PA is not correct by showing
that some formula is provable in his encoding and not in the "real" one, or
the reverse.

I don't think you can convince anyone on this list otherwise.

Hope this helps,

P.


Le mer. 2 mai 2018 à 16:51, Jose Manuel Rodriguez Caballero <
josephcmac AT gmail.com> a écrit :

Dear Chlipala and Amorim,

I answer you questions.

Question 1: Is there any formal system that you find good for doing

interesting mathematics and is free of foundational problems when applied
as an autonomous foundation of mathematics?

Answer: It depends the kind of mathematics you want to do. If you want to

mechanize Differential Geometry, Partial Differential Equations and
Algebraic Number Theory, then CiC is fine. But if you want to mechanize
something which does not assume the definition induction scheme of CiC, you
should definitively use another formal system in order to avoid circular
reasoning from a metamathematical point of view. In my personal case, I
prefer UniMath, but this is just a personal choice. The UniMath library
uses only the Martin-Lof type theory fragment of the CiC. This is because
my research in Model Theory is in conflict with the definition induction
scheme of CiC. I think that there are several mechanized proofs related to
foundations of arithmetic which should be looked from a more critical point
of view, in particular the so-called proof of the "consistency of
arithmetic” (it looks to me like to cure cancer with aids).

Question 2: Many cultures have words for the first few natural numbers

but don't recognize an infinity of numbers.

Answer: there are mathematical universes (elementary topoi) without the

notion of natural numbers:
https://www.youtube.com/watch?v=_7uONqXQvp8&t=1238s

Question 3: it is silly to pretend that inductive definitions need to be

justified in terms of the natural numbers

Answer: In CiC the inductive definitions are given in terms of natural

numbers from the beginning. This is not the case of ZFC, for example.

Question 4: CIC is so simple that all highly educated people across all

societies can understand the proof-validity judgment and apply it
identically, and at the same time CIC is expressive enough that it can be
used to encode all the problems of interest.

Answer: If for you problems of interest are from Differential Geometry,

Partial Differential Equations and Algebraic Number Theory, then CiC is for
you. On the other hand, for delicate questions concerning the foundation of
arithmetic and first-order model theory, CiC is less confortable than
  Martin-Lof type theory, because the induction axiom scheme becomes an
obstacle and you need to simulate a theory that is weaker than CiC itself
(O’Connor approach).

I think that Coq should have a way to invalide CiC in order to work only

with Martin-Lof type theory. That will be helpful for people working in
Model Theory and Foundations of Arithmetic.

Kind Regards,
José M.

On May 2, 2018, at 1:57 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 05/02/2018 12:45 AM, José Manuel Rodriguez Caballero wrote:

(1) Voevodsky's argument: "CIC is not cleaned defined, because it is an

initial model of a theory which itself requires natural numbers to be
specified",

Let me give an engineer's (e.g., my) perspective on these questions.

All of our deliberations are based on human mental hardware.  Tree

structures are built into our brains, in the modules for processing natural
language.  I believe results from cognitive science, including surveys of
cultures around the world, establish that natural numbers are actually not
such a natural (inborn) concept, while parsing language into trees is
universal!  (Many cultures have words for the first few natural numbers but
don't recognize an infinity of numbers.)  Therefore, it is silly to pretend
that inductive definitions need to be justified in terms of the natural
numbers.  Human brains do the opposite.

We are going to accept some set of axioms, and it is economical to pick

ones that map well to the proof-checking hardware -- our brains.  CIC is so
simple that all highly educated people across all societies can understand
the proof-validity judgment and apply it identically, and at the same time
CIC is expressive enough that it can be used to encode all the problems of
interest.  I see little practical value in rejecting any system with those
properties, when unsoundness hasn't been found empirically after extensive
use.