On Saturday, August 26, 2023 at 7:36:07 AM UTC-4, Mild Shock wrote:
[snip]

> 255 Function(h,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
> => [h(a1)=b <=> (a1,b) @ gra]]
> E Spec, 254
>

[snip]

> 402 ~h @ dom
> Conclusion, 389
>

So, for function h: dom -->cod, we have ~h in dom. Seems reasonable, but even if true, so, what??? How is this relevant to my resolution of the Liar Paradox?

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

You see it better in this version, that the Grelling Paradox
has ~q <=> q, i.e. the Liar Paradox, after U Spec. You see
it here, or maybe you don't see, since you are a blind mole?

vvvvvvvvvvvvvvvvvvvv here vvvvvvvvvvvvvvvvvvvvvv
2 ~Phi(u,u) <=> Phi(u,u)
U Spec,
^^^^^^^^^^^^^^^^^^^^^^^ here ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Credits for the Proof go to Culio.

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 ------------------------------------------
Dan Christensen schrieb am Sonntag, 27. August 2023 um 03:35:52 UTC+2:
> On Saturday, August 26, 2023 at 7:36:07 AM UTC-4, Mild Shock wrote:
> [snip]
> > 255 Function(h,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
> > => [h(a1)=b <=> (a1,b) @ gra]]
> > E Spec, 254
> >
> [snip]
>
> > 402 ~h @ dom
> > Conclusion, 389
> >
>
> So, for function h: dom -->cod, we have ~h in dom. Seems reasonable, but even if true, so, what??? How is this relevant to my resolution of the Liar Paradox?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, 27 August 2023 at 14:00:04 UTC+2, Mild Shock wrote:
<snip>
> You see it better in this version, that the Grelling Paradox
> has ~q <=> q, i.e. the Liar Paradox, after U Spec. You see
> it here, or maybe you don't see, since you are a blind mole?
> vvvvvvvvvvvvvvvvvvvv here vvvvvvvvvvvvvvvvvvvvvv
> 2 ~Phi(u,u) <=> Phi(u,u)
> U Spec,
> ^^^^^^^^^^^^^^^^^^^^^^^ here ^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Credits for the Proof go to Culio.

Credits to me for showing *how to formalize* a given
informal (in fact, Logical with capital L) *problem*, which is
the genuinely complex part, and only secondarily for proving
that a self-contradictory statement indeed is identically false,
in around 3 lines of plain constructive FOPL.
<https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/dXjsL3Q4FQAJ>

You not only (systematically) just write the formal statement
as if that per se was any problem, you also take a ridiculous
amount of (strictly non-constructive, of course) machinery
and steps to derive an otherwise trivial consequence.

[From the linked thread:]
> 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?

Can't you do *case analysis*? Or better yet, stop spamming
the Usenet and try another hobby: like, jumping off bridges...

Julio

I don't know, please englighten us. Show us a proof that
doesn't use Rem DNeg. I don't excluded that possiblity
that it can be done.

But I guess you don't belong to the sports camp Culio.
What are you, a lazy nazi potato? An agent of the
enemy with a motivation problem?

LoL

Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 15:05:38 UTC+2:
> Can't you do *case analysis*? Or better yet, stop spamming
> the Usenet and try another hobby: like, jumping off bridges...

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

Mild Shock schrieb am Sonntag, 27. August 2023 um 16:44:24 UTC+2:
> I don't know, please englighten us. Show us a proof that
> doesn't use Rem DNeg. I don't excluded that possiblity
> that it can be done.
>
> But I guess you don't belong to the sports camp Culio.
> What are you, a lazy nazi potato? An agent of the
> enemy with a motivation problem?
>
> LoL
> Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 15:05:38 UTC+2:
> > Can't you do *case analysis*? Or better yet, stop spamming
> > the Usenet and try another hobby: like, jumping off bridges...

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

Nachricht Mild Shock schrieb am Sonntag, 27. August 2023 um 16:59:41 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 ----------------------------------------
> Mild Shock schrieb am Sonntag, 27. August 2023 um 16:44:24 UTC+2:
> > I don't know, please englighten us. Show us a proof that
> > doesn't use Rem DNeg. I don't excluded that possiblity
> > that it can be done.
> >
> > But I guess you don't belong to the sports camp Culio.
> > What are you, a lazy nazi potato? An agent of the
> > enemy with a motivation problem?
> >
> > LoL
> > Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 15:05:38 UTC+2:
> > > Can't you do *case analysis*? Or better yet, stop spamming
> > > the Usenet and try another hobby: like, jumping off bridges...

On Sunday, 27 August 2023 at 16:44:24 UTC+2, Mild Shock wrote:

> I don't know, please englighten us. Show us a proof that
> doesn't use Rem DNeg. I don't excluded that possiblity
> that it can be done.

<https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/V-JR00TkFQAJ>

> But I guess you don't belong to the sports camp Culio.

What camp is that, you stupid spamming cunt?

*Plonk*

Julio

I don't think anybody is helped with showing LTac crap
from Coq, as you do Culio. DC Proof proofs are written in
a form of natural deduction. And if a certain subset

of command is used, and can also see whether a
proof is constructive or not, respectively whether
it is intuitionistically valid or not.

Like if you don't use Rem DNeg, and only Split Join
Detach and Conclusion, you get a nice minimal logic
proof. In the present example there is also U Spec involved

and then an unnamed rule, namely it did add an
existential quantifier during Conclusion.

Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 17:06:20 UTC+2:
> On Sunday, 27 August 2023 at 16:44:24 UTC+2, Mild Shock wrote:
>
> > I don't know, please englighten us. Show us a proof that
> > doesn't use Rem DNeg. I don't excluded that possiblity
> > that it can be done.
> <https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/V-JR00TkFQAJ>
> > But I guess you don't belong to the sports camp Culio.
> What camp is that, you stupid spamming cunt?
>
> *Plonk*
>
> Julio

Maybe thats the reason why logicians don't use Coq,
its just a pile of Ltac crap when you produce a proof:

Godzilla had a stroke trying to read this and fucking died
https://keepmeme.com/meme/godzilla-had-a-stroke-trying-to-read-this-and-died

Mild Shock schrieb am Sonntag, 27. August 2023 um 17:11:26 UTC+2:
> I don't think anybody is helped with showing LTac crap
> from Coq, as you do Culio. DC Proof proofs are written in
> a form of natural deduction. And if a certain subset
>
> of command is used, and can also see whether a
> proof is constructive or not, respectively whether
> it is intuitionistically valid or not.
>
> Like if you don't use Rem DNeg, and only Split Join
> Detach and Conclusion, you get a nice minimal logic
> proof. In the present example there is also U Spec involved
>
> and then an unnamed rule, namely it did add an
> existential quantifier during Conclusion.
> Julio Di Egidio schrieb am Sonntag, 27. August 2023 um 17:06:20 UTC+2:
> > On Sunday, 27 August 2023 at 16:44:24 UTC+2, Mild Shock wrote:
> >
> > > I don't know, please englighten us. Show us a proof that
> > > doesn't use Rem DNeg. I don't excluded that possiblity
> > > that it can be done.
> > <https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/V-JR00TkFQAJ>
> > > But I guess you don't belong to the sports camp Culio.
> > What camp is that, you stupid spamming cunt?
> >
> > *Plonk*
> >
> > Julio

Life is easier with labels. Pehou did a form of
"revenge paradox", you know Dans sentence is L:
L : This sentences is not true.

The "revenge paradox" has a different label R:
R : This sentences is not true and not indeterminate.

Oh sorry, Dans sentences don't have labels. Ok, is this
the reason that Dans doesn't understand the
"revenge paradoxes"? Its all detailed here:

Lecture 1: The Liar Paradox
- Provide a brief introduction to many-valued logics.
- Provide an introduction to the revenge problem.
http://fitelson.org/piksi/piksi_18/cook_notes.pdf

Hint: Revenge arguments purport to show that any proposed
solution to the semantic paradoxes generates new paradoxes.

Mild Shock schrieb am Mittwoch, 6. September 2023 um 22:27:13 UTC+2:
> Life is easier with labels. Pehou did a form of
> "revenge paradox", you know Dans sentence is L:
> L : This sentences is not true.
>
> The "revenge paradox" has a different label R:
> R : This sentences is not true and not indeterminate.
>
> Oh sorry, Dans sentences don't have labels. Ok, is this
> the reason that Dans doesn't understand the
> "revenge paradoxes"? Its all detailed here:
>
> Lecture 1: The Liar Paradox
> - Provide a brief introduction to many-valued logics.
> - Provide an introduction to the revenge problem.
> http://fitelson.org/piksi/piksi_18/cook_notes.pdf

On Wednesday, September 6, 2023 at 4:27:13 PM UTC-4, Mild Shock wrote:
> Life is easier with labels. Pehou did a form of
> "revenge paradox", you know Dans sentence is L:
> L : This sentences is not true.
>
> The "revenge paradox" has a different label R:
> R : This sentences is not true and not indeterminate.
>

Then that sentence is false.

There are 3 mutually exclusive possibilities here. When 2 of them have been eliminated, then the remaining possibility must hold.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Here is a new challenge, can you find a revenge paradox to Dan
Christensens trichotomy, that doesn't use the word "indeterminate"
in its text form, respectively that doesn't use Uy in its formula?

Kind of works with a new hidden state, without mentioning it explicitly?

Mild Shock schrieb am Montag, 24. Juli 2023 um 21:23:27 UTC+2:
> Here we have a stipulation of a
> Trivalent solution to the Liar Paradox:
>
> https://dcproof.com/LiarParadox2.htm
>
> My stipulation is that there will be always
> the posibility to formulate some Paradox.
> For example Trivalently this is a new paradox:
>
> "this sentence does not express a true proposition"
>
> Its based on this truth table for "not express a true proposition":
>
> A A =\= T
> T F
> U T
> F T

Ok, here is a revenge paradox that doesn't mention Uy:

R'' : This sentences is true iff (if it is true then it is false).
(Ty ↔ (Ty → Fy))

This works:

∀x(Fx ∨ (Tx ∨ Ux)), ∀x¬(Fx ∧ Tx),
∀x¬(Fx ∧ Ux), ∀x¬(Tx ∧ Ux) entails ¬(Ty ↔ (Ty → Fy)).
https://www.umsu.de/trees/#~6x(Fx~2Tx~2Ux),~6x(~3(Fx~1Tx)),~6x(~3(Fx~1Ux)),~6x(~3(Tx~1Ux))|=~3(Ty~4(Ty~5Fy))

I got some help from Prolog. And found it with this query:

?- formula(3, X, Y), antinomy(X, (forall(X=t,Y),forall(Y,X=t))).
Y = (X = f; X = u);
Y = (X = u; X = f);
Y = forall(X = t, X = f);
Y = forall(X = t, X = u);
fail.

Prolog source code here:

formula(1, X, X = C) :- !,
value(_, C).
formula(N, X, Y) :- !,
M is N-1, formula(_, M, X, Y).

formula(0, N, X, (\+ Y)) :- formula(N, X, Y).
formula(1, N, X, (Y ; Z)) :- M is N-1, between(1, M, K), J is N-K,
formula(K, X, Y), formula(J, X, Z).
formula(2, N, X, (Y , Z)) :- M is N-1, between(1, M, K), J is N-K,
formula(K, X, Y), formula(J, X, Z).
formula(2, N, X, forall(Y , Z)) :- M is N-1, between(1, M, K), J is N-K,
formula(K, X, Y), formula(J, X, Z).

antinomy(X, Y) :- \+ (value(_, X), Y).

value(0, f).
value(1, u).
value(2, t).

Mild Shock schrieb am Dienstag, 12. September 2023 um 20:07:00 UTC+2:
> Here is a new challenge, can you find a revenge paradox to Dan
> Christensens trichotomy, that doesn't use the word "indeterminate"
> in its text form, respectively that doesn't use Uy in its formula?
>
> Kind of works with a new hidden state, without mentioning it explicitly?
>
> Mild Shock schrieb am Montag, 24. Juli 2023 um 21:23:27 UTC+2:
> > Here we have a stipulation of a
> > Trivalent solution to the Liar Paradox:
> >
> > https://dcproof.com/LiarParadox2.htm
> >
> > My stipulation is that there will be always
> > the posibility to formulate some Paradox.
> > For example Trivalently this is a new paradox:
> >
> > "this sentence does not express a true proposition"
> >
> > Its based on this truth table for "not express a true proposition":
> >
> > A A =\= T
> > T F
> > U T
> > F T

Since it doesn't mention Uy, we can try whether it also
works in bi-valence. And amazingly its also an Antinomy
in bi-valence. I get this result:

L' : This sentences is true iff (if it is true then it is false).
¬(p ↔ (p→¬p)) is valid.
https://www.umsu.de/trees/#~3(p~4(p~5~3p))

Mild Shock schrieb am Dienstag, 12. September 2023 um 20:15:51 UTC+2:
> Ok, here is a revenge paradox that doesn't mention Uy:
>
> R'' : This sentences is true iff (if it is true then it is false).
> (Ty ↔ (Ty → Fy))
>
> This works:
>
> ∀x(Fx ∨ (Tx ∨ Ux)), ∀x¬(Fx ∧ Tx),
> ∀x¬(Fx ∧ Ux), ∀x¬(Tx ∧ Ux) entails ¬(Ty ↔ (Ty → Fy)).
> https://www.umsu.de/trees/#~6x(Fx~2Tx~2Ux),~6x(~3(Fx~1Tx)),~6x(~3(Fx~1Ux)),~6x(~3(Tx~1Ux))|=~3(Ty~4(Ty~5Fy))
>
> I got some help from Prolog. And found it with this query:
>
> ?- formula(3, X, Y), antinomy(X, (forall(X=t,Y),forall(Y,X=t))).
> Y = (X = f; X = u);
> Y = (X = u; X = f);
> Y = forall(X = t, X = f);
> Y = forall(X = t, X = u);
> fail.
>
> Prolog source code here:
>
> formula(1, X, X = C) :- !,
> value(_, C).
> formula(N, X, Y) :- !,
> M is N-1, formula(_, M, X, Y).
>
> formula(0, N, X, (\+ Y)) :- formula(N, X, Y).
> formula(1, N, X, (Y ; Z)) :- M is N-1, between(1, M, K), J is N-K,
> formula(K, X, Y), formula(J, X, Z).
> formula(2, N, X, (Y , Z)) :- M is N-1, between(1, M, K), J is N-K,
> formula(K, X, Y), formula(J, X, Z).
> formula(2, N, X, forall(Y , Z)) :- M is N-1, between(1, M, K), J is N-K,
> formula(K, X, Y), formula(J, X, Z).
>
> antinomy(X, Y) :- \+ (value(_, X), Y).
>
> value(0, f).
> value(1, u).
> value(2, t).
> Mild Shock schrieb am Dienstag, 12. September 2023 um 20:07:00 UTC+2:
> > Here is a new challenge, can you find a revenge paradox to Dan
> > Christensens trichotomy, that doesn't use the word "indeterminate"
> > in its text form, respectively that doesn't use Uy in its formula?
> >
> > Kind of works with a new hidden state, without mentioning it explicitly?
> >
> > Mild Shock schrieb am Montag, 24. Juli 2023 um 21:23:27 UTC+2:
> > > Here we have a stipulation of a
> > > Trivalent solution to the Liar Paradox:
> > >
> > > https://dcproof.com/LiarParadox2.htm
> > >
> > > My stipulation is that there will be always
> > > the posibility to formulate some Paradox.
> > > For example Trivalently this is a new paradox:
> > >
> > > "this sentence does not express a true proposition"
> > >
> > > Its based on this truth table for "not express a true proposition":
> > >
> > > A A =\= T
> > > T F
> > > U T
> > > F T

One key ingredient of Dan Christensens approach is to use
classical logic. He models the Liar sentences as (a e T <=> a e F),
so he uses classical logic. For classical propositional logic

there exists the notion of a propositional variable assignment,
and if L is a formula, set(L) would denote all possible variable
assignment. There is this rather trivial theorem:

Theorem: If sat(L)=\={} and sat(L) ⊆ Y \ X, then:
1) L is an Antinomy in X
2) L has a Resolution in Y

So we can use this for another type of Revenge Paradox, namely
that Dan Christensen has only shown a sufficient example for
Resolution, but not a necessary example for Resolution:

Take X = {{0},{1}} classical logic, then:

1) Y= { {}, {0}, {1}}: 3-valued Logic with bottom, the solution proposed
by Dan Christensen, is a Resolution
2) Y= { {0}, {1}, {0,1}: 3-valued Logic with top, sometimes called
Logic of Paradox, would be also a Resolution
3) Y= { {}, {0}, {1}, {0,1}: 4-valued Logic with bottom and top, called
Belnap FOUR, would be also a Resolution

Since there are more Resolutions than only one, he only showed
a sufficient example, its not some necessary example.