First learn how my historic geometric identity of January 2020 proves your mainstream formulation
of calculus is an elaborate fraud:

https://drive.google.com/file/d/1RDulODvgncItTe7qNI1d8KTN5bl0aTXj

Seeing is believing, so download the following applet and watch how my historic geometric theorem
works for any given function:

https://drive.google.com/file/d/1ON1GQ7b6UNpZSEEsbG14eAFCPv8p03pv

There are no viruses or spy software in my applets and to my knowledge most browsers will warn
you before you download any malicious code in applets. Don't waste your time on the fraudulent
mainstream formulation of calculus which cannot be understood because it is anti-mathematical nonsense.
Download my applet now and gain understanding and knowledge you couldn't find at school or university!

Second, learn how it fixes the mainstream bogus definition of definite integral:

https://drive.google.com/file/d/1uIBgJ1ObroIbkt0V2YFQEpPdd8l-xK6y

Applet which explains the definite integral without any ill-formed concepts such as infinity,
infinitesimals or the circular rot of limit theory:

https://drive.google.com/file/d/1JYRxjGb3MxlYWp_2KqVXwXNr5XUvUNz7

A video explaining the new applet:

https://youtu.be/TJqvbshIGtg

Third, study my free eBook because not only your mathematical future depends on it but also your sanity!

https://drive.google.com/file/d/1CIul68phzuOe6JZwsCuBuXUR8X-AkgEO

Lastly, ignore all the trolls and cranks such as Dan Christensen, Jean Pierre Messager (aka Python aka YBM aka JPM),
Jan Burse, Michael MORONey, QB, Earle, Jens Stuckelberger, Jan Bilawski, Zelos Malum, Markus Klyver, Alan McKenzie,
Ludwig Poehlman (certified crank aka Archimedes Plutonium) etc. These fools have nothing to say about my work.
All they know is how to throw shade because they are ignorant, arrogant, incompetent and incorrigibly stupid.
Unfortunately, sci.math has become the mainstream's "Truth Network" - replete with paid trolls, some of whose names
are mentioned in this paragraph. These fools have lost the privilege of being educated by me. Gracing them with any
kind of response is like placing a prized pearl on a pile of dung.

I shall not respond to any of them again.

At times it's good to laugh at the stupidity and dishonesty of mainstream academics. However, the situation is dire
when religion trumps common sense:

https://drive.google.com/file/d/1520NjhgiakcrssQxtbxRCDXus_aHXpI9

This comment will be periodically reposted for the sake of new visitors as long as I am alive.

My lecture on the true Foundations of Mathematics was recorded.

You can download it here:

https://youtu.be/_WZJY1xgJTk

The Gift applet (almost in power point format!):

https://drive.google.com/file/d/1SYT-MbYtXUAYgwPeTgZ8QC8gxNpj-fap

Remember, you cannot understand mathematics without me because no one understands mathematics as
well as I do. The lecture is a bit on the slow side (because of my health issues), BUT you will
learn more about the foundations of mathematics than you ever knew your entire life!

The Elements is not about geometry. It's not about algebra. It's not about constructions. It is a
template for the realisation of all SCIENCE.

I quote a Greek scholar (http://www.physics.ntua.gr/mourmouras/euclid/common/anti_prologou.html):

Τα Στοιχεία Ευκλείδου δέν είναι Γεωμετρία (ούτε επιπεδομετρία, ούτε γεωμετρία χώρου), απλώς μπορούν
να παραχθούν από αύτα «Γεωμετρίες» (είτε «Ευκλείδειες,» είτε «μή Ευκλείδειες», κλπ), όπως επίσης
μπορούν να παραχθούν πολλές άλλες θεωρίες «Μαθηματικές» καί όχι μόνο, π.χ. Θεωρία Αριθμών, Aναλογίες,
Aσύμμετρα Μεγέθη, Θεωρία της Σχετικότητας, κ.α.

Τα Στοιχεία τού Ευκλείδου δεν είναι ούτε αντικείμενα του Πραγματικού κόσμου, καίούτε είναι αντικείμενα
τών Μαθηματικών, αλλά χωρίς αυτά, όλα τά παραπάνω δέν μπορούν να περιγραφούν, να κατανοηθούν, να ερμηνευτούν.

Πολλοί συγχέουν τον πραγματικό χώρο τών «Φυσικών» επιστημών με τά Στοιχεία Ευκλείδου. Aπό τα Στοιχεία
Ευκλείδου προέρχονται οί πλείστες μαθηματικές καί φυσικές επιστήμες, τόσο οί παραδοσιακές όσο καί οί
μοντέρνες. Γιά τις τεχνολογίες αυτό είναι προφανές.

Τα Στοιχεία Ευκλείδου αποτελούν ένα ενιαίον όλο, ένα «Σύστημα», τό οποίο είναι «κλειστό καί ἀνοικτό»,
τόσο όσο καί ή σκέψη, ό λόγος καί ή γραμματική τής ανθρώπινης υπόστασης. H πληρότητα καί ἡ συνέπεια
είναι δομημένες μέ έναν εκπληκτικό τρόπο, πού τό καθιστούν μοναδικό.

My καθαρεύουσα (high Greek) Greek is very poor, but here is my translation:

Euclidean Elements are not Geometry (neither plane geometry nor space geometry), from these can be produced
"Geometries" (either "Euclidean" or "non-Euclidean", etc.), as well as many other "Mathematical" theories
can be produced and not only, e.g. Number Theory, Proportions, Asymmetric Sizes, Theory of Relativity, etc.

The Elements of Euclid are neither objects of the real world, nor are they objects of Mathematics, but without
them, all the above cannot be described, understood, interpreted. Many confuse the real world of the "Natural"
sciences with the Euclidean Elements. Most of the mathematical and natural sciences, both traditional and modern,
come from the Euclidean Elements. For technologies this is obvious.

The Euclidean Elements constitute a single whole, a "System", which is "closed and open", as much as the thought,
reason and grammar of the human condition. Completeness and consistency are structured in an amazing way,
which make it unique.

----------------------------------------------------------

This professor (of Physics and mathematics) also reads all the Ancient texts and gives lectures. He is quite an
interesting academic and very learned. He is currently reading all of Aristotle's texts:

https://www.youtube.com/c/DimitriosMourmouras

What you probably do not know is that there is no mention of any of the following words in the Elements:

axiom
geometry
straight-edge or ruler
compass

The diagrams are merely used as a means of communicating the relationships between points (location) and
distances (lines).

The Elements is a product of pure thought that was realised first by the brilliant Ancient Greeks.

Become a subscriber to my New Calculus YT channel to learn more mathematics than you learned in all your
school and university years:

https://www.youtube.com/c/JohnGabriel/videos

Mainstream mathematics has turned into a universe of alternate "facts". The majority of mainstream academics
are stupid and ignorant beyond belief so that mainstream math is today more of a cult than the science it was meant to be.

Unfortunately mainstream academia does not teach one how to think, only to memorise the prescribed doctrines
that form their official statement of beliefs. Free yourself from the utter bullshit you are forced to memorise
and if you're honest with yourself, will admit that you never actually understand.

Mainstream academia are themselves alarmed because their days of deception are numbered. I am their prime target
because the more I publish facts (truth), the more I am hated for it. Even the certified cranks (Archimedes Plutonium aka Ludwig Poehlman)
join in the mocking spectacle.

Don't believe a word I say, but prove that what I say is indeed the case. How, you ask? Use your brain!

There's more....

Learn about the BIG LIE "Calculus was made rigorous...":

https://www.academia.edu/45408445/Big_Lie_Calculus_was_made_rigorous

"Why can’t you understand the difference between assuming that f'(x)=3x^2, as a “fact” upon which to build
further proofs, and hypothesizing that f'(x) might equal 3x^2, as a guess to be treated with extreme suspicion
and checked using the definition before I’m allowed to write f'(x)=3x^2?" - Anders Kaesorg.

The 5 Step method is outlined below and it summarises the mindset of most morons from MIT:

1. Assumption of fact
2. Hypothesis
3. Probability
4. Suspicion
5. Verification

:-)

https://youtu.be/gX5Bt8BEdNM

Subscribe to my YT Channel - the best math channel on the web:

https://www.youtube.com/c/JohnGabriel/videos

Who gave you the 0.999... and the 0.333...:

Euler wrote a very good book on algebra but unfortunately it was soiled with his delusional notions.

Daher ist uns Bruch 1/(1+a) gleich dieser unendlichen Reihe 1 - a + aa -aaa + ...&c.

Therefore is our fraction 1/(1+a) equal to this infinite series 1 - a + aa -aaa + ...&c.

1/(1+a) is the <<limit>> of the series <<1 - a + aa -aaa + ...&c.>>

JG's Pathetic Daily Spam Post -- Same shit AGAIN and AGAIN!
STUDENTS BEWARE: Don't be a victim of John Gabriel's fake math

On Sunday, July 17, 2022 at 6:47:36 AM UTC-4, Eram semper recta wrote:
> First learn how ...

[snip]

When will YOU learn Troll Boy?

JG here claims to have a discovered a shortcut to mastering calculus without using limits. Unfortunately for him, this means he has no workable a definition of the derivative of a function. It blows up for functions as simple f(x)=|x|. Or even f(x)=0. As a result, he has had to ban 0, negative numbers and instantaneous rates of change rendering his goofy little system quite useless.

Forget calculus. JG has also banned all axioms because he cannot even derive the most elementary results of basic arithmetic, e.g. 2+2=4. Such results require the use of axioms, so he must figure he's now off the hook.

Even at his advanced age (60+?), John Gabriel is STILL struggling with basic, elementary-school arithmetic. As he has repeatedly posted here:

"There are no points on a line."
--April 12, 2021

"Pi is NOT a number of ANY kind!"
--July 10, 2020

"1/2 not equal to 2/4"
--October 22, 2017

“1/3 does NOT mean 1 divided by 3 and never has meant that”
-- February 8, 2015

"3 =< 4 is nonsense.”
--October 28, 2017

"Zero is not a number."
-- Dec. 2, 2019

"0 is not required at all in mathematics, just like negative numbers."
-- Jan. 4, 2017

“There is no such thing as an empty set.”
--Oct. 4, 2019

“3 <=> 2 + 1 or 3 <=> 8 - 5, etc, are all propositions” (actually all are meaningless gibberish)
--Oct. 22, 2019

No math genius our JG, though he actually lists his job title as “mathematician” at Linkedin.com. Apparently, they do not verify your credentials.

Though really quite disturbing, interested readers should see: “About the spamming troll John Gabriel in his own words...” (lasted updated March 10, 2020) at https://groups.google.com/forum/#!msg/sci.math/PcpAzX5pDeY/1PDiSlK_BwAJ

Dan

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

TUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math
He has absolutely no clue what the text book definition of a function is.

But its extremly extemly trivial.

The concept of a function is not constructed. Its only defined.
Its a classifier and not a factory. It classifies certain sets [or

classes if you dare] as functions. Its quite trivial:

1) rel(f) <=> ALL(z):[z e f => EXIST(x):EXIST(y):[z=(x,y)]]
2) fun(f) <=> rel(f) & ALL(x):ALL(y1):ALL(y2):[(x,y1) e f & (x,y2) e f => y1=y2]]

Then there are derived notions, which have further parameters:

f total on X: ALL(x):[x e X => EXIST(y):[(x,y) e f]]
domain of f: dom(f) = { x | EXIST(y):[(x,y) e f] }
Etc...

One can prove, right? Yes or No?

domain of f = greatest X so that f total on X

Can you prove this theorem in DC Poop?

Dan Christensen schrieb am Sonntag, 17. Juli 2022 um 16:02:59 UTC+2:
> JG's Pathetic Daily Spam Post -- Same shit AGAIN and AGAIN!
> STUDENTS BEWARE: Don't be a victim of John Gabriel's fake math

As some people on math stack exchange (MSE) have explained
you, some things have further names:

- In "f total on X", the parameter X is called an extrinsic domain,
there can be many extrinsic domains for the same particular function f

- In "domain of f", the result is called the intrinsic domain,
in this conceptualization there is exactly one for a particular function f,

the later allows one to write dom(f).

Mostowski Collapse schrieb am Montag, 18. Juli 2022 um 21:53:21 UTC+2:
> TUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math
> He has absolutely no clue what the text book definition of a function is.
>
> But its extremly extemly trivial.
>
> The concept of a function is not constructed. Its only defined.
> Its a classifier and not a factory. It classifies certain sets [or
>
> classes if you dare] as functions. Its quite trivial:
>
> 1) rel(f) <=> ALL(z):[z e f => EXIST(x):EXIST(y):[z=(x,y)]]
> 2) fun(f) <=> rel(f) & ALL(x):ALL(y1):ALL(y2):[(x,y1) e f & (x,y2) e f => y1=y2]]
>
> Then there are derived notions, which have further parameters:
>
> f total on X: ALL(x):[x e X => EXIST(y):[(x,y) e f]]
> domain of f: dom(f) = { x | EXIST(y):[(x,y) e f] }
> Etc...
>
> One can prove, right? Yes or No?
>
> domain of f = greatest X so that f total on X
>
> Can you prove this theorem in DC Poop?
> Dan Christensen schrieb am Sonntag, 17. Juli 2022 um 16:02:59 UTC+2:
> > JG's Pathetic Daily Spam Post -- Same shit AGAIN and AGAIN!
> > STUDENTS BEWARE: Don't be a victim of John Gabriel's fake math

Now we come to the notion of equality, lets use Fritz:

Fritz Feldhase schrieb am Sonntag, 17. Juli 2022 um 23:40:56 UTC+2:
> (a) the set of ordered pairs *is* the function, [set-theoretic approach]
>
> or
>
> (b) The function is a (certain) triple (g, A, B) where g is a set of ordered pairs, the "graph" of the function, A the domain of the function and B its codomain. [Bourbaki's/"mathematical" approach.]

For (a) equality is trivial, one can prove from set theory,
so you DON'T NEED TO DEFINE EQUALITY, it is already built
into set theory through extensionality:

ALL(f):ALL(g):[fun(f) & fun(g) => (f = g <=> dom(f)=dom(g) &
ALL(x):ALL(y1):ALL(y2):[x e dom(f) & (x,y1) e f & (x,y2) e g => y1=y2])]

For (b) you might want to compare the declared
codomain as well. Make functions different when they
have different declared codomain.

Mostowski Collapse schrieb am Montag, 18. Juli 2022 um 22:03:23 UTC+2:
> As some people on math stack exchange (MSE) have explained
> you, some things have further names:
>
> - In "f total on X", the parameter X is called an extrinsic domain,
> there can be many extrinsic domains for the same particular function f
>
> - In "domain of f", the result is called the intrinsic domain,
> in this conceptualization there is exactly one for a particular function f,
>
> the later allows one to write dom(f).
> Mostowski Collapse schrieb am Montag, 18. Juli 2022 um 21:53:21 UTC+2:
> > TUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math
> > He has absolutely no clue what the text book definition of a function is.
> >
> > But its extremly extemly trivial.
> >
> > The concept of a function is not constructed. Its only defined.
> > Its a classifier and not a factory. It classifies certain sets [or
> >
> > classes if you dare] as functions. Its quite trivial:
> >
> > 1) rel(f) <=> ALL(z):[z e f => EXIST(x):EXIST(y):[z=(x,y)]]
> > 2) fun(f) <=> rel(f) & ALL(x):ALL(y1):ALL(y2):[(x,y1) e f & (x,y2) e f => y1=y2]]
> >
> > Then there are derived notions, which have further parameters:
> >
> > f total on X: ALL(x):[x e X => EXIST(y):[(x,y) e f]]
> > domain of f: dom(f) = { x | EXIST(y):[(x,y) e f] }
> > Etc...
> >
> > One can prove, right? Yes or No?
> >
> > domain of f = greatest X so that f total on X
> >
> > Can you prove this theorem in DC Poop?
> > Dan Christensen schrieb am Sonntag, 17. Juli 2022 um 16:02:59 UTC+2:
> > > JG's Pathetic Daily Spam Post -- Same shit AGAIN and AGAIN!
> > > STUDENTS BEWARE: Don't be a victim of John Gabriel's fake math

Mostowski Collapse wrote:

> As some people on math stack exchange (MSE) have explained you, some
> things have further names:
> - In "f total on X", the parameter X is called an extrinsic domain,
> there can be many extrinsic domains for the same particular function f

Good point. I guess the first learn, these dirty lying capitalists, are
*NOT_to_laugh* to the public.

UK's 'next Prime Minister contender' Liz Truss gets completely OWNED
https://www.bitchute.com/video/CdHiFuPwCsuc/

Lying ROYAL HYPOCRITE talks about Climate Change after taking 21 private
jet trips in 2 year https://www.bitchute.com/video/Vmzg6UVKsvcF/

Switzerland 16.7.22 Klaus Schwab, Bill Gates, and Anthony Fauci highlight
wanted posters. https://www.bitchute.com/video/DXlJaWXhxocV/

Are you from the same litter?

J.Geco - Chicken Song
https://www.youtube.com/watch?v=msSc7Mv0QHY

Rico Maria schrieb am Montag, 18. Juli 2022 um 22:11:31 UTC+2:
> ... I am a chicken ...

On Monday, July 18, 2022 at 3:53:21 PM UTC-4, Mostowski Collapse wrote:
> TUDENTS BEWARE...

See my reply to your identical postings just now at sci.logic

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:

> Are you from the same litter? J.Geco - Chicken Song

Your hanging dick corrupts the given data. Here we go one more time.

Good point. I guess the first they learn, these dirty lying capitalists,
are *NOT_to_laugh* to the public.

UK's 'next Prime Minister contender' Liz Truss gets completely OWNED
https://www.bitchute.com/video/CdHiFuPwCsuc/

Lying ROYAL HYPOCRITE talks about Climate Change after taking 21 private
jet trips in 2 year https://www.bitchute.com/video/Vmzg6UVKsvcF/

Switzerland 16.7.22 Klaus Schwab, Bill Gates, and Anthony Fauci highlight
wanted posters. https://www.bitchute.com/video/DXlJaWXhxocV/

The readers have already judged.
There are two notions of functions:

Fritz Feldhase schrieb am Sonntag, 17. Juli 2022 um 23:40:56 UTC+2:
> (a) the set of ordered pairs *is* the function, [set-theoretic approach]
>
> or
>
> (b) The function is a (certain) triple (g, A, B) where g is a set of ordered pairs, the "graph" of the function, A the domain of the function and B its codomain. [Bourbaki's/"mathematical" approach.]

DC Proof got neither correct. Why? Because it doesn't
have a intrinsic notion of domain. In set theoretic
approach the intrinsic notion of domain is:

Mostowski Collapse schrieb am Montag, 18. Juli 2022 um 21:49:31 UTC+2:
> domain of f: dom(f) = { x | EXIST(y):[(x,y) e f] }
> Etc...

Its not some free floating parameter, it depends
on f. You can do the same for Bourbakis, make
domain and codmain intrinsic properties of (g, A, B).

But in your nonsense here, dom and cod are
free foating. Its the biggest stupidity turd I
have ever seen:

> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

It allows easily to derive f=g & ~(f=g). Its
totally useless bull shit.

Dan Christensen schrieb am Montag, 18. Juli 2022 um 22:20:15 UTC+2:
> On Monday, July 18, 2022 at 3:53:21 PM UTC-4, Mostowski Collapse wrote:
> > STUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math
> > He has absolutely no clue what the text book definition of a function is.

On Monday, July 18, 2022 at 6:42:06 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:

> There are two notions of functions:

> Fritz Feldhase schrieb am Sonntag, 17. Juli 2022 um 23:40:56 UTC+2:
> > (a) the set of ordered pairs *is* the function, [set-theoretic approach]
> >
> > or
> >
> > (b) The function is a (certain) triple (g, A, B) where g is a set of ordered pairs, the "graph" of the function, A the domain of the function and B its codomain. [Bourbaki's/"mathematical" approach.]

OR...

(c) From DC Proof and a bit more conventional:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(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]]]]

> It allows easily to derive f=g & ~(f=g).

STILL waiting for your FORMAL (no hand-waving) proof of this outrageous claim, Jan Burse. Do try to keep in mind that to prove that two functions are equal or not equal, they must have the SAME domains and codomains.

Dan

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

Nothing outrageous drama queen. See here:

Mostowski Collapse schrieb am Dienstag, 19. Juli 2022 um 23:20:53 UTC+2:
> I did my part, here is my proof of f1=f2,
> for f1(0)=0 and f2(0)=1 (sic!). Where is your proof ~(f1=f2).
> If you don't deliver it, I can deliver it. No problem.
>
> 62 f1=f2
> Detach, 47, 61
https://groups.google.com/g/sci.logic/c/iRJvlsKToKc/m/dYMKjFEPDQAJ

What do you want to do later. Write an apology?

Jerk

Dan Christensen schrieb am Dienstag, 19. Juli 2022 um 02:14:25 UTC+2:
> STILL waiting for your FORMAL (no hand-waving) proof of this outrageous claim, Jan Burse.

The concept of vacously true, isnt something
that has entered your working memory of logic yet?
It was discussed here in sci.logic like a dozen times.

Basicall if it is that:

ALL(x):[~A(x)]

Then we can conclude:

ALL(x):[A(x) => B(x)]

Mostowski Collapse schrieb am Mittwoch, 20. Juli 2022 um 01:56:54 UTC+2:
> Nothing outrageous drama queen. See here:
>
> Mostowski Collapse schrieb am Dienstag, 19. Juli 2022 um 23:20:53 UTC+2:
> > I did my part, here is my proof of f1=f2,
> > for f1(0)=0 and f2(0)=1 (sic!). Where is your proof ~(f1=f2).
> > If you don't deliver it, I can deliver it. No problem.
> >
> > 62 f1=f2
> > Detach, 47, 61
> https://groups.google.com/g/sci.logic/c/iRJvlsKToKc/m/dYMKjFEPDQAJ
>
> What do you want to do later. Write an apology?
>
> Jerk
> Dan Christensen schrieb am Dienstag, 19. Juli 2022 um 02:14:25 UTC+2:
> > STILL waiting for your FORMAL (no hand-waving) proof of this outrageous claim, Jan Burse.

On Tuesday, July 19, 2022 at 7:56:54 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> Nothing outrageous drama queen. See here:
>
> Mostowski Collapse schrieb am Dienstag, 19. Juli 2022 um 23:20:53 UTC+2:
> > I did my part, here is my proof of f1=f2,
> > for f1(0)=0 and f2(0)=1 (sic!). Where is your proof ~(f1=f2).
> > If you don't deliver it, I can deliver it. No problem.
> >

Jeez, yer dumb! You (or was it your little buddy and fellow troll, JG) proved that two other functions, both empty, are equal. Oh, wait... he doesn't "believe in" empty sets. In any case, now you must prove them NOT equal to obtain the required contradiction. Good luck with that, Jan Burse. (Hee, hee!)

Dan

You said they are not equal here:

You wrote:
> > On Sunday, July 17, 2022 at 2:13:23 AM UTC-4,Mostowski Collapse
> > Here is a proof of f1(0)=0. I guess you can also prove f2(0)=1.
>
> OK.
>
> ~f1(0)=f2(0) and, therefore, ~f1=f2

Do you retract your claim?

Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 04:19:38 UTC+2:
> On Tuesday, July 19, 2022 at 7:56:54 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> > Nothing outrageous drama queen. See here:
> >
> > Mostowski Collapse schrieb am Dienstag, 19. Juli 2022 um 23:20:53 UTC+2:
> > > I did my part, here is my proof of f1=f2,
> > > for f1(0)=0 and f2(0)=1 (sic!). Where is your proof ~(f1=f2).
> > > If you don't deliver it, I can deliver it. No problem.
> > >
> Jeez, yer dumb! You (or was it your little buddy and fellow troll, JG) proved that two other functions, both empty, are equal. Oh, wait... he doesn't "believe in" empty sets. In any case, now you must prove them NOT equal to obtain the required contradiction. Good luck with that, Jan Burse. (Hee, hee!)
>
> Dan

Anyway, you try to evade the demonstration that
your function equality leads to absurdity by being lazy?
Good luck with that, here is the proof now:

146 f1=f2 & ~f1=f2
Join, 65, 145

------------------------------------ cut here ---------------------------------------------

1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Fn Equality

2 ~0=1
Axiom

3 f1(0)=0
Axiom

4 f2(0)=1
Axiom

5 ALL(x):[x ε dom <=> x=0]
Axiom

6 ALL(x):~x ε dom2
Axiom

7 ALL(y):[y ε cod <=> y=0 | y=1]
Axiom

8 Set(dom)
Axiom

9 Set(dom2)
Axiom

10 Set(cod)
Axiom

11 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Fn Equality

12 ALL(cod):ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 11

13 ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 12

14 ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 13

15 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]
U Spec, 14

16 EXIST(a):[a ε dom2 & ~f2(a) ε cod]
Premise

17 u ε dom2 & ~f2(u) ε cod
E Spec, 16

18 ~u ε dom2
U Spec, 6

19 u ε dom2
Split, 17

20 ~f2(u) ε cod
Split, 17

21 u ε dom2 & ~u ε dom2
Join, 19, 18

22 ~EXIST(a):[a ε dom2 & ~f2(a) ε cod]
Conclusion, 16

23 ~~ALL(a):~[a ε dom2 & ~f2(a) ε cod]
Quant, 22

24 ALL(a):~[a ε dom2 & ~f2(a) ε cod]
Rem DNeg, 23

25 ALL(a):~~[~a ε dom2 | ~~f2(a) ε cod]
DeMorgan, 24

26 ALL(a):[~a ε dom2 | ~~f2(a) ε cod]
Rem DNeg, 25

27 ALL(a):[~a ε dom2 | f2(a) ε cod]
Rem DNeg, 26

28 ALL(a):[~~a ε dom2 => f2(a) ε cod]
Imply-Or, 27

29 ALL(a):[a ε dom2 => f2(a) ε cod]
Rem DNeg, 28

30 EXIST(a):[a ε dom2 & ~f1(a) ε cod]
Premise

31 u ε dom2 & ~f1(u) ε cod
E Spec, 30

32 u ε dom2
Split, 31

33 ~f1(u) ε cod
Split, 31

34 ~u ε dom2
U Spec, 6

35 u ε dom2 & ~u ε dom2
Join, 32, 34

36 ~EXIST(a):[a ε dom2 & ~f1(a) ε cod]
Conclusion, 30

37 ~~ALL(a):~[a ε dom2 & ~f1(a) ε cod]
Quant, 36

38 ALL(a):~[a ε dom2 & ~f1(a) ε cod]
Rem DNeg, 37

39 ALL(a):~~[~a ε dom2 | ~~f1(a) ε cod]
DeMorgan, 38

40 ALL(a):[~a ε dom2 | ~~f1(a) ε cod]
Rem DNeg, 39

41 ALL(a):[~a ε dom2 | f1(a) ε cod]
Rem DNeg, 40

42 ALL(a):[~~a ε dom2 => f1(a) ε cod]
Imply-Or, 41

43 ALL(a):[a ε dom2 => f1(a) ε cod]
Rem DNeg, 42

44 Set(dom2) & Set(cod)
Join, 9, 10

45 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
Join, 44, 43

46 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
Join, 45, 29

47 f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]
Detach, 15, 46

48 [f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]]
& [ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2]
Iff-And, 47

49 f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]
Split, 48

50 ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2
Split, 48

51 EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
Premise

52 u ε dom2 & ~f1(u)=f2(u)
E Spec, 51

53 u ε dom2
Split, 52

54 ~f1(u)=f2(u)
Split, 52

55 ~u ε dom2
U Spec, 6

56 u ε dom2 & ~u ε dom2
Join, 53, 55

57 ~EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
Conclusion, 51

58 ~~ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
Quant, 57

59 ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
Rem DNeg, 58

60 ALL(a):~~[~a ε dom2 | ~~f1(a)=f2(a)]
DeMorgan, 59

61 ALL(a):[~a ε dom2 | ~~f1(a)=f2(a)]
Rem DNeg, 60

62 ALL(a):[~a ε dom2 | f1(a)=f2(a)]
Rem DNeg, 61

63 ALL(a):[~~a ε dom2 => f1(a)=f2(a)]
Imply-Or, 62

64 ALL(a):[a ε dom2 => f1(a)=f2(a)]
Rem DNeg, 63

65 f1=f2
Detach, 50, 64

66 ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 1

67 ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 66

68 ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 67

69 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]
U Spec, 68

70 EXIST(a):[a ε dom & ~f1(a) ε cod]
Premise

71 u ε dom & ~f1(u) ε cod
E Spec, 70

72 u ε dom <=> u=0
U Spec, 5

73 [u ε dom => u=0] & [u=0 => u ε dom]
Iff-And, 72

74 u ε dom => u=0
Split, 73

75 u=0 => u ε dom
Split, 73

76 u ε dom
Split, 71

77 ~f1(u) ε cod
Split, 71

78 u=0
Detach, 74, 76

79 ~f1(0) ε cod
Substitute, 78, 77

80 ~0 ε cod
Substitute, 3, 79

81 0 ε cod <=> 0=0 | 0=1
U Spec, 7

82 [0 ε cod => 0=0 | 0=1] & [0=0 | 0=1 => 0 ε cod]
Iff-And, 81

83 0 ε cod => 0=0 | 0=1
Split, 82

84 0=0 | 0=1 => 0 ε cod
Split, 82

85 0=0
Reflex

86 0=0 | 0=1
Arb Or, 85

87 0 ε cod
Detach, 84, 86

88 ~0 ε cod & 0 ε cod
Join, 80, 87

89 ~EXIST(a):[a ε dom & ~f1(a) ε cod]
Conclusion, 70

90 ~~ALL(a):~[a ε dom & ~f1(a) ε cod]
Quant, 89

91 ALL(a):~[a ε dom & ~f1(a) ε cod]
Rem DNeg, 90

92 ALL(a):~~[~a ε dom | ~~f1(a) ε cod]
DeMorgan, 91

93 ALL(a):[~a ε dom | ~~f1(a) ε cod]
Rem DNeg, 92

94 ALL(a):[~a ε dom | f1(a) ε cod]
Rem DNeg, 93

95 ALL(a):[~~a ε dom => f1(a) ε cod]
Imply-Or, 94

96 ALL(a):[a ε dom => f1(a) ε cod]
Rem DNeg, 95

97 EXIST(a):[a ε dom & ~f2(a) ε cod]
Premise

98 u ε dom & ~f2(u) ε cod
E Spec, 97

99 u ε dom
Split, 98

100 ~f2(u) ε cod
Split, 98

101 u ε dom <=> u=0
U Spec, 5

102 [u ε dom => u=0] & [u=0 => u ε dom]
Iff-And, 101

103 u ε dom => u=0
Split, 102

104 u=0 => u ε dom
Split, 102

105 u=0
Detach, 103, 99

106 ~f2(0) ε cod
Substitute, 105, 100

107 ~1 ε cod
Substitute, 4, 106

108 1 ε cod <=> 1=0 | 1=1
U Spec, 7

109 [1 ε cod => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε cod]
Iff-And, 108

110 1 ε cod => 1=0 | 1=1
Split, 109

111 1=0 | 1=1 => 1 ε cod
Split, 109

112 1=1
Reflex

113 1=0 | 1=1
Arb Or, 112

114 1 ε cod
Detach, 111, 113

115 ~1 ε cod & 1 ε cod
Join, 107, 114

116 ~EXIST(a):[a ε dom & ~f2(a) ε cod]
Conclusion, 97

117 ~~ALL(a):~[a ε dom & ~f2(a) ε cod]
Quant, 116

118 ALL(a):~[a ε dom & ~f2(a) ε cod]
Rem DNeg, 117

119 ALL(a):~~[~a ε dom | ~~f2(a) ε cod]
DeMorgan, 118

120 ALL(a):[~a ε dom | ~~f2(a) ε cod]
Rem DNeg, 119

121 ALL(a):[~a ε dom | f2(a) ε cod]
Rem DNeg, 120

122 ALL(a):[~~a ε dom => f2(a) ε cod]
Imply-Or, 121

123 ALL(a):[a ε dom => f2(a) ε cod]
Rem DNeg, 122

124 Set(dom) & Set(cod)
Join, 8, 10

125 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
Join, 124, 96

126 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
Join, 125, 123

127 f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]
Detach, 69, 126

128 [f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]]
& [ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2]
Iff-And, 127

129 f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]
Split, 128

130 ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2
Split, 128

131 ~ALL(a):[a ε dom => f1(a)=f2(a)] => ~f1=f2
Contra, 129

132 ALL(a):[a ε dom => f1(a)=f2(a)]
Premise

On Tuesday, July 19, 2022 at 11:16:12 PM UTC-4, Mostowski Collapse wrote:
> Anyway, you try to evade the demonstration that
> your function equality leads to absurdity by being lazy?
> Good luck with that, here is the proof now:
>
> 146 f1=f2 & ~f1=f2
> Join, 65, 145
>
[snip]

It is your inconsistent assumptions about the domains of these functions that result in contradictions. In one place, you assume their domain is dom2={ } and these functions are equal. In another place, their domain is dom={0} and they turn out to be NOT equal. The user must be careful not to introduce inconsistent axioms.

Dan

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

There is nothing inconsistent in the axioms.
These axioms are not inconsistent, you cannot
derive an inconsistency from them.

They only name an empty set (dom2), a
singleton set (dom) and a set with two elements
(cod). What is inconsistent in having these 3 sets?

The problem is your botched Fn Equality axiom.
Now I can prove any sentence:

146 f1=f2 & ~f1=f2
Join, 65, 145

147 ~AnySentence
Premise

148 f1=f2
Split, 146

149 ~f1=f2
Split, 146

150 f1=f2 & ~f1=f2
Join, 148, 149

151 ~~AnySentence
Conclusion, 147

152 AnySentence

LMAO!

Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 06:32:11 UTC+2:
> On Tuesday, July 19, 2022 at 11:16:12 PM UTC-4, Mostowski Collapse wrote:
> > Anyway, you try to evade the demonstration that
> > your function equality leads to absurdity by being lazy?
> > Good luck with that, here is the proof now:
> >
> > 146 f1=f2 & ~f1=f2
> > Join, 65, 145
> >
> [snip]
>
> It is your inconsistent assumptions about the domains of these functions that result in contradictions. In one place, you assume their domain is dom2={ } and these functions are equal. In another place, their domain is dom={0} and they turn out to be NOT equal. The user must be careful not to introduce inconsistent axioms.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

You use free floating ALL quantification. People
on MSE tried to explain you what extrinsic and
intrinsic paramters are. When you use free floating

ALL quantification then you treat these parameters
as extrinsic and you CANNOT MAKE ANYMORE
FORMALIZATIONS. To make logical formalizations

you need to make all parameters intrinsic.
You have to move from:

ALL(dom):ALL(f): ... f ... dom ....

To something where its not free floating:

ALL(f): ... f ... dom(f) ....

Its the same problem as the white horse problem
that I posted. Where you can flip the truth value
arbitrarily by instantiating the free floating parameter.

Mostowski Collapse schrieb am Mittwoch, 20. Juli 2022 um 09:28:50 UTC+2:
> There is nothing inconsistent in the axioms.
> These axioms are not inconsistent, you cannot
> derive an inconsistency from them.
>
> They only name an empty set (dom2), a
> singleton set (dom) and a set with two elements
> (cod). What is inconsistent in having these 3 sets?
>
> The problem is your botched Fn Equality axiom.
> Now I can prove any sentence:
> 146 f1=f2 & ~f1=f2
> Join, 65, 145
> 147 ~AnySentence
> Premise
>
> 148 f1=f2
> Split, 146
>
> 149 ~f1=f2
> Split, 146
>
> 150 f1=f2 & ~f1=f2
> Join, 148, 149
>
> 151 ~~AnySentence
> Conclusion, 147
>
> 152 AnySentence
>
> LMAO!
> Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 06:32:11 UTC+2:
> > On Tuesday, July 19, 2022 at 11:16:12 PM UTC-4, Mostowski Collapse wrote:
> > > Anyway, you try to evade the demonstration that
> > > your function equality leads to absurdity by being lazy?
> > > Good luck with that, here is the proof now:
> > >
> > > 146 f1=f2 & ~f1=f2
> > > Join, 65, 145
> > >
> > [snip]
> >
> > It is your inconsistent assumptions about the domains of these functions that result in contradictions. In one place, you assume their domain is dom2={ } and these functions are equal. In another place, their domain is dom={0} and they turn out to be NOT equal. The user must be careful not to introduce inconsistent axioms.
> > 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, July 20, 2022 at 3:28:50 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:

> Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 06:32:11 UTC+2:

> > It is your inconsistent assumptions about the domains of these functions that result in contradictions. In one place, you assume their domain is dom2={ } and these functions are equal. In another place, their domain is dom={0} and they turn out to be NOT equal. The user must be careful not to introduce inconsistent axioms.

> There is nothing inconsistent in the axioms.
> These axioms are not inconsistent, you cannot
> derive an inconsistency from them.
>

Wrong again, Jan Burse. You made assumptions about functions in your proof without first establishing their existence using the the Function Axiom. If you are going make such assumptions, you must be very careful. But you got careless, mixed up your domains and got burned. Let this be a lesson to you.

Dan

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

There was a thread about Russells definite descriptions,
and how to translate „the X such that Y“, and Dan Christensen
did it wrong, got some like „all X such that Y“

Now the same problem again. Terrence Tao uses
phrases such as THE domain or THE codomain, which
you cannot translate into ALL, linguistically

they are so called anaphora:

In linguistics, anaphora (/əˈnæfərə/) is the use of an
expression whose interpretation depends upon another
expression in context (its antecedent or postcedent)
https://en.m.wikipedia.org/wiki/Anaphora_(linguistics)

Its the same like in „THE color of the horse is white“
its pretty useless to translate it into:

color = white

you need to translate it into:

color_of(horse) = white

Dan Christensens brainless translation of Terrence Tao
doesnt make any sense. The more many times he posts
how wrongly he translated it, the

cringer the whole bullshit gets. It goes from bullshit,
to apeshit and then to batshit crazy.

Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 16:44:06 UTC+2:
> On Wednesday, July 20, 2022 at 3:28:50 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
>
> > Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 06:32:11 UTC+2:
>
> > > It is your inconsistent assumptions about the domains of these functions that result in contradictions. In one place, you assume their domain is dom2={ } and these functions are equal. In another place, their domain is dom={0} and they turn out to be NOT equal. The user must be careful not to introduce inconsistent axioms.
> > There is nothing inconsistent in the axioms.
> > These axioms are not inconsistent, you cannot
> > derive an inconsistency from them.
> >
> Wrong again, Jan Burse. You made assumptions about functions in your proof without first establishing their existence using the the Function Axiom. If you are going make such assumptions, you must be very careful. But you got careless, mixed up your domains and got burned. Let this be a lesson to you.
> 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, July 20, 2022 at 2:31:16 PM UTC-4, Mostowski Collapse wrote:
> There was a thread about Russells definite descriptions,
> and how to translate „the X such that Y“, and Dan Christensen
> did it wrong, got some like „all X such that Y“
>

I don't recall the particulars, but I do recall that you ended up looking like a complete idiot, Jan Burse. Why don't you post the link?

> Now the same problem again. Terrence Tao uses
> phrases such as THE domain or THE codomain, which
> you cannot translate into ALL

Grasping at straws as always, Jan Burse??? Here is my definition of set equality again:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)

& ALL(a):[a in dom => f1(a) in cod]
& ALL(a):[a in dom => f2(a) in cod]

=> [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

Compare and contrast with:

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
--Terence Tao, "Analysis I," p. 51

Nothing about a "unique" domain or codomain. That would be silly.

*********************************************************************
My definition of a function:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(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]]]]

Compare and contrast with Tao's definition:

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p. 49

FIRST, he specifies sets X and Y and predicate P. (I use graph set G = { (a, b) : a in X & b in Y & P(a, b) }.)

Only then does he introduce the function f. And the definition is NOT applicable for elements outside of the domain X. (Yes, I know, there go your "dark elements." There, there, 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

The inconsistency was derived from the function equality axiom,
I didn't use some of your other crazy axioms. Whats wrong with you?
Why do you start citing Terrence Tao and talking about your other crazies?

Here is the proof again, do you see your other crazies?

146 f1=f2 & ~f1=f2
Join, 65, 145

------------------------------------ cut here ---------------------------------------------

1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Fn Equality

2 ~0=1
Axiom

3 f1(0)=0
Axiom

4 f2(0)=1
Axiom

5 ALL(x):[x ε dom <=> x=0]
Axiom

6 ALL(x):~x ε dom2
Axiom

7 ALL(y):[y ε cod <=> y=0 | y=1]
Axiom

8 Set(dom)
Axiom

9 Set(dom2)
Axiom

10 Set(cod)
Axiom

11 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Fn Equality

12 ALL(cod):ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 11

13 ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 12

14 ALL(f2):[Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
U Spec, 13

15 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]
U Spec, 14

16 EXIST(a):[a ε dom2 & ~f2(a) ε cod]
Premise

17 u ε dom2 & ~f2(u) ε cod
E Spec, 16

18 ~u ε dom2
U Spec, 6

19 u ε dom2
Split, 17

20 ~f2(u) ε cod
Split, 17

21 u ε dom2 & ~u ε dom2
Join, 19, 18

22 ~EXIST(a):[a ε dom2 & ~f2(a) ε cod]
Conclusion, 16

23 ~~ALL(a):~[a ε dom2 & ~f2(a) ε cod]
Quant, 22

24 ALL(a):~[a ε dom2 & ~f2(a) ε cod]
Rem DNeg, 23

25 ALL(a):~~[~a ε dom2 | ~~f2(a) ε cod]
DeMorgan, 24

26 ALL(a):[~a ε dom2 | ~~f2(a) ε cod]
Rem DNeg, 25

27 ALL(a):[~a ε dom2 | f2(a) ε cod]
Rem DNeg, 26

28 ALL(a):[~~a ε dom2 => f2(a) ε cod]
Imply-Or, 27

29 ALL(a):[a ε dom2 => f2(a) ε cod]
Rem DNeg, 28

30 EXIST(a):[a ε dom2 & ~f1(a) ε cod]
Premise

31 u ε dom2 & ~f1(u) ε cod
E Spec, 30

32 u ε dom2
Split, 31

33 ~f1(u) ε cod
Split, 31

34 ~u ε dom2
U Spec, 6

35 u ε dom2 & ~u ε dom2
Join, 32, 34

36 ~EXIST(a):[a ε dom2 & ~f1(a) ε cod]
Conclusion, 30

37 ~~ALL(a):~[a ε dom2 & ~f1(a) ε cod]
Quant, 36

38 ALL(a):~[a ε dom2 & ~f1(a) ε cod]
Rem DNeg, 37

39 ALL(a):~~[~a ε dom2 | ~~f1(a) ε cod]
DeMorgan, 38

40 ALL(a):[~a ε dom2 | ~~f1(a) ε cod]
Rem DNeg, 39

41 ALL(a):[~a ε dom2 | f1(a) ε cod]
Rem DNeg, 40

42 ALL(a):[~~a ε dom2 => f1(a) ε cod]
Imply-Or, 41

43 ALL(a):[a ε dom2 => f1(a) ε cod]
Rem DNeg, 42

44 Set(dom2) & Set(cod)
Join, 9, 10

45 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
Join, 44, 43

46 Set(dom2) & Set(cod)
& ALL(a):[a ε dom2 => f1(a) ε cod]
& ALL(a):[a ε dom2 => f2(a) ε cod]
Join, 45, 29

47 f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]
Detach, 15, 46

48 [f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]]
& [ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2]
Iff-And, 47

49 f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]
Split, 48

50 ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2
Split, 48

51 EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
Premise

52 u ε dom2 & ~f1(u)=f2(u)
E Spec, 51

53 u ε dom2
Split, 52

54 ~f1(u)=f2(u)
Split, 52

55 ~u ε dom2
U Spec, 6

56 u ε dom2 & ~u ε dom2
Join, 53, 55

57 ~EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
Conclusion, 51

58 ~~ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
Quant, 57

59 ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
Rem DNeg, 58

60 ALL(a):~~[~a ε dom2 | ~~f1(a)=f2(a)]
DeMorgan, 59

61 ALL(a):[~a ε dom2 | ~~f1(a)=f2(a)]
Rem DNeg, 60

62 ALL(a):[~a ε dom2 | f1(a)=f2(a)]
Rem DNeg, 61

63 ALL(a):[~~a ε dom2 => f1(a)=f2(a)]
Imply-Or, 62

64 ALL(a):[a ε dom2 => f1(a)=f2(a)]
Rem DNeg, 63

65 f1=f2
Detach, 50, 64

66 ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 1

67 ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 66

68 ALL(f2):[Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
U Spec, 67

69 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]
U Spec, 68

70 EXIST(a):[a ε dom & ~f1(a) ε cod]
Premise

71 u ε dom & ~f1(u) ε cod
E Spec, 70

72 u ε dom <=> u=0
U Spec, 5

73 [u ε dom => u=0] & [u=0 => u ε dom]
Iff-And, 72

74 u ε dom => u=0
Split, 73

75 u=0 => u ε dom
Split, 73

76 u ε dom
Split, 71

77 ~f1(u) ε cod
Split, 71

78 u=0
Detach, 74, 76

79 ~f1(0) ε cod
Substitute, 78, 77

80 ~0 ε cod
Substitute, 3, 79

81 0 ε cod <=> 0=0 | 0=1
U Spec, 7

82 [0 ε cod => 0=0 | 0=1] & [0=0 | 0=1 => 0 ε cod]
Iff-And, 81

83 0 ε cod => 0=0 | 0=1
Split, 82

84 0=0 | 0=1 => 0 ε cod
Split, 82

85 0=0
Reflex

86 0=0 | 0=1
Arb Or, 85

87 0 ε cod
Detach, 84, 86

88 ~0 ε cod & 0 ε cod
Join, 80, 87

89 ~EXIST(a):[a ε dom & ~f1(a) ε cod]
Conclusion, 70

90 ~~ALL(a):~[a ε dom & ~f1(a) ε cod]
Quant, 89

91 ALL(a):~[a ε dom & ~f1(a) ε cod]
Rem DNeg, 90

92 ALL(a):~~[~a ε dom | ~~f1(a) ε cod]
DeMorgan, 91

93 ALL(a):[~a ε dom | ~~f1(a) ε cod]
Rem DNeg, 92

94 ALL(a):[~a ε dom | f1(a) ε cod]
Rem DNeg, 93

95 ALL(a):[~~a ε dom => f1(a) ε cod]
Imply-Or, 94

96 ALL(a):[a ε dom => f1(a) ε cod]
Rem DNeg, 95

97 EXIST(a):[a ε dom & ~f2(a) ε cod]
Premise

98 u ε dom & ~f2(u) ε cod
E Spec, 97

99 u ε dom
Split, 98

100 ~f2(u) ε cod
Split, 98

101 u ε dom <=> u=0
U Spec, 5

102 [u ε dom => u=0] & [u=0 => u ε dom]
Iff-And, 101

103 u ε dom => u=0
Split, 102

104 u=0 => u ε dom
Split, 102

105 u=0
Detach, 103, 99

106 ~f2(0) ε cod
Substitute, 105, 100

107 ~1 ε cod
Substitute, 4, 106

108 1 ε cod <=> 1=0 | 1=1
U Spec, 7

109 [1 ε cod => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε cod]
Iff-And, 108

110 1 ε cod => 1=0 | 1=1
Split, 109

111 1=0 | 1=1 => 1 ε cod
Split, 109

112 1=1
Reflex

113 1=0 | 1=1
Arb Or, 112

114 1 ε cod
Detach, 111, 113

115 ~1 ε cod & 1 ε cod
Join, 107, 114

116 ~EXIST(a):[a ε dom & ~f2(a) ε cod]
Conclusion, 97

117 ~~ALL(a):~[a ε dom & ~f2(a) ε cod]
Quant, 116

118 ALL(a):~[a ε dom & ~f2(a) ε cod]
Rem DNeg, 117

119 ALL(a):~~[~a ε dom | ~~f2(a) ε cod]
DeMorgan, 118

120 ALL(a):[~a ε dom | ~~f2(a) ε cod]
Rem DNeg, 119

121 ALL(a):[~a ε dom | f2(a) ε cod]
Rem DNeg, 120

122 ALL(a):[~~a ε dom => f2(a) ε cod]
Imply-Or, 121

123 ALL(a):[a ε dom => f2(a) ε cod]
Rem DNeg, 122

124 Set(dom) & Set(cod)
Join, 8, 10

125 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
Join, 124, 96

126 Set(dom) & Set(cod)
& ALL(a):[a ε dom => f1(a) ε cod]
& ALL(a):[a ε dom => f2(a) ε cod]
Join, 125, 123

127 f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]
Detach, 69, 126

128 [f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]]
& [ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2]
Iff-And, 127

129 f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]
Split, 128

130 ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2
Split, 128

131 ~ALL(a):[a ε dom => f1(a)=f2(a)] => ~f1=f2
Contra, 129

132 ALL(a):[a ε dom => f1(a)=f2(a)]
Premise

133 0 ε dom => f1(0)=f2(0)
U Spec, 132

134 0 ε dom <=> 0=0
U Spec, 5

135 [0 ε dom => 0=0] & [0=0 => 0 ε dom]
Iff-And, 134

And to the best of my knowledge Terrrence Tao uses
THE in function equality:

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y
with THE same domain and range are said to be equal, f = g, if
and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values
of x, but not others, then we do not consider f andg to be equal.)"
--Terence Tao, "Analysis I," p. 51

But the above is Bourbaki functions not set theory set-like
functions. You need to use triples (g, A, B) to represent
functions. This was explained to you on MSE, and also

here on sci.logic many times. In Bourbaki this here:

f : X -> Y

Is not a notation for f ∈ Y^X, where Y^X is set exponentaion,
it is rather a statement f = (P, X, Y), where P is what Terrence
Tao introduce as the graph, P ⊆ X x Y.

In set theory you then need to do nothing, function equality
is just triple equality, you dont need a Definition 3.3.7.
Definition 3.3.7 is then a theorem, namely this theorem:

Theorem:
ALL(f):ALL(g):ALL(P):ALL(Q):ALL(X):ALL(Y):[f = (P,X,Y) & g = (Q,X,Y)
=> [f = g <=> ALL(x):ALL(y):[x e X & y e Y => [(x,y) e P <=> (x,y) e Q]]]

If you want to use f(a) notation to formulate the theorem, you
need to define this notation on a Bourbaki triple first.

Mostowski Collapse schrieb am Mittwoch, 20. Juli 2022 um 22:21:07 UTC+2:
> The inconsistency was derived from the function equality axiom,
> I didn't use some of your other crazy axioms. Whats wrong with you?
> Why do you start citing Terrence Tao and talking about your other crazies?
>
> Here is the proof again, do you see your other crazies?
> 146 f1=f2 & ~f1=f2
> Join, 65, 145
> ------------------------------------ cut here ---------------------------------------------
>
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Fn Equality
>
> 2 ~0=1
> Axiom
>
> 3 f1(0)=0
> Axiom
>
> 4 f2(0)=1
> Axiom
>
> 5 ALL(x):[x ε dom <=> x=0]
> Axiom
>
> 6 ALL(x):~x ε dom2
> Axiom
>
> 7 ALL(y):[y ε cod <=> y=0 | y=1]
> Axiom
>
> 8 Set(dom)
> Axiom
>
> 9 Set(dom2)
> Axiom
>
> 10 Set(cod)
> Axiom
> 11 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Fn Equality
>
> 12 ALL(cod):ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> & ALL(a):[a ε dom2 => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
> U Spec, 11
> 13 ALL(f1):ALL(f2):[Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> & ALL(a):[a ε dom2 => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
> U Spec, 12
> 14 ALL(f2):[Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> & ALL(a):[a ε dom2 => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]]
> U Spec, 13
> 15 Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> & ALL(a):[a ε dom2 => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]]
> U Spec, 14
>
> 16 EXIST(a):[a ε dom2 & ~f2(a) ε cod]
> Premise
>
> 17 u ε dom2 & ~f2(u) ε cod
> E Spec, 16
>
> 18 ~u ε dom2
> U Spec, 6
>
> 19 u ε dom2
> Split, 17
>
> 20 ~f2(u) ε cod
> Split, 17
>
> 21 u ε dom2 & ~u ε dom2
> Join, 19, 18
>
> 22 ~EXIST(a):[a ε dom2 & ~f2(a) ε cod]
> Conclusion, 16
>
> 23 ~~ALL(a):~[a ε dom2 & ~f2(a) ε cod]
> Quant, 22
>
> 24 ALL(a):~[a ε dom2 & ~f2(a) ε cod]
> Rem DNeg, 23
>
> 25 ALL(a):~~[~a ε dom2 | ~~f2(a) ε cod]
> DeMorgan, 24
>
> 26 ALL(a):[~a ε dom2 | ~~f2(a) ε cod]
> Rem DNeg, 25
>
> 27 ALL(a):[~a ε dom2 | f2(a) ε cod]
> Rem DNeg, 26
>
> 28 ALL(a):[~~a ε dom2 => f2(a) ε cod]
> Imply-Or, 27
>
> 29 ALL(a):[a ε dom2 => f2(a) ε cod]
> Rem DNeg, 28
>
> 30 EXIST(a):[a ε dom2 & ~f1(a) ε cod]
> Premise
>
> 31 u ε dom2 & ~f1(u) ε cod
> E Spec, 30
>
> 32 u ε dom2
> Split, 31
>
> 33 ~f1(u) ε cod
> Split, 31
>
> 34 ~u ε dom2
> U Spec, 6
>
> 35 u ε dom2 & ~u ε dom2
> Join, 32, 34
>
> 36 ~EXIST(a):[a ε dom2 & ~f1(a) ε cod]
> Conclusion, 30
>
> 37 ~~ALL(a):~[a ε dom2 & ~f1(a) ε cod]
> Quant, 36
>
> 38 ALL(a):~[a ε dom2 & ~f1(a) ε cod]
> Rem DNeg, 37
>
> 39 ALL(a):~~[~a ε dom2 | ~~f1(a) ε cod]
> DeMorgan, 38
>
> 40 ALL(a):[~a ε dom2 | ~~f1(a) ε cod]
> Rem DNeg, 39
>
> 41 ALL(a):[~a ε dom2 | f1(a) ε cod]
> Rem DNeg, 40
>
> 42 ALL(a):[~~a ε dom2 => f1(a) ε cod]
> Imply-Or, 41
>
> 43 ALL(a):[a ε dom2 => f1(a) ε cod]
> Rem DNeg, 42
>
> 44 Set(dom2) & Set(cod)
> Join, 9, 10
>
> 45 Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> Join, 44, 43
>
> 46 Set(dom2) & Set(cod)
> & ALL(a):[a ε dom2 => f1(a) ε cod]
> & ALL(a):[a ε dom2 => f2(a) ε cod]
> Join, 45, 29
>
> 47 f1=f2 <=> ALL(a):[a ε dom2 => f1(a)=f2(a)]
> Detach, 15, 46
>
> 48 [f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]]
> & [ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2]
> Iff-And, 47
>
> 49 f1=f2 => ALL(a):[a ε dom2 => f1(a)=f2(a)]
> Split, 48
>
> 50 ALL(a):[a ε dom2 => f1(a)=f2(a)] => f1=f2
> Split, 48
>
> 51 EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
> Premise
>
> 52 u ε dom2 & ~f1(u)=f2(u)
> E Spec, 51
>
> 53 u ε dom2
> Split, 52
>
> 54 ~f1(u)=f2(u)
> Split, 52
>
> 55 ~u ε dom2
> U Spec, 6
>
> 56 u ε dom2 & ~u ε dom2
> Join, 53, 55
>
> 57 ~EXIST(a):[a ε dom2 & ~f1(a)=f2(a)]
> Conclusion, 51
>
> 58 ~~ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
> Quant, 57
>
> 59 ALL(a):~[a ε dom2 & ~f1(a)=f2(a)]
> Rem DNeg, 58
>
> 60 ALL(a):~~[~a ε dom2 | ~~f1(a)=f2(a)]
> DeMorgan, 59
>
> 61 ALL(a):[~a ε dom2 | ~~f1(a)=f2(a)]
> Rem DNeg, 60
>
> 62 ALL(a):[~a ε dom2 | f1(a)=f2(a)]
> Rem DNeg, 61
>
> 63 ALL(a):[~~a ε dom2 => f1(a)=f2(a)]
> Imply-Or, 62
>
> 64 ALL(a):[a ε dom2 => f1(a)=f2(a)]
> Rem DNeg, 63
>
> 65 f1=f2
> Detach, 50, 64
> 66 ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> U Spec, 1
> 67 ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> U Spec, 66
> 68 ALL(f2):[Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> U Spec, 67
> 69 Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]
> U Spec, 68
>
> 70 EXIST(a):[a ε dom & ~f1(a) ε cod]
> Premise
>
> 71 u ε dom & ~f1(u) ε cod
> E Spec, 70
>
> 72 u ε dom <=> u=0
> U Spec, 5
>
> 73 [u ε dom => u=0] & [u=0 => u ε dom]
> Iff-And, 72
>
> 74 u ε dom => u=0
> Split, 73
>
> 75 u=0 => u ε dom
> Split, 73
>
> 76 u ε dom
> Split, 71
>
> 77 ~f1(u) ε cod
> Split, 71
>
> 78 u=0
> Detach, 74, 76
>
> 79 ~f1(0) ε cod
> Substitute, 78, 77
>
> 80 ~0 ε cod
> Substitute, 3, 79
>
> 81 0 ε cod <=> 0=0 | 0=1
> U Spec, 7
>
> 82 [0 ε cod => 0=0 | 0=1] & [0=0 | 0=1 => 0 ε cod]
> Iff-And, 81
>
> 83 0 ε cod => 0=0 | 0=1
> Split, 82
>
> 84 0=0 | 0=1 => 0 ε cod
> Split, 82
>
> 85 0=0
> Reflex
>
> 86 0=0 | 0=1
> Arb Or, 85
>
> 87 0 ε cod
> Detach, 84, 86
>
> 88 ~0 ε cod & 0 ε cod
> Join, 80, 87
>
> 89 ~EXIST(a):[a ε dom & ~f1(a) ε cod]
> Conclusion, 70
>
> 90 ~~ALL(a):~[a ε dom & ~f1(a) ε cod]
> Quant, 89
>
> 91 ALL(a):~[a ε dom & ~f1(a) ε cod]
> Rem DNeg, 90
>
> 92 ALL(a):~~[~a ε dom | ~~f1(a) ε cod]
> DeMorgan, 91
>
> 93 ALL(a):[~a ε dom | ~~f1(a) ε cod]
> Rem DNeg, 92
>
> 94 ALL(a):[~a ε dom | f1(a) ε cod]
> Rem DNeg, 93
>
> 95 ALL(a):[~~a ε dom => f1(a) ε cod]
> Imply-Or, 94
>
> 96 ALL(a):[a ε dom => f1(a) ε cod]
> Rem DNeg, 95
>
> 97 EXIST(a):[a ε dom & ~f2(a) ε cod]
> Premise
>
> 98 u ε dom & ~f2(u) ε cod
> E Spec, 97
>
> 99 u ε dom
> Split, 98
>
> 100 ~f2(u) ε cod
> Split, 98
>
> 101 u ε dom <=> u=0
> U Spec, 5
>
> 102 [u ε dom => u=0] & [u=0 => u ε dom]
> Iff-And, 101
>
> 103 u ε dom => u=0
> Split, 102
>
> 104 u=0 => u ε dom
> Split, 102
>
> 105 u=0
> Detach, 103, 99
>
> 106 ~f2(0) ε cod
> Substitute, 105, 100
>
> 107 ~1 ε cod
> Substitute, 4, 106
>
> 108 1 ε cod <=> 1=0 | 1=1
> U Spec, 7
>
> 109 [1 ε cod => 1=0 | 1=1] & [1=0 | 1=1 => 1 ε cod]
> Iff-And, 108
>
> 110 1 ε cod => 1=0 | 1=1
> Split, 109
>
> 111 1=0 | 1=1 => 1 ε cod
> Split, 109
>
> 112 1=1
> Reflex
>
> 113 1=0 | 1=1
> Arb Or, 112
>
> 114 1 ε cod
> Detach, 111, 113
>
> 115 ~1 ε cod & 1 ε cod
> Join, 107, 114
>
> 116 ~EXIST(a):[a ε dom & ~f2(a) ε cod]
> Conclusion, 97
>
> 117 ~~ALL(a):~[a ε dom & ~f2(a) ε cod]
> Quant, 116
>
> 118 ALL(a):~[a ε dom & ~f2(a) ε cod]
> Rem DNeg, 117
>
> 119 ALL(a):~~[~a ε dom | ~~f2(a) ε cod]
> DeMorgan, 118
>
> 120 ALL(a):[~a ε dom | ~~f2(a) ε cod]
> Rem DNeg, 119
>
> 121 ALL(a):[~a ε dom | f2(a) ε cod]
> Rem DNeg, 120
>
> 122 ALL(a):[~~a ε dom => f2(a) ε cod]
> Imply-Or, 121
>
> 123 ALL(a):[a ε dom => f2(a) ε cod]
> Rem DNeg, 122
>
> 124 Set(dom) & Set(cod)
> Join, 8, 10
>
> 125 Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> Join, 124, 96
>
> 126 Set(dom) & Set(cod)
> & ALL(a):[a ε dom => f1(a) ε cod]
> & ALL(a):[a ε dom => f2(a) ε cod]
> Join, 125, 123
>
> 127 f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]
> Detach, 69, 126
>
> 128 [f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]]
> & [ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2]
> Iff-And, 127
>
> 129 f1=f2 => ALL(a):[a ε dom => f1(a)=f2(a)]
> Split, 128
>
> 130 ALL(a):[a ε dom => f1(a)=f2(a)] => f1=f2
> Split, 128
>
> 131 ~ALL(a):[a ε dom => f1(a)=f2(a)] => ~f1=f2
> Contra, 129
>
> 132 ALL(a):[a ε dom => f1(a)=f2(a)]
> Premise
>
> 133 0 ε dom => f1(0)=f2(0)
> U Spec, 132
>
> 134 0 ε dom <=> 0=0
> U Spec, 5
>
> 135 [0 ε dom => 0=0] & [0=0 => 0 ε dom]
> Iff-And, 134
>
> 136 0 ε dom => 0=0
> Split, 135
>
> 137 0=0 => 0 ε dom
> Split, 135
>
> 138 0=0
> Reflex
>
> 139 0 ε dom
> Detach, 137, 138
>
> 140 f1(0)=f2(0)
> Detach, 133, 139
>
> 141 0=f2(0)
> Substitute, 3, 140
>
> 142 0=1
> Substitute, 4, 141
>
> 143 0=1 & ~0=1
> Join, 142, 2
>
> 144 ~ALL(a):[a ε dom => f1(a)=f2(a)]
> Conclusion, 132
>
> 145 ~f1=f2
> Detach, 131, 144
> 146 f1=f2 & ~f1=f2
> Join, 65, 145
> ------------------------------------ cut here ---------------------------------------------
> Dan Christensen schrieb am Mittwoch, 20. Juli 2022 um 22:13:24 UTC+2:
> > On Wednesday, July 20, 2022 at 2:31:16 PM UTC-4, Mostowski Collapse wrote:
> > > There was a thread about Russells definite descriptions,
> > > and how to translate „the X such that Y“, and Dan Christensen
> > > did it wrong, got some like „all X such that Y“
> > >
> > I don't recall the particulars, but I do recall that you ended up looking like a complete idiot, Jan Burse. Why don't you post the link?
> > > Now the same problem again. Terrence Tao uses
> > > phrases such as THE domain or THE codomain, which
> > > you cannot translate into ALL
> > Grasping at straws as always, Jan Burse??? Here is my definition of set equality again:
> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & ALL(a):[a in dom => f1(a) in cod]
> > & ALL(a):[a in dom => f2(a) in cod]
> >
> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> >
> > Compare and contrast with:
> >
> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
> > --Terence Tao, "Analysis I," p. 51
> >
> > Nothing about a "unique" domain or codomain. That would be silly.
> >
> > *********************************************************************
> > My definition of a function:
> > ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(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]]]]
> > Compare and contrast with Tao's definition:
> >
> > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> > --Terence Tao, "Analysis I," p. 49
> >
> > FIRST, he specifies sets X and Y and predicate P. (I use graph set G = { (a, b) : a in X & b in Y & P(a, b) }.)
> >
> > Only then does he introduce the function f. And the definition is NOT applicable for elements outside of the domain X. (Yes, I know, there go your "dark elements." There, there, 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

On Wednesday, July 20, 2022 at 4:37:45 PM UTC-4, Mostowski Collapse wrote:
> And to the best of my knowledge Terrrence Tao uses
> THE in function equality:

So what?

> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y
> with THE same domain and range are said to be equal, f = g, if
> and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values
> of x, but not others, then we do not consider f andg to be equal.)"

You really are getting desperate, Jan Burse! Use here of the indefinite article would be grammatically incorrect.

> --Terence Tao, "Analysis I," p. 51
> But the above is Bourbaki functions not set theory set-like
> functions.

So what? The above is what is actually used in most math textbooks.

> You need to use triples (g, A, B) to represent
> functions.

That just means a function is fully determined by these three components. Change one and you have another function. Sound familiar?

[snip]

> In set theory you then need to do nothing, function equality
> is just triple equality, you dont need a Definition 3.3.7.

Nevertheless, one of top mathematicians of our time uses another system in his university-level textbook. Why do you think that is, Jan Burse?

> Definition 3.3.7 is then a theorem, namely this theorem:
>
> Theorem:
> ALL(f):ALL(g):ALL(P):ALL(Q):ALL(X):ALL(Y):[f = (P,X,Y) & g = (Q,X,Y)
> => [f = g <=> ALL(x):ALL(y):[x e X & y e Y => [(x,y) e P <=> (x,y) e Q]]]
>
> If you want to use f(a) notation to formulate the theorem, you
> need to define this notation on a Bourbaki triple first.

Nonsense.

Dan

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