The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, June 25, 2011 05:18:41 AM Georgi Guninski wrote:
> Is the Daniel Schepler's inconsistency real?
> 
> Daniel Schepler proved [1][2] both T and ~T using only a plausible axiom
> and I couldn't find any cheating in his proof (I admit I am dumb).
> 
> Possibly due to a coq ``anomaly'' (read a bug) coq gives strange error when
> using both T and ~T (well maybe coded on purpose)
> 
> In his code T and ~T are [uat_maximal_card] and [uat_not_maximal_card].
> 
> Assuming excluded middle, does it mean one of T and ~T is necessarily true
> so it can be taken as an axiom?
> 
> According to my tests if I take as an axiom one of them, in *both* cases I
> can prove False using exactly his approach. One of the proofs will have
> axiom False (genuinely proved by him but unusable due to a bug), but the
> other must be real inconsistency.
> 
> For testing I just replaced [Lemma] by [Axiom] and commented out the
> proof (leaving the proof for the contrary).
> 
> Is this correct?

Let me try to explain what the "paradox" is that I'm formalizing, and what 
the 
resolution is.  I forget the exact name of the paradox, but it's essentially 
the Burali-Forti paradox with cardinals instead of ordinals.  If you 
formulate 
it in ZFC, getting two contradictory statements about the cardinality of the 
collection V of all sets, it's also closely related to the Russell paradox if 
you unfold Cantor's diagonalization argument.

Essentially, if you let U be the disjoint union of all types, and consider 
the 
cardinality mu of U, then you can seem to get two contradictory statements 
about it.  First, for any cardinality kappa which is the cardinality of a 
type 
X, you obviously have an injection from X to U by the inclusion map.  
Therefore, kappa <= mu [uat_maximal_card].  But by Cantor diagonalization, 
2^mu > mu [uat_not_maximal_card].

Here, the key to resolving the apparent paradox is to consider Coq's type 
hierarchy closely.  Suppose the Type in the definition of union_of_all_types 
is 
Type(n).  Then union_of_all_types is in Type(n+1).  Now, in the proof of 
uat_maximal_card, we feed X as an argument of type_inc.  In order for this to 
be valid, the Type in the statement of uat_maximal_card must be at level 
Type(n) or lower.  On the other hand, in the proof of uat_not_maximal_card, 
we 
feed (union_of_all_types -> Prop) into X, which is in Type(n+1), so for this 
statement to be valid the Type here must be Type(n+1) or higher.  If you turn 
on display of universe levels just before trying to process the Qed of 
contradiction, Coq will print an error message like

Error: Universe inconsistency (cannot enforce Top.8 = Top.61).

Here Top.8 is the level of Type in uat_maximal_card and Top.61 is the level 
of 
Type in uat_not_maximal_card.  It wants the two levels to be equal in order 
to 
be able to derive the contradiction False, while internally it must have 
found 
restraints that imply that Top.8 < Top.61.

So as another way of saying it, all this argument proves is that it would be 
inconsistent to assign union_of_all_types to the same level universe 
represented by the Type level in the declaration in type_inc (or lower).  But 
if you "Print union_of_all_types." with universe level printing on, it shows

Inductive union_of_all_types : Type (* (Top.2)+1 *) :=
    type_inc : forall X : Type (* Top.2 *), X -> union_of_all_types

So Coq got the universe level right.
-- 
Daniel