Library Coq.Logic.Hurkens
Exploiting Hurkens's paradox
[Hurkens95] for system U- so as to
derive various contradictory contexts.
The file is divided into various sub-modules which all follow the
same structure: a section introduces the contradictory hypotheses
and a theorem named
paradox concludes the module with a proof of
False.
- The Generic module contains the actual Hurkens's paradox for a
postulated shallow encoding of system U- in Coq. This is an
adaptation by Arnaud Spiwack of a previous, more restricted
implementation by Herman Geuvers. It is used to derive every
other special cases of the paradox in this file.
- The NoRetractToImpredicativeUniverse module contains a simple
and effective formulation by Herman Geuvers [Geuvers01] of a
result by Thierry Coquand [Coquand90]. It states that no
impredicative sort can contain a type of which it is a
retract. This result implies that Coq with classical logic
stated in impredicative Set is inconsistent and that classical
logic stated in Prop implies proof-irrelevance (see
ClassicalFacts.v)
- The NoRetractFromSmallPropositionToProp module is a
specialisation of the NoRetractToImpredicativeUniverse module
to the case where the impredicative sort is Prop.
- The NoRetractToModalProposition module is a strengthening of
the NoRetractFromSmallPropositionToProp module. It shows that
given a monadic modality (aka closure operator) M, the type of
modal propositions (i.e. such that M A -> A) cannot be a
retract of a modal proposition. It is an example of use of the
paradox where the universes of system U- are not mapped to
universes of Coq.
- The NoRetractToNegativeProp module is the specialisation of
the NoRetractFromSmallPropositionToProp module where the
modality is double-negation. This result implies that the
principle of weak excluded middle (forall A, ~~A\/~A) implies
a weak variant of proof irrelevance.
- The NoRetractFromTypeToProp module proves that Prop cannot
be a retract of a larger type.
- The TypeNeqSmallType module proves that Type is different
from any smaller type.
- The PropNeqType module proves that Prop is different from
any larger Type. It is an instance of the previous result.
References:
- [Coquand90] T. Coquand, "Metamathematical Investigations of a
Calculus of Constructions", Proceedings of Logic in Computer
Science (LICS'90), 1990.
- [Hurkens95] A. J. Hurkens, "A simplification of Girard's paradox",
Proceedings of the 2nd international conference Typed Lambda-Calculi
and Applications (TLCA'95), 1995.
- [Geuvers01] H. Geuvers, "Inconsistency of Classical Logic in Type
Theory", 2001, revised 2007
(see external link http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz).
A modular proof of Hurkens's paradox.
It relies on an axiomatisation of a shallow embedding of system U-
(i.e. types of U- are interpreted by types of Coq). The
universes are encoded in a style, due to Martin-Löf, where they
are given by a set of names and a family
El:Name->Type which
interprets each name into a type. This allows the encoding of
universe to be decoupled from Coq's universes. Dependent products
and abstractions are similarly postulated rather than encoded as
Coq's dependent products and abstractions.
Axiomatisation of impredicative universes in a Martin-Löf style
System U- has two impredicative universes. In the proof of the
paradox they are slightly asymmetric (in particular the reduction
rules of the small universe are not needed). Therefore, the
axioms are duplicated allowing for a weaker requirement than the
actual system U-.
Large universe
Variable U1 :
Type.
Variable El1 :
U1 -> Type.
Variable Forall1 :
forall u:
U1,
(El1 u -> U1) -> U1.
Notation "'∀₁' x : A , B" := (
Forall1 A (
fun x =>
B)).
Notation "A '⟶₁' B" := (
Forall1 A (
fun _ =>
B)).
Variable lam1 :
forall u B,
(forall x:
El1 u,
El1 (
B x)
) -> El1 (
∀₁ x:u, B x).
Notation "'λ₁' x , u" := (
lam1 _ _ (
fun x =>
u)).
Variable app1 :
forall u B (
f:
El1 (
Forall1 u B)) (
x:
El1 u),
El1 (
B x).
Notation "f '·₁' x" := (
app1 _ _ f x).
Variable beta1 :
forall u B (
f:
forall x:
El1 u,
El1 (
B x))
x,
(λ₁ y, f y) ·₁ x = f x.
Closure by large products
U1 only needs to quantify over itself.
Variable ForallU1 :
(U1->U1) -> U1.
Notation "'∀₂' A , F" := (
ForallU1 (
fun A =>
F)).
Variable lamU1 :
forall F,
(forall A:
U1,
El1 (
F A)
) -> El1 (
∀₂ A, F A).
Notation "'λ₂' x , u" := (
lamU1 _ (
fun x =>
u)).
Variable appU1 :
forall F (
f:
El1(
∀₂ A,F A)) (
A:
U1),
El1 (
F A).
Notation "f '·₁' [ A ]" := (
appU1 _ f A).
Variable betaU1 :
forall F (
f:
forall A:
U1,
El1 (
F A))
A,
(λ₂ x, f x) ·₁ [ A ] = f A.
Small universe
The small universe is an element of the large one.
Closure by small product
U0 does not need reduction rules
Closure by large products
Automating the rewrite rules of our encoding.
Local Ltac simplify :=
(
repeat rewrite ?
beta1, ?
betaU1);
lazy beta.
Local Ltac simplify_in h :=
(
repeat rewrite ?
beta1, ?
betaU1 in h);
lazy beta in h.
Hurkens's paradox.
An inhabitant of
U0 standing for
False.
Definition V :
U1 :=
∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0.
Definition U :
U1 :=
V ⟶₁ u0.
Definition sb (
z:
El1 V) :
El1 V :=
λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a.
Definition le (
i:
El1 (
U⟶₁u0)) (
x:
El1 U) :
U0 :=
x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)).
Definition le' :
El1 (
(U⟶₁u0) ⟶₁ U ⟶₁ u0) :=
λ₁ i, λ₁ x, le i x.
Definition induct (
i:
El1 (
U⟶₁u0)) :
U0 :=
∀₀¹ x:U, le i x ⟶₀ i ·₁ x.
Definition WF :
El1 U :=
λ₁ z, (induct (
z·₁[U] ·₁ le')
).
Definition I (
x:
El1 U) :
U0 :=
(∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F
.
Lemma Omega :
El0 (
∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF).
Proof.
refine (
λ₀¹ i, λ₀ y, _).
refine (
y·₀[_]·₀_).
unfold le,
WF,
induct.
simplify.
refine (
λ₀¹ x, λ₀ h0, _).
simplify.
refine (
y·₀[_]·₀_).
unfold le.
simplify.
unfold sb at 1.
simplify.
unfold le' at 1.
simplify.
exact h0.
Qed.
Lemma lemma1 :
El0 (
induct (
λ₁ u, I u)).
Proof.
unfold induct.
refine (
λ₀¹ x, λ₀ p, _).
simplify.
refine (
λ₀ q,_).
assert (
El0 (
I (
λ₁ v, (sb v)·₁[U]·₁le'·₁x)))
as h.
{
generalize (
q·₀[λ₁ u, I u]·₀p).
simplify.
intros q'.
exact q'. }
refine (
h·₀_).
refine (
λ₀¹ i,_).
refine (
λ₀ h', _).
generalize (
q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]).
simplify.
intros q'.
refine (
q'·₀_).
clear q'.
unfold le at 1
in h'.
simplify_in h'.
unfold sb at 1
in h'.
simplify_in h'.
unfold le' at 1
in h'.
simplify_in h'.
exact h'.
Qed.
Lemma lemma2 :
El0 (
(∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F).
Proof.
refine (
λ₀ x, _).
assert (
El0 (
I WF))
as h.
{
generalize (
x·₀[λ₁ u, I u]·₀lemma1).
simplify.
intros q.
exact q. }
refine (
h·₀_).
clear h.
refine (
λ₀¹ i, λ₀ h0, _).
generalize (
x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]).
simplify.
intros q.
refine (
q·₀_).
clear q.
unfold le in h0.
simplify_in h0.
unfold WF in h0.
simplify_in h0.
exact h0.
Qed.
Theorem paradox :
El0 F.
Proof.
exact (
lemma2·₀Omega).
Qed.
End Paradox.
The paradox tactic can be called as a shortcut to use the paradox.
Ltac paradox h :=
unshelve (
refine ((
fun h =>
_) (
paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ))).
End Generic.
Impredicative universes are not retracts.
There can be no retract to an impredicative Coq universe from a
smaller type. In this version of the proof, the impredicativity of
the universe is postulated with a pair of functions from the
universe to its type and back which commute with dependent product
in an appropriate way.
u22u1_counit and u22u1_coherent only apply to dependent
product so that the equations happen in the smaller U1 rather
than U2. Indeed, it is not generally the case that one can
project from a large universe to an impredicative universe and
then get back the original type again. It would be too strong a
hypothesis to require (in particular, it is not true of
Prop). The formulation is reminiscent of the monadic
characteristic of the projection from a large type to Prop.
Theorem paradox :
forall F:
U1,
F.
Proof.
intros F.
Generic.paradox h.
Large universe
+
exact U1.
+
exact (
fun X =>
X).
+
cbn.
exact (
fun u F =>
forall x:
u,
F x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun F =>
u22u1 (
forall x,
F x)).
+
cbn.
exact (
fun _ x =>
u22u1_unit _ x).
+
cbn.
exact (
fun _ x =>
u22u1_counit _ x).
Small universe
The interpretation of the small universe is the image of
U0 in U1.
Modal fragments of Prop are not retracts
In presence of a a monadic modality on
Prop, we can define a
subset of
Prop of modal propositions which is also a complete
Heyting algebra. These cannot be a retract of a modal
proposition. This is a case where the universe in system U- are
not encoded as Coq universes.
The universe of modal propositions
Retract of the modal fragment of Prop in a small type
The retract is axiomatized using logical equivalence as the
equality on propositions.
Large universe
+
exact MProp.
+
exact El.
+
exact (
fun _ =>
Forall).
+
cbn.
exact (
fun _ _ f =>
f).
+
cbn.
exact (
fun _ _ f =>
f).
+
exact Forall.
+
cbn.
exact (
fun _ f =>
f).
+
cbn.
exact (
fun _ f =>
f).
Small universe
The negative fragment of Prop is not a retract
The existence in the pure Calculus of Constructions of a retract
from the negative fragment of
Prop into a negative proposition
is inconsistent. This is an instance of the previous result.
The universe of negative propositions.
Retract of the negative fragment of Prop in a small type
The retract is axiomatized using logical equivalence as the
equality on propositions.
Prop is not a retract
The existence in the pure Calculus of Constructions of a retract
from
Prop into a small type of
Prop is inconsistent. This is a
special case of the previous result.
The universe of propositions.
Retract of Prop in a small type, using the identity modality.
Retract of Prop in a small type
The retract is axiomatized using logical equivalence as the
equality on propositions.
Large universes are not retracts of Prop.
The existence in the Calculus of Constructions with universes of a
retract from some
Type universe into
Prop is inconsistent.
Assumption of a retract from Type into Prop
Theorem paradox :
forall P:
Prop,
P.
Proof.
intros P.
Generic.paradox h.
Large universe.
+
exact Type1.
+
exact (
fun X =>
X).
+
cbn.
exact (
fun u F =>
forall x,
F x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
+
exact (
fun F =>
forall A:
Prop,
F(
up A)).
+
cbn.
exact (
fun F f A =>
f (
up A)).
+
cbn.
intros F f A.
specialize (
f (
down A)).
rewrite up_down in f.
exact f.
+
exact Prop.
+
cbn.
exact (
fun X =>
X).
+
cbn.
exact (
fun A P =>
forall x:
A,
P x).
+
cbn.
exact (
fun A P =>
forall x:
A,
P x).
+
cbn.
exact P.
+
exact h.
+
cbn.
easy.
+
cbn.
intros F f A.
destruct (
up_down A).
cbn.
reflexivity.
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
Qed.
End Paradox.
End NoRetractFromTypeToProp.
A<>Type
No Coq universe can be equal to one of its elements.
Universe U is equal to one of its elements.
Let U :=
Type.
Variable A:
U.
Hypothesis h :
U=A.
Universe U is a retract of A
The following context is actually sufficient for the paradox to
hold. The hypothesis
h:U=A is only used to define
down,
up
and
up_down.
Large universe
+
exact U.
+
exact (
fun X=>
X).
+
cbn.
exact (
fun X F =>
forall x:
X,
F x).
+
cbn.
exact (
fun _ _ x =>
x).
+
cbn.
exact (
fun _ _ x =>
x).
+
exact (
fun F =>
forall x:
A,
F (
up x)).
+
cbn.
exact (
fun _ f =>
fun x:
A =>
f (
up x)).
+
cbn.
intros *
f X.
specialize (
f (
down X)).
rewrite up_down in f.
exact f.
Small universe
The interpretation of A as a universe is U.
+
cbn.
exact up.
+
cbn.
exact (
fun _ F =>
down (
forall x,
up (
F x))).
+
cbn.
exact (
fun _ F =>
down (
forall x,
up (
F x))).
+
cbn.
exact (
down False).
+
rewrite up_down in p.
exact p.
+
cbn.
easy.
+
cbn.
intros ?
f X.
destruct (
up_down X).
cbn.
reflexivity.
+
cbn.
intros ? ?
f.
rewrite up_down.
exact f.
+
cbn.
intros ? ?
f.
rewrite up_down in f.
exact f.
+
cbn.
intros ? ?
f.
rewrite up_down.
exact f.
+
cbn.
intros ? ?
f.
rewrite up_down in f.
exact f.
Qed.
End Paradox.
End TypeNeqSmallType.
Prop<>Type.
Special case of
TypeNeqSmallType.