AmateurGate: DC Proof is subject to Grelling's antinomy

[Mild Shock]

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

[Mild Shock]

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

[Dan Christensen]

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

[Mild Shock]

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

[Mild Shock]

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

[Dan Christensen]

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

[Mild Shock]

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]

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

[Mild Shock]

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.

[Mild Shock]

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]

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.

[Fritz Feldhase]

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

[Dan Christensen]

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

"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?)

[Fritz Feldhase]

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.

[Dan Christensen]

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

[Ben Bacarisse]

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

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.

[Ross Finlayson]

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.

[Dan Christensen]

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.

[Mild Shock]

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.

[Mild Shock]

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

[Fritz Feldhase]

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)

[Mild Shock]

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]

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]

But the Alonzo Church decoupling doesn't let dom be completely
free. In Russell types there are levels. So he can distinguish different
heterological predicates depending on the level.

And then his conclusion is that in the presence of a heterological
predicate, Russell types are not anymore polymorphic. We have
found sentences that behave one way below some level and

the other way when above some level:

"The resolution of the antinomy by ramified type theory consists
not merely in the fact that, after restoration of the level indicators,
theorems (6)-(8) are no longer a contradiction, but also in that the
question "Is the propositional form het^k(x) autological or heterological?"
can now be answered: namely it is (by (6)) autological at all levels =< k,
and it is (by (7)) heterological at all levels > k."
https://www.jstor.org/stable/2272393

[Ross Finlayson]

Hmm, you seem to be exploring many new, transcendental concepts,
it's laudable, now that you've heard of class/set distinction yet though
that they're defined by complementary relations, you're considering
relations like Russell's versus Grelling's and Russell versus Grelling,
and getting into what's lower order one way is higher the other, and
vice-versa, soon maybe you'll start to appreciate the notion of the extra-ordinary,
and find it all too clear that it was first transcendental, and that there are
the complementary concepts of the rulial about a natural continuum, where
then perhaps you'll at a "the logic" of the elements of a universe of logical
objects, itself a logical object, cultivating your mental reasoning faculty's
object-sense, to where you may arrive at counting your fingers, and knowing
there's a difference between numbering and counting, courtesy object-sense
and a number-sense, and then be able to relay and communicate this to yourself
in a little note for later, establishing a sort of word-sense, and a fine word soup.


Then maybe you'll start to appreciate what was the non-standard about the
infinite and the continuous and the infinitesimals, in quite a standard way,
resulting an ability to make cognizant what is apeiron, and start to think about
how there are models of arithmetic, at all.

So, pointing out to yourself that paradox must be resolved, in the logical,
meaning way above the mundane discourse of the non-logical, that in the
logical, paradox is somehow resolved, then maybe you'll arrive at a true
sense of a true sense of a true truth and come to understand what what
were your "logical" axioms were either already so according to natural relations
or are simply stipulations making a rulial for essentially a convenience.

[Mild Shock]

Ever heard of this person you moron?

Dmitry Mirimanoff (1861, Russia – 1945, Switzerland)
https://en.wikipedia.org/wiki/Dmitry_Mirimanoff#Set_theory

Ross Boy had a further herpes blister burst when he wrote:
> vice-versa, soon maybe you'll start to appreciate the notion of the extra-ordinary,

Rossy Boy posts contain 50% utter nonsense, and 50% trying
to impress people by using the word extra ordinary. Listen you
freaking idiot, the result. Maybe it can be extended to full regularity:

Mild Shock schrieb am Mittwoch, 23. August 2023 um 09:02:11 UTC+2:
> 402 ~h @ dom
> 5 Conclusion, 389

https://groups.google.com/g/sci.logic/c/TaIENB54MNQ/m/fhxIPrByAwAJ

Its quite interesting that Dan Christensens framework DC Proof
implies certain regularity, although he has not the regularity
axiom from set theory explicitly in his framework.

The result excludes extra-ordinary sets in as far, as it excludes at least
extra ordinary functions, that would have themselves in the domain.
By extra oridnary sets we usually refer to sets which were named after

Dmitry Mirimanoff, Russian Swiss mathematician, who published
about it from 1917 on. Extra ordinary is just a french variant of
irregular, because "regular" becomes "ordinaire" in french.

[Mild Shock]

BTW: Peter Aczel died, R.I.P., he worked in the extra ordinary:

Peter Aczel (31 October 1941 – **1 August 2023**)
https://en.wikipedia.org/wiki/Peter_Aczel

Well the present proof does not exclude all functions f,
where f e dom(f). But the "heterological" function h cannot
exist if we also assume h e dom(h). Without h e dom(h), this

makes the function incapable to be applied to itself, and hence
incapable of provoking the Grelling antinomy. At least in the current
framework of DC Proof the Grelling antinomy with a set like h cannot

be obtained anymore. Since we proved ~h e dom, and therefore

We cannot derive anymore:

/* Not Derivable when h is set like */
43 h(h)=1 & ~h(h)=1
Join, 28, 42

We can only derive, which then leads to ~h e dom:

/* Only Derivable when h is set like */

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

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

But maybe the proof ideas can be picked up, and it can be
shown that all functions f e dom(f) are excluded in the DC Proof
framework, or even that all irregular sets are excluded in DC Proof.

I don't know. Maybe it is also the case that somehow by accident
DC Proof only excludes the "heterological" function h and not other
functions. Functions that can be applied to themselves are

important in computer science, and the work by Lambek & P. Scott,
and the work by D. Scott give also positive answers that these
extra ordinary sets might exist in certain frameworks.

[Fritz Feldhase]

On Thursday, August 24, 2023 at 11:57:50 AM UTC+2, Mild Shock wrote:

> BTW: Peter Aczel died, R.I.P., he worked in the extra ordinary:
>
> Peter Aczel (31 October 1941 – **1 August 2023**)
> https://en.wikipedia.org/wiki/Peter_Aczel

Oh.

> Well the present proof does not exclude all functions f, where f e dom(f).

Some days ago I posted the folllowing in sci.math:

--------------------------------------------------------------------------------------------

It can't be in ZFC (and/or similar set theories adopting the axiom of foundation), but it might very well be possible in the context of some other set theories.

Actually, it's possible in combinatory logic (CL):

"it is remarkable that pure untyped CL does not exclude the self-application of functions. Moreover, its mathematical models showed that a theory in which functions can become their own arguments is completely sensible, in addition to being consistent (what was established earlier using proof theoretic methods)."

https://plato.stanford.edu/entries/logic-combinatory/

[Mild Shock]

Yep, you find it also in Lambek & P.Scott, and in D.Scott.
So is DC Proof a good tool for computer science, if

~h e dom? Or maybe a further exercise, can we define
h in combinatory logic? What would happen if we transpose

a model of this to DC Proof, how would this then not give ~h e dom?

[Mild Shock]

One answer has to do with ideas from intuitionistic/constructive
logic, which does not accept the law of excluded middle, i.e. P v ~P.
So basically we might do something where:

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

is not a contradiction, in combinatory logic and other logics, for
example a logic using lambda expression, an expression h(h) might
turn out to be non-normalizing, therefore h(h)=1 might fail,

at the same time with ~h(h)=1 might fail. Since P v ~P is rejected
h(h)=1 failure does not imply ~h(h)=1 succeess, so they might
simultaneously fail, make the above non-contradictory.

Otherwise, instead of using intuitionistic/constructive logic,
you could also be more careful inside classical logic, and model
equality (=)/2 and appartness (#)/1 and the get that this:

h(h)=1 & h(h)#1

is not necessarely contradictory, for h(h) non-normalizing.

[Julio Di Egidio]

On Thursday, 24 August 2023 at 19:17:04 UTC+2, Mild Shock wrote:

> One answer has to do with ideas from intuitionistic/constructive
> logic, which does not accept the law of excluded middle, i.e. P v ~P.

10 months of writing bullshit about this stuff and you
still don't get it: assuming LEM is known to be consistent
with *constructive* logic.

Julio

[Mild Shock]

You didn't pay attention, unlike DC Proof, which allows
the formation of h(h), Coq doesn't allow the formation
h(h), unless it has some type A = A -> B.

Coq usually has the typing rule:

x : A y : A -> B
--------------------------------------
x(y) : B

Which cannot be satisfied if x and y are the same.

On the other hand DC Proof doesn't have any typing rules.
This means one is free to form h(h) in DC Proof. And the
shortest proof of the Grelling Antinomy is:

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

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

Try doing the same in Coq. Already postulating the definition
of the heterological function h(_) is not accepted in Coq. Unless
you have some type A = A -> B.

[Mild Shock]

I tried to find some Git repository or some paper that
shows a formalization of the Grelling paradox in Coq
or in Isabelle/HOL, but this was to no avail yet.

On the other hand, for example a Russell Paradox
proof is readily found in the Isabelle/HOL proof archive.
For example I find:

lemma UNIV_is_not_in_ZF
https://search.isabelle.in.tum.de/#details/default_Isabelle2022_AFP2022/HOL-ZF.HOLZF.20314.20849

You find also automated proofs in Isabelle/HOL that
have no manual steps. Some tactics can prove the
Russell Paradox automatically. Quite amazing!

Then Isabelle/HOL automated proofs archive has some
PLM Paradox, a Cantor Paradox and a Birthday Paradox.
But I didn't find a Grelling Paradox yet.

[Ross Finlayson]

Though, you can make non-binary terms or partial attributes,
or make for the temporal, i.e. what varies, in the constructive,
where LEM/TND only applies where it applies. I.e. relations are
elementary and predicates are derivative and not all are binary.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

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

Yes, I omitted all that because it about a carelessness that has nothing
to with the whether two function are "incomparable" as far as equality
is concerned.

--
Ben.

[Dan Christensen]

Your motives for your omissions are immaterial. You should know that the intellectual shortcuts that are often used in informal arguments in no way invalidates the formal definition of functional equality given by Terence Tao here.

[Ross Finlayson]

The "foolish hobgoblins" quote is often taken out of context.
(I.e. in the extended context it says "consistency is important",
while in the usual quoted section it says "foolish inconsistency
is a hobgoblin". A hobgoblin is an approximately two hit dice
heavy orc, where the goblin is one small hit die and orc one large.)

As long as he's defining his expressions in the language of arithmetic,
then defining domains either side the image, then he should define the
character of the algebra, what topologies are in effect, whether various
number-theoretic conjectures hold, whether various set-theoretic conjectures
hold, which makes for function theory and topology having that the functions
and the topologies are fungible in the sense that according to various other
theories of the objects like number theory and geometry of course and usual
arithmetic and usual algebras and usual laws of large numbers and usual
definitions of continuous functions and so on, what I'm saying is that you
have a loose and underdefined definition of function that you've found
laying around and picked up without working it up from all the principles.


Or, uh, you missed a spot there. (And the rest, also.)

Over time function theory is about the most let out
of the underdefined, and topology the one where
most the countexamples are put.

[Ross Finlayson]

Some functions are sometimes called mappings.

A usual notion of a function is a set of ordered pairs from domain to range,
it's easier to formalize this way and is a subset of the Cartesian product of
the domain and range, which is the function that way of each of the members
of the domain to each of the members of the range, there's a general notion
that functions have a left-hand-side and a right-hand-side, but more generally
they're just called image and co-image or domain and co-domain or images.

The usual notion of the set of ordered pairs (domain, range) is a quite usual
formalism because all the elements are elementary in terms of being sets
like point-sets.

It's a very usual notion of a function or mapping that there are 1-1 functions
and what they do is _carry_ from the domain to the range, especially continuous
functions, which have that any arbitrary region of the domain carries to a region
of the range, and, a sub-section of that carries to the corresponding sub-section
of the function/mapping/correspondence and similarly concatenations also so
carry. What today is called a continuous function is often enough what classically
was called a function and the most usual working set of those is what are called
classical functions, in a world with continuous functions and also discontinuous
functions which though for example have cases of functions both continuous
and discontinuous according to various things like Dirichlet problem, and
Poincare's rough functions.

Then, these notions of functions and mappings and correspondences, as written
as ordered pairs (if not, each written as there are infinitely many, written as
expressions in the sets of same), also see that there are some functions or
correspondences or mappings that aren't Cartesian, my favorite example of
course being the natural/unit equivalency function, which is non-Cartesian,
and stands out among objects that behave like functions, as that its range is
a continuous domain while its domain is the natural integers, but it can't be
taken apart like usual Cartesian functions, instead that its properties as a mapping
and the relations between its elements, and their relations to each other in terms
of being a continuous domain, are a special sort of unique and central: function,
in mathematics.

Various conjectures in number theory are yet undecided, and also, some may be:
undecideable, or rather that either there are higher axioms of the usual sort of
notions of deciding them, or, there are deconstructive accounts of arithmetic
and the nature of continuity like the Dirichlet problem and Poincare's rough plane,
that basically various laws of large numbers define what are these functions,
variously, though they'd have the same expressions in the language of arithmetic.

So, functions, or, families of relations that relate LHS-RHS domain-codomain,
have that relations are fundamental and as well that sometimes, the transfer
principle applies, and it's only about relating contiguous regions of the domains,
where contiguous suffices to include continuous, which is usually vice-versa,
what "defines" the functions.

Then, it's usual that for any function like "a function R -> R", that usually enough,
any subset of the domain maps to a subset of the range, for 1-1 functions or mappings.
Ditto, any usual extension of the domain brings along without further qualification,
all the semantics according to the language the expression in arithmetic is, in.

So, carefully distinguishing a function as including its domain and range and its
expression or the framework what establishes its mapping, is quite a usual enough
thing, but, there are higher (and lower) mathematics where it either needs be _further_
qualified, or, that it _excludes_ some what "are" mappings or correspondences or functions.

That said it's usually acceptable that the expression itself in the variables in the language
of arithmetic is the function, given that arithmetic usually has very well-known domains,
and that various laws of large numbers and various topologies and various corresponding
measure-theoretic aspects and as about various definitions of continuity and discontinuity
in functions and in the domains, that a more careful definition of reducing it to bounds,
then is just to make it easier to write things like "my Fourier-style analysis shows this
windows and boxes down to these bounds so these functions are the same", in bounds.

So, functions and quantities are in a sense sort of overloaded, because mathematics has
various ways of looking at what _are_ the elementary elements at all, and there are various
theories like arithmetic and the objects of arithmetic, various algebras and their objects,
various correspondences as domains, various topologies, usually pretty much one geometry,
but many various style methods in the numerical and algebraic, which result why what are
elements in one of these sub-fields are approximations or "only after completions", ..., in
others, so that if you actually care about rigorous definition of these terms in these other
terms, that such definitions are made stated, and, as part of entire derivations.

It does help keep most simple things simple and some otherwise capricious
things to make for writing things like "this limit is this sum" and so on. I.e.,
it's for matters of extensionality in systems of bounds, and otherwise wouldn't
need such qualification.

So, it's for keeping various simple things correct, not, "the end-all be-all".

In mathematics the definition of "function" has seen changes, but as elementary,
it is relations, and carries, for example, transfer principle correspondences.

[Fritz Feldhase]

On Friday, August 25, 2023 at 4:31:43 AM UTC+2, Dan Christensen wrote:

> Your motives <bla>

Yes, we know that you are a crank.

Hint: "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)

[Fritz Feldhase]

On Friday, August 25, 2023 at 5:54:56 AM UTC+2, Ross Finlayson wrote:

> [...] functions are sometimes called mappings.

Indeed!

> A usual notion of a function is a set of ordered pairs from domain to range [...]

Yeah, especically in the context of set theory.

> The [...] notion of the set of ordered pairs [...] a quite usual formalism [...]

Yeah, especically in the context of set theory.

> In mathematics the definition of "function" has seen changes

Indeed!

Sometimes a function is defined as a tripel:

<graph of the function, domain of the function, codomain of the function>

In this case the function is NOT just a "set of ordered pairs". [...]

[Ross Finlayson]

One thing about set theory is that the idea that it's fundamental then makes that
usual attachments of usual relations of domains of usual kinds are not included
in the "utterly general" definition of function out of the Cartesian from the "utterly
general" definition of the members of the domains their equivalence classes their
values their sets.

So in set theory that triple is "just a set of ordered pairs" just like that triple is
"just a triple of an expression relating two domains".

They're equi-interpretable insofar as "the elements of the domains are distinct
and distinguishable as elements of sets" and "the expression relates the elements
of the sets by a relation between each element of the model of the mapping",
it's the point of descriptive set theory that's so. All the "analytical character"
of the function is still way up above the point-set domains usually as according
to geometry and definitions and derivations in real analysis.

I.e., it's generally held in set theory that "it's not, not so", that the model as sets
is no more spare than the model as relations usually in the language of arithmetic
between domains usually in the language of numbers, or for functions and type theories
more generally where functions and functors work on "objects" in programming languages,
here though usually in the language of arithmetic the domains of numbers.

Then as above there are reasons _why_ that whether a set of ordered pairs or an
expression by itself in the language of arithmetic with free variables or even just a constant,
or a triple <expr, lhs, rhs>, there are reasons _why_ even none of those are the "complete"
definition of function because there are implicits about what is basically non-standard,
about conjectures in large numbers and the continuous/discontinuous and so on as
examples.

For most people, any old expression in the language of arithmetic is a function,
a dependent variable of the independent variables.

[Ross Finlayson]

Functions are elementary in function theory, in mathematics many or most kinds of
objects are functions ascribed specific character and given specific names. (It's
the equivalence classes, it's the descriptive set theory, it's the monoids.)

It's a usual exercise in thinking that the universe, the physical universe, is infinite,
because functions between objects are also objects, as are those ad infinitum.

This way then for somebody like DesCartes the physics is some fundamentally "vortices".
It's a continuum mechanics.

[Mild Shock]

So while a short form of Grellings Antinomy very quickly arrives
at a Liar Paradox of the form p <=> ~p, for Russells Paradox it takes
a little bit more steps to arrive at p <=> ~p, but it can be also done.

So how are these Paradoxes "resolved"? Where is a Universal Set
assumption in Grellings Antinomy? Do we resolve the resulting Liar
Paradox, or do we do something before the Liar Paradox?

Why can the Grellings Antinomy not be formulated in Coq?
Compare the short form of Grellings Antinomy, it gives p <=> ~p:

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

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

With Russells Paradoxes, not the Antinomy with Naive Set
Comprehension, but the Paradox with Non-Naive Set Comprehension
plus the Universal Set Assumption, gives again the Liar Paradox:

26 v @ v <=> ~v @ v
Iff-And, 25

The proof is a modification of https://www.dcproof.com/UniversalSet.htm:

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

1 Set(u) & ALL(a):a @ u
Premise

2 Set(u)
Split, 1

3 ALL(a):a @ u
Split, 1

4 EXIST(s):[Set(s) & ALL(a):[a @ s <=> a @ u & ~a @ a]]
Subset, 2

5 Set(v) & ALL(a):[a @ v <=> a @ u & ~a @ a]
E Spec, 4

6 Set(v)
Split, 5

7 ALL(a):[a @ v <=> a @ u & ~a @ a]
Split, 5

8 v @ v <=> v @ u & ~v @ v
U Spec, 7

9 v @ v
Premise

10 [v @ v => v @ u & ~v @ v] & [v @ u & ~v @ v => v @ v]
Iff-And, 8

11 v @ v => v @ u & ~v @ v
Split, 10

12 v @ u & ~v @ v => v @ v
Split, 10

13 v @ u & ~v @ v
Detach, 11, 9

14 v @ u
Split, 13

15 ~v @ v
Split, 13

16 v @ v => ~v @ v
4 Conclusion, 9

17 ~v @ v
Premise

18 [v @ v => v @ u & ~v @ v] & [v @ u & ~v @ v => v @ v]
Iff-And, 8

19 v @ v => v @ u & ~v @ v
Split, 18

20 v @ u & ~v @ v => v @ v
Split, 18

21 v @ u
U Spec, 3

22 v @ u & ~v @ v
Join, 21, 17

23 v @ v
Detach, 20, 22

24 ~v @ v => v @ v
4 Conclusion, 17

25 [v @ v => ~v @ v] & [~v @ v => v @ v]
Join, 16, 24

26 v @ v <=> ~v @ v
Iff-And, 25

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

[Mild Shock]

Oh Rossy Boy I hope you don't have the same fate as this poor boy:

A 16-year-old boy died after masturbating 42 times
without stopping in Rubiato town, in Goiás region, Brazil.
https://www.snl24.com/dailysun/news/man-dies-after-too-much-wanking-20210828

Its quite observable that your frequency of nonsense posts
increased. And recently you moved from from your pet Crank Subject
of some space filling curve to set theory and liar paradoxes.

So the hot air balloon shows quite some ascent, will it soon burst?

[Dan Christensen]

On Thursday, August 24, 2023 at 3:14:30 PM UTC-4, Mild Shock wrote:

[snip]

> On the other hand DC Proof doesn't have any typing rules.
> This means one is free to form h(h) in DC Proof. And the
> shortest proof of the Grelling Antinomy is:
> 1 ALL(v):[h(v)=1 <=> ~v(v)=1]
> Axiom
>
> 2 h(h)=1 <=> ~h(h)=1
> U Spec, 1

So, your axiom leads directly to a contradiction. Hmmm...

Change the axiom to a premise to obtain:

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

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

3. ~EXIST(h):EXIST(1):ALL(v):[h(v)=1 <=> ~v(v)=1]
Conclusion, 1

A proof by contradiction.

You really have to be careful when formulating axioms. You even could have P & ~P as an axiom. Then, of course, anything goes!

1. P & ~P
Axiom

2. P
Split, 1

3. ~P
Split, 1

4. ~Q
Premise

5. P & ~P
Join, 2, 3

6. ~~Q
Conclusion, 4

7. Q
Rem DNeg, 6

Anything goes with that axiom!

Changing that axiom to a premise and we obtain:

1. P & ~P
Premise

2. P
Split, 1

3. ~P
Split, 1

4. ~Q
Premise

5. P & ~P
Join, 2, 3

6. ~~Q
Conclusion, 4

7. Q
Rem DNeg, 6

8. P & ~P => Q
Conclusion, 1

The Principle of Explosion! Note that this does NOT mean that Q is true. Or that it is false.

[Ross Finlayson]

Wow, that's hilarious. Maybe you should consider a career as a stage comedian.
Then people could pay to throw eggs and tomatoes at you. And laugh at you.

Oops, sorry about that, my sarcasm slipped out for a second.

Jocelyn Elders was a Surgeon General for a brief time in the '90's. She suggested that
for example the war on drugs did more harm than good, then for example that
masturbation was part of safe sex. It's like they say, "99% do, the rest lie".
It's like they say, "don't do drugs". I've had 100 lovers, who loved me, so,
use it or lose it, as they say. Don't do anything you wouldn't do. "Get some."

As it is, though, it's hard to figure a simpler medium to reach more people
with such high-minded ideas.

Really, I feel very lucky to have been the subject of so many's affections.



There are no "paradoxes".

[Mild Shock]

Since we didn't post a proof that wasn't using function
equality, I started adoption Culios proof in Coq. Now I saw that
it could be non-constructive, since it uses tauto. But have to

check what tauto does. Culios proof reads:

> (* [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.

So it starts with unfold, so we can anyway throw away the
definitions and try directly a proof of the following. Unfortunately
my only version does have <=> so lets do it with two =>:

?- gentzen(∀h: ¬ (∀w: ((¬φ(w,w) →φ(h,w))∧(φ(h,w)→ ¬φ(w,w) ))), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example52/package.html

This is the proof it shows me. It uses Reductio, so its non-
constructive. Maybe can turn it into a constructive proof?

1 ∀w:((¬φ(w, w) → φ(u, w)) ∧ (φ(u, w) → ¬φ(w, w)))
Premise
2 (¬φ(u, u) → φ(u, u)) ∧ (φ(u, u) → ¬φ(u, u))
U Spec 1
3 φ(u, u) → ¬φ(u, u)
Split Right 2
4 ¬φ(u, u) → φ(u, u)
Split Left 2
5 ¬φ(u, u)
Premise
6 φ(u, u)
Premise
7 ⊥
Detach 6,5
8 ¬φ(u, u)
▲ Conclusion 6,7
9 φ(u, u)
Detach 8,4/
10 ⊥
Detach 9,5
11 φ(u, u)
▲ Reductio 5,10
12 ¬φ(u, u)
Detach 11,3
13 ¬φ(u, u)
Premise
14 φ(u, u)
Premise
15 ⊥
Detach 14,13
16 ¬φ(u, u)
▲ Conclusion 14,15
17 φ(u, u)
Detach 16,4
18 ⊥
Detach 17,13
19 φ(u, u)
▲ Reductio 13,18
20 ⊥
Detach 19,12
21 ¬ ∀w:((¬φ(w, w) → φ(u, w)) ∧ (φ(u, w) → ¬φ(w, w)))
▲ Conclusion 1,20
22 ∀h: ¬ ∀w:((¬φ(w, w) → φ(h, w)) ∧ (φ(h, w) → ¬φ(w, w)))
U Gen 21

[Mild Shock]

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

[Mild Shock]

Come look and see, how Rossy Boy looses his marbles:

Ross podcasts talks about mathematics,
physics, science, logic, philosophy
https://groups.google.com/g/sci.math/c/N1YgkTqERJc

"Archimedes Plutonium and Rossy Boy should be thrown in jail
for their willful criminal behavior. The criminals Archimedes
Plutonium and Rossy Boy all the times posts people
name lists together with hate speach about these people.

It is highly likely Archimedes Plutonium and Rossy Boy are
psychos. Archimedes Plutonium and Rossy Boy belong in prison
not on usenet for their mind is complete hate hate hate.
Put these creeps in jail and throw away the keys."

LoL

Ross Finlayson schrieb:

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

[Ross Finlayson]

Nowadays "classical Comte's Boole's logical positivism's Russell's syllogistic", logic,
is read out with its true name, "classical quasi-modal logic".

It's sort of a matter of unmasking its contradiction in terms and showing its true face.

Which looks upside-down, clown.