The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Georgi Guninski wrote:
> if you read the message you would realize i was asking about
> *modifications* of his code. here are two files - one takes T as axiom,
> the other takes ~T as axiom and in both cases False is proven (one of
> the proofs should be real unless i miss something)
>    

Neither proof is showing an inconsistency in Coq.  Rather, you've shown 
that [uat_maximal_card] is an inconsistent axiom even by itself, and 
[uat_not_maximal_card] is inconsistent with [eq_rect_eq].

The key thing to understand here is that, in Coq, proofs may change 
theorem statements, even the statements of past, already-proved 
theorems!  Every occurrence of [Type] is implicitly annotated with a 
universe variable.  Any part of a development that depends on such a 
variable may add constraints on it, in a very "imperative" way.  
Checking these constraints is crucial for consistency.

Daniel's proofs tweak universe variables in a way that makes your 
"axioms" weaker.  The untweaked versions are strong enough to be 
inconsistent, but the tweaked ones are fine.

The moral of the story is to try to avoid axioms whenever you can. ;)