Ok, finally I got something new which wasn't yet patched
by Dan Christensen. Old attempts to prove an inconsistency
gradually got patched, for example Reflexivity rule t=t was changed

and so forth. But was DC Proof made water proof? Or is it rather
like OceanGates submersible that destroys itself during deployment?
I have pointed a million times that self application is dangerous,

and now reeding Alonzos Churchs papers I found a new proof:

/* Grelling's antinomy */
43 h(h)=1 & ~h(h)=1
Join, 28, 42

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

1 ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
Axiom

2 ALL(v):[h(v)=1 <=> EXIST(f):[ALL(x):v(x)=f(x) & ~f(v)=1]]
Axiom

3 h(h)=1 <=> EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
U Spec, 2

4 [h(h)=1 => EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]]
& [EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1]
Iff-And, 3

5 h(h)=1 => EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
Split, 4

6 EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1
Split, 4

7 ~h(h)=1 => ~EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
Contra, 6

8 ~h(h)=1
Premise

9 ~EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
Detach, 7, 8

10 ~~ALL(f):~[ALL(x):h(x)=f(x) & ~f(h)=1]
Quant, 9

11 ALL(f):~[ALL(x):h(x)=f(x) & ~f(h)=1]
Rem DNeg, 10

12 ~[ALL(x):h(x)=h(x) & ~h(h)=1]
U Spec, 11

13 ~~[~ALL(x):h(x)=h(x) | ~~h(h)=1]
DeMorgan, 12

14 ~~[~ALL(x):h(x)=h(x) | h(h)=1]
Rem DNeg, 13

15 ~ALL(x):h(x)=h(x) | h(h)=1
Rem DNeg, 14

16 ~~ALL(x):h(x)=h(x) => h(h)=1
Imply-Or, 15

17 ALL(x):h(x)=h(x) => h(h)=1
Rem DNeg, 16

18 ALL(g):[ALL(x):h(x)=g(x) <=> h=g]
U Spec, 1

19 ALL(x):h(x)=h(x) <=> h=h
U Spec, 18

20 [ALL(x):h(x)=h(x) => h=h] & [h=h => ALL(x):h(x)=h(x)]
Iff-And, 19

21 ALL(x):h(x)=h(x) => h=h
Split, 20

22 h=h => ALL(x):h(x)=h(x)
Split, 20

23 h=h
Reflex

24 ALL(x):h(x)=h(x)
Detach, 22, 23

25 h(h)=1
Detach, 17, 24

26 h(h)=1 & ~h(h)=1
Join, 25, 8

27 ~~h(h)=1
4 Conclusion, 8

28 h(h)=1
Rem DNeg, 27

29 h(h)=1
Premise

30 EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
Detach, 5, 29

31 ALL(x):h(x)=u(x) & ~u(h)=1
E Spec, 30

32 ALL(x):h(x)=u(x)
Split, 31

33 ~u(h)=1
Split, 31

34 ALL(g):[ALL(x):h(x)=g(x) <=> h=g]
U Spec, 1

35 ALL(x):h(x)=u(x) <=> h=u
U Spec, 34

36 [ALL(x):h(x)=u(x) => h=u] & [h=u => ALL(x):h(x)=u(x)]
Iff-And, 35

37 ALL(x):h(x)=u(x) => h=u
Split, 36

38 h=u => ALL(x):h(x)=u(x)
Split, 36

39 h=u
Detach, 37, 32

40 ~h(h)=1
Substitute, 39, 33

41 h(h)=1 & ~h(h)=1
Join, 29, 40

42 ~h(h)=1
4 Conclusion, 29

43 h(h)=1 & ~h(h)=1
Join, 28, 42

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

No wonky axioms involved. This here is extensionality:

/* Function Extensionality */
ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]

You can prove it in set theory, when f and g are set like.
This here is the definition of the adjective heterological:

/* Adjective Heterological */
ALL(v):[h(v)=1 <=> EXIST(f):[ALL(x):v(x)=f(x) & ~f(v)=1]]

See also Wikipedia:

the word "heterological", meaning "inapplicable to itself"
https://en.wikipedia.org/wiki/Grelling%E2%80%93Nelson_paradox

Mild Shock schrieb am Dienstag, 22. August 2023 um 17:13:12 UTC+2:
> Ok, finally I got something new which wasn't yet patched
> by Dan Christensen. Old attempts to prove an inconsistency
> gradually got patched, for example Reflexivity rule t=t was changed
>
> and so forth. But was DC Proof made water proof? Or is it rather
> like OceanGates submersible that destroys itself during deployment?
> I have pointed a million times that self application is dangerous,
>
> and now reeding Alonzos Churchs papers I found a new proof:
>
> /* Grelling's antinomy */
> 43 h(h)=1 & ~h(h)=1
> Join, 28, 42
>
> --------------------------------- begin proof --------------------------------
>
> 1 ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> Axiom
>
> 2 ALL(v):[h(v)=1 <=> EXIST(f):[ALL(x):v(x)=f(x) & ~f(v)=1]]
> Axiom
>
> 3 h(h)=1 <=> EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
> U Spec, 2
>
> 4 [h(h)=1 => EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]]
> & [EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1]
> Iff-And, 3
>
> 5 h(h)=1 => EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
> Split, 4
>
> 6 EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1
> Split, 4
>
> 7 ~h(h)=1 => ~EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
> Contra, 6
>
> 8 ~h(h)=1
> Premise
>
> 9 ~EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
> Detach, 7, 8
>
> 10 ~~ALL(f):~[ALL(x):h(x)=f(x) & ~f(h)=1]
> Quant, 9
>
> 11 ALL(f):~[ALL(x):h(x)=f(x) & ~f(h)=1]
> Rem DNeg, 10
>
> 12 ~[ALL(x):h(x)=h(x) & ~h(h)=1]
> U Spec, 11
>
> 13 ~~[~ALL(x):h(x)=h(x) | ~~h(h)=1]
> DeMorgan, 12
>
> 14 ~~[~ALL(x):h(x)=h(x) | h(h)=1]
> Rem DNeg, 13
>
> 15 ~ALL(x):h(x)=h(x) | h(h)=1
> Rem DNeg, 14
>
> 16 ~~ALL(x):h(x)=h(x) => h(h)=1
> Imply-Or, 15
>
> 17 ALL(x):h(x)=h(x) => h(h)=1
> Rem DNeg, 16
>
> 18 ALL(g):[ALL(x):h(x)=g(x) <=> h=g]
> U Spec, 1
>
> 19 ALL(x):h(x)=h(x) <=> h=h
> U Spec, 18
>
> 20 [ALL(x):h(x)=h(x) => h=h] & [h=h => ALL(x):h(x)=h(x)]
> Iff-And, 19
>
> 21 ALL(x):h(x)=h(x) => h=h
> Split, 20
>
> 22 h=h => ALL(x):h(x)=h(x)
> Split, 20
>
> 23 h=h
> Reflex
>
> 24 ALL(x):h(x)=h(x)
> Detach, 22, 23
>
> 25 h(h)=1
> Detach, 17, 24
>
> 26 h(h)=1 & ~h(h)=1
> Join, 25, 8
>
> 27 ~~h(h)=1
> 4 Conclusion, 8
>
> 28 h(h)=1
> Rem DNeg, 27
>
> 29 h(h)=1
> Premise
>
> 30 EXIST(f):[ALL(x):h(x)=f(x) & ~f(h)=1]
> Detach, 5, 29
>
> 31 ALL(x):h(x)=u(x) & ~u(h)=1
> E Spec, 30
>
> 32 ALL(x):h(x)=u(x)
> Split, 31
>
> 33 ~u(h)=1
> Split, 31
>
> 34 ALL(g):[ALL(x):h(x)=g(x) <=> h=g]
> U Spec, 1
>
> 35 ALL(x):h(x)=u(x) <=> h=u
> U Spec, 34
>
> 36 [ALL(x):h(x)=u(x) => h=u] & [h=u => ALL(x):h(x)=u(x)]
> Iff-And, 35
>
> 37 ALL(x):h(x)=u(x) => h=u
> Split, 36
>
> 38 h=u => ALL(x):h(x)=u(x)
> Split, 36
>
> 39 h=u
> Detach, 37, 32
>
> 40 ~h(h)=1
> Substitute, 39, 33
>
> 41 h(h)=1 & ~h(h)=1
> Join, 29, 40
>
> 42 ~h(h)=1
> 4 Conclusion, 29
>
> 43 h(h)=1 & ~h(h)=1
> Join, 28, 42
>
> --------------------------------- end proof --------------------------------

On Tuesday, August 22, 2023 at 11:33:45 AM UTC-4, Mild Shock wrote:
> No wonky axioms involved. This here is extensionality:
>
> /* Function Extensionality */
> ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]

[snip]

Not in DC Proof. See the Function and Function Equality Axioms on the Sets menu.

Dan

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

In math text books it is. Why should it not hold?
Can you make a counter example? LoL

Dan Christensen schrieb am Dienstag, 22. August 2023 um 18:10:27 UTC+2:
> On Tuesday, August 22, 2023 at 11:33:45 AM UTC-4, Mild Shock wrote:
> > No wonky axioms involved. This here is extensionality:
> >
> > /* Function Extensionality */
> > ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> [snip]
>
> Not in DC Proof. See the Function and Function Equality Axioms on the Sets menu.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Example from math:

f : R\{0} -> R, f(x) = x^2/x
g : R\{0} -> R, g(x) = x if x=\=0 else undefined

Extensionally they are the same function graphs.
And this here holds, for the universal domain:

ALL(x):f(x)=g(x)

If x is outside of R\{0} then f(x) is undefined and
g(x) is undefined, therefore f(x)=g(x). If x is inside
R\{0} then f(x) is defined and g(x) is defined and

we can cancel x, since x is not equal zero, i.e.
f(x) = x^2/x = x = g(x).

Mild Shock schrieb am Dienstag, 22. August 2023 um 18:57:50 UTC+2:
> In math text books it is. Why should it not hold?
> Can you make a counter example? LoL
> Dan Christensen schrieb am Dienstag, 22. August 2023 um 18:10:27 UTC+2:
> > On Tuesday, August 22, 2023 at 11:33:45 AM UTC-4, Mild Shock wrote:
> > > No wonky axioms involved. This here is extensionality:
> > >
> > > /* Function Extensionality */
> > > ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> > [snip]
> >
> > Not in DC Proof. See the Function and Function Equality Axioms on the Sets menu.
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, August 22, 2023 at 12:57:50 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Dienstag, 22. August 2023 um 18:10:27 UTC+2:
> > On Tuesday, August 22, 2023 at 11:33:45 AM UTC-4, Mild Shock wrote:
> > > No wonky axioms involved. This here is extensionality:
> > >
> > > /* Function Extensionality */
> > > ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> > [snip]
> >
> > Not in DC Proof. See the Function and Function Equality Axioms on the Sets menu.
> >

> In math text books it is. Why should it not hold?

Functions f and g are comparable only if they have the same domain and codomain. There is no mention of any domain or codomain in your axioms here. Again, see the Function and Function Equality Axioms on the Sets menu.

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
if and only if f(x) = g(x) for all x ∈ X. "
--Terrance Tao, "Analysis I," p.51

Dan

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

I am a nice person, I don't open a new thread for a revision?

Here is a more precise proof. Now extensionality is
also 100% compatible with set theory, because my original
extensionality axiom assumed implicitly Fun(f) and Fun(g),

but its better to make it explicit, since there are sets that
are not necessarely functional or even pure collection of pairs,
i.e. relations. So with the preconditions Fun(f) and Fun(g) we

are on the safe side. I guess you can also extend it to
Function(f,dom,cod), but for a start here is only the proof
with Fun(f) and Fun(g). I didn't try yet Function(f,dom,cod).

But with Fun(f) I easily get again:

52 h(h)=1 & ~h(h)=1
Join, 51, 50

------------------------------ begin proof version 2 ----------------------------------

1 ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
Axiom

2 Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
Axiom

3 Fun(h)
Split, 2

4 ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
Split, 2

5 h(h)=1 <=> EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
U Spec, 4

6 [h(h)=1 => EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]]
& [EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1]
Iff-And, 5

7 h(h)=1 => EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Split, 6

8 EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1] => h(h)=1
Split, 6

9 ~h(h)=1 => ~EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Contra, 8

10 ~h(h)=1
Premise

11 ~EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Detach, 9, 10

12 ~~ALL(f):~[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Quant, 11

13 ALL(f):~[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Rem DNeg, 12

14 ~[Fun(h) & ALL(x):h(x)=h(x) & ~h(h)=1]
U Spec, 13

15 ~~[~[Fun(h) & ALL(x):h(x)=h(x)] | ~~h(h)=1]
DeMorgan, 14

16 ~[Fun(h) & ALL(x):h(x)=h(x)] | ~~h(h)=1
Rem DNeg, 15

17 ~~[Fun(h) & ALL(x):h(x)=h(x)] => ~~h(h)=1
Imply-Or, 16

18 Fun(h) & ALL(x):h(x)=h(x) => ~~h(h)=1
Rem DNeg, 17

19 Fun(h) & ALL(x):h(x)=h(x) => h(h)=1
Rem DNeg, 18

20 ALL(g):[Fun(h) & Fun(g) => [ALL(x):h(x)=g(x) <=> h=g]]
U Spec, 1

21 Fun(h) & Fun(h) => [ALL(x):h(x)=h(x) <=> h=h]
U Spec, 20

22 Fun(h) & Fun(h)
Join, 3, 3

23 ALL(x):h(x)=h(x) <=> h=h
Detach, 21, 22

24 [ALL(x):h(x)=h(x) => h=h] & [h=h => ALL(x):h(x)=h(x)]
Iff-And, 23

25 ALL(x):h(x)=h(x) => h=h
Split, 24

26 h=h => ALL(x):h(x)=h(x)
Split, 24

27 h=h
Reflex

28 ALL(x):h(x)=h(x)
Detach, 26, 27

29 Fun(h) & ALL(x):h(x)=h(x)
Join, 3, 28

30 h(h)=1
Detach, 19, 29

31 ~h(h)=1 & h(h)=1
Join, 10, 30

32 ~~h(h)=1
4 Conclusion, 10

33 h(h)=1
Rem DNeg, 32

34 h(h)=1
Premise

35 EXIST(f):[Fun(f) & ALL(x):h(x)=f(x) & ~f(h)=1]
Detach, 7, 34

36 Fun(u) & ALL(x):h(x)=u(x) & ~u(h)=1
E Spec, 35

37 Fun(u)
Split, 36

38 ALL(x):h(x)=u(x)
Split, 36

39 ~u(h)=1
Split, 36

40 ALL(g):[Fun(h) & Fun(g) => [ALL(x):h(x)=g(x) <=> h=g]]
U Spec, 1

41 Fun(h) & Fun(u) => [ALL(x):h(x)=u(x) <=> h=u]
U Spec, 40

42 Fun(h) & Fun(u)
Join, 3, 37

43 ALL(x):h(x)=u(x) <=> h=u
Detach, 41, 42

44 [ALL(x):h(x)=u(x) => h=u] & [h=u => ALL(x):h(x)=u(x)]
Iff-And, 43

45 ALL(x):h(x)=u(x) => h=u
Split, 44

46 h=u => ALL(x):h(x)=u(x)
Split, 44

47 h=u
Detach, 45, 38

48 ~h(h)=1
Substitute, 47, 39

49 h(h)=1 & ~h(h)=1
Join, 34, 48

50 ~h(h)=1
4 Conclusion, 34

51 h(h)=1
Rem DNeg, 32

52 h(h)=1 & ~h(h)=1
Join, 51, 50

------------------------------ end proof version 2 ----------------------------------

Dan Christensen schrieb am Dienstag, 22. August 2023 um 20:01:09 UTC+2:
> On Tuesday, August 22, 2023 at 12:57:50 PM UTC-4, Mild Shock wrote:
>
> > Dan Christensen schrieb am Dienstag, 22. August 2023 um 18:10:27 UTC+2:
> > > On Tuesday, August 22, 2023 at 11:33:45 AM UTC-4, Mild Shock wrote:
> > > > No wonky axioms involved. This here is extensionality:
> > > >
> > > > /* Function Extensionality */
> > > > ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> > > [snip]
> > >
> > > Not in DC Proof. See the Function and Function Equality Axioms on the Sets menu.
> > >
> > In math text books it is. Why should it not hold?
> Functions f and g are comparable only if they have the same domain and codomain. There is no mention of any domain or codomain in your axioms here. Again, see the Function and Function Equality Axioms on the Sets menu.
>
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X. "
> --Terrance Tao, "Analysis I," p.51
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, August 22, 2023 at 2:42:49 PM UTC-4, Mild Shock wrote:
[snip]

>
> ------------------------------ begin proof version 2 ----------------------------------
>
> 1 ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> Axiom
>
> 2 Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> Axiom
>
[snip]

I see you would rather not use the function axioms built into DC Proof (on the Sets menu). It seems you get an inconsistency when you use YOUR OWN axioms. What does THAT tell you about your axioms? Garbage in, garbage out???

Dan

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

You can try the your function axioms built into DC Proof.
It wont change anything. For example the function equality is now:

ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
Axiom

With your built in axioms it will become:

1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& Function(f1,dom,cod) & Function(f2,dom,cod)
=> [f1=f2 <=> ALL(a):[a @ dom => f1(a)=f2(a)]]]
Fn Equality

Then the definition of h is currently:

Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
Axiom

With your built in axioms it will become:

2 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]]]
Function

Now question is whether we can create the set gra? Namely
this set, does it exist in DC Proof:

{ (v,1) e dom x cod | EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1] }

Well the subset axiom doesn't prevent the creation of this set. You
can try yourself. It allows me to state:

13 EXIST(h):[Set'(h) & ALL(v):ALL(y):[(v,y) @ h <=> (v,y) @ s &
EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=y]]]
Subset, 11

So I speculate that the Grelling's antinomy can be reproduced.

Dan Christensen schrieb am Dienstag, 22. August 2023 um 21:15:56 UTC+2:
> On Tuesday, August 22, 2023 at 2:42:49 PM UTC-4, Mild Shock wrote:
> [snip]
> >
> > ------------------------------ begin proof version 2 ----------------------------------
> >
> > 1 ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> > Axiom
> >
> > 2 Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> > Axiom
> >
> [snip]
>
> I see you would rather not use the function axioms built into DC Proof (on the Sets menu). It seems you get an inconsistency when you use YOUR OWN axioms. What does THAT tell you about your axioms? Garbage in, garbage out???
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

The only thing that might prevent the Grelling's antinomy, I guess,
is the side condition (v,y) @ s, when we use v=h. But DC Proof
has no regularity axiom. So theoretically its possible.

But then there is another Grelling's antinomy, which is easier to
derive. Namely when we do not require that the "heterological"
adjective itself is constructive, in the sense that it would be

constructed by your subset axiom, but would accept a definition
for a functor. What is then doubtful, is the postulate Fun(h).

Mild Shock schrieb am Dienstag, 22. August 2023 um 23:56:16 UTC+2:
> You can try the your function axioms built into DC Proof.
> It wont change anything. For example the function equality is now:
> ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> Axiom
> With your built in axioms it will become:
>
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & Function(f1,dom,cod) & Function(f2,dom,cod)
> => [f1=f2 <=> ALL(a):[a @ dom => f1(a)=f2(a)]]]
> Fn Equality
>
> Then the definition of h is currently:
> Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> Axiom
> With your built in axioms it will become:
>
> 2 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> => [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
> & ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
> => [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
> => EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
> => [fun(a1)=b <=> (a1,b) @ gra]]]]]
> Function
>
> Now question is whether we can create the set gra? Namely
> this set, does it exist in DC Proof:
>
> { (v,1) e dom x cod | EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1] }
>
> Well the subset axiom doesn't prevent the creation of this set. You
> can try yourself. It allows me to state:
>
> 13 EXIST(h):[Set'(h) & ALL(v):ALL(y):[(v,y) @ h <=> (v,y) @ s &
> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=y]]]
> Subset, 11
>
> So I speculate that the Grelling's antinomy can be reproduced.
> Dan Christensen schrieb am Dienstag, 22. August 2023 um 21:15:56 UTC+2:
> > On Tuesday, August 22, 2023 at 2:42:49 PM UTC-4, Mild Shock wrote:
> > [snip]
> > >
> > > ------------------------------ begin proof version 2 ----------------------------------
> > >
> > > 1 ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> > > Axiom
> > >
> > > 2 Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> > > Axiom
> > >
> > [snip]
> >
> > I see you would rather not use the function axioms built into DC Proof (on the Sets menu). It seems you get an inconsistency when you use YOUR OWN axioms. What does THAT tell you about your axioms? Garbage in, garbage out???
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

To solve the domain problem, we might need to think a little
bit out of the box. What helps here is that DC Proof has no
regularity axiom, so h e dom in itself is not contradictory.

So instead of replicating Grelling's antinomy in this form:

h(h)=1 & ~h(h)=1

We might make an attempt to derive this formula:

[h e dom & h(h)=1] & ~[h e dom & h(h)=1]

This looks quite promissing.

Mild Shock schrieb am Mittwoch, 23. August 2023 um 00:08:15 UTC+2:
> The only thing that might prevent the Grelling's antinomy, I guess,
> is the side condition (v,y) @ s, when we use v=h. But DC Proof
> has no regularity axiom. So theoretically its possible.
>
> But then there is another Grelling's antinomy, which is easier to
> derive. Namely when we do not require that the "heterological"
> adjective itself is constructive, in the sense that it would be
>
> constructed by your subset axiom, but would accept a definition
> for a functor. What is then doubtful, is the postulate Fun(h).
> Mild Shock schrieb am Dienstag, 22. August 2023 um 23:56:16 UTC+2:
> > You can try the your function axioms built into DC Proof.
> > It wont change anything. For example the function equality is now:
> > ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> > Axiom
> > With your built in axioms it will become:
> >
> > 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & Function(f1,dom,cod) & Function(f2,dom,cod)
> > => [f1=f2 <=> ALL(a):[a @ dom => f1(a)=f2(a)]]]
> > Fn Equality
> >
> > Then the definition of h is currently:
> > Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> > Axiom
> > With your built in axioms it will become:
> >
> > 2 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> > => [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
> > & ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
> > => [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
> > => EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
> > => [fun(a1)=b <=> (a1,b) @ gra]]]]]
> > Function
> >
> > Now question is whether we can create the set gra? Namely
> > this set, does it exist in DC Proof:
> >
> > { (v,1) e dom x cod | EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1] }
> >
> > Well the subset axiom doesn't prevent the creation of this set. You
> > can try yourself. It allows me to state:
> >
> > 13 EXIST(h):[Set'(h) & ALL(v):ALL(y):[(v,y) @ h <=> (v,y) @ s &
> > EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=y]]]
> > Subset, 11
> >
> > So I speculate that the Grelling's antinomy can be reproduced.
> > Dan Christensen schrieb am Dienstag, 22. August 2023 um 21:15:56 UTC+2:
> > > On Tuesday, August 22, 2023 at 2:42:49 PM UTC-4, Mild Shock wrote:
> > > [snip]
> > > >
> > > > ------------------------------ begin proof version 2 ----------------------------------
> > > >
> > > > 1 ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> > > > Axiom
> > > >
> > > > 2 Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> > > > Axiom
> > > >
> > > [snip]
> > >
> > > I see you would rather not use the function axioms built into DC Proof (on the Sets menu). It seems you get an inconsistency when you use YOUR OWN axioms. What does THAT tell you about your axioms? Garbage in, garbage out???
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:

> Functions f and g are comparable only if they have the same domain and codomain.

Anyone except crank DC knows that this is nonsense.

*** Holy shit! ***

On Tuesday, August 22, 2023 at 5:56:16 PM UTC-4, Mild Shock wrote:
> You can try the your function axioms built into DC Proof.
> It wont change anything. For example the function equality is now:
> ALL(f):ALL(g):[Fun(f) & Fun(g) => [ALL(x):f(x)=g(x) <=> f=g]]
> Axiom

That apparently leads to inconsistencies. Better to stick to the built-in axioms. Thanks anyway.

> With your built in axioms it will become:
>
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & Function(f1,dom,cod) & Function(f2,dom,cod)
> => [f1=f2 <=> ALL(a):[a @ dom => f1(a)=f2(a)]]]
> Fn Equality
>

Much better! With Function(f1,dom,cod) and Function(f2,dom,cod), you have functions f1 and f2 with the same domain and codomain.

> Then the definition of h is currently:
> Fun(h) & ALL(v):[h(v)=1 <=> EXIST(f):[Fun(f) & ALL(x):v(x)=f(x) & ~f(v)=1]]
> Axiom

To introduce a function, at the very least, you need, at the very least, to name that function and its domain and codomain sets.

> With your built in axioms it will become:
>
> 2 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> => [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
> & ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
> => [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
> => EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
> => [fun(a1)=b <=> (a1,b) @ gra]]]]]
> Function
>
> Now question is whether we can create the set gra? Namely
> this set, does it exist in DC Proof:
>

1. Set(x)
Axiom

2. Set(y)
Axiom

3. 1 in y
Axiom

4. ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in a1 & c2 in a2]]]
Cart Prod

5. ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in a2]]]
U Spec, 4

6. Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
U Spec, 5

7. Set(x) & Set(y)
Join, 1, 2

8. EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
Detach, 6, 7

9. Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
E Spec, 8

10. Set'(xy)
Split, 9

11. ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
Split, 9

12. EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) in sub <=> (a,b) in xy & b=1]]
Subset, 10

13. Set'(g) & ALL(a):ALL(b):[(a,b) in g <=> (a,b) in xy & b=1]
E Spec, 12

13 Set'(g) & ALL(a):ALL(b):[(a,b) in g <=> (a,b) in xy & b=1]
E Spec, 12

14. Set'(g)
Split, 13

15. ALL(a):ALL(b):[(a,b) in g <=> (a,b) in xy & b=1]
Split, 13

Then apply the function axiom:

16. ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 in dom & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]]
Function

17. ALL(cod):ALL(gra):[Set(x) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in cod]
& ALL(a1):[a1 in x => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in cod & b2 in cod
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):[Function(fun,x,cod) & ALL(a1):ALL(b):[a1 in x & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]]
U Spec, 16

18. ALL(gra):[Set(x) & Set(y) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in x & b in y]
& ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
=> EXIST(fun):[Function(fun,x,y) & ALL(a1):ALL(b):[a1 in x & b in y
=> [fun(a1)=b <=> (a1,b) in gra]]]]]
U Spec, 17

Sufficient for functionality of g:

19. Set(x) & Set(y) & Set'(g)

=> [ALL(a1):ALL(b):[(a1,b) in g => a1 in x & b in y]
& ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in g]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
=> [(a1,b1) in g & (a1,b2) in g => b1=b2]]

=> EXIST(fun):[Function(fun,x,y) & ALL(a1):ALL(b):[a1 in x & b in y
=> [fun(a1)=b <=> (a1,b) in g]]]]
U Spec, 18

Will leave the rest to you as a trivial exercise.

Dan

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

On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
>
> > Functions f and g are comparable only if they have the same domain and codomain.
> Anyone except crank DC knows that this is nonsense.
>

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
if and only if f(x) = g(x) for all x ∈ X. "
---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)

Dan

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

On Wednesday, August 23, 2023 at 1:57:52 AM UTC+2, Dan Christensen wrote:
> On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > >
> > > Functions f and g are comparable only if they have the same domain and codomain.
> > >
> > Anyone except crank DC knows that this is nonsense.
> >
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X. "
> ---Terence Tao, "Analysis I," p.51

Yes, we know that you are a crank. And it shows!

Hint: You simply do not know what you are talking about, dumbo.

On Tuesday, August 22, 2023 at 8:08:33 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, August 23, 2023 at 1:57:52 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > > On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > > >
> > > > Functions f and g are comparable only if they have the same domain and codomain.
> > > >
> > > Anyone except crank DC knows that this is nonsense.
> > >

> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > if and only if f(x) = g(x) for all x ∈ X. "

> > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)

> Yes, we know that you are a crank. And it shows!
>

It seems I'm in good company! (Hee, hee!)

Dan

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
>> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
>>
>> > Functions f and g are comparable only if they have the same domain
>> > and codomain.
>>
>> Anyone except crank DC knows that this is nonsense.
>
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X. "
> ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)

Tao does not support your claim. For example (from the same book):

"... the two functions f and g are not considered the same function,
f =/= g, because they have different domains."

Of course, you might just be using the term "comparable" in some odd
way, but it suggests that you think functions with different domains or
codomains are neither equal nor not equal.

--
Ben.

On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> >>
> >> > Functions f and g are comparable only if they have the same domain
> >> > and codomain.
> >>
> >> Anyone except crank DC knows that this is nonsense.
> >
> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > if and only if f(x) = g(x) for all x ∈ X. "
> > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
> Tao does not support your claim. For example (from the same book):
>
> "... the two functions f and g are not considered the same function,
> f =/= g, because they have different domains."
>

Some context:

"Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
--p. 218

It would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of his formal definition of the equality of functions. "[W]e shall often be careless, and say things like..."

Dan

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

On Tuesday, August 22, 2023 at 7:57:56 PM UTC-7, Dan Christensen wrote:
> On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >
> > > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > >>
> > >> > Functions f and g are comparable only if they have the same domain
> > >> > and codomain.
> > >>
> > >> Anyone except crank DC knows that this is nonsense.
> > >
> > > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > > if and only if f(x) = g(x) for all x ∈ X. "
> > > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
> > Tao does not support your claim. For example (from the same book):
> >
> > "... the two functions f and g are not considered the same function,
> > f =/= g, because they have different domains."
> >
> Some context:
>
> "Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
> --p. 218
>
> It would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of his formal definition of the equality of functions. "[W]e shall often be careless, and say things like..."
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Function theory is among the most overloaded of the fields of elementary kinds of objects,
over time.

It's as of matters of relations, where relations are about being more fundamental than predicates,
even though usually enough it's the other way way. Other usual examples includes integers
then rationals or integers in rationals, where intensionality and extensionality get reversible
because they are reversible because there's a geometry of points and spaces for the most of
the assignments of the mathematical objects and it's reversible.

Now, coming from a guy like Dan who says "I proved 0^0 = 1", and it's like no you didn't, you
picked a branch of a multiplicity as what was a singularity to make a regularity and your
restriction of comprehension is noted as simply a letting, to "let", something be, that's
otherwise it's just another usual sort of wishful thinking. Because, for example, otherwise
you'd accept there aren't negative numbers, there aren't complex numbers, and so on,
just like other usual retro-finitist trolls of the sourpuss, folderol, and jibing ape variety.

On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> >>
> >> > Functions f and g are comparable only if they have the same domain
> >> > and codomain.
> >>
> >> Anyone except crank DC knows that this is nonsense.
> >
> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > if and only if f(x) = g(x) for all x ∈ X. "
> > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
> Tao does not support your claim. For example (from the same book):
>
> "... the two functions f and g are not considered the same function,
> f =/= g, because they have different domains."
>

Some context:

"Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
--p. 218

First, it would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of the formal definition of the equality of functions given here.

Also, since the above mentioned functions f and g do not have the same domains, the above definition of function equality cannot be applied to determine if they are equal. In other words, f and g are not considered the same function because they have different domains. The insertion of "f =/= g" is admittedly puzzling. Though it is completely unnecessary, it can certainly not be seen as a repudiation of the above definition.

Dan

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

There is nothing wrong with your function axioms. You are
on the wrong track. Grelling's antinomy is about this notion:

the word "heterological", meaning "inapplicable to itself"
https://en.wikipedia.org/wiki/Grelling%E2%80%93Nelson_paradox

So can we construct the adjective "heterological" in DC Proof?
If yes, we will arrive at a contradiction.

Dan Christensen schrieb am Mittwoch, 23. August 2023 um 07:21:04 UTC+2:
> On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >
> > > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > >>
> > >> > Functions f and g are comparable only if they have the same domain
> > >> > and codomain.
> > >>
> > >> Anyone except crank DC knows that this is nonsense.
> > >
> > > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > > if and only if f(x) = g(x) for all x ∈ X. "
> > > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
> > Tao does not support your claim. For example (from the same book):
> >
> > "... the two functions f and g are not considered the same function,
> > f =/= g, because they have different domains."
> >
> Some context:
>
> "Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
> --p. 218
>
> First, it would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of the formal definition of the equality of functions given here.
>
> Also, since the above mentioned functions f and g do not have the same domains, the above definition of function equality cannot be applied to determine if they are equal. In other words, f and g are not considered the same function because they have different domains. The insertion of "f =/= g" is admittedly puzzling. Though it is completely unnecessary, it can certainly not be seen as a repudiation of the above definition.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Ok, this is a quite long proof, using Function Axiom
and Function Equality twice, making the Grelling function
set like. It bails out with ~h e dom, very similar like what

Dan Christen found in his "Generalized Drinker Paradox" nonsense,
when he found that every set has an outside element:

402 ~h @ dom
5 Conclusion, 389

So when we would assume that h e dom, we would
get a contradiction. Was thinking about using Dana Scotts
trick, to provoke a contradiction. Not yet sure. Because

we have "dom" arbitrary, not really specified, we could
envision a kind of chasing game.

-------------------------- begin proof, collapsed view -----------------------------

1 Set(dom)
Axiom

2 Set(cod)
Axiom

3 ~0=1
Axiom

4 ALL(x):[x @ cod <=> x=0 | x=1]
Axiom

5 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) @ b <=> c1 @ a1 & c2 @ a2]]]
Cart Prod

6 ALL(a2):[Set(dom) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) @ b <=> c1 @ dom & c2 @ a2]]]
U Spec, 5

7 Set(dom) & Set(cod) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) @ b <=> c1 @ dom & c2 @ cod]]
U Spec, 6

8 Set(dom) & Set(cod)
Join, 1, 2

9 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) @ b <=> c1 @ dom & c2 @ cod]]
Detach, 7, 8

10 Set'(rel) & ALL(c1):ALL(c2):[(c1,c2) @ rel <=> c1 @ dom & c2 @ cod]
E Spec, 9

11 Set'(rel)
Split, 10

12 ALL(c1):ALL(c2):[(c1,c2) @ rel <=> c1 @ dom & c2 @ cod]
Split, 10

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

14 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]]
E Spec, 13

15 Set'(gra)
Split, 14

16 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]]
Split, 14

17 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]]]
Function

18 ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]]]
U Spec, 17

19 ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]]]
U Spec, 18

20 Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]]
U Spec, 19

21 Set(dom) & Set(cod) & Set'(gra)
Join, 8, 15

22 ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]
Detach, 20, 21

252 ~~[ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]]
5 Conclusion, 23

253 ALL(a1):ALL(b):[(a1,b) @ gra => a1 @ dom & b @ cod]
& ALL(a1):[a1 @ dom => EXIST(b):[b @ cod & (a1,b) @ gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 @ dom & b1 @ cod & b2 @ cod
=> [(a1,b1) @ gra & (a1,b2) @ gra => b1=b2]]
Rem DNeg, 252

254 EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [fun(a1)=b <=> (a1,b) @ gra]]]
Detach, 22, 253

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

256 Function(h,dom,cod)
Split, 255

257 ALL(a1):ALL(b):[a1 @ dom & b @ cod
=> [h(a1)=b <=> (a1,b) @ gra]]
Split, 255

307 ~[h @ dom & h(h)=1]
5 Conclusion, 258

388 ~[h @ dom & ~h(h)=1]
5 Conclusion, 308

402 ~h @ dom
5 Conclusion, 389

-------------------------- end proof, collapsed view -----------------------------

Mild Shock schrieb am Mittwoch, 23. August 2023 um 07:36:54 UTC+2:
> There is nothing wrong with your function axioms. You are
> on the wrong track. Grelling's antinomy is about this notion:
> the word "heterological", meaning "inapplicable to itself"
> https://en.wikipedia.org/wiki/Grelling%E2%80%93Nelson_paradox
> So can we construct the adjective "heterological" in DC Proof?
> If yes, we will arrive at a contradiction.
> Dan Christensen schrieb am Mittwoch, 23. August 2023 um 07:21:04 UTC+2:
> > On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> > > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> > >
> > > > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > > >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > > >>
> > > >> > Functions f and g are comparable only if they have the same domain
> > > >> > and codomain.
> > > >>
> > > >> Anyone except crank DC knows that this is nonsense.
> > > >
> > > > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > > > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > > > if and only if f(x) = g(x) for all x ∈ X. "
> > > > ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
> > > Tao does not support your claim. For example (from the same book):
> > >
> > > "... the two functions f and g are not considered the same function,
> > > f =/= g, because they have different domains."
> > >
> > Some context:
> >
> > "Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
> > --p. 218
> >
> > First, it would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of the formal definition of the equality of functions given here.
> >
> > Also, since the above mentioned functions f and g do not have the same domains, the above definition of function equality cannot be applied to determine if they are equal. In other words, f and g are not considered the same function because they have different domains. The insertion of "f =/= g" is admittedly puzzling. Though it is completely unnecessary, it can certainly not be seen as a repudiation of the above definition.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, August 23, 2023 at 7:21:04 AM UTC+2, Dan Christensen wrote:
> On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
> > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >
> > > On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
> > >> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
> > >> >
> > >> > Functions f and g are comparable only if they have the same domain and codomain.
> > >> >
> > >> Anyone except crank DC knows that this is nonsense.
> > >
> > > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > > g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
> > > if and only if f(x) = g(x) for all x ∈ X. " ---Terence Tao, "Analysis I," p.51
> > >
> > Tao does not support your claim. For example (from the same book):
> >
> > "... the two functions f and g are not considered the same function,
> > f =/= g, because they have different domains."
> >
> <bla bla bla>

"Cranks characteristically dismiss all evidence or arguments which contradict their own unconventional beliefs, making any rational debate a futile task and rendering them impervious to facts, evidence, and rational inference.." (Wikipedia)

Maybe we can squeeze the lemon, if we change the graph
of the Grelling function, from this here:

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

To this here:

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

This makes the definition side of the Grelling function
independent of the given and cod for the Grelling function.
So we would get graphs gra1, gra2, gra3, etc.. for

dom1, dom2, dom3, etc.. and they would be commulative, if the
domains are commulative, i.e. dom1 ⊆ dom2 ⊆ dom3 ⊆ etc..
I guess this is also the intention and some crucial ingredient

of Alonzo Church's paper, that he decouples the "heterological"
judgement from the domain of the heterological function.

Mild Shock schrieb am Mittwoch, 23. August 2023 um 09:02:11 UTC+2:
> Ok, this is a quite long proof, using Function Axiom
> and Function Equality twice, making the Grelling function
> set like. It bails out with ~h e dom, very similar like what
>
> Dan Christen found in his "Generalized Drinker Paradox" nonsense,
> when he found that every set has an outside element:
>
> 402 ~h @ dom
> 5 Conclusion, 389
>
> So when we would assume that h e dom, we would
> get a contradiction. Was thinking about using Dana Scotts
> trick, to provoke a contradiction. Not yet sure. Because
>
> we have "dom" arbitrary, not really specified, we could
> envision a kind of chasing game.

The Alonzo Church decoupling has the advantage that we can use
x @ dom, and therefore apply the built-in axioms of DC Proof, such as
Function Equality etc.. etc.. Without the decoupling we would get something

like the following. Namely, and the self application is immediately seen:

13 EXIST(gra):[Set'(gra) & ALL(x):ALL(y):[(x,y) @ gra <=>
(x,y) @ rel & ~x(x)=1] <=> y=1]]]

We can redo our initial Grelling Antinomy with such as short definition
as well. We immediately get the Liar Paradox, now the Grelling
Antinomy is only two lines:

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

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

Discussion of the Liar Paradox has already provided proof templates
to show that p <=> ~p is determinate false, or that it is a paradoxical
assumption. Anway we can derive p & ~p from it.

LoL

Mild Shock schrieb am Mittwoch, 23. August 2023 um 14:49:15 UTC+2:
> Maybe we can squeeze the lemon, if we change the graph
> of the Grelling function, from this here:
> 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
> To this here:
> 13 EXIST(gra):[Set'(gra) & ALL(x):ALL(y):[(x,y) @ gra <=> (x,y) @ rel &
> [EXIST(dom):EXIST(cod):EXIST(fun):[Function(fun,dom,cod) & ALL(a):[a @ dom => x(a)=fun(a)] &
> ~[x @ dom & fun(x)=1]] <=> y=1]]]
> Subset, 11
> This makes the definition side of the Grelling function
> independent of the given and cod for the Grelling function.
> So we would get graphs gra1, gra2, gra3, etc.. for
>
> dom1, dom2, dom3, etc.. and they would be commulative, if the
> domains are commulative, i.e. dom1 ⊆ dom2 ⊆ dom3 ⊆ etc..
> I guess this is also the intention and some crucial ingredient
>
> of Alonzo Church's paper, that he decouples the "heterological"
> judgement from the domain of the heterological function.
> Mild Shock schrieb am Mittwoch, 23. August 2023 um 09:02:11 UTC+2:
> > Ok, this is a quite long proof, using Function Axiom
> > and Function Equality twice, making the Grelling function
> > set like. It bails out with ~h e dom, very similar like what
> >
> > Dan Christen found in his "Generalized Drinker Paradox" nonsense,
> > when he found that every set has an outside element:
> >
> > 402 ~h @ dom
> > 5 Conclusion, 389
> >
> > So when we would assume that h e dom, we would
> > get a contradiction. Was thinking about using Dana Scotts
> > trick, to provoke a contradiction. Not yet sure. Because
> >
> > we have "dom" arbitrary, not really specified, we could
> > envision a kind of chasing game.