The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

British political comedy "Yes, Minister" featured the notorious  
exchange (for a specific P):

Official: There's a rumour that P.
Minister: Is it true?
Official: It's true that it's a rumour.

The assertion that P is proven to be a proposition is distinct from  
the assertion that P is a proposition which has been proven.

There remains the technical question of why it is ever necessary to  
conclude a proof of proposition P with Defined rather than the opaque  
Qed. (Why does it hurt to take a provable P as an axiom?) The trouble  
is that some propositions can be eliminated *strictly* over Set, in  
your actual programs. Strict eliminations get stuck if you feed them  
axioms, but compute if you feed them proofs which reduce to canonical  
form. Replacing proofs by axioms thus inhibits definitional equality  
and restricts typability.

With care, it is possible to restrict propositions to those which can  
be eliminated *lazily*, and thence acquire proof irrelevance in the  
definitional equality as well as erasability in extraction. By this  
criterion, accessibility is not propositional (but none the less  
erasable by travaux de Brady), observational equality is propositonal,  
and homotopic equality is neither propositional nor erasable.

Cheers

Conor



On 23 Jun 2011, at 17:30, "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org 
> wrote:

> Hi Georgi,
>
> Your [Theorem T : Prop] proves that [Prop] is inhabited while
> your [Axiom A : T] states that [T] is inhabited.
>
> These statements are not equivalent.
>
> Cheers,
>
> --
> guillaume
>
>
>
> On 23 June 2011 18:03, Georgi Guninski 
> <guninski AT guninski.com>
>  wrote:
> > 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