Your silly function axiom doesn't help doing any mathematics.
How you want to formalize this?

if f is differentiable and g is differentiable then (f+g)' = f' + g'

With total FOL function symbols, they have no intrisic property
where they are undefined. You can prove:

/* Provable */
ALL(x):EXIST(y):g(x)=y

But a set-like function is a set-like domain, and this domain cannot
be the universal class, since it is a set, so you have always some
arguments where the function is undefined:

/* Provable, Not Purple Theorem */
EXIST(x):ALL(y):~(x,y) e h

When you do calculus with set-theory differentiation can litterally
become an operator that maps a set-like function f to another
set-like function f'. And then this resulting set-like function f' will

be defined at x, i.e. EXIST(y):(x,y) e f', iff and only f' is differentiable
at x. It will all fit neatly into taking limits etc.. And then you
can formula a theorem that refers to extremly easily differentiable.

NOBODY USES YOUR SILL FUNCTION AXIOM IN MATHEMATICS

Everybody carries on with h, nobody transfers set-like functions
into class-like FOL functions.

Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 20:11:30 UTC+1:
> On Tuesday, December 28, 2021 at 1:48:12 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 16:55:43 UTC+1:
> > > Testing proposed new version of Function Axiom at https://dcproof.com/LeftInverseOfInjectionV3.htm
> > >
> > > Proves the existence of an left inverse of injective functions.
> > >
> > > ALL(x):ALL(y):ALL(f):[Set(x)
> > > & Set(y)
> > > & ALL(c):[c in x => f(c) in y]
> > > & ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]
> > >
> > > => EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
> > > & ALL(a):[a in rf => g(a) in x]
> > > & ALL(a):[a in rf => f(g(a))=a]]]
> > Is this some mathematical conceptualism joke again.
> > You are still flogging the dead horse of transfering a set-like
> > function into FOL function symbol which is class-like with
> >
> > domain and codomain V? ...
>
> Thank you for your interest. A pity you can't be bit more specific, Jan Burse. It seems you can't argue with the result or my methods of proof, or point to any supposed errors. Just vague, hand-waving generalities. 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

If you have a set-like function h, you can directly ask whether
it is defined at some argument x, just ask:

EXIST(y):(x,y) e h ?

You don't need to carry around an extra variable that indicates
the domain. set-like functions are extremly economic in reasoning.
This theorem here:

if f is differentiable and g is differentiable then (f+g)' = f' + g'

Translates into:

ALL(x):[EXIST(y):(x,y) e f' & EXIST(y):(x,y) e g' => bla bla]

You only need some macro expansion for f(x)=y into (x,y) e f,
but this can be fully automatized. There are tons of papers that
describe how to do it.

Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 20:22:56 UTC+1:
> Your silly function axiom doesn't help doing any mathematics.
> How you want to formalize this?
>
> if f is differentiable and g is differentiable then (f+g)' = f' + g'
>
> With total FOL function symbols, they have no intrisic property
> where they are undefined. You can prove:
> /* Provable */
> ALL(x):EXIST(y):g(x)=y
> But a set-like function is a set-like domain, and this domain cannot
> be the universal class, since it is a set, so you have always some
> arguments where the function is undefined:
> /* Provable, Not Purple Theorem */
> EXIST(x):ALL(y):~(x,y) e h
> When you do calculus with set-theory differentiation can litterally
> become an operator that maps a set-like function f to another
> set-like function f'. And then this resulting set-like function f' will
>
> be defined at x, i.e. EXIST(y):(x,y) e f', iff and only f' is differentiable
> at x. It will all fit neatly into taking limits etc.. And then you
> can formula a theorem that refers to extremly easily differentiable.
>
> NOBODY USES YOUR SILL FUNCTION AXIOM IN MATHEMATICS
>
> Everybody carries on with h, nobody transfers set-like functions
> into class-like FOL functions.
> Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 20:11:30 UTC+1:
> > On Tuesday, December 28, 2021 at 1:48:12 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 16:55:43 UTC+1:
> > > > Testing proposed new version of Function Axiom at https://dcproof.com/LeftInverseOfInjectionV3.htm
> > > >
> > > > Proves the existence of an left inverse of injective functions.
> > > >
> > > > ALL(x):ALL(y):ALL(f):[Set(x)
> > > > & Set(y)
> > > > & ALL(c):[c in x => f(c) in y]
> > > > & ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]
> > > >
> > > > => EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
> > > > & ALL(a):[a in rf => g(a) in x]
> > > > & ALL(a):[a in rf => f(g(a))=a]]]
> > > Is this some mathematical conceptualism joke again.
> > > You are still flogging the dead horse of transfering a set-like
> > > function into FOL function symbol which is class-like with
> > >
> > > domain and codomain V? ...
> >
> > Thank you for your interest. A pity you can't be bit more specific, Jan Burse. It seems you can't argue with the result or my methods of proof, or point to any supposed errors. Just vague, hand-waving generalities. 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 Tuesday, December 28, 2021 at 2:02:42 PM UTC-5, Mostowski Collapse wrote:

> But most of all formulas don't care if their users make
> unnecessary detours and do not get straight to the point.
> You were not able to demonstrate the theorem
>
> without making use of bizzar set theory, something you
> have accused me of promoting and something you claimed
> isn't used in math textbooks, you have again:
>
> Define: h (subset of rfx)
> 21 Set'(h)
> Split, 20
> 22 ALL(b):ALL(c):[(b,c) e h <=> (b,c) e rfx & f(c)=b]
> Split, 20
>
> So h is the set-like function you have constructed.

h is a set of ordered pairs.

> Why
> do you continue your proof?

While it may be intuitively obvious that h has certain function-like properties, there is no place for "intuitively obvious" arguments in formal proofs. A proof like this is as much a test of your methods of proof as anything else. But you should know this. What is your problem, Jan Burse?

> No need to turn h, a set-like function into g, a FOL function
>

In formal proofs anyway, you can't just wave your hands and jump from "(a, b) in h" to "h(a)=b." Recall that you are only allowed to use a fixed list of explicit axioms, rules and definitions.

> symbol which is class-like with domain and codomain V.

There is no universal set/class V in most math textbooks. Why would I include it DC Proof?

> Whereas you can prove for h, which is set-like, and hence
> the domain is also set-like, and cannot be the universal class:
>
> /* Provable, Not Purple Theorem */
> EXIST(x):ALL(y):~(x,y) e h
>
> On the other hand for g you can prove the contrary:
>
> /* Provable */
> ALL(x):EXIST(y):g(x)=y
>
> So your silly transfer from set-like function h into a FOL function
> symbol which is class-like with domain and codomain V, rips
> it off from its set-like property.
>
> In normal mathematics you don't rip off set-like functions h
> from their Not Purple Theorem. You just carry on with h, and
> write h(x)=y, but you don't do it via your Function Axiom.
>
> Its much much more easier:
>
> "h(x)=y is abbrevation for (x,y) in h"

Nice bit of hand-waving, Jan Burse. When will you learn? You really must formalize this "abbreviating" process as I have done with my Function Axiom.

Dan

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

I nowhere used handwaving. These two are provable,
it says that a set like function cannot have a domain
that is all elements from the domain of discourse:

> /* Provable, Not Purple Theorem */
> EXIST(x):ALL(y):~(x,y) e h

And this here is provable. It says that a FOL function
symbol on the other hand hsa a domain that is
all elements from the domain of discourse:

> /* Provable */
> ALL(x):EXIST(y):g(x)=y

Do you deny these two theorems? They are provable in DC Proof.

Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 20:39:07 UTC+1:
> On Tuesday, December 28, 2021 at 2:02:42 PM UTC-5, Mostowski Collapse wrote:
>
> > But most of all formulas don't care if their users make
> > unnecessary detours and do not get straight to the point.
> > You were not able to demonstrate the theorem
> >
> > without making use of bizzar set theory, something you
> > have accused me of promoting and something you claimed
> > isn't used in math textbooks, you have again:
> >
> > Define: h (subset of rfx)
> > 21 Set'(h)
> > Split, 20
> > 22 ALL(b):ALL(c):[(b,c) e h <=> (b,c) e rfx & f(c)=b]
> > Split, 20
> >
> > So h is the set-like function you have constructed.
> h is a set of ordered pairs.
> > Why
> > do you continue your proof?
> While it may be intuitively obvious that h has certain function-like properties, there is no place for "intuitively obvious" arguments in formal proofs. A proof like this is as much a test of your methods of proof as anything else. But you should know this. What is your problem, Jan Burse?
> > No need to turn h, a set-like function into g, a FOL function
> >
> In formal proofs anyway, you can't just wave your hands and jump from "(a, b) in h" to "h(a)=b." Recall that you are only allowed to use a fixed list of explicit axioms, rules and definitions.
> > symbol which is class-like with domain and codomain V.
> There is no universal set/class V in most math textbooks. Why would I include it DC Proof?
> > Whereas you can prove for h, which is set-like, and hence
> > the domain is also set-like, and cannot be the universal class:
> >
> > /* Provable, Not Purple Theorem */
> > EXIST(x):ALL(y):~(x,y) e h
> >
> > On the other hand for g you can prove the contrary:
> >
> > /* Provable */
> > ALL(x):EXIST(y):g(x)=y
> >
> > So your silly transfer from set-like function h into a FOL function
> > symbol which is class-like with domain and codomain V, rips
> > it off from its set-like property.
> >
> > In normal mathematics you don't rip off set-like functions h
> > from their Not Purple Theorem. You just carry on with h, and
> > write h(x)=y, but you don't do it via your Function Axiom.
> >
> > Its much much more easier:
> >
> > "h(x)=y is abbrevation for (x,y) in h"
> Nice bit of hand-waving, Jan Burse. When will you learn? You really must formalize this "abbreviating" process as I have done with my Function Axiom..
> 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 28, 2021 at 2:55:58 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 20:39:07 UTC+1:
> > On Tuesday, December 28, 2021 at 2:02:42 PM UTC-5, Mostowski Collapse wrote:
> >
> > > But most of all formulas don't care if their users make
> > > unnecessary detours and do not get straight to the point.
> > > You were not able to demonstrate the theorem
> > >
> > > without making use of bizzar set theory, something you
> > > have accused me of promoting and something you claimed
> > > isn't used in math textbooks, you have again:
> > >
> > > Define: h (subset of rfx)
> > > 21 Set'(h)
> > > Split, 20
> > > 22 ALL(b):ALL(c):[(b,c) e h <=> (b,c) e rfx & f(c)=b]
> > > Split, 20
> > >
> > > So h is the set-like function you have constructed.
> > h is a set of ordered pairs.

> > > Why
> > > do you continue your proof?

> > While it may be intuitively obvious that h has certain function-like properties, there is no place for "intuitively obvious" arguments in formal proofs. A proof like this is as much a test of your methods of proof as anything else. But you should know this. What is your problem, Jan Burse?

> > > No need to turn h, a set-like function into g, a FOL function
> > >
> > In formal proofs anyway, you can't just wave your hands and jump from "(a, b) in h" to "h(a)=b." Recall that you are only allowed to use a fixed list of explicit axioms, rules and definitions.

> > > symbol which is class-like with domain and codomain V.

> > There is no universal set/class V in most math textbooks. Why would I include it DC Proof?

> I nowhere used handwaving.

When you talk about "abbreviating" here, you resort to shameless hand-having. The '=' is not just an arbitrary symbol. As an operator, it has very specific properties for substitutions.

> These two are provable,
> it says that a set like function cannot have a domain
> that is all elements from the domain of discourse:

> > /* Provable, Not Purple Theorem */
> > EXIST(x):ALL(y):~(x,y) e h

Cannot be proven in DC Proof since a non-empty universe is not assumed.

> And this here is provable. It says that a FOL function
> symbol on the other hand hsa a domain that is
> all elements from the domain of discourse:

> > /* Provable */
> > ALL(x):EXIST(y):g(x)=y

> Do you deny these two theorems? They are provable in DC Proof.

Hmmm... Let's see your proofs.

Dan

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

Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > /* Provable, Not Purple Theorem */
> > > EXIST(x):ALL(y):~(x,y) e h
> Cannot be proven in DC Proof since a non-empty universe is not assumed.

h is there, the universe is non-empty. Should be easily provable in DC Proof.
Just show that dom(h) all elements from universe of discourse leads to a contradiction.
You did such a proof with your Purple example already. Try harder Dan-O-Matik.

> > > /* Provable */
> > > ALL(x):EXIST(y):g(x)=y
> Hmmm... Let's see your proofs.

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

On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > /* Provable, Not Purple Theorem */
> > > > EXIST(x):ALL(y):~(x,y) e h
> > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> h is there, the universe is non-empty.

So, you cannot prove your claim in DC Proof. Thanks for clearing that up.

> Should be easily provable in DC Proof.
> Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > /* Provable */
> > > > ALL(x):EXIST(y):g(x)=y
> > Hmmm... Let's see your proofs.
> ∀x∃yg(x)=y is valid.
> https://www.umsu.de/trees/#~6x~7yg%28x%29=y

I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.

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, December 29, 2021 at 10:30:22 AM UTC-5, Dan Christensen wrote:
> On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > > /* Provable, Not Purple Theorem */
> > > > > EXIST(x):ALL(y):~(x,y) e h
> > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > h is there, the universe is non-empty.
> So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > Should be easily provable in DC Proof.
> > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > /* Provable */
> > > > > ALL(x):EXIST(y):g(x)=y
> > > Hmmm... Let's see your proofs.
> > ∀x∃yg(x)=y is valid.
> > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.

It seems to me that in your proof generator, all functions are defined on the same unspecified domain, the so-called domain of discussion. Not very useful in mathematics where different functions can have different domains.

> 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, December 29, 2021 at 10:30:22 AM UTC-5, Dan Christensen wrote:
> On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > > /* Provable, Not Purple Theorem */
> > > > > EXIST(x):ALL(y):~(x,y) e h
> > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > h is there, the universe is non-empty.
> So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > Should be easily provable in DC Proof.
> > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > /* Provable */
> > > > > ALL(x):EXIST(y):g(x)=y
> > > Hmmm... Let's see your proofs.
> > ∀x∃yg(x)=y is valid.
> > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.
> 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, December 29, 2021 at 10:30:22 AM UTC-5, Dan Christensen wrote:
> On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > > /* Provable, Not Purple Theorem */
> > > > > EXIST(x):ALL(y):~(x,y) e h
> > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > h is there, the universe is non-empty.
> So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > Should be easily provable in DC Proof.
> > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > /* Provable */
> > > > > ALL(x):EXIST(y):g(x)=y
> > > Hmmm... Let's see your proofs.
> > ∀x∃yg(x)=y is valid.
> > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.

It seems to me that in your proof generator, all functions are IMPLICITLY defined on the same unspecified domain, the so-called domain of discussion. Not very useful in mathematics where different functions can have different domains.

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

Its called domain of discourse, not domain of discussion. And
every unary FOL function symbol f is f : V -> V, where V is the domain
of discourse. So you can prove the following in DC Proof:

/* Provable in DC Proof */
ALL(x):EXIST(y):g(x)=y

I proved this already like a 100-times. Its so easy to prove in DC
Proof. What is new, which I didn't try yet in DC Proof, is this here,
I say its provable in DC Proof by the same methods as your purple proof:

/* Provable in DC Proof, Not Purple Theorem */
EXIST(x):ALL(y):~(x,y) e h

If you tell us these things are "useless" or "wonky", well you
can says so. But are these some reflection on your own DC Proof?
Both are provable in DC Proof.

Dan Christensen schrieb am Mittwoch, 29. Dezember 2021 um 18:27:06 UTC+1:
> On Wednesday, December 29, 2021 at 10:30:22 AM UTC-5, Dan Christensen wrote:
> > On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> > > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > > > /* Provable, Not Purple Theorem */
> > > > > > EXIST(x):ALL(y):~(x,y) e h
> > > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > > h is there, the universe is non-empty.
> > So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > > Should be easily provable in DC Proof.
> > > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > > /* Provable */
> > > > > > ALL(x):EXIST(y):g(x)=y
> > > > Hmmm... Let's see your proofs.
> > > ∀x∃yg(x)=y is valid.
> > > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> > I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.
> > 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, December 29, 2021 at 10:30:22 AM UTC-5, Dan Christensen wrote:
> > On Wednesday, December 29, 2021 at 1:34:28 AM UTC-5, Mostowski Collapse wrote:
> > > Dan Christensen schrieb am Dienstag, 28. Dezember 2021 um 22:41:21 UTC+1:
> > > > > > /* Provable, Not Purple Theorem */
> > > > > > EXIST(x):ALL(y):~(x,y) e h
> > > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > > h is there, the universe is non-empty.
> > So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > > Should be easily provable in DC Proof.
> > > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > > /* Provable */
> > > > > > ALL(x):EXIST(y):g(x)=y
> > > > Hmmm... Let's see your proofs.
> > > ∀x∃yg(x)=y is valid.
> > > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> > I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.
> It seems to me that in your proof generator, all functions are IMPLICITLY defined on the same unspecified domain, the so-called domain of discussion.. Not very useful in mathematics where different functions can have different domains.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 7:17:48 AM UTC-5, Mostowski Collapse wrote:

> > > > > > > /* Provable, Not Purple Theorem */
> > > > > > > EXIST(x):ALL(y):~(x,y) e h
> > > > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > > > h is there, the universe is non-empty.
> > > So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > > > Should be easily provable in DC Proof.
> > > > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > > > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > > > /* Provable */
> > > > > > > ALL(x):EXIST(y):g(x)=y
> > > > > Hmmm... Let's see your proofs.
> > > > ∀x∃yg(x)=y is valid.
> > > > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> > > I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.
> > It seems to me that in your proof generator, all functions are IMPLICITLY defined on the same unspecified domain, the so-called domain of discussion. Not very useful in mathematics where different functions can have different domains.

> Its called domain of discourse, not domain of discussion.And
> every unary FOL function symbol f is f : V -> V, where V is the domain
> of discourse. So you can prove the following in DC Proof:
>
> /* Provable in DC Proof */
> ALL(x):EXIST(y):g(x)=y
>

Wrong.

> /* Provable in DC Proof, Not Purple Theorem */
> EXIST(x):ALL(y):~(x,y) e h

Wrong again, Jan Burse.

Dan

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

Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:

And you get:

1 EXIST(x):ALL(y):~g(x)=y
Premise

2 ALL(y):~g(z)=y
E Spec, 1

3 ~g(z)=g(z)
U Spec, 2, 2

4 g(z)=g(z)
Reflex, 3, 2

5 ~g(z)=g(z) & g(z)=g(z)
Join, 3, 4

6 ~EXIST(g):EXIST(x):ALL(y):~g(x)=y
Conclusion, 1

7 ~~ALL(g):~EXIST(x):ALL(y):~g(x)=y
Quant, 6

8 ALL(g):~EXIST(x):ALL(y):~g(x)=y
Rem DNeg, 7

9 ALL(g):~~ALL(x):~ALL(y):~g(x)=y
Quant, 8

10 ALL(g):ALL(x):~ALL(y):~g(x)=y
Rem DNeg, 9

11 ALL(g):ALL(x):~~EXIST(y):~~g(x)=y
Quant, 10

12 ALL(g):ALL(x):EXIST(y):~~g(x)=y
Rem DNeg, 11

13 ALL(g):ALL(x):EXIST(y):g(x)=y
Rem DNeg, 12

Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 13:58:05 UTC+1:
> On Thursday, December 30, 2021 at 7:17:48 AM UTC-5, Mostowski Collapse wrote:
>
> > > > > > > > /* Provable, Not Purple Theorem */
> > > > > > > > EXIST(x):ALL(y):~(x,y) e h
> > > > > > Cannot be proven in DC Proof since a non-empty universe is not assumed.
> > > > > h is there, the universe is non-empty.
> > > > So, you cannot prove your claim in DC Proof. Thanks for clearing that up.
> > > > > Should be easily provable in DC Proof.
> > > > > Just show that dom(h) all elements from universe of discourse leads to a contradiction.
> > > > > You did such a proof with your Purple example already. Try harder Dan-O-Matik.
> > > > > > > > /* Provable */
> > > > > > > > ALL(x):EXIST(y):g(x)=y
> > > > > > Hmmm... Let's see your proofs.
> > > > > ∀x∃yg(x)=y is valid.
> > > > > https://www.umsu.de/trees/#~6x~7yg%28x%29=y
> > > > I'm sure most mathematician would be left scratching their heads at this wonky result. But thanks for confirming that, contrary to your claim, you cannot derive it in DC Proof. I would be very worried if you could.
> > > It seems to me that in your proof generator, all functions are IMPLICITLY defined on the same unspecified domain, the so-called domain of discussion. Not very useful in mathematics where different functions can have different domains.
> > Its called domain of discourse, not domain of discussion.And
> > every unary FOL function symbol f is f : V -> V, where V is the domain
> > of discourse. So you can prove the following in DC Proof:
> >
> > /* Provable in DC Proof */
> > ALL(x):EXIST(y):g(x)=y
> >
> Wrong.
> > /* Provable in DC Proof, Not Purple Theorem */
> > EXIST(x):ALL(y):~(x,y) e h
> Wrong again, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:
>
> And you get:
>
> 1 EXIST(x):ALL(y):~g(x)=y
> Premise
>
> 2 ALL(y):~g(z)=y
> E Spec, 1
>
> 3 ~g(z)=g(z)
> U Spec, 2, 2
>

Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.

Dan

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

What are the changes in the current version. Do you have
release notes or a change log. Do the old examples all still work?

Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:" rel="nofollow" target="_blank">http://www.dcproof.com/dcpsetup2.exe:
> >
> > And you get:
> >
> > 1 EXIST(x):ALL(y):~g(x)=y
> > Premise
> >
> > 2 ALL(y):~g(z)=y
> > E Spec, 1
> >
> > 3 ~g(z)=g(z)
> > U Spec, 2, 2
> >
> Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 9:10:53 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> > On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:
> > >
> > > And you get:
> > >
> > > 1 EXIST(x):ALL(y):~g(x)=y
> > > Premise
> > >
> > > 2 ALL(y):~g(z)=y
> > > E Spec, 1
> > >
> > > 3 ~g(z)=g(z)
> > > U Spec, 2, 2
> > >
> > Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.

> What are the changes in the current version. Do you have
> release notes or a change log.

No, but we discussed it here at the time. With the change, you can specify "f(x)" in a U Spec or Reflex statement only if a previous statement declared it to be an element of some set.

It looks like you used a partially implemented test version. Were you able to download, install and test the latest version?

> Do the old examples all still work?

Yes. No examples I posted would have used "f(x)" for if f did not have an explicit domain and codomain (as is the practice in textbooks), e.g. ALL(a):[a in dom => f(a) in cod] for sets dom and cod.

Dan

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

On Thursday, December 30, 2021 at 9:48:40 AM UTC-5, Dan Christensen wrote:
> On Thursday, December 30, 2021 at 9:10:53 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> > > On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > > > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:
> > > >
> > > > And you get:
> > > >
> > > > 1 EXIST(x):ALL(y):~g(x)=y
> > > > Premise
> > > >
> > > > 2 ALL(y):~g(z)=y
> > > > E Spec, 1
> > > >
> > > > 3 ~g(z)=g(z)
> > > > U Spec, 2, 2
> > > >
> > > Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.
> > What are the changes in the current version. Do you have
> > release notes or a change log.

> No, but we discussed it here at the time. With the change, you can specify "f(x)" in a U Spec or Reflex statement only if a previous statement declared it to be an element of some set.
>

Maybe I will also need to verify that x is a element of a set?

> It looks like you used a partially implemented test version. Were you able to download, install and test the latest version?
> > Do the old examples all still work?
> Yes. No examples I posted would have used "f(x)" for if f did not have an explicit domain and codomain (as is the practice in textbooks), e.g. ALL(a):[a in dom => f(a) in cod] for sets dom and cod.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan-O-Matik tweaked his prover:
> With the change, you can specify "f(x)" in a U Spec or Reflex statement only
if a previous statement declared it to be an element of some set.

g(z) is element of { g(z) }. So what?

Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 15:48:40 UTC+1:
> On Thursday, December 30, 2021 at 9:10:53 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> > > On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > > > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:" rel="nofollow" target="_blank">http://www.dcproof.com/dcpsetup2.exe:
> > > >
> > > > And you get:
> > > >
> > > > 1 EXIST(x):ALL(y):~g(x)=y
> > > > Premise
> > > >
> > > > 2 ALL(y):~g(z)=y
> > > > E Spec, 1
> > > >
> > > > 3 ~g(z)=g(z)
> > > > U Spec, 2, 2
> > > >
> > > Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.
> > What are the changes in the current version. Do you have
> > release notes or a change log.
> No, but we discussed it here at the time. With the change, you can specify "f(x)" in a U Spec or Reflex statement only if a previous statement declared it to be an element of some set.
>
> It looks like you used a partially implemented test version. Were you able to download, install and test the latest version?
> > Do the old examples all still work?
> Yes. No examples I posted would have used "f(x)" for if f did not have an explicit domain and codomain (as is the practice in textbooks), e.g. ALL(a):[a in dom => f(a) in cod] for sets dom and cod.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Follows from this axiom:
https://en.wikipedia.org/wiki/Axiom_of_pairing

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 18:51:00 UTC+1:
> Dan-O-Matik tweaked his prover:
> > With the change, you can specify "f(x)" in a U Spec or Reflex statement only
> if a previous statement declared it to be an element of some set.
> g(z) is element of { g(z) }. So what?
> Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 15:48:40 UTC+1:
> > On Thursday, December 30, 2021 at 9:10:53 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> > > > On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > > > > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:" rel="nofollow" target="_blank">http://www.dcproof.com/dcpsetup2.exe:
> > > > >
> > > > > And you get:
> > > > >
> > > > > 1 EXIST(x):ALL(y):~g(x)=y
> > > > > Premise
> > > > >
> > > > > 2 ALL(y):~g(z)=y
> > > > > E Spec, 1
> > > > >
> > > > > 3 ~g(z)=g(z)
> > > > > U Spec, 2, 2
> > > > >
> > > > Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.
> > > What are the changes in the current version. Do you have
> > > release notes or a change log.
> > No, but we discussed it here at the time. With the change, you can specify "f(x)" in a U Spec or Reflex statement only if a previous statement declared it to be an element of some set.
> >
> > It looks like you used a partially implemented test version. Were you able to download, install and test the latest version?
> > > Do the old examples all still work?
> > Yes. No examples I posted would have used "f(x)" for if f did not have an explicit domain and codomain (as is the practice in textbooks), e.g. ALL(a):[a in dom => f(a) in cod] for sets dom and cod.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

So you botched DC-Proof? You can not anymore more prove?

ALL(x):[Human(x)=>Mortal(x)]
Human(father(newton))
----------------------------------------------------
Mortal(father(newton))

LMAO!

See also:

∀x(Hx → Mx), Hf(n) entails Mf(n)
https://www.umsu.de/trees/#~6x%28Hx~5Mx%29,Hf%28n%29|=Mf%28n%29

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 18:55:02 UTC+1:
> Follows from this axiom:
> https://en.wikipedia.org/wiki/Axiom_of_pairing
> Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 18:51:00 UTC+1:
> > Dan-O-Matik tweaked his prover:
> > > With the change, you can specify "f(x)" in a U Spec or Reflex statement only
> > if a previous statement declared it to be an element of some set.
> > g(z) is element of { g(z) }. So what?
> > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 15:48:40 UTC+1:
> > > On Thursday, December 30, 2021 at 9:10:53 AM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 14:57:26 UTC+1:
> > > > > On Thursday, December 30, 2021 at 8:34:25 AM UTC-5, Mostowski Collapse wrote:
> > > > > > Come on Dan, use http://www.dcproof.com/dcpsetup2.exe:" rel="nofollow" target="_blank">http://www.dcproof.com/dcpsetup2.exe:
> > > > > >
> > > > > > And you get:
> > > > > >
> > > > > > 1 EXIST(x):ALL(y):~g(x)=y
> > > > > > Premise
> > > > > >
> > > > > > 2 ALL(y):~g(z)=y
> > > > > > E Spec, 1
> > > > > >
> > > > > > 3 ~g(z)=g(z)
> > > > > > U Spec, 2, 2
> > > > > >
> > > > > Not possible in current version (date stamp in About DC Proof = 2019-09-14). Download free update at my homepage.
> > > > What are the changes in the current version. Do you have
> > > > release notes or a change log.
> > > No, but we discussed it here at the time. With the change, you can specify "f(x)" in a U Spec or Reflex statement only if a previous statement declared it to be an element of some set.
> > >
> > > It looks like you used a partially implemented test version. Were you able to download, install and test the latest version?
> > > > Do the old examples all still work?
> > > Yes. No examples I posted would have used "f(x)" for if f did not have an explicit domain and codomain (as is the practice in textbooks), e.g. ALL(a):[a in dom => f(a) in cod] for sets dom and cod.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 12:51:00 PM UTC-5, Mostowski Collapse wrote:

> > With the change, you can specify "f(x)" in a U Spec or Reflex statement only
> if a previous statement declared it to be an element of some set.
> g(z) is element of { g(z) }. So what?

There is no such axiom in DC Proof. You will have to try another approach, 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 Thursday, December 30, 2021 at 1:01:17 PM UTC-5, Mostowski Collapse wrote:

> You can not anymore more prove?
>
> ALL(x):[Human(x)=>Mortal(x)]
> Human(father(newton))
> ----------------------------------------------------
> Mortal(father(newton))
>

Easy.

1. ALL(a):[a in humans => a in mortals]
(Axiom)

2. ALL(a):[a in humans => father(a) in humans]
(Axiom)

3. newton in humans
((Axiom)

4. newton in humans => father(newton) in humans
(U Spec, 2)

5. father(newton) in humans
(Detach, 4, 3)

6. father(newton) in humans => father(newton) in mortals
(U Spec, 1, 5)

7. father(newton) in mortals
(Detach, 6, 5)

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 same. Did you also eradicate predicates or what?

LMAO!

Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 20:18:08 UTC+1:
> On Thursday, December 30, 2021 at 1:01:17 PM UTC-5, Mostowski Collapse wrote:
>
> > You can not anymore more prove?
> >
> > ALL(x):[Human(x)=>Mortal(x)]
> > Human(father(newton))
> > ----------------------------------------------------
> > Mortal(father(newton))
> >
> Easy.
>
> 1. ALL(a):[a in humans => a in mortals]
> (Axiom)
>
> 2. ALL(a):[a in humans => father(a) in humans]
> (Axiom)
>
> 3. newton in humans
> ((Axiom)
>
> 4. newton in humans => father(newton) in humans
> (U Spec, 2)
>
> 5. father(newton) in humans
> (Detach, 4, 3)
>
> 6. father(newton) in humans => father(newton) in mortals
> (U Spec, 1, 5)
>
> 7. father(newton) in mortals
> (Detach, 6, 5)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 2:42:10 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 20:18:08 UTC+1:
> > On Thursday, December 30, 2021 at 1:01:17 PM UTC-5, Mostowski Collapse wrote:
> >
> > > You can not anymore more prove?
> > >
> > > ALL(x):[Human(x)=>Mortal(x)]
> > > Human(father(newton))
> > > ----------------------------------------------------
> > > Mortal(father(newton))
> > >
> > Easy.
> >
> > 1. ALL(a):[a in humans => a in mortals]
> > (Axiom)
> >
> > 2. ALL(a):[a in humans => father(a) in humans]
> > (Axiom)
> >
> > 3. newton in humans
> > ((Axiom)
> >
> > 4. newton in humans => father(newton) in humans
> > (U Spec, 2)
> >
> > 5. father(newton) in humans
> > (Detach, 4, 3)
> >
> > 6. father(newton) in humans => father(newton) in mortals
> > (U Spec, 1, 5)
> >
> > 7. father(newton) in mortals
> > (Detach, 6, 5)

> Thats not same. Did you also eradicate predicates or what?
>

Geez, yer dumb!

What if I want to prove:

ALL(x):[Human(x)=>Mortal(x)]
~Mortal(father(newton))
----------------------------------------------------
~Human(father(newton))

Do you claim ~x e A implies x e B for some B?

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 20:42:10 UTC+1:
> Thats not same. Did you also eradicate predicates or what?
>
> LMAO!
> Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 20:18:08 UTC+1:
> > On Thursday, December 30, 2021 at 1:01:17 PM UTC-5, Mostowski Collapse wrote:
> >
> > > You can not anymore more prove?
> > >
> > > ALL(x):[Human(x)=>Mortal(x)]
> > > Human(father(newton))
> > > ----------------------------------------------------
> > > Mortal(father(newton))
> > >
> > Easy.
> >
> > 1. ALL(a):[a in humans => a in mortals]
> > (Axiom)
> >
> > 2. ALL(a):[a in humans => father(a) in humans]
> > (Axiom)
> >
> > 3. newton in humans
> > ((Axiom)
> >
> > 4. newton in humans => father(newton) in humans
> > (U Spec, 2)
> >
> > 5. father(newton) in humans
> > (Detach, 4, 3)
> >
> > 6. father(newton) in humans => father(newton) in mortals
> > (U Spec, 1, 5)
> >
> > 7. father(newton) in mortals
> > (Detach, 6, 5)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Also you invented premisses that I never stated, such as
Human(newton), or ALL(x):[Human(x)=>Human(father(x))]
translated to sets. Where do you see these premisses here?

ALL(x):[Human(x)=>Mortal(x)]
Human(father(newton))
----------------------------------------------------
Mortal(father(newton))

Admit it, you botched DC proof, its not anymore a usable tool
for first order logic. It works for some pyschotic Dan-O-Matik
logic, only this logic is nowhere documented. There is

no change log on your web site.

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 20:44:55 UTC+1:
> What if I want to prove:
>
> ALL(x):[Human(x)=>Mortal(x)]
> ~Mortal(father(newton))
> ----------------------------------------------------
> ~Human(father(newton))
>
> Do you claim ~x e A implies x e B for some B?
> Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 20:42:10 UTC+1:
> > Thats not same. Did you also eradicate predicates or what?
> >
> > LMAO!
> > Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 20:18:08 UTC+1:
> > > On Thursday, December 30, 2021 at 1:01:17 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > You can not anymore more prove?
> > > >
> > > > ALL(x):[Human(x)=>Mortal(x)]
> > > > Human(father(newton))
> > > > ----------------------------------------------------
> > > > Mortal(father(newton))
> > > >
> > > Easy.
> > >
> > > 1. ALL(a):[a in humans => a in mortals]
> > > (Axiom)
> > >
> > > 2. ALL(a):[a in humans => father(a) in humans]
> > > (Axiom)
> > >
> > > 3. newton in humans
> > > ((Axiom)
> > >
> > > 4. newton in humans => father(newton) in humans
> > > (U Spec, 2)
> > >
> > > 5. father(newton) in humans
> > > (Detach, 4, 3)
> > >
> > > 6. father(newton) in humans => father(newton) in mortals
> > > (U Spec, 1, 5)
> > >
> > > 7. father(newton) in mortals
> > > (Detach, 6, 5)
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com