0

Question: How bad is Coq proving both $T$ and $\lnot T$? Can it be abused?

Back in 2011 on the coq-club mailing list there was a thread: Is the Daniel Schepler's inconsistency real?. In the thread Georgi Guninski is me.

Inline in it there are two files (file 1) and (file 2), which are minor modifications of Daniel's code.

In 2023 all of the following can be proved based on the files.

  1. $T$
  2. $\lnot T$.
  3. Taking $T$ as axiom, we can prove $False$.
  4. Taking $\lnot T$ as axiom, we can prove $False$.

Proving $T$ and $\lnot T$ doesn't lead to proof of $False$, with a Coq error.

joro
  • 24,174

1 Answers1

9

Having read the Coq club conversation, I think your summary is slightly misleading. One can prove T with universe constraints X, and one can prove ~ T with universe constraints Y, but the constraints X and Y are incompatible, which is why it is not possible to prove T /\ ~ T. (The Coq error is not a bug, it's a desired state of affairs.)

The main reason I think this presentation is misleading, is that the universe constraints are part of the statement, even if they are usually hidden from the user (because most of the time the user doesn't need to think about them). But they are still there! The given examples of T and ~ T are not actually opposites of each other if you take the universe constraints into account. So everything is fine.

Gerry Myerson
  • 39,024
Ana Borges
  • 191
  • 2
  • Very interesting; is this the same, in some sense, as different things being true in different set theoretical universes? (i.e. different underlying axiomatic systems)? – Alec Rhea Aug 23 '23 at 15:32
  • 4
    @AlecRhea: No. Universe constraints are an indexing scheme to avoid the type of all types paradox. Instead you have hierarchy $Type_0$ in $Type_1$ in $Type_2$... A simplified version of the issue is something like this: proof of $T$ requires that if $a$ is in $Type_n$ then $b$ must be in $Type_{n+1}$, but the proof of $\lnot T$ requires that if $b$ is in $Type_m$ then $a$ must be in $Type_{m+1}$. It's impossible to have both constraints at the same time. – François G. Dorais Aug 23 '23 at 20:17
  • @FrançoisG.Dorais Thank you for clarifying! – Alec Rhea Aug 24 '23 at 01:31
  • Thanks. So Coq's proof of $T$ is not what human mathematician will expect? Coq's proof has additional constraints on the usage of $T$? – joro Aug 24 '23 at 08:31
  • 1
    Just like certain theorems used by very human mathematicians (think the various adjoint functor theorems in category theory) have size conditions on universes of sets, this is also the case of the proofs of $T$ and $\sim T$ here. The fact that one can overlook these side conditions by not being precise about what one means when writing Type or "set" does not mean that "human mathematicians" would not have to consider these. And indeed, as this example shows, overlooking them has a dire impact on consistency, just like the adjoint functor theorem without size restrictions is simply not true. – Meven Lennon-Bertrand Aug 24 '23 at 10:37