Here is a very simple, even trivial example of a formal proof of the existence of a function using DC Proof. We formally prove the existence of the identity function on any given set:

ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]

https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)

Dan

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

How many identity functions "id : a -> a, id(x)=x" do you get for a
certain a using your translation of "id : a -> a, id(x)=x"?

Can you prove the following:
"id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2

I dont think your translation ALL(b):[b in a => f(b)=b]] is correct,
since you will not be able to prove the above.

Here is a counter model:

∀b(Eba → f(b)=b), ∀b(Eba → g(b)=b) does not entail ∀c∀d(f(c)=d ↔ g(c)=d).
Countermodel:
Domain: { 0, 1 }
a: 0
f: { (0,0), (1,1) }
g: { (0,1), (1,1) }
E: { }

Dan Christensen schrieb am Montag, 13. Dezember 2021 um 07:05:10 UTC+1:
> Here is a very simple, even trivial example of a formal proof of the existence of a function using DC Proof. We formally prove the existence of the identity function on any given set:
>
> ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
>
> https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

This shows that you will not be able to prove:

ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

But the notion of identity function is mostly considered WELL
DEFINED. No black booleans. Its just the set of ordered pairs:

id = { (x,x) | x e a }

Is this one of your WM with extra steps posts again?

Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 10:39:47 UTC+1:
> How many identity functions "id : a -> a, id(x)=x" do you get for a
> certain a using your translation of "id : a -> a, id(x)=x"?
>
> Can you prove the following:
> "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
>
> I dont think your translation ALL(b):[b in a => f(b)=b]] is correct,
> since you will not be able to prove the above.
>
> Here is a counter model:
>
> ∀b(Eba → f(b)=b), ∀b(Eba → g(b)=b) does not entail ∀c∀d(f(c)=d ↔ g(c)=d).
> Countermodel:
> Domain: { 0, 1 }
> a: 0
> f: { (0,0), (1,1) }
> g: { (0,1), (1,1) }
> E: { }
> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 07:05:10 UTC+1:
> > Here is a very simple, even trivial example of a formal proof of the existence of a function using DC Proof. We formally prove the existence of the identity function on any given set:
> >
> > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> >
> > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Did Norman Megill (1950-2021) see your posts and got a
stroke, since all his endeavours into metamath seem futil,
since there are still morons like Dan-O-Matik out in the wild?

You can also lookup metamath how function application
is defined, and how they will have advantage that they can
indeed prove uniqueness of certain set-like functions

despite keeping a syntax f(a). Especially their HTML renderer
shows f(a) but under the hood its something more complicated,
so that many of the Dan-O-Matik anomalies dont happen.

Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 10:40:45 UTC+1:
> This shows that you will not be able to prove:
>
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>
> But the notion of identity function is mostly considered WELL
> DEFINED. No black booleans. Its just the set of ordered pairs:
>
> id = { (x,x) | x e a }
>
> Is this one of your WM with extra steps posts again?
> Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 10:39:47 UTC+1:
> > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > certain a using your translation of "id : a -> a, id(x)=x"?
> >
> > Can you prove the following:
> > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> >
> > I dont think your translation ALL(b):[b in a => f(b)=b]] is correct,
> > since you will not be able to prove the above.
> >
> > Here is a counter model:
> >
> > ∀b(Eba → f(b)=b), ∀b(Eba → g(b)=b) does not entail ∀c∀d(f(c)=d ↔ g(c)=d).
> > Countermodel:
> > Domain: { 0, 1 }
> > a: 0
> > f: { (0,0), (1,1) }
> > g: { (0,1), (1,1) }
> > E: { }
> > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 07:05:10 UTC+1:
> > > Here is a very simple, even trivial example of a formal proof of the existence of a function using DC Proof. We formally prove the existence of the identity function on any given set:
> > >
> > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > >
> > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> > >
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

But the sad thing about metamath, half of the deciples
are ultra morons, like David A. Wheeler and Mario Carneiro.
The blocked me on metamath google groups, exactly

when I was discussing something about their function
application. I had some doubts about whether metamath
has a FOL kernel, because some issues with function arity.

Basically a set like function can be polymorphic in the
number of arguments. You could have f = { (0,0), (0,0,0) }
so something like a binary and ternary function at the

same time. This is not standard FOL, where arities are
separated. Each function symbol has its fixed arity. There
is the same bug in DC Proof you can also enter:

1 ALL(x):ALL(y):[f(x)=y <=> f(x,x)=y]
Axiom

On the other hand the tree tool by Wolfgang Schwartz
does it correctly as in standard FOL:

∀x∀y(f(x)=y ↔ f(x,x)=y)
https://www.umsu.de/trees/#~6x~6y%28f%28x%29=y~4f%28x,x%29=y%29
Error message:
Don't use 'f' as both 1-ary function symbol and 2-ary function symbol.
(I'm assuming '=f(x,x)y' is meant to be an atomic formula with predicate '='.)

Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 11:38:25 UTC+1:
> Did Norman Megill (1950-2021) see your posts and got a
> stroke, since all his endeavours into metamath seem futil,
> since there are still morons like Dan-O-Matik out in the wild?
>
> You can also lookup metamath how function application
> is defined, and how they will have advantage that they can
> indeed prove uniqueness of certain set-like functions
>
> despite keeping a syntax f(a). Especially their HTML renderer
> shows f(a) but under the hood its something more complicated,
> so that many of the Dan-O-Matik anomalies dont happen.
> Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 10:40:45 UTC+1:
> > This shows that you will not be able to prove:
> >
> > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> >
> > But the notion of identity function is mostly considered WELL
> > DEFINED. No black booleans. Its just the set of ordered pairs:
> >
> > id = { (x,x) | x e a }
> >
> > Is this one of your WM with extra steps posts again?
> > Mostowski Collapse schrieb am Montag, 13. Dezember 2021 um 10:39:47 UTC+1:
> > > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > > certain a using your translation of "id : a -> a, id(x)=x"?
> > >
> > > Can you prove the following:
> > > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> > >
> > > I dont think your translation ALL(b):[b in a => f(b)=b]] is correct,
> > > since you will not be able to prove the above.
> > >
> > > Here is a counter model:
> > >
> > > ∀b(Eba → f(b)=b), ∀b(Eba → g(b)=b) does not entail ∀c∀d(f(c)=d ↔ g(c)=d).
> > > Countermodel:
> > > Domain: { 0, 1 }
> > > a: 0
> > > f: { (0,0), (1,1) }
> > > g: { (0,1), (1,1) }
> > > E: { }
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 07:05:10 UTC+1:
> > > > Here is a very simple, even trivial example of a formal proof of the existence of a function using DC Proof. We formally prove the existence of the identity function on any given set:
> > > >
> > > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > > >
> > > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> > > >
> > > > 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 4:39:47 AM UTC-5, Mostowski Collapse wrote:
> How many identity functions "id : a -> a, id(x)=x" do you get for a
> certain a using your translation of "id : a -> a, id(x)=x"?
>
> Can you prove the following:
> "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
>

The identity functions on any given set are identical.

Formal Proof:

1. Set(x)
Premise

2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
Premise

3. ALL(a):[a in x => f(a)=a]
Split, 2

4. ALL(a):[a in x => g(a)=a]
Split, 2

5. y in x
Premise

6. y in x => f(y)=y
U Spec, 3

7. f(y)=y
Detach, 6, 5

8. y in x => g(y)=y
U Spec, 4

9. g(y)=y
Detach, 8, 5

10. f(y)=g(y)
Substitute, 9, 7

11. ALL(a):[a in x => f(a)=g(a)]
Conclusion, 5

12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
=> ALL(a):[a in x => f(a)=g(a)]]
Conclusion, 2

As required:

13. ALL(x):[Set(x)
=> ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
=> ALL(a):[a in x => f(a)=g(a)]]]
Conclusion, 1

Dan

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

This here doesn't say f=g:

ALL(a):[a in x => f(a)=g(a)]]]

It only says f|a = g|a, i.e. the restriction of f to a is
the same as the restriction of g to a.

Question was why cant you prove:

ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

Why cant you prove it? Why are there so many
identity functions. Are there dark booleans?

Dan Christensen schrieb am Montag, 13. Dezember 2021 um 15:41:31 UTC+1:
> On Monday, December 13, 2021 at 4:39:47 AM UTC-5, Mostowski Collapse wrote:
> > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > certain a using your translation of "id : a -> a, id(x)=x"?
> >
> > Can you prove the following:
> > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> >
> The identity functions on any given set are identical.
>
> Formal Proof:
>
> 1. Set(x)
> Premise
>
> 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> Premise
>
> 3. ALL(a):[a in x => f(a)=a]
> Split, 2
>
> 4. ALL(a):[a in x => g(a)=a]
> Split, 2
>
> 5. y in x
> Premise
>
> 6. y in x => f(y)=y
> U Spec, 3
>
> 7. f(y)=y
> Detach, 6, 5
>
> 8. y in x => g(y)=y
> U Spec, 4
>
> 9. g(y)=y
> Detach, 8, 5
>
> 10. f(y)=g(y)
> Substitute, 9, 7
>
> 11. ALL(a):[a in x => f(a)=g(a)]
> Conclusion, 5
>
> 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> => ALL(a):[a in x => f(a)=g(a)]]
> Conclusion, 2
>
> As required:
>
> 13. ALL(x):[Set(x)
> => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> => ALL(a):[a in x => f(a)=g(a)]]]
> Conclusion, 1
> 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 11:23:28 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 15:41:31 UTC+1:
> > On Monday, December 13, 2021 at 4:39:47 AM UTC-5, Mostowski Collapse wrote:
> > > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > > certain a using your translation of "id : a -> a, id(x)=x"?
> > >
> > > Can you prove the following:
> > > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> > >
> > The identity functions on any given set are identical.
> >
> > Formal Proof:
> >
> > 1. Set(x)
> > Premise
> >
> > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > Premise
> >
> > 3. ALL(a):[a in x => f(a)=a]
> > Split, 2
> >
> > 4. ALL(a):[a in x => g(a)=a]
> > Split, 2
> >
> > 5. y in x
> > Premise
> >
> > 6. y in x => f(y)=y
> > U Spec, 3
> >
> > 7. f(y)=y
> > Detach, 6, 5
> >
> > 8. y in x => g(y)=y
> > U Spec, 4
> >
> > 9. g(y)=y
> > Detach, 8, 5
> >
> > 10. f(y)=g(y)
> > Substitute, 9, 7
> >
> > 11. ALL(a):[a in x => f(a)=g(a)]
> > Conclusion, 5
> >
> > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > => ALL(a):[a in x => f(a)=g(a)]]
> > Conclusion, 2
> >
> > As required:
> >
> > 13. ALL(x):[Set(x)
> > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > => ALL(a):[a in x => f(a)=g(a)]]]
> > Conclusion, 1

> This here doesn't say f=g:
>

So what?

> ALL(a):[a in x => f(a)=g(a)]]]
>
> It only says f|a = g|a, i.e. the restriction of f to a is
> the same as the restriction of g to a.
>

Contrary to your way of thinking, it is meaningless to talk about f(x) for x outside the domain of f. We say f is undefined in that case.

> Question was why cant you prove:
>
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>
> Why cant you prove it? Why are there so many
> identity functions.

On any given set there is only one identity. As I have shown, if f and g are identity functions on any set x, then f and g are the same function, i.e. both give the same result for a element of their domain x. Deal with it, 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

Donnie Darko wrote:
> Contrary to your way of thinking, it is meaningless to talk about f(x) for x
outside the domain of f. We say f is undefined in that case.

Where do your formulas **say** that?

Dan Christensen schrieb am Montag, 13. Dezember 2021 um 17:53:22 UTC+1:
> On Monday, December 13, 2021 at 11:23:28 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 15:41:31 UTC+1:
> > > On Monday, December 13, 2021 at 4:39:47 AM UTC-5, Mostowski Collapse wrote:
> > > > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > > > certain a using your translation of "id : a -> a, id(x)=x"?
> > > >
> > > > Can you prove the following:
> > > > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> > > >
> > > The identity functions on any given set are identical.
> > >
> > > Formal Proof:
> > >
> > > 1. Set(x)
> > > Premise
> > >
> > > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > Premise
> > >
> > > 3. ALL(a):[a in x => f(a)=a]
> > > Split, 2
> > >
> > > 4. ALL(a):[a in x => g(a)=a]
> > > Split, 2
> > >
> > > 5. y in x
> > > Premise
> > >
> > > 6. y in x => f(y)=y
> > > U Spec, 3
> > >
> > > 7. f(y)=y
> > > Detach, 6, 5
> > >
> > > 8. y in x => g(y)=y
> > > U Spec, 4
> > >
> > > 9. g(y)=y
> > > Detach, 8, 5
> > >
> > > 10. f(y)=g(y)
> > > Substitute, 9, 7
> > >
> > > 11. ALL(a):[a in x => f(a)=g(a)]
> > > Conclusion, 5
> > >
> > > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > => ALL(a):[a in x => f(a)=g(a)]]
> > > Conclusion, 2
> > >
> > > As required:
> > >
> > > 13. ALL(x):[Set(x)
> > > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > => ALL(a):[a in x => f(a)=g(a)]]]
> > > Conclusion, 1
> > This here doesn't say f=g:
> >
> So what?
> > ALL(a):[a in x => f(a)=g(a)]]]
> >
> > It only says f|a = g|a, i.e. the restriction of f to a is
> > the same as the restriction of g to a.
> >
> Contrary to your way of thinking, it is meaningless to talk about f(x) for x outside the domain of f. We say f is undefined in that case.
> > Question was why cant you prove:
> >
> > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> >
> > Why cant you prove it? Why are there so many
> > identity functions.
> On any given set there is only one identity. As I have shown, if f and g are identity functions on any set x, then f and g are the same function, i.e. both give the same result for a element of their domain x. Deal with it, 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 Monday, December 13, 2021 at 12:12:49 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 13. Dezember 2021 um 17:53:22 UTC+1:
> > On Monday, December 13, 2021 at 11:23:28 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Montag, 13. Dezember 2021 um 15:41:31 UTC+1:
> > > > On Monday, December 13, 2021 at 4:39:47 AM UTC-5, Mostowski Collapse wrote:
> > > > > How many identity functions "id : a -> a, id(x)=x" do you get for a
> > > > > certain a using your translation of "id : a -> a, id(x)=x"?
> > > > >
> > > > > Can you prove the following:
> > > > > "id1 : a -> a, id1(x)=x" & "id2 : a -> a, id2(x)=x" => id1 = id2
> > > > >
> > > > The identity functions on any given set are identical.
> > > >
> > > > Formal Proof:
> > > >
> > > > 1. Set(x)
> > > > Premise
> > > >
> > > > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > Premise
> > > >
> > > > 3. ALL(a):[a in x => f(a)=a]
> > > > Split, 2
> > > >
> > > > 4. ALL(a):[a in x => g(a)=a]
> > > > Split, 2
> > > >
> > > > 5. y in x
> > > > Premise
> > > >
> > > > 6. y in x => f(y)=y
> > > > U Spec, 3
> > > >
> > > > 7. f(y)=y
> > > > Detach, 6, 5
> > > >
> > > > 8. y in x => g(y)=y
> > > > U Spec, 4
> > > >
> > > > 9. g(y)=y
> > > > Detach, 8, 5
> > > >
> > > > 10. f(y)=g(y)
> > > > Substitute, 9, 7
> > > >
> > > > 11. ALL(a):[a in x => f(a)=g(a)]
> > > > Conclusion, 5
> > > >
> > > > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > => ALL(a):[a in x => f(a)=g(a)]]
> > > > Conclusion, 2
> > > >
> > > > As required:
> > > >
> > > > 13. ALL(x):[Set(x)
> > > > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > => ALL(a):[a in x => f(a)=g(a)]]]
> > > > Conclusion, 1
> > > This here doesn't say f=g:
> > >
> > So what?
> > > ALL(a):[a in x => f(a)=g(a)]]]
> > >
> > > It only says f|a = g|a, i.e. the restriction of f to a is
> > > the same as the restriction of g to a.
> > >
> > Contrary to your way of thinking, it is meaningless to talk about f(x) for x outside the domain of f. We say f is undefined in that case.
> > > Question was why cant you prove:
> > >
> > > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > >
> > > Why cant you prove it? Why are there so many
> > > identity functions.
> > On any given set there is only one identity. As I have shown, if f and g are identity functions on any set x, then f and g are the same function, i.e. both give the same result for a element of their domain x.

> > Contrary to your way of thinking, it is meaningless to talk about f(x) for x
> > outside the domain of f. We say f is undefined in that case.

> Where do your formulas **say** that?

We have: ALL(a):[a in x => f(a) in y]

This standard functional statement talks only about images of elements of x. Nothing about images of elements NOT in x.

Standard textbook stuff, Jan Burse. I don't know why you are having so much trouble with these elementary math facts. Just too stubborn to admit you were wrong? Like AP, JG and WM? When will you learn?

Dan

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

Where? Dream on...

Dan Christensen schrieb:
>> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> Pay attention, Jan Burse. I just did prove that. Learn some logic.

You only proved:

> ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)

But I cant find any proof of yours of this here:

ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
https://en.wikipedia.org/wiki/Uniqueness_quantification

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:34:42 UTC+1:
> Where? Dream on...
>
> Dan Christensen schrieb:
> >> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > Pay attention, Jan Burse. I just did prove that. Learn some logic.

If you could prove it, then there would be never two
different f1 and f2, such that both satisfy your wonky
identity characteristic formula:

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

But its quite easy to construct such a counter model. Just
use f1 = { (x,x) | x e a } u { (y,0) } and f2 = { (x,x) | x e a } u { (y,1) },
where y is some element ~(y e a).

Now use your function axiom with dom=a, and you get two
times the wonky identity characteristic formula as above.
So there is no EXISTUNIQUE of identity function in

DC Proof à la Dan-O-Matik wonky characteristic.

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:40:20 UTC+1:
> You only proved:
>
> > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
>
> But I cant find any proof of yours of this here:
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> https://en.wikipedia.org/wiki/Uniqueness_quantification
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:34:42 UTC+1:
> > Where? Dream on...
> >
> > Dan Christensen schrieb:
> > >> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > > Pay attention, Jan Burse. I just did prove that. Learn some logic.

Corr.:
No, one would proceed as follows. One would use
the function axiom one time with dom = a u {y1}
and f1, and one time with dom = a u {y2} and f2.

Where we have:

f1 = { (x,x) | x e a } u { (y1,y1) }

f2 = { (x,x) | x e a } u { (y2,y2) }

~(y1 e a), ~(y2 e a), y1 <> y2

One can then use this downgrade lemma:

/* 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

And finally arrive at:

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

Mostowski Collapse schrieb:
> If you could prove it, then there would be never two
> different f1 and f2, such that both satisfy your wonky
> identity characteristic formula:
>
> ALL(b):[b in a => f1(b)=b]] & ALL(b):[b in a => f2(b)=b]]
>
> But its quite easy to construct such a counter model. Just
> use f1 = { (x,x) | x e a } u { (y,0) } and f2 = { (x,x) | x e a } u { (y,1) },
> where y is some element ~(y e a).
>
> Now use your function axiom with dom=a, and you get two
> times the wonky identity characteristic formula as above.
> So there is no EXISTUNIQUE of identity function in
>
> DC Proof à la Dan-O-Matik wonky characteristic.
>
> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:40:20 UTC+1:
>> You only proved:
>>
>>> ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
>>> https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
>>
>> But I cant find any proof of yours of this here:
>> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>> https://en.wikipedia.org/wiki/Uniqueness_quantification
>> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:34:42 UTC+1:
>>> Where? Dream on...
>>>
>>> Dan Christensen schrieb:
>>>>> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>>>> Pay attention, Jan Burse. I just did prove that. Learn some logic.

By set extensionality, its easy to prove:

f1 =/= f2

There is a menu item of Set Equality in DC Proof?

Mostowski Collapse schrieb:
> Corr.:
> No, one would proceed as follows. One would use
> the function axiom one time with dom = a u {y1}
> and f1, and one time with dom = a u {y2} and f2.
>
> Where we have:
>
> f1 = { (x,x) | x e a } u { (y1,y1) }
>
> f2 = { (x,x) | x e a } u { (y2,y2) }
>
> ~(y1 e a), ~(y2 e a), y1 <> y2
>
> One can then use this downgrade lemma:
>
> /* 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
>
>
> And finally arrive at:
>
> ALL(b):[b in a => f1(b)=b]]  &  ALL(b):[b in a => f2(b)=b]]
>
> Mostowski Collapse schrieb:
>> If you could prove it, then there would be never two
>> different f1 and f2, such that both satisfy your wonky
>> identity characteristic formula:
>>
>> ALL(b):[b in a => f1(b)=b]]  &  ALL(b):[b in a => f2(b)=b]]
>>
>> But its quite easy to construct such a counter model. Just
>> use f1 = { (x,x) | x e a } u { (y,0) } and f2 = { (x,x) | x e a } u {
>> (y,1) },
>> where y is some element ~(y e a).
>>
>> Now use your function axiom with dom=a, and you get two
>> times the wonky identity characteristic formula as above.
>> So there is no EXISTUNIQUE of identity function in
>>
>> DC Proof à la Dan-O-Matik wonky characteristic.
>>
>> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:40:20
>> UTC+1:
>>> You only proved:
>>>
>>>> ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
>>>> https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
>>>
>>> But I cant find any proof of yours of this here:
>>> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>>> https://en.wikipedia.org/wiki/Uniqueness_quantification
>>> Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 16:34:42
>>> UTC+1:
>>>> Where? Dream on...
>>>>
>>>> Dan Christensen schrieb:
>>>>>> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>>>>> Pay attention, Jan Burse. I just did prove that. Learn some logic.
>

On Tuesday, December 14, 2021 at 10:40:20 AM UTC-5, Mostowski Collapse wrote:
> You only proved:
>
> > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
>
> But I cant find any proof of yours of this here:
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

You must have missed it. Here it is again:

The identity functions on any given set are identical.

Formal Proof:

1. Set(x)
Premise

2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
Premise

3. ALL(a):[a in x => f(a)=a]
Split, 2

4. ALL(a):[a in x => g(a)=a]
Split, 2

5. y in x
Premise

6. y in x => f(y)=y
U Spec, 3

7. f(y)=y
Detach, 6, 5

8. y in x => g(y)=y
U Spec, 4

9. g(y)=y
Detach, 8, 5

10. f(y)=g(y)
Substitute, 9, 7

11. ALL(a):[a in x => f(a)=g(a)]
Conclusion, 5

12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
=> ALL(a):[a in x => f(a)=g(a)]]
Conclusion, 2

As required:

13. ALL(x):[Set(x)
=> ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
=> ALL(a):[a in x => f(a)=g(a)]]]
Conclusion, 1

Dan

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

It doesn't prove f=g. The quantifier EXISTUNIQUE
requires equality, and not something else, like you do.

I can show f=/=g for a counter model.
Thats really pretty easy.

Just read what EXISTUNIQUE means:
https://en.wikipedia.org/wiki/Uniqueness_quantification

Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 16:59:53 UTC+1:
> On Tuesday, December 14, 2021 at 10:40:20 AM UTC-5, Mostowski Collapse wrote:
> > You only proved:
> >
> > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> >
> > But I cant find any proof of yours of this here:
> > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> You must have missed it. Here it is again:
> The identity functions on any given set are identical.
>
> Formal Proof:
>
> 1. Set(x)
> Premise
>
> 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> Premise
>
> 3. ALL(a):[a in x => f(a)=a]
> Split, 2
>
> 4. ALL(a):[a in x => g(a)=a]
> Split, 2
>
> 5. y in x
> Premise
>
> 6. y in x => f(y)=y
> U Spec, 3
>
> 7. f(y)=y
> Detach, 6, 5
>
> 8. y in x => g(y)=y
> U Spec, 4
>
> 9. g(y)=y
> Detach, 8, 5
>
> 10. f(y)=g(y)
> Substitute, 9, 7
>
> 11. ALL(a):[a in x => f(a)=g(a)]
> Conclusion, 5
>
> 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> => ALL(a):[a in x => f(a)=g(a)]]
> Conclusion, 2
>
> As required:
>
> 13. ALL(x):[Set(x)
> => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> => ALL(a):[a in x => f(a)=g(a)]]]
> Conclusion, 1
> 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 11:04:42 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 16:59:53 UTC+1:
> > On Tuesday, December 14, 2021 at 10:40:20 AM UTC-5, Mostowski Collapse wrote:
> > > You only proved:
> > >
> > > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> > >
> > > But I cant find any proof of yours of this here:
> > > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > You must have missed it. Here it is again:
> > The identity functions on any given set are identical.
> >
> > Formal Proof:
> >
> > 1. Set(x)
> > Premise
> >
> > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > Premise
> >
> > 3. ALL(a):[a in x => f(a)=a]
> > Split, 2
> >
> > 4. ALL(a):[a in x => g(a)=a]
> > Split, 2
> >
> > 5. y in x
> > Premise
> >
> > 6. y in x => f(y)=y
> > U Spec, 3
> >
> > 7. f(y)=y
> > Detach, 6, 5
> >
> > 8. y in x => g(y)=y
> > U Spec, 4
> >
> > 9. g(y)=y
> > Detach, 8, 5
> >
> > 10. f(y)=g(y)
> > Substitute, 9, 7
> >
> > 11. ALL(a):[a in x => f(a)=g(a)]
> > Conclusion, 5
> >
> > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > => ALL(a):[a in x => f(a)=g(a)]]
> > Conclusion, 2
> >
> > As required:
> >
> > 13. ALL(x):[Set(x)
> > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > => ALL(a):[a in x => f(a)=g(a)]]]
> > Conclusion, 1

> It doesn't prove f=g. The quantifier EXISTUNIQUE
> requires equality, and not something else, like you do.
>

It proves that f and g are the same function, i.e. the same input results is same output. There are not different identity mappings on any given set. Learn some basic logic, Jan Burse.

Dan

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

Well I can construct f1 and f2 which are different,
which both satisfy:

ALL(b):[b in a => f(b)=b]]

This tells me the quantifier EXIST cannot be replaced
by the quantifier EXISTUNIQUE in your theorem.

Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 17:54:55 UTC+1:
> On Tuesday, December 14, 2021 at 11:04:42 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 16:59:53 UTC+1:
> > > On Tuesday, December 14, 2021 at 10:40:20 AM UTC-5, Mostowski Collapse wrote:
> > > > You only proved:
> > > >
> > > > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > > > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> > > >
> > > > But I cant find any proof of yours of this here:
> > > > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > > You must have missed it. Here it is again:
> > > The identity functions on any given set are identical.
> > >
> > > Formal Proof:
> > >
> > > 1. Set(x)
> > > Premise
> > >
> > > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > Premise
> > >
> > > 3. ALL(a):[a in x => f(a)=a]
> > > Split, 2
> > >
> > > 4. ALL(a):[a in x => g(a)=a]
> > > Split, 2
> > >
> > > 5. y in x
> > > Premise
> > >
> > > 6. y in x => f(y)=y
> > > U Spec, 3
> > >
> > > 7. f(y)=y
> > > Detach, 6, 5
> > >
> > > 8. y in x => g(y)=y
> > > U Spec, 4
> > >
> > > 9. g(y)=y
> > > Detach, 8, 5
> > >
> > > 10. f(y)=g(y)
> > > Substitute, 9, 7
> > >
> > > 11. ALL(a):[a in x => f(a)=g(a)]
> > > Conclusion, 5
> > >
> > > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > => ALL(a):[a in x => f(a)=g(a)]]
> > > Conclusion, 2
> > >
> > > As required:
> > >
> > > 13. ALL(x):[Set(x)
> > > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > => ALL(a):[a in x => f(a)=g(a)]]]
> > > Conclusion, 1
> > It doesn't prove f=g. The quantifier EXISTUNIQUE
> > requires equality, and not something else, like you do.
> >
> It proves that f and g are the same function, i.e. the same input results is same output. There are not different identity mappings on any given set. Learn some basic logic, 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

Seems both of you are turning into crackpots yourselves. Just try not to give John Gabriel a run for his money!!!

On Tuesday, December 14, 2021 at 1:26:07 PM UTC-5, Mostowski Collapse wrote:
> Well I can construct f1 and f2 which are different,
> which both satisfy:
> ALL(b):[b in a => f(b)=b]]
> This tells me the quantifier EXIST cannot be replaced
> by the quantifier EXISTUNIQUE in your theorem.
> Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 17:54:55 UTC+1:
> > On Tuesday, December 14, 2021 at 11:04:42 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 16:59:53 UTC+1:
> > > > On Tuesday, December 14, 2021 at 10:40:20 AM UTC-5, Mostowski Collapse wrote:
> > > > > You only proved:
> > > > >
> > > > > > ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]
> > > > > > https://www.dcproof.com/IdentityFunctionV2.htm (98 lines)
> > > > >
> > > > > But I cant find any proof of yours of this here:
> > > > > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > > > You must have missed it. Here it is again:
> > > > The identity functions on any given set are identical.
> > > >
> > > > Formal Proof:
> > > >
> > > > 1. Set(x)
> > > > Premise
> > > >
> > > > 2. ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > Premise
> > > >
> > > > 3. ALL(a):[a in x => f(a)=a]
> > > > Split, 2
> > > >
> > > > 4. ALL(a):[a in x => g(a)=a]
> > > > Split, 2
> > > >
> > > > 5. y in x
> > > > Premise
> > > >
> > > > 6. y in x => f(y)=y
> > > > U Spec, 3
> > > >
> > > > 7. f(y)=y
> > > > Detach, 6, 5
> > > >
> > > > 8. y in x => g(y)=y
> > > > U Spec, 4
> > > >
> > > > 9. g(y)=y
> > > > Detach, 8, 5
> > > >
> > > > 10. f(y)=g(y)
> > > > Substitute, 9, 7
> > > >
> > > > 11. ALL(a):[a in x => f(a)=g(a)]
> > > > Conclusion, 5
> > > >
> > > > 12. ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > => ALL(a):[a in x => f(a)=g(a)]]
> > > > Conclusion, 2
> > > >
> > > > As required:
> > > >
> > > > 13. ALL(x):[Set(x)
> > > > => ALL(f):ALL(g):[ALL(a):[a in x => f(a)=a] & ALL(a):[a in x => g(a)=a]
> > > > => ALL(a):[a in x => f(a)=g(a)]]]
> > > > Conclusion, 1
> > > It doesn't prove f=g. The quantifier EXISTUNIQUE
> > > requires equality, and not something else, like you do.
> > >
> > It proves that f and g are the same function, i.e. the same input results is same output. There are not different identity mappings on any given set. Learn some basic logic, 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

It aint over till its over:
https://www.youtube.com/watch?v=TmENMZFUU_0

Mathin3D schrieb am Dienstag, 14. Dezember 2021 um 20:13:32 UTC+1:
> Seems both of you are turning into crackpots yourselves.
> Just try not to give John Gabriel a run for his money!!!

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]]]

Dan

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

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? Whats the desease here, do
you want to make replicates of famouse paintings, like
the mona lisa, by using a black and white xerox copier?

You are worse than WM. You also think formulas are
hieroglyphs that directly appeal to your mental idea in your
mental world. But the meaning of a formula is compositional

and it is bootstrapped from the connectives and quantifiers
in the formula, and the predicates and functions in the formula,
irrespective of a particulare domain of discourse. The

formula doesn't care what domain of discourse you have in
mind, it doesn't automatically pin down the intended domain of
discourse for you. It doesn't tollerate any errors.

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]]]
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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. Why
do you continue your proof? You are already mostly done.
No need to turn h, a set-like function into g, a FOL function

symbol which is class-like with domain and codomain V.
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"

Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:48:12 UTC+1:
> 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? Whats the desease here, do
> you want to make replicates of famouse paintings, like
> the mona lisa, by using a black and white xerox copier?
>
> You are worse than WM. You also think formulas are
> hieroglyphs that directly appeal to your mental idea in your
> mental world. But the meaning of a formula is compositional
>
> and it is bootstrapped from the connectives and quantifiers
> in the formula, and the predicates and functions in the formula,
> irrespective of a particulare domain of discourse. The
>
> formula doesn't care what domain of discourse you have in
> mind, it doesn't automatically pin down the intended domain of
> discourse for you. It doesn't tollerate any errors.
> 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]]]
> > 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 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