The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

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 *)