The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

> Why is it wrong to declare a proven theorem as an axiom? (this appears 
> counter intuitive to me)

As said by the previous answers, if you want to "declare theorem T as
an axiom", you should basically copy the declaration of T and replace
"Theorem" by "Axiom":

Axiom T_ax:Prop.

Which is not useful since T is already proved. Your script declares an
axiom *of type* T, which is not the same. T:Prop does not imply
(neither in coq nor in any consistent type theory) that there exists a
closed term of type T. False is the typical counter-example.


*Replacing* T by T_ax may be useful (for efficiency if T is slow to
compile). It may seem unharmful however it may lead to inconsistencies
if you prove new theorems after that. Even if these theorems are not
about T itself. The reason is that the proof of T comes with universe
constraints which guarantee the consistency of the global proof
environment. Replacing T by T_ax would delete these constraints and
make coq accept proofs that would be inconsistent with the real proof
of T.

An interesting question is: since in this case the potential
inconsistency would not be a consequence of T but a consequence of the
absence of the universe constraints of T, does this provide a way to
build a proof H of False such that Print Assumptions H = \emptyset?
Maybe someone who knows how Print Assumptions works can tell? If yes
then this may be called a "fake proof that looks plausible to human
forensics". However there *is* an axiom somewhere in the environment
that should be detectable in some sense.

Replacing T by (T_ax + universe constraints of T) is an interesting
feature, I believe it is more or less what the -dont-load-proofs
option is made for.

Bests,
Pierre Courtieu


2011/6/23 Georgi Guninski 
<guninski AT guninski.com>:
> 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.
>
> --
> joro
>