By popular demand, here it is in Coq, plainest and simplest,
indeed just *constructive FOPL* if I am not mistaken.

This was a nice exercise: it wasn't trivial (for me) to come
up with a formalization, so I'd encourage you to play with
the problem (in any formalism) before you look at my solution.

Spoiler.
..
..
..
..
..
..
..
..
..
..
..
..
..
..
..
..

The gist of it is that `forall w, phi h w <-> het w`
unfolds to `forall w, phi h w <-> ~ phi w w`, which,
in turn, by specializing with `w:=h`, becomes
`phi h h <-> ~ phi h h`.

```coq
(** Grelling–Nelson Paradox. *)

(* The "set" of words. *)
Parameter W : Type.

(* A word is "applicable" to a word. *)
Parameter phi : W -> W -> Prop.

(* Word [w] is "autological". *)
Definition aut (w : W) : Prop := phi w w.

(* Word [w] is "heterological". *)
Definition het (w : W) : Prop := not (aut w).

(* Exists word [h] to "represent" [het]. *)
Definition exists_h : Prop :=
exists (h : W),
forall (w : W), phi h w <-> het w.

(* [exists_h] is "inconsistent". *)
Theorem exists_h_to_false :
exists_h -> False.
Proof.
unfold exists_h, het, aut.
intros [h H].
destruct (H h) as [PN NP].
tauto.
Qed.
```

Julio

On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:

> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.

A comment:

By Curry-Howard, `exists h -> False` is synonym with `~ (exists h)`,
i.e. we actually have a (*constructive*) proof that, under the given
assumptions [*], there can be no such `h` in `W`.

(*) As far as I can see, the assumption essentially being that we
have a total binary relation `phi` (formalized as a propositional
function) that expresses "applicable" of words in `W`, and we
needn't even require that it be decidable.

Julio

On Friday, 25 August 2023 at 13:27:42 UTC+2, Julio Di Egidio wrote:

> a total binary relation `phi` (formalized as a
> propositional function)

....a binary relation `phi` (formalized as a
total propositional function)...

Julio

The axiom here, is not constructive:

> Definition exists_h : Prop :=
> exists (h : W),
> forall (w : W), phi h w <-> het w.

What would be the witness for h? I guess it violates
some of the "hallmarks" of constructive theories,
since it stipulates without proof an existence.

In mathematical logic, the disjunction and existence properties
are the "hallmarks" of constructive theories such as Heyting
arithmetic and constructive set theories
https://en.wikipedia.org/wiki/Disjunction_and_existence_properties

On the other hand, such rules as U Spec are usually
considered intuitionistically valid and I guess are
also part and parcel of constructive logic. So steps like

this here, are on the other hand not problematic:

> The gist of it is that `forall w, phi h w <-> het w`
> unfolds to `forall w, phi h w <-> ~ phi w w`, which,
> in turn, by specializing with `w:=h`, becomes
> `phi h h <-> ~ phi h h`.

BTW: In as far that exist_h is not constructive it has the
same problem as my proof here. The definiton Axiom is
problematic, the U Spec step is not problematic:

1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom

2 h(h)=1 <=> ~h(h)=1
U Spec, 1

The result is totally different if you try a more constructive
"het", like derive it from subset, instead of using a blant
definition, at least in DC Proof I get, not anymore a contradiction,

rather the conclusion that "het" cannot be in the domain of "het":

402 ~h @ dom
5 Conclusion, 389

See the other thread "AmateurGate".

Julio Di Egidio schrieb am Freitag, 25. August 2023 um 13:56:09 UTC+2:
> On Friday, 25 August 2023 at 13:27:42 UTC+2, Julio Di Egidio wrote:
>
> > a total binary relation `phi` (formalized as a
> > propositional function)
> ...a binary relation `phi` (formalized as a
> total propositional function)...
>
> Julio

If you read the Alonzo Church paper, and use its
decoupled version of "het", the paper also starts with
a nice explanation of what kind of non-constructivity

is involved. The paper starts with a short excursion
into "impredicativity". Basically there is some circularity
in defining "het", since the definition depends on what

is defined. Roughly speaking, a definition is impredicative
if it invokes (mentions or quantifies over) the set being
defined, or (more commonly) another set that

contains the thing being defined. I think its the second
case, i.e. only a reference to a totality that contains what
is is defined, which is then revealed through U Spec.

See also:
https://en.wikipedia.org/wiki/Impredicativity

Negative cycle impredicativity is hard to "resolve". You
can "resolve" positive cycle impredicativity, by for example
defaulting to some smallest solution or somesuch.

But negative cycle impredicativity, well I am still waiting
for the "resolution" announced by Dan Christensen. There
exist actually some "resolutions" in non-classical logics,

which avoid a contradiction. I am still waiting to see that here.

Mild Shock schrieb am Samstag, 26. August 2023 um 12:31:11 UTC+2:
> The axiom here, is not constructive:
> > Definition exists_h : Prop :=
> > exists (h : W),
> > forall (w : W), phi h w <-> het w.
> What would be the witness for h? I guess it violates
> some of the "hallmarks" of constructive theories,
> since it stipulates without proof an existence.
>
> In mathematical logic, the disjunction and existence properties
> are the "hallmarks" of constructive theories such as Heyting
> arithmetic and constructive set theories
> https://en.wikipedia.org/wiki/Disjunction_and_existence_properties
>
> On the other hand, such rules as U Spec are usually
> considered intuitionistically valid and I guess are
> also part and parcel of constructive logic. So steps like
>
> this here, are on the other hand not problematic:
> > The gist of it is that `forall w, phi h w <-> het w`
> > unfolds to `forall w, phi h w <-> ~ phi w w`, which,
> > in turn, by specializing with `w:=h`, becomes
> > `phi h h <-> ~ phi h h`.
> BTW: In as far that exist_h is not constructive it has the
> same problem as my proof here. The definiton Axiom is
> problematic, the U Spec step is not problematic:
>
> 1 ALL(v):[h(v)=1 <=> ~v(v)=1]
> Axiom
>
> 2 h(h)=1 <=> ~h(h)=1
> U Spec, 1
>
> The result is totally different if you try a more constructive
> "het", like derive it from subset, instead of using a blant
> definition, at least in DC Proof I get, not anymore a contradiction,
>
> rather the conclusion that "het" cannot be in the domain of "het":
>
> 402 ~h @ dom
> 5 Conclusion, 389
>
> See the other thread "AmateurGate".
> Julio Di Egidio schrieb am Freitag, 25. August 2023 um 13:56:09 UTC+2:
> > On Friday, 25 August 2023 at 13:27:42 UTC+2, Julio Di Egidio wrote:
> >
> > > a total binary relation `phi` (formalized as a
> > > propositional function)
> > ...a binary relation `phi` (formalized as a
> > total propositional function)...
> >
> > Julio

On Saturday, 26 August 2023 at 12:31:11 UTC+2, Mild Shock wrote:

> The axiom here, is not constructive:
> > Definition exists_h : Prop :=
> > exists (h : W),
> > forall (w : W), phi h w <-> het w.
> What would be the witness for h? I guess it violates

You keep guessing wrongly. That is not an axiom, it just
defines a proposition: and the theorem that follows proves
that proposition identically false.

But you still have no clue what "constructive" even means:
it would be non-constructive had I used LEM or equivalent,
or had I assumed inhabitance, which I didn't.

*Spammer Alert*

Julio

I am not guessing. Definitions are Axioms. In Coq:

"Definitions extend the global environment
by associating names to terms."
https://coq.inria.fr/refman/language/core/definitions.html

Everything that goes into global environment is an Axiom,
even if it doesn't start with Coq keyword "Axiom". Its the
same in any other logic, this here can be also called a Definition:

1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom

It also associates the name "h" with the term lambda v.(~v(v)=1).

Julio Di Egidio schrieb am Samstag, 26. August 2023 um 12:44:04 UTC+2:
> On Saturday, 26 August 2023 at 12:31:11 UTC+2, Mild Shock wrote:
>
> > The axiom here, is not constructive:
> > > Definition exists_h : Prop :=
> > > exists (h : W),
> > > forall (w : W), phi h w <-> het w.
> > What would be the witness for h? I guess it violates
> You keep guessing wrongly. That is not an axiom, it just
> defines a proposition: and the theorem that follows proves
> that proposition identically false.
>
> But you still have no clue what "constructive" even means:
> it would be non-constructive had I used LEM or equivalent,
> or had I assumed inhabitance, which I didn't.
>
> *Spammer Alert*
>
> Julio

Its much harder to make a "Definition & Axiom Free Proof" of
Grellings Antinomy. But this would assure that you
didn't use some Axioms, and that you have derived

the Antinomy from the logic of Coq only. You would
obtain a proof:

|- "Grellings Antinomy"

And not a proof:

"Global Context" |- "Grellings Antinomy"

Your proof has 3 definitions. Only 1 definition is problematic,
since it introduces a constant for a new existence. Can
you eliminate these definitions, and make a purely

logical proof? I hope this isn't the case, since it would
show Coq inconsistent.

BTW: But I guess you didn't wrote the proof by yourself,
since the Author who wrote the proof was careful enough
to not include the problematic Definition in his result, he proved:

> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.

So we can indeed eliminate exists_h from the "Global Context",
and what he proved was:

> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> (exists (h : W),
forall (w : W), phi h w <-> het w) -> False.

Mild Shock schrieb am Samstag, 26. August 2023 um 13:03:54 UTC+2:
> I am not guessing. Definitions are Axioms. In Coq:
>
> "Definitions extend the global environment
> by associating names to terms."
> https://coq.inria.fr/refman/language/core/definitions.html
>
> Everything that goes into global environment is an Axiom,
> even if it doesn't start with Coq keyword "Axiom". Its the
> same in any other logic, this here can be also called a Definition:
> 1 ALL(v):[h(v)=1 <=> ~v(v)=1]
> Axiom
> It also associates the name "h" with the term lambda v.(~v(v)=1).
> Julio Di Egidio schrieb am Samstag, 26. August 2023 um 12:44:04 UTC+2:
> > On Saturday, 26 August 2023 at 12:31:11 UTC+2, Mild Shock wrote:
> >
> > > The axiom here, is not constructive:
> > > > Definition exists_h : Prop :=
> > > > exists (h : W),
> > > > forall (w : W), phi h w <-> het w.
> > > What would be the witness for h? I guess it violates
> > You keep guessing wrongly. That is not an axiom, it just
> > defines a proposition: and the theorem that follows proves
> > that proposition identically false.
> >
> > But you still have no clue what "constructive" even means:
> > it would be non-constructive had I used LEM or equivalent,
> > or had I assumed inhabitance, which I didn't.
> >
> > *Spammer Alert*
> >
> > Julio

But your proof is closer to Alonzo Churchs decoupling
version, because you cannot ask for (het het), this wouldn't
be well type. So you need to indirectly find a "word" h with:

forall (w : W), phi h w <-> het w

Alonzo Churchs was mocking his own approach, and even
any approach that would use a domain "W" with the
intention of words, and thus appealing to a

mention and use distinction. He says this is irrelevant,
the domain "W" would not need to be words. Can be also
something else, and he makes use of this feature.

See also:

"A Comparison of Russell’s Resolution of the Semantical Antinomies
with that of Tarski" Alonzo Church - 1976
The Journal of Symbolic Logic, Volume 41 Issue 4
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/0E1F24F9F14EB30A01C164B536EDC5DE

Mild Shock schrieb am Samstag, 26. August 2023 um 13:11:46 UTC+2:
> Its much harder to make a "Definition & Axiom Free Proof" of
> Grellings Antinomy. But this would assure that you
> didn't use some Axioms, and that you have derived
>
> the Antinomy from the logic of Coq only. You would
> obtain a proof:
>
> |- "Grellings Antinomy"
>
> And not a proof:
>
> "Global Context" |- "Grellings Antinomy"
>
> Your proof has 3 definitions. Only 1 definition is problematic,
> since it introduces a constant for a new existence. Can
> you eliminate these definitions, and make a purely
>
> logical proof? I hope this isn't the case, since it would
> show Coq inconsistent.
>
> BTW: But I guess you didn't wrote the proof by yourself,
> since the Author who wrote the proof was careful enough
> to not include the problematic Definition in his result, he proved:
> > (* [exists_h] is "inconsistent". *)
> > Theorem exists_h_to_false :
> > exists_h -> False.
> So we can indeed eliminate exists_h from the "Global Context",
> and what he proved was:
> > (* [exists_h] is "inconsistent". *)
> > Theorem exists_h_to_false :
> > (exists (h : W),
> forall (w : W), phi h w <-> het w) -> False.
> Mild Shock schrieb am Samstag, 26. August 2023 um 13:03:54 UTC+2:
> > I am not guessing. Definitions are Axioms. In Coq:
> >
> > "Definitions extend the global environment
> > by associating names to terms."
> > https://coq.inria.fr/refman/language/core/definitions.html
> >
> > Everything that goes into global environment is an Axiom,
> > even if it doesn't start with Coq keyword "Axiom". Its the
> > same in any other logic, this here can be also called a Definition:
> > 1 ALL(v):[h(v)=1 <=> ~v(v)=1]
> > Axiom
> > It also associates the name "h" with the term lambda v.(~v(v)=1).
> > Julio Di Egidio schrieb am Samstag, 26. August 2023 um 12:44:04 UTC+2:
> > > On Saturday, 26 August 2023 at 12:31:11 UTC+2, Mild Shock wrote:
> > >
> > > > The axiom here, is not constructive:
> > > > > Definition exists_h : Prop :=
> > > > > exists (h : W),
> > > > > forall (w : W), phi h w <-> het w.
> > > > What would be the witness for h? I guess it violates
> > > You keep guessing wrongly. That is not an axiom, it just
> > > defines a proposition: and the theorem that follows proves
> > > that proposition identically false.
> > >
> > > But you still have no clue what "constructive" even means:
> > > it would be non-constructive had I used LEM or equivalent,
> > > or had I assumed inhabitance, which I didn't.
> > >
> > > *Spammer Alert*
> > >
> > > Julio

Hey Culio, I guess you need a little Crank Spank. Can you
explain how your proof is constructive? You use "tauto".
And what about Unicode, can you not use Greek Letters in Coq.

Also a pitty that DC Proof cannot do Unicode. I cannot use the Greek φ ?
How annoying. Anyway here is the DC Proof proof. The proof
is a little shorter, I think my gentzen/1 proof search generates

some longer detours because of the way it deals with negation,
since it doesn't directly search shortest natural deduction proof,
but rather works its way through search a Gentzen style proof,

but then manually doing the proof, gives something much shorter.
But can we get rid of the two Rem DNeg, to make it constructive?
Or at least can we get rid of the inner Rem DNeg?

15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14

------------------------------------ begin proof ------------------------------------------

1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise

2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1

3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2

4 ~Phi(u,u) => Phi(u,u)
Split, 3

5 Phi(u,u) => ~Phi(u,u)
Split, 3

6 ~Phi(u,u)
Premise

7 Phi(u,u)
Detach, 4, 6

8 ~Phi(u,u) & Phi(u,u)
Join, 6, 7

9 ~~Phi(u,u)
4 Conclusion, 6

10 Phi(u,u)
Rem DNeg, 9

11 ~Phi(u,u)
Detach, 5, 10

12 Phi(u,u) & ~Phi(u,u)
Join, 10, 11

13 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

14 ~~ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Quant, 13

15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14

------------------------------------ end proof ------------------------------------------

Julio Di Egidio schrieb am Freitag, 25. August 2023 um 12:29:55 UTC+2:
> By popular demand, here it is in Coq, plainest and simplest,
> indeed just *constructive FOPL* if I am not mistaken.
>
> This was a nice exercise: it wasn't trivial (for me) to come
> up with a formalization, so I'd encourage you to play with
> the problem (in any formalism) before you look at my solution.
>
> Spoiler.
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
> .
>
> The gist of it is that `forall w, phi h w <-> het w`
> unfolds to `forall w, phi h w <-> ~ phi w w`, which,
> in turn, by specializing with `w:=h`, becomes
> `phi h h <-> ~ phi h h`.
>
> ```coq
> (** Grelling–Nelson Paradox. *)
>
> (* The "set" of words. *)
> Parameter W : Type.
>
> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.
>
> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.
>
> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).
>
> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W),
> forall (w : W), phi h w <-> het w.
>
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.
> Proof.
> unfold exists_h, het, aut.
> intros [h H].
> destruct (H h) as [PN NP].
> tauto.
> Qed.
> ```
>
> Julio

On 27/08/2023 13:53, Mild Shock wrote:

> explain how your proof is constructive? You use "tauto".

<< `tauto` succeeds on any instance of an *intuitionistic
tautological proposition*. >> (my emphasis, on RTFM.)
<https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html?highlight=tauto#coq:tacn.tauto>

That said, here is the simplest explicit (still constructive)
proof of a `forall P, ~ (P <-> ~ P)` that I have been able
to concoct (I wouldn't be surprised if it can be simplified
further) (note: here I use an axiom instead of a theorem
assumption, but this is no substantial difference):

```coq
Module ex_falso''.

Parameter P : Prop. (* i.e. [forall P] *)

Axiom P_iff_not_P : P <-> ~ P.

Lemma ex_falso_quodlibet :
False.
Proof.
assert (H : P <-> ~ P)
by apply P_iff_not_P.
destruct H as [HPN HNP].
assert (HP : P).
{
apply HNP.
intros HP.
apply (HPN HP HP).
}
apply (HPN HP HP).
Qed.

End ex_falso''.
```

HTH,

Julio

Ok "tauto" is not that bad, it doesn't refer to classical tautology
but to tautology in the constructive logic of Coq. Here is
a little test that shows, that it doesn't cover classical logic:

Coq < Theorem couterexample: forall (P Q : Prop), ~ (P -> Q) -> P /\ ~ Q.
1 goal
============================
forall P Q : Prop, ~ (P -> Q) -> P /\ ~ Q
couterexample < tauto.
Toplevel input, characters 0-5:
> tauto.
> ^^^^^
Error: Tactic failure: tauto failed.

couterexample <

Ok here is a different proof of Grellings Paradox in DC
Proof which doesn't use Rem DNeg, even not once. Instead
starting with the Premise ~Phi(u,u) inside the proof, I do now

start with the Premise Phi(u,u). Also I formulate the result with
~EXIST(u) instead of ALL(u)~, assuming that the exist inference
rule from DC Proof is already constructive?

12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

----------------------------- begin proof ----------------------------------------

1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise

2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1

3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2

4 ~Phi(u,u) => Phi(u,u)
Split, 3

5 Phi(u,u) => ~Phi(u,u)
Split, 3

9 ~Phi(u,u)
5 Conclusion, 6

10 Phi(u,u)
Detach, 4, 9

11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10

12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

----------------------------- end proof ----------------------------------------

Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 16:58:27 UTC+2:
> On 27/08/2023 13:53, Mild Shock wrote:
>
> > explain how your proof is constructive? You use "tauto".
> << `tauto` succeeds on any instance of an *intuitionistic
> tautological proposition*. >> (my emphasis, on RTFM.)
> <https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html?highlight=tauto#coq:tacn.tauto>
>
> That said, here is the simplest explicit (still constructive)
> proof of a `forall P, ~ (P <-> ~ P)` that I have been able
> to concoct (I wouldn't be surprised if it can be simplified
> further) (note: here I use an axiom instead of a theorem
> assumption, but this is no substantial difference):
>
> ```coq
> Module ex_falso''.
>
> Parameter P : Prop. (* i.e. [forall P] *)
>
> Axiom P_iff_not_P : P <-> ~ P.
>
> Lemma ex_falso_quodlibet :
> False.
> Proof.
> assert (H : P <-> ~ P)
> by apply P_iff_not_P.
> destruct H as [HPN HNP].
> assert (HP : P).
> {
> apply HNP.
> intros HP.
> apply (HPN HP HP).
> }
> apply (HPN HP HP).
> Qed.
>
> End ex_falso''.
> ```
>
> HTH,
>
> Julio

Sorry, I didn't expand the proof completely:

12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

---------------- begin proof, now completely expanded ----------------------------

1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise

2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1

3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2

4 ~Phi(u,u) => Phi(u,u)
Split, 3

5 Phi(u,u) => ~Phi(u,u)
Split, 3

6 Phi(u,u)
Premise

7 ~Phi(u,u)
Detach, 5, 6

8 Phi(u,u) & ~Phi(u,u)
Join, 6, 7

9 ~Phi(u,u)
4 Conclusion, 6

10 Phi(u,u)
Detach, 4, 9

11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10

12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

---------------- end proof, now completely expanded -----------------------

Mild Shock schrieb am Sonntag, 27. August 2023 um 17:00:04 UTC+2:
> Ok "tauto" is not that bad, it doesn't refer to classical tautology
> but to tautology in the constructive logic of Coq. Here is
> a little test that shows, that it doesn't cover classical logic:
>
> Coq < Theorem couterexample: forall (P Q : Prop), ~ (P -> Q) -> P /\ ~ Q.
> 1 goal
> ============================
> forall P Q : Prop, ~ (P -> Q) -> P /\ ~ Q
> couterexample < tauto.
> Toplevel input, characters 0-5:
> > tauto.
> > ^^^^^
> Error: Tactic failure: tauto failed.
>
> couterexample <
>
> Ok here is a different proof of Grellings Paradox in DC
> Proof which doesn't use Rem DNeg, even not once. Instead
> starting with the Premise ~Phi(u,u) inside the proof, I do now
>
> start with the Premise Phi(u,u). Also I formulate the result with
> ~EXIST(u) instead of ALL(u)~, assuming that the exist inference
> rule from DC Proof is already constructive?
>
> 12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
> 4 Conclusion, 1
>
> ----------------------------- begin proof ----------------------------------------
> 1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
> Premise
>
> 2 ~Phi(u,u) <=> Phi(u,u)
> U Spec, 1
>
> 3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
> Iff-And, 2
>
> 4 ~Phi(u,u) => Phi(u,u)
> Split, 3
>
> 5 Phi(u,u) => ~Phi(u,u)
> Split, 3
> 9 ~Phi(u,u)
> 5 Conclusion, 6
>
> 10 Phi(u,u)
> Detach, 4, 9
>
> 11 ~Phi(u,u) & Phi(u,u)
> Join, 9, 10
>
> 12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
> 4 Conclusion, 1
>
> ----------------------------- end proof ----------------------------------------
> Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 16:58:27 UTC+2:
> > On 27/08/2023 13:53, Mild Shock wrote:
> >
> > > explain how your proof is constructive? You use "tauto".
> > << `tauto` succeeds on any instance of an *intuitionistic
> > tautological proposition*. >> (my emphasis, on RTFM.)
> > <https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html?highlight=tauto#coq:tacn.tauto>
> >
> > That said, here is the simplest explicit (still constructive)
> > proof of a `forall P, ~ (P <-> ~ P)` that I have been able
> > to concoct (I wouldn't be surprised if it can be simplified
> > further) (note: here I use an axiom instead of a theorem
> > assumption, but this is no substantial difference):
> >
> > ```coq
> > Module ex_falso''.
> >
> > Parameter P : Prop. (* i.e. [forall P] *)
> >
> > Axiom P_iff_not_P : P <-> ~ P.
> >
> > Lemma ex_falso_quodlibet :
> > False.
> > Proof.
> > assert (H : P <-> ~ P)
> > by apply P_iff_not_P.
> > destruct H as [HPN HNP].
> > assert (HP : P).
> > {
> > apply HNP.
> > intros HP.
> > apply (HPN HP HP).
> > }
> > apply (HPN HP HP).
> > Qed.
> >
> > End ex_falso''.
> > ```
> >
> > HTH,
> >
> > Julio

On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
<snip>
> (** Grelling–Nelson Paradox. *)

These all have the form "I am not provable"
(in particular, as opposed to "I am not true"):

- The Grelling–Nelson Paradox
- The Barber Paradox (see below)
- The Diagonal Argument (see below)
- Goedel's Incompleteness Theorem (not yet)

In fact, I still have to try GIT, which looks more
complicated than the straight translations below,
although the form should be the same: GIT is a
"complicated" diagonal argument...

I also have to try and see what happens if we extend
the initial set with the "non-standard" element: is it
necessarily turtles all the way up, or can we close the
system?

To be continued...

===============================The Barber Paradox
===============================
> (* The "set" of words. *)
> Parameter W : Type.

The "set" of men.

> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.

A man "shaves" a man?

> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.

Man [w] shaves himself?

> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).

Man [w] does NOT shave himself?

> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.

Exists man [h] s.t. [h] shaves [w]
iff [w] does NOT shave himself?

> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false : exists_h -> False.

Exists such man [h] is false! QED.
===============================
===============================The Diagonal Argument
===============================
> (* The "set" of words. *)
> Parameter W : Type.

The "set" of natural numbers.

> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.

A "total" list of binary strings
(in Prop instead of bool covers also
the undecidable ones...)
Equivalently, a function of (i,j) that
returns the j-th digit of the i-th string.

> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.

The [w]-th diagonal digit of the list is True (i.e. 1)?

> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).

The [w]-th diagonal digit is NOT True (i.e. 0)?

> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.

Exists natural number [h] s.t. the [w]-th digit
of the [h]-th string is True iff the [w]-th diagonal
digit is NOT True?

> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false : exists_h -> False.

Exists such natural number [h] is false! QED.

(Namely: the "diagonal" here is represented by the
function [aut], the "antidiagonal" is represented by
[het], and, as expected, we have proven that there
is NO natural number [h] such that the antidiagonal
is at place [h] in any list [phi].)
===============================
Julio

Very Good! Congratulations! Now I am waiting for a
further Coq formalization. To learn something about
Russells Type levels. Alonzo Church managed a

completely different result, using Russells Type levels.
Namely he had a form of Grelling Paradox, which
said exist_h is "ok" and (het h) is sometimes had

"yes" and sometimes "no". How was this possible, is
this even correct? Can you model that in Coq?
Try sci-hub.se to get this paper, just use the DOI:

Comparison of Russell's Resolution of the Semantical
Antinomies with that of Tarski - Alonzo Church
The Journal of Symbolic Logic
Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
https://doi.org/10.2307/2272393

Julio Di Egidio schrieb am Montag, 28. August 2023 um 11:11:47 UTC+2:
> On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
> <snip>
> > (** Grelling–Nelson Paradox. *)
> These all have the form "I am not provable"
> (in particular, as opposed to "I am not true"):
>
> - The Grelling–Nelson Paradox
> - The Barber Paradox (see below)
> - The Diagonal Argument (see below)
> - Goedel's Incompleteness Theorem (not yet)
>
> In fact, I still have to try GIT, which looks more
> complicated than the straight translations below,
> although the form should be the same: GIT is a
> "complicated" diagonal argument...
>
> I also have to try and see what happens if we extend
> the initial set with the "non-standard" element: is it
> necessarily turtles all the way up, or can we close the
> system?
>
> To be continued...
>
> ================================
> The Barber Paradox
> ===============================> > (* The "set" of words. *)
> > Parameter W : Type.
> The "set" of men.
> > (* A word is "applicable" to a word. *)
> > Parameter phi : W -> W -> Prop.
> A man "shaves" a man?
> > (* Word [w] is "autological". *)
> > Definition aut (w : W) : Prop := phi w w.
> Man [w] shaves himself?
> > (* Word [w] is "heterological". *)
> > Definition het (w : W) : Prop := not (aut w).
> Man [w] does NOT shave himself?
> > (* Exists word [h] to "represent" [het]. *)
> > Definition exists_h : Prop :=
> > exists (h : W), forall (w : W), phi h w <-> het w.
> Exists man [h] s.t. [h] shaves [w]
> iff [w] does NOT shave himself?
> > (* [exists_h] is "inconsistent". *)
> > Theorem exists_h_to_false : exists_h -> False.
> Exists such man [h] is false! QED.
> ================================
>
> ================================
> The Diagonal Argument
> ===============================> > (* The "set" of words. *)
> > Parameter W : Type.
> The "set" of natural numbers.
> > (* A word is "applicable" to a word. *)
> > Parameter phi : W -> W -> Prop.
> A "total" list of binary strings
> (in Prop instead of bool covers also
> the undecidable ones...)
> Equivalently, a function of (i,j) that
> returns the j-th digit of the i-th string.
> > (* Word [w] is "autological". *)
> > Definition aut (w : W) : Prop := phi w w.
> The [w]-th diagonal digit of the list is True (i.e. 1)?
> > (* Word [w] is "heterological". *)
> > Definition het (w : W) : Prop := not (aut w).
> The [w]-th diagonal digit is NOT True (i.e. 0)?
> > (* Exists word [h] to "represent" [het]. *)
> > Definition exists_h : Prop :=
> > exists (h : W), forall (w : W), phi h w <-> het w.
> Exists natural number [h] s.t. the [w]-th digit
> of the [h]-th string is True iff the [w]-th diagonal
> digit is NOT True?
> > (* [exists_h] is "inconsistent". *)
> > Theorem exists_h_to_false : exists_h -> False.
> Exists such natural number [h] is false! QED.
>
> (Namely: the "diagonal" here is represented by the
> function [aut], the "antidiagonal" is represented by
> [het], and, as expected, we have proven that there
> is NO natural number [h] such that the antidiagonal
> is at place [h] in any list [phi].)
> ================================
>
> Julio

A way to get "exist_h" ok, is to add a type
where h comes form, and some comprehension
axiom, and formulate "exist h" slightly different.

Like here, where comprehension is done over
the type "rel":

13 EXIST(gra):[Set'(gra) & ALL(x):ALL(y):[(x,y) @ gra <=>
(x,y) @ rel & [EXIST(fun):[Function(fun,dom,cod) &
ALL(a):[a @ dom => x(a)=fun(a)] & ~[x @ dom & fun(x)=1]] <=> y=1]]]
Subset, 11

The result was not "exist_h" is identically false, but
the "rel" I used led me to a h, which had "~h e dom". But
having "exist_h" ok is rather on the line of "resolving" the

paradox, than just state it "unresolved" as "exist_h"
identically false. And Alonzo Church was showing this
resolution used in the Principia and then compared it to

some discussion by Tarski. Concerning the Principia,
Alonzo Church mentions even two resolutions, two
printed versions of resolutions, see footnote 1:

"Russell's earlier version of the ramified type hierarchy is
in [6] and in the Introduction to the first edition of (Principia)
[12]. The later version is in *12 and in (Russell's) Introduction
to the second edition (Principia) of [12]."
https://doi.org/10.2307/2272393

Mild Shock schrieb am Montag, 28. August 2023 um 14:51:38 UTC+2:
> Very Good! Congratulations! Now I am waiting for a
> further Coq formalization. To learn something about
> Russells Type levels. Alonzo Church managed a
>
> completely different result, using Russells Type levels.
> Namely he had a form of Grelling Paradox, which
> said exist_h is "ok" and (het h) is sometimes had
>
> "yes" and sometimes "no". How was this possible, is
> this even correct? Can you model that in Coq?
> Try sci-hub.se to get this paper, just use the DOI:
> Comparison of Russell's Resolution of the Semantical
> Antinomies with that of Tarski - Alonzo Church
> The Journal of Symbolic Logic
> Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
> https://doi.org/10.2307/2272393
> Julio Di Egidio schrieb am Montag, 28. August 2023 um 11:11:47 UTC+2:
> > On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
> > <snip>
> > > (** Grelling–Nelson Paradox. *)
> > These all have the form "I am not provable"
> > (in particular, as opposed to "I am not true"):
> >
> > - The Grelling–Nelson Paradox
> > - The Barber Paradox (see below)
> > - The Diagonal Argument (see below)
> > - Goedel's Incompleteness Theorem (not yet)
> >
> > In fact, I still have to try GIT, which looks more
> > complicated than the straight translations below,
> > although the form should be the same: GIT is a
> > "complicated" diagonal argument...
> >
> > I also have to try and see what happens if we extend
> > the initial set with the "non-standard" element: is it
> > necessarily turtles all the way up, or can we close the
> > system?
> >
> > To be continued...
> >
> > ================================
> > The Barber Paradox
> > ================================
> > > (* The "set" of words. *)
> > > Parameter W : Type.
> > The "set" of men.
> > > (* A word is "applicable" to a word. *)
> > > Parameter phi : W -> W -> Prop.
> > A man "shaves" a man?
> > > (* Word [w] is "autological". *)
> > > Definition aut (w : W) : Prop := phi w w.
> > Man [w] shaves himself?
> > > (* Word [w] is "heterological". *)
> > > Definition het (w : W) : Prop := not (aut w).
> > Man [w] does NOT shave himself?
> > > (* Exists word [h] to "represent" [het]. *)
> > > Definition exists_h : Prop :=
> > > exists (h : W), forall (w : W), phi h w <-> het w.
> > Exists man [h] s.t. [h] shaves [w]
> > iff [w] does NOT shave himself?
> > > (* [exists_h] is "inconsistent". *)
> > > Theorem exists_h_to_false : exists_h -> False.
> > Exists such man [h] is false! QED.
> > ================================
> >
> > ================================
> > The Diagonal Argument
> > ================================
> > > (* The "set" of words. *)
> > > Parameter W : Type.
> > The "set" of natural numbers.
> > > (* A word is "applicable" to a word. *)
> > > Parameter phi : W -> W -> Prop.
> > A "total" list of binary strings
> > (in Prop instead of bool covers also
> > the undecidable ones...)
> > Equivalently, a function of (i,j) that
> > returns the j-th digit of the i-th string.
> > > (* Word [w] is "autological". *)
> > > Definition aut (w : W) : Prop := phi w w.
> > The [w]-th diagonal digit of the list is True (i.e. 1)?
> > > (* Word [w] is "heterological". *)
> > > Definition het (w : W) : Prop := not (aut w).
> > The [w]-th diagonal digit is NOT True (i.e. 0)?
> > > (* Exists word [h] to "represent" [het]. *)
> > > Definition exists_h : Prop :=
> > > exists (h : W), forall (w : W), phi h w <-> het w.
> > Exists natural number [h] s.t. the [w]-th digit
> > of the [h]-th string is True iff the [w]-th diagonal
> > digit is NOT True?
> > > (* [exists_h] is "inconsistent". *)
> > > Theorem exists_h_to_false : exists_h -> False.
> > Exists such natural number [h] is false! QED.
> >
> > (Namely: the "diagonal" here is represented by the
> > function [aut], the "antidiagonal" is represented by
> > [het], and, as expected, we have proven that there
> > is NO natural number [h] such that the antidiagonal
> > is at place [h] in any list [phi].)
> > ================================
> >
> > Julio

On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:

> But having "exist_h" ok is rather on the line of "resolving"
> the paradox, than just state it "unresolved" as "exist_h"
> identically false.

The "paradox" *is* resolved, `~ exists h` as in "there can
be no such barber (on that island)" is a definite answer.

> And Alonzo Church was showing this
> resolution used in the Principia and then compared it to
> some discussion by Tarski. Concerning the Principia,
> Alonzo Church mentions even two resolutions, two
> printed versions of resolutions, see footnote 1:

Which is the opposite of a resolution, it's the turtles all
the way up, and provably so, courtesy Burali-Forti. I was
proposing we rather try closing the system, adding one
and only one non-standard element: but I am still playing
with it...

Julio

Thats not what started the discussion. The paper
I was citing to start a discussion was this here,
because it shows what traditionally "resolve" means,

Comparison of Russell's Resolution of the Semantical
Antinomies with that of Tarski - Alonzo Church
The Journal of Symbolic Logic
Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
https://doi.org/10.2307/2272393

to clarify whether for example Dan Christense
"resolves" anything. There is nothing about non-standard
elements in Alonzo Churchs paper. Then I figured

out that the paper discusses Grellings Paradox and
its resolution. Then you hitch hicked the topic and
claimed Grellings Paradox in Coq. Now please finish

the business and show a resolution as Alonzo Church does.

Julio Di Egidio schrieb am Montag, 28. August 2023 um 19:48:09 UTC+2:
> On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:
>
> > But having "exist_h" ok is rather on the line of "resolving"
> > the paradox, than just state it "unresolved" as "exist_h"
> > identically false.
> The "paradox" *is* resolved, `~ exists h` as in "there can
> be no such barber (on that island)" is a definite answer.
> > And Alonzo Church was showing this
> > resolution used in the Principia and then compared it to
> > some discussion by Tarski. Concerning the Principia,
> > Alonzo Church mentions even two resolutions, two
> > printed versions of resolutions, see footnote 1:
> Which is the opposite of a resolution, it's the turtles all
> the way up, and provably so, courtesy Burali-Forti. I was
> proposing we rather try closing the system, adding one
> and only one non-standard element: but I am still playing
> with it...
>
> Julio

On Monday, 28 August 2023 at 11:11:47 UTC+2, Julio Di Egidio wrote:
> On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
> <snip>
> > (** Grelling–Nelson Paradox. *)
> These all have the form "I am not provable"
> (in particular, as opposed to "I am not true"):
>
> - The Grelling–Nelson Paradox
> - The Barber Paradox (see below)
> - The Diagonal Argument (see below)
> - Goedel's Incompleteness Theorem (not yet)

But I have said that upside down: it's "I am not true"
that is self-contradictory, while "I am not provable"
is necessarily true (under the given assumptions
and semantics).

Should add Russell Paradox to that list, and check
why with Epimenides Paradox I got a somewhat
different result...

> GIT is a "complicated" diagonal argument...

So maybe not, not that simple...

Julio

On Monday, 28 August 2023 at 19:48:09 UTC+2, Julio Di Egidio wrote:
> On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:
>
> > But having "exist_h" ok is rather on the line of "resolving"
> > the paradox, than just state it "unresolved" as "exist_h"
> > identically false.
>
> The "paradox" *is* resolved, `~ exists h` as in "there can
> be no such barber (on that island)" is a definite answer.

But I must concede this "resolution" falls somewhat short: while
it is reasonable that << there is no such barber on that island >>,
it does sound unsatisfactory if not ridiculous that << in the realm
of denotation, no word denotes... "heterological" >>...

Julio

On Tuesday, 29 August 2023 at 15:29:25 UTC+2, Julio Di Egidio wrote:
> On Monday, 28 August 2023 at 11:11:47 UTC+2, Julio Di Egidio wrote:
> > On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
> > <snip>
> > > (** Grelling–Nelson Paradox. *)
> > These all have the form "I am not provable"
> > (in particular, as opposed to "I am not true"):
> >
> > - The Grelling–Nelson Paradox
> > - The Barber Paradox (see below)
> > - The Diagonal Argument (see below)
> > - Goedel's Incompleteness Theorem (not yet)
>
> But I have said that upside down: it's "I am not true"
> that is self-contradictory, while "I am not provable"
> is necessarily true (under the given assumptions
> and semantics).
>
> Should add Russell Paradox to that list, and check
> why with Epimenides Paradox I got a somewhat
> different result...
>
> > GIT is a "complicated" diagonal argument...
>
> So maybe not, not that simple...

Maybe I should not even add Russell's to that list...

I am still unclear about the Liar proper, namely as
opposed to Grelling's and co.: SEP insists (*) that
<< The first ingredient in building a Liar is a truth
predicate >>, while our `phi` can be anything... but,
in fact, I (still?) cannot find a way to apply our (truly
basic) scheme to "I am not true": what `W` and
`phi` be in this case?

OTOH "I am not true" indeed is not as simple (basic)
as "I do not tell the truth": so maybe Russell does go
with Epimenides...

(*) <https://plato.stanford.edu/entries/liar-paradox/#TrutPred>

Julio

On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:

> OTOH "I am not true" indeed is not as simple (basic)
> as "I do not tell the truth"

Sorry, of course I meant the other way around...

Julio

On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:

[Corrected:]
> OTOH "I do not tell the truth" indeed is not as simple (basic)
> as "I am not true": so maybe Russell does go with Epimenides...

Here is (my) Epimenides' for comparison:
<https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ>
with the caution that it is not finished, i.e. it's neither polished
nor, more importantly, I have tried all conclusions I could draw.

Julio

The Epimenides Paradox is not an Antinomy like the Liar Paradox.
If we take the Liar Paradox to be Q <=> ~Q, we see that this here
is also a Liar Paradox, when we replace Q by ALL(x):P(x):

ALL(x):P(x) <=> ~ALL(x):P(x)

Wolfgang Scharz tree tool indeed confirms that it is an Antinomy,
in that it can be Refuted, i.e. Disproved by producing a proof
of its negation. The proof tells me the truth table has "F" everywhere:

¬(∀xPx ↔ ¬∀xPx) is valid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~6xPx)

Now how do we get the Epimenides Paradox? You only need to
tweak the above formula a little bit, and you get not anymore
an Antinomy. Negation is not provable so the truth table has somewhere "T":

¬(∀xPx ↔ ¬∃xPx) is invalid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~7xPx)

But the above formula has another advantage, you can use
it to prove the contrary of what it has inside:

(∀xPx ↔ ¬∃xPx) → ∃xPx is valid..
https://www.umsu.de/trees/#(~6xPx~4~3~7xPx)~5~7xPx

This is similar to the True(x) that appears inside the Epimenides
proof in DC Proof, that then leads to ~True(x). Actually I think
the Epimenides proof can be reduced to the above, I found

it my some manipulations of the Epimendides proof.

Julio Di Egidio schrieb am Donnerstag, 31. August 2023 um 20:05:42 UTC+2:
> On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:
>
> [Corrected:]
> > OTOH "I do not tell the truth" indeed is not as simple (basic)
> > as "I am not true": so maybe Russell does go with Epimenides...
>
> Here is (my) Epimenides' for comparison:
> <https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ>
> with the caution that it is not finished, i.e. it's neither polished
> nor, more importantly, I have tried all conclusions I could draw.
>
> Julio

Nope, I made an error, I have to retract my claim.
I think I nevertheless found the Liar Paradox inside
the Epimenides Paradox. I think Dan Christensen used

something like:

(Pb ↔ ∀x¬Px) → ¬Pb is valid.
https://www.umsu.de/trees/#(Pb~4~6x~3Px)~5~3Pb

We can also write it like this, there is now a collection of b's
that satisfies Pb, and this collection is non-empty, this is what ∃xPx says.

(∃xPx ↔ ∀x¬Px) → ¬∃xPx is valid.
https://www.umsu.de/trees/#(~7xPx~4~6x~3Px)~5~3~7xPx

But the above is a vacous truth, since ∃xPx ↔ ∀x¬Px is
logically equivalent to ∃xPx ↔ ¬∃xPx which is an
antinomy, namely we have:

¬(∃xPx ↔ ¬∃xPx) is valid.
https://www.umsu.de/trees/#~3(~7xPx~4~3~7xPx)

Mild Shock schrieb am Donnerstag, 31. August 2023 um 23:55:47 UTC+2:
> The Epimenides Paradox is not an Antinomy like the Liar Paradox.
> If we take the Liar Paradox to be Q <=> ~Q, we see that this here
> is also a Liar Paradox, when we replace Q by ALL(x):P(x):
>
> ALL(x):P(x) <=> ~ALL(x):P(x)
>
> Wolfgang Scharz tree tool indeed confirms that it is an Antinomy,
> in that it can be Refuted, i.e. Disproved by producing a proof
> of its negation. The proof tells me the truth table has "F" everywhere:
>
> ¬(∀xPx ↔ ¬∀xPx) is valid.
> https://www.umsu.de/trees/#~3(~6xPx~4~3~6xPx)
>
> Now how do we get the Epimenides Paradox? You only need to
> tweak the above formula a little bit, and you get not anymore
> an Antinomy. Negation is not provable so the truth table has somewhere "T":
>
> ¬(∀xPx ↔ ¬∃xPx) is invalid.
> https://www.umsu.de/trees/#~3(~6xPx~4~3~7xPx)
>
> But the above formula has another advantage, you can use
> it to prove the contrary of what it has inside:
>
> (∀xPx ↔ ¬∃xPx) → ∃xPx is valid.
> https://www.umsu.de/trees/#(~6xPx~4~3~7xPx)~5~7xPx
>
> This is similar to the True(x) that appears inside the Epimenides
> proof in DC Proof, that then leads to ~True(x). Actually I think
> the Epimenides proof can be reduced to the above, I found
>
> it my some manipulations of the Epimendides proof.
> Julio Di Egidio schrieb am Donnerstag, 31. August 2023 um 20:05:42 UTC+2:
> > On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:
> >
> > [Corrected:]
> > > OTOH "I do not tell the truth" indeed is not as simple (basic)
> > > as "I am not true": so maybe Russell does go with Epimenides...
> >
> > Here is (my) Epimenides' for comparison:
> > <https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ>
> > with the caution that it is not finished, i.e. it's neither polished
> > nor, more importantly, I have tried all conclusions I could draw.
> >
> > Julio