New version of DC Proof 2.0 released today. Includes:

1. Bug fix for Arbitrary Consequent Rule that was missing certain error conditions.

2. Re-introduced requirements for non-empty domain and codomain sets in function axioms. Adventurous users are still able to introduce their own versions of axioms at the beginning of proofs.

NEW FUNCTION AXIOM (1 variable)

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
& EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW

=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]

=> EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod
=> [fun(a1)=b <=> (a1,b) in gra]]]]

where

dom = domain set
cod = codomain set
gra = graph set
fun = function operator

NEW FUNCTION EQUALITY AXIOM (1 variable)

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

& EXIST(a):a in dom & EXIST(a):a in cod <---- NEW

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

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

NEW FUNCTION SPACE AXIOM (1 variable)

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

& EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW

=> EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]

Dan

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

Now I can prove the following, all non-empty
identity functions are equal:

ALL(f):ALL(g):[idfun(f) & idfun(g) => f=g]

Where idfun(f) is defined as:

idfun(f) <=> EXIST(dom):[EXIST(a): a in dom <----- NEW
& ALL(a):[a in dom => f(a) in dom]]

In Terrence Tao id : X->X are differnent for
different X. Even in set theory this is the case.

LMAO!

Dan Christensen schrieb am Freitag, 15. April 2022 um 20:03:12 UTC+2:
> NEW FUNCTION EQUALITY AXIOM (1 variable)
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>
> & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
>
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
>
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

On Friday, April 15, 2022 at 3:53:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> Now I can prove the following, all non-empty
> identity functions are equal:
>

On any given non-empty set X, there exists only one identity function id: X --> X such that id(x)=x. I will leave it to you as an exercise, Jan Burse

Hint: Start with a set X. Construct an identity function id: X --> X. Let id': X --> X be another identity function on X. Then prove id=id' on X.

Dan

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

On Friday, April 15, 2022 at 4:18:11 PM UTC-4, Dan Christensen wrote:
> On Friday, April 15, 2022 at 3:53:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > Now I can prove the following, all non-empty
> > identity functions are equal:
> >
> On any given non-empty set X, there exists only one identity function id: X --> X such that id(x)=x. I will leave it to you as an exercise, Jan Burse
>
> Hint: Start with a set X. Construct an identity function id: X --> X. Let id': X --> X be another identity function on X. Then prove id=id' on X.

I was able to prove:

ALL(x):[Set(x) & EXIST(a):a in x
=> EXIST(id):[ALL(a):[a in x => id(a)=a] & ALL(id'):[ALL(a):[a in x => id'(a)=a] => id=id']]] (136 lines)

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 prove in DC Proof:

ALL(f):ALL(g):[idfun(f) & idfun(g) => f=g]

Where:

idfun(f) <=> EXIST(dom):[Set(dom) & EXIST(a): a in dom <----- NEW
& ALL(a):[a in dom => f(a) in dom]]

Dan Christensen schrieb am Samstag, 16. April 2022 um 00:52:17 UTC+2:
> On Friday, April 15, 2022 at 4:18:11 PM UTC-4, Dan Christensen wrote:
> > On Friday, April 15, 2022 at 3:53:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > > Now I can prove the following, all non-empty
> > > identity functions are equal:
> > >
> > On any given non-empty set X, there exists only one identity function id: X --> X such that id(x)=x. I will leave it to you as an exercise, Jan Burse
> >
> > Hint: Start with a set X. Construct an identity function id: X --> X. Let id': X --> X be another identity function on X. Then prove id=id' on X.
> I was able to prove:
>
> ALL(x):[Set(x) & EXIST(a):a in x
> => EXIST(id):[ALL(a):[a in x => id(a)=a] & ALL(id'):[ALL(a):[a in x => id'(a)=a] => id=id']]] (136 lines)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Corr:
idfun(f) <=> EXIST(dom):[Set(dom) & EXIST(a): a in dom <----- NEW
& ALL(a):[a in dom => f(a)=a]]

Here is a proof sketch:

if idfun(f) & idfun(g), then there are fd and gd:

Set(fd ) & EXIST(a): a in fd <----- NEW
& ALL(a):[a in fd => f(a)=a]
Set(gd) & EXIST(a): a in gd <----- NEW
& ALL(a):[a in gd => g(a)=a]]

Now by your function existence axiom, you can contruct
for fgd = fd u fg and identity function h:

Set(fgd ) & EXIST(a): a in fgd <----- NEW
& ALL(a):[a in fgd => h(a)=a]]

By using your function equality axiom with dom/cod=fd
respectively with dom/cod=gd you can prove:

f=h
g=h

Using subsitution of DC proof, you can prove:

f=g

Mostowski Collapse schrieb am Samstag, 16. April 2022 um 00:59:59 UTC+2:
> Well I can prove in DC Proof:
> ALL(f):ALL(g):[idfun(f) & idfun(g) => f=g]
>
> Where:
> idfun(f) <=> EXIST(dom):[Set(dom) & EXIST(a): a in dom <----- NEW
> & ALL(a):[a in dom => f(a) in dom]]
> Dan Christensen schrieb am Samstag, 16. April 2022 um 00:52:17 UTC+2:
> > On Friday, April 15, 2022 at 4:18:11 PM UTC-4, Dan Christensen wrote:
> > > On Friday, April 15, 2022 at 3:53:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > > > Now I can prove the following, all non-empty
> > > > identity functions are equal:
> > > >
> > > On any given non-empty set X, there exists only one identity function id: X --> X such that id(x)=x. I will leave it to you as an exercise, Jan Burse
> > >
> > > Hint: Start with a set X. Construct an identity function id: X --> X. Let id': X --> X be another identity function on X. Then prove id=id' on X.
> > I was able to prove:
> >
> > ALL(x):[Set(x) & EXIST(a):a in x
> > => EXIST(id):[ALL(a):[a in x => id(a)=a] & ALL(id'):[ALL(a):[a in x => id'(a)=a] => id=id']]] (136 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 Friday, April 15, 2022 at 9:53:04 PM UTC+2, Mostowski Collapse wrote:
>
> In Terrence Tao id : X->X are differnent for
> different X.

No, they aren't.

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> New version of DC Proof 2.0 released today. Includes:
>
> 1. Bug fix for Arbitrary Consequent Rule that was missing certain
> error conditions.
>
> 2. Re-introduced requirements for non-empty domain and codomain sets
> in function axioms. Adventurous users are still able to introduce
> their own versions of axioms at the beginning of proofs.

> NEW FUNCTION EQUALITY AXIOM (1 variable)
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>
> & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
>
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
>
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

With this axiom, and the existence of a set with 0 in it, DC Proof
proves

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

Is that what you want? It looks like something that would confuse
students.

Have you considered the much simpler functions that are usually used in
mathematical logic? See, for example, Mendelson or Shoenfield.

You haven't replied to my request for help in defining the two different
functions that I could prove equal. You made some remarks, but none of
them would alter the proof. I know you are not obliged to help me, but
it should be simple to define two distinct functions on, say, {0,1} so
that they can't be proved equal using your axiom. If you don't have
time, or don't think it's a serious problem, just say.

--
Ben.

On Friday, April 15, 2022 at 9:10:12 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > New version of DC Proof 2.0 released today. Includes:
> >
> > 1. Bug fix for Arbitrary Consequent Rule that was missing certain
> > error conditions.
> >
> > 2. Re-introduced requirements for non-empty domain and codomain sets
> > in function axioms. Adventurous users are still able to introduce
> > their own versions of axioms at the beginning of proofs.
> > NEW FUNCTION EQUALITY AXIOM (1 variable)
> >
> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> >
> > & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
> >
> > & ALL(a):[a in dom => f1(a) in cod]
> > & ALL(a):[a in dom => f2(a) in cod]
> >
> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> With this axiom, and the existence of a set with 0 in it, DC Proof
> proves
>
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>
> Is that what you want? It looks like something that would confuse
> students.
>
> Have you considered the much simpler functions that are usually used in
> mathematical logic? See, for example, Mendelson or Shoenfield.
>
> You haven't replied to my request for help in defining the two different
> functions that I could prove equal. You made some remarks, but none of
> them would alter the proof. I know you are not obliged to help me, but
> it should be simple to define two distinct functions on, say, {0,1} so
> that they can't be proved equal using your axiom. If you don't have
> time, or don't think it's a serious problem, just say.
>

I didn't really follow your proof, Ben. Maybe this will help: https://www.dcproof.com/IdentityFunctionsUnique.htm
Dan

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

On Friday, April 15, 2022 at 7:05:51 PM UTC-4, Mostowski Collapse wrote:
> Corr:
> idfun(f) <=> EXIST(dom):[Set(dom) & EXIST(a): a in dom <----- NEW
> & ALL(a):[a in dom => f(a)=a]]
>
> Here is a proof sketch:
>
> if idfun(f) & idfun(g), then there are fd and gd:
>
> Set(fd ) & EXIST(a): a in fd <----- NEW
> & ALL(a):[a in fd => f(a)=a]
> Set(gd) & EXIST(a): a in gd <----- NEW
> & ALL(a):[a in gd => g(a)=a]]
>

My Function Equality Axiom compares only functions that have both the same domain and codomain. Make up your own non-standard function axioms if you think you can make them work. Stick them on the front of your proofs with using the Axiom Rule.

> Now by your function existence axiom, you can contruct
> for fgd = fd u fg and identity function h:
>
> Set(fgd ) & EXIST(a): a in fgd <----- NEW
> & ALL(a):[a in fgd => h(a)=a]]
>
> By using your function equality axiom with dom/cod=fd
> respectively with dom/cod=gd you can prove:
>
> f=h
> g=h
>
> Using subsitution of DC proof, you can prove:
>
> f=g

This may help: https://www.dcproof.com/IdentityFunctionsUnique.htm

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 wrote:

>> Set(fd ) & EXIST(a): a in fd <----- NEW & ALL(a):[a in fd => f(a)=a]
>> Set(gd) & EXIST(a): a in gd <----- NEW & ALL(a):[a in gd => g(a)=a]]
> My Function Equality Axiom compares only functions that have both the
> same domain and codomain. Make up your own non-standard function axioms
> if you think you can make them work. Stick them on the front of your
> proofs with using the Axiom Rule.

nonsense.

British captive who fought in Mariupol describes ‘reality’
The Ukrainian forces have shown “lack of care” for civilians, Aiden Aslin
claims
https://www.rt.com/russia/553933-british-captive-mariupol-ukraine-reality/

“The situation in Mariupol is catastrophic. It could have been avoided
should Ukraine have left but they chose to stay. nazi *Zelensky* had a big
role [in this decision]. He could have told them to leave but they stayed.
I did not want this, I wanted to leave because we do not need war,” Aslin
can be seen saying in the video.

How? It has an ALL(_) quantifier, your axion says:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[.... bla bla ....]

I can plug into the ALL(_) quantifier what ever I want with
your U Spec inference rule. The axiom doesn't say:

ALL(d):ALL(c):ALL(f1):ALL(f2):[d=dom(f1) & d=dom(f2) etc.. .... bla bla ....]

You even dont have a dom(_) function in DC Proof.

Dan Christensen schrieb am Samstag, 16. April 2022 um 06:59:32 UTC+2:
> My Function Equality Axiom compares only functions that have both the same domain and codomain.

Ben is right, when he writes:

> With this axiom, and the existence of a set with 0 in it, DC Proof proves
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

But this here is also provable:

> ALL(f):ALL(g):[idfun(f) & idfun(g) => f=g]
> Where idfun(f) is defined as:
> idfun(f) <=> EXIST(dom):[EXIST(a): a in dom <----- NEW
> & ALL(a):[a in dom => f(a) in dom]]

The identity functioins must not cover the same points, could
be f(0)=0 and g(1)=1. I sketched a proof already.

Mostowski Collapse schrieb am Sonntag, 17. April 2022 um 00:17:39 UTC+2:
> How? It has an ALL(_) quantifier, your axion says:
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[.... bla bla ....]
>
> I can plug into the ALL(_) quantifier what ever I want with
> your U Spec inference rule. The axiom doesn't say:
>
> ALL(d):ALL(c):ALL(f1):ALL(f2):[d=dom(f1) & d=dom(f2) etc.. .... bla bla ....]
>
> You even dont have a dom(_) function in DC Proof.
> Dan Christensen schrieb am Samstag, 16. April 2022 um 06:59:32 UTC+2:
> > My Function Equality Axiom compares only functions that have both the same domain and codomain.

On Saturday, April 16, 2022 at 4:46:46 PM UTC-4, Tate Marugo wrote:
> Dan Christensen wrote:
>
> >> Set(fd ) & EXIST(a): a in fd <----- NEW & ALL(a):[a in fd => f(a)=a]
> >> Set(gd) & EXIST(a): a in gd <----- NEW & ALL(a):[a in gd => g(a)=a]]
> > My Function Equality Axiom compares only functions that have both the
> > same domain and codomain. Make up your own non-standard function axioms
> > if you think you can make them work. Stick them on the front of your
> > proofs with using the Axiom Rule.
> nonsense.
>
> British captive who fought in Mariupol describes ‘reality’
> The Ukrainian forces have shown “lack of care” for civilians, Aiden Aslin
> claims
> https://www.rt.com/....
>

rt.com???? HA, HA, HA!!!

They are already different in set theory.

id1 : {1,2} -> {1,2} is id1={(1,1),(2,2)}
id2: {2,3} -> {2,3} is id2={(2,2),(3,3)}

Do you claim id1=id2?

Fritz Feldhase schrieb am Samstag, 16. April 2022 um 02:11:58 UTC+2:
> On Friday, April 15, 2022 at 9:53:04 PM UTC+2, Mostowski Collapse wrote:
> >
> > In Terrence Tao id : X->X are differnent for
> > different X.
> No, they aren't.

They are different, but in DC Proof you can
take id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

And using the Ben Trick, prove via Dans ad-hoc Axiom:

id2=id3 Hint: Use dom/cod = {1,2}
id1=id3 Hint: Use dom/cod = {2,3}

Then using DC Proof substition:

id1=id2

LoL

Mostowski Collapse schrieb am Sonntag, 17. April 2022 um 00:22:32 UTC+2:
> They are already different in set theory.
>
> id1 : {1,2} -> {1,2} is id1={(1,1),(2,2)}
> id2: {2,3} -> {2,3} is id2={(2,2),(3,3)}
>
> Do you claim id1=id2?
> Fritz Feldhase schrieb am Samstag, 16. April 2022 um 02:11:58 UTC+2:
> > On Friday, April 15, 2022 at 9:53:04 PM UTC+2, Mostowski Collapse wrote:
> > >
> > > In Terrence Tao id : X->X are differnent for
> > > different X.
> > No, they aren't.

On Saturday, April 16, 2022 at 6:17:39 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 16. April 2022 um 06:59:32 UTC+2:
> > My Function Equality Axiom compares only functions that have both the same domain and codomain.

> How?

We can see this by inspection. (See below)

> It has an ALL(_) quantifier, your axion says:
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)

> & EXIST(a):a in dom & EXIST(a):a in cod
> & ALL(a):[a in dom => f1(a) in cod] <---- function f1 here with domain = dom, codomain = cod
> & ALL(a):[a in dom => f2(a) in cod] <---- another function f2 with the SAME domain and codomain

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

>
> I can plug into the ALL(_) quantifier what ever I want with
> your U Spec inference rule. The axiom doesn't say:
>
> ALL(d):ALL(c):ALL(f1):ALL(f2):[d=dom(f1) & d=dom(f2) etc.. .... bla bla ....]
>
> You even dont have a dom(_) function in DC Proof.

As you can see, there is really no need for it. It just leads to confusion. KISS

Dan

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

On Saturday, April 16, 2022 at 6:22:32 PM UTC-4, Mostowski Collapse wrote:
> They are already different in set theory.
>
> id1 : {1,2} -> {1,2} is id1={(1,1),(2,2)}
> id2: {2,3} -> {2,3} is id2={(2,2),(3,3)}
>
> Do you claim id1=id2?

NO. You cannot infer that id1=id2 from the standard definition of functional equality since the functions id1 and id2 have different domains and codomains.

Dan

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

On Saturday, April 16, 2022 at 6:26:25 PM UTC-4, Mostowski Collapse wrote:
> They are different, but in DC Proof you can
> take id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
>
> And using the Ben Trick, prove via Dans ad-hoc Axiom:
>
> id2=id3 Hint: Use dom/cod = {1,2}
> id1=id3 Hint: Use dom/cod = {2,3}
>
> Then using DC Proof substition:
>
> id1=id2
>

We must really see the proof of this, Jan Burse.

Maybe you didn't know, but A=B and C=D does NOT imply that A=D.

Dan

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

Corr.: Typo
id1=id3 Hint: Use dom/cod = {1,2}
id2=id3 Hint: Use dom/cod = {2,3}

You axiom has ALL(_), so you can plug-in dom={1,2} and cod={1,2}
and then prove:

id1=id3

Thats pretty trivial. We are horsing around your nonsense ad-hoc
axiom with always the same trick,

I call it Bens trick.

Dan Christensen schrieb am Sonntag, 17. April 2022 um 00:51:30 UTC+2:
> On Saturday, April 16, 2022 at 6:26:25 PM UTC-4, Mostowski Collapse wrote:
> > They are different, but in DC Proof you can
> > take id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
> >
> > And using the Ben Trick, prove via Dans ad-hoc Axiom:
> >
> > id2=id3 Hint: Use dom/cod = {1,2}
> > id1=id3 Hint: Use dom/cod = {2,3}
> >
> > Then using DC Proof substition:
> >
> > id1=id2
> >
> We must really see the proof of this, Jan Burse.
>
> Maybe you didn't know, but A=B and C=D does NOT imply that A=D.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan please get sober. Do you deny:

ALL(a):[a in {1,2} => id1(a) in {1,2}]
ALL(a):[a in {1,2} => id3(a) in {1,2} ]
ALL(a):[a in {1,2} => id1(a)=id3(a)]]]

If not, then we have:

id1=id3

Similarly you can prove:

id2=id3

And then by using DC Proof substitution:

id1=id2

Mostowski Collapse schrieb am Sonntag, 17. April 2022 um 01:01:31 UTC+2:
> Corr.: Typo
> id1=id3 Hint: Use dom/cod = {1,2}
> id2=id3 Hint: Use dom/cod = {2,3}
>
>
> You axiom has ALL(_), so you can plug-in dom={1,2} and cod={1,2}
> and then prove:
>
> id1=id3
>
> Thats pretty trivial. We are horsing around your nonsense ad-hoc
> axiom with always the same trick,
>
> I call it Bens trick.
> Dan Christensen schrieb am Sonntag, 17. April 2022 um 00:51:30 UTC+2:
> > On Saturday, April 16, 2022 at 6:26:25 PM UTC-4, Mostowski Collapse wrote:
> > > They are different, but in DC Proof you can
> > > take id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
> > >
> > > And using the Ben Trick, prove via Dans ad-hoc Axiom:
> > >
> > > id2=id3 Hint: Use dom/cod = {1,2}
> > > id1=id3 Hint: Use dom/cod = {2,3}
> > >
> > > Then using DC Proof substition:
> > >
> > > id1=id2
> > >
> > We must really see the proof of this, Jan Burse.
> >
> > Maybe you didn't know, but A=B and C=D does NOT imply that A=D.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 16, 2022 at 7:05:52 PM UTC-4, Mostowski Collapse wrote:
> Do you deny:
>
> ALL(a):[a in {1,2} => id1(a) in {1,2}]
> ALL(a):[a in {1,2} => id3(a) in {1,2} ]
> ALL(a):[a in {1,2} => id1(a)=id3(a)]]]
>

Assuming id1 and id3 are identity functions.

> If not, then we have:
>
> id1=id3
>
> Similarly you can prove:
>
> id2=id3
>
> And then by using DC Proof substitution:
>
> id1=id2

Only assuming id2 is also an identity functions on {1, 2}.

Dan

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

take
id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.
id2: {2,3} -> {2,3} is id2 = {(2,2),(3,3)}.
id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

You can prove:

ALL(a):[a in {1,2} => id1(a) in {1,2}]
ALL(a):[a in {1,2} => id3(a) in {1,2} ]
ALL(a):[a in {1,2} => id1(a)=id3(a)]]]

Which implies, according to your ad-hoc axiom:

id1 = id3

You can prove:

ALL(a):[a in {2,3} => id2(a) in {2,3}]
ALL(a):[a in {2,3} => id3(a) in {2,3} ]
ALL(a):[a in {2,3} => id2(a)=id3(a)]]]

Which implies, according to your ad-hoc axiom:

id2 = id3

Now use subst from your DC Proof, and you can derive:

id1 = id2

Dan Christensen schrieb am Sonntag, 17. April 2022 um 01:49:52 UTC+2:
> On Saturday, April 16, 2022 at 7:05:52 PM UTC-4, Mostowski Collapse wrote:
> > Do you deny:
> >
> > ALL(a):[a in {1,2} => id1(a) in {1,2}]
> > ALL(a):[a in {1,2} => id3(a) in {1,2} ]
> > ALL(a):[a in {1,2} => id1(a)=id3(a)]]]
> >
> Assuming id1 and id3 are identity functions.
> > If not, then we have:
> >
> > id1=id3
> >
> > Similarly you can prove:
> >
> > id2=id3
> >
> > And then by using DC Proof substitution:
> >
> > id1=id2
> Only assuming id2 is also an identity functions on {1, 2}.
> 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 <Dan_Christensen@sympatico.ca> writes:

> On Friday, April 15, 2022 at 9:10:12 PM UTC-4, Ben wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > New version of DC Proof 2.0 released today. Includes:
>> >
>> > 1. Bug fix for Arbitrary Consequent Rule that was missing certain
>> > error conditions.
>> >
>> > 2. Re-introduced requirements for non-empty domain and codomain sets
>> > in function axioms. Adventurous users are still able to introduce
>> > their own versions of axioms at the beginning of proofs.
>> > NEW FUNCTION EQUALITY AXIOM (1 variable)
>> >
>> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>> >
>> > & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
>> >
>> > & ALL(a):[a in dom => f1(a) in cod]
>> > & ALL(a):[a in dom => f2(a) in cod]
>> >
>> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
>> With this axiom, and the existence of a set with 0 in it, DC Proof
>> proves
>>
>> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>>
>> Is that what you want? It looks like something that would confuse
>> students.

No comment? Is that really something you want your axiom to entail?

>> Have you considered the much simpler functions that are usually used in
>> mathematical logic? See, for example, Mendelson or Shoenfield.
>>
>> You haven't replied to my request for help in defining the two different
>> functions that I could prove equal. You made some remarks, but none of
>> them would alter the proof. I know you are not obliged to help me, but
>> it should be simple to define two distinct functions on, say, {0,1} so
>> that they can't be proved equal using your axiom. If you don't have
>> time, or don't think it's a serious problem, just say.
>
> I didn't really follow your proof, Ben.

You said it was fine, were just guessing? Anyway, as I say, you are
under no obligation to help.

> Maybe this will help:
> https://www.dcproof.com/IdentityFunctionsUnique.htm

Not really. I can prove too many things equal. The problem is how to
define my two function so they /can't/ be proved equal.

--
Ben.

On Saturday, April 16, 2022 at 8:33:46 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Friday, April 15, 2022 at 9:10:12 PM UTC-4, Ben wrote:
> >> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >>
> >> > New version of DC Proof 2.0 released today. Includes:
> >> >
> >> > 1. Bug fix for Arbitrary Consequent Rule that was missing certain
> >> > error conditions.
> >> >
> >> > 2. Re-introduced requirements for non-empty domain and codomain sets
> >> > in function axioms. Adventurous users are still able to introduce
> >> > their own versions of axioms at the beginning of proofs.
> >> > NEW FUNCTION EQUALITY AXIOM (1 variable)
> >> >
> >> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> >> >
> >> > & EXIST(a):a in dom & EXIST(a):a in cod <---- NEW
> >> >
> >> > & ALL(a):[a in dom => f1(a) in cod]
> >> > & ALL(a):[a in dom => f2(a) in cod]
> >> >
> >> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> >> With this axiom, and the existence of a set with 0 in it, DC Proof
> >> proves
> >>
> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >>
> >> Is that what you want? It looks like something that would confuse
> >> students.
> No comment? Is that really something you want your axiom to entail?
> >> Have you considered the much simpler functions that are usually used in
> >> mathematical logic? See, for example, Mendelson or Shoenfield.
> >>
> >> You haven't replied to my request for help in defining the two different
> >> functions that I could prove equal. You made some remarks, but none of
> >> them would alter the proof. I know you are not obliged to help me, but
> >> it should be simple to define two distinct functions on, say, {0,1} so
> >> that they can't be proved equal using your axiom. If you don't have
> >> time, or don't think it's a serious problem, just say.
> >
> > I didn't really follow your proof, Ben.
> You said it was fine, were just guessing? Anyway, as I say, you are
> under no obligation to help.
> > Maybe this will help:
> > https://www.dcproof.com/IdentityFunctionsUnique.htm
> Not really. I can prove too many things equal. The problem is how to
> define my two function so they /can't/ be proved equal.
>

I think you are missing the point that the equality of a pair of function operators f1 and f2 is always equality with respect to a COMMON domain. Nothing else would make sense.

Recall:

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

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

This says nothing about either function outside of the specified domain.

Dan

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