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?

You seem to be getting more desperate by the hour, Jan Burse! See my reply to your identical posting at sci.logic just now.

Dan

On Thursday, November 25, 2021 at 4:15:39 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".
>
> 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?

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

Dan Christensen schrieb am Donnerstag, 25. November 2021 um 17:14:17 UTC+1:
> You seem to be getting more desperate by the hour, Jan Burse! See my reply to your identical posting at sci.logic just now.
>
> Dan
> On Thursday, November 25, 2021 at 4:15:39 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".
> >
> > 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?

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.

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 18:17:07 UTC+1:
> 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
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 17:14:17 UTC+1:
> > You seem to be getting more desperate by the hour, Jan Burse! See my reply to your identical posting at sci.logic just now.
> >
> > Dan
> > On Thursday, November 25, 2021 at 4:15:39 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".
> > >
> > > 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?

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 schrieb am Donnerstag, 25. November 2021 um 18:42:34 UTC+1:
>> 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.

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

Dan

On Thursday, November 25, 2021 at 1:37:20 PM UTC-5, 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?
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 18:42:34 UTC+1:
> >> 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.

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

Dan Christensen schrieb am Donnerstag, 25. November 2021 um 21:57:20 UTC+1:
> See my reply today to your identical posting at sci.logic.
>
> Dan
> On Thursday, November 25, 2021 at 1:37:20 PM UTC-5, 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?
> > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 18:42:34 UTC+1:
> > >> 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.

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 schrieb am Donnerstag, 25. November 2021 um 23:18:01 UTC+1:
> 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
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 21:57:20 UTC+1:
> > See my reply today to your identical posting at sci.logic.
> >
> > Dan
> > On Thursday, November 25, 2021 at 1:37:20 PM UTC-5, 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?
> > > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 18:42:34 UTC+1:
> > > >> 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.

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.

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 23:19:13 UTC+1:
> 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 schrieb am Donnerstag, 25. November 2021 um 23:18:01 UTC+1:
> > 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
> > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 21:57:20 UTC+1:
> > > See my reply today to your identical posting at sci.logic.
> > >
> > > Dan
> > > On Thursday, November 25, 2021 at 1:37:20 PM UTC-5, 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?
> > > > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 18:42:34 UTC+1:
> > > > >> 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.

Mostowski Collapse wrote:

> 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

ohh my butt, they are even saying the capitalism destroyed eastern europe,
but the capitalists isn't getting it. As we speak. Ie, eating kids from
capitalist china, saving the climate same time!!

PROJECT EAT HUMAN BABIES TO SOLVE WORLD HUNGER- CANNIBALISM TO GO
MAINSTREAM IN SCHOOLS (PURE EVIL)
https://153news.net/watch_video.php?v=Y6Y313YOYH79
🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴
🔴🔴🔴🔴🔴🌕🌕🔴🌕🌕🔴🔴🔴🔴🔴
🔴🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴🔴🔴
🔴🔴🔴🌕🌕🌕🌕🔴🔴🔴🌕🌕🔴🔴🔴
🔴🔴🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🌕🔴🔴
🔴🌕🌕🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🔴🔴
🔴🔴🌕🌕🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴
🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🔴
🔴🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🌕🌕🌕🔴
🔴🔴🔴🔴🌕🔴🔴🔴🌕🌕🌕🌕🌕🔴🔴
🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🔴
🔴🌕🌕🌕🔴🌕🌕🌕🌕🌕🌕🌕🌕🔴🔴
🔴🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴
🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴

Micro penis tells his life:
> ohh my butt

Brain Hubbs schrieb am Freitag, 26. November 2021 um 00:01:25 UTC+1:
> Mostowski Collapse wrote:
>
> > 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
> ohh my butt, they are even saying the capitalism destroyed eastern europe,
> but the capitalists isn't getting it. As we speak. Ie, eating kids from
> capitalist china, saving the climate same time!!
>
> PROJECT EAT HUMAN BABIES TO SOLVE WORLD HUNGER- CANNIBALISM TO GO
> MAINSTREAM IN SCHOOLS (PURE EVIL)
> https://153news.net/watch_video.php?v=Y6Y313YOYH79
> 🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴
> 🔴🔴🔴🔴🔴🌕🌕🔴🌕🌕🔴🔴🔴🔴🔴
> 🔴🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴🔴🔴
> 🔴🔴🔴🌕🌕🌕🌕🔴🔴🔴🌕🌕🔴🔴🔴
> 🔴🔴🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🌕🔴🔴
> 🔴🌕🌕🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🔴🔴
> 🔴🔴🌕🌕🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴
> 🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🔴
> 🔴🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🌕🌕🌕🔴
> 🔴🔴🔴🔴🌕🔴🔴🔴🌕🌕🌕🌕🌕🔴🔴
> 🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🔴
> 🔴🌕🌕🌕🔴🌕🌕🌕🌕🌕🌕🌕🌕🔴🔴
> 🔴🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴
> 🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴

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.

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 schrieb am Freitag, 4. Februar 2022 um 18:31:46 UTC+1:
> 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.

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:

They 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 schrieb am Freitag, 4. Februar 2022 um 18:39:03 UTC+1:
> 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 schrieb am Freitag, 4. Februar 2022 um 18:31:46 UTC+1:
> > 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.

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?

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

To formally construct the real numbers and the required arithmetic operations is a massive project of literally tens of thousands of lines of formal proof. I will leave it to you as an exercise, Jan Burse.

Informally then...

f(x) = |x| = x for x>=0, -x for x <0. Compare that left and right-hand limits at x=0.

Right limit: Lim(h-->0+): ((f(0+h) - f(0))/h) = h/h = 1 (the slope of y=f(x) for x >= 0)

Left Limit: Lim(h-->0-): ((f(0+h) - f(0))/h) = -h/h = -1 (the slope of y=f(x) for x < 0)

The left and right-hand limits differ at x=0, so the limit does not exist there. Thus, the derivative of f(x)=|x| is said to be undefined at x=0.

So, we have: f'(x) is 1 if x>=0, -1 for x<0, and undefined for x=0.

I hope this helps sort out your wonky math, Jan Burse. (He likes to make "dark" inferences about functions outside of their domain in his wonky system. Really quite useless.)

Dan

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

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:
> To formally construct the real numbers and the required arithmetic operations is a massive project of literally tens of thousands of lines of formal proof. I will leave it to you as an exercise, Jan Burse.
>
> Informally then...
>
> f(x) = |x| = x for x>=0, -x for x <0. Compare that left and right-hand limits at x=0.
>
> Right limit: Lim(h-->0+): ((f(0+h) - f(0))/h) = h/h = 1 (the slope of y=f(x) for x >= 0)
>
> Left Limit: Lim(h-->0-): ((f(0+h) - f(0))/h) = -h/h = -1 (the slope of y=f(x) for x < 0)
>
> The left and right-hand limits differ at x=0, so the limit does not exist there. Thus, the derivative of f(x)=|x| is said to be undefined at x=0.
>
> So, we have: f'(x) is 1 if x>=0, -1 for x<0, and undefined for x=0.
>
> I hope this helps sort out your wonky math, Jan Burse. (He likes to make "dark" inferences about functions outside of their domain in his wonky system. Really quite useless.)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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.

On Thursday, February 10, 2022 at 12:09:58 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> I don't see a proof by DC poop of:
> g(x) is undefined at x = 0

I guess that example was a bit complicated for you, Jan Burse. Here is simpler example from DC Proof. Only 3 lines.

Define the function f on set x such that:

1. ALL(a):[a in x => f(a) in x]
Axiom

Suppose...

2. ~t in x
Premise

Specifying that a=t in (1), we obtain:

3. t in x => f(t) in x
U Spec, 1

The definition of f (line 1) tells us nothing about elements NOT in x. In this case, we say that f(t) is UNDEFINED.

Get it? Didn't think so. Oh, well...

Dan

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

On Thursday, February 10, 2022 at 12:09:58 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> I don't see a proof by DC poop of:
> g(x) is undefined at x = 0

I guess that example was a bit complicated for you, Jan Burse. Here is simpler example from DC Proof. Only 3 lines.

Define the function f on set x such that:

1. ALL(a):[a in x => f(a) in x]
Axiom

Suppose...

2. ~t in x
Premise

Specifying that a=t in (1), we obtain:

3. t in x => f(t) in x
U Spec, 1

The definition of f (line 1) tells us nothing about elements NOT in x. In this case, we say that f(t) is UNDEFINED.

In summary: If ALL(a):[a in x => f(a) in x] & ~t in x then f(t) is UNDEFINED.

Get it? Didn't think so. Oh, well...

Dan

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

On Thursday, February 10, 2022 at 12:09:58 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> I don't see a proof by DC poop of:
> g(x) is undefined at x = 0

I guess that example was a bit complicated for you, Jan Burse. Here is simpler example from DC Proof. Only 3 lines.

Define the function f on set x such that:

1. ALL(a):[a in x => f(a) in x]
Axiom

Suppose...

2. ~t in x
Premise

Specifying that a=t in (1), we obtain:

3. t in x => f(t) in x
U Spec, 1

The definition of f (line 1) tells us nothing about elements NOT in x. In this case, we say that f(t) is UNDEFINED.

In summary: If f, x and t are such that ALL(a):[a in x => f(a) in x] & ~t in x, then, without any further information, we can say that f(t) is UNDEFINED.

Get it? Didn't think so. Oh, well...

Dan

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

And why can I prove in DC poop:

g(0) - g(0) = 0

When g(0) is indefined?

Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 20:43:57 UTC+1:
> In summary: If f, x and t are such that ALL(a):[a in x => f(a) in x] & ~t in x, then, without any further information, we can say that f(t) is UNDEFINED.

On Thursday, February 10, 2022 at 2:53:29 PM UTC-5, Mostowski Collapse wrote:
> And why can I prove in DC poop:
>
> g(0) - g(0) = 0
>

Let's see your proof.

Dan

I mean why can I not prove in DC poop:

g(0) - g(0) ≠ 0

Highschool math will tell me, when g(0)
is undefined, then undefined - undefined is
undefined and undefined is not zero.
Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 21:01:43 UTC+1:
> On Thursday, February 10, 2022 at 2:53:29 PM UTC-5, Mostowski Collapse wrote:
> > And why can I prove in DC poop:
> >
> > g(0) - g(0) = 0
> >
> Let's see your proof.
>
> Dan