[FOM] About Paradox Theory

[Andrej Bauer]

> Anyone care to comment on whether it's intuitionistically valid as it
> stands?

Obviously yes:

-----Coq 8.3------
Parameter A : Set.
Parameter F : A -> A -> Prop.
Lemma pratt: ~ exists y, forall x, F x y <-> ~ F x x.
Proof.
  firstorder.
Qed.

Print pratt.

pratt =
fun H : exists y : A, forall x : A, F x y <-> ~ F x x =>
ex_ind
  (fun (x : A) (H0 : forall x0 : A, F x0 x <-> ~ F x0 x0) =>
   and_ind
     (fun (H1 : F x x -> ~ F x x) (H2 : ~ F x x -> F x x) =>
      let H3 := let H3 := fun H3 : F x x => H1 H3 H3 in H2 H3 in H1 H3 H3)
     (H0 x)) H
     : ~ (exists y : A, forall x : A, F x y <-> ~ F x x)
---------

With kind regards,

Andrej