The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Hi José,

Fellow student here. You should read up on Godel's incompleteness theorems and their implications for Hilbert's program. I know it's taken me many, many tries to get a feeling for what Godel's second incompleteness theorem means. Bearing in mind that I am by no means a master of this subject area, here are a few of my thoughts on your email.

Below, I assume (it appears obvious, but I'm not an expert) that the formal system Coq is covered by Godel's second incompleteness theorem. Wikipedia has a nice overview (https://en.wikipedia.org/wiki/Godel's_incompleteness_theorems) of the required conditions.

Defining your function Coq(n) in Coq, which requires proving Coq is consistent in Coq, is impossible by Godel. You could assume Coq is consistent as an axiom, but now your proof is not formalizable inside Coq. You could assume there is a proof that Coq is consistent inside (your formalized, deep embedding of) Coq, but then Godel's second incompleteness theorem gives you a proof of False.

The formalization `Coq in Coq` formalizes only a fragment of Coq, specifically the Calculus of Constructions (no inductive types). A quick glance suggests that it also supports only three universes, `prop`, `sort`, and `kind`, while full Coq has a countable infinity of universes. The proof of consistency does use inductive types, and I suspect that it uses higher universes than `kind`. Therefore, the proof can not be formalized inside the system being proved consistent.

More generally, I don't believe people expect all of Coq to be formalizable inside of Coq without any axioms (since this would entail a proof of False, infinite loops, things Coq was designed very carefully to avoid). I expect that Coq with finitely many universes is formalizable inside of Coq with one or two more universes, and I also expect that if you assume suitable extra axioms (for which there exists some computational model, or set theoretic model) perhaps corresponding to the existence of a universe containing all of Coq's countably infinite universes, you can prove Coq is consistent.

But neither of these allow a proof of the consistency of some theory inside the theory itself.

In conclusion, I agree that the function `Coq(n)` is not definable in Coq, and therefore that the function from a string of Coq code to the computed natural number (0 if type checking fails) is also not definable in Coq. However, in light of Godel's incompleteness theorems, this is not a terribly interesting result. Any formal system which can be checked by a computer (effective axiomatization) and can do basic arithmetic suffers from the same flaw. Just as set theory has large cardinal assumptions, universes in type theory are connected to proof theoretical power. Adding larger universes to prove consistency of systems with smaller universes is definitely begging the question. Unfortunately, Godel tells us that we can't help begging the question. Any notion of "metamathematical" proof or "natural" proof which can be represented in a formal system checkable by a computer and proves the consistency of Robinson arithmetic (which lacks induction!) can not prove its own consistency.

Best regards,

- Jasper Hugunin

On Mon, May 7, 2018 at 4:41 PM José Manuel Rodriguez Caballero <josephcmac AT gmail.com> wrote:

Hi, I know that there is a project of formalization of Coq in Coq: https://github.com/coq-contribs/coq-in-coq

I would like to know if the following (informal) argument can be formalized in Coq as a theorem (it is my version of Berry paradox).

Let Coq(n) be the largest natural number that can be defined in Coq using at most n characters from the keyboard of the programmer. It can be computed just checking all the possible arrays of n characters. It easily follows that the function fun (n : nat) => Coq(n) is non-decreasing and the limit of Coq(n) is infinite when n goes to infinite.

For all n, Coq(10^n) contains n+6 characters, where "10^n" is just a notation (we should write in Coq the actual number) . Let k be the number of characters of the implementation of the function fun (n : nat) => Coq(n)  in Coq. So, Coq(n+k+6) is at least Coq(10^n) for all n, because Coq(10^n) is a chain of n+6 characters in Coq and we can implement the function n -> Coq(n) using k characters. For each n large enough, Coq(t) is constant for all t in the interval [n+k+6 .. 10^n]. We can substitute n by n+1, in order to obtain that Coq(t) is constant for all t in [n+k+7 .. 10^(n+1)] for all n large enough. So, Coq(t) is constant for all t in [n+k+6 .. 10^(n+1)] for all n large enough. Hence, Coq(n) is constant for all n large enough, but this is absurd.

Therefore, the function fun (n : nat) => Coq(n) cannot be implemented in Coq.

Thank you in advance,

José M.