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

A simple set-theoretic 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."

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

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

No artificial restrictions at all.

Yeah very good. The function() guards, especially ExEy(z = <x, y>,
prevent counter examples such as:

f = {(1,1)}
g = {(1,1), {}}

Fritz Feldhase schrieb am Montag, 18. April 2022 um 13:15:15 UTC+2:
> A simple set-theoretic 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."
> f(x) := U{y e UUf : <x, y> e f}
> Theorem:
> AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)))).
>
> No artificial restrictions at all.

Mostowski Collapse wrote:

> Yeah very good. The function() guards, especially ExEy(z = <x, y>,
> prevent counter examples such as: f = {(1,1)} g = {(1,1), {}}

but the russian army shall show no mercy to those nazis, called
"ukrainians". The dirt of the earth, those nazis. That's was the fault of
russian people, not evil enough. They thought could negotiate _humanity_
with the nazis. You fucking idiot. 30 *_bio_weapon_labs_* to commit evil
to humanity, here the russian, hungarian, moldavian, tjekian and romanian
people. 30 *_bio_weapon_labs_*, you fucking idiot, since those are
*_strict_forbidden_* in capitalist america, thousands of miles distant
from capitalist nazi europe.

More Surrender in Ukraine
https://www.brighteon.com/2d5257b8-9f50-4e39-b94b-ec09e08c892d

These baby boys are surely not from Moskva, they are
too properly shaved and they are grinning. So the
nazi fish got a full load of aquatic feed?

Ship Funeral Service for Moskva
https://www.youtube.com/watch?v=dQw4w9WgXcQ

Troy Matsuda schrieb am Montag, 18. April 2022 um 14:32:15 UTC+2:
> Mostowski Collapse wrote:
>
> > Yeah very good. The function() guards, especially ExEy(z = <x, y>,
> > prevent counter examples such as: f = {(1,1)} g = {(1,1), {}}

On Monday, April 18, 2022 at 5:18:17 AM UTC-4, Mostowski Collapse wrote:

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

> Its utter nonsense, since:
> ALL(a):[a in x => f(a) in x]
> Doesn't say f : x -> x.
>

They mean the same thing. Mine is a more useful notation, however. It is already a logical expression to which you can directly apply the rules of inference, e.g. universal specification and detachment.

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

Another unnecessary layer of abstraction IMHO. And you still don't have a logical expression to work on.

Dan

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

Mostowski Collapse wrote:

> These baby boys are surely not from Moskva, they are
> too properly shaved and they are grinning. So the
> nazi fish got a full load of aquatic feed?
>
> Ship Funeral Service for Moskva

No, you are in huge error, much indeed. Next stop would be the nazi
shithole named *switserland*, accidentally populated by nazi slavic
immigrants, turned anglo-saxon overnight. Then the nazi Polakia and so on,
*nazi_nato_bitches* sending imbecile army, fighting their lies into
truths.

You have to learn what your fake money means. You killed an innocent man
in the Bible, because of the fake money, you stinking *nazi_bitch*. How we
say in physics, you are fucked up. Expect no mercy. You Russian provinces
have to learn a lesson you never forget.

More Surrender in Ukraine
https://www.brighteon.com/2d5257b8-9f50-4e39-b94b-ec09e08c892d

UKRAINE: MILITARY PAWNSHOP! MISC. TIDBITS FROM THE BIDEN-GATE ZONE.
https://www.bitchute.com/video/KWD1O5v9Ch7i/

On Monday, April 18, 2022 at 11:59:21 AM UTC-4, Troy Matsuda wrote:
> Mostowski Collapse wrote:
>
> > These baby boys are surely not from Moskva, they are
> > too properly shaved and they are grinning. So the
> > nazi fish got a full load of aquatic feed?
> >
> > Ship Funeral Service for Moskva
> No, you are in huge error, much indeed. Next stop would be the nazi
> shithole named *switserland*, accidentally populated by nazi slavic
> immigrants, turned anglo-saxon overnight. Then the nazi Polakia and so on,
> *nazi_nato_bitches* sending imbecile army, fighting their lies into
> truths.
>
> You have to learn what your fake money means. You killed an innocent man
> in the Bible, because of the fake money, you stinking *nazi_bitch*. How we
> say in physics, you are fucked up. Expect no mercy. You Russian provinces
> have to learn a lesson you never forget.

Wow! When the enemy stoops to this, you know you they are just about to collapse.

On Monday, April 18, 2022 at 5:57:18 PM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 5:18:17 AM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Montag, 18. April 2022 um 04:44:47 UTC+2:
> >
> > Its utter nonsense, since:
> > ALL(a):[a in x => f(a) in x]
> > doesn't say f : x -> x.
> >
> They mean the same thing.

No, they don't mean the same thing.

"f: X --> Y" means "f is a function with domain X and codomain Y."

Hence "f: X --> X" means "f is a function with domain X and codomain X."

> Mine is a more useful notation, however.

Nonsense. You are arguing like a crank, man, you know.

Hint: _No one_ agrees with you. (Hmmm... Didn't take into account WM and JG though.)

> It is already a logical expression to which you can directly apply the rules of inference, e.g. universal specification and detachment.

So what?

Everyone is able to grasp the concept of a "function" as a certain /relation/. It's a rather fundamental concept. Set theory is up to the task to _define_ the necessary notions.

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

Right.

Actually, the set theoretic approach is rather simple:

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}

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

No artificial restrictions at all: This approach allows to deal with the empty function too.

> Another unnecessary layer of abstraction IMHO.

You are either a complete idiot when it comes to math or a crank (or both).

> And you still don't have a logical expression to work on.

Which "logical expression" are you asking for?

On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> On Monday, April 18, 2022 at 5:57:18 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 5:18:17 AM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Montag, 18. April 2022 um 04:44:47 UTC+2:
> > >
> > > Its utter nonsense, since:
> > > ALL(a):[a in x => f(a) in x]
> > > doesn't say f : x -> x.
> > >
> > They mean the same thing.
> No, they don't mean the same thing.
>
> "f: X --> Y" means "f is a function with domain X and codomain Y."
>
> Hence "f: X --> X" means "f is a function with domain X and codomain X."

You can also infer this from: ALL(a):[a in x => f(a) in x].

[snip]

> > It is already a logical expression to which you can directly apply the rules of inference, e.g. universal specification and detachment.
> So what?
>

So, it is convenient for writing proofs.
[snip]

> > > 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
> Right.
>
> Actually, the set theoretic approach is rather simple:
> 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}
>

Or, more conveniently: ALL(a):[a in x => f(a) in x]

> Theorem:
> AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)))).
> No artificial restrictions at all: This approach allows to deal with the empty function too.

If users really want to play with empty functions, they can introduce your own function axioms allowing empty domains and see where it might lead. In the end, after some backtracking, I felt I could not recommend it to students.

[snip]

> > And you still don't have a logical expression to work on.
> Which "logical expression" are you asking for?

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

Ultimately, it must come to this even with your "set theoretic" approach.

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, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> >
> > Actually, the set theoretic approach is rather simple:
> >
> > 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} ("the value of f at x")
> >
> > No artificial restrictions at all: This approach allows to deal with the empty function too.

Now you are asking for
> > >
> > > a logical expression to work on.
> > >
> > Which "logical expression" are you asking for?
> >
> ALL(a):[a in x => f(a) in x]

You can't get that from "nothing", hence it's rather a "mathematical expression".

Actually the theorem is

AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).

Or slightly more general

AXAYAf: (f: X --> Y) -> Ax(x e X -> f(x) e Y).

> Ultimately, it must come to this even with your "set theoretic" approach.

Of course, so where do you see a problem? It follows from the definitions mentioned above (and some axioms of set theory).

You see. we do not need any additional axioms concerning "functions" only SOME of the usual set theoretic axioms (actually the most basic of them) and some definitions. From this we get "identity of functions" as theorem as well as your "logical expression".

Hint: That's why set theory is considered as a foundation for math, you know.

On Monday, April 18, 2022 at 8:46:39 PM UTC+2, Fritz Feldhase wrote:
> On Monday, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> > >
> > > Actually, the set theoretic approach is rather simple:
> > >
> > > 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} ("the value of f at x")
> > >
> > > No artificial restrictions at all: This approach allows to deal with the empty function too.
> Now you are asking for
> > > >
> > > > a logical expression to work on.
> > > >
> > > Which "logical expression" are you asking for?
> > >
> > ALL(a):[a in x => f(a) in x]
> >
> Actually, the theorem is
>
> AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).

Note that

AXAYAf: Ax(x e X -> f(x) e X) -> (f: X --> X )

does n o t hold. That's why MC stated:

> > Its utter nonsense, since:
> > ALL(a):[a in x => f(a) in x]
> > doesn't say f : x -> x.

and why your claim "They mean the same thing" is false.

Hint: Let f be the function f: IR --> IR defined with f(x) = x^2 for all x in IR. Now let X = {1}.

Then clearly Ax(x e X -> f(x) e X) (since 1^2 = 1). BUT f certainly isn't a function with domain {1}, since we defined f such that its domain is IR (and IR =/= {1}).

On Monday, April 18, 2022 at 8:46:39 PM UTC+2, Fritz Feldhase wrote:
> On Monday, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> > >
> > > Actually, the set theoretic approach is rather simple:
> > >
> > > 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} ("the value of f at x")
> > >
> > > No artificial restrictions at all: This approach allows to deal with the empty function too.
> > >
> Now you are asking for
> > > >
> > > > a logical expression to work on.
> > > >
> > > Which "logical expression" are you asking for?
> > >
> > ALL(a):[a in x => f(a) in x]
> >
> Actually, the theorem is
>
> AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).

Note that

AXAf: Ax(x e X -> f(x) e X) -> (f: X --> X)

does n o t hold. That's why MC stated:

> > Its utter nonsense, since:
> > ALL(a):[a in x => f(a) in x]
> > doesn't say f : x -> x.

and why your claim "They mean the same thing" is false.

Hint: Let f be the function f: IR --> IR defined with f(x) = x^2 for all x in IR. Now let X = {1}.

Then clearly Ax(x e X -> f(x) e X) (since 1^2 = 1). BUT f certainly isn't a function with domain {1}, since we defined f such that its domain is IR (and IR =/= {1}).

Maybe we should explain Dan Christensen what happens
with ~(a e dom(f)). Here is my guess, rather trivial:

ALL(a):[~(a e dom(f)) => ~EXIST(b):(a,b) e f]

And when we define f(a) as in Fritz we get, depends
on how f(a) is exactly defined:

ALL(a):[~(a e dom(f)) => f(a) = {}]

The later I am not 100% sure.

Fritz Feldhase schrieb am Montag, 18. April 2022 um 21:16:52 UTC+2:
> On Monday, April 18, 2022 at 8:46:39 PM UTC+2, Fritz Feldhase wrote:
> > On Monday, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> > > On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> > > >
> > > > Actually, the set theoretic approach is rather simple:
> > > >
> > > > 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} ("the value of f at x")
> > > >
> > > > No artificial restrictions at all: This approach allows to deal with the empty function too.
> > > >
> > Now you are asking for
> > > > >
> > > > > a logical expression to work on.
> > > > >
> > > > Which "logical expression" are you asking for?
> > > >
> > > ALL(a):[a in x => f(a) in x]
> > >
> > Actually, the theorem is
> >
> > AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).
> Note that
>
> AXAf: Ax(x e X -> f(x) e X) -> (f: X --> X)
>
> does n o t hold. That's why MC stated:
>
> > > Its utter nonsense, since:
> > > ALL(a):[a in x => f(a) in x]
> > > doesn't say f : x -> x.
> and why your claim "They mean the same thing" is false.
>
> Hint: Let f be the function f: IR --> IR defined with f(x) = x^2 for all x in IR. Now let X = {1}.
>
> Then clearly Ax(x e X -> f(x) e X) (since 1^2 = 1). BUT f certainly isn't a function with domain {1}, since we defined f such that its domain is IR (and IR =/= {1}).

It would also show that this is unfortunately wrong,
in the setting of Fritz, nothing to worry about, it must be
so, for both f and g satisfying function(f) and function(g):

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

The => direction is trivial, substitution, the other
direction, has a counter example, like for example:

f={(1,1),(2,{})} and g={(1,1)}

But on the other hand with Dan Christensens ad-hoc
axiom it follows from ALL(a):[f(a)=g(a)] that f=g.
Just use an arbitrary elemeint c, and dom={c}

and cod={f(c)}, we can use Dan Christensens ad-hoc
axiom to show f=g. So this is also something
that runs counter the usual set based functions,

and especially the problems defining f(a).

Mostowski Collapse schrieb am Montag, 18. April 2022 um 22:19:59 UTC+2:
> Maybe we should explain Dan Christensen what happens
> with ~(a e dom(f)). Here is my guess, rather trivial:
>
> ALL(a):[~(a e dom(f)) => ~EXIST(b):(a,b) e f]
>
> And when we define f(a) as in Fritz we get, depends
> on how f(a) is exactly defined:
>
> ALL(a):[~(a e dom(f)) => f(a) = {}]
>
> The later I am not 100% sure.
> Fritz Feldhase schrieb am Montag, 18. April 2022 um 21:16:52 UTC+2:
> > On Monday, April 18, 2022 at 8:46:39 PM UTC+2, Fritz Feldhase wrote:
> > > On Monday, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> > > > On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> > > > >
> > > > > Actually, the set theoretic approach is rather simple:
> > > > >
> > > > > 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} ("the value of f at x")
> > > > >
> > > > > No artificial restrictions at all: This approach allows to deal with the empty function too.
> > > > >
> > > Now you are asking for
> > > > > >
> > > > > > a logical expression to work on.
> > > > > >
> > > > > Which "logical expression" are you asking for?
> > > > >
> > > > ALL(a):[a in x => f(a) in x]
> > > >
> > > Actually, the theorem is
> > >
> > > AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).
> > Note that
> >
> > AXAf: Ax(x e X -> f(x) e X) -> (f: X --> X)
> >
> > does n o t hold. That's why MC stated:
> >
> > > > Its utter nonsense, since:
> > > > ALL(a):[a in x => f(a) in x]
> > > > doesn't say f : x -> x.
> > and why your claim "They mean the same thing" is false.
> >
> > Hint: Let f be the function f: IR --> IR defined with f(x) = x^2 for all x in IR. Now let X = {1}.
> >
> > Then clearly Ax(x e X -> f(x) e X) (since 1^2 = 1). BUT f certainly isn't a function with domain {1}, since we defined f such that its domain is IR (and IR =/= {1}).

On Monday, April 18, 2022 at 10:19:59 PM UTC+2, Mostowski Collapse wrote:

> Maybe we should explain Dan Christensen what happens
> with ~(a e dom(f)). Here is my guess, rather trivial:
>
> ALL(a):[~(a e dom(f)) => ~EXIST(b):(a,b) e f]

Right.

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

The other way round:

If Ey(<x, y> e f), then x e dom(f).

> And when we define f(a) as in Fritz we get [...]
>
> ALL(a):[~(a e dom(f)) => f(a) = {}]

Right (I'd say).

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

> The later I am not 100% sure

Same, same. So let's think about it.

If x is not in dom(f), then there's no y such that Ey(<x, y> e f) (see statement from above).

This means that the set {y e UUf : <x, y> e f} is empty, and hence U{y e UUf : <x, y> e f} is empty too.

Hence f(x) = {}. qed

On the other hand, we are't interested in f(x) for x !e dom(f). Hence there's no problem with that.

On Monday, April 18, 2022 at 10:27:35 PM UTC+2, Mostowski Collapse wrote:

> It would also show that this is unfortunately wrong,
> in the setting of Fritz, nothing to worry about, it must be
> so, for both f and g satisfying function(f) and function(g):
>
> f=g <=> ALL(a):[f(a) = g(a)]
>
> The => direction is trivial, substitution, the other
> direction, has a counter example, like for example:
>
> f={(1,1),(2,{})} and g={(1,1)}

Exaxctly.

Though for any two functions f, g (i. e. two sets f and g satisfying function(f) and function(g)):

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

> and especially the problems defining f(a).

Which isn't a problem at all in the context of the "set theoretic" approach.

(Of course, it can be done adopting, say, the iota-operator too.)

It seems to me that the "set theoretic" approach does not suffer from the may "problems" which arise from DC's approach (implemented in DC Spoof).

Next step: Functions a la Boubaki (based on the present approach).

Our aim: A theorem which states

AfAg(Function(f) & Function(g) --> (f = g <-> Dom(f) = Dom(g) & Cod(f) = Cod(g) & Ax e dom(f): f(x) = g(x))).

Simple...

Its a syntax problem also. Dan Christensen insists to use
the FOL function symbols f(a) notation. But in the FOL function
symbols f(a) notation, f is not an individual variable.

So what tool can you use, to redefine f(a), in what tool
is this possible. So my old proposal was to introduce
the so called Peano apostroph, and make a definition

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

Now there is a second problem. Dan Christensens tool
doesn't have := operator, it also doesn't have U operator,
it has something for pairs.

So I would say its insurmountable, giving proper treatment
to functions, DC Proof. Thats is a huge challenge...

See also:
The left apostrophe notation originated with Peano and
was adopted in Definition *30.01 of [WhiteheadRussell] p. 235,
Definition 10.11 of [Quine] p. 68, and Definition 6.11 of
[TakeutiZaring] p. 26. See df-fv 5930.
http://us.metamath.org/mpeuni/df-fv.html

But they do it yet slightly different, with Russell's definition
description binder, and in literature one finds also " (double
quote, not single quote) as an operator, for example used

by Gödel. I think Gödel used the Fritz definition. Have to check.

Fritz Feldhase schrieb am Montag, 18. April 2022 um 23:33:18 UTC+2:
> > and especially the problems defining f(a).
> Which isn't a problem at all in the context of the "set theoretic" approach.

On Monday, April 18, 2022 at 11:33:18 PM UTC+2, Fritz Feldhase wrote:

Correction: dom(f) > > > Dom(f)

> Our aim: A theorem which states
>
> AfAg(Function(f) & Function(g) --> (f = g <-> Dom(f) = Dom(g) & Cod(f) = Cod(g) & Ax e Dom(f): f(x) = g(x))).

We will follow the appoach due to Bourbaki.

On Monday, April 18, 2022 at 2:46:39 PM UTC-4, Fritz Feldhase wrote:
> On Monday, April 18, 2022 at 7:26:50 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 18, 2022 at 1:00:45 PM UTC-4, Fritz Feldhase wrote:
> > >
> > > Actually, the set theoretic approach is rather simple:
> > >
> > > 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} ("the value of f at x")
> > >
> > > No artificial restrictions at all: This approach allows to deal with the empty function too.

Now you are asking for

> > > >
> > > > a logical expression to work on.
> > > >
> > > Which "logical expression" are you asking for?
> > >

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

> You can't get that from "nothing", hence it's rather a "mathematical expression".
>

In DC Proof, you can introduce logical expression from (1) an axiom introduced the user, e.g .ALL(a):[a in n => s(a) in n] (Peano's Axioms), (2) from a premise, or (3) from an application of the Function Axiom.

> Actually the theorem is
>
> AXAf: (f: X --> X) -> Ax(x e X -> f(x) e X).
>

Not necessary in DC Proof.

> Or slightly more general
>
> AXAYAf: (f: X --> Y) -> Ax(x e X -> f(x) e Y).

> > Ultimately, it must come to this even with your "set theoretic" approach.
> Of course, so where do you see a problem? It follows from the definitions mentioned above (and some axioms of set theory).
>

From what appear to be unnecessary definitions that only complicate matters. There is, for example, no compelling need for a domain function.

> You see. we do not need any additional axioms concerning "functions" only SOME of the usual set theoretic axioms (actually the most basic of them) and some definitions.

We do not need your additional formal axioms for domain and codomain operators, etc.
> From this we get "identity of functions" as theorem as well as your "logical expression".
>

Given any non-empty set X, we can prove the existence of an identity function f:X --> X where f(x)=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 Monday, April 18, 2022 at 11:44:30 PM UTC+2, Mostowski Collapse wrote:

> Its a syntax problem also. Dan Christensen insists to use
> the FOL function symbols f(a) notation.

Well, what can he do? It's just usus to do so. You will find it in almost all textbooks.

> But in the FOL function symbols f(a) notation, f is not an individual variable.

Indeed. Actually, in the context of the "set theoretic approach" the symbols "f", "g", "h", etc. used in "f(x)", "g(y)", "h(x)" are "set variables", just like "x", "y", ... (if they aren't constants referring to certain sets), this way allowing for quantification:

Af(function(f) -> ...f...)

Ef(function(f) & ...f...)

> So what tool can you use, to redefine f(a), in what tool
> is this possible. So my old proposal was to introduce
> the so called Peano apostroph, and make a definition
>
> f'x := U{y e UUf : <x, y> e f}

Yes, why not. Though not that common.

Another notation seen in a paper by von Neumann, "[f, x]". So we might define:

[f, x] := U{y e UUf : <x, y> e f}.

We might call [. , .] the "application operator". :-)

> Now there is a second problem. Dan Christensens tool
> doesn't have := operator, it also doesn't have U operator,
> it has something for pairs.

Yes.

Definitions seem to be a problem in DC Proof.

How to introduce new "operation symbols", like "P" (for the power set), "U" for "union" etc.

> So I would say its insurmountable, giving proper treatment
> to functions, DC Proof. Thats is a huge challenge...

Agree. There would be ways, but... (say, implementing the iota-operator and allowing for definution via equations, etc.)

> See also:
> The left apostrophe notation originated with Peano and
> was adopted in Definition *30.01 of [WhiteheadRussell] p. 235,
> Definition 10.11 of [Quine] p. 68, and Definition 6.11 of
> [TakeutiZaring] p. 26. See df-fv 5930.
> http://us.metamath.org/mpeuni/df-fv.html
>
> But they do it yet slightly different, with Russell's definition
> description binder, and in literature one finds also " (double
> quote, not single quote) as an operator, for example used
> by Gödel. I think Gödel used the Fritz definition. " approach.

Guess so. Though I might have seen it in Kelley iirc.

There a further problem. He allows forming f(f), i.e.
self application. So he needs not only a definition
discipline, but also a typing discipline.

Because of well founded ness, in ZF, one cannot
have something else than f(f) = {}, with the Fritz application,
because if f(f) =\= {}, this would mean f e dom(f).

But a set which allows f e dom(f) is not well founded.
So regularity axiom is not present in DC Proof.
Although we might also say our sets can be irregular,

this is maybe not such a monster anymore, like it was
50 years ago. But its nevertheless fun to derive the following
in DC Proof, we a few simple illfounded definitions:

f(f) e f(f)

Fritz Feldhase schrieb am Dienstag, 19. April 2022 um 00:10:48 UTC+2:
> On Monday, April 18, 2022 at 11:44:30 PM UTC+2, Mostowski Collapse wrote:
>
> > Its a syntax problem also. Dan Christensen insists to use
> > the FOL function symbols f(a) notation.
> Well, what can he do? It's just usus to do so. You will find it in almost all textbooks.
> > But in the FOL function symbols f(a) notation, f is not an individual variable.
> Indeed. Actually, in the context of the "set theoretic approach" the symbols "f", "g", "h", etc. used in "f(x)", "g(y)", "h(x)" are "set variables", just like "x", "y", ... (if they aren't constants referring to certain sets), this way allowing for quantification:
>
> Af(function(f) -> ...f...)
>
> Ef(function(f) & ...f...)
> > So what tool can you use, to redefine f(a), in what tool
> > is this possible. So my old proposal was to introduce
> > the so called Peano apostroph, and make a definition
> >
> > f'x := U{y e UUf : <x, y> e f}
> Yes, why not. Though not that common.
>
> Another notation seen in a paper by von Neumann, "[f, x]". So we might define:
>
> [f, x] := U{y e UUf : <x, y> e f}.
>
> We might call [. , .] the "application operator". :-)
> > Now there is a second problem. Dan Christensens tool
> > doesn't have := operator, it also doesn't have U operator,
> > it has something for pairs.
> Yes.
>
> Definitions seem to be a problem in DC Proof.
>
> How to introduce new "operation symbols", like "P" (for the power set), "U" for "union" etc.
> > So I would say its insurmountable, giving proper treatment
> > to functions, DC Proof. Thats is a huge challenge...
> Agree. There would be ways, but... (say, implementing the iota-operator and allowing for definution via equations, etc.)
> > See also:
> > The left apostrophe notation originated with Peano and
> > was adopted in Definition *30.01 of [WhiteheadRussell] p. 235,
> > Definition 10.11 of [Quine] p. 68, and Definition 6.11 of
> > [TakeutiZaring] p. 26. See df-fv 5930.
> > http://us.metamath.org/mpeuni/df-fv.html
> >
> > But they do it yet slightly different, with Russell's definition
> > description binder, and in literature one finds also " (double
> > quote, not single quote) as an operator, for example used
> > by Gödel. I think Gödel used the Fritz definition. " approach..
>
> Guess so. Though I might have seen it in Kelley iirc.

On Monday, April 18, 2022 at 11:57:38 PM UTC+2, Dan Christensen wrote:
>
> Given any non-empty set X, we can prove the existence of an identity function f:X --> X where f(x)=x [for all x e X].

Indeed. Let X be a nonempty set. Now let f = {(x, x) : x e X}.

Then it's easy to show/prove

f: X --> X

as well as

Ax e X: f(x) = x,

where

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} ("the value of f at x")

Actually, the restriction that X is nonempty is unnecessary.

Hint: We can prove:

AXEf(f: X --> X & Ax e X: f(x) = x).

Though how do you define the statement "f: X --> X" ("f is a function from X to X") in DC Proof?

Fritz Feldhase <franz.fritschee.ff@gmail.com> writes:

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

This looks a little complicated but then I'm not sure where you are
starting from. But for reference, Shoenfield defines pairs (<x,y> =
{{x}, {x,y}}) and projections p1 and p2, and then says that a function f
is a set of pairs with the property that

f subset Ra(f) x Do(f)

and

<a,b> in f and <a',b> in f -> a = a'

where Do(f) = [p2(y) | y in f] and Ra(f) = [p1(y) | y in f].

Note that he uses the other order for the pairs.

Done like this, there is no definition of equality of functions other
than that of sets.

--
Ben.

On Tuesday, April 19, 2022 at 12:25:29 AM UTC+2, Mostowski Collapse wrote:

> There a further problem. He allows forming f(f), i.e.
> self application. So he needs not only a definition
> discipline, but also a typing discipline.

No problem with

f(x) := [f, x].

(if "function terms" like "f(x)" are not part of the original framework of FOPL we adopt as basis for our system. Avoiding a clash of notation this way.]

So we may consider

f(f) (or [f, f]).

I guess we will be able to prove

f(f) = {}

or at least

Af(function(f) -> f(f) = {}).

> Because of well founded ness, in ZF, one cannot
> have something else than f(f) = {}, with the Fritz application,
> because if f(f) =\= {}, this would mean f e dom(f).

Right.

> But a set which allows f e dom(f) is not well founded.
> So regularity axiom is not present in DC Proof.
> Although we might also say our sets can be irregular,
>
> this is maybe not such a monster anymore, like it was
> 50 years ago. But its nevertheless fun to derive the following
> in DC Proof, with a few simple illfounded definitions:
>
> f(f) e f(f)

Of course, "my" approach (with ZFC as background theory) would not alow for such a theorem. :-)

On Tuesday, April 19, 2022 at 12:28:06 AM UTC+2, Ben wrote:
> Fritz Feldhase <franz.fri...@gmail.com> writes:
>
> > 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)))).
> >
> This looks a little complicated

because it is/was

I've simplified it now:

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}

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

> but then I'm not sure where you are
> starting from. But for reference, Shoenfield defines pairs (<x,y> =
> {{x}, {x,y}}) and projections p1 and p2, and then says that a function f
> is a set of pairs with the property that
>
> f subset Ra(f) x Do(f)
>
> and
>
> <a,b> in f and <a',b> in f -> a = a'
>
> where Do(f) = [p2(y) | y in f] and Ra(f) = [p1(y) | y in f].
>
> Note that he uses the other order for the pairs.
>
> Done like this, there is no definition of equality of functions other
> than that of sets.

Right. I'd say, my approach mentioned above is "essentialy" the same (modulo some technical details).

I'd say its the "standard appoach" in textbooks if these type (as you mentioned).