The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Fri, 20 Jan 2012 22:25:01 +0800,
Jean-Francois Monin 
<jean-francois.monin AT imag.fr>
 a écrit :

> forall Q, (p a ->  Q) ->  (p b ->  Q) -> Q
> is the well-known impredicative encoding of p a \/ p b
> 
> Jean-Francois
> 
> On Fri, Jan 20, 2012 at 08:39:15AM -0500, Adam Chlipala wrote:
> > AUGER Cédric wrote:
> > >Consider the following "inductive".
> > >
> > >Inductive p : Prop ->  Prop :=
> > >| P0 : p True
> > >| P1 : forall a b, (p a \/ p b) ->  p (a\/b)
> > >| P2 : forall a b, (forall Q, ((p a) ->  Q) ->
> > >                               ((p b) ->  Q) ->
> > >                               Q) ->
> > >                    p (a\/b)
> > >.
> > >
> > >(It won't compile for positivity reasons)
> > >
> > >For me, either P1 and P2 should be both accepted, or they should be
> > >both refused, since P2 use the elimination principle of \/.
> > >
> > >In fact P1 is accepted, but not P2.
> > >
> > >I would be very surprised to learn that P2 is trully "unsound"
> > >whereas P1 is "sound". Is there some particular reasons not to be
> > >compatible with an elimination principle?
> > 
> >  [...]  I'm not
> > sure what is your basis for deciding that [P2] can't break
> > consistency, but it's far from obvious to me.  It's easy to see how
> > allowing non-strictly-positive occurrences can break consistency for
> > considerably simpler examples; I give such an example somewhere in
> > CPDT.

More precisely, imagine the Coq system allowing [P2]; and imagine it is
inconsistant, then you have a proof of False using "X:forall Q, ((p a)
-> Q) -> ((p b) -> Q) -> Q)". Now redo the proof without [P2] and when
you need [P2], use [P1] instead, and when you need "X:forall Q, …", you
will have "X:a∨b" instead, so by using "(fun Q (H1:p a -> Q) (H2:p b ->
Q) => or_ind Q H1 H2 X): forall Q, …" then you will be able to replay a
proof of False without using [P2]; so I am pretty sure [P2] cannot
break consistency.