The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 23 Jun 2011 19:03:58 +0300,
Georgi Guninski 
<guninski AT guninski.com>
 a écrit :

> I am investigating fake proofs that look plausible to human forensics.
> 
> Why is it wrong to declare a proven theorem as an axiom? (this
> appears counter intuitive to me)
> 
> Theorem T : Prop.
> exact False.
> Defined.
> 
> Axiom A : T.
> 
> Lemma FUCKMS: False.
> pose proof A. compute in H. contradiction.
> Defined.
> 
> Coq < Print Assumptions FUCKMS.
> Axioms:
> A : T
> 
> If $T$ were False, how was it proven as a theorem?
> 
> Thank you.
> 

It is quite simple, it is just a question of the "level" of the object
you prove.

Theorem T: Prop.
 exact False.
Defined.

Just claims that "Prop" is inhabited, that is that there is a
proposition (namely False) which exists; you don't say that this
proposition is inhabited ("true") or not.
Like in natural languages, we can speak of "being false", it is usefull
to formulate statements, but you do not pretend to be able to prove
something "being false".

Axiom A : T.

Claims that there is something of type T.
Here T=False, so your axiom is the same as:

Axiom A : False.
So in natural language, you say that you know that something "being
false" is in fact provable.

In fact, you can see your axiom as:
Axiom A : (False : Prop).
where "False:Prop" is proved by "T".

I am not sure to have been clear in my explanation.

Maybe considering this other example:

Theorem T: Type.
 exact nat.
Defined.

Theorem A : T.
 exact 42.
Qed.

You can see that "T" and "A" are not on the same level.