Dan-O-Matik was talking nonsense (on sci.logic):
> And while Dedekind infinite sets are often mentioned in math
textbooks, the ZFC axioms are seldom if ever mentioned other
than in passing, as I recall.

An example of a simple theorem where you need some ZF axiom is:

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

The above is provable in FOL+ZF.
It is not provable in DC Proof alone.

Additionally assuming f : x -> y for some x,y is
not required to prove it in FOL+ZF. It would be also
nonsense, since the preimage a is not supposed

to be a subset of x. It can be any set a from the
whole universe of discourse. How would this theorem
then work? Well you need something from ZF,

but FOL itself also helps, since one can prove:

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

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 15:21:10 UTC+1:
> Dan-O-Matik was talking nonsense (on sci.logic):
> > And while Dedekind infinite sets are often mentioned in math
> textbooks, the ZFC axioms are seldom if ever mentioned other
> than in passing, as I recall.
>
> An example of a simple theorem where you need some ZF axiom is:
>
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
>
> The above is provable in FOL+ZF.
> It is not provable in DC Proof alone.

I am not suggesting Borel determinancy as an exercise:
“Skolem needed a snack, so he ate enough for an entire wedding party”.
https://golem.ph.utexas.edu/category/2021/07/borel_determinacy_does_not_require_replacement.html

I am myself a little astonished that the basic math
problem needs some axiom? Right? If I have time
I will provide a proof of it using the axiom I have

in mind. I don't know yet how to show that it cannot
be proved without the axiom or a weaker form of it.
But I am assuming I will be not in a hurry since DC

Proof will not be able to prove the same basic math.

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 15:22:44 UTC+1:
> Additionally assuming f : x -> y for some x,y is
> not required to prove it in FOL+ZF. It would be also
> nonsense, since the preimage a is not supposed
>
> to be a subset of x. It can be any set a from the
> whole universe of discourse. How would this theorem
> then work? Well you need something from ZF,
>
> but FOL itself also helps, since one can prove:
>
> ALL(x):EXIST(y):f(x)=y
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 15:21:10 UTC+1:
> > Dan-O-Matik was talking nonsense (on sci.logic):
> > > And while Dedekind infinite sets are often mentioned in math
> > textbooks, the ZFC axioms are seldom if ever mentioned other
> > than in passing, as I recall.
> >
> > An example of a simple theorem where you need some ZF axiom is:
> >
> > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> >
> > The above is provable in FOL+ZF.
> > It is not provable in DC Proof alone.

Now this is like fukushima. I guess Dan-O-Matiks
brain is now melting. We finally found it:

∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
A Dan-O-Matik function is a binary relation iff the domain is the universal class
https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29

We could only chill fukushima, if Dan-O-Matik were
as cool as this man here, who sings many languages:

Alpha Blondy - Jérusalem
https://www.youtube.com/watch?v=WcqK9Ls7Eos

But Dan-O-Matik isn't cool, he doesn't grasp that a FOL
function symbol and a set-like function are not the same.

Actually learning 3 languages would be helpful:
- FOL function symbol
- class-like functions
- set-like functions

Mostowski Collapse schrieb am Freitag, 10. Dezember 2021 um 19:34:00 UTC+1:
> Now this is like fukushima. I guess Dan-O-Matiks
> brain is now melting. We finally found it:
>
> ∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
> A Dan-O-Matik function is a binary relation iff the domain is the universal class
> https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
>
> We could only chill fukushima, if Dan-O-Matik were
> as cool as this man here, who sings many languages:
>
> Alpha Blondy - Jérusalem
> https://www.youtube.com/watch?v=WcqK9Ls7Eos
>
> But Dan-O-Matik isn't cool, he doesn't grasp that a FOL
> function symbol and a set-like function are not the same.

But there is cure, Dan-O-Matik could exercise and get fluent
in all 3 languages by this little booklet:

Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795

Only 20 bucks or so.

Mostowski Collapse schrieb am Freitag, 10. Dezember 2021 um 19:41:41 UTC+1:
> Actually learning 3 languages would be helpful:
> - FOL function symbol
> - class-like functions
> - set-like functions
> Mostowski Collapse schrieb am Freitag, 10. Dezember 2021 um 19:34:00 UTC+1:
> > Now this is like fukushima. I guess Dan-O-Matiks
> > brain is now melting. We finally found it:
> >
> > ∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
> > A Dan-O-Matik function is a binary relation iff the domain is the universal class
> > https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
> >
> > We could only chill fukushima, if Dan-O-Matik were
> > as cool as this man here, who sings many languages:
> >
> > Alpha Blondy - Jérusalem
> > https://www.youtube.com/watch?v=WcqK9Ls7Eos
> >
> > But Dan-O-Matik isn't cool, he doesn't grasp that a FOL
> > function symbol and a set-like function are not the same.

Unfortunately Dan-O-Matik is only genuinely stupid:

Two things are infinite: the universe and human
stupidity; and I’m not sure about th’universe!
- Albert Einstein

Dan-O-Matik even tops that. He still doesn't understand
FOL, and how a FOL function symbol works. A definition def
for A -> B would be WELL DEFINED if we can prove the folllowing:

(*) def(f) & def(g) => f=g

Dan-O-Matik doesn't understand that this is impossible
for FOL function symbols with his serial formula. From
computer science there are ways to fix it.

For example one fix introduces a new symbol undefined ⊥.
We have to assume the universe of discourse is non-empty.
And then uses Dan-O-Matik serial formula:

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

And adds this axiom:

ALL(x):[~x in A => f(x)=⊥]

Now you can prove (*). But most mathematicians do it more
easy, they don't use FOL function symbols, but set like function
symbols, since the domain A is already set like:

ALL(x):[~x in A => ~EXIST(y):(x,y) e f]

For example JavaScript implements undefined ⊥:

Legts get back to the 10 booleans array problem.
Just open any browser, switch to development view,
and enter in the console:

> a=[0,0,0,0,0,0,0,0,0,0];a[10]
undefined

In JavaScript accessing out of bound gives undefined.
There is a bound check, but there is no exception but a
special value.

This is closer to some logical modelling of automated
verification of programs which uses undefined ⊥.

Mostowski Collapse schrieb am Sonntag, 12. Dezember 2021 um 10:40:01 UTC+1:
> Unfortunately Dan-O-Matik is only genuinely stupid:
>
> Two things are infinite: the universe and human
> stupidity; and I’m not sure about th’universe!
> - Albert Einstein
>
> Dan-O-Matik even tops that. He still doesn't understand
> FOL, and how a FOL function symbol works. A definition def
> for A -> B would be WELL DEFINED if we can prove the folllowing:
>
> (*) def(f) & def(g) => f=g
>
> Dan-O-Matik doesn't understand that this is impossible
> for FOL function symbols with his serial formula. From
> computer science there are ways to fix it.
>
> For example one fix introduces a new symbol undefined ⊥.
> We have to assume the universe of discourse is non-empty.
> And then uses Dan-O-Matik serial formula:
>
> ALL(x):[x in A => f(x) in B]
>
> And adds this axiom:
>
> ALL(x):[~x in A => f(x)=⊥]
>
> Now you can prove (*). But most mathematicians do it more
> easy, they don't use FOL function symbols, but set like function
> symbols, since the domain A is already set like:
>
> ALL(x):[~x in A => ~EXIST(y):(x,y) e f]

Corr.: The WELL DEFINED issue arises when for example
A={0} and B={0}, we then want from def(h) <=> h : A -> B:

(*) def(f) & def(g) => f=g

Otherwise issue arises with the collection of functions,
they just become too big if we don't constrain FOL function

symbols outside of the domain.

Mostowski Collapse schrieb am Sonntag, 12. Dezember 2021 um 10:46:41 UTC+1:
> For example JavaScript implements undefined ⊥:
>
> Legts get back to the 10 booleans array problem.
> Just open any browser, switch to development view,
> and enter in the console:
>
> > a=[0,0,0,0,0,0,0,0,0,0];a[10]
> undefined
>
> In JavaScript accessing out of bound gives undefined.
> There is a bound check, but there is no exception but a
> special value.
>
> This is closer to some logical modelling of automated
> verification of programs which uses undefined ⊥.
> Mostowski Collapse schrieb am Sonntag, 12. Dezember 2021 um 10:40:01 UTC+1:
> > Unfortunately Dan-O-Matik is only genuinely stupid:
> >
> > Two things are infinite: the universe and human
> > stupidity; and I’m not sure about th’universe!
> > - Albert Einstein
> >
> > Dan-O-Matik even tops that. He still doesn't understand
> > FOL, and how a FOL function symbol works. A definition def
> > for A -> B would be WELL DEFINED if we can prove the folllowing:
> >
> > (*) def(f) & def(g) => f=g
> >
> > Dan-O-Matik doesn't understand that this is impossible
> > for FOL function symbols with his serial formula. From
> > computer science there are ways to fix it.
> >
> > For example one fix introduces a new symbol undefined ⊥.
> > We have to assume the universe of discourse is non-empty.
> > And then uses Dan-O-Matik serial formula:
> >
> > ALL(x):[x in A => f(x) in B]
> >
> > And adds this axiom:
> >
> > ALL(x):[~x in A => f(x)=⊥]
> >
> > Now you can prove (*). But most mathematicians do it more
> > easy, they don't use FOL function symbols, but set like function
> > symbols, since the domain A is already set like:
> >
> > ALL(x):[~x in A => ~EXIST(y):(x,y) e f]

How would one formulate in DC Proof, which is supposed to
be the tool for mathematics textbooks, the following:

if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined

See also:

Definedness, Solomon Feferman - Dedicated to Alonzo Church
https://math.stanford.edu/~feferman/papers/definedness.pdf

Ha Ha, on page 7:

The axioms DES are of clear philosophical interest, providing one solution
of the familiar puzzles as to how to handle non-referring definite descriptions,
such as in ‘the present king of France is bald’. But they also serve to regulate
the use of mathematical definitions such a lim xn

But Fefi was sloppy, when defining his Impredicative Theory of
Operations and Classes (IOC), at least in this paper in sec 7
there is a blooper, when he says:

Now write: (i) f:(A→B)for∀x∈A(fx∈B)

Thats Dan-O-Matik nonsense! Did he fix that in another
publication? Same problem in Gerhard Jäger, these things
were never really used? Page 6:

(f :a→b) := (∀x∈a)(fx∈b)
https://home.inf.unibe.ch/ltg/publications/2009/jae09b.pdf

But maybe harmless for what they do with it? Fefi only
uses it to express totality over the natural numbers for
his gcd toy example.

Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 22:25:27 UTC+1:
> How would one formulate in DC Proof, which is supposed to
> be the tool for mathematics textbooks, the following:
>
> if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
>
> See also:
>
> Definedness, Solomon Feferman - Dedicated to Alonzo Church
> https://math.stanford.edu/~feferman/papers/definedness.pdf
>
> Ha Ha, on page 7:
>
> The axioms DES are of clear philosophical interest, providing one solution
> of the familiar puzzles as to how to handle non-referring definite descriptions,
> such as in ‘the present king of France is bald’. But they also serve to regulate
> the use of mathematical definitions such a lim xn

On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> How would one formulate in DC Proof, which is supposed to
> be the tool for mathematics textbooks, the following:
>
> if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
>

There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? 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

Why can Terence Tao then prove:

Theorem 10.1.13 (Differential calculus)
(Sum rule) If f and g are differentiable at x0, then f + g is also
differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf

You say this textbook mathematics is not formalizable?

Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > How would one formulate in DC Proof, which is supposed to
> > be the tool for mathematics textbooks, the following:
> >
> > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> >
> There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question.. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? 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

With defined operator ↓, a corollar from the Sum rule:

f′(x) ↓ v g′(x) ↓ => (f + g)′(x) ↓

Or taking contraposition, now talking about undefined:

~ (f + g)′(x) ↓ => ~ f′(x) ↓ v ~ g′(x) ↓

Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 23:37:56 UTC+1:
> Why can Terence Tao then prove:
>
> Theorem 10.1.13 (Differential calculus)
> (Sum rule) If f and g are differentiable at x0, then f + g is also
> differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
>
> You say this textbook mathematics is not formalizable?
> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > How would one formulate in DC Proof, which is supposed to
> > > be the tool for mathematics textbooks, the following:
> > >
> > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > >
> > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? 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 Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:

> You say this textbook mathematics is not formalizable?
> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > How would one formulate in DC Proof, which is supposed to
> > > be the tool for mathematics textbooks, the following:
> > >
> > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > >
> > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...

> Why can Terence Tao then prove:
>
> Theorem 10.1.13 (Differential calculus)
> (Sum rule) If f and g are differentiable at x0, then f + g is also
> differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
>

More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.

Dan

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

Thats not the correct approach in logic. Since Peano, we find something else:

"Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
has the same meaning as the more familiar but ambiguous notation F(x).
For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
See df-fv 5865. In the ASCII (input) representation there are spaces around the
grave accent; there is a single accent when it is used directly, and it is
doubled within comments."
http://us.metamath.org/mpeuni/conventions.html

Metamath can use the same symbol for function F and the function graph F,
in the above F is the same referent. Metamath uses then the empty set as
undefined marker, in case an argument is not in dom(F).

There are even aspects of definite description, F need not be a function graph
per see. They can therefore prove the following definite descriptions theorem.
It is not like in Russell, where we get false, its more we get the defined marker:

/* Provable in Metamath */
~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}

I don't think DC Proof/Donnie Darko has such a maker u:

/* Not Provable in DC Proof with Donnie Darke Function approach */
~ EXISTUNIQUE(x) (a,x) e F => F(a) = u

The Peano apostroph was later adopted by for example Withhead Russell,
Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
Proof with Donnie Darke Function approach is not what is common in logic.

Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
>
> > You say this textbook mathematics is not formalizable?
> > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > How would one formulate in DC Proof, which is supposed to
> > > > be the tool for mathematics textbooks, the following:
> > > >
> > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > >
> > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
>
> > Why can Terence Tao then prove:
> >
> > Theorem 10.1.13 (Differential calculus)
> > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> >
> More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So only ALL(a):[a e x => f(x) e b] , the Donnie Darko approach, like
dark numbers in WM, is just WM with extra steps, not saying
what is f outside of the domain a is not what we do in logic.

Thats just too dark for logic, these dark booleans. LoL

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 08:50:36 UTC+1:
> Thats not the correct approach in logic. Since Peano, we find something else:
>
> "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> has the same meaning as the more familiar but ambiguous notation F(x).
> For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> See df-fv 5865. In the ASCII (input) representation there are spaces around the
> grave accent; there is a single accent when it is used directly, and it is
> doubled within comments."
> http://us.metamath.org/mpeuni/conventions.html
>
> Metamath can use the same symbol for function F and the function graph F,
> in the above F is the same referent. Metamath uses then the empty set as
> undefined marker, in case an argument is not in dom(F).
>
> There are even aspects of definite description, F need not be a function graph
> per see. They can therefore prove the following definite descriptions theorem.
> It is not like in Russell, where we get false, its more we get the defined marker:
>
> /* Provable in Metamath */
> ~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}
>
> I don't think DC Proof/Donnie Darko has such a maker u:
>
> /* Not Provable in DC Proof with Donnie Darke Function approach */
> ~ EXISTUNIQUE(x) (a,x) e F => F(a) = u
>
> The Peano apostroph was later adopted by for example Withhead Russell,
> Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
> Proof with Donnie Darke Function approach is not what is common in logic.
> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> >
> > > You say this textbook mathematics is not formalizable?
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > How would one formulate in DC Proof, which is supposed to
> > > > > be the tool for mathematics textbooks, the following:
> > > > >
> > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > >
> > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> >
> > > Why can Terence Tao then prove:
> > >
> > > Theorem 10.1.13 (Differential calculus)
> > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > >
> > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

The only new development in logic might be these partial function
logics, where we dont need f'x can go back to f(x), but we have
axioms and inference rules for the operator ↓ .

But there is even a simpler approach than using an operator ↓,
one can also use a special value ⊥. DC Proof didn't make any
choice so far, its Function action

postulates same referent f for both the function graph
and the function, but the Function axiom is quite weak:

- It only applies when f is a function graph
- It doesn't say what f(x) should be outside of the domain

This is unlike the f'x approach which allows both. Then the
f(x) approach is less subject to the first problem, but the second
problem is solved in the new f(x) apprach either through

an operator ↓ or a special value ⊥ .

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 08:55:46 UTC+1:
> So only ALL(a):[a e x => f(x) e b] , the Donnie Darko approach, like
> dark numbers in WM, is just WM with extra steps, not saying
> what is f outside of the domain a is not what we do in logic.
>
> Thats just too dark for logic, these dark booleans. LoL
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 08:50:36 UTC+1:
> > Thats not the correct approach in logic. Since Peano, we find something else:
> >
> > "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> > has the same meaning as the more familiar but ambiguous notation F(x).
> > For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> > originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> > p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> > See df-fv 5865. In the ASCII (input) representation there are spaces around the
> > grave accent; there is a single accent when it is used directly, and it is
> > doubled within comments."
> > http://us.metamath.org/mpeuni/conventions.html
> >
> > Metamath can use the same symbol for function F and the function graph F,
> > in the above F is the same referent. Metamath uses then the empty set as
> > undefined marker, in case an argument is not in dom(F).
> >
> > There are even aspects of definite description, F need not be a function graph
> > per see. They can therefore prove the following definite descriptions theorem.
> > It is not like in Russell, where we get false, its more we get the defined marker:
> >
> > /* Provable in Metamath */
> > ~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}
> >
> > I don't think DC Proof/Donnie Darko has such a maker u:
> >
> > /* Not Provable in DC Proof with Donnie Darke Function approach */
> > ~ EXISTUNIQUE(x) (a,x) e F => F(a) = u
> >
> > The Peano apostroph was later adopted by for example Withhead Russell,
> > Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
> > Proof with Donnie Darke Function approach is not what is common in logic.
> > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > You say this textbook mathematics is not formalizable?
> > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > > How would one formulate in DC Proof, which is supposed to
> > > > > > be the tool for mathematics textbooks, the following:
> > > > > >
> > > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > > >
> > > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> > >
> > > > Why can Terence Tao then prove:
> > > >
> > > > Theorem 10.1.13 (Differential calculus)
> > > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > > >
> > > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Then there is a whole field where the underlying logic is changed,
and where the underlying logic is not anymore classical logic,
but where for example 3-valued logic is used.

A prominent example is the SQL database system query language,
which has even an ISO standard. In SQL there is a special value ⊥,
written NULL. But there is also a third truth value.

"Since Null is not a member of any data domain, it is not considered
a "value", but rather a marker (or placeholder) indicating the
undefined value. [...] SQL implements three logical results, so SQL
implementations must provide for a specialized three-valued logic (3VL)."
https://en.wikipedia.org/wiki/Null_%28SQL%29#Comparisons_with_NULL_and_the_three-valued_logic_%283VL%29

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 09:51:46 UTC+1:
> The only new development in logic might be these partial function
> logics, where we dont need f'x can go back to f(x), but we have
> axioms and inference rules for the operator ↓ .
>
> But there is even a simpler approach than using an operator ↓,
> one can also use a special value ⊥. DC Proof didn't make any
> choice so far, its Function action
>
> postulates same referent f for both the function graph
> and the function, but the Function axiom is quite weak:
>
> - It only applies when f is a function graph
> - It doesn't say what f(x) should be outside of the domain
>
> This is unlike the f'x approach which allows both. Then the
> f(x) approach is less subject to the first problem, but the second
> problem is solved in the new f(x) apprach either through
>
> an operator ↓ or a special value ⊥ .
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 08:55:46 UTC+1:
> > So only ALL(a):[a e x => f(x) e b] , the Donnie Darko approach, like
> > dark numbers in WM, is just WM with extra steps, not saying
> > what is f outside of the domain a is not what we do in logic.
> >
> > Thats just too dark for logic, these dark booleans. LoL
> > Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 08:50:36 UTC+1:
> > > Thats not the correct approach in logic. Since Peano, we find something else:
> > >
> > > "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> > > has the same meaning as the more familiar but ambiguous notation F(x)..
> > > For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> > > originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> > > p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> > > See df-fv 5865. In the ASCII (input) representation there are spaces around the
> > > grave accent; there is a single accent when it is used directly, and it is
> > > doubled within comments."
> > > http://us.metamath.org/mpeuni/conventions.html
> > >
> > > Metamath can use the same symbol for function F and the function graph F,
> > > in the above F is the same referent. Metamath uses then the empty set as
> > > undefined marker, in case an argument is not in dom(F).
> > >
> > > There are even aspects of definite description, F need not be a function graph
> > > per see. They can therefore prove the following definite descriptions theorem.
> > > It is not like in Russell, where we get false, its more we get the defined marker:
> > >
> > > /* Provable in Metamath */
> > > ~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}
> > >
> > > I don't think DC Proof/Donnie Darko has such a maker u:
> > >
> > > /* Not Provable in DC Proof with Donnie Darke Function approach */
> > > ~ EXISTUNIQUE(x) (a,x) e F => F(a) = u
> > >
> > > The Peano apostroph was later adopted by for example Withhead Russell,
> > > Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
> > > Proof with Donnie Darke Function approach is not what is common in logic.
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > > > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > You say this textbook mathematics is not formalizable?
> > > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > > > How would one formulate in DC Proof, which is supposed to
> > > > > > > be the tool for mathematics textbooks, the following:
> > > > > > >
> > > > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > > > >
> > > > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> > > >
> > > > > Why can Terence Tao then prove:
> > > > >
> > > > > Theorem 10.1.13 (Differential calculus)
> > > > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > > > >
> > > > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, December 14, 2021 at 2:50:36 AM UTC-5, Mostowski Collapse wrote:

> Proof with Donnie Darke Function approach is not what is common in logic.
> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> >
> > > You say this textbook mathematics is not formalizable?
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > How would one formulate in DC Proof, which is supposed to
> > > > > be the tool for mathematics textbooks, the following:
> > > > >
> > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > >
> > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> >
> > > Why can Terence Tao then prove:
> > >
> > > Theorem 10.1.13 (Differential calculus)
> > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > >
> > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.

> Thats not the correct approach in logic. Since Peano, we find something else:
>
> "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> has the same meaning as the more familiar but ambiguous notation F(x).
> For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> See df-fv 5865. In the ASCII (input) representation there are spaces around the
> grave accent; there is a single accent when it is used directly, and it is
> doubled within comments."
> http://us.metamath.org/mpeuni/conventions.html
>

We still have f(x) being undefined (or meaningless) for x outside the domain of function f. See, for example, Tao's "Analysis I" (quoted here).

Dan

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

Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree
with Terence Tao. When you use a FOL function symbol,
and you only prove:

ALL(a):[x e a => ALL(y):[y e b => [(x,y) e F <=> f(x)=y]]]

Then obviously f(x) for ~(x e a) isn't pinned down. And then
you can for example not replace the EXIST quantfier in the
below, by an EXISTUNIQUE quantifier:

/* Doesn't work with EXISTUNIQUE also as per Terence Tao */
ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]

I am only trying to explain you the basic facts of beginner
mathematics. The metamath page does something different,
it doesn't use two symbols F and f, as in Terence Tao.

With the metamath approach you can prove EXISTUNIQUE.
With the Terence Tao approach you cannot prove
EXISTUNIQUE.

Whats wrong with you?

Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 17:47:14 UTC+1:
> On Tuesday, December 14, 2021 at 2:50:36 AM UTC-5, Mostowski Collapse wrote:
>
> > Proof with Donnie Darke Function approach is not what is common in logic.
> > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > You say this textbook mathematics is not formalizable?
> > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > > How would one formulate in DC Proof, which is supposed to
> > > > > > be the tool for mathematics textbooks, the following:
> > > > > >
> > > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > > >
> > > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> > >
> > > > Why can Terence Tao then prove:
> > > >
> > > > Theorem 10.1.13 (Differential calculus)
> > > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > > >
> > > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > Thats not the correct approach in logic. Since Peano, we find something else:
> >
> > "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> > has the same meaning as the more familiar but ambiguous notation F(x).
> > For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> > originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> > p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> > See df-fv 5865. In the ASCII (input) representation there are spaces around the
> > grave accent; there is a single accent when it is used directly, and it is
> > doubled within comments."
> > http://us.metamath.org/mpeuni/conventions.html
> >
> We still have f(x) being undefined (or meaningless) for x outside the domain of function f. See, for example, Tao's "Analysis I" (quoted here).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

With the metamath approach you can prove EXISTUNIQUE
when the undefined marker is not in the codomain. Its like
here, the undefined marker is supposed to usually

not be used in codomains:

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 10:07:32 UTC+1:
> "Since Null is not a member of any data domain, it is not considered
> a "value", but rather a marker (or placeholder) indicating the
> undefined value. [...]
> https://en.wikipedia.org/wiki/Null_%28SQL%29#Comparisons_with_NULL_and_the_three-valued_logic_%283VL%29
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/JYKAbTdhCAAJ

But since you deal with identity functions, EXISTUNIQUE
will be provable when the undefined marker is not
in the domain, I guess you only look at identity

functions where dom=codom.

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 19:34:07 UTC+1:
> Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree
> with Terence Tao. When you use a FOL function symbol,
> and you only prove:
>
> ALL(a):[x e a => ALL(y):[y e b => [(x,y) e F <=> f(x)=y]]]
>
> Then obviously f(x) for ~(x e a) isn't pinned down. And then
> you can for example not replace the EXIST quantfier in the
> below, by an EXISTUNIQUE quantifier:
>
> /* Doesn't work with EXISTUNIQUE also as per Terence Tao */
> ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
>
> I am only trying to explain you the basic facts of beginner
> mathematics. The metamath page does something different,
> it doesn't use two symbols F and f, as in Terence Tao.
>
> With the metamath approach you can prove EXISTUNIQUE.
> With the Terence Tao approach you cannot prove
> EXISTUNIQUE.
>
> Whats wrong with you?
> Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 17:47:14 UTC+1:
> > On Tuesday, December 14, 2021 at 2:50:36 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Proof with Donnie Darke Function approach is not what is common in logic.
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > > > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > You say this textbook mathematics is not formalizable?
> > > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > > > How would one formulate in DC Proof, which is supposed to
> > > > > > > be the tool for mathematics textbooks, the following:
> > > > > > >
> > > > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > > > >
> > > > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> > > >
> > > > > Why can Terence Tao then prove:
> > > > >
> > > > > Theorem 10.1.13 (Differential calculus)
> > > > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > > > >
> > > > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > > Thats not the correct approach in logic. Since Peano, we find something else:
> > >
> > > "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> > > has the same meaning as the more familiar but ambiguous notation F(x)..
> > > For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> > > originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> > > p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> > > See df-fv 5865. In the ASCII (input) representation there are spaces around the
> > > grave accent; there is a single accent when it is used directly, and it is
> > > doubled within comments."
> > > http://us.metamath.org/mpeuni/conventions.html
> > >
> > We still have f(x) being undefined (or meaningless) for x outside the domain of function f. See, for example, Tao's "Analysis I" (quoted here).
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

So maybe what Fefi (Solom Feferman) explains is the more
cleaner approach. You don't have to fiddle with domains and
codomains, there is only new operator ↓. In the metamath

approach you would require that functions are kind of
normalized, for example that a function f = { ... (x, ⊥) ...}
would be forbidden, whereas a function that doesn't

have the ordered pair (x, ⊥) would be tolerated.

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 19:41:04 UTC+1:
> With the metamath approach you can prove EXISTUNIQUE
> when the undefined marker is not in the codomain. Its like
> here, the undefined marker is supposed to usually
>
> not be used in codomains:
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 10:07:32 UTC+1:
> > "Since Null is not a member of any data domain, it is not considered
> > a "value", but rather a marker (or placeholder) indicating the
> > undefined value. [...]
> > https://en.wikipedia.org/wiki/Null_%28SQL%29#Comparisons_with_NULL_and_the_three-valued_logic_%283VL%29
> https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/JYKAbTdhCAAJ
>
> But since you deal with identity functions, EXISTUNIQUE
> will be provable when the undefined marker is not
> in the domain, I guess you only look at identity
>
> functions where dom=codom.
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 19:34:07 UTC+1:
> > Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree
> > with Terence Tao. When you use a FOL function symbol,
> > and you only prove:
> >
> > ALL(a):[x e a => ALL(y):[y e b => [(x,y) e F <=> f(x)=y]]]
> >
> > Then obviously f(x) for ~(x e a) isn't pinned down. And then
> > you can for example not replace the EXIST quantfier in the
> > below, by an EXISTUNIQUE quantifier:
> >
> > /* Doesn't work with EXISTUNIQUE also as per Terence Tao */
> > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> >
> > I am only trying to explain you the basic facts of beginner
> > mathematics. The metamath page does something different,
> > it doesn't use two symbols F and f, as in Terence Tao.
> >
> > With the metamath approach you can prove EXISTUNIQUE.
> > With the Terence Tao approach you cannot prove
> > EXISTUNIQUE.
> >
> > Whats wrong with you?
> > Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 17:47:14 UTC+1:
> > > On Tuesday, December 14, 2021 at 2:50:36 AM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Proof with Donnie Darke Function approach is not what is common in logic.
> > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:52:45 UTC+1:
> > > > > On Monday, December 13, 2021 at 5:37:56 PM UTC-5, Mostowski Collapse wrote:
> > > > >
> > > > > > You say this textbook mathematics is not formalizable?
> > > > > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 23:33:32 UTC+1:
> > > > > > > On Monday, December 13, 2021 at 4:25:27 PM UTC-5, Mostowski Collapse wrote:
> > > > > > > > How would one formulate in DC Proof, which is supposed to
> > > > > > > > be the tool for mathematics textbooks, the following:
> > > > > > > >
> > > > > > > > if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
> > > > > > > >
> > > > > > > There is no formal notion undefined. You look at the relevant definition and determine whether or not it can be applied to the statement in question. It not, then we say that that it is UNDEFINED (with respect to that definition). Get it, Jan Burse??? Didn't think so. Oh, well...
> > > > >
> > > > > > Why can Terence Tao then prove:
> > > > > >
> > > > > > Theorem 10.1.13 (Differential calculus)
> > > > > > (Sum rule) If f and g are differentiable at x0, then f + g is also
> > > > > > differentiable at x0, and (f + g)′(x0) = f′(x0) + g′(x0).
> > > > > > https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
> > > > > >
> > > > > More grasping at straws, Jan Burse??? What has this got to do functions outside of there domain? Hint: Nothing.
> > > > Thats not the correct approach in logic. Since Peano, we find something else:
> > > >
> > > > "Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
> > > > has the same meaning as the more familiar but ambiguous notation F(x).
> > > > For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
> > > > originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
> > > > p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
> > > > See df-fv 5865. In the ASCII (input) representation there are spaces around the
> > > > grave accent; there is a single accent when it is used directly, and it is
> > > > doubled within comments."
> > > > http://us.metamath.org/mpeuni/conventions.html
> > > >
> > > We still have f(x) being undefined (or meaningless) for x outside the domain of function f. See, for example, Tao's "Analysis I" (quoted here).
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, December 14, 2021 at 1:34:07 PM UTC-5, Mostowski Collapse wrote:
> Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree
> with Terence Tao. When you use a FOL function symbol,
> and you only prove:
>
> ALL(a):[x e a => ALL(y):[y e b => [(x,y) e F <=> f(x)=y]]]
>

Tao actually wrote, as I think every working mathematician would agree, that if you have a binary relation P such such that ALL(a):[a in X => EXIST(b):[b in Y & P(a,b) & ALL(c):[c in Y => [P(a,c) => c=b]]]] then we will have a UNIQUE function f: X --> Y such that ALL(a):ALL(b):[a in X & b in Y => [f(a)=b <=> P(a,b)].

This is consistent with the handling of functions in DC Proof.

Dan

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

The deeper problem is not Terrence Tao versus Dan-O-Matik
versus metamath. In all 3 approaches this here then fails:

/* Not Provable */
ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

Thats very easy to see. Just chew on the downgrade Lemma:

/* Downgrade Lemma */
ALL(b):[b in a => b in c] & ALL(b):[b in c => f(b)=b]] => ALL(b):[b in a => f(b)=b]]

The tree tool of Wolfgang Schwartz can prove it, you
can also prove it with DC Proof, can't you:

/* Encoding E__ stands for _ in _ */
∀x(Exa → Exc), ∀x(Exc → f(x)=x) entails ∀x(Exa → f(x)=x).
https://www.umsu.de/trees/#~6x%28Exa~5Exb%29,~6x%28Exb~5f%28x%29=x%29|=~6x%28Exa~5f%28x%29=x%29

Do you know what it says?
Do you know why it prevents EXISTUNIQUE?