Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
>> Dan Christensen writes:
>
> See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm

And in what sense does this address any of the points in the post you
replied to? If you don't want to discuss it, that's fine, but don't
reply "see here" as if anything there is new.

--
Ben.

On Thursday, April 21, 2022 at 11:50:29 AM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
> >> Dan Christensen writes:
> >>
> >
> > See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm

> Please remove my name from your website -- both in file names and in any
> pages where you might have used it.
>
> Also what you prove is not my theorem.

It's an original theorem AFAIK. You recently posted it here originally.

> Why would you dishonestly
> pretend that it is?

> What you show is your attempt to make
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> look less silly.
>

More readable and transparent.

> If you asked a student (your target audience I think) to write, in DC
> Proof, that the equality of all pairs of two things was a consequence of
> some predicate, they would write (I hope)
>
> ALL(x):ALL(y):[P(x,y) => x=y]
>

That should be:

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

> And I hope they would question (indeed reject) an axiom that allowed
> that predicate to be x(0)=0 & y(0)=0.
>

Don't know what you are getting at, but they should be able to easily prove:

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]
& ALL(a):[a in s => g(a) in s]
& f=g]]

For a more opaque presentation, they could, as you did, leave out "ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s]" in the final conclusion. It might cost them a mark or 2 for poor style. For the record, following is the full text of Ben's Singleton Theorem. (Sorry about the length.)

Dan

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

THEOREM

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]
& ALL(a):[a in s => g(a) in s]
& f=g]]

PROOF

Functional Equality Axiom (1 variable)

1 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)]]]
Fn Equality

Suppose...

2 EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
Premise

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

Define: s s = {x0}

4 Set(s)
Split, 3

5 ALL(a):[a in s <=> a=x0]
Split, 3

Apply Functional Equality

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

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

8 x0 in s <=> x0=x0
U Spec, 5

9 [x0 in s => x0=x0] & [x0=x0 => x0 in s]
Iff-And, 8

10 x0 in s => x0=x0
Split, 9

11 x0=x0 => x0 in s
Split, 9

12 x0=x0
Reflex

As Required:

13 x0 in s
Detach, 11, 12

As Required:

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

Prove: 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]

Suppose...

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

Prove: ALL(a):[a in s => f(a) in s]

Suppose...

16 z in s
Premise

17 z in s <=> z=x0
U Spec, 5

18 [z in s => z=x0] & [z=x0 => z in s]
Iff-And, 17

19 z in s => z=x0
Split, 18

20 z=x0 => z in s
Split, 18

21 z=x0
Detach, 19, 16

22 x0 in s
Substitute, 21, 16

23 f(x0)=x0
Split, 15

24 g(x0)=x0
Split, 15

25 f(x0) in s
Substitute, 23, 22

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

As Required:

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

Prove: ALL(a):[a in s => g(a) in s]

Suppose...

28 z in s
Premise

29 z in s <=> z=x0
U Spec, 5

30 [z in s => z=x0] & [z=x0 => z in s]
Iff-And, 29

31 z in s => z=x0
Split, 30

32 z=x0 => z in s
Split, 30

33 z=x0
Detach, 31, 28

34 x0 in s
Substitute, 33, 28

35 f(x0)=x0
Split, 15

36 g(x0)=x0
Split, 15

37 g(x0) in s
Substitute, 36, 34

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

As Required:

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

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

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

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

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

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

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

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

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

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

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

Sufficient: For f=g

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

Prove: ALL(a):[a in s => f(a)=g(a)]

Suppose...

51 z in s
Premise

52 z in s <=> z=x0
U Spec, 5

53 [z in s => z=x0] & [z=x0 => z in s]
Iff-And, 52

54 z in s => z=x0
Split, 53

55 z=x0 => z in s
Split, 53

56 z=x0
Detach, 54, 51

57 f(x0)=x0
Split, 15

58 g(x0)=x0
Split, 15

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

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

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

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

As Required:

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

64 f=g
Detach, 50, 63

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

As Required:

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

As Required:

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]
& ALL(a):[a in s => g(a) in s]
& f=g]]
Conclusion, 2

You can also prove ALL(a):[a e s => f(a) e s] and
ALL(a):[a e s => f(a) e s], and elimate it from your
theorem. I already posted a file domex.html a

few days ago here on sci.math. Now do the same
with f(x)=y & g(x)=y, and you will arrive at the following:

f ~ g <=> EXIST(x):EXIST(y):[f(x)=y & g(x)=y]

Which basically says two functions are equal if
the intersect, which of course nonsense,

not equality as we understand it, therefore your
ad hoc axiom is nonsense.

Dan Christensen schrieb am Donnerstag, 21. April 2022 um 18:37:36 UTC+2:
> On Thursday, April 21, 2022 at 11:50:29 AM UTC-4, Ben wrote:
> > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >
> > > On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
> > >> Dan Christensen writes:
> > >>
> > >
> > > See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm
>
> > Please remove my name from your website -- both in file names and in any
> > pages where you might have used it.
> >
> > Also what you prove is not my theorem.
> It's an original theorem AFAIK. You recently posted it here originally.
> > Why would you dishonestly
> > pretend that it is?
>
> > What you show is your attempt to make
> > ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > look less silly.
> >
> More readable and transparent.
> > If you asked a student (your target audience I think) to write, in DC
> > Proof, that the equality of all pairs of two things was a consequence of
> > some predicate, they would write (I hope)
> >
> > ALL(x):ALL(y):[P(x,y) => x=y]
> >
> That should be:
> 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)]]]
> > And I hope they would question (indeed reject) an axiom that allowed
> > that predicate to be x(0)=0 & y(0)=0.
> >
> Don't know what you are getting at, but they should be able to easily prove:
>
> 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]
> & ALL(a):[a in s => g(a) in s]
> & f=g]]
>
> For a more opaque presentation, they could, as you did, leave out "ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s]" in the final conclusion. It might cost them a mark or 2 for poor style. For the record, following is the full text of Ben's Singleton Theorem. (Sorry about the length..)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
> THEOREM
>
> 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]
> & ALL(a):[a in s => g(a) in s]
> & f=g]]
>
> PROOF
>
> Functional Equality Axiom (1 variable)
> 1 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)]]]
> Fn Equality
>
>
> Suppose...
>
> 2 EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> Premise
>
> 3 Set(s) & ALL(a):[a in s <=> a=x0]
> E Spec, 2
>
>
> Define: s s = {x0}
>
> 4 Set(s)
> Split, 3
>
> 5 ALL(a):[a in s <=> a=x0]
> Split, 3
>
> Apply Functional Equality
> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> & EXIST(a):a in s & EXIST(a):a in cod
> & ALL(a):[a in s => f1(a) in cod]
> & ALL(a):[a in s => f2(a) in cod]
> => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> U Spec, 1
>
> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a in s & EXIST(a):a in s
> & ALL(a):[a in s => f1(a) in s]
> & ALL(a):[a in s => f2(a) in s]
> => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> U Spec, 6
>
> 8 x0 in s <=> x0=x0
> U Spec, 5
>
> 9 [x0 in s => x0=x0] & [x0=x0 => x0 in s]
> Iff-And, 8
>
> 10 x0 in s => x0=x0
> Split, 9
>
> 11 x0=x0 => x0 in s
> Split, 9
>
> 12 x0=x0
> Reflex
>
> As Required:
>
> 13 x0 in s
> Detach, 11, 12
>
> As Required:
>
> 14 EXIST(a):a in s
> E Gen, 13
>
>
> Prove: 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]
> Suppose...
>
> 15 f(x0)=x0 & g(x0)=x0
> Premise
>
>
> Prove: ALL(a):[a in s => f(a) in s]
>
> Suppose...
>
> 16 z in s
> Premise
>
> 17 z in s <=> z=x0
> U Spec, 5
>
> 18 [z in s => z=x0] & [z=x0 => z in s]
> Iff-And, 17
>
> 19 z in s => z=x0
> Split, 18
>
> 20 z=x0 => z in s
> Split, 18
>
> 21 z=x0
> Detach, 19, 16
>
> 22 x0 in s
> Substitute, 21, 16
>
> 23 f(x0)=x0
> Split, 15
>
> 24 g(x0)=x0
> Split, 15
>
> 25 f(x0) in s
> Substitute, 23, 22
>
> 26 f(z) in s
> Substitute, 21, 25
>
> As Required:
>
> 27 ALL(a):[a in s => f(a) in s]
> Conclusion, 16
>
>
> Prove: ALL(a):[a in s => g(a) in s]
>
> Suppose...
>
> 28 z in s
> Premise
>
> 29 z in s <=> z=x0
> U Spec, 5
>
> 30 [z in s => z=x0] & [z=x0 => z in s]
> Iff-And, 29
>
> 31 z in s => z=x0
> Split, 30
>
> 32 z=x0 => z in s
> Split, 30
>
> 33 z=x0
> Detach, 31, 28
>
> 34 x0 in s
> Substitute, 33, 28
>
> 35 f(x0)=x0
> Split, 15
>
> 36 g(x0)=x0
> Split, 15
>
> 37 g(x0) in s
> Substitute, 36, 34
>
> 38 g(z) in s
> Substitute, 33, 37
>
> As Required:
>
> 39 ALL(a):[a in s => g(a) in s]
> Conclusion, 28
>
> 40 ALL(f2):[Set(s) & Set(s)
> & EXIST(a):a in s & EXIST(a):a in s
> & ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => f2(a) in s]
> => [f=f2 <=> ALL(a):[a in s => f(a)=f2(a)]]]
> U Spec, 7
>
> 41 Set(s) & Set(s)
> & EXIST(a):a in s & EXIST(a):a in s
> & ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> => [f=g <=> ALL(a):[a in s => f(a)=g(a)]]
> U Spec, 40
>
> 42 Set(s) & Set(s)
> Join, 4, 4
> 43 Set(s) & Set(s) & EXIST(a):a in s
> Join, 42, 14
>
> 44 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> Join, 43, 14
>
> 45 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> & ALL(a):[a in s => f(a) in s]
> Join, 44, 27
>
> 46 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> & ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> Join, 45, 39
>
> 47 f=g <=> ALL(a):[a in s => f(a)=g(a)]
> Detach, 41, 46
>
> 48 [f=g => ALL(a):[a in s => f(a)=g(a)]]
> & [ALL(a):[a in s => f(a)=g(a)] => f=g]
> Iff-And, 47
>
> 49 f=g => ALL(a):[a in s => f(a)=g(a)]
> Split, 48
>
> Sufficient: For f=g
>
> 50 ALL(a):[a in s => f(a)=g(a)] => f=g
> Split, 48
>
>
> Prove: ALL(a):[a in s => f(a)=g(a)]
>
> Suppose...
>
> 51 z in s
> Premise
>
> 52 z in s <=> z=x0
> U Spec, 5
>
> 53 [z in s => z=x0] & [z=x0 => z in s]
> Iff-And, 52
>
> 54 z in s => z=x0
> Split, 53
>
> 55 z=x0 => z in s
> Split, 53
>
> 56 z=x0
> Detach, 54, 51
>
> 57 f(x0)=x0
> Split, 15
>
> 58 g(x0)=x0
> Split, 15
>
> 59 z=g(x0)
> Substitute, 58, 56
>
> 60 x0=g(x0)
> Substitute, 56, 59
>
> 61 f(x0)=g(x0)
> Substitute, 57, 60
>
> 62 f(z)=g(z)
> Substitute, 56, 61
> As Required:
>
> 63 ALL(a):[a in s => f(a)=g(a)]
> Conclusion, 51
>
> 64 f=g
> Detach, 50, 63
> 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
> As Required:
>
> 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
> As Required:
>
> 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]
> & ALL(a):[a in s => g(a) in s]
> & f=g]]
> Conclusion, 2

domex.html was here:

Here is a file domex.html, that shows as an example how you
can prove some ALL(a):[a e dom => f(a) e cod], without
having it as an axiom:
https://groups.google.com/g/sci.math/c/on3M3w_8t6Q/m/sWOSREt_BQAJ

So you only need f(x)=y & g(x)=y, and you will
get some dom and cod, and then you will get f ~ g.

LoL

Mostowski Collapse schrieb am Donnerstag, 21. April 2022 um 21:16:38 UTC+2:
> You can also prove ALL(a):[a e s => f(a) e s] and
> ALL(a):[a e s => f(a) e s], and elimate it from your
> theorem. I already posted a file domex.html a
>
> few days ago here on sci.math. Now do the same
> with f(x)=y & g(x)=y, and you will arrive at the following:
>
> f ~ g <=> EXIST(x):EXIST(y):[f(x)=y & g(x)=y]
>
> Which basically says two functions are equal if
> the intersect, which of course nonsense,
>
> not equality as we understand it, therefore your
> ad hoc axiom is nonsense.
> Dan Christensen schrieb am Donnerstag, 21. April 2022 um 18:37:36 UTC+2:
> > On Thursday, April 21, 2022 at 11:50:29 AM UTC-4, Ben wrote:
> > > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> > >
> > > > On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
> > > >> Dan Christensen writes:
> > > >>
> > > >
> > > > See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm
> >
> > > Please remove my name from your website -- both in file names and in any
> > > pages where you might have used it.
> > >
> > > Also what you prove is not my theorem.
> > It's an original theorem AFAIK. You recently posted it here originally.
> > > Why would you dishonestly
> > > pretend that it is?
> >
> > > What you show is your attempt to make
> > > ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > look less silly.
> > >
> > More readable and transparent.
> > > If you asked a student (your target audience I think) to write, in DC
> > > Proof, that the equality of all pairs of two things was a consequence of
> > > some predicate, they would write (I hope)
> > >
> > > ALL(x):ALL(y):[P(x,y) => x=y]
> > >
> > That should be:
> > 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)]]]
> > > And I hope they would question (indeed reject) an axiom that allowed
> > > that predicate to be x(0)=0 & y(0)=0.
> > >
> > Don't know what you are getting at, but they should be able to easily prove:
> >
> > 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]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> >
> > For a more opaque presentation, they could, as you did, leave out "ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s]" in the final conclusion. It might cost them a mark or 2 for poor style. For the record, following is the full text of Ben's Singleton Theorem. (Sorry about the length.)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> > THEOREM
> >
> > 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]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> >
> > PROOF
> >
> > Functional Equality Axiom (1 variable)
> > 1 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)]]]
> > Fn Equality
> >
> >
> > Suppose...
> >
> > 2 EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> > Premise
> >
> > 3 Set(s) & ALL(a):[a in s <=> a=x0]
> > E Spec, 2
> >
> >
> > Define: s s = {x0}
> >
> > 4 Set(s)
> > Split, 3
> >
> > 5 ALL(a):[a in s <=> a=x0]
> > Split, 3
> >
> > Apply Functional Equality
> > 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> > & EXIST(a):a in s & EXIST(a):a in cod
> > & ALL(a):[a in s => f1(a) in cod]
> > & ALL(a):[a in s => f2(a) in cod]
> > => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> > U Spec, 1
> >
> > 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f1(a) in s]
> > & ALL(a):[a in s => f2(a) in s]
> > => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> > U Spec, 6
> >
> > 8 x0 in s <=> x0=x0
> > U Spec, 5
> >
> > 9 [x0 in s => x0=x0] & [x0=x0 => x0 in s]
> > Iff-And, 8
> >
> > 10 x0 in s => x0=x0
> > Split, 9
> >
> > 11 x0=x0 => x0 in s
> > Split, 9
> >
> > 12 x0=x0
> > Reflex
> >
> > As Required:
> >
> > 13 x0 in s
> > Detach, 11, 12
> >
> > As Required:
> >
> > 14 EXIST(a):a in s
> > E Gen, 13
> >
> >
> > Prove: 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]
> > Suppose...
> >
> > 15 f(x0)=x0 & g(x0)=x0
> > Premise
> >
> >
> > Prove: ALL(a):[a in s => f(a) in s]
> >
> > Suppose...
> >
> > 16 z in s
> > Premise
> >
> > 17 z in s <=> z=x0
> > U Spec, 5
> >
> > 18 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 17
> >
> > 19 z in s => z=x0
> > Split, 18
> >
> > 20 z=x0 => z in s
> > Split, 18
> >
> > 21 z=x0
> > Detach, 19, 16
> >
> > 22 x0 in s
> > Substitute, 21, 16
> >
> > 23 f(x0)=x0
> > Split, 15
> >
> > 24 g(x0)=x0
> > Split, 15
> >
> > 25 f(x0) in s
> > Substitute, 23, 22
> >
> > 26 f(z) in s
> > Substitute, 21, 25
> >
> > As Required:
> >
> > 27 ALL(a):[a in s => f(a) in s]
> > Conclusion, 16
> >
> >
> > Prove: ALL(a):[a in s => g(a) in s]
> >
> > Suppose...
> >
> > 28 z in s
> > Premise
> >
> > 29 z in s <=> z=x0
> > U Spec, 5
> >
> > 30 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 29
> >
> > 31 z in s => z=x0
> > Split, 30
> >
> > 32 z=x0 => z in s
> > Split, 30
> >
> > 33 z=x0
> > Detach, 31, 28
> >
> > 34 x0 in s
> > Substitute, 33, 28
> >
> > 35 f(x0)=x0
> > Split, 15
> >
> > 36 g(x0)=x0
> > Split, 15
> >
> > 37 g(x0) in s
> > Substitute, 36, 34
> >
> > 38 g(z) in s
> > Substitute, 33, 37
> >
> > As Required:
> >
> > 39 ALL(a):[a in s => g(a) in s]
> > Conclusion, 28
> >
> > 40 ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => f2(a) in s]
> > => [f=f2 <=> ALL(a):[a in s => f(a)=f2(a)]]]
> > U Spec, 7
> >
> > 41 Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > => [f=g <=> ALL(a):[a in s => f(a)=g(a)]]
> > U Spec, 40
> >
> > 42 Set(s) & Set(s)
> > Join, 4, 4
> > 43 Set(s) & Set(s) & EXIST(a):a in s
> > Join, 42, 14
> >
> > 44 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > Join, 43, 14
> >
> > 45 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > Join, 44, 27
> >
> > 46 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > Join, 45, 39
> >
> > 47 f=g <=> ALL(a):[a in s => f(a)=g(a)]
> > Detach, 41, 46
> >
> > 48 [f=g => ALL(a):[a in s => f(a)=g(a)]]
> > & [ALL(a):[a in s => f(a)=g(a)] => f=g]
> > Iff-And, 47
> >
> > 49 f=g => ALL(a):[a in s => f(a)=g(a)]
> > Split, 48
> >
> > Sufficient: For f=g
> >
> > 50 ALL(a):[a in s => f(a)=g(a)] => f=g
> > Split, 48
> >
> >
> > Prove: ALL(a):[a in s => f(a)=g(a)]
> >
> > Suppose...
> >
> > 51 z in s
> > Premise
> >
> > 52 z in s <=> z=x0
> > U Spec, 5
> >
> > 53 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 52
> >
> > 54 z in s => z=x0
> > Split, 53
> >
> > 55 z=x0 => z in s
> > Split, 53
> >
> > 56 z=x0
> > Detach, 54, 51
> >
> > 57 f(x0)=x0
> > Split, 15
> >
> > 58 g(x0)=x0
> > Split, 15
> >
> > 59 z=g(x0)
> > Substitute, 58, 56
> >
> > 60 x0=g(x0)
> > Substitute, 56, 59
> >
> > 61 f(x0)=g(x0)
> > Substitute, 57, 60
> >
> > 62 f(z)=g(z)
> > Substitute, 56, 61
> > As Required:
> >
> > 63 ALL(a):[a in s => f(a)=g(a)]
> > Conclusion, 51
> >
> > 64 f=g
> > Detach, 50, 63
> > 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
> > As Required:
> >
> > 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
> > As Required:
> >
> > 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]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> > Conclusion, 2

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Thursday, April 21, 2022 at 11:50:29 AM UTC-4, Ben wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
>> >> Dan Christensen writes:
>> >>
>> >
>> > See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm
>
>> Please remove my name from your website -- both in file names and in any
>> pages where you might have used it.
>>
>> Also what you prove is not my theorem.
>
> It's an original theorem AFAIK. You recently posted it here
> originally.

When I looked is was your rather pointless rewriting of the conclusion.
Have you removed my name from any and all of your work?

>> Why would you dishonestly
>> pretend that it is?
>
>> What you show is your attempt to make
>> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> look less silly.
>
> More readable and transparent.
>
>> If you asked a student (your target audience I think) to write, in DC
>> Proof, that the equality of all pairs of two things was a consequence of
>> some predicate, they would write (I hope)
>>
>> ALL(x):ALL(y):[P(x,y) => x=y]
>
> That should be:
>
> 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)]]]

How could it be? Any two things should not be quantified like that nor
should the antecedent be like that. How could anyone get from "the
equality of all pairs of two things is a consequence of some predicate"
to the nonsense above? There isn't even an arbitrary predicate in your
"solution".

How about the reverse? If someone wrote (though I think it's not valid
syntax) ALL(x):ALL(y):[P(x,y) => x=y], what would that mean in English?

>> And I hope they would question (indeed reject) an axiom that allowed
>> that predicate to be x(0)=0 & y(0)=0.
>
> Don't know what you are getting at,

So I see.

> but they should be able to easily prove:
>
> 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]
> & ALL(a):[a in s => g(a) in s]
> & f=g]]
>
> For a more opaque presentation, they could, as you did, leave out
> "ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s]" in the
> final conclusion. It might cost them a mark or 2 for poor style. For
> the record, following is the full text of Ben's Singleton
> Theorem. (Sorry about the length.)

I don't think what theorems follow from your flawed axiom is really in
doubt. The issue I raised was what something of the form
ALL(x):ALL(y):[P(x,y) => x=y] means. And you said you didn't follow
what I was getting at. I'm happy to say more if you want.

And what followed was not a theorem of mine. Strange that you want to
associate my name with something I think is a silly modification to what
I wrote.

--
Ben.