The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Even if you are using classical Logic, you cannot prove False
from your scripts because you still have the Universe inconsistency
problem:

Require Import Classical.

Inductive union_of_all_types : Type :=
| type_inc: forall {X:Type}, X -> union_of_all_types.

Definition injective {X Y:Type} (f:X->Y) : Prop :=
 forall x1 x2:X, f x1 = f x2 -> x1 = x2.

Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.

pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.

Lemma contradiction : False.
Proof.
case (classic (forall (X:Type), exists f:X->union_of_all_types,
injective f)) ; intro H.

destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).

apply H.
intros.
exists (@type_inc X).
red; intros.
injection H0.
Require Import Eqdep.
apply inj_pair2.
Qed. (** Fail : Universe inconsistency **)

--
gallais



On 25 June 2011 15:21, Georgi Guninski 
<guninski AT guninski.com>
 wrote:
> On Sat, Jun 25, 2011 at 09:06:26AM -0400, Adam Chlipala wrote:
>> Georgi Guninski wrote:
>> >Is the Daniel Schepler's inconsistency real?
>>
>> No, his code does not demonstrate an inconsistency.
>>
>
> 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)
>
> (*file 1*)
> Inductive union_of_all_types : Type :=
> | type_inc: forall {X:Type}, X -> union_of_all_types.
>
> Definition injective {X Y:Type} (f:X->Y) : Prop :=
>  forall x1 x2:X, f x1 = f x2 -> x1 = x2.
>
> Axiom uat_maximal_card: forall (X:Type), exists f:X->union_of_all_types,
>  injective f.
> (*
> Proof.
> intros.
> exists (@type_inc X).
> red; intros.
> injection H.
> Require Import Eqdep.
> apply inj_pair2.
> Qed.
> *)
>
> Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
> Proof.
> intros.
> intro Hinj.
> pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
> pose (x0 := f S0).
> assert (~ S0 x0).
> intro.
> unfold S0 in H.
> destruct H as [S' []].
> unfold x0 in H0.
> apply Hinj in H0.
> rewrite H0 in H.
> unfold S0 in H.
> contradiction H.
> exists S0.
> split; trivial.
>
> pose proof H.
> unfold S0 in H0.
> contradiction H0.
> exists S0.
> split; trivial.
> Qed.
>
> Lemma uat_not_maximal_card:
>  ~ (forall (X:Type), exists f:X->union_of_all_types, injective f).
>
> Proof.
>
> intro.
> destruct (H (union_of_all_types -> Prop)) as [f].
> exact (not_power_inj _ _ H0).
> Qed.
>
>
> Print Assumptions uat_maximal_card.
> Print Assumptions uat_not_maximal_card.
>
> Lemma contradiction: False.
> Proof.
> exact (uat_not_maximal_card uat_maximal_card).
> Qed.  (* Done *)
>
> (*file 2*)
>
> Inductive union_of_all_types : Type :=
> | type_inc: forall {X:Type}, X -> union_of_all_types.
>
> Definition injective {X Y:Type} (f:X->Y) : Prop :=
>  forall x1 x2:X, f x1 = f x2 -> x1 = x2.
>
> Lemma uat_maximal_card: forall (X:Type), exists f:X->union_of_all_types,
>  injective f.
>
> Proof.
> intros.
> exists (@type_inc X).
> red; intros.
> injection H.
> Require Import Eqdep.
> apply inj_pair2.
> Qed.
>
>
> Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
> Proof.
> intros.
> intro Hinj.
> pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
> pose (x0 := f S0).
> assert (~ S0 x0).
> intro.
> unfold S0 in H.
> destruct H as [S' []].
> unfold x0 in H0.
> apply Hinj in H0.
> rewrite H0 in H.
> unfold S0 in H.
> contradiction H.
> exists S0.
> split; trivial.
>
> pose proof H.
> unfold S0 in H0.
> contradiction H0.
> exists S0.
> split; trivial.
> Qed.
>
> Axiom uat_not_maximal_card:
>  ~ (forall (X:Type), exists f:X->union_of_all_types, injective f).
>
> (*
> Proof.
>
> intro.
> destruct (H (union_of_all_types -> Prop)) as [f].
> exact (not_power_inj _ _ H0).
> Qed.
> *)
>
> Print Assumptions uat_maximal_card.
> Print Assumptions uat_not_maximal_card.
>
> Lemma contradiction: False.
> Proof.
> exact (uat_not_maximal_card uat_maximal_card).
> Qed.  (* Done *)
>