The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, June 26, 2011 05:20:59 AM you wrote:
> Thank you.
> 
> I was asking what was wrong with taking as an axiom one of your statements.
> In both cases False is proven and excluded middle appears to guarantee one
> of the proofs to be genuine.
> 
> btw, setting the lemma as Definition and proving D and ~D doesn't work
> for me.

What's wrong with setting one of them as an axiom is that it doesn't generate 
the appropriate constraints on the level of Type in the statement.

Maybe it might help understanding to make a couple definitions:

Definition small_univ := Type.
Inductive union_of_all_small_types : small_univ :=
| small_type_inc : forall {X:small_univ},
  X -> union_of_all_small_types.

This should give a universe inconsistency error right away.

On the other hand, with:

Definition small_univ := Type.
Definition large_univ := Type.
Inductive union_of_all_small_types : large_univ :=
| small_type_inc: forall {X:small_univ},
  X -> union_of_all_small_types.

This should be fine, and just forces that small_univ is at a strictly lower 
level in the type hierarchy than large_univ.

Then the correct statements of uat_maximal_card and uat_not_maximal_card are:

Lemma uat_maximal_card: forall X:small_univ, exists f :
  X->union_of_all_small_types, injective f.
Lemma uat_not_maximal_card: ~ forall X:large_univ, exists f :
  X->union_of_all_small_types, injective f.

But if you declare the original statements as axioms, in uat_maximal_card, 
for 
all Coq knows, the Type occuring there might be large_univ.  Similarly, in 
not_uat_maximal_card, for all Coq knows, the Type occuring there might be 
small_univ.  So this would have the same effect as declaring

Axiom uat_maximal_card_ax: forall X:large_univ, exists f :
  X->union_of_all_small_types, injective f.

or

Axiom uat_not_maximal_card_ax: ~ forall X:small_univ, exists f :
  X->union_of_all_small_types, injective f.

If you set the statement as a definition, that forces there to be a single 
instance of Type, with the proofs of uat_maximal_card and 
uat_not_maximal_card 
generating incompatible constraints on the level of this Type compared to the 
level of the Type in the definition of union_of_all_types.  So you could 
prove 
either one of the statements D or ~D, but not both at the same time.  In 
trying to adapt this approach to the small_univ / large_univ case, you'd have 
to decide whether to put small_univ or large_univ into the definition.  
Depending on which you choose, you would be able to prove one or the other of 
D or ~D, but not both at the same time.

So one conclusion you can draw from the "paradox" is that small_univ <> 
large_univ.  Which would look strange on its own given the definitions of 
small_univ and large_univ, if you didn't know about the type hierarchy and 
that different instances of Type are distinct objects to Coq.
-- 
Daniel