Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Sunday, April 17, 2022 at 8:46:13 PM UTC-4, Ben wrote:
>
>> >> Unfortunately it entails nonsense. Is that a feature of DC Proof that
>> >> you want? Starting from only two axioms, yours and that the set {0}
>> >> exists, it's possible to prove
>> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> >> Can that be what you intended to follow from your axiom?
>> >
>> > We have:
>> >
>> > dom = cod = {0}
>> >
>> > Both are non-empty.
>> >
>> > f: {0} --> {0}
>> >
>> > g:{0} --> {0}
>
>> This isn't DC Proof notation is it?
>
> No.
>
>> > So, we can apply the definition to obtain:
>> >
>> > f=g <=> ALL(a):[a in {0} => f(a)=g(a)]
>
>> Is this possible in DC Proof?
>
> f=g <=> ALL(a):[a in dom => f(a)=g(a)]
>
> where f, g and dom are whatever names you specified for the two
> functions in question and their domain sets.

I feel sure we are talking at cross purposes here. With the set model
of functions, this is a non-issue. I'd define

f = {(0,0), (1,1)}
g = {(0,0), (1,0)}

and I would not be able to prove f=g. Writing

f(0)=0 & f(1)=1 & g(0)=0 & g(1)=0

in DC Proof won't work because of those ALL(dom):ALL(cod) quantifiers
are real for alls. I can derive (as I showed you) f=g from you axiom so
there must be more I need to say about f and g to prevent this.

>> > With me so far?
>
>> If you don't have time to answer me /about DC Proof/, that's fine but I
>> don't want to be drip feed what I already know to be true about
>> functions and domains. Imagine that you are talking to someone who's
>> got a maths degree and has read a the standard textbooks on mathematical
>> logic.
>>
>> I wanted to know if you intended
>> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> to be provable from your axiom.
>
> No.
>
>> It not a theorem I'd want from an axiom
>> of mine about function equality, so I thought you might care enough to
>> either defend it or correct it.
>
> The theorem (in DC Proof notation) should instead be something like:
>
> ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in
> x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]

That may also be a theorem but so is

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

======================================================================
1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& EXIST(a):a ε dom & EXIST(a):a ε cod
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Axiom

2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
Axiom

3 Set(s) & ALL(a):[a ε s <=> a=0]
E Spec, 2

4 Set(s)
Split, 3

5 ALL(a):[a ε s <=> a=0]
Split, 3

6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
& EXIST(a):a ε s & EXIST(a):a ε cod
& ALL(a):[a ε s => f1(a) ε cod]
& ALL(a):[a ε s => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
U Spec, 1

7 ALL(f1):ALL(f2):[Set(s) & Set(s)
& EXIST(a):a ε s & EXIST(a):a ε s
& ALL(a):[a ε s => f1(a) ε s]
& ALL(a):[a ε s => f2(a) ε s]
=> [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
U Spec, 6

8 0 ε s <=> 0=0
U Spec, 5

9 [0 ε s => 0=0] & [0=0 => 0 ε s]
Iff-And, 8

10 0 ε s => 0=0
Split, 9

11 0=0 => 0 ε s
Split, 9

12 0=0
Reflex

13 0 ε s
Detach, 11, 12

14 EXIST(a):a ε s
E Gen, 13

15 f(0)=0 & g(0)=0
Premise

16 z ε s
Premise

17 z ε s <=> z=0
U Spec, 5

18 [z ε s => z=0] & [z=0 => z ε s]
Iff-And, 17

19 z ε s => z=0
Split, 18

20 z=0 => z ε s
Split, 18

21 z=0
Detach, 19, 16

22 0 ε s
Substitute, 21, 16

23 f(0)=0
Split, 15

24 g(0)=0
Split, 15

25 f(0) ε s
Substitute, 23, 22

26 f(z) ε s
Substitute, 21, 25

27 ALL(a):[a ε s => f(a) ε s]
Conclusion, 16

28 z ε s
Premise

29 z ε s <=> z=0
U Spec, 5

30 [z ε s => z=0] & [z=0 => z ε s]
Iff-And, 29

31 z ε s => z=0
Split, 30

32 z=0 => z ε s
Split, 30

33 z=0
Detach, 31, 28

34 0 ε s
Substitute, 33, 28

35 f(0)=0
Split, 15

36 g(0)=0
Split, 15

37 g(0) ε s
Substitute, 36, 34

38 g(z) ε s
Substitute, 33, 37

39 ALL(a):[a ε s => g(a) ε s]
Conclusion, 28

40 ALL(f2):[Set(s) & Set(s)
& EXIST(a):a ε s & EXIST(a):a ε s
& ALL(a):[a ε s => f(a) ε s]
& ALL(a):[a ε s => f2(a) ε s]
=> [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
U Spec, 7

41 Set(s) & Set(s)
& EXIST(a):a ε s & EXIST(a):a ε s
& ALL(a):[a ε s => f(a) ε s]
& ALL(a):[a ε s => g(a) ε s]
=> [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
U Spec, 40

42 Set(s) & Set(s)
Join, 4, 4

43 Set(s) & Set(s) & EXIST(a):a ε s
Join, 42, 14

44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
Join, 43, 14

45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
& ALL(a):[a ε s => f(a) ε s]
Join, 44, 27

46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
& ALL(a):[a ε s => f(a) ε s]
& ALL(a):[a ε s => g(a) ε s]
Join, 45, 39

47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
Detach, 41, 46

48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
& [ALL(a):[a ε s => f(a)=g(a)] => f=g]
Iff-And, 47

49 f=g => ALL(a):[a ε s => f(a)=g(a)]
Split, 48

50 ALL(a):[a ε s => f(a)=g(a)] => f=g
Split, 48

51 z ε s
Premise

52 z ε s <=> z=0
U Spec, 5

53 [z ε s => z=0] & [z=0 => z ε s]
Iff-And, 52

54 z ε s => z=0
Split, 53

55 z=0 => z ε s
Split, 53

56 z=0
Detach, 54, 51

57 f(0)=0
Split, 15

58 g(0)=0
Split, 15

59 z=g(0)
Substitute, 58, 56

60 0=g(0)
Substitute, 56, 59

61 f(0)=g(0)
Substitute, 57, 60

62 f(z)=g(z)
Substitute, 56, 61

63 ALL(a):[a ε s => f(a)=g(a)]
Conclusion, 51

64 f=g
Detach, 50, 63

65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
Conclusion, 15

--
Ben.

Fritz Feldhase <franz.fritschee.ff@gmail.com> writes:

> I've simplified it now:
>
> function(f) :<-> Az(z e f -> ExEy(z = <x, y>) & AxAyAz(<x, y> e f & <x, z> e f -> y = z)
> dom(f) := {x e UUf : Ey(<x, y> e f)}
> img(f) := {y e UUf : Ex(<x, y> e f)}
>
> f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
> "f is a function from X to Y."
>
> f(x) := U{y e UUf : <x, y> e f}
>
> Theorem:
> AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x))).

>> ... for reference, Shoenfield defines pairs (<x,y> = {{x}, {x,y}})
>> and projections p1 and p2, and then says that a function f is a set
>> of pairs with the property that
>>
>> f subset Ra(f) x Do(f)
>>
>> and
>>
>> <a,b> in f and <a',b> in f -> a = a'
>>
>> where Do(f) = [p2(y) | y in f] and Ra(f) = [p1(y) | y in f].
>>
>> Note that he uses the other order for the pairs.
>>
>> Done like this, there is no definition of equality of functions other
>> than that of sets.
>
> Right. I'd say, my approach mentioned above is "essentialy" the same
> (modulo some technical details).

It looks similar but I'm not sure what all your notation means. What is
UUf

--
Ben.

On Monday, April 18, 2022 at 6:25:29 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> There a further problem. He allows forming f(f), i.e.
> self application.

It hasn't caused any problem. Assumptions about f(f) are pretty much a dead end, as you have found out for yourself, Jan Burse.

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, April 19, 2022 at 1:12:20 AM UTC+2, Ben wrote:
>
> It looks similar but I'm not sure what all your notation means. What is
> UUf

It's just a technical detail (since my set theory is ZFC).

It means the union of the union of f.

So if f is, say {<1, 2>, <3, 4>} = {{{1}, {1, 2}}, {{3}, {3, 4}}}, Uf is {{1}, {1, 2}, {3}, {3, 4}} and UUf is {1, 2, 3, 4}. This allows to define

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

in the context of ZFC. (Remember the "set builder notation", {x e A : ...x...}, in ZFC...)

Of course in this case we have

Ax(x e dom(f) <-> Ey(<x, y> e f))

and

Ay(y e img(f) <-> Ex(<x, y> e f)).

So

function(f) :<-> Az(z e f -> ExEy(z = <x, y>) & AxAyAz(<x, y> e f & <x, z> e f -> y = z)

just means that f is a function iff it is a set of pairs which is "functional".

and

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

are clear now, I guess.

These notions allow for the quite handy definition

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."

From this we might prove, say,

AXAYAf: (f: X --> Y) -> f c X x Y

etc.

On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Sunday, April 17, 2022 at 8:46:13 PM UTC-4, Ben wrote:
> >
> >> >> Unfortunately it entails nonsense. Is that a feature of DC Proof that
> >> >> you want? Starting from only two axioms, yours and that the set {0}
> >> >> exists, it's possible to prove
> >> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >> >> Can that be what you intended to follow from your axiom?
> >> >
> >> > We have:
> >> >
> >> > dom = cod = {0}
> >> >
> >> > Both are non-empty.
> >> >
> >> > f: {0} --> {0}
> >> >
> >> > g:{0} --> {0}
> >
> >> This isn't DC Proof notation is it?
> >
> > No.
> >
> >> > So, we can apply the definition to obtain:
> >> >
> >> > f=g <=> ALL(a):[a in {0} => f(a)=g(a)]
> >
> >> Is this possible in DC Proof?
> >
> > f=g <=> ALL(a):[a in dom => f(a)=g(a)]
> >
> > where f, g and dom are whatever names you specified for the two
> > functions in question and their domain sets.
>
> I feel sure we are talking at cross purposes here. With the set model
> of functions, this is a non-issue. I'd define
>
> f = {(0,0), (1,1)}
> g = {(0,0), (1,0)}
>
> and I would not be able to prove f=g. Writing
>
> f(0)=0 & f(1)=1 & g(0)=0 & g(1)=0
>
> in DC Proof won't work because of those ALL(dom):ALL(cod) quantifiers
> are real for alls. I can derive (as I showed you) f=g from you axiom so
> there must be more I need to say about f and g to prevent this.
>
> >> > With me so far?
> >
> >> If you don't have time to answer me /about DC Proof/, that's fine but I
> >> don't want to be drip feed what I already know to be true about
> >> functions and domains. Imagine that you are talking to someone who's
> >> got a maths degree and has read a the standard textbooks on mathematical
> >> logic.
> >>
> >> I wanted to know if you intended
> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >> to be provable from your axiom.
> >
> > No.
> >
> >> It not a theorem I'd want from an axiom
> >> of mine about function equality, so I thought you might care enough to
> >> either defend it or correct it.
> >
> > The theorem (in DC Proof notation) should instead be something like:
> >
> > ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in
> > x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]
> That may also be a theorem but so is
>
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>
> ======================================================================
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a ε dom & EXIST(a):a ε cod
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Axiom
>

The Axiom for Functional Equality (1 variable)

> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> Axiom
>
> 3 Set(s) & ALL(a):[a ε s <=> a=0]
> E Spec, 2
>

s = {0}

> 4 Set(s)
> Split, 3
>
> 5 ALL(a):[a ε s <=> a=0]
> Split, 3
>
> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> & EXIST(a):a ε s & EXIST(a):a ε cod
> & ALL(a):[a ε s => f1(a) ε cod]
> & ALL(a):[a ε s => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 1
>
> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f1(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 6
>
> 8 0 ε s <=> 0=0
> U Spec, 5
>
> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
> Iff-And, 8
>
> 10 0 ε s => 0=0
> Split, 9
>
> 11 0=0 => 0 ε s
> Split, 9
>
> 12 0=0
> Reflex
>
> 13 0 ε s
> Detach, 11, 12
>
> 14 EXIST(a):a ε s
> E Gen, 13
>

s is non-empty

> 15 f(0)=0 & g(0)=0
> Premise
>

f and g introduced

> 16 z ε s
> Premise

Suppose z in s

>
> 17 z ε s <=> z=0
> U Spec, 5
>
> 18 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 17
>
> 19 z ε s => z=0
> Split, 18
>
> 20 z=0 => z ε s
> Split, 18
>
> 21 z=0
> Detach, 19, 16
>
> 22 0 ε s
> Substitute, 21, 16
>

0 in s

> 23 f(0)=0
> Split, 15
>
> 24 g(0)=0
> Split, 15
>
> 25 f(0) ε s
> Substitute, 23, 22
>
> 26 f(z) ε s
> Substitute, 21, 25
>
> 27 ALL(a):[a ε s => f(a) ε s]
> Conclusion, 16
>

f is a function on s

> 28 z ε s
> Premise
>

z in s

> 29 z ε s <=> z=0
> U Spec, 5
>
> 30 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 29
>
> 31 z ε s => z=0
> Split, 30
>
> 32 z=0 => z ε s
> Split, 30
>
> 33 z=0
> Detach, 31, 28
>
> 34 0 ε s
> Substitute, 33, 28
>
> 35 f(0)=0
> Split, 15
>
> 36 g(0)=0
> Split, 15
>
> 37 g(0) ε s
> Substitute, 36, 34
>
> 38 g(z) ε s
> Substitute, 33, 37
>
> 39 ALL(a):[a ε s => g(a) ε s]
> Conclusion, 28
>

g is a function on s

> 40 ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
> U Spec, 7
>
> 41 Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
> U Spec, 40
>
> 42 Set(s) & Set(s)
> Join, 4, 4
>
> 43 Set(s) & Set(s) & EXIST(a):a ε s
> Join, 42, 14
>
> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> Join, 43, 14
>
> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> Join, 44, 27
>
> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> Join, 45, 39
>
> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
> Detach, 41, 46
>
> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
> Iff-And, 47
>
> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
> Split, 48
>
> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
> Split, 48
>
> 51 z ε s
> Premise
>
> 52 z ε s <=> z=0
> U Spec, 5
>
> 53 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 52
>
> 54 z ε s => z=0
> Split, 53
>
> 55 z=0 => z ε s
> Split, 53
>
> 56 z=0
> Detach, 54, 51
>
> 57 f(0)=0
> Split, 15
>
> 58 g(0)=0
> Split, 15
>
> 59 z=g(0)
> Substitute, 58, 56
>
> 60 0=g(0)
> Substitute, 56, 59
>
> 61 f(0)=g(0)
> Substitute, 57, 60
>
> 62 f(z)=g(z)
> Substitute, 56, 61
>
> 63 ALL(a):[a ε s => f(a)=g(a)]
> Conclusion, 51
>
> 64 f=g
> Detach, 50, 63
>
> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> Conclusion, 15
>

The problem is your axiom on line 2. It should really be a premise. Then when you invoke the Conclusion Rule on the next line to discharge that premise, you would get something like:

On Tuesday, April 19, 2022 at 2:26:52 AM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:
> > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >
> > > On Sunday, April 17, 2022 at 8:46:13 PM UTC-4, Ben wrote:
> > >
> > >> >> Unfortunately it entails nonsense. Is that a feature of DC Proof that
> > >> >> you want? Starting from only two axioms, yours and that the set {0}
> > >> >> exists, it's possible to prove
> > >> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > >> >> Can that be what you intended to follow from your axiom?
> > >> >
> > >> > We have:
> > >> >
> > >> > dom = cod = {0}
> > >> >
> > >> > Both are non-empty.
> > >> >
> > >> > f: {0} --> {0}
> > >> >
> > >> > g:{0} --> {0}
> > >
> > >> This isn't DC Proof notation is it?
> > >
> > > No.
> > >
> > >> > So, we can apply the definition to obtain:
> > >> >
> > >> > f=g <=> ALL(a):[a in {0} => f(a)=g(a)]
> > >
> > >> Is this possible in DC Proof?
> > >
> > > f=g <=> ALL(a):[a in dom => f(a)=g(a)]
> > >
> > > where f, g and dom are whatever names you specified for the two
> > > functions in question and their domain sets.
> >
> > I feel sure we are talking at cross purposes here. With the set model
> > of functions, this is a non-issue. I'd define
> >
> > f = {(0,0), (1,1)}
> > g = {(0,0), (1,0)}
> >
> > and I would not be able to prove f=g. Writing
> >
> > f(0)=0 & f(1)=1 & g(0)=0 & g(1)=0
> >
> > in DC Proof won't work because of those ALL(dom):ALL(cod) quantifiers
> > are real for alls. I can derive (as I showed you) f=g from you axiom so
> > there must be more I need to say about f and g to prevent this.
> >
> > >> > With me so far?
> > >
> > >> If you don't have time to answer me /about DC Proof/, that's fine but I
> > >> don't want to be drip feed what I already know to be true about
> > >> functions and domains. Imagine that you are talking to someone who's
> > >> got a maths degree and has read a the standard textbooks on mathematical
> > >> logic.
> > >>
> > >> I wanted to know if you intended
> > >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > >> to be provable from your axiom.
> > >
> > > No.
> > >
> > >> It not a theorem I'd want from an axiom
> > >> of mine about function equality, so I thought you might care enough to
> > >> either defend it or correct it.
> > >
> > > The theorem (in DC Proof notation) should instead be something like:
> > >
> > > ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in
> > > x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]
> > That may also be a theorem but so is
> >
> > ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >
> > ======================================================================
> > 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & EXIST(a):a ε dom & EXIST(a):a ε cod
> > & ALL(a):[a ε dom => f1(a) ε cod]
> > & ALL(a):[a ε dom => f2(a) ε cod]
> > => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> > Axiom
> The Axiom for Functional Equality (1 variable)

Now:

> > 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> > Axiom

There shouldn't be a problem with that axiom, actually it is provable from the usual axioms of (any) set theory.

It just states that there is the singleton set {0}, containing 0 as its sole element.

Not that exciting.

NOTE that "0" in set theory is not a variable but a constant.

> > 3 Set(s) & ALL(a):[a ε s <=> a=0]
> > E Spec, 2
> >
> s = {0}

Exactly.

> > 4 Set(s)
> > Split, 3
> >
> > 5 ALL(a):[a ε s <=> a=0]
> > Split, 3
> >
> > 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> > & EXIST(a):a ε s & EXIST(a):a ε cod
> > & ALL(a):[a ε s => f1(a) ε cod]
> > & ALL(a):[a ε s => f2(a) ε cod]
> > => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> > U Spec, 1
> >
> > 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a ε s & EXIST(a):a ε s
> > & ALL(a):[a ε s => f1(a) ε s]
> > & ALL(a):[a ε s => f2(a) ε s]
> > => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> > U Spec, 6
> >
> > 8 0 ε s <=> 0=0
> > U Spec, 5
> >
> > 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
> > Iff-And, 8
> >
> > 10 0 ε s => 0=0
> > Split, 9
> >
> > 11 0=0 => 0 ε s
> > Split, 9
> >
> > 12 0=0
> > Reflex
> >
> > 13 0 ε s
> > Detach, 11, 12
> >
> > 14 EXIST(a):a ε s
> > E Gen, 13
> >
> s is non-empty.

Right.

> > 15 f(0)=0 & g(0)=0
> > Premise
> >
> f and g introduced
> > 16 z ε s
> > Premise
> Suppose z in s
> >
> > 17 z ε s <=> z=0
> > U Spec, 5
> >
> > 18 [z ε s => z=0] & [z=0 => z ε s]
> > Iff-And, 17
> >
> > 19 z ε s => z=0
> > Split, 18
> >
> > 20 z=0 => z ε s
> > Split, 18
> >
> > 21 z=0
> > Detach, 19, 16
> >
> > 22 0 ε s
> > Substitute, 21, 16
> >
> 0 in s

Indeed. :-)

> > 23 f(0)=0
> > Split, 15
> >
> > 24 g(0)=0
> > Split, 15
> >
> > 25 f(0) ε s
> > Substitute, 23, 22
> >
> > 26 f(z) ε s
> > Substitute, 21, 25
> >
> > 27 ALL(a):[a ε s => f(a) ε s]
> > Conclusion, 16
> >
> f is a function on s
> > 28 z ε s
> > Premise
> >
> z in s
> > 29 z ε s <=> z=0
> > U Spec, 5
> >
> > 30 [z ε s => z=0] & [z=0 => z ε s]
> > Iff-And, 29
> >
> > 31 z ε s => z=0
> > Split, 30
> >
> > 32 z=0 => z ε s
> > Split, 30
> >
> > 33 z=0
> > Detach, 31, 28
> >
> > 34 0 ε s
> > Substitute, 33, 28
> >
> > 35 f(0)=0
> > Split, 15
> >
> > 36 g(0)=0
> > Split, 15
> >
> > 37 g(0) ε s
> > Substitute, 36, 34
> >
> > 38 g(z) ε s
> > Substitute, 33, 37
> >
> > 39 ALL(a):[a ε s => g(a) ε s]
> > Conclusion, 28
> >
> g is a function on s
> > 40 ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a ε s & EXIST(a):a ε s
> > & ALL(a):[a ε s => f(a) ε s]
> > & ALL(a):[a ε s => f2(a) ε s]
> > => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
> > U Spec, 7
> >
> > 41 Set(s) & Set(s)
> > & EXIST(a):a ε s & EXIST(a):a ε s
> > & ALL(a):[a ε s => f(a) ε s]
> > & ALL(a):[a ε s => g(a) ε s]
> > => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
> > U Spec, 40
> >
> > 42 Set(s) & Set(s)
> > Join, 4, 4
> >
> > 43 Set(s) & Set(s) & EXIST(a):a ε s
> > Join, 42, 14
> >
> > 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> > Join, 43, 14
> >
> > 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> > & ALL(a):[a ε s => f(a) ε s]
> > Join, 44, 27
> >
> > 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> > & ALL(a):[a ε s => f(a) ε s]
> > & ALL(a):[a ε s => g(a) ε s]
> > Join, 45, 39
> >
> > 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
> > Detach, 41, 46
> >
> > 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
> > & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
> > Iff-And, 47
> >
> > 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
> > Split, 48
> >
> > 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
> > Split, 48
> >
> > 51 z ε s
> > Premise
> >
> > 52 z ε s <=> z=0
> > U Spec, 5
> >
> > 53 [z ε s => z=0] & [z=0 => z ε s]
> > Iff-And, 52
> >
> > 54 z ε s => z=0
> > Split, 53
> >
> > 55 z=0 => z ε s
> > Split, 53
> >
> > 56 z=0
> > Detach, 54, 51
> >
> > 57 f(0)=0
> > Split, 15
> >
> > 58 g(0)=0
> > Split, 15
> >
> > 59 z=g(0)
> > Substitute, 58, 56
> >
> > 60 0=g(0)
> > Substitute, 56, 59
> >
> > 61 f(0)=g(0)
> > Substitute, 57, 60
> >
> > 62 f(z)=g(z)
> > Substitute, 56, 61
> >
> > 63 ALL(a):[a ε s => f(a)=g(a)]
> > Conclusion, 51
> >
> > 64 f=g
> > Detach, 50, 63
> >
> > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > Conclusion, 15
> >
> The problem is your axiom on line 2. It should really be a premise. Then when you invoke the Conclusion Rule on the next line to discharge that premise, you would get something like: [<nonsense>].

On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:

> > The theorem (in DC Proof notation) should instead be something like:
> >
> > ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in
> > x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]
> That may also be a theorem but so is
>
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>
> ======================================================================
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a ε dom & EXIST(a):a ε cod
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Axiom
>
> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> Axiom
>
> 3 Set(s) & ALL(a):[a ε s <=> a=0]
> E Spec, 2
>
> 4 Set(s)
> Split, 3
>
> 5 ALL(a):[a ε s <=> a=0]
> Split, 3
>
> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> & EXIST(a):a ε s & EXIST(a):a ε cod
> & ALL(a):[a ε s => f1(a) ε cod]
> & ALL(a):[a ε s => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 1
>
> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f1(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 6
>
> 8 0 ε s <=> 0=0
> U Spec, 5
>
> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
> Iff-And, 8
>
> 10 0 ε s => 0=0
> Split, 9
>
> 11 0=0 => 0 ε s
> Split, 9
>
> 12 0=0
> Reflex
>
> 13 0 ε s
> Detach, 11, 12
>
> 14 EXIST(a):a ε s
> E Gen, 13
>
> 15 f(0)=0 & g(0)=0
> Premise
>
> 16 z ε s
> Premise
>
> 17 z ε s <=> z=0
> U Spec, 5
>
> 18 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 17
>
> 19 z ε s => z=0
> Split, 18
>
> 20 z=0 => z ε s
> Split, 18
>
> 21 z=0
> Detach, 19, 16
>
> 22 0 ε s
> Substitute, 21, 16
>
> 23 f(0)=0
> Split, 15
>
> 24 g(0)=0
> Split, 15
>
> 25 f(0) ε s
> Substitute, 23, 22
>
> 26 f(z) ε s
> Substitute, 21, 25
>
> 27 ALL(a):[a ε s => f(a) ε s]
> Conclusion, 16
>
> 28 z ε s
> Premise
>
> 29 z ε s <=> z=0
> U Spec, 5
>
> 30 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 29
>
> 31 z ε s => z=0
> Split, 30
>
> 32 z=0 => z ε s
> Split, 30
>
> 33 z=0
> Detach, 31, 28
>
> 34 0 ε s
> Substitute, 33, 28
>
> 35 f(0)=0
> Split, 15
>
> 36 g(0)=0
> Split, 15
>
> 37 g(0) ε s
> Substitute, 36, 34
>
> 38 g(z) ε s
> Substitute, 33, 37
>
> 39 ALL(a):[a ε s => g(a) ε s]
> Conclusion, 28
>
> 40 ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
> U Spec, 7
>
> 41 Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
> U Spec, 40
>
> 42 Set(s) & Set(s)
> Join, 4, 4
>
> 43 Set(s) & Set(s) & EXIST(a):a ε s
> Join, 42, 14
>
> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> Join, 43, 14
>
> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> Join, 44, 27
>
> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> Join, 45, 39
>
> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
> Detach, 41, 46
>
> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
> Iff-And, 47
>
> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
> Split, 48
>
> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
> Split, 48
>
> 51 z ε s
> Premise
>
> 52 z ε s <=> z=0
> U Spec, 5
>
> 53 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 52
>
> 54 z ε s => z=0
> Split, 53
>
> 55 z=0 => z ε s
> Split, 53
>
> 56 z=0
> Detach, 54, 51
>
> 57 f(0)=0
> Split, 15
>
> 58 g(0)=0
> Split, 15
>
> 59 z=g(0)
> Substitute, 58, 56
>
> 60 0=g(0)
> Substitute, 56, 59
>
> 61 f(0)=g(0)
> Substitute, 57, 60
>
> 62 f(z)=g(z)
> Substitute, 56, 61
>
> 63 ALL(a):[a ε s => f(a)=g(a)]
> Conclusion, 51
>
> 64 f=g
> Detach, 50, 63
>

A less mysterious ending would be:

65. ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
Join, 27, 39

66. ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
& f=g
Join, 65, 64

67. ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
=> ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
& f=g]
Conclusion, 15

68. ALL(x0):[EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
=> EXIST(s):ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0

=> ALL(a):[a in s => f(a) in s] <---- NEW
& ALL(a):[a in s => g(a) in s] <---- NEW
& f=g]]
Conclusion, 2

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, April 18, 2022 at 9:46:49 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 2:26:52 AM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:

> > > ======================================================================
> > > 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > > & EXIST(a):a ε dom & EXIST(a):a ε cod
> > > & ALL(a):[a ε dom => f1(a) ε cod]
> > > & ALL(a):[a ε dom => f2(a) ε cod]
> > > => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> > > Axiom
> > The Axiom for Functional Equality (1 variable)
> Now:
> > > 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> > > Axiom
> There shouldn't be a problem with that axiom, actually it is provable from the usual axioms of (any) set theory.
>

It is not a theorem of DC Proof set theory. There is no axiom of set theory that postulates the existence of any object, not even the empty set. The domain of discourse is also not assumed to be non-empty as in standard FOL. As such, there are no existential theorems, i.e. theorems of the form EXIST(a):P(a) in DC Proof.

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, April 19, 2022 at 3:46:49 AM UTC+2, Fritz Feldhase wrote:
>
> There seems to be something wrong with DC proof and/or your axioms.

Actually, it's quite simple to see what.

Your axiom

1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a ε dom & EXIST(a):a ε cod
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Axiom

essentially states that f1 = f2 if f1 agrees with f2 on a (nonempty) SUBSET of their common domain (one might think).

But that is not sufficient.

Hence the nonsensical result derived by Ben.

But "actually" not even t h i s characterization is correct.

After all, w h i c h magic ensures that the set /dom/ is actually the domain of f1 and f2?

It might just be some arbitrary set, and that f1(a) e cod and f2 e cod for all x in dom might just be a coincidence.

In short, your axiom is completely bogus.

And right, Tao's version differs from your formulation.

He uses the notion f: X --> Y which explicitly states that f is a function with domain X and codomain Y.

You approach is lacking any "connection" between a function f and its domain (and codomain).

Actually (in real math) the domain of a function is one of its "properties"..

Hence we can define an "operation" dom which delivers its domain.

Moreover this explains why dom(f) =/= dom(g) implies f =/= g.

On Tuesday, April 19, 2022 at 4:08:49 AM UTC+2, Dan Christensen wrote:
>
> There is no axiom [in DC Proof] that postulates the existence of any object, not even the empty set. The domain of discourse is also not assumed to be non-empty as in standard FOL. As such, there are no existential theorems, i.e. theorems of the form EXIST(a):P(a) in DC Proof.

We certainly will have to ad axioms or assumptions which state the existence of some object(s).

Otherwise it would be hard to suffice the clause

EXIST(a):a ε dom & EXIST(a):a ε cod

in your "function equality axiom".

Don't you think so?

Hint: Your axiom is bogus. See my other post.

On Monday, April 18, 2022 at 10:19:52 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 3:46:49 AM UTC+2, Fritz Feldhase wrote:
> >
> > There seems to be something wrong with DC proof and/or your axioms.
> Actually, it's quite simple to see what.
>
> Your axiom
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & EXIST(a):a ε dom & EXIST(a):a ε cod
> > & ALL(a):[a ε dom => f1(a) ε cod]
> > & ALL(a):[a ε dom => f2(a) ε cod]
> > => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> > Axiom
> essentially states that f1 = f2 if f1 agrees with f2 on a (nonempty) SUBSET of their common domain (one might think).
>

Should be: "f1 = f2 iff f1 agrees with f2 everywhere on their common domain."

> But that is not sufficient.
>
> Hence the nonsensical result derived by Ben.
>
> But "actually" not even t h i s characterization is correct.
>
> After all, w h i c h magic ensures that the set /dom/ is actually the domain of f1 and f2?
>
> It might just be some arbitrary set, and that f1(a) e cod and f2 e cod for all x in dom might just be a coincidence.
>

Coincidence? ....

> In short, your axiom is completely bogus.
>
> And right, Tao's version differs from your formulation.
>

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
Terence Tao, "Analysis I, 3rd Ed." p.51

> He uses the notion f: X --> Y which explicitly states that f is a function with domain X and codomain Y.
>

As does my formalization:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& EXIST(a):a in dom & EXIST(a):a in cod
& ALL(a):[a in dom => f1(a) in cod]
& ALL(a):[a in dom => f2(a) in cod]

=> [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

Unlike Tao, my formalization restricts the domain and codomain to non-empty sets. I also use the word "codomain" instead of "range." Minor points IMHO..

> You approach is lacking any "connection" between a function f and its domain (and codomain).
>

"ALL(a):[a in dom => f1(a) in cod] & ALL(a):[a in dom => f2(a) in cod]" tells us that both f1 and f2 are functions with the same dom and codomain.

> Actually (in real math) the domain of a function is one of its "properties".
>
> Hence we can define an "operation" dom which delivers its domain.
>

Given "ALL(a):[a in x => f(a) in y]", it is easy to identify the function (f) and its domain (x) and codomain (y). There is no need to concoct any formal operators for these things in most math textbooks.

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, April 18, 2022 at 10:48:19 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 4:08:49 AM UTC+2, Dan Christensen wrote:
> >
> > There is no axiom [in DC Proof] that postulates the existence of any object, not even the empty set. The domain of discourse is also not assumed to be non-empty as in standard FOL. As such, there are no existential theorems, i.e. theorems of the form EXIST(a):P(a) in DC Proof.
>
> We certainly will have to ad axioms or assumptions which state the existence of some object(s).
>

Users can introduce axioms, e.g. Peano's Axioms or the Group Axioms, at the beginning of proofs.

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, April 19, 2022 at 5:50:55 AM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 10:19:52 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, April 19, 2022 at 3:46:49 AM UTC+2, Fritz Feldhase wrote:
> > >
> > > There seems to be something wrong with DC proof and/or your axioms.
> > Actually, it's quite simple to see what.
> >
> > Your axiom
> > >
> > > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > > & EXIST(a):a ε dom & EXIST(a):a ε cod
> > > & ALL(a):[a ε dom => f1(a) ε cod]
> > > & ALL(a):[a ε dom => f2(a) ε cod]
> > > => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> > >
> > essentially (!!!) states that f1 = f2 if f1 agrees with f2 on a (nonempty) SUBSET of their common domain (one might think).
> >
> Should be: "f1 = f2 if f1 agrees with f2 everywhere on their common domain."

It should be, but it isn't.

> > But that is not sufficient.
> >
> > Hence the nonsensical result derived by Ben.

Did, you get that, idiot?

But...

> > "actually" not even t h i s characterization (of your axiom) is correct..
> >
> > After all, w h i c h magic ensures that the set /dom/ is actually the domain of f1 and f2?
> >
> > It might just be some arbitrary set, and that f1(a) e cod and f2 e cod for all x in dom might just be a coincidence.
> >
> Coincidence?

Yes.

Does DC Spoof *specify* the "value" of f(x) if x !e dom(f)?

Is it even "determined"?

I.e. is f(x) = g(x) for any two functions f, g where x !e dom(f) and x !e dom(g)?

Hint:

> > In short, your axiom is completely bogus.

If you didn't notice: That was *proved* by Ben.

> > And right, Tao's version differs from your formulation.
> >
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
> Terence Tao, "Analysis I, 3rd Ed."

Hint:

> > He uses the notion f: X --> Y which explicitly states that f is a function with domain X and codomain Y.
> >
> As does my formalization

No. Your formalization doesn't do that. Actually, it c a n ' t do that.

> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a in dom & EXIST(a):a in cod
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

lol. What's the matter with you, dumbo?

Your axiom is nonsense.
Hint:

> > You approach is lacking any "connection" between a function f and its domain (and codomain).
> >
> "ALL(a):[a in dom => f1(a) in cod] & ALL(a):[a in dom => f2(a) in cod]" tells us that both f1 and f2 are functions with the same dom and codomain.

No, it doesn't.

> > Actually (in real math) the domain of a function is one of its "properties".
> >
> > Hence we can define an "operation" dom which delivers its domain.
> >
> Given "ALL(a):[a in x => f(a) in y]", it is easy to identify the function (f) and its domain (x) and codomain (y).

Nonsense, you silly crank.

> There is no need to

Shut up, idiot!

On Tuesday, April 19, 2022 at 7:08:21 AM UTC+2, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 5:50:55 AM UTC+2, Dan Christensen wrote:
> > >
> > > You approach is lacking any "connection" between a function f and its domain (and codomain).
> > >
> > "ALL(a):[a in dom => f1(a) in cod] & ALL(a):[a in dom => f2(a) in cod]" tells us that both f1 and f2 are functions with the same dom and codomain.
> >
> No, it doesn't.

Hint: Consider two functions f: {1} --> {1} with f(x) = x and g: {1, 2} --> {1, 4 } with g(x) = x^2.

Hint: This means that dom(f) =/= dom(g) and codom(f) =/= codom(g).

If dom = {1} and cod = {1}, which is entirely possible, since we are free to arbitrary chose dom and cod in your approach, then ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod], but -as just mentioned- f and g AREN'T functions with the same domain and codomain.

> > > Actually (in real math) the domain of a function is one of its "properties".
> > >
> > > Hence we can define an "operation" dom which delivers the domain of a function.
> > >
> > Given "ALL(a):[a in x => f(a) in y]", it is easy to identify the function (f) and its domain (x) and codomain (y).
> >
> Nonsense.

Hint: To be get the domain of f from your statement

ALL(a):[a in x => f(a) in y]

x would have to be unique, which is n o t the case (in general).

I already told you that

ALL(a):[a in x => f(a) in codom(f)]

holds for any x c domain(f).

Consider a function f: {1, 2, 3} --> {1, 2, 3}, i. e. a function f with domain {1, 2, 3} and codomain {1, 2, 3}.

Then

ALL(a):[a in x => f(a) in {1, 2, 3}]

holds for x = {}, x = {1}, x = {2, 3}, etc.

Now, w h i c h of these x *is* the domain of f?

Fritz Feldhase's profile photo
Fritz Feldhase
7:43 AM (16 minutes ago)
toz
On Tuesday, April 19, 2022 at 7:08:21 AM UTC+2, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 5:50:55 AM UTC+2, Dan Christensen wrote:
> > >
> > > You approach is lacking any "connection" between a function f and its domain (and codomain).
> > >
> > "ALL(a):[a in dom => f1(a) in cod] & ALL(a):[a in dom => f2(a) in cod]" tells us that both f1 and f2 are functions with the same dom and codomain.
> >
> No, it doesn't.

Hint: Consider two functions f: {1} --> {1} with f(x) = x and g: {1, 2} --> {1, 4 } with g(x) = x^2.

Hint: This means that dom(f) =/= dom(g) and codom(f) =/= codom(g).

If dom = {1} and cod = {1}, which is entirely possible, since we are free to arbitrarily choose dom and cod in your approach, then ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod], but -as just mentioned- f and g AREN'T functions with the same domain and codomain.

> > > Actually (in real math) the domain of a function is one of its "properties".
> > >
> > > Hence we can define an "operation" dom which delivers the domain of a function.
> > >
> > Given "ALL(a):[a in x => f(a) in y]", it is easy to identify the function (f) and its domain (x) and codomain (y).
> >
> Nonsense.

Hint: To be able to get the domain of f from your statement

ALL(a):[a in x => f(a) in y]

x would have to be unique, which is n o t the case (in general).

I already told you that

ALL(a):[a in x => f(a) in codom(f)]

holds for any x c domain(f).

Consider a function f: {1, 2, 3} --> {1, 2, 3}, i. e. a function f with domain {1, 2, 3} and codomain {1, 2, 3}.

Then

ALL(a):[a in x => f(a) in {1, 2, 3}]

holds for x = {}, x = {1}, x = {2, 3}, etc.

Now, w h i c h of these x *is* the domain of f?

On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:

> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a ε dom & EXIST(a):a ε cod
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Axiom
>
> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> Axiom
>

[snip]

>
> 15 f(0)=0 & g(0)=0
> Premise
>

[snip]
>
> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> Conclusion, 15
>

Thanks, Ben. I came up with a different version of your proof that makes the problem clear even more clear:

ALL(x0):[EXIST(s):[Set(s) & ALL(a):[a in s <=> a=x0]] <--- s = {x0}

=> ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0 => f=g]] <--- YIKES!

I was looking for a way to talk about the equality of a pair of functions in their common domain. What better way, I guess, than to simply say that ALL(a):[a in dom => f1(a)=f2(a)]? I could hard-code a built-in predicate FEQ(f1,f2,dom) to this effect, but I'm not convinced it would be a net benefit to users. In any case I, will be deactivating my Function Equality Axiom for now.

Dan

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

Removed troublesome Function Equality Axiom. The equality of functions f1 and f2 within a common domain can still be indicated by

ALL(a):[a in dom => f1(a)=f2(a)]

On Friday, April 15, 2022 at 2:03:12 PM UTC-4, Dan Christensen wrote:
> New version of DC Proof 2.0 released today. Includes:
>
> 1. Bug fix for Arbitrary Consequent Rule that was missing certain error conditions.
>
> 2. Re-introduced requirements for non-empty domain and codomain sets in function axioms. Adventurous users are still able to introduce their own versions of axioms at the beginning of proofs.
>
> NEW FUNCTION AXIOM (1 variable)
>
> ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
>
> & EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW
>
> => [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):ALL(a1):ALL(b):[a1 in dom & b in cod
> => [fun(a1)=b <=> (a1,b) in gra]]]]
>
>
> where
>
> dom = domain set
> cod = codomain set
> gra = graph set
> fun = function operator
>
> NEW FUNCTION EQUALITY AXIOM (1 variable)
>

REMOVED

>
>
> NEW FUNCTION SPACE AXIOM (1 variable)
>
> ALL(dom):ALL(cod):[Set(dom) & Set(cod)
>
> & EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW
>
> => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
>
>
>
> 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, April 19, 2022 at 5:25:13 PM UTC+2, Dan Christensen wrote:
>
> What better way, I guess, than to simply say that ALL(a):[a in dom => f1(a)=f2(a)]?

One might think. The problem here is that dom is not a "function" of f1 and/or f2. Its just an arbitrary set!

Actually, the following holds for any (set theoretic) functions f, g:

f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)).

If we consider "mathematical functions" (due to Bourbaki), then for any two functions f, g:

f = g <-> dom(f) = dom(g) & cod(f) = cod(g) & Ax(x e dom(f) -> f(x) = g(x)).

The second approach might be considerd an extension of the first.

So what you really, really need is an operation dom() which "delivers" the domain of a given function.

Actually, in a set theoretic context its easy to define that notion: dom(f) := {x e UUf : Ey(<x, y> e f}.

Here functions are just (defined as) certain sets of ordered pairs. Hence domain and image of a function can be determined on the basis of the function as such.

On Tuesday, April 19, 2022 at 1:35:58 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 5:25:13 PM UTC+2, Dan Christensen wrote:
> >
> > What better way, I guess, than to simply say that ALL(a):[a in dom => f1(a)=f2(a)]?
> One might think. The problem here is that dom is not a "function" of f1 and/or f2. Its just an arbitrary set!
>
> Actually, the following holds for any (set theoretic) functions f, g:
>
> f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)).
>
> If we consider "mathematical functions" (due to Bourbaki), then for any two functions f, g:
>
> f = g <-> dom(f) = dom(g) & cod(f) = cod(g) & Ax(x e dom(f) -> f(x) = g(x)).
>
> The second approach might be considerd an extension of the first.
>
> So what you really, really need is an operation dom() which "delivers" the domain of a given function.
>
> Actually, in a set theoretic context its easy to define that notion: dom(f) := {x e UUf : Ey(<x, y> e f}.
>
> Here functions are just (defined as) certain sets of ordered pairs. Hence domain and image of a function can be determined on the basis of the function as such.

Thanks, but that all seems like an inelegant kludge. I have withdrawn my Function Equality Axiom for now, but I hope to find an elegant way to avoid the bizarre result that Ben has obtained. I am hoping a minor change to the text of the axiom will do.

Dan

Ha Ha, kludge. You must be joking. Since when are
theorems kludges? This here is a theorem:

> Actually, the following holds for any (set theoretic) functions f, g:
> f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)).

Dan Christensen schrieb am Dienstag, 19. April 2022 um 22:14:08 UTC+2:
> Thanks, but that all seems like an inelegant kludge.

On Tuesday, April 19, 2022 at 10:14:08 PM UTC+2, Dan Christensen wrote:
> On Tuesday, April 19, 2022 at 1:35:58 PM UTC-4, Fritz Feldhase wrote:

Concerning the "set theoretic" approach:

> > Here functions are just (defined as) certain sets of ordered pairs. Hence domain and image of a function can be determined on the basis of the function itself.
> >
> Thanks, but that all seems like an inelegant kludge.

Huh?!

Hint: "Most math textbooks don't have formal proofs. You are doing something
not in most textbooks. However, all textbooks on mathematical logic do
include formal proofs and there's a reason they don't define function
axioms like yours." (Ben)

Indeed!

You know: "Everything should be made as simple as possible, but not simpler."

On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:

> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a ε dom & EXIST(a):a ε cod
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Axiom
>
> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> Axiom
>
> 3 Set(s) & ALL(a):[a ε s <=> a=0]
> E Spec, 2
>
> 4 Set(s)
> Split, 3
>
> 5 ALL(a):[a ε s <=> a=0]
> Split, 3
>
> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> & EXIST(a):a ε s & EXIST(a):a ε cod
> & ALL(a):[a ε s => f1(a) ε cod]
> & ALL(a):[a ε s => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 1
>
> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f1(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> U Spec, 6
>
> 8 0 ε s <=> 0=0
> U Spec, 5
>
> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
> Iff-And, 8
>
> 10 0 ε s => 0=0
> Split, 9
>
> 11 0=0 => 0 ε s
> Split, 9
>
> 12 0=0
> Reflex
>
> 13 0 ε s
> Detach, 11, 12
>
> 14 EXIST(a):a ε s
> E Gen, 13
>
> 15 f(0)=0 & g(0)=0
> Premise
>
> 16 z ε s
> Premise
>
> 17 z ε s <=> z=0
> U Spec, 5
>
> 18 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 17
>
> 19 z ε s => z=0
> Split, 18
>
> 20 z=0 => z ε s
> Split, 18
>
> 21 z=0
> Detach, 19, 16
>
> 22 0 ε s
> Substitute, 21, 16
>
> 23 f(0)=0
> Split, 15
>
> 24 g(0)=0
> Split, 15
>
> 25 f(0) ε s
> Substitute, 23, 22
>
> 26 f(z) ε s
> Substitute, 21, 25
>
> 27 ALL(a):[a ε s => f(a) ε s]
> Conclusion, 16
>
> 28 z ε s
> Premise
>
> 29 z ε s <=> z=0
> U Spec, 5
>
> 30 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 29
>
> 31 z ε s => z=0
> Split, 30
>
> 32 z=0 => z ε s
> Split, 30
>
> 33 z=0
> Detach, 31, 28
>
> 34 0 ε s
> Substitute, 33, 28
>
> 35 f(0)=0
> Split, 15
>
> 36 g(0)=0
> Split, 15
>
> 37 g(0) ε s
> Substitute, 36, 34
>
> 38 g(z) ε s
> Substitute, 33, 37
>
> 39 ALL(a):[a ε s => g(a) ε s]
> Conclusion, 28
>
> 40 ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => f2(a) ε s]
> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
> U Spec, 7
>
> 41 Set(s) & Set(s)
> & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
> U Spec, 40
>
> 42 Set(s) & Set(s)
> Join, 4, 4
>
> 43 Set(s) & Set(s) & EXIST(a):a ε s
> Join, 42, 14
>
> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> Join, 43, 14
>
> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> Join, 44, 27
>
> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> & ALL(a):[a ε s => f(a) ε s]
> & ALL(a):[a ε s => g(a) ε s]
> Join, 45, 39
>
> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
> Detach, 41, 46
>
> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
> Iff-And, 47
>
> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
> Split, 48
>
> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
> Split, 48
>
> 51 z ε s
> Premise
>
> 52 z ε s <=> z=0
> U Spec, 5
>
> 53 [z ε s => z=0] & [z=0 => z ε s]
> Iff-And, 52
>
> 54 z ε s => z=0
> Split, 53
>
> 55 z=0 => z ε s
> Split, 53
>
> 56 z=0
> Detach, 54, 51
>
> 57 f(0)=0
> Split, 15
>
> 58 g(0)=0
> Split, 15
>
> 59 z=g(0)
> Substitute, 58, 56
>
> 60 0=g(0)
> Substitute, 56, 59
>
> 61 f(0)=g(0)
> Substitute, 57, 60
>
> 62 f(z)=g(z)
> Substitute, 56, 61
>
> 63 ALL(a):[a ε s => f(a)=g(a)]
> Conclusion, 51
>
> 64 f=g
> Detach, 50, 63
>
> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> Conclusion, 15
>

Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:

65. ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
Join, 27, 39

66. ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
& f=g
Join, 65, 64

67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
=> ALL(a):[a in s => f(a) in s]
& ALL(a):[a in s => g(a) in s]
& f=g]
Conclusion, 15

Given that s={0} (line 3), this nails down functions f and g. What is there to be concerned about here? Perhaps I over-reacted in disabling the Function Equality Axiom.

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, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> >
> > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > Conclusion, 15
> >
> Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
>
> :
>
> 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> => ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> & f=g]
> Conclusion, 15
>
> Given that s={0} (line 3), this nails down functions f and g.

Huh?! This doesn't "nail down" these functions.

ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s] & s = {0}

just states

f(0) = 0 and g(0) = 0.

Hint: x e {0} <-> x = 0.

The problem with your axiom arises from the fact that NOT all functions which just agree on a single element in their common domain are identical.

> What is there to be concerned about here? Perhaps I over-reacted in disabling the Function Equality Axiom.

*sigh*

On Wednesday, April 20, 2022 at 1:39:02 AM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> > >
> > > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > Conclusion, 15
> > >
> > Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
> >
> > :
> >
> > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]
> > Conclusion, 15
> >
> > Given that s={0} (line 3), this nails down functions f and g.
> Huh?! This doesn't "nail down" these functions.
>

s is a singleton. There is only one function mapping s to itself. So the above result makes perfect sense.

[snip]

Dan

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

Your ad hoc axiom is useless, because you can
prove f=g and ~f=g. Never head of Ex Falso Quodlibet?

https://de.wikipedia.org/wiki/Ex_falso_quodlibet

Ben schrieb am Sonntag, 17. April 2022 um 23:00:09 UTC+2:
> (Reminder, in case you do have time, f' and g' are both from {0,1} and
> to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
> proof that they were equal but you've suggested that I needed to say
> more about them, but none of the lines you posted would have made the
> proof impossible.)

Dan Christensen schrieb am Mittwoch, 20. April 2022 um 16:29:29 UTC+2:
> On Wednesday, April 20, 2022 at 1:39:02 AM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> > > >
> > > > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > > Conclusion, 15
> > > >
> > > Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
> > >
> > > :
> > >
> > > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > > => ALL(a):[a in s => f(a) in s]
> > > & ALL(a):[a in s => g(a) in s]
> > > & f=g]
> > > Conclusion, 15
> > >
> > > Given that s={0} (line 3), this nails down functions f and g.
> > Huh?! This doesn't "nail down" these functions.
> >
> s is a singleton. There is only one function mapping s to itself. So the above result makes perfect sense.
>
> [snip]
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com