On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:

> Nothing else would make sense.

Nope, you silly crank.

Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."

(Donald Hartig, PhD Mathematics, University of California, Santa Barbara)

On Saturday, April 16, 2022 at 10:50:40 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:
>
> > Nothing else would make sense.
> Nope, you silly crank.
>
> Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."
>
> (Donald Hartig, PhD Mathematics, University of California, Santa Barbara)

Hint 2: "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
g : X → Y with the same domain and range are said to be equal, f = g,
if and only if f(x) = g(x) for all x ∈ X."
--Terence Tao, "Analysis I, 3rd Ed.," p. 51

Look familiar?

Dan

Dan Christensen wrote:

> On Saturday, April 16, 2022 at 4:46:46 PM UTC-4, Tate Marugo wrote:
>> Dan Christensen wrote:
>> > 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!!!

Indeed. He forgets that you, the oppressed from shitholes stolen
conglomerates dictator countries, may not read *truths* from RT.com and
other sources, except your own nazi massmedia propaganda apparatus. They
truly convinced a 90% of you wankers, to take a lethal serum into your
veins, illegally called "vaccines".

{1,2} is a common domain of:
> id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.
> id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

Every dom is a common domain of f1 : dom1 -> cod1 and f2 : dom2 -> cod2,
and can be used in your axiom in case we have:

dom ⊆ dom1 and dom ⊆ dom2

Do you finally see the "bug" in your ad hoc axiom. Or are you simply
too stupid Dan-O-Matik Ultra Moron?

P.S.: You can check yourself if this is provable:
ALL(a):[a in dom1 => f1(a) in cod1 ]
ALL(a):[a in dom2 => f2(a) in cod2 ]

Then this is also provable:
ALL(a):[a in dom => f1(a) in cod1 ]
ALL(a):[a in dom => f2(a) in cod2 ]

This is called CONTRAVARIANCE in the domain.
We told you already a 1000-times.

Dan Christensen schrieb am Sonntag, 17. April 2022 um 05:44:53 UTC+2:
> On Saturday, April 16, 2022 at 10:50:40 PM UTC-4, Fritz Feldhase wrote:
> > On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:
> >
> > > Nothing else would make sense.
> > Nope, you silly crank.
> >
> > Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."
> >
> > (Donald Hartig, PhD Mathematics, University of California, Santa Barbara)
> Hint 2: "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X."
> --Terence Tao, "Analysis I, 3rd Ed.," p. 51
>
> Look familiar?
>
> Dan

The more general law about bounded quantifiers is simply:

ALL(a):[A(a) => B(a)] & ALL(a):[C(a) => A(a)] => ALL(a):[C(a) => B(a)]

The schema is called BARBARA, and it is one of Aristoteles Syllogisms.

How stupid are you Dan-O-Matik on a scale of 1-1000? 9000 Stupid?

https://de.wikipedia.org/wiki/Modus_Barbara

Mostowski Collapse schrieb am Sonntag, 17. April 2022 um 15:38:38 UTC+2:
> {1,2} is a common domain of:
> > id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.
> > id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
> Every dom is a common domain of f1 : dom1 -> cod1 and f2 : dom2 -> cod2,
> and can be used in your axiom in case we have:
>
> dom ⊆ dom1 and dom ⊆ dom2
>
> Do you finally see the "bug" in your ad hoc axiom. Or are you simply
> too stupid Dan-O-Matik Ultra Moron?
>
> P.S.: You can check yourself if this is provable:
> ALL(a):[a in dom1 => f1(a) in cod1 ]
> ALL(a):[a in dom2 => f2(a) in cod2 ]
>
> Then this is also provable:
> ALL(a):[a in dom => f1(a) in cod1 ]
> ALL(a):[a in dom => f2(a) in cod2 ]
>
> This is called CONTRAVARIANCE in the domain.
> We told you already a 1000-times.
> Dan Christensen schrieb am Sonntag, 17. April 2022 um 05:44:53 UTC+2:
> > On Saturday, April 16, 2022 at 10:50:40 PM UTC-4, Fritz Feldhase wrote:
> > > On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:
> > >
> > > > Nothing else would make sense.
> > > Nope, you silly crank.
> > >
> > > Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."
> > >
> > > (Donald Hartig, PhD Mathematics, University of California, Santa Barbara)
> > Hint 2: "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > g : X → Y with the same domain and range are said to be equal, f = g,
> > if and only if f(x) = g(x) for all x ∈ X."
> > --Terence Tao, "Analysis I, 3rd Ed.," p. 51
> >
> > Look familiar?
> >
> > Dan

On Sunday, April 17, 2022 at 5:44:53 AM UTC+2, Dan Christensen wrote:
> On Saturday, April 16, 2022 at 10:50:40 PM UTC-4, Fritz Feldhase wrote:
> > On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:
> > >
> > > Nothing else would make sense.
> > >
> > Nope, you silly crank.
> >
> > Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."
> > (Donald Hartig, PhD Mathematics, University of California, Santa Barbara)

Which d i s p r o v e s your silly/idiotic claim.

> Definition 3.3.7 (Equality of functions)

A silly approach, especially in a formal context.

Because Dan-O-Matik is cluster fucked up, its especially
difficult to argue with him, he jumps from his BARBARA
fallacies to his Definite Description fallacies,

back and forth, and commits dozen other fallacies,
like the use of first order function symbols f : V -> V,
so that it is quite difficult discuss

functions spaces and equality. Because he did never
study the Greek, seen in that he has BARBARA not
present, and because he never read Nikolas Burbaki,

one could equally well talk to a wall now. He also
tries some fraud in that he attempts formulating
his ad hoc axioms with "if" instead "iff", thinking

they become less wrong.

Rika trying to convince Satoko to leave Hinamizawa
https://www.reddit.com/r/Higurashinonakakoroni/comments/nnnfpy/rika_talking_to_a_wall/

Fritz Feldhase schrieb am Sonntag, 17. April 2022 um 16:08:15 UTC+2:
> On Sunday, April 17, 2022 at 5:44:53 AM UTC+2, Dan Christensen wrote:
> > On Saturday, April 16, 2022 at 10:50:40 PM UTC-4, Fritz Feldhase wrote:
> > > On Sunday, April 17, 2022 at 4:27:40 AM UTC+2, Dan Christensen wrote:
> > > >
> > > > Nothing else would make sense.
> > > >
> > > Nope, you silly crank.
> > >
> > > Hint: "f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain."
> > > (Donald Hartig, PhD Mathematics, University of California, Santa Barbara)
> Which d i s p r o v e s your silly/idiotic claim.
>
> > Definition 3.3.7 (Equality of functions)
>
> A silly approach, especially in a formal context.

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

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

So you can't help? I really would like to know how to specify my two
functions so I can't prove them equal. Is it really hard?

(Reminder, in case you do have time, f' and g' are both from {0,1} and
to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
proof that they were equal but you've suggested that I needed to say
more about them, but none of the lines you posted would have made the
proof impossible.)

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

I am fully aware of that choice. That's why I chose functions with the
same domain and co-domain in my proof (though, apparently, I did not
specify them properly).

It's much simpler to have functions equal only if (as you refer to it)
their graphs are equal and not equal otherwise. That how most texts on
mathematical logic seem to do it, but the definition you've chosen is
not wrong, it's only the way it's written that's wrong. The axiom
appears to allow nonsense to be proved.

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

Unfortunately it entails nonsense. Is that a feature of DC Proof that
you want? Starting from only two axioms, yours and that the set {0}
exists, it's possible to prove

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

Can that be what you intended to follow from your axiom?

--
Ben.

On Sunday, April 17, 2022 at 5:00:09 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > 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.
> So you can't help? I really would like to know how to specify my two
> functions so I can't prove them equal. Is it really hard?
>
> (Reminder, in case you do have time, f' and g' are both from {0,1} and
> to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
> proof that they were equal

On what domain is
f' = g'?

Hint: Not on {0, 1}

but you've suggested that I needed to say
> more about them, but none of the lines you posted would have made the
> proof impossible.)
> >> > 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.

> I am fully aware of that choice. That's why I chose functions with the
> same domain and co-domain in my proof (though, apparently, I did not
> specify them properly).
>
> It's much simpler to have functions equal only if (as you refer to it)
> their graphs are equal and not equal otherwise.

I am not convinced.

> That how most texts on
> mathematical logic seem to do it,

But not in most math textbooks.

> but the definition you've chosen is
> not wrong, it's only the way it's written that's wrong. The axiom
> appears to allow nonsense to be proved.

Still waiting for a proof of any nonsensical theorems in DC Proof.

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

> Unfortunately it entails nonsense. Is that a feature of DC Proof that
> you want? Starting from only two axioms, yours and that the set {0}
> exists, it's possible to prove
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> Can that be what you intended to follow from your axiom?

We have:

dom = cod = {0}

Both are non-empty.

f: {0} --> {0}

g:{0} --> {0}

So, we can apply the definition to obtain:

f=g <=> ALL(a):[a in {0} => f(a)=g(a)]

With me so far?

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 Sunday, April 17, 2022 at 5:00:09 PM UTC-4, Ben wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > 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.
>> So you can't help? I really would like to know how to specify my two
>> functions so I can't prove them equal. Is it really hard?
>>
>> (Reminder, in case you do have time, f' and g' are both from {0,1} and
>> to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
>> proof that they were equal
>
> On what domain is
> f' = g'?
>
> Hint: Not on {0, 1}

The domain of f' and 'g are both {0,1}. How do I tell DC Proof that so
that I can't prove f'=g'?

I don't know how to make my request any clearer. Do you know how to do
it? Just say if it can't be done in DC Proof.

>> but you've suggested that I needed to say
>> more about them, but none of the lines you posted would have made the
>> proof impossible.)
>> >> > 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.
>
>> I am fully aware of that choice. That's why I chose functions with the
>> same domain and co-domain in my proof (though, apparently, I did not
>> specify them properly).
>>
>> It's much simpler to have functions equal only if (as you refer to it)
>> their graphs are equal and not equal otherwise.
>
> I am not convinced.

Sure. And I would not expect you to be convinced by me. Have you read
any of the classic texts on mathematical logic? What left you
unconvinced if you have? And is there any reason a student learning
logic should trust your judgement over that of established authors?
I.e. why should they go down your chosen path rather than the more usual
one.

>> That how most texts on
>> mathematical logic seem to do it,
>
> But not in most math textbooks.

Most math textbooks don't have formal proofs. You are doing something
not in most textbooks. However, all textbooks on mathematical logic do
include formal proofs and there's a reason they don't define function
axioms like yours.

>> but the definition you've chosen is
>> not wrong, it's only the way it's written that's wrong. The axiom
>> appears to allow nonsense to be proved.
>
> Still waiting for a proof of any nonsensical theorems in DC Proof.

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

Can't you prove that from your axiom (and the existence of the set {0})?

If you can't, what's the simplest way to get plain text proofs out of DC
Proof and paste mine for you. It was fiddly to extract text the last
time.

>> > 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.
>
>> Unfortunately it entails nonsense. Is that a feature of DC Proof that
>> you want? Starting from only two axioms, yours and that the set {0}
>> exists, it's possible to prove
>> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> Can that be what you intended to follow from your axiom?
>
> We have:
>
> dom = cod = {0}
>
> Both are non-empty.
>
> f: {0} --> {0}
>
> g:{0} --> {0}

This isn't DC Proof notation is it?

> So, we can apply the definition to obtain:
>
> f=g <=> ALL(a):[a in {0} => f(a)=g(a)]

Is this possible in DC Proof? There's no mention of this notation in
the help pages.

> With me so far?

If you don't have time to answer me /about DC Proof/, that's fine but I
don't want to be drip feed what I already know to be true about
functions and domains. Imagine that you are talking to someone who's
got a maths degree and has read a the standard textbooks on mathematical
logic.

I wanted to know if you intended

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

to be provable from your axiom. It not a theorem I'd want from an axiom
of mine about function equality, so I thought you might care enough to
either defend it or correct it.

--
Ben.

On Sunday, April 17, 2022 at 12:35:20 AM UTC+2, Dan Christensen wrote:
> On Saturday, April 16, 2022 at 6:17:39 PM UTC-4, Mostowski Collapse wrote:
> >
> > You even dont have a dom(_) [operation --ff] in DC Proof.
> >
> As you can see, there is really no need for it.

Of course there is "a need" for it, you silly idiot.

Hint: If f is a "set-theoretic" function, then

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

This allows to define the expression

f: X ---> Y

the following way:

f: X --> Y :<-> f is a set of ordered pairs & f is functional & dom(f) = X & img(f) c Y
"f is a (set-theoretic) function with domain X and co-domain Y."

Note that the co-domain for a (set-theoretic) function is not unique.

With

ord_pair(p) :<-> ExEy(p = <x, y>) "p id an ordered pair"
f is a set of ordered pairs :<-> Az(z e f -> ord_pair(z))
f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)

We now may define

function(f) :<-> EXEY: f: X --> Y (for any set f)

and

f(x) := U{y e UUf : <x, y> e f} (for a n y set f)

This finally allows to state the THEOREM:

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(f(x) = g(x)))).

From this theorem we get for any two f, g with function(f) and function(g):

dom(f) =/= dom(g) -> f =/= g.

This *is* a desirable result in math, though you are too dumb to get it.

> It just leads to confusion.

It certainly confuses *you*.

On Sunday, April 17, 2022 at 12:35:20 AM UTC+2, Dan Christensen wrote:
> On Saturday, April 16, 2022 at 6:17:39 PM UTC-4, Mostowski Collapse wrote:
> >
> > You even dont have a dom(_) [operation --ff] in DC Proof.
> >
> As you can see, there is really no need for it.

Of course there is "a need" for it, you silly idiot.

Hint: If f is a "set-theoretic" function, then

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

This allows to define the expression

f: X ---> Y

the following way:

f: X --> Y :<-> f is a set of ordered pairs & f is functional & dom(f) = X & img(f) c Y
"f is a (set-theoretic) function with domain X and co-domain Y."

Note that the co-domain for a (set-theoretic) function is not unique.

With

ord_pair(p) :<-> ExEy(p = <x, y>) "p id an ordered pair"
f is a set of ordered pairs :<-> Az(z e f -> ord_pair(z))
f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)

We now may define

function(f) :<-> EXEY: f: X --> Y (for any set f)

and

f(x) := U{y e UUf : <x, y> e f} (for a n y set f)

This finally allows to state the THEOREM:

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> (f(x) = g(x)))).

From this theorem we get for any two f, g with function(f) and function(g):

dom(f) =/= dom(g) -> f =/= g.

This *is* a desirable result in math, though you are too dumb to get it.

> It just leads to confusion.

It certainly confuses *you*.

On Saturday, April 16, 2022 at 3:10:12 AM UTC+2, Ben wrote:

> Have you considered the much simpler functions that are usually used in
> mathematical logic?

Something like this?

f: X --> Y :<-> f is a set of ordered pairs & f is functional & dom(f) = X & img(f) c Y
"f is a (set-theoretic) function with domain X and co-domain Y."

(Note that the co-domain for a (set-theoretic) function is not unique.)

With

ord_pair(p) :<-> ExEy(p = <x, y>) "p is an ordered pair"
f is a set of ordered pairs :<-> Az(z e f -> ord_pair(z))
f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)
dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

We now may define

function(f) :<-> EXEY: f: X --> Y (for any set f)

and

f(x) := U{y e UUf : <x, y> e f} (for any set f)

This finally allows to state the THEOREM:

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).

On Sunday, April 17, 2022 at 8:46:13 PM UTC-4, Ben wrote:

> >> Unfortunately it entails nonsense. Is that a feature of DC Proof that
> >> you want? Starting from only two axioms, yours and that the set {0}
> >> exists, it's possible to prove
> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >> Can that be what you intended to follow from your axiom?
> >
> > We have:
> >
> > dom = cod = {0}
> >
> > Both are non-empty.
> >
> > f: {0} --> {0}
> >
> > g:{0} --> {0}

> This isn't DC Proof notation is it?

No.

> > So, we can apply the definition to obtain:
> >
> > f=g <=> ALL(a):[a in {0} => f(a)=g(a)]

> Is this possible in DC Proof?

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

where f, g and dom are whatever names you specified for the two functions in question and their domain sets.

>
> > With me so far?
>

> If you don't have time to answer me /about DC Proof/, that's fine but I
> don't want to be drip feed what I already know to be true about
> functions and domains. Imagine that you are talking to someone who's
> got a maths degree and has read a the standard textbooks on mathematical
> logic.
>
> I wanted to know if you intended
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> to be provable from your axiom.

No.

> It not a theorem I'd want from an axiom
> of mine about function equality, so I thought you might care enough to
> either defend it or correct it.
>

The theorem (in DC Proof notation) should instead be something like:

ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]

Dan

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

On Sunday, April 17, 2022 at 9:20:40 PM UTC-4, Fritz Feldhase wrote:
> On Saturday, April 16, 2022 at 3:10:12 AM UTC+2, Ben wrote:
>
> > Have you considered the much simpler functions that are usually used in
> > mathematical logic?

This is "simpler???"

You can't be serious!

> Something like this?
> f: X --> Y :<-> f is a set of ordered pairs & f is functional & dom(f) = X & img(f) c Y
> "f is a (set-theoretic) function with domain X and co-domain Y."
> (Note that the co-domain for a (set-theoretic) function is not unique.)
>
> With
>
> ord_pair(p) :<-> ExEy(p = <x, y>) "p is an ordered pair"
> f is a set of ordered pairs :<-> Az(z e f -> ord_pair(z))
> f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)
> dom(f) := {x e UUf : Ey(<x, y> e f)}
> img(f) := {y e UUf : Ex(<x, y> e f)}
> We now may define
>
> function(f) :<-> EXEY: f: X --> Y (for any set f)
>
> and
> f(x) := U{y e UUf : <x, y> e f} (for any set f)
> This finally allows to state the THEOREM:
> AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).

Its utter nonsense, since:
ALL(a):[a in x => f(a) in x]

Doesn't say f : x -> x.

Just read Fritz Feldhase. As long as you don't have dom(f) and img(f),
you cannot define f : x -> y, since it says, among other things:

dom(f) = x
img(f) ⊆ y

But the main desease is that you think you can translate mathematics
literally ad-hoc into your first order logic variant.

Literally ad-hoc, without much thinking...

LoL

Dan Christensen schrieb am Montag, 18. April 2022 um 04:44:47 UTC+2:
> The theorem (in DC Proof notation) should instead be something like:
> ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]

Actually what implies dom(f)=X is seriality:

A binary relation is serial (also called left-total) if
∀ x ∈ X , ∃ y ∈ Y , ( x , y ) ∈ R .
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

dom(f) = X means the function is maximally **total** on X.
For partial functions on X you would only have dom(f) ⊆ X.
Well you find the notion total, see above, also used on

Wikipedia, i.e. left-total. One of the bugs of your nonsense:

/* Dan-O-Matik Nonsense */
ALL(a):[a e X => f(a) e Y]

That it doesn't imply that X is the largest set where f is total,
i.e. it doesn't imply dom(f)=X. But there is a real cluster of bugs,
since for example you use first order function symbols,

which anyway have dom(f) = V. Since this is provable:

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

LMAO!

Mostowski Collapse schrieb am Montag, 18. April 2022 um 11:18:17 UTC+2:
> Its utter nonsense, since:
> ALL(a):[a in x => f(a) in x]
> Doesn't say f : x -> x.
>
> Just read Fritz Feldhase. As long as you don't have dom(f) and img(f),
> you cannot define f : x -> y, since it says, among other things:
>
> dom(f) = x
> img(f) ⊆ y
>
> But the main desease is that you think you can translate mathematics
> literally ad-hoc into your first order logic variant.
>
> Literally ad-hoc, without much thinking...
>
> LoL
> Dan Christensen schrieb am Montag, 18. April 2022 um 04:44:47 UTC+2:
> > The theorem (in DC Proof notation) should instead be something like:
> > ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0] & ALL(a):[a in x => f(a) in x] & ALL(a):[a in x => g(a) in x] => f=g]

On Monday, April 18, 2022 at 7:18:04 AM UTC+2, Dan Christensen wrote:
> On Sunday, April 17, 2022 at 9:20:40 PM UTC-4, Fritz Feldhase wrote:
> > On Saturday, April 16, 2022 at 3:10:12 AM UTC+2, Ben wrote:
> > >
> > > Have you considered the much simpler functions that are usually used in
> > > mathematical logic?
> > >
> This is "simpler???"
>
> You can't be serious!

Ok, my initial approach was unlucky. I'll try to make it simpler.

function(f) :<-> f is a set of ordered pairs & f is functional

with

f is a set of ordered pairs :<-> Az(z e f -> ExEy(z = <x, y>)
f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z

In addition we may define

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

and, say,

f(x) := U{y e UUf : <x, y> e f}

Note that f(x) is defined for any two sets f and x.

We now can PROVE the THEOREM

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).

Still not simple enough?

Anyway, we n o w may define the (in)famous statement "f: X --> Y" the following way:

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y

"f is a (set-theoretic) function with domain X and co-domain Y."

(Note that the co-domain for a (set-theoretic) function is not unique.)

On Monday, April 18, 2022 at 12:00:10 PM UTC+2, Fritz Feldhase wrote:

> Ok, my initial approach was unlucky. I'll try to make it simpler.

function(f) :<-> Az(z e f -> ExEy(z = <x, y>) & AxAyAz(<x, y> e f & <x, z> e f -> y = z)
dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."

f(x) := U{y e UUf : <x, y> e f}

Now

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x))))

is a theorem.

Still not simple enough?

Nice!

Its not Terrence Tao though, since in Terrence Tao the equality
of functions would also include some codomain declaration. But
you can bootstrap it from F : X -> Y, and then use a pair:

f = <F, Y>

Now you have the codomain also included in your equality f = g.
Now you can talk about:

f is surjective

Which is not possible for, this here would give nonsense.

F is surjective

Because from img(F) you cannot know Y. It can be any Y such
that img(F) ⊆ Y, and surjective is only when img(F) = Y. Y
is not a definite description in the set-theoretic setting.

A pair <F, Y> is enough, a triple as in Nicolas Bourbakis could
be also useful i.e. <F,X,Y>, we could then relax X ⊆ dom(F),
but for such unnormalized relaxed tripples we would need

to define a separate equality. For the pairs its the original
equality of pairs I guess.

Fritz Feldhase schrieb am Montag, 18. April 2022 um 12:00:10 UTC+2:
> On Monday, April 18, 2022 at 7:18:04 AM UTC+2, Dan Christensen wrote:
> > On Sunday, April 17, 2022 at 9:20:40 PM UTC-4, Fritz Feldhase wrote:
> > > On Saturday, April 16, 2022 at 3:10:12 AM UTC+2, Ben wrote:
> > > >
> > > > Have you considered the much simpler functions that are usually used in
> > > > mathematical logic?
> > > >
> > This is "simpler???"
> >
> > You can't be serious!
> Ok, my initial approach was unlucky. I'll try to make it simpler.
>
> function(f) :<-> f is a set of ordered pairs & f is functional
>
> with
>
> f is a set of ordered pairs :<-> Az(z e f -> ExEy(z = <x, y>)
> f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z
> In addition we may define
> dom(f) := {x e UUf : Ey(<x, y> e f)}
> img(f) := {y e UUf : Ex(<x, y> e f)}
> and, say,
> f(x) := U{y e UUf : <x, y> e f}
> Note that f(x) is defined for any two sets f and x.
>
> We now can PROVE the THEOREM
> AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).
> Still not simple enough?
>
> Anyway, we n o w may define the (in)famous statement "f: X --> Y" the following way:
>
> f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
> "f is a (set-theoretic) function with domain X and co-domain Y."
>
> (Note that the co-domain for a (set-theoretic) function is not unique.)

But thats quite a mountain of stuff for DC Proof. To
arrive at Terrence Tao. Maybe insurmountable?

Mostowski Collapse schrieb am Montag, 18. April 2022 um 12:16:06 UTC+2:
> Nice!
>
> Its not Terrence Tao though, since in Terrence Tao the equality
> of functions would also include some codomain declaration. But
> you can bootstrap it from F : X -> Y, and then use a pair:
>
> f = <F, Y>
>
> Now you have the codomain also included in your equality f = g.
> Now you can talk about:
>
> f is surjective
>
> Which is not possible for, this here would give nonsense.
>
> F is surjective
>
> Because from img(F) you cannot know Y. It can be any Y such
> that img(F) ⊆ Y, and surjective is only when img(F) = Y. Y
> is not a definite description in the set-theoretic setting.
>
> A pair <F, Y> is enough, a triple as in Nicolas Bourbakis could
> be also useful i.e. <F,X,Y>, we could then relax X ⊆ dom(F),
> but for such unnormalized relaxed tripples we would need
>
> to define a separate equality. For the pairs its the original
> equality of pairs I guess.
> Fritz Feldhase schrieb am Montag, 18. April 2022 um 12:00:10 UTC+2:
> > On Monday, April 18, 2022 at 7:18:04 AM UTC+2, Dan Christensen wrote:
> > > On Sunday, April 17, 2022 at 9:20:40 PM UTC-4, Fritz Feldhase wrote:
> > > > On Saturday, April 16, 2022 at 3:10:12 AM UTC+2, Ben wrote:
> > > > >
> > > > > Have you considered the much simpler functions that are usually used in
> > > > > mathematical logic?
> > > > >
> > > This is "simpler???"
> > >
> > > You can't be serious!
> > Ok, my initial approach was unlucky. I'll try to make it simpler.
> >
> > function(f) :<-> f is a set of ordered pairs & f is functional
> >
> > with
> >
> > f is a set of ordered pairs :<-> Az(z e f -> ExEy(z = <x, y>)
> > f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z
> > In addition we may define
> > dom(f) := {x e UUf : Ey(<x, y> e f)}
> > img(f) := {y e UUf : Ex(<x, y> e f)}
> > and, say,
> > f(x) := U{y e UUf : <x, y> e f}
> > Note that f(x) is defined for any two sets f and x.
> >
> > We now can PROVE the THEOREM
> > AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).
> > Still not simple enough?
> >
> > Anyway, we n o w may define the (in)famous statement "f: X --> Y" the following way:
> >
> > f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
> > "f is a (set-theoretic) function with domain X and co-domain Y."
> >
> > (Note that the co-domain for a (set-theoretic) function is not unique.)

On Monday, April 18, 2022 at 11:18:17 AM UTC+2, Mostowski Collapse wrote:
>
> Its utter nonsense, since:
> ALL(a):[a in x => f(a) in x]
> Doesn't say f : x -> x.
>
> Just read Fritz Feldhase. As long as you don't have dom(f) and img(f),
> you cannot define f : x -> y, since it says, among other things:
>
> dom(f) = x
> img(f) ⊆ y

Since DC asked for it, I've simplified "my" original approach:

function(f) :<-> Az(z e f -> ExEy(z = <x, y>) & AxAyAz(<x, y> e f & <x, z> e f -> y = z)
dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."

Whats your take on a simplified Terrence Tao?

Fritz Feldhase schrieb am Montag, 18. April 2022 um 12:23:36 UTC+2:
> On Monday, April 18, 2022 at 11:18:17 AM UTC+2, Mostowski Collapse wrote:
> >
> > Its utter nonsense, since:
> > ALL(a):[a in x => f(a) in x]
> > Doesn't say f : x -> x.
> >
> > Just read Fritz Feldhase. As long as you don't have dom(f) and img(f),
> > you cannot define f : x -> y, since it says, among other things:
> >
> > dom(f) = x
> > img(f) ⊆ y
> Since DC asked for it, I've simplified "my" original approach:
>
> function(f) :<-> Az(z e f -> ExEy(z = <x, y>) & AxAyAz(<x, y> e f & <x, z> e f -> y = z)
> dom(f) := {x e UUf : Ey(<x, y> e f)}
> img(f) := {y e UUf : Ex(<x, y> e f)}
> f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
> "f is a function from X to Y."

On Monday, April 18, 2022 at 12:16:06 PM UTC+2, Mostowski Collapse wrote:

> Its not Terrence Tao though, since in Terrence Tao the equality
> of functions would also include some codomain declaration.

Right. This will be the next step.

I just started with the (basic) "set-theoretic" approach.

I'd like to call the functions defined this way "set-theoretic functions", in contrast to "mathematical functions" (a la Bourbaki) which-of course-are still defined in a set theoretic framework.

> a triple as in Nicolas Bourbakis could be also useful i.e. <F,X,Y>,

Right.

<will have to wait, need some sleep first>

On Friday, April 15, 2022 at 8:03:12 PM UTC+2, Dan Christensen wrote:
> 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)]]]