I can use your function axiom, and dom'={0,1}, cod'={0,1}
and gra={(0,0),(1,1)} and show that fun exists.
And then prove, a contradiction:

P(fun,1) & ~P(fun,1)

Just use your silly definition:

ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) &
ALL(a):[a in dom => fun(a) in cod]
=> [P(fun,elt) <=> elt in dom]]

One time with dom={0,1} and cod={0,1}, and another
time with dom={0} and cod={0}, and then join the
results. Here is a proof:

104 P(fun,1) & ~P(fun,1)
Join, 103, 45

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

1 ~1=0
Axiom

2 Set(s0)
Axiom

3 ALL(x):[x ε s0 <=> x=0]
Axiom

4 Set(s01)
Axiom

5 ALL(x):[x ε s01 <=> x=0 | x=1]
Axiom

6 ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a ε dom => fun(a) ε cod]
=> [P(fun,elt) <=> elt ε dom]]
Axiom

7 fun(0)=0
Axiom

8 fun(1)=1
Axiom

9 ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a ε dom => fun(a) ε cod]
=> [P(fun,elt) <=> elt ε dom]]
U Spec, 6

10 ALL(cod):ALL(elt):[Set(s0) & Set(cod) & ALL(a):[a ε s0 => fun(a) ε cod]
=> [P(fun,elt) <=> elt ε s0]]
U Spec, 9

11 ALL(elt):[Set(s0) & Set(s0) & ALL(a):[a ε s0 => fun(a) ε s0]
=> [P(fun,elt) <=> elt ε s0]]
U Spec, 10

12 Set(s0) & Set(s0) & ALL(a):[a ε s0 => fun(a) ε s0]
=> [P(fun,1) <=> 1 ε s0]
U Spec, 11

13 ~ALL(a):[a ε s0 => fun(a) ε s0]
Premise

14 ~~EXIST(a):~[a ε s0 => fun(a) ε s0]
Quant, 13

15 EXIST(a):~[a ε s0 => fun(a) ε s0]
Rem DNeg, 14

16 ~[u ε s0 => fun(u) ε s0]
E Spec, 15

17 ~~[u ε s0 & ~fun(u) ε s0]
Imply-And, 16

18 u ε s0 & ~fun(u) ε s0
Rem DNeg, 17

19 u ε s0
Split, 18

20 ~fun(u) ε s0
Split, 18

21 u ε s0 <=> u=0
U Spec, 3

22 [u ε s0 => u=0] & [u=0 => u ε s0]
Iff-And, 21

23 u ε s0 => u=0
Split, 22

24 u=0 => u ε s0
Split, 22

25 u=0
Detach, 23, 19

26 ~fun(0) ε s0
Substitute, 25, 20

27 ~0 ε s0
Substitute, 7, 26

28 ~u ε s0
Substitute, 25, 27

29 u ε s0 & ~u ε s0
Join, 19, 28

30 ~~ALL(a):[a ε s0 => fun(a) ε s0]
Conclusion, 13

31 ALL(a):[a ε s0 => fun(a) ε s0]
Rem DNeg, 30

32 Set(s0) & Set(s0)
Join, 2, 2

33 Set(s0) & Set(s0)
& ALL(a):[a ε s0 => fun(a) ε s0]
Join, 32, 31

34 P(fun,1) <=> 1 ε s0
Detach, 12, 33

35 1 ε s0 <=> 1=0
U Spec, 3

36 [1 ε s0 => 1=0] & [1=0 => 1 ε s0]
Iff-And, 35

37 1 ε s0 => 1=0
Split, 36

38 1=0 => 1 ε s0
Split, 36

39 [P(fun,1) => 1 ε s0] & [1 ε s0 => P(fun,1)]
Iff-And, 34

40 P(fun,1) => 1 ε s0
Split, 39

41 1 ε s0 => P(fun,1)
Split, 39

42 ~1 ε s0 => ~P(fun,1)
Contra, 40

43 ~1=0 => ~1 ε s0
Contra, 37

44 ~1 ε s0
Detach, 43, 1

45 ~P(fun,1)
Detach, 42, 44

46 ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a ε dom => fun(a) ε cod]
=> [P(fun,elt) <=> elt ε dom]]
U Spec, 6

47 ALL(cod):ALL(elt):[Set(s01) & Set(cod) & ALL(a):[a ε s01 => fun(a) ε cod]
=> [P(fun,elt) <=> elt ε s01]]
U Spec, 46

48 ALL(elt):[Set(s01) & Set(s01) & ALL(a):[a ε s01 => fun(a) ε s01]
=> [P(fun,elt) <=> elt ε s01]]
U Spec, 47

49 Set(s01) & Set(s01) & ALL(a):[a ε s01 => fun(a) ε s01]
=> [P(fun,1) <=> 1 ε s01]
U Spec, 48

50 ~ALL(a):[a ε s01 => fun(a) ε s01]
Premise

51 ~~EXIST(a):~[a ε s01 => fun(a) ε s01]
Quant, 50

52 EXIST(a):~[a ε s01 => fun(a) ε s01]
Rem DNeg, 51

53 ~[u ε s01 => fun(u) ε s01]
E Spec, 52

54 ~~[u ε s01 & ~fun(u) ε s01]
Imply-And, 53

55 u ε s01 & ~fun(u) ε s01
Rem DNeg, 54

56 u ε s01
Split, 55

57 ~fun(u) ε s01
Split, 55

58 u ε s01 <=> u=0 | u=1
U Spec, 5

59 [u ε s01 => u=0 | u=1] & [u=0 | u=1 => u ε s01]
Iff-And, 58

60 u ε s01 => u=0 | u=1
Split, 59

61 u=0 | u=1 => u ε s01
Split, 59

62 u=0 | u=1
Detach, 60, 56

63 u=0
Premise

64 0 ε s01 <=> 0=0 | 0=1
U Spec, 5

65 [0 ε s01 => 0=0 | 0=1] & [0=0 | 0=1 => 0 ε s01]
Iff-And, 64

66 0 ε s01 => 0=0 | 0=1
Split, 65

67 0=0 | 0=1 => 0 ε s01
Split, 65

68 u=0 | 0=1 => 0 ε s01
Substitute, 63, 67

69 u=0 | 0=1
Arb Or, 63

70 0 ε s01
Detach, 68, 69

71 fun(0) ε s01
Substitute, 7, 70

72 fun(u) ε s01
Substitute, 63, 71

73 u=0 => fun(u) ε s01
Conclusion, 63

74 u=1
Premise

75 1 ε s01 <=> 1=0 | 1=1
U Spec, 5

76 [1 ε s01 => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε s01]
Iff-And, 75

77 1 ε s01 => 1=0 | 1=1
Split, 76

78 1=0 | 1=1 => 1 ε s01
Split, 76

79 1=0 | u=1 => 1 ε s01
Substitute, 74, 78

80 1=0 | u=1
Arb Or, 74

81 1 ε s01
Detach, 79, 80

82 fun(1) ε s01
Substitute, 8, 81

83 fun(u) ε s01
Substitute, 74, 82

84 u=1 => fun(u) ε s01
Conclusion, 74

85 [u=0 => fun(u) ε s01] & [u=1 => fun(u) ε s01]
Join, 73, 84

86 fun(u) ε s01
Cases, 62, 85

87 ~fun(u) ε s01 & fun(u) ε s01
Join, 57, 86

88 ~~ALL(a):[a ε s01 => fun(a) ε s01]
Conclusion, 50

89 ALL(a):[a ε s01 => fun(a) ε s01]
Rem DNeg, 88

90 Set(s01) & Set(s01)
Join, 4, 4

91 Set(s01) & Set(s01)
& ALL(a):[a ε s01 => fun(a) ε s01]
Join, 90, 89

92 P(fun,1) <=> 1 ε s01
Detach, 49, 91

93 [P(fun,1) => 1 ε s01] & [1 ε s01 => P(fun,1)]
Iff-And, 92

94 P(fun,1) => 1 ε s01
Split, 93

95 1 ε s01 => P(fun,1)
Split, 93

96 1 ε s01 <=> 1=0 | 1=1
U Spec, 5

97 [1 ε s01 => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε s01]
Iff-And, 96

98 1 ε s01 => 1=0 | 1=1
Split, 97

99 1=0 | 1=1 => 1 ε s01
Split, 97

100 1=1
Reflex

101 1=0 | 1=1
Arb Or, 100

102 1 ε s01
Detach, 99, 101

103 P(fun,1)
Detach, 95, 102

104 P(fun,1) & ~P(fun,1)
Join, 103, 45

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

Mostowski Collapse schrieb am Sonntag, 14. Mai 2023 um 01:20:07 UTC+2:
> I see a big problem with your definition, it is wrong:
> ALL(a):[a in dom => fun(a) in cod] => [P(fun,elt) <=> elt in dom]
> Where P should express that fun is defined at elt, right?
>
> Now take the following dom and cod:
>
> dom={0}, cod={0}
>
> And take the following function:
>
> fun(0)=0
> fun(1)=1
>
> Is it defined at 1?
> Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 00:56:31 UTC+2:
> > On Saturday, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > > > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > > > So how would we express a predication:
> > > > >
> > > > > P(f,x) <=> The function f is defined at the point x?
> > > > >
> > > > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> > > >
> > > > => [P(fun,elt) <=> elt in dom]]
> > > Well a binary predicate definition would only read:
> > >
> > > ALL(f):ALL(x):[P(f,x) <=> ...]
> > >
> > What is f? What is x?
> >
> > You need something a little more specific, Mr. Collapse.
> >
> > Let me guess... You want to be able to infer that P(f,x) is false is f is not a function or x has not been declared to be a set. That's not usually how things work in mathematics. In that case, P(f,x) would be indeterminate.
> >
> > Try again, Mr. Collapse.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, May 13, 2023 at 2:33:05 PM UTC-4, Dan Christensen wrote:
> On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > So how would we express a predication:
> >
> > P(f,x) <=> The function f is defined at the point x?
> >

Requires additional parameters for domain and codomain sets.

> ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
>
> => [P(fun,elt) <=> elt in dom]]

Correction:

=> [P(fun,dom, code,elt) <=> elt in dom]]

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

On Saturday, May 13, 2023 at 2:33:05 PM UTC-4, Dan Christensen wrote:
> On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > So how would we express a predication:
> >
> > P(f,x) <=> The function f is defined at the point x?
> >

Requires additional parameters for domain and codomain sets.

> ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
>
> => [P(fun,elt) <=> elt in dom]]

Correction:

=> [P(fun,dom, cod,elt) <=> elt in dom]]

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

LoL

The original task was to define P(f,x). So its impossible in DC Proof?

(P.S.: In FOL ZFC its possible, rather trivial)

Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 05:45:55 UTC+2:
> On Saturday, May 13, 2023 at 2:33:05 PM UTC-4, Dan Christensen wrote:
> > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > So how would we express a predication:
> > >
> > > P(f,x) <=> The function f is defined at the point x?
> > >
> Requires additional parameters for domain and codomain sets.
> > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> >
> > => [P(fun,elt) <=> elt in dom]]
> Correction:
>
> => [P(fun,dom, cod,elt) <=> elt in dom]]
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

I don't know how easy or difficult it would be in Coq.
It depends how you define the thingy of a partial function.

Mostowski Collapse schrieb am Sonntag, 14. Mai 2023 um 22:40:41 UTC+2:
> LoL
>
> The original task was to define P(f,x). So its impossible in DC Proof?
>
> (P.S.: In FOL ZFC its possible, rather trivial)
> Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 05:45:55 UTC+2:
> > On Saturday, May 13, 2023 at 2:33:05 PM UTC-4, Dan Christensen wrote:
> > > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > > So how would we express a predication:
> > > >
> > > > P(f,x) <=> The function f is defined at the point x?
> > > >
> > Requires additional parameters for domain and codomain sets.
> > > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> > >
> > > => [P(fun,elt) <=> elt in dom]]
> > Correction:
> >
> > => [P(fun,dom, cod,elt) <=> elt in dom]]
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > So how would we express a predication:
> > >
> > > P(f,x) <=> The function f is defined at the point x?
> > >
> > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> >

=> [P(fun,dom,cod,elt) <=> elt in dom]]

> Well a binary predicate definition would only read:
>
> ALL(f):ALL(x):[P(f,x) <=> ...]
>

Not good enough, Mr. Collapse. Maybe you didn't know, but to specify a function, you really must specify its domain and codomain sets. (See Tao)

Dan

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

Where do you need codomain for the following specification:

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 22:56:28 UTC+2:
> Dans delusional functions and the drinker paradox
> In set theory one can express undefinedness of f at x by:
> ~EXIST(y):(x,y) e f
>
> In free logic one could use instead:
> E!f(x)
https://groups.google.com/g/sci.logic/c/yxICDw_Q7-s/m/iZ3KikwvBwAJ

Why would one define:

> Ooops! Correction:
> => [P(fun,dom,cod,elt) <=> elt in dom]]

Where do you need cod?

LMAO!

Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 23:42:08 UTC+2:
> On Saturday, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:
> > Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > > So how would we express a predication:
> > > >
> > > > P(f,x) <=> The function f is defined at the point x?
> > > >
> > > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> > >
> => [P(fun,dom,cod,elt) <=> elt in dom]]
> > Well a binary predicate definition would only read:
> >
> > ALL(f):ALL(x):[P(f,x) <=> ...]
> >
> Not good enough, Mr. Collapse. Maybe you didn't know, but to specify a function, you really must specify its domain and codomain sets. (See Tao)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Well the task is to define the notion of Definedness of a function
f at a point x. By occams razor, we do not need to know the
Codomain. Or do you disaggre?

Where do you see "cod" on the right hand side "elt in dom" here:

=> [P(fun,dom,cod,elt) <=> elt in dom]]

It only says "elt in dom". No "cod" needed. There are more
notions that don't need the codomain, and some need it.
It depends on the notion:

Notion that doesn't need the codomain:
- Injectivity

Notion that does need a reference to a codomain
- Surjectivity

Got it?

Mostowski Collapse schrieb am Montag, 15. Mai 2023 um 19:47:22 UTC+2:
> Where do you need codomain for the following specification:
>
> Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 22:56:28 UTC+2:
> > Dans delusional functions and the drinker paradox
> > In set theory one can express undefinedness of f at x by:
> > ~EXIST(y):(x,y) e f
> >
> > In free logic one could use instead:
> > E!f(x)
> https://groups.google.com/g/sci.logic/c/yxICDw_Q7-s/m/iZ3KikwvBwAJ
>
> Why would one define:
>
> > Ooops! Correction:
> > => [P(fun,dom,cod,elt) <=> elt in dom]]
> Where do you need cod?
>
> LMAO!
> Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 23:42:08 UTC+2:
> > On Saturday, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:
> > > Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > > > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > > > So how would we express a predication:
> > > > >
> > > > > P(f,x) <=> The function f is defined at the point x?
> > > > >
> > > > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> > > >
> > => [P(fun,dom,cod,elt) <=> elt in dom]]
> > > Well a binary predicate definition would only read:
> > >
> > > ALL(f):ALL(x):[P(f,x) <=> ...]
> > >
> > Not good enough, Mr. Collapse. Maybe you didn't know, but to specify a function, you really must specify its domain and codomain sets. (See Tao)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Monday, May 15, 2023 at 1:47:22 PM UTC-4, Mostowski Collapse wrote:

>
> Why would one define:
>
> > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) &
> > ALL(a):[a in dom => fun(a) in cod]
> > => [Def(fun,dom,cod,elt) <=> elt in dom]]

Where Def(fun,dom,cod,elt) means that the function (fun) mapping domain (dom) to codomain (cod) is defined at elt.

Why? Because you want it to make sense.

> Where do you need cod?
>

Maybe you didn't know, but...

"In mathematics, the CODOMAIN (cod) or set of destination of a function is the set into which all of the output of the function is constrained to fall.. It is the set Y in the notation f: X → Y."
https://en.wikipedia.org/wiki/Codomain

I hope this helps.

Dan

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

On Monday, May 15, 2023 at 2:45:07 PM UTC-4, Mostowski Collapse wrote:
> Well the task is to define the notion of Definedness of a function
> f at a point x.

Have done so. Once again:

ALL(fun):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
ALL(a):[a in dom => fun(a) in cod]
=> [Def(fun,dom,cod,elt) <=> x in dom]]

Where Def(fun,dom,cod,x) means that the function (fun) mapping domain (dom) to codomain (cod) is defined at x.

By occams razor, we do not need to know the
> Codomain. Or do you disaggre?
>

"Everything should be made as simple as possible, but not simpler."
--Albert Einstein

As you discovered here, you can get some wonky results by oversimplifying and neglecting to consider key parameters in a 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 Monday, May 15, 2023 at 2:45:07 PM UTC-4, Mostowski Collapse wrote:
> Well the task is to define the notion of Definedness of a function
> f at a point x.

Have done so. Once again:

ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
ALL(a):[a in dom => f(a) in cod]
=> [Def(f,dom,cod,x) <=> x in dom]]

Where Def(f,dom,cod,x) means that a function (f) mapping domain (dom) to codomain (cod) is defined at x.

> By occams razor, we do not need to know the
> Codomain. Or do you disaggre?
>

"Everything should be made as simple as possible, but not simpler."
--Albert Einstein

As you discovered here, you can get some wonky results by oversimplifying and neglecting to consider key parameters in a definition.

Dan

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

I got the wonky result from your wonky:

> ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> ALL(a):[a in dom => f(a) in cod]
> => [Def(f,x) <=> x in dom]]

Do you indulge on the idea that this leads also to an inconsistency:

> ALL(dom):ALL(x):
> [Def(dom,x) <=> x in dom]]

If yes, how then?

LoL

Dan Christensen schrieb am Montag, 15. Mai 2023 um 21:01:49 UTC+2:
> On Monday, May 15, 2023 at 2:45:07 PM UTC-4, Mostowski Collapse wrote:
> > Well the task is to define the notion of Definedness of a function
> > f at a point x.
> Have done so. Once again:
>
> ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> ALL(a):[a in dom => f(a) in cod]
> => [Def(f,dom,cod,x) <=> x in dom]]
>
> Where Def(f,dom,cod,x) means that a function (f) mapping domain (dom) to codomain (cod) is defined at x.
> > By occams razor, we do not need to know the
> > Codomain. Or do you disaggre?
> >
> "Everything should be made as simple as possible, but not simpler."
> --Albert Einstein
>
> As you discovered here, you can get some wonky results by oversimplifying and neglecting to consider key parameters in a 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 Monday, May 15, 2023 at 4:17:58 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 15. Mai 2023 um 21:01:49 UTC+2:
> > On Monday, May 15, 2023 at 2:45:07 PM UTC-4, Mostowski Collapse wrote:
> > > Well the task is to define the notion of Definedness of a function
> > > f at a point x.
> > Have done so. Once again:
> >
> > ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> > ALL(a):[a in dom => f(a) in cod]
> > => [Def(f,dom,cod,x) <=> x in dom]]
> >
> > Where Def(f,dom,cod,x) means that a function (f) mapping domain (dom) to codomain (cod) is defined at x.
> > > By occams razor, we do not need to know the
> > > Codomain. Or do you disaggre?
> > >
> > "Everything should be made as simple as possible, but not simpler."
> > --Albert Einstein
> >
> > As you discovered here, you can get some wonky results by oversimplifying and neglecting to consider key parameters in a definition.

> I got the wonky result from your wonky:
> > ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> > ALL(a):[a in dom => f(a) in cod]
> > => [Def(f,x) <=> x in dom]]
>

Your desperation seems to be growing by the hour, Mr. Collapse. As you know, I subsequently posted the obvious correction:

ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
ALL(a):[a in dom => f(a) in cod]
=> [Def(f,dom,cod,x) <=> x in dom]] <--------- Correction here

Deal with it, Mr. Collapse.

Dan

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

But you didn't get my point that the correction is overkill.
Why would you need the parameter cod?

I wrote this here:

Mostowski Collapse schrieb am Montag, 15. Mai 2023 um 20:45:07 UTC+2:
> Where do you see "cod" on the right hand side "elt in dom" here:
> => [P(fun,dom,cod,elt) <=> elt in dom]]
> It only says "elt in dom". No "cod" needed.
https://groups.google.com/g/sci.math/c/PwyRME9DOdY/m/FVVo7YJeBgAJ

Whats wrong with you? You then used appeal to authority,
i.e. Terrence Tao would say a function comes with cod.
Well yes. And? A function my come with cod. But does

the notion "Definedness" need cod? You avoided the
question so far. Obviously it doesn't need "cod", if
you cast Definedness as "elt in dom". There is a small

chance that you would really need "cod" in the FOL/ZFC
version, if you would rephrase this:

~EXIST(y):(x,y) e f

Into this:

~EXIST(y):[y e cod & (x,y) e f]

To make the exist quantifier more bounded. But in
FOL/ZFC this is not really needed, when operating with
extensionally equivalent functions. We can define:

dom(f) := { x | EXIST(y): (x,y) e f }

Dan Christensen schrieb am Montag, 15. Mai 2023 um 22:29:19 UTC+2:
> Your desperation seems to be growing by the hour, Mr. Collapse. As you know, I subsequently posted the obvious correction:
> ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> ALL(a):[a in dom => f(a) in cod]
> => [Def(f,dom,cod,x) <=> x in dom]] <--------- Correction here
>
> Deal with it, Mr. Collapse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Anyway dream on if you think your nonsense is
compatible with Terrence Tao. In FOL/ZFC when operating
with extensionally equivalent functions, we can define:

dom(f) := { x | EXIST(y): (x,y) e f }

So every function f has a unique domain dom(f).
There is no ambiguity. With the recent DC Poop
nonsense we can not anymore prove:

104 P(fun,1) & ~P(fun,1)
Join, 103, 45

But we can now prove in DC Poop:

P(fun,s01,s01,1) & ~P(fun,s0,s0,1)

So "fun" can have differing domains s0 and s01?
Very funny. Please try again definining functions in
DC Poop. Your approach is nonsense. Also not what

Terrence Tao writes. Since Terrence Tao requires
F ⊆ X x Y. So if ~P(fun,s0,s0,1) this should also imply
~P(fun,s01,s01,1). But we can show P(fun,s01,s01,1) in DC Poop.

Your nonsense is even not compatible with Terrence Tao.

Mostowski Collapse schrieb am Dienstag, 16. Mai 2023 um 09:34:50 UTC+2:
> But you didn't get my point that the correction is overkill.
> Why would you need the parameter cod?
>
> I wrote this here:
> Mostowski Collapse schrieb am Montag, 15. Mai 2023 um 20:45:07 UTC+2:
> > Where do you see "cod" on the right hand side "elt in dom" here:
> > => [P(fun,dom,cod,elt) <=> elt in dom]]
> > It only says "elt in dom". No "cod" needed.
> https://groups.google.com/g/sci.math/c/PwyRME9DOdY/m/FVVo7YJeBgAJ
>
> Whats wrong with you? You then used appeal to authority,
> i.e. Terrence Tao would say a function comes with cod.
> Well yes. And? A function my come with cod. But does
>
> the notion "Definedness" need cod? You avoided the
> question so far. Obviously it doesn't need "cod", if
> you cast Definedness as "elt in dom". There is a small
>
> chance that you would really need "cod" in the FOL/ZFC
> version, if you would rephrase this:
>
> ~EXIST(y):(x,y) e f
>
> Into this:
>
> ~EXIST(y):[y e cod & (x,y) e f]
>
> To make the exist quantifier more bounded. But in
> FOL/ZFC this is not really needed, when operating with
> extensionally equivalent functions. We can define:
>
> dom(f) := { x | EXIST(y): (x,y) e f }
> Dan Christensen schrieb am Montag, 15. Mai 2023 um 22:29:19 UTC+2:
> > Your desperation seems to be growing by the hour, Mr. Collapse. As you know, I subsequently posted the obvious correction:
> > ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> > ALL(a):[a in dom => f(a) in cod]
> > => [Def(f,dom,cod,x) <=> x in dom]] <--------- Correction here
> >
> > Deal with it, Mr. Collapse.
> > 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, May 16, 2023 at 3:34:50 AM UTC-4, Mostowski Collapse wrote:
> But you didn't get my point that the correction is overkill.
> Why would you need the parameter cod?
>

When you specify a function, you must specify BOTH the domain and codomain sets. You could try using definedness without the codomain parameter, but you may come across some wonky results, as you yourself discovered. To be safe, you should include the codomain. It couldn't hurt.

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, May 16, 2023 at 3:40:57 AM UTC-4, Mostowski Collapse wrote:

> But we can now prove in DC Proof:
>
> P(fun,s01,s01,1) & ~P(fun,s0,s0,1)

Nothing wrong with that.

>
> So "fun" can have differing domains s0 and s01?

There is nothing to stop you from making self-contradictory assumptions about a given function and where it is defined and not defined. You can even assume P & ~P. (Recall: P & ~P => Q for any propositions P and Q, be they true or false.)

> Your approach is nonsense. Also not what
>
> Terrence Tao writes. Since Terrence Tao requires
> F ⊆ X x Y.

Wrong. He makes no mention of ordered pairs in his definition of a function here (reposted):

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p.49

The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.

Dan

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

LoL

Terrence Taos: "let P(x, y) be a property pertaining to an object x ∈ X
and an object y ∈ Y" isn't this the same as P ⊆ X x Y ?

This means if either x ∈ X or y ∈ Y is false, then P(x, y) is false.

Dan Christensen schrieb am Dienstag, 16. Mai 2023 um 19:03:01 UTC+2:
> On Tuesday, May 16, 2023 at 3:40:57 AM UTC-4, Mostowski Collapse wrote:
>
> > But we can now prove in DC Proof:
> >
> > P(fun,s01,s01,1) & ~P(fun,s0,s0,1)
>
> Nothing wrong with that.
> >
> > So "fun" can have differing domains s0 and s01?
> There is nothing to stop you from making self-contradictory assumptions about a given function and where it is defined and not defined. You can even assume P & ~P. (Recall: P & ~P => Q for any propositions P and Q, be they true or false.)
> > Your approach is nonsense. Also not what
> >
> > Terrence Tao writes. Since Terrence Tao requires
> > F ⊆ X x Y.
> Wrong. He makes no mention of ordered pairs in his definition of a function here (reposted):
>
> "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> --Terence Tao, "Analysis I," p.49
>
> The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.
> 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, May 16, 2023 at 6:58:40 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 16. Mai 2023 um 19:03:01 UTC+2:
> > On Tuesday, May 16, 2023 at 3:40:57 AM UTC-4, Mostowski Collapse wrote:
> >
> > > But we can now prove in DC Proof:
> > >
> > > P(fun,s01,s01,1) & ~P(fun,s0,s0,1)
> >
> > Nothing wrong with that.
> > >
> > > So "fun" can have differing domains s0 and s01?
> > There is nothing to stop you from making self-contradictory assumptions about a given function and where it is defined and not defined. You can even assume P & ~P. (Recall: P & ~P => Q for any propositions P and Q, be they true or false.)
> > > Your approach is nonsense. Also not what
> > >
> > > Terrence Tao writes. Since Terrence Tao requires
> > > F ⊆ X x Y.
> > Wrong. He makes no mention of ordered pairs in his definition of a function here (reposted):
> >
> > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> > --Terence Tao, "Analysis I," p.49
> >
> > The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.

>
> Terrence Taos: "let P(x, y) be a property pertaining to an object x ∈ X
> and an object y ∈ Y" isn't this the same as P ⊆ X x Y ?
>
> This means if either x ∈ X or y ∈ Y is false, then P(x, y) is false.

Mr. Collapse, you misleadingly wrote, "Terrence Tao requires F ⊆ X x Y."

By his definition here, a function is NOT a set of ordered pairs or a binary predicate as you suggest.

Again, he wrote, "We define the function f : X → Y defined by P on the domain X and range [codomain] Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the UNIQUE OBJECT f(x) for which P(x, f(x)) is true."

Again, from his definition, if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is INDETERMINATE. In your system, it would be false. Sorry, that is NOT the same thing at all, Mr. Collapse. Deal with it.

Dan

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

I didn't use the word set of ordered pairs. But you are right his phrase:

"let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y"

Can be viewed as saying pairs (x,y) belong to P, i.e. P is a relation.
But the expression P ⊆ X x Y can be interpreted two ways. I didn't
specify which one should be applied:

Either this way:

1)
P ⊆ X x Y <=> ∀x∀y(P(x,y) => x ∈ X & y ∈ Y)

Or this way:

2)
P ⊆ X x Y <=> ∀x∀y((x,y) ∈ P => x ∈ X & y ∈ Y)

Do you suggest the shorthand P ⊆ X x Y means 2) and not 1) ?

Dan Christensen schrieb am Mittwoch, 17. Mai 2023 um 01:35:01 UTC+2:
> On Tuesday, May 16, 2023 at 6:58:40 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Dienstag, 16. Mai 2023 um 19:03:01 UTC+2:
> > > On Tuesday, May 16, 2023 at 3:40:57 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > > But we can now prove in DC Proof:
> > > >
> > > > P(fun,s01,s01,1) & ~P(fun,s0,s0,1)
> > >
> > > Nothing wrong with that.
> > > >
> > > > So "fun" can have differing domains s0 and s01?
> > > There is nothing to stop you from making self-contradictory assumptions about a given function and where it is defined and not defined. You can even assume P & ~P. (Recall: P & ~P => Q for any propositions P and Q, be they true or false.)
> > > > Your approach is nonsense. Also not what
> > > >
> > > > Terrence Tao writes. Since Terrence Tao requires
> > > > F ⊆ X x Y.
> > > Wrong. He makes no mention of ordered pairs in his definition of a function here (reposted):
> > >
> > > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> > > --Terence Tao, "Analysis I," p.49
> > >
> > > The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.
>
> >
> > Terrence Taos: "let P(x, y) be a property pertaining to an object x ∈ X
> > and an object y ∈ Y" isn't this the same as P ⊆ X x Y ?
> >
> > This means if either x ∈ X or y ∈ Y is false, then P(x, y) is false.
> Mr. Collapse, you misleadingly wrote, "Terrence Tao requires F ⊆ X x Y."
>
> By his definition here, a function is NOT a set of ordered pairs or a binary predicate as you suggest.
>
> Again, he wrote, "We define the function f : X → Y defined by P on the domain X and range [codomain] Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the UNIQUE OBJECT f(x) for which P(x, f(x)) is true."
>
> Again, from his definition, if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is INDETERMINATE. In your system, it would be false. Sorry, that is NOT the same thing at all, Mr. Collapse. Deal with it.
> 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, May 17, 2023 at 5:07:08 AM UTC-4, Mostowski Collapse wrote:
> I didn't use the word set of ordered pairs. But you are right his phrase:
> "let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y"
> Can be viewed as saying pairs (x,y) belong to P, i.e. P is a relation.
> But the expression P ⊆ X x Y can be interpreted two ways. I didn't
> specify which one should be applied:
>
> Either this way:
>
> 1)
> P ⊆ X x Y <=> ∀x∀y(P(x,y) => x ∈ X & y ∈ Y)
>
> Or this way:
>
> 2)
> P ⊆ X x Y <=> ∀x∀y((x,y) ∈ P => x ∈ X & y ∈ Y)
>
> Do you suggest the shorthand P ⊆ X x Y means 2) and not 1) ?

Still grasping at straws, Mr. Collapse???

Just admit you were wrong when you wrote, "Terrence Tao requires F ⊆ X x Y" where F is supposedly a function.

Also admit that, by Tao's definition, if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) would be INDETERMINATE.

That definition again:

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p.49

In the formal notation of DC Proof, that would be:

ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in x => EXIST(d):[d in y & [P(c,d) & ALL(e):[e in y => [P(c,e) => e=d]]]]]
=> EXIST(f):ALL(c):[c in x => f(c) in y & P(c,f(c))]]

Where P is binary predicate, not a function.

Dan

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

I wasn't talking about:

"if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) ?"

Why would you need "y=f(x)" when we talk about the notion
"f is defined at x". It doesn't have some y in it. Where do you see an y?

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 22:56:28 UTC+2:
> Dans delusional functions and the drinker paradox
> In set theory one can express undefinedness of f at x by:
> ~EXIST(y):(x,y) e f
>
> In free logic one could use instead:
> E!f(x)
https://groups.google.com/g/sci.logic/c/yxICDw_Q7-s/m/iZ3KikwvBwAJ

Both formulas ~EXIST(y):(x,y) e f and E!f(x) don't have y as a free variable.
Also there is no equality sign = involved in both formulas. The first formula
is from FOL/ZFC when we look at functions as graphs:

The graph of a function f : X → Y is the subset Gf of X × Y defined by
Gf = {(x, y) ∈ X × Y : x ∈ X and y = f(x)} .
https://www.math.ucdavis.edu/~hunter/intro_analysis_pdf/ch1.pdf

And the second formula is from free logic. The free logic approach
is a little unsatisfactory since I didn't figure out yet, what it would
mean to have a explicit domain X and not an implicit domain of discourse:

To distinguish terms that denote members of D from those that do not,
free logic often employs the one-place “existence” predicate.
https://plato.stanford.edu/entries/logic-free/

Whats the DC Proof formula to determine whether "f is defined at x"?
There is no such formula. You cannot define it in DC Proof. You have
not yet provided a definition using only the parameters f and x.

P.S.: Here is a trick to let free logic talk about an explicit domain X and
not the implicit domain of discourse D only. Just require, i.e. case
we want to model f: X -> Y.

~x ∈ X → ~E!f(x)
x ∈ X → E!f(x) & f(x) ∈ Y

So we can use D outside value as a marker for definedness on an
explicitly given domain X.

Dan Christensen schrieb am Mittwoch, 17. Mai 2023 um 14:46:22 UTC+2:
> On Wednesday, May 17, 2023 at 5:07:08 AM UTC-4, Mostowski Collapse wrote:
> > I didn't use the word set of ordered pairs. But you are right his phrase:
> > "let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y"
> > Can be viewed as saying pairs (x,y) belong to P, i.e. P is a relation.
> > But the expression P ⊆ X x Y can be interpreted two ways. I didn't
> > specify which one should be applied:
> >
> > Either this way:
> >
> > 1)
> > P ⊆ X x Y <=> ∀x∀y(P(x,y) => x ∈ X & y ∈ Y)
> >
> > Or this way:
> >
> > 2)
> > P ⊆ X x Y <=> ∀x∀y((x,y) ∈ P => x ∈ X & y ∈ Y)
> >
> > Do you suggest the shorthand P ⊆ X x Y means 2) and not 1) ?
> Still grasping at straws, Mr. Collapse???
>
> Just admit you were wrong when you wrote, "Terrence Tao requires F ⊆ X x Y" where F is supposedly a function.
>
> Also admit that, by Tao's definition, if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) would be INDETERMINATE.
>
> That definition again:
> "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> --Terence Tao, "Analysis I," p.49
> In the formal notation of DC Proof, that would be:
>
> ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in x => EXIST(d):[d in y & [P(c,d) & ALL(e):[e in y => [P(c,e) => e=d]]]]]
> => EXIST(f):ALL(c):[c in x => f(c) in y & P(c,f(c))]]
>
> Where P is binary predicate, not a function.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

I don't think a proposal of functions, functions and ultimately
a defined of definedness that uses 4 parameters like this
here is sustainable and makes any sense:

ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
ALL(a):[a in dom => f(a) in cod]
=> [Def(f,dom,cod,x) <=> x in dom]]

How would you infer what the domain of a function
composition is. Lets say you have two functions f and g.
When is this function h defined?

h = f o g

Its not that difficult to find a solution in FOL/ZFC
to the problem, neither its extremly difficult in free logic.
What is your take in DC Poop?

Mostowski Collapse schrieb am Mittwoch, 17. Mai 2023 um 16:56:43 UTC+2:
> I wasn't talking about:
>
> "if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) ?"
>
> Why would you need "y=f(x)" when we talk about the notion
> "f is defined at x". It doesn't have some y in it. Where do you see an y?
> Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 22:56:28 UTC+2:
> > Dans delusional functions and the drinker paradox
> > In set theory one can express undefinedness of f at x by:
> > ~EXIST(y):(x,y) e f
> >
> > In free logic one could use instead:
> > E!f(x)
> https://groups.google.com/g/sci.logic/c/yxICDw_Q7-s/m/iZ3KikwvBwAJ
> Both formulas ~EXIST(y):(x,y) e f and E!f(x) don't have y as a free variable.
> Also there is no equality sign = involved in both formulas. The first formula
> is from FOL/ZFC when we look at functions as graphs:
>
> The graph of a function f : X → Y is the subset Gf of X × Y defined by
> Gf = {(x, y) ∈ X × Y : x ∈ X and y = f(x)} .
> https://www.math.ucdavis.edu/~hunter/intro_analysis_pdf/ch1.pdf
>
> And the second formula is from free logic. The free logic approach
> is a little unsatisfactory since I didn't figure out yet, what it would
> mean to have a explicit domain X and not an implicit domain of discourse:
>
> To distinguish terms that denote members of D from those that do not,
> free logic often employs the one-place “existence” predicate.
> https://plato.stanford.edu/entries/logic-free/
>
> Whats the DC Proof formula to determine whether "f is defined at x"?
> There is no such formula. You cannot define it in DC Proof. You have
> not yet provided a definition using only the parameters f and x.
>
> P.S.: Here is a trick to let free logic talk about an explicit domain X and
> not the implicit domain of discourse D only. Just require, i.e. case
> we want to model f: X -> Y.
>
> ~x ∈ X → ~E!f(x)
> x ∈ X → E!f(x) & f(x) ∈ Y
>
> So we can use D outside value as a marker for definedness on an
> explicitly given domain X.
> Dan Christensen schrieb am Mittwoch, 17. Mai 2023 um 14:46:22 UTC+2:
> > On Wednesday, May 17, 2023 at 5:07:08 AM UTC-4, Mostowski Collapse wrote:
> > > I didn't use the word set of ordered pairs. But you are right his phrase:
> > > "let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y"
> > > Can be viewed as saying pairs (x,y) belong to P, i.e. P is a relation..
> > > But the expression P ⊆ X x Y can be interpreted two ways. I didn't
> > > specify which one should be applied:
> > >
> > > Either this way:
> > >
> > > 1)
> > > P ⊆ X x Y <=> ∀x∀y(P(x,y) => x ∈ X & y ∈ Y)
> > >
> > > Or this way:
> > >
> > > 2)
> > > P ⊆ X x Y <=> ∀x∀y((x,y) ∈ P => x ∈ X & y ∈ Y)
> > >
> > > Do you suggest the shorthand P ⊆ X x Y means 2) and not 1) ?
> > Still grasping at straws, Mr. Collapse???
> >
> > Just admit you were wrong when you wrote, "Terrence Tao requires F ⊆ X x Y" where F is supposedly a function.
> >
> > Also admit that, by Tao's definition, if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) would be INDETERMINATE.
> >
> > That definition again:
> > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> > --Terence Tao, "Analysis I," p.49
> > In the formal notation of DC Proof, that would be:
> >
> > ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in x => EXIST(d):[d in y & [P(c,d) & ALL(e):[e in y => [P(c,e) => e=d]]]]]
> > => EXIST(f):ALL(c):[c in x => f(c) in y & P(c,f(c))]]
> >
> > Where P is binary predicate, not a function.
> > 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, May 17, 2023 at 11:08:47 AM UTC-4, Mostowski Collapse wrote:
> I don't think a proposal of functions, functions and ultimately
> a defined of definedness that uses 4 parameters like this
> here is sustainable and makes any sense:

> ALL(f):ALL(dom):ALL(cod):ALL(x):[Set(dom) & Set(cod) &
> ALL(a):[a in dom => f(a) in cod]
> => [Def(f,dom,cod,x) <=> x in dom]]

It works. It makes sense. Deal with it, Mr. Collapse.

> How would you infer what the domain of a function
> composition is. Lets say you have two functions f and g.
> When is this function h defined?
>
> h = f o g
>

Not a problem. The domain of h will be domain of g. The codomain of h will be codomain of f

Dan

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

Are you sure you wrote DC Proof by yourself. And you didn't plagiarize
from somewhere. Why does this proof need the subset axiom?

https://www.dcproof.com/JanBurse15.htm

Are you mental. Its a pure logical theorem, you
can prove it without the subset axiom:

∀x(Exu → Exp) ↔ ∀a(∀y(Eya → Eyu) → ∀z(Eza → Ezp)) is valid.
https://www.umsu.de/trees/#~6x(Exu~5Exp)~4~6a(~6y(Eya~5Eyu)~5~6z(Eza~5Ezp))

Dan Christensen schrieb am Donnerstag, 8. Juni 2023 um 05:25:40 UTC+2:
> Comments?