And what do you construct to determine f differentiable.

A penguin?

If crankness had a name, it would be Dan-O-Matik.

Dan Christensen schrieb am Mittwoch, 9. Februar 2022 um 20:27:00 UTC+1:
> On Wednesday, February 9, 2022 at 1:50:13 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> > WHATS WRONG WITH YOU, JAN BURSE?????
> >
> > Where do you see the domain of f' given
> > for example for the problem f : R -> R, f(x) = |x|.
> >
> In a formal proof anyway, you first need to construct, i.e. prove the existence of the subset D of R where f is differentiable. In this case D = R \ {0}. Only then can you construct a function f' on D such that f'(x) = -1 for x<0, and +1 for x>0.
>
> Remember: First comes domains and codomains, THEN comes functions. I hope this helps.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, February 9, 2022 at 3:32:17 PM UTC-5, Mostowski Collapse wrote:
> And what do you construct to determine f differentiable.
>

See Tao's definition of differentiability recently quoted here.

Dan

He defines when we are allowed to write:

f'(x) = L

Where do you see a domain of f' declared?
What is its variable name in Terence Tao for the domain of f'?
The variable name X is the domain of f, and not of f'.

You are confused.

Dan Christensen schrieb am Mittwoch, 9. Februar 2022 um 21:47:37 UTC+1:
> On Wednesday, February 9, 2022 at 3:32:17 PM UTC-5, Mostowski Collapse wrote:
> > And what do you construct to determine f differentiable.
> >
> See Tao's definition of differentiability recently quoted here.
>
> Dan

On Wednesday, February 9, 2022 at 3:55:57 PM UTC-5, Mostowski Collapse wrote:
> He defines when we are allowed to write:
>
> f'(x) = L
>
> Where do you see a domain of f' declared?
> What is its variable name in Terence Tao for the domain of f'?

It is the subset of X where the limit in question exists. In a formal mathematical proof, you would have to name it. Otherwise you could not formally construct the required function f'. Maybe in philosophy class, but not in math.

Dan

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

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 schrieb am Mittwoch, 9. Februar 2022 um 22:58:12 UTC+1:
> On Wednesday, February 9, 2022 at 3:55:57 PM UTC-5, Mostowski Collapse wrote:
> > He defines when we are allowed to write:
> >
> > f'(x) = L
> >
> > Where do you see a domain of f' declared?
> > What is its variable name in Terence Tao for the domain of f'?
> It is the subset of X where the limit in question exists. In a formal mathematical proof, you would have to name it. Otherwise you could not formally construct the required function f'. Maybe in philosophy class, but not in math.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, February 9, 2022 at 5:14:48 PM UTC-5, Mostowski Collapse wrote:
> 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'?
>

No, the limit in this case is a real number.
> Look at the limit, it has a parameter x0, so it maps
> x0 to L.

The function f' maps the limit points in X to the real numbers.

> Its one and the same function as f'. Where
> do you think they differ?

Here, the limits in question are real numbers, not functions.

Dan

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

Your function axiom will literally only state where:
- f is differentiable

It will not state where:
- f is not differentiable

So you get kind of a f' that is half in the shadow. Take the
function f(x) = tan(x). f'(x) is undefined for x = pi/2+n*pi.
Nothing prevents your idiotic function axiom that f' is never-

theless defined on x = pi/2 + n*pi, since your idiotic
function axiom would only give:

ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => f'(x) = Lim(x)]

Now take this function:

g(x) = tan'(x) if x=\=pi/2 + n*pi for some n e N otherwise 0.

It will also satisfy:

ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => g(x) = Lim(x)]

Your function axiom is the most idiotic
idea that has ever surfaced the earth. Not
suitable for anything calculus.

Mostowski Collapse schrieb:
> Your function axiom will literally only state where:
> - f is differentiable
>
> It will not state where:
> - f is not differentiable
>
> So you get kind of a f' that is half in the shadow. Take the
> function f(x) = tan(x). f'(x) is undefined  for x = pi/2+n*pi.
> Nothing prevents your idiotic function axiom that f' is never-
>
> theless defined on x = pi/2 + n*pi, since your idiotic
> function axiom would only give:
>
> ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => f'(x) = Lim(x)]
>
> Now take this function:
>
> g(x) = tan'(x) if x=\=pi/2 + n*pi for some n e N otherwise 0.
>
> It will also satisfy:
>
> ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => g(x) = Lim(x)]

The bottonline is that your revised
function axiom, that has now an EXIST(fun),
the EXIST(fun) is not a EXISTUNIQUE(fun).

Its just complete nonsense. The nonsense
is best explained for fun = f'. It
will only state the differentiable part of f,

and not the part that is not differentiable.
Hence it will not in any way capture f',
you does not constuct f', but a family

of functions which share the differentiable
part of f, but where f is not differentiable
gets lost. Unless you go back to Lim(x),

but f'(x) and Lim(x) are the same!!!!!!!

Mostowski Collapse schrieb:
> Your function axiom is the most idiotic
> idea that has ever surfaced the earth. Not
> suitable for anything calculus.
>
> Mostowski Collapse schrieb:
>> Your function axiom will literally only state where:
>> - f is differentiable
>>
>> It will not state where:
>> - f is not differentiable
>>
>> So you get kind of a f' that is half in the shadow. Take the
>> function f(x) = tan(x). f'(x) is undefined  for x = pi/2+n*pi.
>> Nothing prevents your idiotic function axiom that f' is never-
>>
>> theless defined on x = pi/2 + n*pi, since your idiotic
>> function axiom would only give:
>>
>> ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => f'(x) = Lim(x)]
>>
>> Now take this function:
>>
>> g(x) = tan'(x) if x=\=pi/2 + n*pi for some n e N otherwise 0.
>>
>> It will also satisfy:
>>
>> ALL(x):[x in R \ {x|x=pi/2 + n*pi, n e N} => g(x) = Lim(x)]
>

You cannot prove that f'(x) and Lim(x)
are the same. You cannot prove that f'
is undefined where Lim(x) doesn't converge.

Mostowski Collapse schrieb:
> The bottonline is that your revised
> function axiom, that has now an EXIST(fun),
> the EXIST(fun) is not a EXISTUNIQUE(fun).
>
> Its just complete nonsense. The nonsense
> is best explained for fun = f'. It
> will only state the differentiable part of f,
>
> and not the part that is not differentiable.
> Hence it will not in any way capture f',
> you does not constuct f', but a family
>
> of functions which share the differentiable
> part of f, but where f is not differentiable
> gets lost. Unless you go back to Lim(x),
>
> but f'(x) and Lim(x) are the same!!!!!!!

On Wednesday, February 9, 2022 at 5:31:39 PM UTC-5, Mostowski Collapse wrote:
> Your function axiom will literally only state where:
> - f is differentiable
>

The Function Axiom is used only to introduce the standard "f(x)" notation given a non-empty domain set, a non-empty codomain set and a graph set. If you are unfamiliar with this terminology, see https://en.wikipedia.org/wiki/Function_(mathematics)

For functions of one variable:

1. ALL(dom):ALL(cod):ALL(gra):[Set(dom) & EXIST(a1):a1 in dom
& Set(cod) & EXIST(a):a in cod & Set'(gra)

=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]

=> EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]
Function

where

dom = domain set
cod = codomain
gra = graph set
fun = function name (using "f(x)" notation)

Dan

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

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

them and didn't understand a bit of it:

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

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

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

Of course you need to have the corresponding set theory
in DC Proof first, to redo the proof in DC Proof. But you
don't have set theory in DC Proof. This axiom is missing:

This axiom was introduced by Ernst Zermelo.
https://en.wikipedia.org/wiki/Axiom_of_union

It allows to define a function operator U : V -> V. With this
function operator, which is eliminable, you can
do the Firtz definions. These two lemmas help

proving my theorem:

Lemma 1: Empty Lemma: U {} = {}

Lemma 2: Singleton Lemma : U {x} = x

Maybe start proving these first in DC Proof, and then
wark your way to f(a), and finally obtain the disputed
theorem, also in DC Proof, when Set(f) and f(a) is

the Fritz application:

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

But you need true sets like in set theory. Not your
cartesian baby washed sets Set, Set', Set'' which are
kind of ZFCU, sets with urelements, but without

the Axiom of Union and a lot of other axioms missing.

Mostowski Collapse schrieb am Donnerstag, 28. April 2022 um 09:49:58 UTC+2:
> The Fritz definitions are here, which allow you
> to prove the disputed theorem that I gave. I
> am 100% convinced Dan-O-Matik always skipped
>
> them and didn't understand a bit of it:
>
> Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:
> > img(f) := {y e UUf : Ex(<x, y> e f)}
> > f(x) := U{y e UUf : <x, y> e f} "the value of f at x"
> https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ
>
> With these definitions, you don't need axioms
> for them you could also expand them, you can
> easily prove in FOL + ZFC:
>
> ALL(f):EXIST(y):ALL(a):[f(a) e y]

On Thursday, April 28, 2022 at 3:49:58 AM UTC-4, Mostowski Collapse wrote:
> The Fritz definitions are here, which allow you
> to prove the disputed theorem that I gave. I
> am 100% convinced Dan-O-Matik always skipped
>
> them and didn't understand a bit of it:
>
> Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 05:34:26 UTC+2:
> > img(f) := {y e UUf : Ex(<x, y> e f)}
> > f(x) := U{y e UUf : <x, y> e f} "the value of f at x"
> https://groups.google.com/g/sci.logic/c/ciw2EB2-4LE/m/3AYJ0sOTBwAJ
>
> With these definitions, you don't need axioms
> for them you could also expand them, you can
> easily prove in FOL + ZFC:
>
> ALL(f):EXIST(y):ALL(a):[f(a) e y]

I guess wonky results like this are part of the reason so-called "mathematical" logic is not a required course in many if not all university pure math programs (e.g. at MIT). I think most mathematicians would wondering if this wasn't a typo. They would be wondering what f and y are. Maybe f s some kind of function operator? If so, what is its domain? Puzzling.

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, April 28, 2022 at 10:49:16 PM UTC+2, Dan Christensen wrote:

> I guess wonky results like this are part of the reason so-called "mathematical" logic is <bla>

Dan, you are an idiotic crank. Please, shut up!

I think we could go with the answer by Asaf Karagila for
some issue we have. Asaf Karagila introduces some new
terminology we might find useful:

"Surjectivity is a relationship between a function and a
set. It is an extrinsic property of a function, when the
function is defined as a set of ordered pairs. Not an
intrinsic one like injectivity is."
https://math.stackexchange.com/a/4438437/1002973

I think he has put the Bourbaki idea f = <F,X,Y> aside,
and talks set theory, when he writes the above. Since in
Bourbaki we have Y is intrinsic and not extrinsic:

Y = π3(f) /* third projection from the triple <F,X,Y> */

We might also use the term intrinsic and extrinsic
to point out a lot of problems in Dan-O-Matiks treatment
so far, for example in this here:

ALL(a):[x e dom => f(a) e cod]

Two extrinsic properties dom and cod are used. That
dom is extrinsic is the more annoying thing, because
dom is intrinsic in set theory:

dom(f) := { x | EXIST(y):[(x,y) e f]

Depending on the pairing function we can show that
dom(f) exists as a set when f is a set already in Z
or we might need ZF. Similar in set theory we can prove:

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

Fritz Feldhase schrieb am Freitag, 29. April 2022 um 00:09:23 UTC+2:
> On Thursday, April 28, 2022 at 10:49:16 PM UTC+2, Dan Christensen wrote:
>
> > I guess wonky results like this are part of the reason so-called "mathematical" logic is <bla>
>
> Dan, you are an idiotic crank. Please, shut up!

sci.logic
Datenschutz
•
Nutzungsbedingungen
1 von 38914
DC Proof is the biggest teaching mistake
457 Aufrufe
Abonnieren
Profilbild von Mostowski Collapse
Mostowski Collapse
22.11.2021, 11:38:04
That an empty universe of discourse is allowed has recently become a hiding space for being lazy.
Profilbild von Dan Christensen
Dan Christensen
22.11.2021, 14:15:04
On Monday, November 22, 2021 at 5:38:04 AM UTC-5, Mostowski Collapse wrote: > That an empty
Profilbild von Mostowski Collapse
Mostowski Collapse
22.11.2021, 17:33:54
Shouldn't be provable in a logic with a possibly empty domain of discourse. Because any statement
Profilbild von Dan Christensen
Dan Christensen
22.11.2021, 21:16:13
On Monday, November 22, 2021 at 11:33:54 AM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Kip Foh
Kip Foh
23.11.2021, 01:36:40
Dan Christensen wrote: >> So how should it be possible to prove some EXIST(a):A(a) sentence
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 01:45:07
Why would you even be interested in proving this? > 2) EXIST(f):[Dedekind(f) => EXIST(w):Peano(
Profilbild von Dan Christensen
Dan Christensen
23.11.2021, 03:17:05
On Monday, November 22, 2021 at 7:45:07 PM UTC-5, Mostowski Collapse wrote: > Why would you even
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 08:39:59
Mathematics proves things like, using some foundational axioms. Thats standard routine: 3) EXIST(f):
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 08:50:16
For example when constructing the reals, its standard to then prove: 1) EXIST(x):[xe R & x^2 = 2]
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 09:01:08
When constructing the reals bottom up, you will likely need countable infinite sequences, and to show
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 09:10:24
If you don't have sqrt(2) as a real number object, you might have it as a class. But you refuse
Die Nachricht wurde gelöscht
Profilbild von Dan Christensen
Dan Christensen
23.11.2021, 18:30:57
> Dan Christensen schrieb am Dienstag, 23. November 2021 um 03:17:05 UTC+1: > > On Monday,
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 19:39:56
Nope you cannot introduce this as an axiom. It would consume the name f. Thats the whole point of
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 19:46:05
And this here is not FOL, when you use this here as an axiom: EXIST(x):EXIST(f):[Set(x) & ALL(a):
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 19:52:34
FOL = First Order Logic A function symbols is a second order logic object.. If U is the universe of
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 20:00:23
And this is buggy nonsense, it refers to x, but when you have an axiom EXIST(x):... how can you refer
Profilbild von Dan Christensen
Dan Christensen
23.11.2021, 21:18:06
On Tuesday, November 23, 2021 at 1:39:56 PM UTC-5, Mostowski Collapse wrote: > > The first line
Profilbild von Mostowski Collapse
Mostowski Collapse
23.11.2021, 22:54:45
Why do you talk nonsense all day? Its only equivalent when you have the axiom of regularity, or
Profilbild von Dan Christensen
Dan Christensen
24.11.2021, 01:27:13
On Tuesday, November 23, 2021 at 4:54:45 PM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
24.11.2021, 01:35:31
You continue talking nonsense as usual. Dan Christensen schrieb am Mittwoch, 24. November 2021 um 01:
Profilbild von Fritz Feldhase
Fritz Feldhase
24.11.2021, 05:49:56
On Tuesday, November 23, 2021 at 6:30:57 PM UTC+1, Dan Christensen wrote: > Again, I proved: &
Profilbild von Dan Christensen
Dan Christensen
24.11.2021, 05:58:08
On Tuesday, November 23, 2021 at 11:49:56 PM UTC-5, Fritz Feldhase wrote: > On Tuesday, November
Profilbild von Mostowski Collapse
Mostowski Collapse
24.11.2021, 15:16:53
Dan-O-Matik was talking nonsense: > And while Dedekind infinite sets are often mentioned in math
Profilbild von Mostowski Collapse
Mostowski Collapse
24.11.2021, 15:19:38
Additionally assuming f : x -> y for some x,y is not required to prove it in FOL+ZF. It would be
Profilbild von Mostowski Collapse
Mostowski Collapse
24.11.2021, 15:36:03
I am not suggesting Borel determinancy as an exercise: “Skolem needed a snack, so he ate enough for
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 16:59:15
Can we buy these double chimpazee copper bracelets already on Amazon? Here is your fallacy explained.
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 17:07:44
Even a blind mole can show both claims: > /* provable */ > F is hyperbola => ALL(x):[x≠0 Profilbild von Dan Christensen
Dan Christensen
05.12.2021, 17:17:24
On Sunday, December 5, 2021 at 10:59:15 AM UTC-5, Mostowski Collapse wrote: > Can we buy these
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 17:21:52
Corr.: Need to fix my blind mole proof, serial shouldn't be there. Don't know how much is
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 17:43:21
Ok here is a corrected proof, now saying for the reciprocal hyperbola, that the reciprocal hyperbola
Profilbild von FredJeffries
FredJeffries
05.12.2021, 17:54:12
On Sunday, December 5, 2021 at 8:17:24 AM UTC-8, Dan Christensen wrote: > On Sunday, December 5,
Profilbild von Dan Christensen
Dan Christensen
05.12.2021, 18:51:40
On Sunday, December 5, 2021 at 11:54:12 AM UTC-5, FredJeffries wrote: > On Sunday, December 5,
Profilbild von Dan Christensen
Dan Christensen
05.12.2021, 19:18:18
On Sunday, December 5, 2021 at 11:43:21 AM UTC-5, Mostowski Collapse wrote: > Ok here is a
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 19:50:19
Why would somebody try to prove that? When its not provable? It is easy to show that it has a counter
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 19:53:52
On the other hand one can prove: F is the reciprocal hyperbola => ~F(0,1) Here is the rather
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 20:13:43
Maybe you cannot cope with the mental disonnance between you double chimpanzee nonsense and standard
Profilbild von Dan Christensen
Dan Christensen
05.12.2021, 22:10:40
On Sunday, December 5, 2021 at 1:50:19 PM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 22:39:03
I am already telling you for the 1000-th times: hyperbola: f(0)≠1 provable double chimpanzee: f(0)≠1
Profilbild von Dan Christensen
Dan Christensen
05.12.2021, 22:56:40
On Sunday, December 5, 2021 at 4:39:03 PM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 23:05:54
Not in the hyperbola, in the f(0)≠1 provable Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um
Profilbild von Mostowski Collapse
Mostowski Collapse
05.12.2021, 23:07:39
Or more precisly, when: ALL(a):ALL(b):(F(a,b) <=> a*b=1) Then ~F(0,1). F(x)=y is the reciprocal
Profilbild von FredJeffries
FredJeffries
06.12.2021, 17:46:22
On Sunday, December 5, 2021 at 9:51:40 AM UTC-8, Dan Christensen wrote: > On Sunday, December 5,
Profilbild von Mostowski Collapse
Mostowski Collapse
10.12.2021, 19:36:08
Now this is like fukushima. I guess Dan-O-Matiks brain is now melting. We finally found it: ∀x(Px →
Profilbild von Mostowski Collapse
Mostowski Collapse
10.12.2021, 19:40:54
Actually learning 3 languages would be helpful: - FOL function symbol - class-like functions - set-
Profilbild von Mostowski Collapse
Mostowski Collapse
10.12.2021, 19:46:51
But there is cure, Dan-O-Matik could exercise and get fluent in all 3 languages by this little
Profilbild von Mostowski Collapse
Mostowski Collapse
12.12.2021, 10:47:50
Unfortunately Dan-O-Matik is only genuinely stupid: Two things are infinite: the universe and human
Profilbild von Mostowski Collapse
Mostowski Collapse
12.12.2021, 10:49:15
For example JavaScript implements undefined ⊥: Legts get back to the 10 booleans array problem. Just
Profilbild von Mostowski Collapse
Mostowski Collapse
12.12.2021, 10:53:21
Corr.: The WELL DEFINED issue arises when for example A={0} and B={0}, we then want from def(h) <Profilbild von Mostowski Collapse
Mostowski Collapse
13.12.2021, 22:26:00
How would one formulate in DC Proof, which is supposed to be the tool for mathematics textbooks, the
Profilbild von Mostowski Collapse
Mostowski Collapse
13.12.2021, 23:12:35
But Fefi was sloppy, when defining his Impredicative Theory of Operations and Classes (IOC), at least
Profilbild von Dan Christensen
Dan Christensen
14.12.2021, 03:54:02
On Monday, December 13, 2021 at 4:26:00 PM UTC-5, Mostowski Collapse wrote: > How would one
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 08:50:01
Thats not the correct approach in logic. Since Peano, we find something else: "Function
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 08:54:49
So only ALL(a):[aex => f(x) eb] , the Donnie Darko approach, like dark numbers in WM, is just WM
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 10:02:05
The only new development in logic might be these partial function logics, where we dont need f'x
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 10:07:07
Then there is a whole field where the underlying logic is changed, and where the underlying logic is
Profilbild von Dan Christensen
Dan Christensen
14.12.2021, 18:08:36
See my reply just now to your identical posting at sci.math Dan On Tuesday, December 14, 2021 at 2:50
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 19:34:41
Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree with Terence Tao. When you use a
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 19:43:49
With the metamath approach you can prove EXISTUNIQUE when the undefined marker is not in the codomain
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 19:48:28
So maybe what Fefi (Solom Feferman) explains is the more cleaner approach. You don't have to
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 20:49:27
The deeper problem is not Terrence Tao versus Dan-O-Matik versus metamath. In all 3 approaches this
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 20:55:33
It prevents EXISTUNIQUE because you can find (f1,c1) and (f2, c2), where f1≠f2 and: ALL(b):[b in c1 Profilbild von Dan Christensen
Dan Christensen
14.12.2021, 22:43:06
Set my reply just now to your identical posting as sci.math. Dan On Tuesday, December 14, 2021 at 2:
Profilbild von Mostowski Collapse
Mostowski Collapse
14.12.2021, 22:48:49
You used this EXISTUNIQUE(f,a): EXISTUNIQUE(f,a):A(f) <=> EXIST(h):A(h) & ALL(f):ALL(g):[A(
Profilbild von Mostowski Collapse
Mostowski Collapse
18.12.2021, 14:20:21
I dont think DC proof correctly associates functions and function graphs. You can also try Terence
Profilbild von Mostowski Collapse
Mostowski Collapse
18.12.2021, 14:27:35
Or asked differently how many decrement functions are there in Peano arithmetic? Can you prove:
Profilbild von Mostowski Collapse
Mostowski Collapse
24.12.2021, 10:27:34
What is easier to use, DC proof or ZFC? DC proof claims that certain things are given: > ALL(a):[a
Profilbild von Mostowski Collapse
Mostowski Collapse
24.12.2021, 10:41:12
With ZFC I only need to do the following: 1) let g = { (y, x) | (x, y) in f}, show it is a set 2)
Profilbild von Dan Christensen
Dan Christensen
24.12.2021, 17:24:47
See my reply just now to your identical postings at sci.math Dan On Friday, December 24, 2021 at 4:27
Profilbild von Mostowski Collapse
Mostowski Collapse
24.12.2021, 23:52:42
You are changing topic. I dont mind if you need Set(_) as well in DC poop. The question is rather can
Profilbild von Mostowski Collapse
Mostowski Collapse
26.12.2021, 11:06:23
So you cannot show existence of g? Hiding behind some absurd claims the encoding of functions as set
Profilbild von Mostowski Collapse
Mostowski Collapse
26.12.2021, 18:11:58
Can you prove your ExistenceOfInverse without using bizzar sets, like this here: Define: f' (as
Profilbild von Dan Christensen
Dan Christensen
27.12.2021, 04:07:11
On Sunday, December 26, 2021 at 5:06:23 AM UTC-5, Mostowski Collapse wrote: > So you cannot show
Profilbild von Mostowski Collapse
Mostowski Collapse
01.01.2022, 13:00:49
Ha Ha, Dan-O-Matik is quite desperate, he now denies valid proofs in mathematics: Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
02.01.2022, 20:19:53
Can this be proved in DC Proof? ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] Here is a LK calculus
Profilbild von Dan Christensen
Dan Christensen
03.01.2022, 04:01:38
See my reply to your identical posting at sci.math. Dan On Sunday, January 2, 2022 at 2:19:53 PM UTC-
Profilbild von Mostowski Collapse
Mostowski Collapse
03.01.2022, 13:27:59
Dan-O-Matik fights the evils of darkness: > In mathematics, it can't just be lurking unseen in
Profilbild von Mostowski Collapse
Mostowski Collapse
03.01.2022, 13:48:10
From ALL(a):[a in u => a in u & f(a) in u] it also follows: ALL(a):[a in u => f(a) in u]
Profilbild von Mostowski Collapse
Mostowski Collapse
03.01.2022, 14:11:17
I dont know how to fix your DC Puff and do what you want to do. Some free logics dont touch (Refl):
Profilbild von Dan Christensen
Dan Christensen
03.01.2022, 15:03:53
See my reply just now to your identical posting at sci.math. Dan On Monday, January 3, 2022 at 7:27:
Profilbild von Mostowski Collapse
Mostowski Collapse
03.01.2022, 17:25:20
You are changing topic, are you hunted by some shadows, Dr. Frankenstein? This here shouldn't be
Profilbild von Mostowski Collapse
Mostowski Collapse
03.01.2022, 23:55:46
So DC Proof has something like Emperor penguins from antarctica as functions, with the exotic USpec.
Profilbild von Dan Christensen
Dan Christensen
04.01.2022, 06:54:50
See my reply just now to a nearly identical posting at sci.math. Dan On Monday, January 3, 2022 at 5:
Die Nachricht wurde gelöscht
Profilbild von Mostowski Collapse
Mostowski Collapse
04.01.2022, 10:29:43
DC Proof is subject to "Fake it till you make it". You claim: Dan Christensen schrieb am
Profilbild von Mostowski Collapse
Mostowski Collapse
05.01.2022, 22:33:07
Here is a quizz, which collections are in some bijection? 1) { f | f : Q -> R }, where R the real
Profilbild von Mostowski Collapse
Mostowski Collapse
06.01.2022, 06:01:08
You find your beloved CBS theorem, together with the correct reading of function spaces, namely set
Profilbild von Mostowski Collapse
Mostowski Collapse
06.01.2022, 07:00:53
Also stop talking utter nonsense like: > Nothing there to support your claim that we can make
Profilbild von Mostowski Collapse
Mostowski Collapse
06.01.2022, 07:36:55
How flat chested is DC Proof? LoL It doesn't have a power set axiom? These two sets are provably
Profilbild von Mostowski Collapse
Mostowski Collapse
08.01.2022, 18:22:21
Warning: I am looking at the direction -->, the old topic, and not at the direction <--, the
Profilbild von Mostowski Collapse
Mostowski Collapse
08.01.2022, 18:23:22
Injectivity can now be examined, since only now by ALL(a):[g'(a)=g(a)] we have a mapping from
Profilbild von Mostowski Collapse
Mostowski Collapse
09.01.2022, 00:06:00
Actually this is a nice logic exercise, show that there is no bijection? At least in the finite case,
Profilbild von Mostowski Collapse
Mostowski Collapse
09.01.2022, 00:10:08
Check out for yourself: "Given two sets S and T, the set of all functions from T to S is denoted
Profilbild von Mostowski Collapse
Mostowski Collapse
10.01.2022, 23:08:41
Its very unclear why DC Proof even needs a Function Axiom? Litterally translating Terrence Tao, he
Profilbild von Mostowski Collapse
Mostowski Collapse
10.01.2022, 23:10:51
We can also do it Gödel style, follows also, proving seriality and functionality without the codomain
Profilbild von Dan Christensen
Dan Christensen
11.01.2022, 04:39:34
See my reply just now to your identical posting at sci.math. Dan On Monday, January 10, 2022 at 5:08:
Profilbild von Mostowski Collapse
Mostowski Collapse
12.01.2022, 23:28:55
As usual you are talking nonsense and even contradicting your own DC poop tool. Can you prove the
Profilbild von Mostowski Collapse
Mostowski Collapse
12.01.2022, 23:30:30
So stop talking nonsense about some text book paranoia. Here is the axiom your are presenting for
Profilbild von Dan Christensen
Dan Christensen
13.01.2022, 03:28:26
See my reply just now to your identical posting at sci.math On Wednesday, January 12, 2022 at 5:30:30
Profilbild von Mostowski Collapse
Mostowski Collapse
13.01.2022, 21:29:10
Fraenkel did nothing. The AOI is found in a paper by Zermelo. Its an axiom of the form: EXIST(S): ...
Profilbild von Mostowski Collapse
Mostowski Collapse
13.01.2022, 21:46:04
In FOL the schema works: (∃fDf ∧ ∀f(Df → Pc(f))) → ∃nPn is valid. https://www.umsu.de/trees/#~7fDf~1~
Profilbild von Mostowski Collapse
Mostowski Collapse
15.01.2022, 00:10:03
Of course Peano axioms have an encyclopedia entry, but its not anymore practiced. How do you now
Profilbild von Dan Christensen
Dan Christensen
15.01.2022, 05:21:05
See my reply just now to your identical posting at sci.math. Dan On Friday, January 14, 2022 at 6:10:
Profilbild von Mostowski Collapse
Mostowski Collapse
16.01.2022, 21:11:55
WHATS WRONG WITH YOU??????????????? Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47
Profilbild von Dan Christensen
Dan Christensen
17.01.2022, 02:19:29
On Sunday, January 16, 2022 at 3:11:55 PM UTC-5, Mostowski Collapse wrote: > WHATS WRONG WITH YOU?
Profilbild von Mostowski Collapse
Mostowski Collapse
17.01.2022, 02:44:15
I nowhere said I would only use set theory of DC Proof. DC Proof refers to the full package. If I can
Profilbild von Mostowski Collapse
Mostowski Collapse
19.01.2022, 18:13:46
If you insist, that I should not use Peano with your Set Theory!! How should I do that? I would like
Profilbild von Dan Christensen
Dan Christensen
19.01.2022, 23:18:16
On Wednesday, January 19, 2022 at 12:13:46 PM UTC-5, Mostowski Collapse wrote: > If you insist,
Profilbild von Mostowski Collapse
Mostowski Collapse
20.01.2022, 19:03:05
Q: How do you use DC poop to prove Landau's: ∀x∀y(x + y = y + x) A: Not at all, it doesn't
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 15:38:05
On Thursday, January 20, 2022 at 1:03:05 PM UTC-5, Mostowski Collapse wrote: > Q: How do you use
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 17:32:39
I don't think you are doing the same. Why does it take 252 steps? I can do it in simple 60 steps.
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 17:37:24
STUDENTS BEWARE: Unnatural DC Proof, totally not modular nonsense proofs, only an alien species can
Die Nachricht wurde gelöscht
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 17:56:45
Ok, thats the correct timing I get. Will post an internet link later: % Wall 1 ms, gc 0 ms, 108000
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 18:25:16
On Friday, January 21, 2022 at 11:32:39 AM UTC-5, Mostowski Collapse wrote: > I don't think
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 18:34:40
WHATS WRONG WITH YOU???? Dan-O-Matik asked: > How do you express Peano's Axioms? Well like
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 18:38:53
Here is a transliteration of the screenshot from Landau: Theorem 4, and at the same time Definition 1
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 18:47:12
Theorem 4 would be: ∀x ∀y ∃z (x + y = z) ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t) But this
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 18:51:53
On Friday, January 21, 2022 at 12:34:40 PM UTC-5, Mostowski Collapse wrote: > WHATS WRONG WITH YOU
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 18:58:50
Not interested in xe N, and a >200 step proof for commutativity. What you post below is not the
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 18:59:59
On Friday, January 21, 2022 at 12:38:53 PM UTC-5, Mostowski Collapse wrote: > Here is a
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 19:05:17
Its rather the other way around. You proved too much. Please read Landau carefully. He only said:
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 19:16:25
On Friday, January 21, 2022 at 12:58:50 PM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 19:17:49
If you want to interpret Landaus "assign" differently, in the sense of "by finite
Profilbild von Dan Christensen
Dan Christensen
21.01.2022, 19:29:21
On Friday, January 21, 2022 at 1:05:17 PM UTC-5, Mostowski Collapse wrote: > Dan Christensen
Profilbild von Mostowski Collapse
Mostowski Collapse
21.01.2022, 19:31:23
The problem is, math stackexchange is not the right place to learn anything mathematics or anything
Profilbild von Mostowski Collapse
Mostowski Collapse
23.01.2022, 23:19:01
So how meaningful is Dan-O-Matiks function space. We can show: ye S f : S -> {y} Dan-O-Matik style
Profilbild von Mostowski Collapse
Mostowski Collapse
28.01.2022, 18:24:15
Ha Ha, the domain of discourse and what quantifiers do in logic, the greatest miracle for Dan-O-Matik
Profilbild von Mostowski Collapse
Mostowski Collapse
28.01.2022, 21:25:56
The grandmother is very desperate. The little brat does not only not understand quantifiers and the
Profilbild von Mostowski Collapse
Mostowski Collapse
28.01.2022, 22:33:51
The grandmother is considering to give the grandson free for adoption. He is useless in the house,
Profilbild von Mostowski Collapse
Mostowski Collapse
29.01.2022, 00:39:58
Grandmother is a little angry with grandson. Grandson thinks he could just sprinkle some inference
Profilbild von Mostowski Collapse
Mostowski Collapse
04.02.2022, 05:06:10
If I take Dan-O-Matiks advice: > "Perhaps you didn't know, but two functions f and f'
Profilbild von Dan Christensen
Dan Christensen
04.02.2022, 17:05:29
On Thursday, February 3, 2022 at 11:06:10 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote: > If
Profilbild von Mostowski Collapse
Mostowski Collapse
04.02.2022, 18:22:41
The standard same-ness is: f ≈ g :<=> ∀x(f(x)=g(x)) You can then prove, for example in tree
Profilbild von Dan Christensen
Dan Christensen
04.02.2022, 20:05:25
On Friday, February 4, 2022 at 12:22:41 PM UTC-5, Mostowski Collapse wrote: > The standard same-
Profilbild von Mostowski Collapse
Mostowski Collapse
04.02.2022, 20:50:05
Well the domain of a function is easy: dom(f) = { x | ∃y (x,y) ef } You then have: f = g => dom(f)
Profilbild von Dan Christensen
Dan Christensen
04.02.2022, 22:33:39
On Friday, February 4, 2022 at 2:50:05 PM UTC-5, Mostowski Collapse wrote: > Don't you have
Profilbild von Mostowski Collapse
Mostowski Collapse
04.02.2022, 23:21:52
Dan-O-Matik halucinated: > for all x in X, we have f(x)=g(x) You cannot prove: f ≈ g => dom(f)
Profilbild von Mostowski Collapse
Mostowski Collapse
07.02.2022, 11:59:21
Ok, here is a high school exercise: f : R \ {0} -> R, identity function except for x=0 where
Profilbild von Dan Christensen
Dan Christensen
07.02.2022, 17:53:54
See my reply today to your identical posting at sci.math Dan On Monday, February 7, 2022 at 5:59:21
Profilbild von Mostowski Collapse
Mostowski Collapse
07.02.2022, 21:47:13
You see, your result is nonsense: ALL(a):[a in non0 => g(f(a))=1] Thats a strange identity
Profilbild von Mostowski Collapse
Mostowski Collapse
07.02.2022, 22:27:54
This theorem is not provable in DC poop: dom(goh) = h^(-1)[dom(g)] Because DC poop refuses to define
Profilbild von Dan Christensen
Dan Christensen
08.02.2022, 01:33:46
On Monday, February 7, 2022 at 3:47:13 PM UTC-5, Mostowski Collapse wrote: > You see, your result
Profilbild von Mostowski Collapse
Mostowski Collapse
08.02.2022, 12:40:52
One more nonsense: > 32. ALL(a):[a in non01 => g(f(a))=a] Conclusion, 9 Try this here: 6. ALL(a
Profilbild von Mostowski Collapse
Mostowski Collapse
09.02.2022, 19:50:41
WHATS WRONG WITH YOU????? Where do you see the domain of f' given for example for the problem f :
Profilbild von Mostowski Collapse
Mostowski Collapse
09.02.2022, 21:47:09
Just read Terence Tao. From f you construct a function: Step 1: g(x,h) = (f(x+h) - f(x)) / h And from
Profilbild von Dan Christensen
Dan Christensen
10.02.2022, 04:23:43
See my reply earlier today to your identical posting at sci.math Dan On Wednesday, February 9, 2022
Profilbild von Mostowski Collapse
Mostowski Collapse
28.04.2022, 09:47:57 (gestern)
The Fritz definitions are here, which allow you to prove the disputed theorem that I gave. I am 100%
Profilbild von Mostowski Collapse
Mostowski Collapse
28.04.2022, 09:56:57 (gestern)
Of course you need to have the corresponding set theory in DC Proof first, to redo the proof in DC
Profilbild von Dan Christensen
Dan Christensen
28.04.2022, 22:58:59 (vor 17 Stunden)
See my reply just now to your identical posting at sci.math. Dan On Thursday, April 28, 2022 at 3:47:
Profilbild von Mostowski Collapse
Mostowski Collapse
15:46 (vor 16 Minuten)
I think we could go with the answer by Asaf Karagila for some issue we have.. Asaf Karagila introduces
Profilbild von Mostowski Collapse
Mostowski Collapse
ungelesen,
16:02 (jetzt)
an
Unfortunately Asaf Karagila is not a very expanded
answer. When he writes then "ask whether or not the range is
equal to the its codomain", we are a bit left with the

Unfortunately Asaf Karagila is not a very expanded
answer. When he writes then "ask whether or not the range is
equal to the its codomain", we are a bit left with the

question what is range? And is it extrinsic or
intrinsic? And what about the codomain, where do
I find it? Anyway proving this one could answer

all questions:

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

P.S.: Also Dan Christensen uses a faux definition in
his question. Since wikipedia explicitly states that cod
is not what Dan Christensen writes: "The codomain set

is just the set of all its 2nd co-ordinates (ordinates)."
So there is a category in Dan Christensens question
since by co-domain we understand:

It is the set Y in the notation f: X → Y.

So maybe we have already an answer, the codomain
is extrinsic, and the range is intrinsic?

LoL

Mostowski Collapse schrieb am Freitag, 29. April 2022 um 15:45:00 UTC+2:
> I think we could go with the answer by Asaf Karagila for
> some issue we have. Asaf Karagila introduces some new
> terminology we might find useful:
>
> "Surjectivity is a relationship between a function and a
> set. It is an extrinsic property of a function, when the
> function is defined as a set of ordered pairs. Not an
> intrinsic one like injectivity is."
> https://math.stackexchange.com/a/4438437/1002973
>
> I think he has put the Bourbaki idea f = <F,X,Y> aside,
> and talks set theory, when he writes the above. Since in
> Bourbaki we have Y is intrinsic and not extrinsic:
>
> Y = π3(f) /* third projection from the triple <F,X,Y> */
>
> We might also use the term intrinsic and extrinsic
> to point out a lot of problems in Dan-O-Matiks treatment
> so far, for example in this here:
>
> ALL(a):[x e dom => f(a) e cod]
>
> Two extrinsic properties dom and cod are used. That
> dom is extrinsic is the more annoying thing, because
> dom is intrinsic in set theory:
>
> dom(f) := { x | EXIST(y):[(x,y) e f]
>
> Depending on the pairing function we can show that
> dom(f) exists as a set when f is a set already in Z
> or we might need ZF. Similar in set theory we can prove:
> ALL(f):EXIST(y):ALL(a):[f(a) e y]
> Fritz Feldhase schrieb am Freitag, 29. April 2022 um 00:09:23 UTC+2:
> > On Thursday, April 28, 2022 at 10:49:16 PM UTC+2, Dan Christensen wrote:
> >
> > > I guess wonky results like this are part of the reason so-called "mathematical" logic is <bla>
> >
> > Dan, you are an idiotic crank. Please, shut up!

So how did Dan Christensen crank it up? Play himself some tricks?
There is a grave category error (not from category theory, but from
use of terminology in the field) in the question by the OP.

Error 1: The OP claims:

The codomain set is just the set of all its 2nd co-ordinates (ordinates).

But wikipedia disagrees:

In mathematics, the codomain or set of destination of a function is
the set into which all of the output of the function is constrained to fall..
It is the set Y in the notation f: X → Y. https://en.wikipedia.org/wiki/Codomain

Also the question by the OP insinuates something that is not given.
Namely that range would have a common notion. I guess we would fare
better if we would use image instead range, to decrease the variation
points that might lead to confusion:

Error 2: The OP claims:

There is no distinction made between the codomain and what is
commonly called the range of a function.

But Wikipedia disagrees:

The term range is sometimes ambiguously used to refer to either the
codomain or image of a function. https://en.wikipedia.org/wiki/Codomain

Mostowski Collapse schrieb am Freitag, 29. April 2022 um 16:12:35 UTC+2:
> Unfortunately Asaf Karagila is not a very expanded
> answer. When he writes then "ask whether or not the range is
> equal to the its codomain", we are a bit left with the
>
> question what is range? And is it extrinsic or
> intrinsic? And what about the codomain, where do
> I find it? Anyway proving this one could answer
>
> all questions:
> ALL(f):EXIST(y):ALL(a):[f(a) e y]
> P.S.: Also Dan Christensen uses a faux definition in
> his question. Since wikipedia explicitly states that cod
> is not what Dan Christensen writes: "The codomain set
>
> is just the set of all its 2nd co-ordinates (ordinates)."
> So there is a category in Dan Christensens question
> since by co-domain we understand:
>
> It is the set Y in the notation f: X → Y.
>
> So maybe we have already an answer, the codomain
> is extrinsic, and the range is intrinsic?
>
> LoL
> Mostowski Collapse schrieb am Freitag, 29. April 2022 um 15:45:00 UTC+2:
> > I think we could go with the answer by Asaf Karagila for
> > some issue we have. Asaf Karagila introduces some new
> > terminology we might find useful:
> >
> > "Surjectivity is a relationship between a function and a
> > set. It is an extrinsic property of a function, when the
> > function is defined as a set of ordered pairs. Not an
> > intrinsic one like injectivity is."
> > https://math.stackexchange.com/a/4438437/1002973
> >
> > I think he has put the Bourbaki idea f = <F,X,Y> aside,
> > and talks set theory, when he writes the above. Since in
> > Bourbaki we have Y is intrinsic and not extrinsic:
> >
> > Y = π3(f) /* third projection from the triple <F,X,Y> */
> >
> > We might also use the term intrinsic and extrinsic
> > to point out a lot of problems in Dan-O-Matiks treatment
> > so far, for example in this here:
> >
> > ALL(a):[x e dom => f(a) e cod]
> >
> > Two extrinsic properties dom and cod are used. That
> > dom is extrinsic is the more annoying thing, because
> > dom is intrinsic in set theory:
> >
> > dom(f) := { x | EXIST(y):[(x,y) e f]
> >
> > Depending on the pairing function we can show that
> > dom(f) exists as a set when f is a set already in Z
> > or we might need ZF. Similar in set theory we can prove:
> > ALL(f):EXIST(y):ALL(a):[f(a) e y]
> > Fritz Feldhase schrieb am Freitag, 29. April 2022 um 00:09:23 UTC+2:
> > > On Thursday, April 28, 2022 at 10:49:16 PM UTC+2, Dan Christensen wrote:
> > >
> > > > I guess wonky results like this are part of the reason so-called "mathematical" logic is <bla>
> > >
> > > Dan, you are an idiotic crank. Please, shut up!

On Friday, April 29, 2022 at 10:15:41 AM UTC-4, Mostowski Collapse wrote:

> There is a grave category error (not from category theory, but from
> use of terminology in the field) in the question by the OP.
>
> Error 1: The OP claims:
> The codomain set is just the set of all its 2nd co-ordinates (ordinates).

That is true for your system with those dom (.) and cod(.) operators, Jan Burse. Your idea of a function is just a set of ordered pairs. Looks kind of silly now?

> But wikipedia disagrees:
>
> In mathematics, the codomain or set of destination of a function is
> the set into which all of the output of the function is constrained to fall.
> It is the set Y in the notation f: X → Y. https://en.wikipedia.org/wiki/Codomain
>
> Also the question by the OP insinuates something that is not given.
> Namely that range would have a common notion. I guess we would fare
> better if we would use image instead range, to decrease the variation
> points that might lead to confusion:
>
> Error 2: The OP claims:
>
> There is no distinction made between the codomain and what is
> commonly called the range of a function.
>

Again, that is true of YOUR system, Jan Burse.

> But Wikipedia disagrees:
>
> The term range is sometimes ambiguously used to refer to either the
> codomain or image of a function. https://en.wikipedia.org/wiki/Codomain
> Mostowski Collapse schrieb am Freitag, 29. April 2022 um 16:12:35 UTC+2:

Dan

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

I must say I had only an intuitive gut that range should be avoided. Also I don't
understand why José Carlos Santos, Xander Henderson and Arturo Magidin go
off the tangent. I have used the same clarification as here:

Domain, Co-Domain & Range of a Function
https://math.stackexchange.com/questions/59432/domain-co-domain-range-of-a-function

Do they also deny their own stack exchange bitrot now, only to persist in a trolling
act, is that their character? Anyway I am also used to rng() and not img(),
you find rng() here, I really recommend this booklet:

Basic Set Theory - Azriel Levy
6.9 Definition
range the class of the second components of the ordered pairs
https://www.amazon.de/Basic-Theory-Dover-Books-Mathematics/dp/0486420795

Dan Christensen schrieb am Freitag, 29. April 2022 um 17:25:53 UTC+2:
> On Friday, April 29, 2022 at 10:15:41 AM UTC-4, Mostowski Collapse wrote:
>
> > There is a grave category error (not from category theory, but from
> > use of terminology in the field) in the question by the OP.
> >
> > Error 1: The OP claims:
> > The codomain set is just the set of all its 2nd co-ordinates (ordinates).
> That is true for your system with those dom (.) and cod(.) operators, Jan Burse. Your idea of a function is just a set of ordered pairs. Looks kind of silly now?
> > But wikipedia disagrees:
> >
> > In mathematics, the codomain or set of destination of a function is
> > the set into which all of the output of the function is constrained to fall.
> > It is the set Y in the notation f: X → Y. https://en.wikipedia.org/wiki/Codomain
> >
> > Also the question by the OP insinuates something that is not given.
> > Namely that range would have a common notion. I guess we would fare
> > better if we would use image instead range, to decrease the variation
> > points that might lead to confusion:
> >
> > Error 2: The OP claims:
> >
> > There is no distinction made between the codomain and what is
> > commonly called the range of a function.
> >
> Again, that is true of YOUR system, Jan Burse.
> > But Wikipedia disagrees:
> >
> > The term range is sometimes ambiguously used to refer to either the
> > codomain or image of a function. https://en.wikipedia.org/wiki/Codomain
> > Mostowski Collapse schrieb am Freitag, 29. April 2022 um 16:12:35 UTC+2:
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

That Dan-O-Matik is more mentally impaired than WM,
that we have basically proof of "a fool with a tool, is still
a fool", is that after asking this question:

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

He can still not make a suitable definition of gra(a),
i.e. function application for a set-like function,
and then prove the following:

ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[gra(a) e y]]

I still speculate that DC Proof is some WW2 trophy,
and not something that Dan Christensen wrote himself.
Doesn't Set'(_) in DC Proof mean set of ordered pairs?

Maybe his Set' axioms are too weak, and he cannot
prove it. Possibly again a problem with this fallacy?

The french eat baguette
Therefore
Baquette eaters are french

So function spaces, as found in mathematics, are
still miles away, insurmountable obstacles?

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 14:54:11 UTC+2:
> That Dan-O-Matik is more mentally impaired than WM,
> that we have basically proof of "a fool with a tool, is still
> a fool", is that after asking this question:
>
> Are there non-surjective functions in ZFC theory?
> https://math.stackexchange.com/q/4438429/1002973
>
> He can still not make a suitable definition of gra(a),
> i.e. function application for a set-like function,
> and then prove the following:
>
> ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[gra(a) e y]]
>
> I still speculate that DC Proof is some WW2 trophy,
> and not something that Dan Christensen wrote himself.
> Doesn't Set'(_) in DC Proof mean set of ordered pairs?

On Saturday, April 30, 2022 at 8:54:11 AM UTC-4, Mostowski Collapse wrote:
> That Dan-O-Matik is more mentally impaired than WM,
> that we have basically proof of "a fool with a tool, is still
> a fool", is that after asking this question:
>
> Are there non-surjective functions in ZFC theory?
> https://math.stackexchange.com/q/4438429/1002973
>
> He can still not make a suitable definition of gra(a),
> i.e. function application for a set-like function,
> and then prove the following:
>
> ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[gra(a) e y]]
>

If I could prove that, it would be a serious bug in my program. It is nonsense.

Dan

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

Why, if gra is set of ordered pairs, then there is also a set
of elements of the second ordinate? Do you have a counter
example to this claim. You called this set codomain here:

Are there non-surjective functions in ZFC theory?
Your own words:
The codomain set is just the **set** of all its 2nd co-ordinates (ordinates).
https://math.stackexchange.com/q/4438429/1002973

But the more precise name is range. But this formula
doesnt give a name to this set, it only says EXIST(y) Set(y)
so its free from linguistic baggage. Do you still

ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[gra(a) e y]]

claim its not provable? Did you ask on MSE?

LoL

elDan Christensen schrieb am Samstag, 30. April 2022 um 15:24:45 UTC+2:
> On Saturday, April 30, 2022 at 8:54:11 AM UTC-4, Mostowski Collapse wrote:
> > That Dan-O-Matik is more mentally impaired than WM,
> > that we have basically proof of "a fool with a tool, is still
> > a fool", is that after asking this question:
> >
> > Are there non-surjective functions in ZFC theory?
> > https://math.stackexchange.com/q/4438429/1002973
> >
> > He can still not make a suitable definition of gra(a),
> > i.e. function application for a set-like function,
> > and then prove the following:
> >
> > ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[gra(a) e y]]
> >
> If I could prove that, it would be a serious bug in my program. It is nonsense.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com