Well the core question is why would one need this in
Number Theory? I asked this already a dozen time.
Why does one need your Function Axiom or a

Construction of add, why does one need an add based
on material implication, when Landau can do the
following without it?

Landau can do in FOL=:

∀x ∀y ∃!z (x + y = z)

Landau can do in FOL= with Set-Less Induction Schema:

∀x ∀y (x + y = y + x)

Also you don't show really existence of add, since you
assume Set Induction. But for example in ZFC Set Induction
can itself be shown to exist.

You don't make any sense with your pseudo existence
of add. It needs existence of induction. ZFC on the other
hand can prove induction.

You don't make any sense with your pseudo existence
of add, its not needed for ∀x ∀y ∃!z (x + y = z) and its
not needed for ∀x ∀y (x + y = y + x) .

So your add construction is:
a) False claim, it depens on Induction (unlike a ZFC construction)
b) Not motivated, we still don't know what it is used for,
neither Landau ∀x ∀y ∃!z (x + y = z) nor ∀x ∀y (x + y = y + x)
needs it.

Dan Christensen schrieb am Freitag, 21. Januar 2022 um 19:57:02 UTC+1:
> On Friday, January 21, 2022 at 1:19:17 PM UTC-5, Mostowski Collapse wrote:
> > Its rather the other way around. You proved too
> > much. Please read Landau carefully. He only said:
> >
> > "To every pair of numbers x, y, we may assign
> > exactly one way a natural number"
> >
> > This can be cast as:
> >
> > ∀x ∀y ∃!z (x + y = z)
> >
> > Which translates to:
> >
> > ∀x ∀y ∃z (x + y = z)
> > ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
> >
> The same is true of ANY binary function on a given set. You have A=B and A=C, therefore B=C. Nothing profound there. This is certainly no substitute for a formal proof of existence of the addition function on N, as I have given here:
>
> https://www.dcproof.com/ConstructAdditionNew.htm
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

In FOL all functions exist. The question would be differently
posed, namely are the Peano Axioms consistent. But
consistency of con(PA) cannot be shown.

Here PA denotes Peano Axioms without any x e N, are
the Axioms without x e N and with the Set-Less Induction
Schema consistent, resp. do they have a model.

On the other hand we have something like con(ZFC)
implies con(PA). With con(PA) and/or con(ZFC) we are in
the Waters of Gödel Incompletness Theorems.
Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 20:22:51 UTC+1:
> Well the core question is why would one need this in
> Number Theory? I asked this already a dozen time.
> Why does one need your Function Axiom or a
>
> Construction of add, why does one need an add based
> on material implication, when Landau can do the
> following without it?
>
> Landau can do in FOL=:
> ∀x ∀y ∃!z (x + y = z)
> Landau can do in FOL= with Set-Less Induction Schema:
>
> ∀x ∀y (x + y = y + x)
>
> Also you don't show really existence of add, since you
> assume Set Induction. But for example in ZFC Set Induction
> can itself be shown to exist.
>
> You don't make any sense with your pseudo existence
> of add. It needs existence of induction. ZFC on the other
> hand can prove induction.
>
> You don't make any sense with your pseudo existence
> of add, its not needed for ∀x ∀y ∃!z (x + y = z) and its
> not needed for ∀x ∀y (x + y = y + x) .
>
> So your add construction is:
> a) False claim, it depens on Induction (unlike a ZFC construction)
> b) Not motivated, we still don't know what it is used for,
> neither Landau ∀x ∀y ∃!z (x + y = z) nor ∀x ∀y (x + y = y + x)
> needs it.
> Dan Christensen schrieb am Freitag, 21. Januar 2022 um 19:57:02 UTC+1:
> > On Friday, January 21, 2022 at 1:19:17 PM UTC-5, Mostowski Collapse wrote:
> > > Its rather the other way around. You proved too
> > > much. Please read Landau carefully. He only said:
> > >
> > > "To every pair of numbers x, y, we may assign
> > > exactly one way a natural number"
> > >
> > > This can be cast as:
> > >
> > > ∀x ∀y ∃!z (x + y = z)
> > >
> > > Which translates to:
> > >
> > > ∀x ∀y ∃z (x + y = z)
> > > ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
> > >
> > The same is true of ANY binary function on a given set. You have A=B and A=C, therefore B=C. Nothing profound there. This is certainly no substitute for a formal proof of existence of the addition function on N, as I have given here:
> >
> > https://www.dcproof.com/ConstructAdditionNew.htm
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

P.S.: In FOL all function exists AND they are not the
empty function {}, i.e. empty domain, since the universe
of discourse is non-empty. So we can prove:

∃x∃yf(x)=y is valid.
https://www.umsu.de/trees/#~7x~7yf%28x%29=y

In FOL= all function versus a set of positive equality
equations do also exist. Equality is very forgiving,
for example we can prove:

0=1 → f(0)=f(1) is valid.
https://www.umsu.de/trees/#=%280,1%29~5f%280%29=f%281%29

That a set of positive equality equations is satisfiable
can be explained that in the worst case the equality
classes of the equations cover all elements of the

unverse of discourse, making the unverse of discourse
a "singleton", but then trivially the equations are satisfied.
The Peano Axioms are not that simple besides =, they have also ≠.

Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 20:48:13 UTC+1:
> In FOL all functions exist. The question would be differently
> posed, namely are the Peano Axioms consistent. But
> consistency of con(PA) cannot be shown.
>
> Here PA denotes Peano Axioms without any x e N, are
> the Axioms without x e N and with the Set-Less Induction
> Schema consistent, resp. do they have a model.
>
> On the other hand we have something like con(ZFC)
> implies con(PA). With con(PA) and/or con(ZFC) we are in
> the Waters of Gödel Incompletness Theorems.
> Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 20:22:51 UTC+1:
> > Well the core question is why would one need this in
> > Number Theory? I asked this already a dozen time.
> > Why does one need your Function Axiom or a
> >
> > Construction of add, why does one need an add based
> > on material implication, when Landau can do the
> > following without it?
> >
> > Landau can do in FOL=:
> > ∀x ∀y ∃!z (x + y = z)
> > Landau can do in FOL= with Set-Less Induction Schema:
> >
> > ∀x ∀y (x + y = y + x)
> >
> > Also you don't show really existence of add, since you
> > assume Set Induction. But for example in ZFC Set Induction
> > can itself be shown to exist.
> >
> > You don't make any sense with your pseudo existence
> > of add. It needs existence of induction. ZFC on the other
> > hand can prove induction.
> >
> > You don't make any sense with your pseudo existence
> > of add, its not needed for ∀x ∀y ∃!z (x + y = z) and its
> > not needed for ∀x ∀y (x + y = y + x) .
> >
> > So your add construction is:
> > a) False claim, it depens on Induction (unlike a ZFC construction)
> > b) Not motivated, we still don't know what it is used for,
> > neither Landau ∀x ∀y ∃!z (x + y = z) nor ∀x ∀y (x + y = y + x)
> > needs it.
> > Dan Christensen schrieb am Freitag, 21. Januar 2022 um 19:57:02 UTC+1:
> > > On Friday, January 21, 2022 at 1:19:17 PM UTC-5, Mostowski Collapse wrote:
> > > > Its rather the other way around. You proved too
> > > > much. Please read Landau carefully. He only said:
> > > >
> > > > "To every pair of numbers x, y, we may assign
> > > > exactly one way a natural number"
> > > >
> > > > This can be cast as:
> > > >
> > > > ∀x ∀y ∃!z (x + y = z)
> > > >
> > > > Which translates to:
> > > >
> > > > ∀x ∀y ∃z (x + y = z)
> > > > ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
> > > >
> > > The same is true of ANY binary function on a given set. You have A=B and A=C, therefore B=C. Nothing profound there. This is certainly no substitute for a formal proof of existence of the addition function on N, as I have given here:
> > >
> > > https://www.dcproof.com/ConstructAdditionNew.htm
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, January 21, 2022 at 2:22:51 PM UTC-5, Mostowski Collapse wrote:
> Well the core question is why would one need this in
> Number Theory? I asked this already a dozen time.
> Why does one need your Function Axiom or a
>

Why does one need ZFC or any formal systems? It's an important question. I'm truly surprised you have to ask. To get you started, you might have a look at https://en.wikipedia.org/wiki/Formal_system

> Construction of add, why does one need an add based
> on material implication, when Landau can do the
> following without it?
>

Why are you so fixated on material implication? I can only guess that you have never done many actual proofs. It's certainly nothing to get worked up about it. You might take a look at my blog posting on this topic at https://dcproof.wordpress.com/2017/12/28/if-pigs-could-fly/

Dan

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

Mostowski Collapse wrote:

> P.S.: In FOL all function exists AND they are not the empty function {},
> i.e. empty domain, since the universe of discourse is non-empty. So we
> can prove: ∃x∃yf(x)=y is valid.
> https://www.umsu.de/trees/#~7x~7yf%28x%29=y

you fool, the *public_servants*, you pay for, are calling themself
*elite*, you disgusting piece of shit. Claus schwab &co will penetrate
your stupid asses by force. It's on the agenda, for decades now. You
sci.math addicted don't even understand *elites*.

THEY Are Openly Calling Themselves 'THE ELITE' Now...Masks Are Off
https://www.bitchute.com/video/xc2fO_6o40A/

Mostowski Collapse wrote:

> P.S.: In FOL all function exists AND they are not the empty function {},
> i.e. empty domain, since the universe of discourse is non-empty. So we
> can prove: ∃x∃yf(x)=y is valid.
> https://www.umsu.de/trees/#~7x~7yf%28x%29=y

more details here. You should start *arresting_that_mazafaka_claus_schab*
&co *parasites* immediately.

Too Good To Be True - What is Going on
https://www.bitchute.com/video/CIbO5RxsuMT3/

So how meaningful is Dan-O-Matiks function space.
We can show:

y e S
f : S -> {y} Dan-O-Matik style.
∴ f : {y} -> {y}, Dan-O-Matik style.

(EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.
https://www.umsu.de/trees/#EyS~1~6a%28EaS~5f%28a%29=y]~5~6a%28a=y~5f%28a%29=y%29

But the later allows to extract:

y e S
f : S -> {y} Dan-O-Matik style.
∴ f(y) = y

(EyS ∧ ∀a(EaS → f(a)=y)) → f(y)=y is valid.
https://www.umsu.de/trees/#EyS~1~6a%28EaS~5f%28a%29=y]~5f%28y%29=y

Just like the f(z)=z here, LoL:
https://dcproof.com/FunctionSpaceSingletons.htm

Ha Ha, the domain of discourse and what quantifiers
do in logic, the greatest miracle for Dan-O-Matik.

Did he even write DC Proof on his own, or maybe
his wise grandmother wrote it for him, and now she gets

a lot migraine because his grandson doesn't have a clue.

Mostowski Collapse wrote:

> Ha Ha, the domain of discourse and what quantifiers do in logic, the
> greatest miracle for Dan-O-Matik.
> Did he even write DC Proof on his own, or maybe his wise grandmother wrote
> it for him, and now she gets a lot migraine because his grandson doesn't have a clue.

the bitch of Ursula addressed globalist claus schwab with "_dear_claus_"

EU watchdog accuses Ursula von der Leyen of 'maladministration' and orders
her to hand over secret texts she sent to Pfizer's CEO during efforts to
buy 1.8billion Covid jabs
https://www.dailymail.co.uk/news/article-10451919/EU-watchdog-orders-Ursula-von-der-Leyen-hand-secret-texts-sent-Pfizers-CEO.html

The grandmother is very desperate. The little brat
does not only not understand quantifiers and the

domain of discourse. He is also having troubles
with bi-conditional (<=>)/2 and these laws:

A => (B => A)
(A => B) & (~A => B) => B

LoL

Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 18:23:47 UTC+1:
> Ha Ha, the domain of discourse and what quantifiers
> do in logic, the greatest miracle for Dan-O-Matik.
>
> Did he even write DC Proof on his own, or maybe
> his wise grandmother wrote it for him, and now she gets
>
> a lot migraine because his grandson doesn't have a clue.

The grandmother is considering to give the grandson
free for adoption. He is useless in the house, and

consistent/inconsistent is not part of his vocabulary.
Ex Falso Quodlibet is also something new for him.
Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 21:25:28 UTC+1:
> The grandmother is very desperate. The little brat
> does not only not understand quantifiers and the
>
> domain of discourse. He is also having troubles
> with bi-conditional (<=>)/2 and these laws:
>
> A => (B => A)
> (A => B) & (~A => B) => B
>
> LoL
> Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 18:23:47 UTC+1:
> > Ha Ha, the domain of discourse and what quantifiers
> > do in logic, the greatest miracle for Dan-O-Matik.
> >
> > Did he even write DC Proof on his own, or maybe
> > his wise grandmother wrote it for him, and now she gets
> >
> > a lot migraine because his grandson doesn't have a clue.

Grandmother is a little angry with grandson.
Grandson thinks he could just sprinkle some

inference rules with additional nonsense
restrictions which are even not water proof.

Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 22:33:08 UTC+1:
> The grandmother is considering to give the grandson
> free for adoption. He is useless in the house, and
>
> consistent/inconsistent is not part of his vocabulary.
> Ex Falso Quodlibet is also something new for him.
> Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 21:25:28 UTC+1:
> > The grandmother is very desperate. The little brat
> > does not only not understand quantifiers and the
> >
> > domain of discourse. He is also having troubles
> > with bi-conditional (<=>)/2 and these laws:
> >
> > A => (B => A)
> > (A => B) & (~A => B) => B
> >
> > LoL
> > Mostowski Collapse schrieb am Freitag, 28. Januar 2022 um 18:23:47 UTC+1:
> > > Ha Ha, the domain of discourse and what quantifiers
> > > do in logic, the greatest miracle for Dan-O-Matik.
> > >
> > > Did he even write DC Proof on his own, or maybe
> > > his wise grandmother wrote it for him, and now she gets
> > >
> > > a lot migraine because his grandson doesn't have a clue.

If I take Dan-Matiks advice:

> "Perhaps you didn't know, but two functions f and f' with the same domain X
> and codomain Y are actually the SAME function if f(a)=f'(a) for all a in X. "
> See for example, lines 114-122 in my proof https://www.dcproof.com/ExistenceUniqueIdentityFunction.htm

I would define, what is proved in 114-122:

f ≈ f' :<=> ALL(a):[a e x => f(a) e y] &
ALL(a):[a e x => f'(a) e y]
=> ALL(a):[a e x => f(a)=f'(a)]

But this obviously doesn't work. If f has a different
doman and codomain as f', then we have f ≈ f' trivially
true because of the material main implication =>:

A B A => B
0 0 1
0 1 1
1 0 0
1 1 1

If ALL(a):[a e x => f(a) e y] and ALL(a):[a e x => f'(a) e y]
are not simultaneously satisfied, then material implicaton
is trivially true, as can be read off from the truth table,

thats just the case where A=0. So what is the Dan-O-Matik
definition of f ≈ f' exactly?

On Thursday, February 3, 2022 at 11:03:35 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> If I take Dan-Matiks advice:
>
> > "Perhaps you didn't know, but two functions f and f' with the same domain X
> > and codomain Y are actually the SAME function if f(a)=f'(a) for all a in X. "
> > See for example, lines 114-122 in my proof https://www.dcproof.com/ExistenceUniqueIdentityFunction.htm
>
> I would define, what is proved in 114-122:
>
> f ≈ f' :<=> ALL(a):[a e x => f(a) e y] &
> ALL(a):[a e x => f'(a) e y]
> => ALL(a):[a e x => f(a)=f'(a)]
>
> But this obviously doesn't work. If f has a different
> doman and codomain as f', then we have f ≈ f' trivially
> true because of the material main implication =>:
>

Pay attention, Jan Burse! I am comparing functions f and f' each with the SAME domain (x) and codomain (y).

Dan

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

So f ≈ f' is false if f and f' have not the same domain and codomain?
So why do you point to 114-122, this is not covered there.

So what is your definition of f ≈ f'? Students be aware, John
Gabriels new calculus is more formal than DC poops gibberish.

Still no formal definition of f ≈ f' available?

Dan Christensen schrieb am Freitag, 4. Februar 2022 um 06:54:12 UTC+1:
> On Thursday, February 3, 2022 at 11:03:35 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> > If I take Dan-Matiks advice:
> >
> > > "Perhaps you didn't know, but two functions f and f' with the same domain X
> > > and codomain Y are actually the SAME function if f(a)=f'(a) for all a in X. "
> > > See for example, lines 114-122 in my proof https://www.dcproof.com/ExistenceUniqueIdentityFunction.htm
> >
> > I would define, what is proved in 114-122:
> >
> > f ≈ f' :<=> ALL(a):[a e x => f(a) e y] &
> > ALL(a):[a e x => f'(a) e y]
> > => ALL(a):[a e x => f(a)=f'(a)]
> >
> > But this obviously doesn't work. If f has a different
> > doman and codomain as f', then we have f ≈ f' trivially
> > true because of the material main implication =>:
> >
> Pay attention, Jan Burse! I am comparing functions f and f' each with the SAME domain (x) and codomain (y).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, February 4, 2022 at 2:29:26 AM UTC-5, Mostowski Collapse wrote:
> So f ≈ f' is false if f and f' have not the same domain and codomain?

Deny it if it makes you feel better, but given functions f and g such that ALL(a): [ a in x => f(a) in y ] and ALL(a): [ a in x => g(a) in y ], it is commonly said that f and g are the SAME function iff ALL(a): [ a in x => f(a)=g(a) ].

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

Thats verbal gibberisch, what is your formal definition
of f ≈ g could you please write it down?

Dan Christensen schrieb am Freitag, 4. Februar 2022 um 16:39:06 UTC+1:
> On Friday, February 4, 2022 at 2:29:26 AM UTC-5, Mostowski Collapse wrote:
> > So f ≈ f' is false if f and f' have not the same domain and codomain?
> Deny it if it makes you feel better, but given functions f and g such that ALL(a): [ a in x => f(a) in y ] and ALL(a): [ a in x => g(a) in y ], it is commonly said that f and g are the SAME function iff ALL(a): [ a in x => f(a)=g(a) ].
>
> 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

The standard same-ness is:

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

You can then prove, for example in tree tool, that
there are universal class many different identity
functions on N, that satisfy this

Dan-O-Matik nonsense:

∀x(x in N => f(x) = x)

Thats easy to prove, just take N to be purple, and
then some ~(c e N), some not purple. We immediately
get the following, f : N u {c} -> N u {c} identity by

Dan-O-Matik standards, then the same f, also
f : N -> N identity by Dan-O-Matik standards, namely
we can prove this here:

∀x((ExN ∨ x=c) → f(x)=x) → ∀x(ExN → f(x)=x) is valid.

Dan-O-Matik himself proved already that NOT PURPLE
is a proper class. You can choose f_c : N u {c} -> N u {c}
so that f_c(x) = 0 for ~(x e N u {c}),

so that by the standard sameness all the f_c are
different. So they form a proper class, since there is
a bijection to NOT PURPLE.

Q.E.D.

Mostowski Collapse schrieb am Freitag, 4. Februar 2022 um 18:24:55 UTC+1:
> Thats verbal gibberisch, what is your formal definition
> of f ≈ g could you please write it down?
> Dan Christensen schrieb am Freitag, 4. Februar 2022 um 16:39:06 UTC+1:
> > On Friday, February 4, 2022 at 2:29:26 AM UTC-5, Mostowski Collapse wrote:
> > > So f ≈ f' is false if f and f' have not the same domain and codomain?
> > Deny it if it makes you feel better, but given functions f and g such that ALL(a): [ a in x => f(a) in y ] and ALL(a): [ a in x => g(a) in y ], it is commonly said that f and g are the SAME function iff ALL(a): [ a in x => f(a)=g(a) ].
> >
> > 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

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 schrieb am Freitag, 4. Februar 2022 um 18:25:48 UTC+1:
> The standard same-ness is:
>
> f ≈ g :<=> ∀x(f(x)=g(x))
>
> You can then prove, for example in tree tool, that
> there are universal class many different identity
> functions on N, that satisfy this
>
> Dan-O-Matik nonsense:
>
> ∀x(x in N => f(x) = x)
>
> Thats easy to prove, just take N to be purple, and
> then some ~(c e N), some not purple. We immediately
> get the following, f : N u {c} -> N u {c} identity by
>
> Dan-O-Matik standards, then the same f, also
> f : N -> N identity by Dan-O-Matik standards, namely
> we can prove this here:
>
> ∀x((ExN ∨ x=c) → f(x)=x) → ∀x(ExN → f(x)=x) is valid.
>
> Dan-O-Matik himself proved already that NOT PURPLE
> is a proper class. You can choose f_c : N u {c} -> N u {c}
> so that f_c(x) = 0 for ~(x e N u {c}),
>
> so that by the standard sameness all the f_c are
> different. So they form a proper class, since there is
> a bijection to NOT PURPLE.
>
> Q.E.D.
> Mostowski Collapse schrieb am Freitag, 4. Februar 2022 um 18:24:55 UTC+1:
> > Thats verbal gibberisch, what is your formal definition
> > of f ≈ g could you please write it down?
> > Dan Christensen schrieb am Freitag, 4. Februar 2022 um 16:39:06 UTC+1:
> > > On Friday, February 4, 2022 at 2:29:26 AM UTC-5, Mostowski Collapse wrote:
> > > > So f ≈ f' is false if f and f' have not the same domain and codomain?
> > > Deny it if it makes you feel better, but given functions f and g such that ALL(a): [ a in x => f(a) in y ] and ALL(a): [ a in x => g(a) in y ], it is commonly said that f and g are the SAME function iff ALL(a): [ a in x => f(a)=g(a) ].
> > >
> > > 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 Friday, February 4, 2022 at 12:25:48 PM UTC-5, Mostowski Collapse wrote:
> The standard same-ness is:
>
> f ≈ g :<=> ∀x(f(x)=g(x))
>

Maybe in philosophy class, but in mathematics, you can't have a function without an explicit domain set. Try again, Jan Burse.

Dan

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

Well the domain of a function is easy:

dom(f) := { x | ∃y (x,y) e f }

You then have:

f = g => dom(f) = dom(g)

Don't you have dom() in DC poop?

You can even prove that. You don't need
to "believe" anything. Write Exy for
x in y and write p(x) for the projection

of a pair to its first component:

∀x(Exf ↔ Exg) → ∀x(∃y(Eyf ∧ x=p(y)) ↔ ∃y(Eyg ∧ x=p(y)))
https://www.umsu.de/trees/#~6x%28Exf~4Exg%29~5~6x%28~7y%28Eyf~1x=p%28y%29%29~4~7y%28Eyg~1x=p%28y%29%29%29

The proof needs only reflexivity of equality.

Mostowski Collapse schrieb:
> Well the domain of a function is easy:
>
> dom(f) := { x | ∃y (x,y) e f }
>
> You then have:
>
> f = g => dom(f) = dom(g)
>
> Don't you have dom() in DC poop?

Nice corrolary:

dom(f) ≠ dom(g) => f ≠ g

Proof:
Just use contraposition.

Q.E.D.

The corrolary motivates my question,
what does Dan-O-Matik SAME-ness do, when
domains are different?

It should give false, doesn't it? What
is your definition of SAME-ness for
your functions Dan-O-Matik?

You still don't know?
So you don't know what you are doing?

LMAO!

Mostowski Collapse schrieb:
> You can even prove that. You don't need
> to "believe" anything. Write Exy for
> x in y and write p(x) for the projection
>
> of a pair to its first component:
>
> ∀x(Exf ↔ Exg) → ∀x(∃y(Eyf ∧ x=p(y)) ↔ ∃y(Eyg ∧ x=p(y)))
> https://www.umsu.de/trees/#~6x%28Exf~4Exg%29~5~6x%28~7y%28Eyf~1x=p%28y%29%29~4~7y%28Eyg~1x=p%28y%29%29%29
>
>
> The proof needs only reflexivity of equality.
>
> Mostowski Collapse schrieb:
>> Well the domain of a function is easy:
>>
>> dom(f) := { x | ∃y (x,y) e f }
>>
>> You then have:
>>
>> f = g => dom(f) = dom(g)
>>
>> Don't you have dom() in DC poop?
>

On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse wrote:
> Well the domain of a function is easy:
>
> dom(f) := { x | ∃y (x,y) e f }
>
> You then have:
>
> f = g => dom(f) = dom(g)
>
> Don't you have dom()

I haven't found it necessary. As is standard practice in textbook math proofs, whenever I introduce a function in a proof, I also introduce its domain and codomain sets.

Dan

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

And what is your standard practice SAME-ness, that you
are using. Can you define it? Or are you still clueless?

Clueless - ORIGINAL TRAILER HD
https://www.youtube.com/watch?v=9Um1SvJvDLY

Dan Christensen schrieb:
> On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse wrote:
>> Well the domain of a function is easy:
>>
>> dom(f) := { x | ∃y (x,y) e f }
>>
>> You then have:
>>
>> f = g => dom(f) = dom(g)
>>
>> Don't you have dom()
>
> I haven't found it necessary. As is standard practice in textbook math proofs, whenever I introduce a function in a proof, I also introduce its domain and codomain sets.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>