Function Spaces of Empty Functions

[Dan Christensen]

THEOREM

1. On every set, there is exists a unique empty function.

ALL(x):[Set(x)

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

& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]


2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.

ALL(x):[Set(x)

=> EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs

& [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs

& ALL(f2):[f2 in fs => f2=f1]]]]

Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 ines)

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]

Whats wrong with you? Running out of medis?

Unfortunately the theorem is not correct.
You have two vacuous truths, so basically you say:

EXIST(f):ALL(g):[g = f]

You say all functions are the same.
Just replace the vacuous truth by *T* and simplify the theorem.

LMAO!

[Dan Christensen]

On Monday, March 28, 2022 at 5:34:10 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 28. März 2022 um 23:14:43 UTC+2:
> > THEOREM
> >
> > 1. On every set, there is exists a unique empty function.
> >
> > ALL(x):[Set(x)
> >
> > => EXIST(f):[ALL(a):[a in null => f(a) in x]
> >
> > & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
> >
> >
> > 2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.
> >
> > ALL(x):[Set(x)
> >
> > => EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs
> >
> > & [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs
> >
> > & ALL(f2):[f2 in fs => f2=f1]]]]
> >

> > Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 lines)

> >


> Unfortunately the theorem is not correct.
> You have two vacuous truths, so basically you say:
>
> EXIST(f):ALL(g):[g = f]
>

Maybe you didn't know, but the principle of vacuous truth is a legitimate and widely used method of proof in mathematics. Maybe you can find something about it at Wikipedia.

This is typically how you use it in DC Proof:

1. A
Premise

2. ~A => B
Arb Cons, 1

Where: Arb Cons = Arbitrary Consequent.

If you don' t like doing things the easy way, you could obtain the same result as follows:

1. A
Premise

2. ~A
Premise

3. ~B
Premise

4. A & ~A
Join, 1, 2

5. ~~B
Conclusion, 3

6. B
Rem DNeg, 5

7. ~A => B
Conclusion, 2

[Mostowski Collapse]

A proof A & ~A => B is pretty irrelevant here.
It seems you are not able to simplify formulas with
vacuous truths in it. So I will do it for you.

You proved:

ALL(x):[Set(x)
=> EXIST(f):[ALL(a):[a in null => f(a) in x]
& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

Now observe that ALL(a):[a in null => P] is
a vacuous truth. So we can replace it by TRUE.
Lets doit:

You proved:

ALL(x):[Set(x)
=> EXIST(f):[TRUE
& ALL(g):[TRUE => g=f]]]

Now everybody knows the identities [TRUE & P] === P and
that [TRUE => P] === P. So apply these identities and
lets see what we get:

You proved:

ALL(x):[Set(x)
=> EXIST(f):[ALL(g):[g=f]]]

Now since you have the Set(null) == TRUE, its one Axiom of
yours, we can instantiate your theorem by null, and we can
apply again an identity about TRUE and we get:

You proved:

EXIST(f):[ALL(g):[g=f]]]

So as I said, you proved that there is a function f that
equals any functions g. Which is utter rubbish.

LMAO!

Dan Christensen schrieb am Dienstag, 29. März 2022 um 03:43:11 UTC+2:
> ... Gibberish ...

[Dan Christensen]

See my reply today to your identical posting at sci.math

Dan

On Wednesday, March 30, 2022 at 11:50:44 AM UTC-4, Mostowski Collapse wrote:
> A proof A & ~A => B is pretty irrelevant here.
> It seems you are not able to simplify formulas with
> vacuous truths in it. So I will do it for you.
>
> You proved:

....

[Mostowski Collapse]

The error is on your side, not on Wikipedias side. Wikipedia
uses nowhere a Vacuously True only condition. They have
also the condition f ⊆ X x Y.

Its YOUR PROBLEM Dan-O-Matik. Scape goating Wikipedia
doesn't work. Its YOUR BLUNDER.

[Graham Cooper]

> This is typically how you use it in DC Proof:
>
> 1. A
> Premise
>
> 2. ~A => B
> Arb Cons, 1
>
> Where: Arb Cons = Arbitrary Consequent.

OK!

>
> If you don' t like doing things the easy way, you could obtain the same result as follows:
>

> 1. A ****************************
> Premise
>
> 2. ~A ****************************

> Premise
>
> 3. ~B
> Premise
>
> 4. A & ~A
> Join, 1, 2
>
> 5. ~~B
> Conclusion, 3
>
> 6. B
> Rem DNeg, 5
>
> 7. ~A => B
> Conclusion, 2

NOPE! your theory is INCONSISTENT!

It can prove ANYTHING! Ex Contradictine Quodlibet

[Dan Christensen]

Wrong again, Graham. Maybe you didn't know, but if the antecedent of an implication false, then the implication itself must true, but it cannot be used to infer anything about the consequent. You should learn some basic logic.

[Graham Cooper]

Bwahaha you have 2 theorems A & ~A

your theory is INCONSISTENT

This really shows what a piece of TRASH DCPoop is

[Dan Christensen]

HA, HA! So, you don't even know what a theorem is. Not surprising.

Dan

[Graham Cooper]

Boy! 1st you introduce 2 AXIOMS

1. A
2. ~A

in logic terms, this is as smart as starting up the 4WD and flooring it into the garage door!


THEN, you say A and ~A are not theorems!


What's next Dan ? *FACE PALM*

you just dig yourself deeper and deeper into a hole

[Dan Christensen]

Jeez yer dumb.

Hint: Those are NOT axioms. Look harder!

Dan

[Mostowski Collapse]

You talking about yourself, don't you?

Whats so difficult in undertstanding that:

ALL(x):[Set(x)
=> EXIST(f):[ALL(a):[a in null => f(a) in x]
& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

https://dcproof.com/EmptyFunctionsUniqueV2.htm

Implies:
EXIST(f):[ALL(g):[g=f]]]

Even a blind mole can figure this result. It is
ultra trivial. 99 out of 100 grandmothers can do that.

Dan Christensen schrieb am Sonntag, 3. April 2022 um 05:09:08 UTC+2:
> Jeez yer dumb.

[Dan Christensen]

On Sunday, April 3, 2022 at 6:40:37 AM UTC-4, Mostowski Collapse wrote:
> You talking about yourself, don't you?
>
> Whats so difficult in undertstanding that:
> ALL(x):[Set(x)
> => EXIST(f):[ALL(a):[a in null => f(a) in x]
> & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
> https://dcproof.com/EmptyFunctionsUniqueV2.htm
>
> Implies:
> EXIST(f):[ALL(g):[g=f]]]
>

This requires a proof, Jan Burse. Not your usual hand-waving nonsense, but a formal proof. Think you can do that? Didn't think so. Oh, well...

Dan

[Mostowski Collapse]

You are an Uber Moron arent you, Dan-O-Matik?
The proof was already given. The proof is of the type:

Via so called rules of replacement:
https://en.wikipedia.org/wiki/Rule_of_replacement

Whats wrong with you?

The used rules of replacement were:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.
https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

2) TRUE is Multiplicative Identity:
((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) FALSE is Additive Identity & Material Implication
((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

The used replacement steps where:

ALL(x):[Set(x)
=> EXIST(f):[ALL(a):[a in null => f(a) in x]
& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):[(R∨¬R)

& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):[(R∨¬R)
& ALL(g):[(R∨¬R) => g=f]]]

Apply 2) to get:

ALL(x):[Set(x)
=> EXIST(f):[ALL(g):[(R∨¬R) => g=f]]]

Apply 3) to get:

ALL(x):[Set(x)
=> EXIST(f):[ALL(g):[g=f]]]

Apply the Forall Instantiation rule of Natural Deduction:

[Set(null)
=> EXIST(f):[ALL(g):[g=f]]]

Apply Modus Ponens of Natural Deduction with your Set(null) Axiom:

EXIST(f):[ALL(g):[g=f]]]

[Mostowski Collapse]

Ok, here is the first part, its called idiot.html.
Its the proof of f=g. Do you want me to post also
idiot2.html, the proof of ~f=g, for the same functions

f(null)=null
g(null)=one

, or can you do it by yourself?


1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a ε
dom => f(a) ε dom] & ALL(a):[a ε dom => g(a) ε dom] => [f=g <=>
ALL(a):[a ε dom => f(a)=g(a)]]]
Axiom

2 Set(null)
Axiom

3 ALL(a):~a ε null
Axiom

4 f(null)=null
Axiom

5 g(null)=one
Axiom

6 ~ALL(a):[a ε null => f(a) ε null]
Premise

7 ~~EXIST(a):~[a ε null => f(a) ε null]
Quant, 6

8 EXIST(a):~[a ε null => f(a) ε null]
Rem DNeg, 7

9 ~[b ε null => f(b) ε null]
E Spec, 8

10 ~~[b ε null & ~f(b) ε null]
Imply-And, 9

11 b ε null & ~f(b) ε null
Rem DNeg, 10

12 ~b ε null
U Spec, 3

13 b ε null
Split, 11

14 ~f(b) ε null
Split, 11

15 ~b ε null & b ε null
Join, 12, 13

16 ~~ALL(a):[a ε null => f(a) ε null]
Conclusion, 6

17 ALL(a):[a ε null => f(a) ε null]
Rem DNeg, 16

18 ~ALL(a):[a ε null => g(a) ε null]
Premise

19 ~~EXIST(a):~[a ε null => g(a) ε null]
Quant, 18

20 EXIST(a):~[a ε null => g(a) ε null]
Rem DNeg, 19

21 ~[c ε null => g(c) ε null]
E Spec, 20

22 ~~[c ε null & ~g(c) ε null]
Imply-And, 21

23 c ε null & ~g(c) ε null
Rem DNeg, 22

24 ~c ε null
U Spec, 3

25 c ε null
Split, 23

26 ~g(c) ε null
Split, 23

27 ~c ε null & c ε null
Join, 24, 25

28 ~~ALL(a):[a ε null => g(a) ε null]
Conclusion, 18

29 ALL(a):[a ε null => g(a) ε null]
Rem DNeg, 28

30 Set(null) & Set(null)
Join, 2, 2

31 Set(null) & Set(null)
& ALL(a):[a ε null => f(a) ε null]
Join, 30, 17

32 Set(null) & Set(null)
& ALL(a):[a ε null => f(a) ε null]
& ALL(a):[a ε null => g(a) ε null]
Join, 31, 29

33 ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a ε null =>
f(a) ε null] & ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε
null => f(a)=g(a)]]]
U Spec, 1

34 ALL(f):ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε
null] & ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]
U Spec, 33

35 ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] &
ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]
U Spec, 34

36 Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] &
ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null => f(a)=g(a)]]
U Spec, 35

37 f=g <=> ALL(a):[a ε null => f(a)=g(a)]
Detach, 36, 32

38 ~ALL(a):[a ε null => f(a)=g(a)]
Premise

39 ~~EXIST(a):~[a ε null => f(a)=g(a)]
Quant, 38

40 EXIST(a):~[a ε null => f(a)=g(a)]
Rem DNeg, 39

41 ~[d ε null => f(d)=g(d)]
E Spec, 40

42 ~~[d ε null & ~f(d)=g(d)]
Imply-And, 41

43 d ε null & ~f(d)=g(d)
Rem DNeg, 42

44 ~d ε null
U Spec, 3

45 d ε null
Split, 43

46 ~f(d)=g(d)
Split, 43

47 ~d ε null & d ε null
Join, 44, 45

48 ~~ALL(a):[a ε null => f(a)=g(a)]
Conclusion, 38

49 ALL(a):[a ε null => f(a)=g(a)]
Rem DNeg, 48

50 [f=g => ALL(a):[a ε null => f(a)=g(a)]]
& [ALL(a):[a ε null => f(a)=g(a)] => f=g]
Iff-And, 37

51 f=g => ALL(a):[a ε null => f(a)=g(a)]
Split, 50

52 ALL(a):[a ε null => f(a)=g(a)] => f=g
Split, 50

53 f=g
Detach, 52, 49


Dan Christensen schrieb:
> THEOREM
>
> 1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) &
> ALL(a):[a e dom => f(a) e cod] & ALL(a):[a e dom => g(a) e cod]
> => [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]
> Axiom
>
> 2 Set(null)
> Axiom
>
> 3 ALL(a):~a ε null
> Axiom
https://dcproof.com/EmptyFunctionsUniqueV3.htm

[Mostowski Collapse]

We are waiting, still no ~f=g. Ok here is a further hint:

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:

1 f(null)=null
Axiom

2 ALL(a):[a ε one <=> a=null]
Axiom

3 ~ALL(a):[a ε one => f(a) ε one]
Premise

4 ~~EXIST(a):~[a ε one => f(a) ε one]
Quant, 3

5 EXIST(a):~[a ε one => f(a) ε one]
Rem DNeg, 4

6 ~[b ε one => f(b) ε one]
E Spec, 5

7 ~~[b ε one & ~f(b) ε one]
Imply-And, 6

8 b ε one & ~f(b) ε one
Rem DNeg, 7

9 b ε one <=> b=null
U Spec, 2

10 [b ε one => b=null] & [b=null => b ε one]
Iff-And, 9

11 b ε one => b=null
Split, 10

12 b=null => b ε one
Split, 10

13 b ε one
Split, 8

14 ~f(b) ε one
Split, 8

15 b=null
Detach, 11, 13

16 ~f(null) ε one
Substitute, 15, 14

17 ~null ε one
Substitute, 1, 16

18 null ε one <=> null=null
U Spec, 2

19 [null ε one => null=null] & [null=null => null ε one]
Iff-And, 18

20 null ε one => null=null
Split, 19

21 null=null => null ε one
Split, 19

22 null=null
Reflex

23 null ε one
Detach, 21, 22

24 ~null ε one & null ε one
Join, 17, 23

25 ~~ALL(a):[a ε one => f(a) ε one]
Conclusion, 3

26 ALL(a):[a ε one => f(a) ε one]
Rem DNeg, 25

Hope this helps...

[Mostowski Collapse]

For the counter example, where we already proved
in the file idiot.html that f=g:

f(null)=null
g(null)=one

In a a file idiot2.html, you only need to set one={null}
and two={null,one} and then prove:

ALL(a):[a e one => f(a) e two]
ALL(a):[a e one => g(a) e two]
~ALL(a):[a e one => f(a)=g(a)]

You then get ~f=g. Joining you get f=g & ~f=g.
We are waiting Dan-O-Matik. Too difficult for DC poop?

[Dan Christensen]

On Sunday, April 10, 2022 at 5:33:56 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Sonntag, 10. April 2022 um 00:58:50 UTC+2:

> > > Ok, here is the first part, its called idiot.html.
> > > Its the proof of f=g. Do you want me to post also
> > > idiot2.html, the proof of ~f=g, for the same functions
> > >

EXAMPLE 1 (f=g)

> > >
> > > 1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a ε
> > > dom => f(a) ε dom] & ALL(a):[a ε dom => g(a) ε dom] => [f=g <=>
> > > ALL(a):[a ε dom => f(a)=g(a)]]]
> > > Axiom
> > >
> > > 2 Set(null)
> > > Axiom
> > >
> > > 3 ALL(a):~a ε null
> > > Axiom
> > >

Defines null, the empty set.

Here you applied the definition the equality of functions for domain = codomain = null.

Both f and g are empty functions and are equal.

[snip]

EXAMPLE 2 (f=/=g)

> > > f(null)=null
> > > g(null)=one
> > >

Annother example with a different domain! Whatever domain you may have in mind here (it must have { } as an element), you will have f=/=g since f(null)=/=g(null).

> In a a file idiot2.html, you only need to set one={null}
> and two={null,one} and then prove:
>
> ALL(a):[a e one => f(a) e two]
> ALL(a):[a e one => g(a) e two]
> ~ALL(a):[a e one => f(a)=g(a)]
>
> You then get ~f=g. Joining you get f=g & ~f=g.

Jeez, yer dumb, Jan Burse! Some functions are equal (as in your first example), other functions are NOT equal (as in your 2nd example).

[Mostowski Collapse]

You still dont believe your theorems reduce to:

EXIST(g):ALL(f):[g = f]
ALL(f1):ALL(f2):[f1 = f2]

Here is one more hint:

You can use any pair of functions, you will always be able to prove
them equal. For example using a binary version of your ad hoc axiom 1
and your beloved Peano axioms, you will be able to prove:

add = mul

Simply because these formulas are vacuously true:

ALL(a):ALL(b):[a e null & b e null => add(a,b) e cod]
ALL(a):ALL(b):[a e null & b e null => mul(a,b) e cod]
ALL(a):ALL(b):[a e null & b e null => add(a,b) = mul(a,b)]

Got it Dumbo?

LMAO!

[Mostowski Collapse]

Ok here is a proof called allsame.html, we only
use these axioms (I fixed a bug in my old idiot.html,
axiom 1 now looks a little better, its now the same as Dans):

1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) &

ALL(a):[a ε dom => f(a) ε cod] &
ALL(a):[a ε dom => g(a) ε cod]

=> [f=g <=> ALL(a):[a ε dom => f(a)=g(a)]]]
Axiom

2 Set(null)
Axiom

3 ALL(a):~a ε null
Axiom

And we then prove:

59 ALL(f):ALL(g):f=g
Rem DNeg, 58

Here is the full proof:

1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a ε dom

=> f(a) ε cod] & ALL(a):[a ε dom => g(a) ε cod] => [f=g <=> ALL(a):[a ε

dom => f(a)=g(a)]]]
Axiom

2 Set(null)
Axiom

3 ALL(a):~a ε null
Axiom

4 ~f=g
Premise

5 ~ALL(a):[a ε null => f(a) ε null]
Premise

6 ~~EXIST(a):~[a ε null => f(a) ε null]
Quant, 5

7 EXIST(a):~[a ε null => f(a) ε null]
Rem DNeg, 6

8 ~[b ε null => f(b) ε null]
E Spec, 7

9 ~~[b ε null & ~f(b) ε null]
Imply-And, 8

10 b ε null & ~f(b) ε null
Rem DNeg, 9

11 ~b ε null
U Spec, 3

12 b ε null
Split, 10

13 ~f(b) ε null
Split, 10

14 ~b ε null & b ε null
Join, 11, 12

15 ~~ALL(a):[a ε null => f(a) ε null]
Conclusion, 5

16 ALL(a):[a ε null => f(a) ε null]
Rem DNeg, 15

17 ~ALL(a):[a ε null => g(a) ε null]
Premise

18 ~~EXIST(a):~[a ε null => g(a) ε null]
Quant, 17

19 EXIST(a):~[a ε null => g(a) ε null]
Rem DNeg, 18

20 ~[c ε null => g(c) ε null]
E Spec, 19

21 ~~[c ε null & ~g(c) ε null]
Imply-And, 20

22 c ε null & ~g(c) ε null
Rem DNeg, 21

23 ~c ε null
U Spec, 3

24 c ε null
Split, 22

25 ~g(c) ε null
Split, 22

26 ~c ε null & c ε null
Join, 23, 24

27 ~~ALL(a):[a ε null => g(a) ε null]
Conclusion, 17

28 ALL(a):[a ε null => g(a) ε null]
Rem DNeg, 27

29 Set(null) & Set(null)
Join, 2, 2

30 Set(null) & Set(null)

& ALL(a):[a ε null => f(a) ε null]

Join, 29, 16

31 Set(null) & Set(null)
& ALL(a):[a ε null => f(a) ε null]

& ALL(a):[a ε null => g(a) ε null]

Join, 30, 28

32 ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a ε null =>
f(a) ε cod] & ALL(a):[a ε null => g(a) ε cod] => [f=g <=> ALL(a):[a ε

null => f(a)=g(a)]]]
U Spec, 1

33 ALL(f):ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε

null] & ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]

U Spec, 32

34 ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] &

ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]
U Spec, 33

35 Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] & ALL(a):[a

ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null => f(a)=g(a)]]
U Spec, 34

36 f=g <=> ALL(a):[a ε null => f(a)=g(a)]
Detach, 35, 31

37 ~ALL(a):[a ε null => f(a)=g(a)]
Premise

38 ~~EXIST(a):~[a ε null => f(a)=g(a)]
Quant, 37

39 EXIST(a):~[a ε null => f(a)=g(a)]
Rem DNeg, 38

40 ~[d ε null => f(d)=g(d)]
E Spec, 39

41 ~~[d ε null & ~f(d)=g(d)]
Imply-And, 40

42 d ε null & ~f(d)=g(d)
Rem DNeg, 41

43 ~d ε null
U Spec, 3

44 d ε null
Split, 42

45 ~f(d)=g(d)
Split, 42

46 ~d ε null & d ε null
Join, 43, 44

47 ~~ALL(a):[a ε null => f(a)=g(a)]
Conclusion, 37

48 ALL(a):[a ε null => f(a)=g(a)]
Rem DNeg, 47

49 [f=g => ALL(a):[a ε null => f(a)=g(a)]]

& [ALL(a):[a ε null => f(a)=g(a)] => f=g]

Iff-And, 36

50 f=g => ALL(a):[a ε null => f(a)=g(a)]

Split, 49

51 ALL(a):[a ε null => f(a)=g(a)] => f=g
Split, 49

52 f=g
Detach, 51, 48

53 f=g & ~f=g
Join, 52, 4

54 ~EXIST(f):EXIST(g):~f=g
Conclusion, 4

55 ~EXIST(f):~ALL(g):~~f=g
Quant, 54

56 ~~ALL(f):~~ALL(g):~~f=g
Quant, 55

57 ~~ALL(f):~~ALL(g):f=g
Rem DNeg, 56

58 ~~ALL(f):ALL(g):f=g
Rem DNeg, 57

59 ALL(f):ALL(g):f=g
Rem DNeg, 58

[Mostowski Collapse]

With very lttle effort the proof can be extended:

59 ALL(f):ALL(g):f=g
Rem DNeg, 58

60 ALL(g):null=g
U Spec, 59

61 EXIST(f):ALL(g):f=g
E Gen, 60

So we arrive at the two reductions, that Dan-O-Matik denied:

Mostowski Collapse schrieb am Montag, 11. April 2022 um 20:06:13 UTC+2:
> You still dont believe your theorems reduce to:
>
> EXIST(g):ALL(f):[g = f]
> ALL(f1):ALL(f2):[f1 = f2]

https://groups.google.com/g/sci.logic/c/qdh5sCBDPJo/m/No87kD2LCQAJ

[Jeff Barnett]

Laugh away. The construct "For all propositions X: non truth => X" is,
of course, true. However, it does not prove that any particular X is true.
--
Jeff Barnett

[Mostowski Collapse]

Its not needed, we do not need to know the part
"add(a,b) = mul(a,b)" in the formula:

ALL(a):ALL(b):[a e null & b e null => add(a,b) = mul(a,b)]

The 3 vacuously true formulas:

ALL(a):ALL(b):[a e null & b e null => add(a,b) e cod]
ALL(a):ALL(b):[a e null & b e null => mul(a,b) e cod]
ALL(a):ALL(b):[a e null & b e null => add(a,b) = mul(a,b)]

Go into this axiom (binary version of Dans unary version):

1 ALL(dom1):ALL(dom2):ALL(cod):ALL(f):ALL(g):[Set(dom1) & Set(dom2) & Set(cod) &
ALL(a):ALL(b):[a ε dom1 & b ε dom2 => f(a,b) ε dom] &
ALL(a):ALL(b):[a ε dom1 & b ε dom2 => g(a,b) ε dom] =>
[f=g <=> ALL(a):ALL(b):[a ε dom1 & b ε dom2 => f(a,b)=g(a,b)]]]
Axiom

And then add=mul pops out!!!

Got it? Or do you disagree?

[Mostowski Collapse]

If we would need to know the part "f(a,b)=g(a,b)" or
in the unary case the part "f(a)=g(a)" then this result
would not be possible:

Mostowski Collapse schrieb am Montag, 11. April 2022 um 21:06:55 UTC+2:
> And we then prove:
>
> 59 ALL(f):ALL(g):f=g
> Rem DNeg, 58

https://groups.google.com/g/sci.logic/c/qdh5sCBDPJo/m/B4nPfo2OCQAJ

But its quite trivially provable. There is something
like dog years in DC poop. Whereas a human year
corresponds to 7 dog years, 7 DC poop proof lines

corresponds to one normal proof line, so the
wooping 57 proof lines, is roughly 57 / 7 ~ 8
proof lines. So you can say its a short proof.

https://www.pedigree.com/dog-care/dog-age-calculator

[Mostowski Collapse]

But it seems DC poop is a total falure in communicating
proofs. Even Dan-O-Matik doesn't understand the proof.
up to point that he doubts his own tool, nor the Audience

here has any understanding whats going on, evidence is
the post by Jeff Barnett. Possibly nobody reads a 57 proof
lines proof. If it could be condensed to like 8 proof lines, it

would be maybe easier to follow. There is a lot of baggage
in a DC poop proof that nobody is really interested in a
proof such as ALL(f):ALL(g):f=g ,

like de Morgan based transforms etc.. For example before
I get the compact result:

59 ALL(f):ALL(g):f=g
Rem DNeg, 58

The tool forces me to perform these insane steps:

54 ~EXIST(f):EXIST(g):~f=g
Conclusion, 4

55 ~EXIST(f):~ALL(g):~~f=g
Quant, 54

56 ~~ALL(f):~~ALL(g):~~f=g
Quant, 55

57 ~~ALL(f):~~ALL(g):f=g
Rem DNeg, 56

58 ~~ALL(f):ALL(g):f=g
Rem DNeg, 57

Why does it even generate ~EXIST(f):EXIST(g):~f=g in the
first place and not simply ALL(f):ALL(g):f=g ?

[Jeff Barnett]

I agree that "ALL(a):ALL(b):[a e null & b e null => add(a,b) =
mul(a,b)]" but that does not mean that "add = mul" is true. In the same
way that "gold is made of solver atoms => blue berries are meat" is true
but that doesn't decide the truth status of "blue berries are meat". Do
you disagree with that? Please don't repeat your entire message again; I
read it once. It ages like fish, not wine.

Once again, do you disagree with "gold is made of solver atoms => blue
berries are meat" is true but that doesn't decide the truth status of
"blue berries are meat"?
--
Jeff Barnett

[Mostowski Collapse]

I nowhere claimed this chain of inference:

> I agree that "ALL(a):ALL(b):[a e null & b e null => add(a,b) =
mul(a,b)]" but that does not mean that "add = mul" is true.

The chain of inference is to use it inside Dans axiom 1,
mich is the focus of my attention, not material implication
and forall quantifier.

I am not interested in basic logic here, but in Dans axiom 1,
which you find in the beginning of this thread. Please have
a look, folllow the link posted by Dan:

Dan Christensen schrieb am Montag, 28. März 2022 um 23:14:43 UTC+2:

> Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 ines)

What do you find there as an axiom?

[Ross A. Finlayson]

If you're going to arithmetize, the conscientious demands it's total.

Basically (ex falso) quodlibet is "garbage in, implies garbage out",
while some nihilum is "garbage in, nothing out".

It's basic that "the empty set", is naively a singleton, but
any type theory basically also has copies for zero, for where
whatever convenient substitution for "zero" some value of an
arithmetic where arithmetization makes _models of arithmetic
for each model of counting things_, for each "type" of things,
including all their types and all their types ad infinitum, most
naive inference demonstrators are usually enough just relating
cases in increment or alternate - not only is the empty set a
singleton but it isn't really the model of anything, .....

So, anyways, like infinity itself, the empty set kinds of reflects
and denies itself, being an object of theory (and an object of
theory, an element and an ur-element.)

Then, I think most people point to ZF set theory as "strong enough
the theory, in terms of type theory and model theory and all the
constructible", then that it's the usual "paradoxes" of naive set theory,
which according to logic of course _don't exist_, that the real objects
of the real complete and consistent theory modeled as much as it
is by sets, has that axioms of restriction of comprehension like "this
infinity exists and also is ordinary" or "this empti-ness exists and
also is not ubiquitous", which are basically the two non-logical definitions
of ZF set theory, those simply make for the ordinary in the regular.
but, they're just as well what makes the regular in the ordinary,
where by regular I mean equipartitioned and ordinary is recursive,
for where infinity and empty that they are not, instead it is that
they are again, in a stronger theory courtesy axiomless natural deduction.

Talking about logic as singular (for constant, consistent, complete, and
at least according to science falsifiably for any determinism according
to mathematical model, concrete), "the" logic, basically results as under
"the equi-interpretable, the logics, a logic, the logic".

Then, for my slates for uncountability and (logical) paradox for
resolving what are "this is infinite, yet still ordinary", or, "this
is empty, but still counted", is for "Borel vs. Combinatorics".

Then why it's about golden shells or decade counter,
the extension of constructions or best tools to add to
the classical to square the circles or Archimedes' spiral,
where the fundamental theorem of algebra is that "roots
are zeroes, of functions in one variable", it's neat to have
models of arithmetic with the integer lattice and continuity
as line continuity, field continuity, and signal continuity.

And that their "bridge" functions exists, ..., which for example
is the only way to conscientiously explain the metrizing ultrafilter,
of topology, to conscientious topologists, who happen to know
their theorem, and its entire what-was constructible, model.

So, we might turn to such radicals as John Corcoran and The Vatican,
with a convenient and classical square of dialectical opposition
_derived_ "naturally", makes more sense than "material implication:
funny, no?".

Then that the very same principles lead directly to all aspects
of continuum analysis, even helps realize and understand a
clock hypothesis after fundamental relativity, and the explanatory
power of a "light speed rest frame" theory and a "rest exchange
momentum theory" with a "fall gravity" and "space contraction"
and all "unifying field theory".

(Nearest book is "Superstring Theory 1: Introduction".)

[Mostowski Collapse]

Was this the bridge you crossed, when
you went to the other side of the rainbow?

[Ross A. Finlayson]

Another word is "pons", basically the bridge of fools is that
there is a bridge that fools don't cross.

There are also bridges only crossed by fools, thus that if
there's a metaphor, let it be fields with a fence. I.e.,
nobody crosses the fence. Then, the idea of a stile, is
that it is a step-stool of sorts, a ladder, that bridges
the top of the fence making that there is either side
of the fence and a means.

Then, where the universe is outside or inside, basically makes
that it's an objective realization, what a bridge is.

Here now that's reduced to two properties, but don't forget
it's rather each and their negation, than their being their
only alternatives to each other - simply given that there are other.

I.e., there is always accommodating the model and its
limits, and, the model and its possibilities.

Then that's a usual matter of objectivity, like "Einstein's
'the entire train is leaving the station, but I am still here'."
Including, "Einstein's 'now that my objective view is on the
train, I must have left'."

Then, the rainbow bridge, the closure that is the bridge
though all pan-chromatic, makes for looking down under
the rainbow and a tunnel of rainbows.

I mostly approached studying foundations as a matter
of personal luxury and a performance sport, with the idea
of along the lines of "if I know more pure and applied
mathematics then I will excel or not be exploited", or,
"if I know a history of all mathematics then whatever
anybody says I can point them to an edifice of canon",
it's plenty of effort that I could barely afford, why I'm
most content is for authoritating my own opinion.

Also there's the "it's nice to know mathematics, logic,
that the most compelling because it's the least to learn
is the foundations and what they are, ..., to know enough
mathematics for any given purposes".

Which you can take with you ....

I don't know if it helps but I constantly question my own opinion.
This doesn't bother me because it's a just opinion.

So, when I look to all mathematics, for spaces in words
(theories) and spaces in numbers (geometry), then it's
nice to have what are suitable fundamentals that are
both "classicals to all apologetics" and "apologetics to
all classicals" - and modern.

(That for me it's nice "... that I wrote".)

Then, after all explaining "crisis in ordinary mathematics
and why there's a bridge and how it is", briefly, it's about
the same for physics, where, it's key to understand that
there's a core fundamental objective body of concern,
that "the catastrophes of physics are solved about the
same way as the crises in mathematics".

What all I wrote....

[Mostowski Collapse]

Who did you meet on the other side of the
rainbow? Some witches on a broom stick?
Or just a big void, like in your brain.

Ross A. Finlayson schrieb am Montag, 25. April 2022 um 18:25:00 UTC+2:
> On Monday, April 25, 2022 at 5:12:08 AM UTC-7, Mostowski Collapse wrote:
> > Was this the bridge you crossed, when

[Mostowski Collapse]

At least you could now understand empty
functions, they map nothing to nothing,
just like when Herpes Boy crosses a bridge.

But as soon as you understand this
your brain is not anymore empty, wouldnt
it then not have the empty function itself

as an entity of thought? Now cross the bridge
again, and you have a singleton function,
and so on, suddently out of nothing, thanks

to the rainbow bridge, we are in Peanos Paradies,
now there is bridge island, which has many bridges
all leading to this island, it has one bridge which

goes out of the island, the prisma bridge, if blue, red,
yellow and green go into the island the prisma bridge
shines white, and so begins Cantors Paradies…

[Mostowski Collapse]

The problem with Dan O Matiks idea of a function
f_null such that we only have, using his theorem
with x = null:

ALL(a):[a e null => f(a) e null]

There would be now many different bridges
connecting the empty island with the empty
island, whereas in mathematics,

there is only one bridge f : null -> null. I
guess when Dan O Matik cross the bridge,
he doesn't meet the big void like Herpes Boy,

its rather he gets in contant millions of
black witches on broom sticks, clouding
his notion of a bridge, he already meets

them when he sets foot on the bridge, since
there is not one bridge but many many bridges,
everything is shaky in DC poop.

[Dan Christensen]

On Tuesday, April 26, 2022 at 7:58:22 AM UTC-4, Mostowski Collapse wrote:
> The problem with Dan O Matiks idea of a function
> f_null such that we only have, using his theorem
> with x = null:
>
> ALL(a):[a e null => f(a) e null]
>

In the current version of DC Proof, the built-in Function Axiom does not allow functions with empty domains. If you really want to play around with empty functions, you can introduce your own modified version using the Axiom Rule at the beginning of your proof. I don't recommend it for students. Too many wonky results with very little benefit IMHO, but the option is there.

[Mostowski Collapse]

Same problem with non-empty functions.
How many singleton functions are there?

f : one -> one

Where one = {null}. Its quite funny in DC poops
world behind the rainbow.

[Dan Christensen]

On Tuesday, April 26, 2022 at 9:32:27 AM UTC-4, Mostowski Collapse wrote:
> Same problem with non-empty functions.
> How many singleton functions are there?
>

For any singleton X, there exists a function f: X --> X such that for all f', if f': X --> X then f(a)=f'(a). All functions on X are equivalent.

[Mostowski Collapse]

LoL, how can show two functions equal, if you
even cannot prove the following:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

If your functions do not always have an image, how do
you want to apply Terrence Tao equality?

[Dan Christensen]

On Tuesday, April 26, 2022 at 1:52:38 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 26. April 2022 um 18:21:23 UTC+2:
> > On Tuesday, April 26, 2022 at 9:32:27 AM UTC-4, Mostowski Collapse wrote:
> > > Same problem with non-empty functions.
> > > How many singleton functions are there?
> > >
> > For any singleton X, there exists a function f: X --> X such that for all f', if f': X --> X then f(a)=f'(a). All functions on X are equivalent.

I was able to prove:

ALL(x):[Set(x) & EXIST(a):[a in x & ALL(b):[b in x => b=a]]

=> EXIST(a):EXIST(f):[a in x & ALL(b):[b in x => b=a]
& ALL(b):[b in x => f(b)=a]
& ALL(f'):[ALL(b):[b in x => f'(b)=a] => ALL(b):[b in x => f'(b)=f(b)]]]]

> LoL, how can show two functions equal, if you
> even cannot prove the following:
>
> ALL(f):EXIST(y):ALL(a):[f(a) e y]
>

Did you leave something out? Something about f? I would be very worried if I could prove this in DC Proof.


> If your functions do not always have an image...

Not sure what you are getting at, but it is trivial, in DC Proof, to prove in 7 lines:

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

=> EXIST(imgx):[Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]]]

where x is the domain of function f, y is its codomain and imgx is the _image of x under f_ (or the _range of f_) .

[Mostowski Collapse]

The thread says Re: File idiot.html , I guess I know
why. You did prove this here:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

In natural deduction with set theory, and without
any extra axioms or premisses. Only definitions please.
What term is defined by this here, no term is defined:

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

It doesn't give a unique f. Only definitions where
the definiens is unique. Also do not define stuff that
is quantified in the desired theorem.

Doesn't make any sense.... Whats wrong with you?

[Dan Christensen]

On Tuesday, April 26, 2022 at 5:13:47 PM UTC-4, Mostowski Collapse wrote:
> The thread says Re: File idiot.html , I guess I know
> why. You did prove this here:
> ALL(f):EXIST(y):ALL(a):[f(a) e y]

If I did prove that, it would be the result of serious bug in my program. It is utter nonsense.

> In natural deduction with set theory, and without
> any extra axioms or premisses. Only definitions please.
> What term is defined by this here, no term is defined:
> ALL(a):[a in x => f(a) in y]

This represents a function f mapping elements of set x to elements of set y.

> It doesn't give a unique f.

Of course not. It is an arbitrary function on two arbitrary sets. Deal with it, Jan Burse.

[Ross A. Finlayson]

Peano, Cantor, and Zeno?

Most of the "paradoxes" of infinite are given to Zeno.

Cantor has a few more, then Peano is with "here's all you get".

Heap and the Sand-Reckoner, here the view is "of a cave".

It's nice though the beach, Achilles and tortoises all running around, archery.

Then, though I wrote the slates, there's plenty left already there (for most purposes).

So, it's extreme and total when the theory is "Finlayson theory" specifically
"A-Theory: Finlayson's theory of perfect theory", I have most all "Peano,
Cantor, Zeno" on down from that.

With no paradoxes....

Then, the bridge though really is the relevance what results for topology
and connectiveness, that in set theory falls under what are resulting from
the "existence of transfer principle: so for each is so for all together". I.e.,
as a model in set theory, is for making it under terms that it's exactly where
it is so for connectiveness or connectedness, where there is the special
case of constant and uniform motion, in time, the most usual mathematical
object.

So, if you didn't already know "there's these collections of results called
bridge results after transfer principle what result resolving what otherwise
would be matters of paradox", they are central in the measure theory, and
specifically besides the usual invariant measure theory that is geometry,
of a space in itself, is the quasi-invariant, measure theory, where if you know
already there's that "measure theory for spaces of continuous functions"
is more than less the center of topology the center of mathematics.

So, though I put down the slates, it's still so that constructively they're of
course only sliver-iest fragments besides all set theory, geometry, descriptive
set theory, topology, ..., analysis.

I.e., this is all pure mathematics for all applied mathematics - constructively.

Then, that I put down the slates, uncountability and paradox the logical
resolved in a course, a usual course-of-passage the ordinals about numbering
and counting, for geometry and words, and their algebras, it's not to be left
off that in the canon of uncountability in paradox and the logical paradoxes
in quantification, and, reference in words, it comes down from the slates
those result sole inferences - where something like "A Theory" itself,
decides something like those exist.

Now, I understand some of the terrible confusion that set-theoretic transfinity
results even for usual people who studied the infinite for calculus and geometry,
where sometimes methods of exhaustion are simpler as it were than "the infinite"
itself and "formally" at least the 'regular set-theoretic cardinal infinite' is well-defined
if clear, for the usual notion that "the unit line segment is split into infinitely many
equal-sized segments and these are infinitesimals and also iota-values", just because
those are set against each other "let's prove the irrationals are uncountable so LUB"
and "yes naively real analysis is the differential", the measure in the one is a simpler
length assignment, these are 'models of the real numbers, i.e. being models at all
meaning satisfying all the properties of any other model of real numbers', anyways
the point of resolving all this mathematical paradox is: then there is none.

[Mostowski Collapse]

No its not a bug that you cannot prove it.
It only shows that your functions are not sets.
If you cannot prove this:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

Then your functions are classes. Also under
the Fritz application, there is an extension
of Fritz to classes. Just allow f to be a class
and then dom(f) to be a class.

You can then show, now F ranging over classes:

ALL(F):[Set(F) => EXIST(y):ALL(a):[F(a) e y]]

You should be able to prove the above in DC Proof
using Fritz application for F(a). You should be able
to prove it with the guard Set(F). On the other hand
it shouldnt be provable without the guard Set(F)

and when F ranges over classes.

[Mostowski Collapse]

In FOL its provable because in ZFC everything is
a set. There is no predicate Set(_). So your statement:

> If I did prove that, it would be the result of serious
bug in my program. It is utter nonsense.

Is proof of your ignorance of set theory. It boils
down to your complete disorientation in anything
set theorey, and it also begs the question whether
you have written DC Proof by yourself. Its not

open source. We dont know if its some ruSSian
orcSS trophy from world war 2. How can the
creator of tool that has a Set(_) predication
have zero knowledge of sets versus classes?

[Mostowski Collapse]

Of course when we pose a Problem in FOL
ZFC you need to first translate it to your
dang stupid DC proof. How to translate

this theorem here into your tool?

ALL(f):EXIST(y):ALL(a):[f(a) e y]

We dont know. Translating it with
some f : A -> B assumption is only legit
if you can also proof before hand:

ALL(f):EXIST(A):EXIST(B):[f : A -> B]

But if you had such a proof you would
be already finished with my theorem.

LMAO!

[Dan Christensen]

On Wednesday, April 27, 2022 at 10:17:02 AM UTC-4, Mostowski Collapse wrote:

> ALL(f):EXIST(A):EXIST(B):[f : A -> B]
>
> But if you had such a proof you would
> be already finished with my theorem.
>

Have already done so. I have proven: There exists a range set for every function.

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

=> EXIST(rng):[Set(rng) & ALL(a):[a in rng <=> a in y & EXIST(b):[b in x & f(b)=a]]]]

And IIUC, there are no non-surjective functions in ZFC -- a very serious limitation. I guess that's part of the reason why ZFC set theory is not a required course in many (if not all) pure math programs (e.g. at MIT).

[Mostowski Collapse]

Where is EXIST(y) on the left hand side.
You only have ALL(y) on the left hand side.

You still didnt prove:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

You only proved the tautology:

ALL(y):[P(y) => EXIST(y):P(y)]

Which holds for any P(_). Whats wrong with you?
A chicken can do more logic.

[Mostowski Collapse]

You only used the comprehension axiom
to rephrase the second P(_) a little bit.

But its not some proof of this sort,
which would give us a deeper insight
to sets and the Fritz application. You
did not proof EXIST(y) on the left hand side:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

Possibly you dont under stand the theorem
a least bit of it, since you call it a bug.
You so dense, one could build bunkers
from your skull. Talking to a wall is more

refreshing then seeing your proofs that
do not proof what is asked.

[Dan Christensen]

On Wednesday, April 27, 2022 at 12:49:48 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 27. April 2022 um 17:47:21 UTC+2:
> > On Wednesday, April 27, 2022 at 10:17:02 AM UTC-4, Mostowski Collapse wrote:
> >
> > > ALL(f):EXIST(A):EXIST(B):[f : A -> B]
> > >
> > > But if you had such a proof you would
> > > be already finished with my theorem.
> > >
> > Have already done so. I have proven: There exists a range set for every function.
> >
> > ALL(f):ALL(x):ALL(y):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> >
> > => EXIST(rng):[Set(rng) & ALL(a):[a in rng <=> a in y & EXIST(b):[b in x & f(b)=a]]]]
> >
> > And IIUC, there are no non-surjective functions in ZFC -- a very serious limitation. I guess that's part of the reason why ZFC set theory is not a required course in many (if not all) pure math programs (e.g. at MIT).

No comment on surjective functions??? Can't blame you! A set theory in which all functions are surjective is not of much practical use in mathematics.

> Where is EXIST(y) on the left hand side.
> You only have ALL(y) on the left hand side.
>
> You still didnt prove:
> ALL(f):EXIST(y):ALL(a):[f(a) e y]

A good thing too. It is utter nonsense.

> You only proved the tautology:
>
> ALL(y):[P(y) => EXIST(y):P(y)]
>

Wrong again, Jan Burse. My proof:

1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
Premise

2. Set(y)
Split, 1

3. EXIST(rng):[Set(rng) & ALL(a):[a in rng <=> a in y & EXIST(b):[b in x & f(b)=a]]]
Subset, 2

4. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]

=> EXIST(rng):[Set(rng) & ALL(a):[a in rng <=> a in y & EXIST(b):[b in x & f(b)=a]]]]

Conclusion, 1

This makes sense. Your wonky theorem does not.

[Mostowski Collapse]

First things first. What can we say about a symbol f,
such a symbol occurence in DC Proof, and such
a symbol occurence in FOL+ZFC.

In FOL+ZFC a symbol f, when it is a set variable,
it will hold a set. What is a set? Well a set in FOL+ZFC
is a first class object {x1,...,xn} where x1,..,xn are

sets again. So how are pairs made, well they are
made of sets as well. There are different ways to
make pairs. One way is such that taking the

infinite union U U f gives at least the union of the
left and right domain of these pairs. This is
for example the case for so called Kuratowski pairs:

(a,b) = {{a},{a,b}}

So if you have f={(a1,b1), ...,(am,bm),y1,..,yk} where
(a1,b1)...(am,bm) are Kuratowski pairs and y1,..,yk are
things that do not count as Kuratowski pairs,

The we have for U f that it gives:

U f = {{a1},{a1,b1},...{am},{am,bm},z1,..,zj}

where z1,..,zj is some garbage resulting from the
previous garbage y1,..,yk. You can use infinite union
again, and then you get:

U U f = {a1,b1,...am,bm,t1,..,ti}

So U U f will be at least contain {a1,..,am} and
{b1,...,bm}. You can use this to do the all the definitions
that Fritz did, but that Dan-O-Matik completely ignored,

because he is a big piece of ignorant bullshit.

[Mostowski Collapse]

The Fritz definitions are here, which allow you
to prove the disputed theorem that I gave. I
am 100% convinced Dan-O-Matik always skipped

them and didn't understand a bit of it:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:
> img(f) := {y e UUf : Ex(<x, y> e f)}
> f(x) := U{y e UUf : <x, y> e f} "the value of f at x"
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

With these definitions, you don't need axioms
for them you could also expand them, you can
easily prove in FOL + ZFC:

ALL(f):EXIST(y):ALL(a):[f(a) e y]

[Dan Christensen]

All this wonkiness so you can have empty functions and give up non-surjective functions? Thanks, but no thanks, Jan Burse!

STILL NO COMMENT on surjective functions, Jan Burse??? Can't blame you! A set theory in which all functions are surjective is not of much practical use in mathematics.

[Mostowski Collapse]

f : X -> Y doesn't imply that f is surjective.
Thats the case in set theory semantics and
in Terrence Tao semantics.

What are you babling about?

Also you asked for a proof in set theory and
natural deduction. When people present you
the proof idea in set theory, you call it wonky?

How corrupt and crazy are you?

Dan Christensen schrieb:

[Mostowski Collapse]

Also there are more vulgar names for the Burbaki names:

- injective: one-to-one
- surjective: onto
- bijective: one-to-one and onto

But it doesn't add much to the discussion set versus class,
and the bug that Dan Christensen uses class symbols
for functions.

Also the Bourbaki Triple, if you use <F, X, Y>, F needs to
be a set and not a class, although a class works also,
if we would use this equality:

f = f' <=> F|X = F'|X' , Y = Y'

Best is when we have X = dom(F), i.e. have kind of
normed Bourbaki triples, then equality is:

f = f' <=> F = F' & Y = Y'

We don't need to say X = X' in both cases, since
F = F' implies dom(F)=dom(F').

[Dan Christensen]

On Thursday, April 28, 2022 at 3:30:00 AM UTC-4, Mostowski Collapse wrote:
> f : X -> Y doesn't imply that f is surjective.

It doesn't in DC Proof, but I think is does in your system.

Try to construct a function f in your system such that EXIST(x):[x in cod(f) & ALL(y):[y in dom(f) => f(y)=/=x]] where dom( ) and cod( ) are as you have defined them elsewhere.

[Mostowski Collapse]

Why would f : X -> Y imply that f is surjective?
Lets put Bourbaki on the side for the moment,
in Fritz f : X -> Y only says:

img(f) ⊆ Y

Whereby surjective means:

img(f) = Y

Could you explain your claim more clearly so
that it can be followed? By refering to Fritz
f : X -> Y for example? You find Fritz here:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:
> img(f) := {y e UUf : Ex(<x, y> e f)}
> f(x) := U{y e UUf : <x, y> e f} "the value of f at x"
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

[Mostowski Collapse]

Easy example: real valued function absolute value
abs : R -> R, is not surjective onto R.

[Mostowski Collapse]

Does this answer your question:
"Try to construct a function f in your system" ?
Example that does not have surjectivity was abs : F -> F.

It works of course in set theory. It doesn't work in DC Proof,
since DC Proof abuses FOL function symbols, which are
classes, and uses nonsense such as ALL(a):[a e X => f(a) e Y]

as replacement for f : X -> Y, . Whereby in set theory the function
symbols would be set variables. One of the discerning theorems,
that discerns set from classes in this respect, would

be for example this formula here which is provable for sets:

/* Provable for sets */

ALL(f):EXIST(y):ALL(a):[f(a) e y]

But which is not provable for classes:

/* Not Provable for classes */
ALL(F):EXIST(y):ALL(a):[F(a) e y]

Using Fritz application in both cases. But the term "surjectivity"
can be also extended to classes. But you then need to have
function operators f : A -> B with A and B classes that

do not cover the full domain of discourse. But FOL
function symbols are always f : V -> V, so you can say
thay are always surjective, or phrased it the other way,

they are total on the domain of discourse. Jumping to
the conclusion that set theory has also domain of discourse
total functions is quite hillarious.

LMAO!

[Dan Christensen]

See my recent reply to your identical posting at sci.math

[Mostowski Collapse]

I already responded there. You think codomain = { y | EXIST(x):(x,y) e f }.
But it doesn't make much sense to use this definition, since we started
here working with Fritz definition:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:
> img(f) := {y e UUf : Ex(<x, y> e f)}
> f(x) := U{y e UUf : <x, y> e f} "the value of f at x"
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

What does img(f) give you? On the other hand codomain is
define as the Y in a declaration f : X -> Y. It only constrains
img(f), it only gives you:

img(f) ⊆ Y

Or as Fritz already wrote:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

Do you see the img(f) c Y. Did you read Fritz even once?
Read and understand what he wrote?

[Dan Christensen]

On Friday, April 29, 2022 at 4:12:38 AM UTC-4, Mostowski Collapse wrote:
> Easy example: real valued function absolute value
> abs : R -> R, is not surjective onto R.

Not a good example. In your system, abs = {(x,y) in R^2 : y=x if x>=0; y=-x otherwise}.

You have dom(abs) = R and cod(abs)= {x in R : x>=0}

In your system, you obtain the bizarre result that abs is surjective. Kind of embarrassing, isn't it?

[Mostowski Collapse]

There is nothing of some sort of my system. Its all
out in the wild, you can read yourself:

For a function f:X→Y, the codomain is just the set Y. For instance,
if f:R→R is x↦x^2, then the codomain is R. This terminology is agreed
upon by all who use it: i.e., I have never seen anyone use the term
"codomain" to mean anything else.
https://math.stackexchange.com/questions/59432/domain-co-domain-range-of-a-function

Now what is the rng(f) of the above function? Do
we have rng(f) = R?

[Mostowski Collapse]

Nothing changes when you look at f set theoretically,
f ⊆ X x Y and rng(f) ⊆ Y , not necessarely rng(f)=Y.

Or how Fritz writes it:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

Which amounts to the same. He only uses img(_)
instead of rng(_).

[Mostowski Collapse]

Or lets make a table for our youngster:

Function Codomain Range
abs : R->R, abs(x)=|x| R [0,oo)
sqr : R->R, sqr(x)=x^2 R [0,oo)

Got it?

[Mostowski Collapse]

You can also use ↦ and make the table with ↦:

Function Codomain Range
abs : R -> R, x |-> |x| R [0,oo)
sqr : R -> R, x |-> x^2 R [0,oo)

|-> is the maps to operator. Can be even used with
multiple arguments. But this metamath is a little different:

http://us.metamath.org/mpeuni/df-mpt.html

You have the domain built-in and no specification of
a codomain, so the metamath variant cannot be

used to make such a table.

[Dan Christensen]

On Friday, April 29, 2022 at 12:40:32 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Freitag, 29. April 2022 um 18:37:02 UTC+2:
> > On Friday, April 29, 2022 at 4:12:38 AM UTC-4, Mostowski Collapse wrote:
> > > Easy example: real valued function absolute value
> > > abs : R -> R, is not surjective onto R.
> > Not a good example. In your system, abs = {(x,y) in R^2 : y=x if x>=0; y=-x otherwise}.
> >
> > You have dom(abs) = R and cod(abs)= {x in R : x>=0}
> >
> > In your system, you obtain the bizarre result that abs is surjective. Kind of embarrassing, isn't it?

> There is nothing of some sort of my system. Its all
> out in the wild, you can read yourself:
>
> For a function f:X→Y, the codomain is just the set Y.

What are dom(abs) and cod(abs) (your example)? Are there any elements of cod(abs) that have no pre-image in dom(abs)?

[Mostowski Collapse]

I nowhere use a function cod(_). Its an
extrinisic concept, similar to surjective,
see this here:

https://math.stackexchange.com/a/4438437/1002973

You connot extract the codomain from f,
in the non-Bourbaki setting. Thats also
why surjective is extrinsic.

In which setting do you work, set theory
or Bourbaki?

Dan Christensen schrieb:

[Mostowski Collapse]

Fritz has also nowhere a cod(_) function
operator. You have Fritz before your eyes,
don't you? The codomain is only a component

of a declaration of the form:

f : X -> Y,

its the Y component. The declaration
unfolds to the following formula:

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."
https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ

You have img(f) ⊆ Y and not img(f) = Y
required. Because if it where img(f) = Y,
we would say f is a surjective mapping

from X onto Y, otherwise we only say f
is a mapping from X to Y.

Mostowski Collapse schrieb:

[Mostowski Collapse]

So maybe you understand the table
if I write it as follows:

Function Declared Computed
Declaration Codomain Range

abs : R -> R, x |-> |x| R [0,oo)
sqr : R -> R, x |-> x^2 R [0,oo)

Everything clear now? This is for non-Bourbaki.
For Bourbaki we could replace Declared Domain,

by cod(f). There would be a function cod(f).
But the table wouldn't look any different

essentially, also for Bourbaki its possible
cod(f)=\=rng(f).

Mostowski Collapse schrieb:

[Dan Christensen]

On Friday, April 29, 2022 at 1:40:02 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

>
> Dan Christensen schrieb:
> > On Friday, April 29, 2022 at 12:40:32 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> >
> >> Dan Christensen schrieb am Freitag, 29. April 2022 um 18:37:02 UTC+2:
> >>> On Friday, April 29, 2022 at 4:12:38 AM UTC-4, Mostowski Collapse wrote:
> >>>> Easy example: real valued function absolute value
> >>>> abs : R -> R, is not surjective onto R.
> >>> Not a good example. In your system, abs = {(x,y) in R^2 : y=x if x>=0; y=-x otherwise}.
> >>>
> >>> You have dom(abs) = R and cod(abs)= {x in R : x>=0}
> >>>
> >>> In your system, you obtain the bizarre result that abs is surjective. Kind of embarrassing, isn't it?
> >
> >> There is nothing of some sort of my system. Its all
> >> out in the wild, you can read yourself:
> >>
> >> For a function f:X→Y, the codomain is just the set Y.
> >
> > What are dom(abs) and cod(abs) (your example)? Are there any elements of cod(abs) that have no pre-image in dom(abs)?
> >

> I nowhere use a function cod(_).

It is interesting that you are now apparently disowning an essential feature of so-called set-theoretic functions. Painted yourself in another corner, Jan Burse?

>Its an
> extrinisic concept, similar to surjective,
> see this here:
>
> https://math.stackexchange.com/a/4438437/1002973
>
> You connot extract the codomain from f,
> in the non-Bourbaki setting. Thats also
> why surjective is extrinsic.
>
> In which setting do you work, set theory
> or Bourbaki?

The set theory most commonly used in math textbooks. (Hint: not ZFC)

[Mostowski Collapse]

Does your set theory change this table?

Function Declared Computed
Declaration Codomain Range

abs : R -> R, x |-> |x| R [0,oo)
sqr : R -> R, x |-> x^2 R [0,oo)

I don't think so. You can define rng(f) also
differently than fritz did:

Fritzs definition:

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

Alternative definition:
img(f) := { π2(z) | z e f & z is a pair }

So in DC Proof you could use Set'(f), and
you would also derive rng(f) = [0,oo).

On the other hand Codomain is an extra logical
concept from the context, also in DC Proof.

You can easily verify that you can prove in
DC Proof:

ALL(a):[a e R => abs(a) e R u {pink unikorn}]

ALL(a):[a e R => abs(a) e [0,oo) u {-1,-2}]

I don't see any cod(f) in DC Proof, so its
non-Bourbaki.

Dan Christensen schrieb:

[Mostowski Collapse]

You should have asked that you don't mean ZFC on math
stack exchange. This would be a quite exciting question.

But you only wrote:

Are there non-surjective functions in ZFC theory?
https://math.stackexchange.com/q/4438429/1002973

So whats up Dan-O-Matik?

LoL

[Mostowski Collapse]

But I already answered the question even for non-ZFC,
if you would use something more powerful. Like NBG,
only the most crazy idiot by the name José Carlos Santos

interfered on MSE. I already wrote in my answer that img(_)
respectively rng(_) can be extended. But it would not
change anything for this table, since this table

is a geometric fact:

Function Declared Computed
Declaration Codomain Range

abs : R -> R, x |-> |x| R [0,oo)
sqr : R -> R, x |-> x^2 R [0,oo)

The function declaration abs : R -> R defines the
drawing board, R x R, the whole Euclidean plan.
Then rng(f) is the projection, the shadow of f on

the y axis. Whats the shadow of abs(_) on the
y axis? Its always [0,oo) n C where C is the codomain.
You can use whathever formalization, ZFC or non-ZFC,

Bourbaki or non-Bourbaki, its always [0,oo). And the
intention of abs : R -> R is also always the same, to
tell us what is our bigger surround world we are

considering, i.e. R x R. Of course if you only consider
a half Euclidean plane R x [0,oo), and say abs : R -> [0,oo),
then suddently abs becomes surjective, because the rng(f)

shadow now covers all of the y axis, which is now only a half y axis.

[Mostowski Collapse]

The core problem is that people are not anymore
grounded in geometry. Easy notations like f : X -> Y
and rng(f) that can be easily explained geometrically,

are not anymore understood by folks such as Dan
Christensen und by utter morons like José Carlos Santos
from the group of homo stack exchangis, in the clade

of homo trollensis. They have totally lost their
grounding of mathematics in geometry and are only
good for politics and polemics.

Example:
- Dan Christensen: The set theory most commonly

used in math textbooks. (Hint: not ZFC)

- José Carlos Santos: “There is no distinction made
between the codomain and what is commonly called
the range of a function”. And, in your answer, you
seem to be unaware of that.

Blistering nonsense to confound codomain and range.
Doesn't make any sense geometrically. If domain codomain
span some space, that houses some functions,

this does not imply that codomain is the range of a
function. This is everywhere like that. If you model
the problem with or without set theory.

Thats just geometry.

Mostowski Collapse schrieb:

[Mostowski Collapse]

José Carlos Santos addressed me, about my unawareness,
while I was in process of explaining when and why
codomain and range are not the same.

Thats possibly the most bold trolling somebody ever
did, or José Carlos Santos had the some unfortunate
brain stroke the moment he used his keyboard,

and we are back to:

Our conjecture is that the cycle will prove most
reliable. A doctor who gets an unlucky string of
misleading results will do the least damage there.
https://plato.stanford.edu/entries/formal-epistemology/#TheZolEff

But this is a much too benevolent interpretation,
possibly José Carlos Santos is just a pervert, that
saw somebody with 101 points and started a fight.

Mostowski Collapse schrieb:

[Mostowski Collapse]

Maybe José Carlos Santos had really a stroke of some
sort, maybe he is a chain smoker? Since he wrote:

"Beacause the OP wrote that, in ZFC,"

Whats the typo in because? Also ZFC has a specific language
like set-like function, otherwise a function is a class. So there is
a THIRD CATEGORY MISTAKE in the question:

If I understand correctly, in ZFC set theory, a function is just a set
of ordered pairs with certain properties.
https://math.stackexchange.com/q/4438429/1002973

The correct phrasing would be:

If I understand correctly, in ZFC set theory, a set-like function is
just a set of ordered pairs with certain properties.
https://math.stackexchange.com/q/4438429/1002973

You can check yourself:

6.8 Definition A class S is said to be a (binary) relation if
evey member x of S is an ordered pair.
6.12 Definition A relation F is said to be a function if ...
Basic Set Theory - Azriel Levy
https://www.amazon.de/Basic-Theory-Dover-Books-Mathematics/dp/0486420795

Mostowski Collapse schrieb:

[Mostowski Collapse]

3 category mistakes in one MSE question.
Congratulations Dan Christensen, thats
something for the Guiness Book of Records.

Lets also include the burping administrators
of stack exchange in the Guiness Book of
Records entry. Giving the cloud of comments

the two remaining answers have on MSE,
maybe MSE would have been wise to first
sift the question terminological wise, it

seems that the confusion remains...

LMAO!

Mostowski Collapse schrieb:

[Ross A. Finlayson]

Shut up Musatov / answer the paradoxes.

[Mostowski Collapse]

The Dan Christensen nonsense resembles this fallacy:

The french eat baguette
Therefore
Baquette eaters are french

Mostowski Collapse schrieb am Mittwoch, 30. März 2022 um 21:09:33 UTC+2:
> The error is on your side, not on Wikipedias side. Wikipedia
> uses nowhere a Vacuously True only condition. They have
> also the condition f ⊆ X x Y.
>
> Its YOUR PROBLEM Dan-O-Matik. Scape goating Wikipedia
> doesn't work. Its YOUR BLUNDER.
> Dan Christensen schrieb am Mittwoch, 30. März 2022 um 20:20:13 UTC+2:
> > See my reply today to your identical posting at sci.math
> >
> > Dan
> > On Wednesday, March 30, 2022 at 11:50:44 AM UTC-4, Mostowski Collapse wrote:
> > > A proof A & ~A => B is pretty irrelevant here.
> > > It seems you are not able to simplify formulas with
> > > vacuous truths in it. So I will do it for you.
> > >
> > > You proved:
> > ....

[Fritz Feldhase]

On Saturday, April 30, 2022 at 11:27:54 AM UTC+2, Mostowski Collapse wrote:
> The Dan Christensen nonsense resembles this fallacy:
>
> The french eat baguette
> Therefore
> Baquette eaters are french

Reminds me to WM. He is convinced that

An(IN_def -> Phi[n])

defines (!) IN_def (somehow).

You will find the same (type of) error in his book. There he assumes thst IN is "specified" by "IN c M for all inductive sets M". He does not understand that "IN is an inductive set" is missing in his "axiom system for the nstural numbers".

What's the matter with these guys?

[Mostowski Collapse]

He can try himself, one can prove
with gra from your function axiom:

/* Provable */
ALL(gra):EXIST(y):ALL(a):[f(a) e y]

But with fun from your function axiom:

/* Not Provable */
ALL(fun):EXIST(y):ALL(a):[f(a) e y]

I am refering to a Fritz translation
of f(a). So something gets lost

in your "translation". You turn French
into Baquette eaters, and then assume

they are automatically French.

Fritz Feldhase schrieb:

[Mostowski Collapse]

Corr.: Typo

He can try himself, one can prove

with gra from your function axiom,

because we have Set(gra):

/* Provable */
ALL(gra):EXIST(y):ALL(a):[gra(a) e y]

But with fun from your function axiom:

/* Not Provable */

ALL(fun):EXIST(y):ALL(a):[fun(a) e y]

[Dan Christensen]

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

Dan

On Saturday, April 30, 2022 at 8:38:45 AM UTC-4, Mostowski Collapse wrote:
> Corr.: Typo
> He can try himself, one can prove
> with gra from your function axiom,
>
> because we have Set(gra):
>

...

[Mostowski Collapse]

I will be only convinced of a good modelling of
function spaces, when the candidate can prove
the following cardinality theorem:

/* Cardinality Lemma */
f : A -> B => |f| = |A|

Proof Sketch:
Take these two injections:
i1 : A -> f, i1(a) = (a,f(a))
i2 : f -> A, i2((a,_)) = a.

By the Cantor Bernstein Schroeder (CBS) theorem there is
a bijection. Did not Dan Christensen proof the CBS already?
What about the Cardinality Lemma?

[Mostowski Collapse]

Guess what, this nonsense does not satisfy the
cardinality lemma. If we require only:

EXIST(add):[
1) ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
2) & ALL(a):[a e n => add(a,0)=a]
3) & ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]
https://dcproof.com/ConstructAddFunction.htm

We could also have:

+ : R x R -> R

That satisfies the requirements. But + : R x R -> R
is an uncountable large set of triples, whereas the
usual add : N x N -> N is only a countable set of

triples. So the cardinality lemma cannot be proved,
there is too much dark matter in the room.

LMAO!

[Fritz Feldhase]

On Sunday, May 1, 2022 at 10:32:10 PM UTC+2, Mostowski Collapse wrote:

> I will be only convinced of a good modelling of
> function spaces, when the candidate can prove
> the following cardinality theorem:
>
> /* Cardinality Lemma */
> f : A -> B => |f| = |A|

On the other hand, in the context of Bourbaki functions, |f| = 3. :-P

But - of course - |gra(f)| = |A| will hold for them "too".

> Proof Sketch:
> Take these two injections:
> i1 : A -> f, i1(a) = (a,f(a))
> i2 : f -> A, i2((a,_)) = a.
>
> By the Cantor Bernstein Schroeder (CBS) theorem there is
> a bijection. Did not Dan Christensen proof the CBS already?
> What about the Cardinality Lemma?

How about:

Define g: f --> A = dom(f) with g(p) = pi_1(p) for all p e f.

Then g is a bijection from f onto A.

Proof: g is a function from f _onto_ A.

Let x0 e A, then Ey((x0, y) e f), since A = dom(f). Hence Ep e f: pi_1(p) = x0, hence Ep e f: g(p) = x0.

g is injective. Assume g(p) = g(p') for arbitrary p, p' e f. Then pi_1(p) = pi_1(p'). Hence there's is an x and some y, y' such that (x, y) = p and (x, y') = p' with p, p' e f. Hence y = y', since f is a function. Hence p = p'.

qed. (Since |X| = |Y| iff X ~ Y for any sets X, Y.)

From our proof we got pi_1[f] = A as a side result. Didn't Peano speak of a "shaddow" in this connection?

[Ross A. Finlayson]

Ah, so "the cardinality lemma can not be proved, both ways".

Do you know Cohen's forcing is "cardinality, alternate maximal
limit ordinal"?

What trichotomy leaves....

Then, all model theory is result limit ordinal.

Which in powersets have cardinals that are not their ordinals, ....

Typical universes and domains the integers have
any "infinity" a limit ordinal, and so in terms.

Where the number actually has the term is singular,
what so follows why it's leavable out under definition.

Let's keep in mind Cantor Schroeder Bernstein equation,
where coverage both ways is for example dense in usual models.

These in rules are neat.

You're just talking about order in trichotomy.

[Fritz Feldhase]

On Monday, May 2, 2022 at 2:18:49 AM UTC+2, Fritz Feldhase wrote:
> On Sunday, May 1, 2022 at 10:32:10 PM UTC+2, Mostowski Collapse wrote:
>
> > I will be only convinced of a good modelling of
> > function spaces, when the candidate can prove
> > the following cardinality theorem:
> >
> > /* Cardinality Lemma */
> > f : A -> B => |f| = |A|
> >
> On the other hand, in the context of Bourbaki functions, |f| = 3. :-P

In this case here we would have f = (gra(f), A, B).

> But - of course - |gra(f)| = |A| will hold for them "too".

Note that for "mathematical functions" (al la Bourbaki) the definition for .(.) has to be modified slightly (in comparison with the definition for "set theoretic" functions).

In this case we might use the following definition:

f(x) = U{y e UUpi_1(f) : (x, y) e pi_1(f)}.

Or, with gra(f) := pi_1(f):

f(x) = U{y e UUgra(f) : (x, y) e gra(f)}.

[Mostowski Collapse]

Was using simple set theoretic function spaces,
so that the notation is defined as:

f : A -> B :<=> f e B^A /* set exponentiation */

The same applies form the function space usage
in the proof sketch. But I used a little Haskell or
Prolog pattern matching in the definition of the

> Proof Sketch:
> Take these two injections:
> i1 : A -> f, i1(a) = (a,f(a))
> i2 : f -> A, i2((a,_)) = a.

two injections. Can this all be done in DC Poop?
And the cardinality lemma be verified in DC Poop?
Some first baby steps into function spaces?

[Mostowski Collapse]

Also I have the impression, Dan Christensen does
not understand the least what function SPACE means.
Why does he prove this here:

> On every set, there is exists a unique empty function.

With set x as a parameter? Does he think the SPACE
is spanned by having

multiple functions with different signatures?

That is not what SPACE means here, it means only
the following:

multiple functions with same signature

When we write f : A -> B, we talk about multiple
functions with the same signature A -> B.

The signature doesn't vary. Why would somebody
prove a nonsense example where the function space
has a single element i.e. f : {} -> X and then

vary X? Thats very crankish.

[Mostowski Collapse]

In as far this here is a misleading statement:

> 2. The function space (fs) of all functions mapping the empty set to any set x has only a single element (lines 92-137)
https://dcproof.com/EmptyFunctionsUniqueV2.htm

Intentionally there is no "the" function space {} -> X,
since it has a parameter X. So notationally you have
a couple of function space notations:

{} -> X1
{} -> X2
...

Now under Terrence Tao they are not the same, if X1=\=X2,
because even if some element f : {} -> X1 and g : {} -> X2
they are automatically different since cod(f) =\= cod(g).

Under the non-Terrence Tao semantics, we have for
set exponentiation indeed that:

X^{} = {} for all X

Is this what he wants to say. I thought Dan O Matik subscribes
to the Terrence Tao semantics? But from the above my conclusion
is rather he is living in the land of confusion.

LMAO!

[Mostowski Collapse]

Corr.: Typo

X^{} = { {} } for all X

[Dan Christensen]

On Monday, March 28, 2022 at 5:30:05 PM UTC-4, Dan Christensen wrote:
> The following proof demonstrates how functions, function equality, function spaces and empty functions can be handled in my DC Proof system.
>

The current version of DC Proof does not deal with empty functions. Users who still want to play with empty functions can still introduce their own version of the Function Axiom that must be introduced at the beginning of a proof using the Axiom Rule (on Logic menu).

[Mostowski Collapse]

LoL, same problem with identity function.
How many identity functions are there in

THE function space, or across the
functions spaces over all parameters X?

id : {a} -> X

Only one, like x |-> x. Or multiple? What
does Terrence Tao say?

[Dan Christensen]

On Monday, May 2, 2022 at 1:35:06 PM UTC-4, Mostowski Collapse wrote:
> LoL, same problem with identity function.
> How many identity functions are there in
>
> THE function space, or across the
> functions spaces over all parameters X?
>
> id : {a} -> X
>
> Only one, like x |-> x. Or multiple?

On any non-empty set A, I have shown that there exists a unique identity function on A, unique in the sense that, if id: A-->A where id(x)=x, and id': A-->A where id'(x)=x, then for all x in A, we have id'(x)=id(x).

[Fritz Feldhase]

On Monday, May 2, 2022 at 8:34:15 PM UTC+2, Dan Christensen wrote:

> On any non-empty set A, I have shown that there exists a unique identity function on A, unique in the sense that, if id: A-->A where id(x)=x, and id': A-->A where id'(x)=x, then for all x in A, we have id'(x)=id(x).

You are talking nonsense, idiot.

Hint: You DON'T have a formal representation of "f: X --> Y", i. e. "function(f) & dom(f) = X & codom(f) = Y" in your system.

What's the matter with you? Are you brain dead?

Hence all you have shown is:

if id(x)=x for all x in A and id'(x)=x for all x in A, then id(x)=id'(x) for all x in A.

What an incredible result!

What you WOULD have to show is that for any set A and any two functions id: A --> A, id': A --> A with id(x) = x for all x e A and id'(x) = x for all x e A:

id = id' ,

dumbo. The latter expresses uniqueness of the two functions id and id'.

When will you ever learn; Dan?

Hint: Tao's "definition for equality of functions" WOULD deliver id = id'. But it seems that this "definition" didn't work well in the context of DC Poop.

[Dan Christensen]

On Monday, May 2, 2022 at 3:25:29 PM UTC-4, Fritz Feldhase wrote:
> On Monday, May 2, 2022 at 8:34:15 PM UTC+2, Dan Christensen wrote:
>
> > On any non-empty set A, I have shown that there exists a unique identity function on A, unique in the sense that, if id: A-->A where id(x)=x, and id': A-->A where id'(x)=x, then for all x in A, we have id'(x)=id(x).
> You are talking nonsense, idiot.
>
> Hint: You DON'T have a formal representation of "f: X --> Y", i. e. "function(f) & dom(f) = X & codom(f) = Y" in your system.
>

For "f: X --> Y", I have: ALL(a):[a in x => f(a) in y]

I haven't found the others necessary to formalize.

> Hence all you have shown is:
>
> if id(x)=x for all x in A and id'(x)=x for all x in A, then id(x)=id'(x) for all x in A.
>
> What an incredible result!
>

Thanks. Nothing else is really required.

> What you WOULD have to show is that for any set A and any two functions id: A --> A, id': A --> A with id(x) = x for all x e A and id'(x) = x for all x e A:
>
> id = id' ,
>

You would have to settle for my "incredible result" (your words) above. After all, we are not usually interested in comparing two functions unless they both the same domain.

[Fritz Feldhase]

On Monday, May 2, 2022 at 9:44:46 PM UTC+2, Dan Christensen wrote:
> On Monday, May 2, 2022 at 3:25:29 PM UTC-4, Fritz Feldhase wrote:

Seems that you still did't get it.

> > Hint: You DON'T have a formal representation of "f: X --> Y", i. e. "function(f) & dom(f) = X & codom(f) = Y" in your system.
> >
> For "f: X --> Y", I have: ALL(a):[a in x => f(a) in y]

No, you DON'T, you just may THINK SO.

"f: X --> Y" stands for "function(f) & dom(f) = X & codom(f) = Y"

This means that you can DERIVE (especially) "dom(f) = X" and "codom(f) = Y" from "f: X --> Y".

You can't derive this from "ALL(a):[a in x => f(a) in y] "

What's the matter with you? Cant't you comprehend this simple fact?

Hint: If f: X --> Y, i. e. function(f) & dom(f) = X & codom(f) = Y, then for ANY x c X:

ALL(a):[a in x => f(a) in Y], (*)

In other words, (*) holds for any subset x of X.

Again: If (*) HOLDS for some x, this does NOT imply that x is the domain of f.

Hence ALL(a):[a in x => f(a) in y] DOES NOT express that x is the domain of f (since it CAN'T do that).

Hint: ALL(a):[a in x => f(a) in y] holds for x = {} and ANY function f (and any set y).

[Dan Christensen]

On Monday, May 2, 2022 at 4:22:57 PM UTC-4, Fritz Feldhase wrote:
> On Monday, May 2, 2022 at 9:44:46 PM UTC+2, Dan Christensen wrote:
> > On Monday, May 2, 2022 at 3:25:29 PM UTC-4, Fritz Feldhase wrote:
> Seems that you still did't get it.
> > > Hint: You DON'T have a formal representation of "f: X --> Y", i. e. "function(f) & dom(f) = X & codom(f) = Y" in your system.
> > >
> > For "f: X --> Y", I have: ALL(a):[a in x => f(a) in y]

> No, you DON'T, you just may THINK SO.
>

I do and see no reason to doubt it.

> "f: X --> Y" stands for "function(f) & dom(f) = X & codom(f) = Y"
>

Needlessly complicated. I like ALL(a):[a in x => f(a) in y]

> This means that you can DERIVE (especially) "dom(f) = X" and "codom(f) = Y" from "f: X --> Y".
>

I like to START with a domain and codomain set. Then prove the existence of the required function on the required domain and codomain.

> You can't derive this from "ALL(a):[a in x => f(a) in y] "
>

I prefer not to work backwards like you to do. FIRST the domain and codomain, THEN the function.

> What's the matter with you? Cant't you comprehend this simple fact?
>
> Hint: If f: X --> Y, i. e. function(f) & dom(f) = X & codom(f) = Y, then for ANY x c X:
>
> ALL(a):[a in x => f(a) in Y], (*)
>
> In other words, (*) holds for any subset x of X.
>

So what?

> Again: If (*) HOLDS for some x, this does NOT imply that x is the domain of f.
>

In (*), x can be considered to be domain without any inconsistency. I don't see any problem here.

> Hence ALL(a):[a in x => f(a) in y] DOES NOT express that x is the domain of f (since it CAN'T do that).
>

I disagree.

> Hint: ALL(a):[a in x => f(a) in y] holds for x = {} and ANY function f (and any set y).

Recall that the current version of DC Proof does not allow for empty functions. No great loss AFAICT.

[Ben]

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

> On Monday, May 2, 2022 at 3:25:29 PM UTC-4, Fritz Feldhase wrote:

>> Hint: You DON'T have a formal representation of "f: X --> Y",
>> i. e. "function(f) & dom(f) = X & codom(f) = Y" in your system.
>
> For "f: X --> Y", I have: ALL(a):[a in x => f(a) in y]

But they don't mean the same thing. For example, from

∀a (a ∈ ℕ → f(a) ∈ ℕ)

I can conclude that

∀a (a ∈ {1} → f(a) ∈ ℕ)

but from f: ℕ → ℕ I can /not/ conclude that f: {1} → ℕ.

--
Ben.