On Monday, August 15, 2022 at 3:46:21 AM UTC-4, Mostowski Collapse wrote:
> Well the task is to prove "literally":
>
> Surjective(f)
> ~Surjective(g)
>

No, the task was to prove:

ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]] (which can be abbreviated Surjective(f,x,x))

EXIST(a):[a in y & ALL(b):[b in x => ~g(b)=a]] (which can be abbreviated ~Surjective(g,x,y))

where x = {0}, y = {0, 1}, f: x --> x, g: x --> y and f(0)=g(0)=0

It may be possible to squeeze in some unconventional unary predicate for surjectivity as you suggest, but can I see no advantage in it.

Dan

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

Still nothing?

LMAO!

Mostowski Collapse schrieb am Montag, 15. August 2022 um 09:46:21 UTC+2:
> Well the task is to prove "literally":
>
> Surjective(f)
> ~Surjective(g)
>
> And not some other nonsense.
> The word literally means word for word, verbatim.
> I made this already clear here a few days ago:
>
> Mostowski Collapse schrieb am Montag, 8. August 2022 um 23:38:01 UTC+2:
> > What is so difficult to understand in the word " literally ", it means
> > " word for word " / " verbatim ", the task is to prove this:
> >
> > Surjective(f)
> > ~Surjective(g)
> >
> > word for word. And nothing else.
> https://groups.google.com/g/sci.logic/c/QSfRj2g1ur8/m/EqceW2QNAQAJ
> Dan Christensen schrieb am Montag, 15. August 2022 um 06:23:11 UTC+2:
> > On Sunday, August 14, 2022 at 10:43:01 PM UTC-4, Fritz Feldhase wrote:
> > > On Sunday, August 14, 2022 at 5:18:55 PM UTC+2, Dan Christensen wrote:
> > > >
> > > > Why would I adopt such an unconventional definition when there is nothing wrong with the standard one that I use? (See Tao)
> > > Tao's definition is totally nonsensical.
> > See my reply just now to your identical claim at sci.logic.
> >
> > Dan

Here is a proof you lazy ass:

https://www.rubycap.ch/dcproof17_unary.html

It proofs:

53 Surjective(f)
Detach, 19, 52

86 ~Surjective(g)
Detach, 63, 85

For the full proof see here:

----------------------------------- begin full proof ---------------------------------------------

1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
& Function(f,dom,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
Axiom

2 Set(x)
Axiom

3 Set(y)
Axiom

4 ~1=0
Axiom

5 ALL(a):[a ε x <=> a=0]
Axiom

6 ALL(a):[a ε y <=> a=0 | a=1]
Axiom

7 Function(f,x,x)
Axiom

8 Function(g,x,y)
Axiom

9 f(0)=0
Axiom

10 g(0)=0
Axiom

11 ALL(cod):ALL(f):[Set(x) & Set(cod)
& Function(f,x,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε x & f(a)=b]]]]
U Spec, 1

12 ALL(f):[Set(x) & Set(x)
& Function(f,x,x) => [Surjective(f) <=> ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]]]
U Spec, 11

13 Set(x) & Set(x)
Join, 2, 2

14 Set(x) & Set(x) & Function(f,x,x)
Join, 13, 7

15 Set(x) & Set(x)
& Function(f,x,x) => [Surjective(f) <=> ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]]
U Spec, 12

16 Surjective(f) <=> ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]
Detach, 15, 14

17 [Surjective(f) => ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]]
& [ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]] => Surjective(f)]
Iff-And, 16

18 Surjective(f) => ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]
Split, 17

19 ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]] => Surjective(f)
Split, 17

20 EXIST(b):[b ε x & ~EXIST(a):[a ε x & f(a)=b]]
Premise

21 u ε x & ~EXIST(a):[a ε x & f(a)=u]
E Spec, 20

22 u ε x
Split, 21

23 ~EXIST(a):[a ε x & f(a)=u]
Split, 21

24 ~~ALL(a):~[a ε x & f(a)=u]
Quant, 23

25 ALL(a):~[a ε x & f(a)=u]
Rem DNeg, 24

26 ~[0 ε x & f(0)=u]
U Spec, 25

27 ~~[~0 ε x | ~f(0)=u]
DeMorgan, 26

28 ~0 ε x | ~f(0)=u
Rem DNeg, 27

29 u ε x <=> u=0
U Spec, 5

30 [u ε x => u=0] & [u=0 => u ε x]
Iff-And, 29

31 u ε x => u=0
Split, 30

32 u=0 => u ε x
Split, 30

33 u=0
Detach, 31, 22

34 ~~0 ε x => ~f(0)=u
Imply-Or, 28

35 0 ε x => ~f(0)=u
Rem DNeg, 34

36 0 ε x <=> 0=0
U Spec, 5

37 [0 ε x => 0=0] & [0=0 => 0 ε x]
Iff-And, 36

38 0 ε x => 0=0
Split, 37

39 0=0 => 0 ε x
Split, 37

40 0=0
Reflex

41 0 ε x
Detach, 39, 40

42 ~f(0)=u
Detach, 35, 41

43 ~f(0)=0
Substitute, 33, 42

44 f(0)=0 & ~f(0)=0
Join, 9, 43

45 ~EXIST(b):[b ε x & ~EXIST(a):[a ε x & f(a)=b]]
Conclusion, 20
46 ~~ALL(b):~[b ε x & ~EXIST(a):[a ε x & f(a)=b]]
Quant, 45

47 ALL(b):~[b ε x & ~EXIST(a):[a ε x & f(a)=b]]
Rem DNeg, 46

48 ALL(b):~~[~b ε x | ~~EXIST(a):[a ε x & f(a)=b]]
DeMorgan, 47

49 ALL(b):[~b ε x | ~~EXIST(a):[a ε x & f(a)=b]]
Rem DNeg, 48

50 ALL(b):[~b ε x | EXIST(a):[a ε x & f(a)=b]]
Rem DNeg, 49

51 ALL(b):[~~b ε x => EXIST(a):[a ε x & f(a)=b]]
Imply-Or, 50

52 ALL(b):[b ε x => EXIST(a):[a ε x & f(a)=b]]
Rem DNeg, 51

53 Surjective(f)
Detach, 19, 52

54 ALL(cod):ALL(f):[Set(x) & Set(cod)
& Function(f,x,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε x & f(a)=b]]]]
U Spec, 1

55 ALL(f):[Set(x) & Set(y)
& Function(f,x,y) => [Surjective(f) <=> ALL(b):[b ε y => EXIST(a):[a ε x & f(a)=b]]]]
U Spec, 54

56 Set(x) & Set(y)
& Function(g,x,y) => [Surjective(g) <=> ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]]
U Spec, 55

57 Set(x) & Set(y)
Join, 2, 3

58 Set(x) & Set(y) & Function(g,x,y)
Join, 57, 8

59 Surjective(g) <=> ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]
Detach, 56, 58

60 [Surjective(g) => ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]]
& [ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]] => Surjective(g)]
Iff-And, 59

61 Surjective(g) => ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]
Split, 60

62 ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]] => Surjective(g)
Split, 60

63 ~ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]] => ~Surjective(g)
Contra, 61

64 ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]
Premise

65 1 ε y => EXIST(a):[a ε x & g(a)=1]
U Spec, 64

66 1 ε y <=> 1=0 | 1=1
U Spec, 6

67 [1 ε y => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε y]
Iff-And, 66

68 1 ε y => 1=0 | 1=1
Split, 67

69 1=0 | 1=1 => 1 ε y
Split, 67

70 1=1
Reflex

71 1=0 | 1=1
Arb Or, 70

72 1 ε y
Detach, 69, 71

73 EXIST(a):[a ε x & g(a)=1]
Detach, 65, 72

74 u ε x & g(u)=1
E Spec, 73

75 u ε x <=> u=0
U Spec, 5

76 [u ε x => u=0] & [u=0 => u ε x]
Iff-And, 75

77 u ε x => u=0
Split, 76

78 u=0 => u ε x
Split, 76

79 u ε x
Split, 74

80 g(u)=1
Split, 74

81 u=0
Detach, 77, 79

82 g(0)=1
Substitute, 81, 80

83 1=0
Substitute, 82, 10

84 ~1=0 & 1=0
Join, 4, 83

85 ~ALL(b):[b ε y => EXIST(a):[a ε x & g(a)=b]]
Conclusion, 64
86 ~Surjective(g)
Detach, 63, 85

----------------------------------- end full proof ---------------------------------------------

Dan Christensen schrieb am Montag, 15. August 2022 um 20:33:10 UTC+2:
> On Monday, August 15, 2022 at 3:46:21 AM UTC-4, Mostowski Collapse wrote:
> > Well the task is to prove "literally":
> >
> > Surjective(f)
> > ~Surjective(g)
> >
> No, the task was to prove:
>
> ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]] (which can be abbreviated Surjective(f,x,x))
>
> EXIST(a):[a in y & ALL(b):[b in x => ~g(b)=a]] (which can be abbreviated ~Surjective(g,x,y))
>
> where x = {0}, y = {0, 1}, f: x --> x, g: x --> y and f(0)=g(0)=0
>
> It may be possible to squeeze in some unconventional unary predicate for surjectivity as you suggest, but can I see no advantage in it.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Mostowski Collapse wrote:

> It proofs:
>
> 53 Surjective(f)
> Detach, 19, 52

https://cdni.russiatoday.com/files/2022.08/thumbnail/62f9f27785f54039660ce229.jpg

On Tuesday, August 16, 2022 at 3:39:06 AM UTC-4, Mostowski Collapse wrote:

[snip abuse]

> For the full proof see here:
>
> ----------------------------------- begin full proof ---------------------------------------------
>
> 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> & Function(f,dom,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> Axiom

May I suggest the simpler and more conventional:

ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
=> [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]] <---- Leave out Function predicate

I have actually found it easier to work with. Give it a try. You could have saved some axioms here (lines 7-8).

> 2 Set(x)
> Axiom
>
> 3 Set(y)
> Axiom
>
> 4 ~1=0
> Axiom
>
> 5 ALL(a):[a ε x <=> a=0]
> Axiom
>
> 6 ALL(a):[a ε y <=> a=0 | a=1]
> Axiom
>
> 7 Function(f,x,x)
> Axiom
>
> 8 Function(g,x,y)
> Axiom
>
[snip]

Dan

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

(Correction)

On Tuesday, August 16, 2022 at 1:47:32 PM UTC-4, Dan Christensen wrote:
> On Tuesday, August 16, 2022 at 3:39:06 AM UTC-4, Mostowski Collapse wrote:
>
> [snip abuse]
> > For the full proof see here:
> >
> > ----------------------------------- begin full proof ---------------------------------------------
> >
> > 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > & Function(f,dom,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> > Axiom

> May I suggest the simpler and more conventional:
> ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]] <---- Leave out Function predicate

Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]]

Think of it as defining an abbreviation for "ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]" to enhance readability.

>
> I have actually found it easier to work with. Give it a try. You could have saved some axioms here (lines 7-8).
> > 2 Set(x)
> > Axiom
> >
> > 3 Set(y)
> > Axiom
> >
> > 4 ~1=0
> > Axiom
> >
> > 5 ALL(a):[a ε x <=> a=0]
> > Axiom
> >
> > 6 ALL(a):[a ε y <=> a=0 | a=1]
> > Axiom
> >
> > 7 Function(f,x,x)
> > Axiom
> >
> > 8 Function(g,x,y)
> > Axiom
> >
> [snip]
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

More dense than kryptonite:
https://www.kryptonitelock.de/en/home.html

LMAO!

Fritz Feldhase schrieb am Dienstag, 16. August 2022 um 21:21:20 UTC+2:
> On Tuesday, August 16, 2022 at 7:32:42 PM UTC+2, Dan Christensen wrote:
>
> > May I suggest the simpler and more conventional:
> > ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> You are inceredible dense, man.

Dan Christensen schrieb am Dienstag, 16. August 2022 um 22:34:49 UTC+2:
> (Correction)
> On Tuesday, August 16, 2022 at 1:47:32 PM UTC-4, Dan Christensen wrote:
> > On Tuesday, August 16, 2022 at 3:39:06 AM UTC-4, Mostowski Collapse wrote:
> >
> > [snip abuse]
> > > For the full proof see here:
> > >
> > > ----------------------------------- begin full proof ---------------------------------------------
> > >
> > > 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > > & Function(f,dom,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> > > Axiom
>
> > May I suggest the simpler and more conventional:
> > ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]] <---- Leave out Function predicate
> Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]]
>
> Think of it as defining an abbreviation for "ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]" to enhance readability.
> >
> > I have actually found it easier to work with. Give it a try. You could have saved some axioms here (lines 7-8).
> > > 2 Set(x)
> > > Axiom
> > >
> > > 3 Set(y)
> > > Axiom
> > >
> > > 4 ~1=0
> > > Axiom
> > >
> > > 5 ALL(a):[a ε x <=> a=0]
> > > Axiom
> > >
> > > 6 ALL(a):[a ε y <=> a=0 | a=1]
> > > Axiom
> > >
> > > 7 Function(f,x,x)
> > > Axiom
> > >
> > > 8 Function(g,x,y)
> > > Axiom
> > >
> > [snip]
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Any one can use his own function axiom:

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

To get the Function(f,x,x) and Function(g,x,y) facts, from gra = { (0,0) }.

So that we can prove:

53 Surjective(f)
Detach, 19, 52
86 ~Surjective(g)
Detach, 63, 85
https://www.rubycap.ch/dcproof17_unary.html

And then a proof of:

6 ~f=g
Conclusion, 3
https://www.rubycap.ch/dcproof16_compare.html

Refuting his claim that there is no function inequality for functions with different domains.

Mostowski Collapse schrieb am Dienstag, 16. August 2022 um 23:26:56 UTC+2:
> More dense than kryptonite:
> https://www.kryptonitelock.de/en/home.html
>
> LMAO!
>
> Fritz Feldhase schrieb am Dienstag, 16. August 2022 um 21:21:20 UTC+2:
> > On Tuesday, August 16, 2022 at 7:32:42 PM UTC+2, Dan Christensen wrote:
> >
> > > May I suggest the simpler and more conventional:
> > > ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > > => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> > You are inceredible dense, man.
> Dan Christensen schrieb am Dienstag, 16. August 2022 um 22:34:49 UTC+2:
> > (Correction)
> > On Tuesday, August 16, 2022 at 1:47:32 PM UTC-4, Dan Christensen wrote:
> > > On Tuesday, August 16, 2022 at 3:39:06 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > [snip abuse]
> > > > For the full proof see here:
> > > >
> > > > ----------------------------------- begin full proof ---------------------------------------------
> > > >
> > > > 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > > > & Function(f,dom,cod) => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> > > > Axiom
> >
> > > May I suggest the simpler and more conventional:
> > > ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > > => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]] <---- Leave out Function predicate
> > Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]]
> >
> > Think of it as defining an abbreviation for "ALL(a):[a ε cod => EXIST(b):[a ε dom & f(b)=a]]" to enhance readability.
> > >
> > > I have actually found it easier to work with. Give it a try. You could have saved some axioms here (lines 7-8).
> > > > 2 Set(x)
> > > > Axiom
> > > >
> > > > 3 Set(y)
> > > > Axiom
> > > >
> > > > 4 ~1=0
> > > > Axiom
> > > >
> > > > 5 ALL(a):[a ε x <=> a=0]
> > > > Axiom
> > > >
> > > > 6 ALL(a):[a ε y <=> a=0 | a=1]
> > > > Axiom
> > > >
> > > > 7 Function(f,x,x)
> > > > Axiom
> > > >
> > > > 8 Function(g,x,y)
> > > > Axiom
> > > >
> > > [snip]
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, August 16, 2022 at 5:32:02 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:

[snip]

> So that we can prove:
> 53 Surjective(f)
> Detach, 19, 52
> 86 ~Surjective(g)
> Detach, 63, 85
> https://www.rubycap.ch/dcproof17_unary.html
>
> And then a proof of:
>
> 6 ~f=g
> Conclusion, 3
> https://www.rubycap.ch/dcproof16_compare.html
>

At that link:

1 Surjective(f)
Axiom

2 ~Surjective(g)
Axiom

3 f=g
Premise

4 Surjective(g)
Substitute, 3, 1

5 Surjective(g) & ~Surjective(g)
Join, 4, 2

6 ~f=g
Conclusion, 3

Huh???

> Refuting his claim that there is no function inequality for functions with different domains.

Ummm... Not really, Jan Burse.

THEOREM

~EXIST(a):EXIST(b):[P(a) & ~P(b) & a=b]

Where P is ANY unary predicate.

PROOF

Suppose to the contrary...

1 P(x) & ~P(y) & x=y
Premise

2 P(x)
Split, 1

3 ~P(y)
Split, 1

4 x=y
Split, 1

5 ~P(x)
Substitute, 4, 3

6 P(x) & ~P(x)
Join, 2, 5

As required:

7 ~EXIST(a):EXIST(b):[P(a) & ~P(b) & a=b]
Conclusion, 1

Get it? Do keep trying, Jan Burse. (Hee, hee!)

Dan

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

Whats the problem? Now continue your proof,
you will get this here:

9 ALL(a):ALL(b):[P(a) & ~P(b) => ~a=b]
Rem DNeg, 8

Which is exactly what I proved here, using
P=Surjective and a=f and b=g:

> 6 ~f=g
> Conclusion, 3
> https://www.rubycap.ch/dcproof16_compare.html

----------------- continuation of Dan O Matik ----------------------

1 ~EXIST(a):EXIST(b):[P(a) & ~P(b) & a=b]
Axiom

2 ~~ALL(a):~EXIST(b):[P(a) & ~P(b) & a=b]
Quant, 1

3 ALL(a):~EXIST(b):[P(a) & ~P(b) & a=b]
Rem DNeg, 2

4 ALL(a):~~ALL(b):~[P(a) & ~P(a) & a=b]
Quant, 3

5 ALL(a):ALL(b):~[P(a) & ~P(b) & a=b]
Rem DNeg, 4

6 ALL(a):ALL(b):~~[~[P(a) & ~P(b)] | ~a=b]
DeMorgan, 5

7 ALL(a):ALL(b):[~[P(a) & ~P(b)] | ~a=b]
Rem DNeg, 6

8 ALL(a):ALL(b):[~~[P(a) & ~P(b)] => ~a=b]
Imply-Or, 7

9 ALL(a):ALL(b):[P(a) & ~P(b) => ~a=b]
Rem DNeg, 8

----------------- continuation of Dan O Matik ----------------------

Dan Christensen schrieb am Mittwoch, 17. August 2022 um 04:33:27 UTC+2:
> On Tuesday, August 16, 2022 at 5:32:02 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
>
> [snip]
> > So that we can prove:
> > 53 Surjective(f)
> > Detach, 19, 52
> > 86 ~Surjective(g)
> > Detach, 63, 85
> > https://www.rubycap.ch/dcproof17_unary.html
> >
> > And then a proof of:
> >
> > 6 ~f=g
> > Conclusion, 3
> > https://www.rubycap.ch/dcproof16_compare.html
> >
> At that link:
>
> 1 Surjective(f)
> Axiom
>
> 2 ~Surjective(g)
> Axiom
>
> 3 f=g
> Premise
>
> 4 Surjective(g)
> Substitute, 3, 1
>
> 5 Surjective(g) & ~Surjective(g)
> Join, 4, 2
>
> 6 ~f=g
> Conclusion, 3
>
> Huh???
> > Refuting his claim that there is no function inequality for functions with different domains.
> Ummm... Not really, Jan Burse.
>
> THEOREM
>
> ~EXIST(a):EXIST(b):[P(a) & ~P(b) & a=b]
>
> Where P is ANY unary predicate.
>
> PROOF
>
> Suppose to the contrary...
>
> 1 P(x) & ~P(y) & x=y
> Premise
>
> 2 P(x)
> Split, 1
>
> 3 ~P(y)
> Split, 1
>
> 4 x=y
> Split, 1
>
> 5 ~P(x)
> Substitute, 4, 3
>
> 6 P(x) & ~P(x)
> Join, 2, 5
>
> As required:
>
> 7 ~EXIST(a):EXIST(b):[P(a) & ~P(b) & a=b]
> Conclusion, 1
>
> Get it? Do keep trying, Jan Burse. (Hee, hee!)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, August 17, 2022 at 10:08:41 AM UTC-4, Mostowski Collapse wrote:
> Whats the problem?

The problem may your wonky definition of a unary predicate for surjectivity..

From Terence Tao's definition:
"Definition 3.3.17 (Onto functions). A function f [f: X --> Y is understood] is onto (or surjective) if f(X) = Y , i.e., every element in Y comes from applying f to some element in X: For every y ∈ Y, there exists x ∈ X such that f(x) = y."
--"Analysis I," p.54

The last line:

"For every y ∈ Y, there exists x ∈ X such that f(x) = y."

It can be translated as:

ALL(y):[y ∈ Y => EXIST(x):[x ∈ X & f(x)=y]]

This can be abbreviated quite naturally as Surjective(f,X,Y). Give it a try.. And it is not the least bit wonky.

Dan

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

On Wednesday, August 17, 2022 at 6:13:23 PM UTC+2, Dan Christensen wrote:

> From Terence Tao's [corrected and slightly modified] definition:
>
> Definition 3.3.17* (Surjective functions). A function f:X --> Y is called /surjective/ if f(X) = Y, i.e., every element in Y comes from applying f to some element in X: For every y ∈ Y, there exists x ∈ X such that f(x) = y.

> The last line:
>
> "For every y ∈ Y, there exists x ∈ X such that f(x) = y.."
>
> It can be translated as:
>
> ALL(y):[y ∈ Y => EXIST(x):[x ∈ X & f(x)=y]]

A slight variant of the definition (where f is a function):

surjective(f) :<-> ALL(y):[y ∈ codom(f) => EXIST(x):[x ∈ dom(f) & f(x)=y]]

Thank you for pointing this out, that [f: X --> Y is understood],
thats exactly what I did:

1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
& Function(f,dom,cod) <---------------------------- Here
=> [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
Axiom
https://www.rubycap.ch/dcproof17_unary.html

Do you see the <---------------------------- Here arrow?
Whats wrong with you, why do you call it wonky,
when you defend it?

Lost your logic marbles again?

Dan Christensen schrieb am Mittwoch, 17. August 2022 um 18:13:23 UTC+2:
> On Wednesday, August 17, 2022 at 10:08:41 AM UTC-4, Mostowski Collapse wrote:
> > Whats the problem?
>
> The problem may your wonky definition of a unary predicate for surjectivity.
>
> From Terence Tao's definition:
> "Definition 3.3.17 (Onto functions). A function f [f: X --> Y is understood] is onto (or surjective) if f(X) = Y , i.e., every element in Y comes from applying f to some element in X: For every y ∈ Y, there exists x ∈ X such that f(x) = y."
> --"Analysis I," p.54
>
> The last line:
>
> "For every y ∈ Y, there exists x ∈ X such that f(x) = y.."
>
> It can be translated as:
>
> ALL(y):[y ∈ Y => EXIST(x):[x ∈ X & f(x)=y]]
>
> This can be abbreviated quite naturally as Surjective(f,X,Y). Give it a try. And it is not the least bit wonky.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, August 17, 2022 at 1:52:11 PM UTC-4, Mostowski Collapse wrote:
> Thank you for pointing this out, that [f: X --> Y is understood],
> thats exactly what I did:
> 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> & Function(f,dom,cod) <---------------------------- Here
> => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]

[snip]

Should have been Surjective(f,dom,cod)

Otherwise workable, but needlessly cumbersome with the Function signature. AFAICT it is only really required for function equality.

Dan

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

On Wednesday, August 17, 2022 at 9:18:29 PM UTC+2, Dan Christensen wrote:
> On Wednesday, August 17, 2022 at 1:52:11 PM UTC-4, Mostowski Collapse wrote:
> >
> > Thank you for pointing this out, that [f: X --> Y is understood],
> > thats exactly what I did:
> >
> > 1 ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod)
> > & Function(f,dom,cod) <---------------------------- Here
> > => [Surjective(f) <=> ALL(b):[b ε cod => EXIST(a):[a ε dom & f(a)=b]]]]
> >
> [snip]
>
> Should have been Surjective(f,dom,cod)
>
> Otherwise workable, but needlessly cumbersome with the Function signature.. AFAICT it is only really required for function equality.

Fuck off, you silly bastard!

The function equality of DC Proof is stil crap.
For example, how would you define:

cod(fun) = ?

So that we can for example prove:

~cod(g)={0}

for the runing example g: {0} --> {0,1} and g(0)=0.

See my reply just now to your nearly identical posting at sci.logic.

Dan

On Thursday, August 18, 2022 at 5:31:31 AM UTC-4, Mostowski Collapse wrote:
> The function equality of DC Proof is stil crap.
> For example, how would you define:
>
> cod(fun) = ?
>
> So that we can for example prove:
>
> ~cod(g)={0}
>
> for the runing example g: {0} --> {0,1} and g(0)=0.

Maybe we should lookup:

Calculus: Early Transcendentals 8. Auflage
https://www.amazon.de/dp/1305272358

He has a section "Four Ways to Represent a Function"
What does this section say?

P.S.: I have very low expectations that this would settle
any formalization, we just end with another Terrence Tao?

Drinker Paradox is the biggest challenge for
Dan-O-Matik aka Wonly Man. The Drinker Paradox
is based on these two theorems from FOL:

/* Provable: Non-Empty Domain */
EXIST(x):x=x
/* Not Provable: D can be full */
EXIST(x):~D(x)

When you mode to set theory, both are flipped:

/* Not Provable: Possibly Empty Domain */
EXIST(x):(x e pub)
/* Provable: drinkers can never be full */
EXIST(x):~(x e drinkers)

Guess what? Smullyan uses the two FOL theorems.
Dan-O-Matik perverts the Drinker Paradox by not
ploughing through Smullyans proof, and uses

the flipped theorems to produce some abomination.

On Friday, October 28, 2022 at 10:51:14 AM UTC-4, Mostowski Collapse wrote:
> Drinker Paradox is the biggest challenge for

> [snip childish abuse]

> The Drinker Paradox
> is based on these two theorems from FOL:
>
> /* Provable: Non-Empty Domain */
> EXIST(x):x=x
> /* Not Provable: D can be full */
> EXIST(x):~D(x)
>
> When you mode to set theory, both are flipped:
>
> /* Not Provable: Possibly Empty Domain */
> EXIST(x):(x e pub)
> /* Provable: drinkers can never be full */
> EXIST(x):~(x e drinkers)
>
> Guess what? Smullyan uses the two FOL theorems.
> Dan-O-Matik perverts the Drinker Paradox by not
> ploughing through Smullyans proof, and uses
> the flipped theorems to produce some abomination.

Poor Jan Burse really seems to be losing it here. (Hee, hee! )

Again, Smullyans original scenario was stated informally as:

"There exists someone such that whenever he (or she) drinks, everybody drinks." (Admittedly no mention of a pub.)
--"What is the name of this book?" p. 210

I originally proved: EXIST(x):[x in drinker => ALL(y):[y in pub => y in drinkers]].

The introduction of the set pub here made for an humorous visual, but ANY proposition (be it true or false) could be substituted for "ALL(y):[y in pub => y in drinkers]" here. Deal with it, 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

Thats the result "There exists someone such that whenever he (or she)
drinks, everybody drinks." But he also did publish a proof:

> Case 1:
> =============================
> Let us look at it this way: Either it is true that everybody
> drinks or it isn't. Suppose it is true that everybody drinks.
> Then take any person—call him Jim. Since everybody
> drinks and Jim drinks, then it is true that if Jim drinks
> then everybody drinks. So there is at least one person—
> namely Jim—such that if he drinks then everybody drinks.
>
> Case 2:
> =============================
> Suppose, however, that it is not true that everybody drinks;
> what then? Well, in that case there is at least one person—
> call him Jim—who doesn't drink. Since it is false that Jim
> drinks, then it is true that if Jim drinks, everybody drinks.
> So again there is a person—namely Jim—such that if he drinks,
> everybody drinks.
>
> https://archive.org/details/whatisnameofthis00smul/page/210/mode/2up

Where do you replicated this proof? You cannot replicate
this proof with y in drinkers, because ALL(y):[y in drinkers]

never happens. Also Smullyan had no y in pub which
you already admitted elsewhere.

Dan Christensen schrieb am Freitag, 28. Oktober 2022 um 19:01:15 UTC+2:
> On Friday, October 28, 2022 at 10:51:14 AM UTC-4, Mostowski Collapse wrote:
> > Drinker Paradox is the biggest challenge for
> > [snip childish abuse]
> > The Drinker Paradox
> > is based on these two theorems from FOL:
> >
> > /* Provable: Non-Empty Domain */
> > EXIST(x):x=x
> > /* Not Provable: D can be full */
> > EXIST(x):~D(x)
> >
> > When you mode to set theory, both are flipped:
> >
> > /* Not Provable: Possibly Empty Domain */
> > EXIST(x):(x e pub)
> > /* Provable: drinkers can never be full */
> > EXIST(x):~(x e drinkers)
> >
> > Guess what? Smullyan uses the two FOL theorems.
> > Dan-O-Matik perverts the Drinker Paradox by not
> > ploughing through Smullyans proof, and uses
> > the flipped theorems to produce some abomination.
> Poor Jan Burse really seems to be losing it here. (Hee, hee! )
>
> Again, Smullyans original scenario was stated informally as:
>
> "There exists someone such that whenever he (or she) drinks, everybody drinks." (Admittedly no mention of a pub.)
> --"What is the name of this book?" p. 210
>
> I originally proved: EXIST(x):[x in drinker => ALL(y):[y in pub => y in drinkers]].
>
> The introduction of the set pub here made for an humorous visual, but ANY proposition (be it true or false) could be substituted for "ALL(y):[y in pub => y in drinkers]" here. Deal with it, 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

If your nonsense and Smullyans Drinker Paradox were the
same, then you could not only prove this here:

/* Some Nonsense you invented already in 2014 1) */
Ex:[x in S => Q]

But also this here:

/* Not Provable in FOL */
Ex:[D(x) => Q]

How comes, can you explain why the second formula is
not provable and your first formula is provable? Does your
first formula use some assumptions that Smullyan doesn't use?

1) In 2014 we find this Nonsense by Dan Christensen:
https://groups.google.com/g/sci.math/c/mLv3DorRtpQ/m/H_l_0S9rtWgJ

2) In 2015 people told him already that it is nonsense on MSE:
https://math.stackexchange.com/questions/1186282/help-with-generalized-drinkers-paradox-exists-xdx-implies-q

Mostowski Collapse schrieb am Freitag, 28. Oktober 2022 um 21:00:42 UTC+2:
> Thats the result "There exists someone such that whenever he (or she)
> drinks, everybody drinks." But he also did publish a proof:
>
> > Case 1:
> > =============================
> > Let us look at it this way: Either it is true that everybody
> > drinks or it isn't. Suppose it is true that everybody drinks.
> > Then take any person—call him Jim. Since everybody
> > drinks and Jim drinks, then it is true that if Jim drinks
> > then everybody drinks. So there is at least one person—
> > namely Jim—such that if he drinks then everybody drinks.
> >
> > Case 2:
> > =============================
> > Suppose, however, that it is not true that everybody drinks;
> > what then? Well, in that case there is at least one person—
> > call him Jim—who doesn't drink. Since it is false that Jim
> > drinks, then it is true that if Jim drinks, everybody drinks.
> > So again there is a person—namely Jim—such that if he drinks,
> > everybody drinks.
> >
> > https://archive.org/details/whatisnameofthis00smul/page/210/mode/2up
>
> Where do you replicated this proof? You cannot replicate
> this proof with y in drinkers, because ALL(y):[y in drinkers]
>
> never happens. Also Smullyan had no y in pub which
> you already admitted elsewhere.
> Dan Christensen schrieb am Freitag, 28. Oktober 2022 um 19:01:15 UTC+2:
> > On Friday, October 28, 2022 at 10:51:14 AM UTC-4, Mostowski Collapse wrote:
> > > Drinker Paradox is the biggest challenge for
> > > [snip childish abuse]
> > > The Drinker Paradox
> > > is based on these two theorems from FOL:
> > >
> > > /* Provable: Non-Empty Domain */
> > > EXIST(x):x=x
> > > /* Not Provable: D can be full */
> > > EXIST(x):~D(x)
> > >
> > > When you mode to set theory, both are flipped:
> > >
> > > /* Not Provable: Possibly Empty Domain */
> > > EXIST(x):(x e pub)
> > > /* Provable: drinkers can never be full */
> > > EXIST(x):~(x e drinkers)
> > >
> > > Guess what? Smullyan uses the two FOL theorems.
> > > Dan-O-Matik perverts the Drinker Paradox by not
> > > ploughing through Smullyans proof, and uses
> > > the flipped theorems to produce some abomination.
> > Poor Jan Burse really seems to be losing it here. (Hee, hee! )
> >
> > Again, Smullyans original scenario was stated informally as:
> >
> > "There exists someone such that whenever he (or she) drinks, everybody drinks." (Admittedly no mention of a pub.)
> > --"What is the name of this book?" p. 210
> >
> > I originally proved: EXIST(x):[x in drinker => ALL(y):[y in pub => y in drinkers]].
> >
> > The introduction of the set pub here made for an humorous visual, but ANY proposition (be it true or false) could be substituted for "ALL(y):[y in pub => y in drinkers]" here. Deal with it, 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 Friday, October 28, 2022 at 4:10:33 PM UTC-4, Mostowski Collapse wrote:
> If your nonsense and Smullyans Drinker Paradox were the
> same, then you could not only prove this here:
>
> /* Some Nonsense you invented already in 2014 1) */
> Ex:[x in S => Q]
>
> But also this here:
>
> /* Not Provable in FOL */
> Ex:[D(x) => Q]
>

I don't know if it is or not. And don't care. I have a proof that is more accessible to math students that uses familiar set notation. Must be frustrating as hell for you, 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

Could you please show us numbers, where you
don't assume a non-empty domain, like here,
from DC Poops menu item:

1 Set(n)
Axiom

2 1 ε n
Axiom

And then do this proof:

> Euclid's theorem is a fundamental statement in
> number theory that asserts that there are infinitely
> many prime numbers.
https://en.wikipedia.org/wiki/Euclid's_theorem

We can say a mathematical theory does not
have the non-empty domain assumption
if we cannot prove EXIST(x):x=x. But this is

already the case (in DC Proof) for:

1 Set(n)
Axiom

It implies:

9 EXIST(x):x=x
Rem DNeg, 8

So are there any mathematical theories that
don't share the non-empty domain assumption?
It doesn't matter whether they are

explicit or implicit. It only matters whether
mathematics works with theories T such
that T |/- EXIST(x):x=x ?

If some such really exists, then a tool like
DC Proof would make sense. Otherwise its
a useless feature.

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

1 Set(n)
Axiom

2 ~EXIST(x):x=x
Premise

3 ~~ALL(x):~x=x
Quant, 2

4 ALL(x):~x=x
Rem DNeg, 3

5 ~n=n
U Spec, 4

6 n=n
Reflex

7 ~n=n & n=n
Join, 5, 6

8 ~~EXIST(x):x=x
Conclusion, 2

9 EXIST(x):x=x
Rem DNeg, 8

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

Mostowski Collapse schrieb am Montag, 31. Oktober 2022 um 17:04:19 UTC+1:
> Could you please show us numbers, where you
> don't assume a non-empty domain, like here,
> from DC Poops menu item:
>
> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom
>
> And then do this proof:
>
> > Euclid's theorem is a fundamental statement in
> > number theory that asserts that there are infinitely
> > many prime numbers.
> https://en.wikipedia.org/wiki/Euclid's_theorem