DC Proofs waterloo is Russells definite descriptions

[Mostowski Collapse]

DC Proof creator Dan-O-Matik suffers from some major
didactic deficiencies:

1) Errorneously translates "the X is Y" into "all X are Y".

2) Denies that ZFC is integral part of modern basic math.

Latest example:

Dan Christensen schrieb am Mittwoch, 24. November 2021 um 05:09:48 UTC+1:
> 17 ALL(x):ALL(f):ALL(y):ALL(z):[ALL(a):[a in x => f(a) in y]
> & EXIST(a):a in x
> & ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
> => EXIST(a):a in z]
> Conclusion, 1
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/YXt2f3OIBAAJ

Why the hell ALL(z)? How many images of the function f do you
expect to exist? Zero many images? More than one images?

Isn't the common notation f[a] from mathematics for the image by
the function f a definite description?

What does it take to show that it is a definite decription?

[Dan Christensen]

On Thursday, November 25, 2021 at 4:17:23 AM UTC-5, Mostowski Collapse wrote:
> DC Proof creator Dan-O-Matik suffers from some major
> didactic deficiencies:
>
> 1) Errorneously translates "the X is Y" into "all X are Y".
>

Here we go again! Jan Burse here has never gotten over the fact, given, for example, that there is presently no king of France, anything you can say about someone (e.g that they are bald) is vacuously true of any present king of France. Contrary to Jan Burse's claim, it doesn't matter if there is at most one king of France since there are actually NONE.

> 2) Denies that ZFC is integral part of modern basic math.
>

I don't know why Jan Burse is so invested in a strict interpretation of ZFC, but the fact is that, with the exception of the Axiom of Choice, most math textbooks make mention of the ZFC axioms only in passing, if that. Mathematical logic (includes ZFC set theory) is not a required course in many pure math programs (e.g. at MIT). My guess it that ZFC is something of a pedagogical nightmare. DC Proof incorporates the axioms of set theory are, implicitly anyway, those actually used in most math textbooks. Users of DC Proof also have the option of introducing their own axioms at the beginning of proofs.

> Latest example:
>
> Dan Christensen schrieb am Mittwoch, 24. November 2021 um 05:09:48 UTC+1:

> > 17 ALL(x):ALL(f):ALL(y):ALL(z):[

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

That is, f is a function with domain x and codomain y

> > & EXIST(a):a in x

x is non-empty

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

z is the image of set x under f

> > => EXIST(a):a in z]

Therefore, z must be non-empty.

As Jan Burse himself correctly put it, "The image of a non empty domain is non empty."

In other words, in general, if (1) f is a function, (2) its domain is non-empty, and (3) z is the image of the domain under f, then z must also be non-empty.

> > Conclusion, 1
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/YXt2f3OIBAAJ
>

> Why the hell ALL(z)?

Learn some logic, Jan Burse! See "In other words, IN GENERAL..." above. We call such statements, universal generalizations. See https://en.wikipedia.org/wiki/Universal_generalization

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]

f[A] notation is also on your beloved Wikipedia:

f[A] = {f(x):x in A}
https://en.wikipedia.org/wiki/Image_%28mathematics%29#Image_of_a_subset

You find it in usage everywhere in math textbooks.
You need an axiom schema from ZFC to have f[A] exist.
But the you can not only show that it exist, its also unique.

To translate "the X is Y" into "all X are Y" is a common beginner error.
Unfortunately in your case it leads to denial of ZFC.
Your childish behavior is kind of WM with extra steps:

FACEPALM MEME 🤣 HD 🤣
https://www.youtube.com/watch?v=g-bVEc8oZvk

[Mostowski Collapse]

Apropos pedagogical nightmare, here it is in your own words:

> > > & ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
> z is the image of set x under f

Only if it z exists and if z is unique. Then you are allowed
to use the phrase "the X is Y". Otherwise z could be the king of
france, which doesn't exist. How can you show that z exists?

(Hint you need ZFC) I rather watch 2 1/2 hours garlic bread
sent to outer space, than the ever repeating nonsense of
Dan-O-Matik proofs spammed into sci.logic and sci.math.

2½ Hours of Unedited Garlic Bread Flight Footage
https://www.youtube.com/watch?v=YKAblynZYhI

BTW: You can fix your pedagogical nightmare if you rephrase:
> if z is an image of set x under f

After all "=>" translates to "if then" and "ALL(z)"
translates to the indeterminate article.

[Dan Christensen]

> f[A] notation is also on your beloved Wikipedia:
>
> f[A] = {f(x):x in A}
> https://en.wikipedia.org/wiki/Image_%28mathematics%29#Image_of_a_subset
>
> You find it in usage everywhere in math textbooks.
> You need an axiom schema from ZFC to have f[A] exist.

See Subset Axiom on the Sets menu of DC Proof. It is documented in the user manual.

> But the you can not only show that it exist, its also unique.
>

To show it is unique, you will also need the Set Equality Axiom on the Sets menu. I will leave it to you an exercise. It seems like you need the practice, Jan Burse. Really, it's not that difficult.

> To translate "the X is Y" into "all X are Y" is a common beginner error.

No errors on my part. See my original reply here.

> Unfortunately in your case it leads to denial of ZFC.

Not so much denial as using the axioms and rules that are actually used in most math textbooks. Again, see my original reply here.

[Mostowski Collapse]

The co-domain of f is not given.
The subset axiom doesn't work for this here:

f[A] = {f(x):x in A}

Why do you think you can prove existence of f[A] with subset axiom?

[Dan Christensen]

On Thursday, November 25, 2021 at 1:34:07 PM UTC-5, Mostowski Collapse wrote:
> The co-domain of f is not given.

You can give it a name, e.g. y.

> The subset axiom doesn't work for this here:
> f[A] = {f(x):x in A}
> Why do you think you can prove existence of f[A] with subset axiom?

Here are the first 5 lines to get you started:

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

2 Set(x)
Split, 1

3 Set(y)
Split, 1

4 ALL(a):[a in x => f(a) in y]
Split, 1

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

Just 44 lines. Enjoy.

[Mostowski Collapse]

I don't think that is what is written on Wikipedia, I don't see
an Y in their definition of f[A]. But lets forget about Wikipedia.

Lets say I have a function f : V -> V, that maps any set to some set.
This was the function of my original problem, that is still not solved

in DC Proof. How do you show that this here exists:

f[A] = {f(x):x in A}

Here is my original problem again:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

[Fritz Feldhase]

On Thursday, November 25, 2021 at 7:34:07 PM UTC+1, Mostowski Collapse wrote:

> The co-domain of f is not given.
> The subset axiom doesn't work for this here:
> f[A] = {f(x) : x in A}
> Why do you think you can prove existence of f[A] with subset axiom?

In the context of set theory a /function/ is actually a certain set of pairs. For example, f = {(1, 1), (2, 4), (3, 9)} is a function. This allows to get a set [f] from f by set theoretic operations (repeated application of union) such that Df(f) c [f] as well as Im(f) c [f]. Hence we get f[A] = {f(x) e [f] : x in A} for any A c Df(f).

Since I don't know DC proof's subset axiom, I'm not sure if these set theoretic states of affairs suffice to get f[A] from it. But clearly f[A] is a subset of [f] for all A c Df(f).

[Fritz Feldhase]

On Thursday, November 25, 2021 at 8:14:10 PM UTC+1, Fritz Feldhase wrote:

> In the context of set theory a /function/ is actually a certain set of pairs. For example, f = {(1, 1), (2, 4), (3, 9)} is a function.

See: https://de.wikipedia.org/wiki/Funktion_(Mathematik)#Mengentheoretische_Definition

[Mostowski Collapse]

I am not considering set-like functions f : X -> Y where X and Y are sets.
I am considering function symbols from FOL, which are f : V -> V,
where V is the universal class. For function symbols from FOL you

can prove the following:

ALL(x):EXIST(y):f(x)=y

a function symbol from FOL sends every element from the domain
of discourse to some element from the domain of discourse.
They are assumed to be total on the domain of discourse. In ZFC

the domain of discourse is assumed to be sets, so a FOL function
symbol in FOL+ZFC maps any set to some set. Example of such
a function that maps any set to some set:

succ(x) = x u {x}

It is defined on the universal class V.

[Mostowski Collapse]

Another example of such a function f : V -> V, is the
power set operator, according to the power set axiom
of ZFC, this here is defined on the universal class:

P(x) = { y | y ⊆ x }

To distinguish functions f : V -> V from set like
functions f : X -> Y where X and Y are sets, the name
"operator" or "class function" is sometimes used.

But I didn't need to use these words, since I presented
the problem as a FOL formula, and in a FOL formula
the function symbols are all oprators:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

[Dan Christensen]

On Thursday, November 25, 2021 at 2:10:14 PM UTC-5, Mostowski Collapse wrote:

>
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 19:55:42 UTC+1:
> > On Thursday, November 25, 2021 at 1:34:07 PM UTC-5, Mostowski Collapse wrote:
> > > The co-domain of f is not given.
> > You can give it a name, e.g. y.
> > > The subset axiom doesn't work for this here:
> > > f[A] = {f(x):x in A}
> > > Why do you think you can prove existence of f[A] with subset axiom?
> > Here are the first 5 lines to get you started:
> >
> > 1 Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > Premise
> >
> > 2 Set(x)
> > Split, 1
> >
> > 3 Set(y)
> > Split, 1
> >
> > 4 ALL(a):[a in x => f(a) in y]
> > Split, 1
> >
> > 5 EXIST(a):[Set(a) & ALL(b):[b in a <=> b in y & EXIST(c):[c in x & f(c)=b]]]
> > Subset, 3
> >
> > Just 44 lines. Enjoy.

> I don't think that is what is written on Wikipedia, I don't see
> an Y in their definition of f[A]. But lets forget about Wikipedia.
>
> Lets say I have a function f : V -> V, that maps any set to some set.
> This was the function of my original problem, that is still not solved
>
> in DC Proof. How do you show that this here exists:
> f[A] = {f(x):x in A}

You give up too easily. It's only 44 lines as follows:

THEOREM

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

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


PROOF

Suppose...

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

2 Set(x)
Split, 1

3 Set(y)
Split, 1

4 ALL(a):[a in x => f(a) in y]
Split, 1

Construct the image of set x under f

Apply Subset Axiom

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

6 Set(z) & ALL(b):[b in z <=> b in y & EXIST(c):[c in x & f(c)=b]]
E Spec, 5

Define: z

7 Set(z)
Split, 6

8 ALL(b):[b in z <=> b in y & EXIST(c):[c in x & f(c)=b]]
Split, 6

Prove: z is unique

Suppose...

9 Set(z') & ALL(b):[b in z' <=> b in y & EXIST(c):[c in x & f(c)=b]]
Premise

Define: z'

10 Set(z')
Split, 9

11 ALL(b):[b in z' <=> b in y & EXIST(c):[c in x & f(c)=b]]
Split, 9

Prove: z=z'

Apply Set Equality Axiom

12 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c in a <=> c in b]]]
Set Equality

13 ALL(b):[Set(z) & Set(b) => [z=b <=> ALL(c):[c in z <=> c in b]]]
U Spec, 12

14 Set(z) & Set(z') => [z=z' <=> ALL(c):[c in z <=> c in z']]
U Spec, 13

15 Set(z) & Set(z')
Join, 7, 10

16 z=z' <=> ALL(c):[c in z <=> c in z']
Detach, 14, 15

17 [z=z' => ALL(c):[c in z <=> c in z']]
& [ALL(c):[c in z <=> c in z'] => z=z']
Iff-And, 16

Sufficient: For z=z'

18 ALL(c):[c in z <=> c in z'] => z=z'
Split, 17

'=>'

Suppose...

19 t in z
Premise

20 t in z <=> t in y & EXIST(c):[c in x & f(c)=t]
U Spec, 8

21 [t in z => t in y & EXIST(c):[c in x & f(c)=t]]
& [t in y & EXIST(c):[c in x & f(c)=t] => t in z]
Iff-And, 20

22 t in z => t in y & EXIST(c):[c in x & f(c)=t]
Split, 21

23 t in y & EXIST(c):[c in x & f(c)=t]
Detach, 22, 19

24 t in z' <=> t in y & EXIST(c):[c in x & f(c)=t]
U Spec, 11

25 [t in z' => t in y & EXIST(c):[c in x & f(c)=t]]
& [t in y & EXIST(c):[c in x & f(c)=t] => t in z']
Iff-And, 24

26 t in y & EXIST(c):[c in x & f(c)=t] => t in z'
Split, 25

27 t in z'
Detach, 26, 23

As Required:

28 ALL(c):[c in z => c in z']
Conclusion, 19

'<='

Suppose...

29 t in z'
Premise

30 t in z' <=> t in y & EXIST(c):[c in x & f(c)=t]
U Spec, 11

31 [t in z' => t in y & EXIST(c):[c in x & f(c)=t]]
& [t in y & EXIST(c):[c in x & f(c)=t] => t in z']
Iff-And, 30

32 t in z' => t in y & EXIST(c):[c in x & f(c)=t]
Split, 31

33 t in y & EXIST(c):[c in x & f(c)=t]
Detach, 32, 29

34 t in z <=> t in y & EXIST(c):[c in x & f(c)=t]
U Spec, 8

35 [t in z => t in y & EXIST(c):[c in x & f(c)=t]]
& [t in y & EXIST(c):[c in x & f(c)=t] => t in z]
Iff-And, 34

36 t in y & EXIST(c):[c in x & f(c)=t] => t in z
Split, 35

37 t in z
Detach, 36, 33

As Required:

38 ALL(c):[c in z' => c in z]
Conclusion, 29

Joining results...

39 ALL(c):[[c in z => c in z'] & [c in z' => c in z]]
Join, 28, 38

40 ALL(c):[c in z <=> c in z']
Iff-And, 39

As Required:

41 z=z'
Detach, 18, 40

z is unique

As Required:

42 ALL(a):[Set(a) & ALL(b):[b in a <=> b in y & EXIST(c):[c in x & f(c)=b]]
=> z=a]
Conclusion, 9

43 Set(z) & ALL(b):[b in z <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[Set(a) & ALL(b):[b in a <=> b in y & EXIST(c):[c in x & f(c)=b]]
=> z=a]
Join, 6, 42

As Required:

44 ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
=> EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[Set(a) & ALL(b):[b in a <=> b in y & EXIST(c):[c in x & f(c)=b]]
=> z=a]]]
Conclusion, 1

[Mostowski Collapse]

Not what was required:

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

I don't see any EXIST(b). And you restrict a to be subset of X.
But there is no f : X -> Y. The function under discussion is
an operator f : V -> V. And a is not restricted in any way, except

that it is non-empty.

[Fritz Feldhase]

On Thursday, November 25, 2021 at 8:18:45 PM UTC+1, Mostowski Collapse wrote:

> I am not considering set-like functions f : X -> Y where X and Y are sets.
> I am considering function symbols from FOL, which are f : V -> V,

It might be helpful to call these entities referred to by those symbols "(set theoretic) operations".

"P" (power) , "U" (union), etc. are such (symbols for) operations.

> where V is the universal class. For [a] function symbol [f] from FOL you

>
> can prove the following:
>
> ALL(x):EXIST(y):f(x)=y

I'd propose to use "upper case" symbols in this case, to avoid confusion (ALL(x):EXIST(y): F(x)=y).

Funny thing is that the usual symbol

f(x)

where "f" denotes a set theoretic function, actually "hides" such a set theoretic operation (which we might call "application").

Von Neumann's notation [f, x] made that "application operation" explicit by using a certain symbol for refering to it ([., .]).

Ok, we might claim that ".(.)" is the symbol in standard set theory for that operation (note that it is a binary operation V x V --> V). But it might easilly be mixed-up with the FOPL notation "<function symbol>(.)".

We can formulate things like "{f | f: A --> B}" in set theory, or "for all functions f:" [Af: ...], etc. Or even state "Ef ... f(0) = 1", etc. BUT we can't derive "Ef: f(A) = B" from "P(A) = B".

[Mostowski Collapse]

You cannot solve my problem with Wikipedia nonsense,
where f[A] ⊆ Y because A ⊆ X and f : X -> Y.

What needs to pop out at the end of the proof is
this here, and nothing else:

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

[Mostowski Collapse]

In DC Proof predicates are upper case.

[Fritz Feldhase]

On Thursday, November 25, 2021 at 8:48:45 PM UTC+1, Fritz Feldhase wrote:

> But it might easilly be mixed-up with

easily - indeed!

[Fritz Feldhase]

On Thursday, November 25, 2021 at 8:53:25 PM UTC+1, Mostowski Collapse wrote:

> In DC Proof predicates are upper case.

Didn't talk about DC Proof. Who the hell cares about DC Proof anyway? :-)

[Dan Christensen]

On Thursday, November 25, 2021 at 2:45:51 PM UTC-5, Mostowski Collapse wrote:
> Not what was required:

> > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

> I don't see any EXIST(b). And you restrict a to be subset of X.
> But there is no f : X -> Y. The function under discussion is
> an operator f : V -> V. And a is not restricted in any way, except
>
> that it is non-empty.

Do pay attention, Jan Burse!

Here I prove that, as you requested, if f is a function with domain x and codomain y, then there exists a unique subset of y that is the image of x under f.

[Mostowski Collapse]

Not requested at all. My function f : V -> V doesn't
have a set like domain x and a set like codomain y.

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

You can only put a Q.E.D. if you prove what was request.
Because Q.E.D. means that:

Inglese WWWWW Which Was What Was Wanted
Latino Q.E.D quod erat demonstrandum
https://it.wikipedia.org/wiki/Come_volevasi_dimostrare#In_altre_lingue

[Mostowski Collapse]

Here is a tableaux proof of the theorem
in FOL+ZF, using Exy for x in y:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
https://www.umsu.de/trees

The LHS ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) is an instance of the axiom schema
of replacement from ZF. The RHS ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b)))
is what was wanted.

Woa! Thats quite amazing that trees can find it.
Pitty trees doesn't show some statistics about its search.
In a blink the website shows some numbers,

but then when it has found a proof it replaces
the HTML by a tableaux refutation method proof.

[Mostowski Collapse]

You can also use |= instead of the main →, it then shows:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) entails ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))).
https://www.umsu.de/trees

But I guess the distinction between |= and → is more
something for modal logic? Here in this example the
results are the same. Maybe the vdash |- would be a

better choice than the models |=, but anyway, nice tool.

[Dan Christensen]

On Thursday, November 25, 2021 at 5:13:14 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 20:58:28 UTC+1:
> > On Thursday, November 25, 2021 at 2:45:51 PM UTC-5, Mostowski Collapse wrote:
> > > Not what was required:
> >
> > > > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > > > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> >
> > > I don't see any EXIST(b). And you restrict a to be subset of X.
> > > But there is no f : X -> Y. The function under discussion is
> > > an operator f : V -> V. And a is not restricted in any way, except
> > >
> > > that it is non-empty.
> > Do pay attention, Jan Burse!
> >
> > Here I prove that, as you requested, if f is a function with domain x and codomain y, then there exists a unique subset of y that is the image of x under f.

> Not requested at all. My function f : V -> V doesn't
> have a set like domain x and a set like codomain y.

As I have shown, you do not need a universal set V to talk about the range of a function (i.e. the image of the domain set under that function).

[Mostowski Collapse]

I nowhere use universal set. I wrote:

Not requested at all. My function f : V -> V doesn't
have a set like domain x and a set like codomain y.

This implies that V is not a set.
Whats wrong with you.

[Mostowski Collapse]

Anyway its proved by https://www.umsu.de/trees .
And DC Proof cannot prove it from its built-in
set theory axioms, because DC Proof doesn't

provide the axiom schema of replacement.
And one cannot prove it without the axiom schema
of replacement, right? Yes or yes?

[Mostowski Collapse]

From the description of the tree tool:

Supported logics
Besides classical propositional logic and first-order predicate
logic (with functions and identity), a few normal modal
logics are supported.

The word function in the above FOL context refers
to functions f : V -> V, you can prove for every function
symbol in FOL:

ALL(x):EXIST(y):f(x) = y

Even the tree tool itself can prove it:

∀x∃yf(x)=y is valid.
https://www.umsu.de/trees .

LoL

[Dan Christensen]

On Thursday, November 25, 2021 at 5:34:11 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 23:31:41 UTC+1:
> > On Thursday, November 25, 2021 at 5:13:14 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 20:58:28 UTC+1:
> > > > On Thursday, November 25, 2021 at 2:45:51 PM UTC-5, Mostowski Collapse wrote:
> > > > > Not what was required:
> > > >
> > > > > > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > > > > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > > > > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > > > > > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> > > >
> > > > > I don't see any EXIST(b). And you restrict a to be subset of X.
> > > > > But there is no f : X -> Y. The function under discussion is
> > > > > an operator f : V -> V. And a is not restricted in any way, except
> > > > >
> > > > > that it is non-empty.
> > > > Do pay attention, Jan Burse!
> > > >
> > > > Here I prove that, as you requested, if f is a function with domain x and codomain y, then there exists a unique subset of y that is the image of x under f.
> > > Not requested at all. My function f : V -> V doesn't
> > > have a set like domain x and a set like codomain y.

> > As I have shown, you do not need a universal set V to talk about the range of a function (i.e. the image of the domain set under that function).

> I nowhere use universal set. I wrote:
>
> Not requested at all. My function f : V -> V doesn't
> have a set like domain x and a set like codomain y.
> This implies that V is not a set.

The universal set is usually denoted by the symbol V. Deny it if you must. It changes nothing. It turns out to be an unnecessary construct in this case.

[Dan Christensen]

On Thursday, November 25, 2021 at 5:38:17 PM UTC-5, Mostowski Collapse wrote:
> Anyway its proved by https://www.umsu.de/trees .
> And DC Proof cannot prove it from its built-in
> set theory axioms, because DC Proof doesn't
>
> provide the axiom schema of replacement.

Like V, it too is not required to talk about the range of a function (i.e. the image of the domain of that function). Is it any wonder that the ZFC axioms are largely ignored even in pure math? Like I said, a pedagogical nightmare.

> And one cannot prove it without the axiom schema
> of replacement, right?

As we see here, using DC Proof, the proof is quite straightforward, the only axioms of set theory required being ones for subsets and set equality.

[Mostowski Collapse]

I still dont see a Q.E.D. from DC Proof of this simple
and trivial theorem. You dont find V in it. Where do you
see the class symbol V = { x | x=x } in it?

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

What drugs are you consuming that you literally
see a V? You cannot distingish motivational speech
from what is wanted. What is wanted can be proved:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) entails ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))).
https://www.umsu.de/trees

The above makes use of the axiom schema of replacement.
The axiom schema belongs to ZF and was introduced
by Abraham Fraenkel. You can read about it here:

https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

Do you think DC Proof has a menu item for it?
Or do you think its not needed for a Q.E.D.?
If its not needed for a Q.E.D. can you show a

Q.E.D. of exactly what is wanted without it? Can
you name the axioms you were using?

[Mostowski Collapse]

Maybe you get the next Able price if you can prove
it without the axiom schema of replacement, similar
like John Gabriel who got an Able price for his

new calculoose. Once a crank, always a crank. LoL

[Dan Christensen]

On Thursday, November 25, 2021 at 6:24:55 PM UTC-5, Mostowski Collapse wrote:
> I still dont see a Q.E.D. from DC Proof of this simple
> and trivial theorem.

See the conclusion on line 44:

44 ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
=> EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[Set(a) & ALL(b):[b in a <=> b in y & EXIST(c):[c in x & f(c)=b]] => z=a]]]
Conclusion, 1

> You dont find V in it.

A needless complication in this case.

[Mostowski Collapse]

Here is a screenshot of the proof, it has 31 Lines:

Screenshot of proof:
∀a∃b∀x(Exb↔∃y(Eya∧f(y)=x))|=∀a(∃zEza→∃b(∃zEzb∧∀y(Eya→Ef(y)b)))
https://www.umsu.de/trees
https://gist.github.com/jburse/241bef9f58e7c88ce843287b9862236c#gistcomment-3974810

The general idea of this kind of proofs aka
refutation method is to approach P |= Q,
by showing P, ~Q |= f.

Most likely you can take the proof and convert
it by some proof transformation into a natural
deduction proof.

But I don't have a tool right now. Would need
to think, how this could be done. The easiest would
be to look for a natural deduction proof

from the beginning.

[Mostowski Collapse]

The conclusion matches in no way what is wanted:

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

You prove z=a. Are you insane?

What are the axioms you are using? Do you
use f:x -> y. Since when belongs such an axiom
to ZFC. As I told you there is no such assumption.

Whats wrong with you? Have you lost your mind?

[Mostowski Collapse]

Here are again the requirements:
a) Prove ∀a(∃z(z in a)→∃b(∃z(z in b) ∧∀y(y in a→f(y) in b)))
b) From some axioms of set theory
c) Name the axioms

Do you see some <=> in the goal? No.

So don't introduce it. Q.E.D. says:

Inglese WWWWW Which Was What Was Wanted
Latino Q.E.D quod erat demonstrandum
https://it.wikipedia.org/wiki/Come_volevasi_dimostrare#In_altre_lingue

What is wanted is a) nothing less and nothing more.

[Dan Christensen]

On Thursday, November 25, 2021 at 6:41:04 PM UTC-5, Mostowski Collapse wrote:
> Here is a screenshot of the proof, it has 31 Lines:
>
> Screenshot of proof:
> ∀a∃b∀x(Exb↔∃y(Eya∧f(y)=x))|=∀a(∃zEza→∃b(∃zEzb∧∀y(Eya→Ef(y)b)))
> https://www.umsu.de/trees
> https://gist.github.com/jburse/241bef9f58e7c88ce843287b9862236c#gistcomment-3974810
>

Yikes! A real dog's breakfast. Thanks, but no thanks.

[Mostowski Collapse]

A few hours ago you write:

Dan Christensen schrieb am Donnerstag, 25. November 2021 um 20:30:28 UTC+1:
> You give up too easily.

https://groups.google.com/g/sci.logic/c/3CrCpBI8I2E/m/lnMRlEUJBQAJ

Now you are the dog pulling the tail.
You are the definition of an idiot.

[Dan Christensen]

On Thursday, November 25, 2021 at 6:57:19 PM UTC-5, Mostowski Collapse wrote:
> A few hours ago you write:
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 20:30:28 UTC+1:
> > You give up too easily.
> https://groups.google.com/g/sci.logic/c/3CrCpBI8I2E/m/lnMRlEUJBQAJ
>
> Now you are the dog pulling the tail.
> You are the definition of an idiot.

You are the one making basic mathematics needlessly complicated. Isn't that rather idiotic, Jan Burse?

Dan

[Mostowski Collapse]

What do you mean by "making complicated"? Do you
think I can change the reality of mathematics, like
I would be atlas and the world is on my shoulders,

and by changing my position I can change mathematics?

LoL

Thats flattering. But I cannot change mathematics.

[Mostowski Collapse]

You still use the words "necessary" or "needed" wrong
in mathematics. Has nothing to do with taste. Its
not that you can add more or less salt to a soup

here. What has mathematical content is for example
showing dependency among axioms. An axiom An
is independent from axioms A1,..,An-1 if you

can exhibit two models M1 and M2, such that:

M1 |= A1,..,An-1,An

M2 |= A1,..,An-1, ~An

Harvey Friedman and Donald A. Martin are some
names in connection with independence of axiom
schema of replacement. Interesting read is also

Kechris and Descriptive Set Theory. But I am currently
kind of rediscovering the axiom schema of replacement,
didn't know that is Dan-O-Matik Idiot applications.

[Mostowski Collapse]

You could ask on the new proof assistant stackexchange
whether DC Proof can prove this simple and trivial
theorem or not:

> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

My current hypthesis is that it needs the axiom schema of
replacement. Because there is a countermodel for the above
from the theory Z alone. So I guess there is model of M of Z, with:

M |= Z, ~ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

So lets find a model M with an operator and a domain, so
that the range is then not a set.

[Mostowski Collapse]

I don't think using another sameness, as Dan-O-Matik
suggests changes anything. Dan-O-Matik suggest to
use something else than:

f ≈ g :<=> ∀x(f(x)=g(x))

but the main problem is not same-ness. The main
problems is Dan-O-Matik style functions, that pop
out of the function axiom.

For Dan-O-Matik style identification on the natural
function f : N -> N, we can prove that every
f_c : N u {c} -> N u {c} is also such a Dan-O-Matik

style function f_c : N -> N:

∀x((ExN ∨ x=c) → f(x)=x) → ∀x(ExN → f(x)=x) is valid.
https://www.umsu.de/trees/#~6x%28ExN~2x=c~5f%28x%29=x%29~5~6x%28ExN~5f%28x%29=x%29

I wonder what else definition of same-ness would
prevent the above theorem. The above theorem doesn't
make use of sameness, there is no f ≈ g in it.

[Mostowski Collapse]

We would only get a different result when the two
occerences of the function symbol f here:

∀x((ExN ∨ x=c) → f(x)=x) → ∀x(ExN → f(x)=x) is valid.
https://www.umsu.de/trees/#~6x%28ExN~2x=c~5f%28x%29=x%29~5~6x%28ExN~5f%28x%29=x%29

If we were forced to write it with two different function
symbols and a sameness between it:

f ≈ g ∧ ∀x((ExN ∨ x=c) → f(x)=x) → ∀x(ExN → g(x)=x) ?

Its then possibly that the above fallacy of Dan-O-Matiks
function spaces and function axiom does not anymore
happen, if additionally the sameness would violate the following:

The indiscernibility of identicals:
∀ x ∀ y [ x ≈ y → ∀ F ( F x ↔ F y ) ]
https://en.wikipedia.org/wiki/Identity_of_indiscernibles

But if the above is violated then the sameness is not
an identity anymore, and all the proofs that Dan-O-Matik
did claiming uniqueness are moot, because he

didn't use an identity, but some wonky sameness.

[Mostowski Collapse]

Although wikipedia thinks that principle 1 is undisputed
and lists some doubts for principle 2. We can use the
same list of doubts for principle 1 to challenge it:

The all challenge the F in the "conception of properties
used to define indiscernibility":
- pure vesus impure properties
- qualitative versus non-qualitative properties
- intrinsic versus extrinsic properties
https://en.wikipedia.org/wiki/Identity_of_indiscernibles#Indiscernibility_and_conceptions_of_properties

***********************************************************
You could add "transcending values versus non-transcending
values", where for Dan-O-Matik f(x) is transcending when
x is not element of a domain A. He clearly lives not in the
***********************************************************

world of first order logic (FOL), where any formula A(x) is
Ok for principle 1, its part of (FOL=), i.e. first order logic with
equality. He lives in a world different from first order logic

with equality, where certain formulas A(x) are meaning less,
even when they are wellformed, because they invoke transcend
values in some function application. This is in stark contrast to

first order logic with equality (FOL=) where a wellformed
formula has a truth value from {true,false} in a model.
There is no third truth value {true,false,meaningless}.

But did DC Proof succeed in providing a calculus for such a
logic that sees formulas A(x) from a 3-valued viewpoint? He
never defined some model theory for his DC Proof.

What would be a model theory that can do that?

[Mostowski Collapse]

Dan-O-Matik flash halucinated:
> You write "It is the subset of X where the limit in
question exists. Otherwise you could not formally
construct the required function f'. "

The limit in question is the function f'!

Look at the limit, it has a parameter x0, so it maps
x0 to L. Its one and the same function as f'. Where
do you think they differ?

[Dan Christensen]

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

Dan

[Mostowski Collapse]

If your shitty function axiom is so good, then please use
the derivative of the absolute value function f(x) = |x|,

which is the following function:

g(x) = x / |x|

And please show the following mathematical theorem,
that you can find in every math textbook:

g(x) is undefined at x = 0

[Dan Christensen]

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

Dan

[Mostowski Collapse]

I don't see a proof by DC poop of:

g(x) is undefined at x = 0

LMAO!

[Mostowski Collapse]

As per your own decree, the Burse Paradox,
you cannot express it in DC poop, although you
insists that FOL function symbols and your

idiotic function axiom are necessary for
functions in DC poop. Congratulations you
shoot yourself in the foot.

Mostowski Collapse schrieb am Donnerstag, 10. Februar 2022 um 18:09:58 UTC+1:
> I don't see a proof by DC poop of:
>
> g(x) is undefined at x = 0
>
> LMAO!
>

> Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 17:27:46 UTC+1:
> > So, we have: f'(x) is 1 if x>=0, -1 for x<0, and undefined for x=0.

[Dan Christensen]

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

Dan

On Thursday, February 10, 2022 at 12:16:47 PM UTC-5, Mostowski Collapse wrote:
> As per your own decree, the Burse Paradox,
> you cannot express it in DC poop, although you
> insists that FOL function symbols and your
>

...

[Mostowski Collapse]

Here is a stretcher, getting fully into the muddy
waters of everyday mathematics. What if I had
defined g(x) as follows:

g(x) = 1 / (|x| / x)

Can you show, in DC poop:

g(x) = f'(x) where f(x) = |x|

LoL

[Dan Christensen]

On Thursday, February 10, 2022 at 3:21:47 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> Here is a stretcher, getting fully into the muddy
> waters of everyday mathematics. What if I had
> defined g(x) as follows:
>
> g(x) = 1 / (|x| / x)
>
> Can you show, in DC poop:
>
> g(x) = f'(x) where f(x) = |x|
>

You will have to settle for the informal proof I posted here yesterday, Jan Burse. A formal proof is not practical. If you disagree, let's see YOUR formal proof using ONLY the ZFC axioms with a single ZFC axiom being cited for each line of your proof. Not today??? Oh, well...

[Mostowski Collapse]

You dont need ZFC for Highschool mathematics.
All that is needed is:

0 ≠ 1

Then by Russells Definite Descriptions, this
here is provable:

~∃z /(0,0,z)

[Dan Christensen]

On Friday, February 11, 2022 at 2:22:47 AM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Freitag, 11. Februar 2022 um 06:58:11 UTC+1:
> > On Thursday, February 10, 2022 at 3:21:47 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> > > Here is a stretcher, getting fully into the muddy
> > > waters of everyday mathematics. What if I had
> > > defined g(x) as follows:
> > >
> > > g(x) = 1 / (|x| / x)
> > >
> > > Can you show, in DC poop:
> > >
> > > g(x) = f'(x) where f(x) = |x|
> > >
> > You will have to settle for the informal proof I posted here yesterday, Jan Burse. A formal proof is not practical. If you disagree, let's see YOUR formal proof using ONLY the ZFC axioms with a single ZFC axiom being cited for each line of your proof. Not today??? Oh, well...

> You dont need ZFC for Highschool mathematics.
> All that is needed is:
>
> 0 ≠ 1
>
> Then by Russells Definite Descriptions, this
> here is provable:
>
> ~∃z /(0,0,z)

So, you can't formally prove that the derivative of f(x)=|x| is -1 if x<0, +1 if x>0 and undefined if x=0. Thought so. You are busted again, Jan Burse.

[Mostowski Collapse]

No I cant in DC poop. It doesn't have function spaces.
How would you define the limit of a sequence? You
don't have sequences in DC poop.

[Dan Christensen]

On Friday, February 11, 2022 at 6:56:23 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Freitag, 11. Februar 2022 um 15:39:19 UTC+1:
> > So, you can't formally prove that the derivative of f(x)=|x| is -1 if x<0, +1 if x>0
> > and undefined if x=0. Thought so. You are busted again, Jan Burse.

> No I cant in DC Proof. It doesn't have function spaces.

Wrong again, Jan Burse. Select the Function Space option on the Sets menu. Then enter the number variables in your functions.

> How would you define the limit of a sequence? You

> don't have sequences in DC Proof.

You can construct a function mapping N to any non-empty set. That function will be a sequence. Deal with it, Jan Burse. Just admit you are wrong yet again.

[Mostowski Collapse]

Newest low in Dan-O-Matiks logic capabilities.
He doesn't see that Vacuous Truth means that

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

Is logically equivalent to TRUE, i.e.

P v ~P

He is slower than the Snake Gary in Sponge Bob.

Gary the Snail's Most SAVAGE Moments!
https://www.youtube.com/watch?v=HvBgdUXis5Y

Dan Christensen schrieb am Samstag, 12. Februar 2022 um 04:27:46 UTC+1:
> I just admit that I am an idiot.

[Dan Christensen]

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

Dan

[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.

[Mostowski Collapse]

Also you don't need much logic to see that you proved
nonsense. Its only trivial high school logic:

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 Absorbed by Conjunction:
((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) Left Hand Side TRUE is Absorbed by Implication
((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

Its then trivial to see that what 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]]]
https://dcproof.com/EmptyFunctionsUniqueV2.htm

Is logical equivalent to:
EXIST(f):[ALL(g):[g=f]]]

But such a Theorem is obviously incorrect. Since there
is more then one function possible in mathematics, for
example the functions sinus sin() and cosinus cos(),

which have sin=\=cos, so your theorem is nonsense.
When you can prove an incorrect theorem in DC poop,
this means DC poop is inconsistent.

[Jeff Barnett]

On 3/30/2022 11:14 AM, Mostowski Collapse wrote:
> Newest low in Dan-O-Matiks logic capabilities.
> He doesn't see that Vacuous Truth means that
>
> ALL(a):[a e null => Q]
>
> Is logically equivalent to TRUE, i.e.

Yes it is logically TRUE. However, that doesn't mean that Q is TRUE. I
can't tell if you know that or not.

"the moon is made of green cheese => Mr. Collapse is a smart guy" is
TRUE but doesn't tell us anything about you.
--
Jeff Barnett

[Mostowski Collapse]

Its irrelevant whether Q is true or not. Because Q drops out.
The aim is to show that what Dan-O-Matik 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]]]
https://dcproof.com/EmptyFunctionsUniqueV2.htm

Implies:

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

[Mostowski Collapse]

By Modus Ponens, if A => B, and you have proved A,
then you have also proved B:

|- A |- A => B
--------------------------------------
|- B

Dan-O-Matik might silly insist that he has only literally
proved A. But his proof also implies a proof of B.

I guess Dan-O-Matik is not aware that every proof
of a statement A implies also a proof of every

statement B, folllowing from A, thats Modus Ponens.

[Mostowski Collapse]

Maybe use this naming for what Dan-O-Matik hasnt
internalized yet about logic. He is such a baby:

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

4) Additive Associativity & Material Implication & De Morgan's laws
(P → (Q→R)) ↔ ((P∧Q) → R) is valid.
https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29

Material implication: (A => B) <=> (~A | B)
https://en.wikipedia.org/wiki/Material_implication_%28rule_of_inference%29

De Morgan's laws: ~(A & B) <=> (~A | ~B)
https://en.wikipedia.org/wiki/De_Morgan's_laws

[Mostowski Collapse]

Propositional Logic is like Rubiks Cube. Some can do
it very quick, some are not that quick.

Dan-O-Matik on the other hand doesn't master propositional
logic at all, otherwise he would post one nonsense

after the other, without seeing that some of axioms
or axiom schemas are buggy.

[Mostowski Collapse]

Corr.:

Dan-O-Matik on the other hand doesn't master propositional

logic at all, otherwise he wouldn't post one nonsense

[Dan Christensen]

On Thursday, March 31, 2022 at 3:25:58 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> Its irrelevant whether Q is true or not. Because Q drops out.
> The aim is to show that what Dan-O-Matik 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]]]
> 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]

STUDENTS BEWARE: Dan-O-Matik the numbnut in propositional logic.

[Mostowski Collapse]

So Dan-O-Matik doesn't know this meta rule of replacement,
which can be meta derived in natural deduction(*)?

P <=> Q
--------------------
A(P) <=> A(Q)

This is left as an exercise. Or lookup W. V. Quine Mathematical Logic,
you find this rule also mentioned.

Mathematical Logic Revised Edition W. V. Quine
$40.00 - ISBN 9780674554511 - 11/16/1982 - 364 pages
https://www.hup.harvard.edu/catalog.php?isbn=9780674554511

(*) BTW: it works in any complete calculus, this meta
theorem. Need not be only natural deduction, can be
also another calculus.

[Mostowski Collapse]

Here is a proof by induction, over the implicative fragment:

Base Case:
A(P) = P, A(Q) = Q, trivial (P <=> Q) / (P <=> Q)
A(P) = R, A(Q) = R, trivial (P <=> Q) / (R <=> R)

Inductive Step:
A(P) = (A1(P) => A2(P)), A(Q) = (A1(Q) => A2(Q)),
By induction hypothessis we have:
(P <=> Q) / (A1(P) <=> A1(Q))
(P <=> Q) / (A2(P) <=> A2(Q))
All we have to show that we can now create a proof
in the calculus of choice:

A1(P) <=> A1(Q) A2(P) <=> A2(Q)
--------------------------------------------------------------------------
(A1(P) => A2(P)) <=> (A1(Q) => A2(Q))

Which should be possible:

((P↔Q) ∧ (R↔S)) → ((P→R) ↔ (Q→S)) is valid.
https://www.umsu.de/trees/#%28P~4Q%29~1%28R~4S%29~5%28%28P~5R%29~4%28Q~5S%29%29

[Dan Christensen]

On Sunday, April 3, 2022 at 1:17:32 PM UTC-4, Mostowski Collapse wrote:
> Here is a proof by induction, over the implicative fragment:
>
> Base Case:
> A(P) = P, A(Q) = Q, trivial (P <=> Q) / (P <=> Q)
> A(P) = R, A(Q) = R, trivial (P <=> Q) / (R <=> R)
>
> Inductive Step:
> A(P) = (A1(P) => A2(P)), A(Q) = (A1(Q) => A2(Q)),
> By induction hypothessis we have:
> (P <=> Q) / (A1(P) <=> A1(Q))
> (P <=> Q) / (A2(P) <=> A2(Q))
> All we have to show that we can now create a proof
> in the calculus of choice:
>
> A1(P) <=> A1(Q) A2(P) <=> A2(Q)
> --------------------------------------------------------------------------
> (A1(P) => A2(P)) <=> (A1(Q) => A2(Q))
>
> Which should be possible:
>
> ((P↔Q) ∧ (R↔S)) → ((P→R) ↔ (Q→S)) is valid.
> https://www.umsu.de/trees/#%28P~4Q%29~1%28R~4S%29~5%28%28P~5R%29~4%28Q~5S%29%29

Pay attention, Jan Burse! Recall that your assignment was to formally prove using some form of NATURAL DEDUCTION that:

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

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) e x] => f1=f2]]
=> ALL(x):[Set(x) =>ALL(f1): ALL(f2):[f1=f2]]

I take it, you were unable to do so. Oh, well...

[Mostowski Collapse]

Hey Uber Moron, you prove the same way like the other
formula. You can even derive a stronger statement,
which shows the full extend of your nonsense claim:

ALL(f1): ALL(f2):[f1=f2]]

Its extremly easy, even my grandmother can do it.

The used rules of replacement are:

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 are:

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

Apply 1) to get:

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

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) e x] => f1=f2]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[(R∨¬R) & ALL(a):[a in null => f2(a) e x] => f1=f2]]

Apply 1) to get:

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

Apply 2) to get:

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

Apply 3) to get:

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

Apply EXIST(v):A when v not in A is the same as A:

ALL(x):[Set(x)
=> (R∨¬R)
& ALL(f1):ALL(f2):[f1=f2]]

Apply 2) to get:

ALL(x):[Set(x)
=> ALL(f1):ALL(f2):[f1=f2]]

Apply the Forall Instantiation rule of Natural Deduction:

[Set(null)
=> ALL(f1):ALL(f2):[f1=f2]]

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

ALL(f1):ALL(f2):[f1=f2]]

[Dan Christensen]

On Sunday, April 3, 2022 at 5:22:22 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 3. April 2022 um 21:21:35 UTC+2:
> > ALL(x):[Set(x)
> > => EXIST(f):ALL(a):[a in null => f(a) in x]
> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) e x] => f1=f2]]
> > => ALL(x):[Set(x) =>ALL(f1): ALL(f2):[f1=f2]]

> Hey Uber Moron, you prove the same way like the other
> formula. You can even derive a stronger statement,
> which shows the full extend of your nonsense claim:
>
> ALL(f1): ALL(f2):[f1=f2]]
>
> Its extremly easy, even my grandmother can do it.
>

Does she not understand what a formal proof is either?

NOT a formal proof. Sorry, Jan Burse. Each of your "replacements" need to be formally justified using some form of natural deduction. Note that, in conventional mathematics, an argument of vacuous truth cannot introduce new free variables or function images of them. You can only introduce new free variables/constants using axioms, premises or existential specification. I hope this helps.

BTW your Tree program apparently does not allow a symbol to stand for both a function and a free variable. As such, it is quite useless here. You need something based on more conventional mathematics, e.g. DC Proof.

[Ross A. Finlayson]

If you're going to express matters of relation in template and call
it "proofs" then is for what-all the proofs both affirm and negate.

I.e. for matters of definition is for what "defines" up front, then in
that "definition always carries" then that "redefinition is eliminated".

I.e., to contrasting inferences redefining each other, "redefinition is
eliminated by establishing contradiction or the un-defined".

There is whereas "after all definition carries together, they the
inferences are only mutually re-defined". That of course though
is over and under matters of definition.

This "mutual conclusion" is really the effect of the proof.


You can stop calling what you're doing "natural deduction" and
leave off at "grounds for mutual conclusion".

Unless of course you admit that "natural deduction" leaves off
all your objects as, "undefined".

That constructive inference is syllogism most all agree.

But, deductive inference is dependent in cases over the mutual,
in any case.

The affirmatory and negatory are quite different things in what
over relation they mean in the universal and existential,
quantifier disambiguation and impredicativity are usual features,
for quantifier disambiguation for the affirmatory and negatory,
what indicates a form of a model of all constructive inference,
which altogether is "mutually conclusive in the constructive".

And well-defined....

The very meaning of terms under definition, has the syllogism
and "thus", of course, is for "thusly".

Given mutual terms, proof is direct.

Here there's infinite in the numbers, universal in the domain,
inside and outside numbering in ordering, besides zero in the
numbers, one in the domain, counting, mathematics. Indeed
the primary objects are first, in their theories.

[Mostowski Collapse]

Dan-O-Matik braught up:
> non-negative real number x such the x =/= |x|.

Can we agree about the following new axiom for DC Proof?

ALL(f):ALL(g):[EXIST(a):[f(a)=/=g(a)] => f=/=g]

[Mostowski Collapse]

It becomes evident that Dan-O-Matiks psychosis is
based on his age old confusion of "the" with "a".

He writes axioms like:

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

But thinks about them in terms of:

1 ALL(f):ALL(g):THE(dom):THE(cod):[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

Just plain crazy....

THE: Is his mind reading quantifier.

[Ross A. Finlayson]

Arithmetic?

There are at least two ways,
rolling over and rolling under.

Subtraction, might as well be undefined,
for zero, it being a limit ordinal and all.

I.e "don't forget to leave out what you left sitting in the middle."

"Number theory" writ large, conveniently includes arithmetic.

[Ross A. Finlayson]

You know thinking about it since knowing addition and substraction were complementary,
and that sums commute, for a long time I thought of "the numbers" as "from negative infinity
to infinity", probably because I had a picture of numbers as the XY chart, with zero the origin
in the middle. Yet, in the organization of array, zero is usally the origin in the corner, while
building out enough diagonals and back in to build the rectangular, is instead in columns and
rows, what organize "numbers" as a model, in computer or machine arithmetic, simply arithmetic.

Then, _starting_ with the numbers "only positive integers then only non-integer part", or, "positive
integers and their fractions and the finite sums of those fractions, rational numbers".

I.e., the at least two models are where the integers roll-over and fraction roll-under, clock arithmetic
or the modular respectively, about values in the integers upon which continuous functions live. (Exist.)

There is building the rationals for example as plain fractions, then for arithmetic, about keeping in
the terms, what are all additive constructs as result also even rounds.

An example is complex arithmetic and matrix rotations being undefined at 90 degrees,
because "requires floating point identity not necessarily 0, to be define, no different
that zero, for not having the 'worst case' at the 'simplest, identity case'".

When there are only four orientations anyways, it makes sense to simply as well enough
compute the coordinates, as the eight cases what result, where it's defined.

So, "Dan's 'a framework of the generally undefined'", results in a soup of sorts, what
is "simply never backward".

I.e. though there's writing out backward and what results, to be included anywhere
there is writing forward, it's his own fault for leaving it out.

Basically there is theory with universal and void, the elementary and domains.

Then that it's "0,1", "0, infinity", it subsumes the attachment, results the sublime theorems,
for the "fundamental theories of 0, 1, and infinity", what are fundamental in the elementary,
and sublime in the domain, or fundamental in the domain and sublime in the elementary,
it's a so necessarily and relevant attachment that then sets uncontradicted, definition.

According to arithmetic....

That there's category of domain in arithmetic is for number theory,
what for category of domain in arithmetic is topology.

Number theory and topology reflect together, even for that
"number theory is geometry and also topology is geometry",
for a geometry of numbers and a topology of geometry.

Then, this "point and space theory" is "topology, ..., geometry".

While directly and simply category of domain....


See, now the usual "original theory" is much simpler and quite abstract.

[Ross A. Finlayson]

When "subtraction's not defined for all numbers or elements"
it's always element of a model. This is in a sense that "in model
theory in logic when there is a model of elements their relations,
then carrying the relation on the model is the same as the logic".

So, there are two models, "addition and subtraction, defined",
and "addition and not-addition, where the model says or model
does-not-say, results of addition".

Then model theory is most usual for having two theories with
the same model, or of course two theories with different models,
and how their sub-models and super-models are the same
(or different, or, opposite).

This way "substraction, and, not-subtraction" are as well defined
as "addition, and, not-addition".

Otherwise there is closing in terms the complementary then
erasing except as "defined, also closed".

Then, "completeness" is generally in terms of model while
"closedness" or "closure", is in the "defined and not-defined".

Then, that some have the integers with infinity, is for its
properties where undefined as "not-complete" or "not-compact",
that also it's "infinity" that defines "complete" or "compact".

Here for example "-1 is undefined as an element, that according
to the axiomatization of elements existing must exist, the element
to have any properties, obviously it is its own defined term".


Then, the point of languages like ZF set theory with "only two
defined terms Empty Set and Regular Well-Founded Infinite
Set, the rest resulting after existence the logical axioms in relation
where the only relation is "element-of" that also the only elements
are "defined by their elements", except Empty Set defining one set",
then for example is for first that counting numbers fit.

Which results all the arithmetic on sets combined with their membership
properties and regularity and well-foundedness....

There is for example "in the language of domains, each has their own
empty set representing the relation in types via placeholder", or,
"that there is an infinite set defines more than one, infinite 'set',
by its members or what it contains or what is an element of it",
just reminds of the symmetric and complementary relations, which
in all infinite arithmetic fully let out or roll over that rolls under, while,
when only needing closed categories, they roll over to roll over,
making just as natural a model and even directly, what all suffices
for elements of arithmetic from the elements, or from the domain.

Of course this is usually enough called "schemes" that result for
under one big scheme, of transfinite induction, it's not relevant
writing out the each case "and for k (+++...), +1, ...", from writing
"for each k: k+1".

"Garbage in : garbage out" is the usual idea that "inferences are
blameless, but stipulations aren't", that those would or could be
"false axioms" to otherwise unqualifiedly "declare their domain
and elements and a model".

Then, the point is relation to fallacy is close: the "arguments ad ...",
are _not erroneous_ in the sense of existing grounds for mutual
conclusion, only _erroneous to not negate from defined_ what
results "their conclusion, their conclusion, their conclusion, ...".

This is where "a true negatory and affirmatory logic has no prototype
of non-logical fallacy, because all contradictions have the same form
as the Liar, which is not necessarily a logical paradox".




(Of course one can define numbers including in terms infinity - (infinity - 0),
infinity - (infinity - 1), ... resulting in a model of positive integers by "subtraction",
and a limit ordinal, with that basically "only pairs cancel" instead of "zeros are zero".)

[Mostowski Collapse]

Now I can prove the following, all non-empty
identity functions are equal:

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

Where idfun(f) is defined as:

idfun(f) <=> EXIST(dom):[EXIST(a): a in dom <----- NEW
& ALL(a):[a in dom => f(a) in dom]]

In Terrence Tao id : X->X are differnent for
different X. Even in set theory this is the case.

LMAO!

Dan Christensen schrieb am Freitag, 15. April 2022 um 20:03:12 UTC+2:
> NEW FUNCTION EQUALITY AXIOM (1 variable)
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>
> & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
>
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
>
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

[Mostowski Collapse]

So Dan Christensen still does not
believe that you cannot infer:

f : X -> X <=> ALL(a):[a in X => f(a) in X]

Easy counter example f = {(1,1),(2,2)} and X={1}, it
satisfies ALL(a):[a in X => f(a) in X], but it does not
satisfy f : X -> X, since dom(f)={1,2} =/= X.

Dan Christensen schrieb am Montag, 18. April 2022 um 19:26:50 UTC+2:
> > Hence "f: X --> X" means "f is a function with domain X and codomain X."
> You can also infer this from: ALL(a):[a in x => f(a) in x].
> Ultimately, it must come to this even with your "set theoretic" approach.

[Dan Christensen]

On Monday, April 18, 2022 at 4:33:24 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Montag, 18. April 2022 um 19:26:50 UTC+2:
> > > Hence "f: X --> X" means "f is a function with domain X and codomain X."
> > You can also infer this from: ALL(a):[a in x => f(a) in x].
> > Ultimately, it must come to this even with your "set theoretic" approach.

> So Dan Christensen still does not
> believe that you cannot infer:
>
> f : X -> X <=> ALL(a):[a in X => f(a) in X]
>

Informally, they mean the same thing.

> Easy counter example f = {(1,1),(2,2)} and X={1}, it
> satisfies ALL(a):[a in X => f(a) in X], but it does not
> satisfy f : X -> X, since dom(f)={1,2} =/= X.
>

You really have two functions here. One with domain {1}, the other with a domain {1, 2}. No wonder you are confused, Jan Burse!

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 12:57:23 AM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 4:33:24 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
>
> > Dan Christensen schrieb am Montag, 18. April 2022 um 19:26:50 UTC+2:
> > > > Hence "f: X --> X" means "f is a function with domain X and codomain X."
> > > You can also infer this from: ALL(a):[a in x => f(a) in x].
> > > Ultimately, it must come to this even with your "set theoretic" approach.
> > So Dan Christensen still does not
> > believe that you cannot infer:
> >
> > f : X -> X <=> ALL(a):[a in X => f(a) in X]
> >
> Informally, they mean the same thing.

No, they don't.

Try to get that streight, idiot:

> > Easy counter example f = {(1,1),(2,2)} and X={1}, it
> > satisfies ALL(a):[a in X => f(a) in X], but it does not
> > satisfy f : X -> X, since dom(f)={1,2} =/= X.
> >
> You really have two functions here.

No, idiot. MC explicitly defined f the following way: f = {(1,1),(2,2)}, so there are no "two" functions, it's just f. Hint: dom(f) = {1, 2} and img(f) = {1, 2}).

In a "mathematical" context we might rather define f the following way:

"We define the function f: {1, 2} --> {1, 2} with f(x) = x for all x e {1, 2}."

Still with me?

Now, let X = {1}. Then clearly

Ax(x e X --> f(x) e X) ,

BUT "informally" (i. e. certainly) of course NOT

f: {1} --> {1}.

Since f is NOT defined as a function from {1} to {1} (i. e. a function with domain {1} and image c {1}).

Hence "ALL(a):[a in X => f(a) in X]" does n o t "mean" the same as "f: X --> X".

______________

Your claim "You really have two functions here" is rather funny! :-)

I guess you had the following two functions in mind here:

f: {1, 2} --> {1, 2}, defined with f(x) = x for all x e {1, 2}
g: {1} --> {1}, defined with g(x) = x for all x e {1}

And right, f =/= g (since dom(f) =/= dom(g)).

But didn't you CLAIM that Tao's (and hence your) approach does not allow for deriving that result, since these "two" functions don't have the same domains and codomans?

Hint: Of course, in the context lf the usual "set theoretic" approach it's trivial to derive

f =/= g.

Implying

card({f, g}) = 2 ,

which justifies talking about "two" functions f and g.

Why don't you like math, Dan?

[Dan Christensen]

On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 12:57:23 AM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 4:33:24 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> >
> > > Dan Christensen schrieb am Montag, 18. April 2022 um 19:26:50 UTC+2:
> > > > > Hence "f: X --> X" means "f is a function with domain X and codomain X."
> > > > You can also infer this from: ALL(a):[a in x => f(a) in x].
> > > > Ultimately, it must come to this even with your "set theoretic" approach.
> > > So Dan Christensen still does not
> > > believe that you cannot infer:
> > >
> > > f : X -> X <=> ALL(a):[a in X => f(a) in X]
> > >
> > Informally, they mean the same thing.
> No, they don't.
>

> > > Easy counter example f = {(1,1),(2,2)} and X={1}, it
> > > satisfies ALL(a):[a in X => f(a) in X], but it does not
> > > satisfy f : X -> X, since dom(f)={1,2} =/= X.
> > >
> > You really have two functions here.

> No. MC explicitly defined f the following way: f = {(1,1),(2,2)}, so there are no "two" functions, it's just f. Hint: dom(f) = {1, 2} and img(f) = {1, 2}).

I guess Jan Burse (MC) and others are free to use unconventional definitions that produce these results, though I can't imagine why. I will stick to those used in most modern math textbooks, e.g. Tao. There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X.

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 6:37:56 AM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> >

> > There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X].

No, we don't have that.

Hint: Consider the function f: {1, 2} --> {1, 2} with f(x) = x for all x e {1, 2}.

If X = {1}, then X is a non-empty set and ALL(a):[a in X => f(a) in X], BUT we don't have f: X --> X (since f: {1, 2} --> {1, 2}, and {1} =/= {1, 2}). Hence it's NOT the case that we have f: X --> X <=> ALL(a):[a in X => f(a) in X] for any non-empty set X. qed

[Mostowski Collapse]

Like the 1000-time, tring to explain Dan Christensen
how basic logic works. Basic logic based on ALL(_) and =>.

Dan Christensen still doesn't get it what his ALL(a):[a in X => f(a) in X]
does. That it is CONTRAVARIATE in the domain, and COVARIATE

in the codomain. This is just Aristoteles BARBARA....

LoL

[Mostowski Collapse]

We know that John Gabriel was educated on a cow
farm in africa. But where did Dan Christensen

his education from?

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 11:16:17 AM UTC+2, Mostowski Collapse wrote:
>
> Dan Christensen still doesn't get it what his ALL(a):[a in X => f(a) in X] does.

Indeed. Seems that he doesn't get that it will (at least) hold for _all_ X c A if f: A --> A.

Hence it does NOT "mean the same" as f: A --> A.

Moreover, It will especially hold for each and every function f, if X = {} (though he tried to "exclude" that case by an additionl clause in his infamous axiom). Hence each and every function has an empty domain?

Seems that he considers a bug a feature. Problems even h e cannot deny are fixed by some ad hoc patches.

[Fritz Feldhase]

His whole approach concerning "functions" in DC Proof is bogus, though he once KNEW that (set-theoretic) functions are (defined as) certain (namely functional) sets of ordered pairs (it seems to me). The latter approach allows to determine the domain of a "given" function.

Why on earth doesn't he just adopt that rather straightforward approach?

It seems to me that he doesn't undertand the "foundational" role of set theory in "classical mathematics". Though most textbooks might not explicitly state ZFC and point out its role as a foundation of the material covered in the book, it is well known that ZFC d o e s deliver such a foundation. (One might just read the first page in Zermelo's famous paper from 1908 where he introduced his set theory.)

[Mostowski Collapse]

Carful with the axe. If you have f : A -> A, it holds for all X c A and all A c Y,
that ALL(a):[a e X -> f(a) e Y]. But you cannot always shrink the domain
and the codomain at the same time. For the identity function it would work,

shrinking both domain and codomain. But in general the domain is
contravariat, i.e. X c A and the codomain is covariate A c Y.

[Mostowski Collapse]

Here is an example of a smaller domain, but the codomain
doesnt get smaller, because the function is not injective:

f = {(1,1), (2,2), (3,2)} , its dom(f) = {1,2,3} and ran(f) = {1,2}.
I am using ran for range and not img for image.

Now if you restrict the function to X = {1,2}, i.e. look at
f | X defined as { (x,y) | (x,y) e f & x e X } then you get:

f | X = { (1,1), (2,2) }

But althouge you restricted the function to a smaller domain,
the range didnt get smaller we still have:

ran(f | X) = {1,2}

Its possible to translate Dan Christensens formula into a
expression using the restrict operator |. Maybe this could

help Dan Christensen to better think about it:

ALL(a):[a e X => f(a) e Y]

it is the same as stating:

ran(f | X) c Y

which is far away from what f : X -> Y states.

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 4:54:03 PM UTC+2, Mostowski Collapse wrote:

> Carful with the axe. If you have f : A -> A, it holds for all X c A and all A c Y,
> that ALL(a):[a e X -> f(a) e Y]. But you cannot always shrink the domain
> and the codomain at the same time.

Jep. You are right. Was slightly too fast.

> For the identity function it would work,
> shrinking both domain and codomain. But in general the domain is
> contravariat, i.e. X c A and the codomain is covariate A c Y.

So let's assume that f = id_A (i. e. consider a special case).

Thanks for the hint.

[Dan Christensen]

On Tuesday, April 19, 2022 at 1:55:32 AM UTC-4, Fritz Feldhase wrote:
> On Tuesday, April 19, 2022 at 6:37:56 AM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> > >
> > > There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X].
>
> No, we don't have that.
>
> Hint: Consider the function f: {1, 2} --> {1, 2} with f(x) = x for all x e {1, 2}.
>
> If X = {1}, then X is a non-empty set and ALL(a):[a in X => f(a) in X], BUT we don't have f: X --> X (since f: {1, 2} --> {1, 2}, and {1} =/= {1, 2}).

Makes no sense. You seem to be using the same variable X to represent both {1} and {1, 2}. Try using different names for each.

> Hence it's NOT the case that we have f: X --> X <=> ALL(a):[a in X => f(a) in X] for any non-empty set X. qed

I don't know what convention you are using here, but I think most math textbooks treat f: X --> X as the logical equivalent of ALL(a):[a in X => f(a) in X].

[Fritz Feldhase]

On Wednesday, April 20, 2022 at 9:50:09 PM UTC+2, Dan Christensen wrote:
> On Tuesday, April 19, 2022 at 1:55:32 AM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, April 19, 2022 at 6:37:56 AM UTC+2, Dan Christensen wrote:
> > > On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> > > >
> > > > There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X].
> > > >
> > No, we don't have that.
> >
> > Hint:

Let Y = {1, 2}.

Now consider the function f: Y --> Y defined with f(x) = x for all x e Y

and let X = {1}.

Then X is a non-empty set and ALL(a):[a in X => f(a) in X].

BUT we don't have f: X --> X (since we defined f as f: Y --> Y, and X =/= Y).

HENCE it's NOT the case that we have f: X --> X <=> ALL(a):[a in X => f(a) in X] for any non-empty set X. qed

> [...] but I think most math textbooks treat f: X --> X as [...] equivalent [with] ALL(a):[a in X => f(a) in X].

Mind to quote such a claim/statement? (Did you see it in Mückenheim's textbook? Or in one of Archies books?)

Hint: We already told you:

YES: AX: f: X --> X => ALL(a):[a in X => f(a) in X]

NO: AX: f: ALL(a):[a in X => f(a) in X] => f: X --> X.

See proof from above.

[Dan Christensen]

On Wednesday, April 20, 2022 at 4:21:13 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 20, 2022 at 9:50:09 PM UTC+2, Dan Christensen wrote:
> > On Tuesday, April 19, 2022 at 1:55:32 AM UTC-4, Fritz Feldhase wrote:
> > > On Tuesday, April 19, 2022 at 6:37:56 AM UTC+2, Dan Christensen wrote:
> > > > On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> > > > >
> > > > > There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X].
> > > > >
> > > No, we don't have that.
> > >
> > > Hint:
> Let Y = {1, 2}.
>
> Now consider the function f: Y --> Y defined with f(x) = x for all x e Y
>

Looks suspiciously like ALL(x):[x in Y => f(x) in Y]

> and let X = {1}.
>
> Then X is a non-empty set and ALL(a):[a in X => f(a) in X].
>
> BUT we don't have f: X --> X (since we defined f as f: Y --> Y, and X =/= Y).
>
> HENCE it's NOT the case that we have f: X --> X <=> ALL(a):[a in X => f(a) in X] for any non-empty set X. qed
>

Thanks, but I think I will stick the usual convention of f: X --> Y being an informal abbreviation of ALL(a):[a in X => f(x)].

> > [...] but I think most math textbooks treat f: X --> X as [...] equivalent [with] ALL(a):[a in X => f(a) in X].
>
> Mind to quote such a claim/statement?
>

"Arrow Notation

"The notation f:S→T means f is a function with domain S and codomain T. ...

"Pronunciation of arrow notation

"The expression "f:A→B" can be used as a name or as an independent sentence.

- Standing alone, the expression may be read aloud this way: 'f is a function from A to B' or 'f goes from A to B'.

- The expression may occur embedded in a sentence, as in 'Let f:A→B be a differ­entiable function.' This may be read 'Let f from A to B be a differ­entiable function.'"

https://abstractmath.org/MM/MMFuncNotation.htm#:~:text=Arrow%20Notation,it%20from%20barred%20arrow%20notation.

Pretty sure this isn't from Mucke or Archie Poo.

[Fritz Feldhase]

On Wednesday, April 20, 2022 at 10:51:11 PM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 4:21:13 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, April 20, 2022 at 9:50:09 PM UTC+2, Dan Christensen wrote:
> > > On Tuesday, April 19, 2022 at 1:55:32 AM UTC-4, Fritz Feldhase wrote:
> > > > On Tuesday, April 19, 2022 at 6:37:56 AM UTC+2, Dan Christensen wrote:
> > > > > On Monday, April 18, 2022 at 7:32:39 PM UTC-4, Fritz Feldhase wrote:
> > > > > >
> > > > > > There, for any non-empty set X, we have f: X --> X <=> ALL(a):[a in X => f(a) in X].
> > > > > >
> > > > No, we don't have that.
> > > >
> > > > Hint:
> >
> > Let Y = {1, 2}.
> >
> > Now consider the function f: Y --> Y defined with f(x) = x for all x e Y
> >

> Looks suspiciously like <bla>

What's the matter with you, you silly asshole?

Hint: Our definition of f implies for all X c Y:

Ax(x e X -> f(x) = x).

Y is just o n e such X (if Y =/= {}).

Now

> > let X = {1}.
> >
> > Then X is a non-empty set and ALL(a):[a in X => f(a) in X].

Can't you get that simple fact, idiot?

> > BUT we don't have f: X --> X (since we defined f as f: Y --> Y, and X =/= Y).

And

> > HENCE it's NOT the case that we have f: X --> X <=> ALL(a):[a in X => f(a) in X] for any non-empty set X. qed

Got it?

Are you demented or what?

> Thanks, but I think I will

Seems that you are.

Just like WM.

> > > [...] I think most math textbooks treat f: X --> X as [...] equivalent [with] ALL(a):[a in X => f(a) in X].

> >
> > Mind to quote such a claim/statement?

Still no such quote? Yeah, thought so.

Did you check WM's and AP's textbooks too?

[Fritz Feldhase]

On Thursday, November 25, 2021 at 10:17:23 AM UTC+1, Mostowski Collapse wrote:

> DC Proof creator Dan-O-Matik suffers from some major
> didactic deficiencies:
>
> 1) Errorneously translates "the X is Y" into "all X are Y".

Maybe he was missled by the following fact:

P(a) <-> Ax(x = a -> P(x).

Of course, the following is nonsense:

* P(ix Q(x)) <-> Ax(Q(x) -> P(x)).

While "All present kings of France are bald" is clearly true the truth value of "The present king of France is bald" may be open to some debate. (Russell's approach would lead to /false/.)

> 2) Denies that ZFC is integral part of modern basic math.

What an idiot.

Ok, most textbooks may not explicitly state the axioms of ZFC, but the latter still "is present" - at least as a "backgroud theory". Actually, most of ZFC's notions may be formulated and/or used quite "naturally". In analysis we usually define sets as subsets of some "domain set": "Let M = {x e IR : ...x...}."

Moreover: "classical mathematics refers generally to the mainstream approach to mathematics, which is based on classical logic and ZFC set theory." (Wikipedia)

On the other hand, it's certainly not an integral part of DC Spoof.

[Mostowski Collapse]

The biggest problem, he denies his own U Spec inference rule:

Dan Christensen schrieb am Donnerstag, 21. April 2022 um 16:30:36 UTC+2:
> > the ad hoc axiom can prove g ~ h with g(-1/2)=1/2 & h(-1/2)=1/2,
> Another domain? Make up your mind, Jan Burse!

Thats just like Putin, no we didn't invade Ukraine. Balant denial.