Following is a simple example of how a function is constructed in DC Proof--not just defined, but formally proven to exist.

Dan

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

THEOREM

On every non-empty set, there exists a unique identity function. In other words, there exists an identity function on that set, and it does not differ from any other identity function on that set. Formally:

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]

=> ALL(a):[a in x => id'(a)=id(a)]]]]

OUTLINE OF PROOF

Given a non-empty set x.

1. Construct the Cartesian product of x with itself (x2). (Lines 3-11)

2. Construct the subset g of x2, the graph of the required function. (Lines 12-15)

3. Apply the Function Axiom to obtain the sufficient conditions for the functionality of g. (Lines 16-24)

4. Show that each of these conditions hold. (Lines 25-78)

5. Define the required function id in terms of g. (Lines 79-80)

6. Show that ALL(a):[a in x => id(a)=a]. Lines(81-101)

7. Show that if ALL(a):[a in x => id'(a)=a], then ALL(a):[a in x => id'(a)=id(a)]. (Lines 102-109)

PROOF (Full Text)

https://dcproof.com/IdentityFunctionUniqueV2.htm (112 lines)

Dont be victim of fake DC poop. He cannot prove,

ALL(f):EXIST(y):ALL(a):[f(a) e y]

Yet he claims his function symbols would be
those found in mathematics in expressions such
as f : X -> Y where X and Y are sets.

Dan Christensen schrieb am Montag, 25. April 2022 um 06:34:33 UTC+2:
> Following is a simple example of how a function is constructed in DC Proof--not just defined, but formally proven to exist.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>
> THEOREM
>
> On every non-empty set, there exists a unique identity function. In other words, there exists an identity function on that set, and it does not differ from any other identity function on that set. Formally:
>
> 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]
>
> => ALL(a):[a in x => id'(a)=id(a)]]]]
>
> OUTLINE OF PROOF
>
> Given a non-empty set x.
>
> 1. Construct the Cartesian product of x with itself (x2). (Lines 3-11)
>
> 2. Construct the subset g of x2, the graph of the required function. (Lines 12-15)
>
> 3. Apply the Function Axiom to obtain the sufficient conditions for the functionality of g. (Lines 16-24)
>
> 4. Show that each of these conditions hold. (Lines 25-78)
>
> 5. Define the required function id in terms of g. (Lines 79-80)
>
> 6. Show that ALL(a):[a in x => id(a)=a]. Lines(81-101)
>
> 7. Show that if ALL(a):[a in x => id'(a)=a], then ALL(a):[a in x => id'(a)=id(a)]. (Lines 102-109)
>
> PROOF (Full Text)
>
> https://dcproof.com/IdentityFunctionUniqueV2.htm (112 lines)

Its easy to prove with Fritz application.
Just observe for Fritz application:

f(a) = b if (a,b) e f
= {} otherwise

Now to prove the theorem just use
y = img(f) u {{}}.

Mostowski Collapse schrieb am Dienstag, 26. April 2022 um 13:18:50 UTC+2:
> Dont be victim of fake DC poop. He cannot prove,
>
> ALL(f):EXIST(y):ALL(a):[f(a) e y]
>
> Yet he claims his function symbols would be
> those found in mathematics in expressions such
> as f : X -> Y where X and Y are sets.
> Dan Christensen schrieb am Montag, 25. April 2022 um 06:34:33 UTC+2:
> > Following is a simple example of how a function is constructed in DC Proof--not just defined, but formally proven to exist.
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> >
> >
> > THEOREM
> >
> > On every non-empty set, there exists a unique identity function. In other words, there exists an identity function on that set, and it does not differ from any other identity function on that set. Formally:
> >
> > 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]
> >
> > => ALL(a):[a in x => id'(a)=id(a)]]]]
> >
> > OUTLINE OF PROOF
> >
> > Given a non-empty set x.
> >
> > 1. Construct the Cartesian product of x with itself (x2). (Lines 3-11)
> >
> > 2. Construct the subset g of x2, the graph of the required function. (Lines 12-15)
> >
> > 3. Apply the Function Axiom to obtain the sufficient conditions for the functionality of g. (Lines 16-24)
> >
> > 4. Show that each of these conditions hold. (Lines 25-78)
> >
> > 5. Define the required function id in terms of g. (Lines 79-80)
> >
> > 6. Show that ALL(a):[a in x => id(a)=a]. Lines(81-101)
> >
> > 7. Show that if ALL(a):[a in x => id'(a)=a], then ALL(a):[a in x => id'(a)=id(a)]. (Lines 102-109)
> >
> > PROOF (Full Text)
> >
> > https://dcproof.com/IdentityFunctionUniqueV2.htm (112 lines)

On Tuesday, April 26, 2022 at 7:26:45 AM UTC-4, Mostowski Collapse wrote:
> Its easy to prove with Fritz application.
> Just observe for Fritz application:
>
> f(a) = b if (a,b) e f
> = {} otherwise
>
> Now to prove the theorem just use
> y = img(f) u {{}}.

STILL waiting your proof--a formal derivation using some known set theory and system of natural deduction. Not possible??? Oh, well...

Dan

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

Its very easy:

First prove f(a) e img(f) u {{}} with f(a) the Fritz definition.
Then prove ALL(a):ALL(a):[f(a) e img(f) u {{}}]
Then prove EXIST(y):ALL(a):[f(a) e y]
Then prove ALL(f): EXIST(y):ALL(a):[f(a) e y]

Whats the prolololoblem?

Dan Christensen schrieb am Dienstag, 26. April 2022 um 15:08:35 UTC+2:
> On Tuesday, April 26, 2022 at 7:26:45 AM UTC-4, Mostowski Collapse wrote:
> > Its easy to prove with Fritz application.
> > Just observe for Fritz application:
> >
> > f(a) = b if (a,b) e f
> > = {} otherwise
> >
> > Now to prove the theorem just use
> > y = img(f) u {{}}.
> STILL waiting your proof--a formal derivation using some known set theory and system of natural deduction. Not possible??? Oh, well...
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, April 26, 2022 at 9:35:30 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 26. April 2022 um 15:08:35 UTC+2:
> > On Tuesday, April 26, 2022 at 7:26:45 AM UTC-4, Mostowski Collapse wrote:
> > > Its easy to prove with Fritz application.
> > > Just observe for Fritz application:
> > >
> > > f(a) = b if (a,b) e f
> > > = {} otherwise
> > >
> > > Now to prove the theorem just use
> > > y = img(f) u {{}}.
> > STILL waiting your proof--a formal derivation using some known set theory and system of natural deduction. Not possible??? Oh, well...

> Its very easy:
>
> First prove f(a) e img(f) u {{}} with f(a) the Fritz definition.

Please do so.

> Then prove ALL(a):ALL(a):[f(a) e img(f) u {{}}]

Likewise.

> Then prove EXIST(y):ALL(a):[f(a) e y]
> Then prove ALL(f): EXIST(y):ALL(a):[f(a) e y]
>

Umm... Guessing that you are unable to actually prove your outrageous claim as required.

> Whats the prolololoblem?

The problem is, you don't have a proof as required, Jan Burse. Oh, well...

Dan

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

On Tuesday, April 26, 2022 at 12:53:25 PM UTC-4, Dan Christensen wrote:
> On Tuesday, April 26, 2022 at 9:35:30 AM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Dienstag, 26. April 2022 um 15:08:35 UTC+2:
> > > On Tuesday, April 26, 2022 at 7:26:45 AM UTC-4, Mostowski Collapse wrote:
> > > > Its easy to prove with Fritz application.
> > > > Just observe for Fritz application:
> > > >
> > > > f(a) = b if (a,b) e f
> > > > = {} otherwise
> > > >
> > > > Now to prove the theorem just use
> > > > y = img(f) u {{}}.
> > > STILL waiting your proof--a formal derivation using some known set theory and system of natural deduction. Not possible??? Oh, well...
> > Its very easy:
> >
> > First prove f(a) e img(f) u {{}} with f(a) the Fritz definition.
> Please do so.
> > Then prove ALL(a):ALL(a):[f(a) e img(f) u {{}}]
> Likewise.
> > Then prove EXIST(y):ALL(a):[f(a) e y]
> > Then prove ALL(f): EXIST(y):ALL(a):[f(a) e y]
> >
> Umm... Guessing that you are unable to actually prove your outrageous claim as required.
>
> > Whats the prolololoblem?
>
> The problem is, you don't have a proof as required, Jan Burse. Oh, well...

Based on your comments here and in other threads, I'm guessing you may be talking about the image of the domain of a function (or its range). Maybe you will find this proof useful:

1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
Premise

2. Set(x)
Split, 1

3. Set(y)
Split, 1

4. ALL(a):[a in x => f(a) in y]
Split, 1

5. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in y & EXIST(b):[b in x & f(b)=a]]]
Subset, 3

6. Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]
E Spec, 5

7. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
=> EXIST(imgx):[Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]]]
Conclusion, 1

Dan

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

On Tuesday, April 26, 2022 at 6:53:25 PM UTC+2, Dan Christensen wrote:
> On Tuesday, April 26, 2022 at 9:35:30 AM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Dienstag, 26. April 2022 um 15:08:35 UTC+2:
> > > On Tuesday, April 26, 2022 at 7:26:45 AM UTC-4, Mostowski Collapse wrote:
> > > > Its easy to prove with Fritz application.
> > > > Just observe for Fritz application:
> > > >
> > > > f(a) = b if (a,b) e f
> > > > = {} otherwise
> > > >
> > > > Now to prove the theorem just use
> > > > y = img(f) u {{}}.
> > > STILL waiting your proof--a formal derivation using some known set theory and system of natural deduction. Not possible??? Oh, well...
> > Its very easy:
> >
> > First prove f(a) e img(f) u {{}} with f(a) the Fritz definition.
> Please do so.
> > Then prove ALL(a):ALL(a):[f(a) e img(f) u {{}}]
> Likewise.
> > Then prove EXIST(y):ALL(a):[f(a) e y]
> > Then prove ALL(f): EXIST(y):ALL(a):[f(a) e y]
> >
> Umm... Guessing that you are unable to actually prove your outrageous claim as required.
>
> > Whats the prolololoblem?
>
> The problem is, you don't have a proof as required, Jan Burse. Oh, well...
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Its not useful. The idea is to prove this:

ALL(f): EXIST(y):ALL(a):[f(a) e y]

You cannot prove it in DC Proof. Because the above theorem
doesn't work for when f is a proper class. When f is a proper class,
then there is no y. On the other hand when f is a set,

you can prove it. And then prove will not be logical or using
only the comprehension axiom of set theory. You need slightly
more set theory to prove it.

Dan Christensen schrieb am Dienstag, 26. April 2022 um 21:42:02 UTC+2:
> Based on your comments here and in other threads, I'm guessing you may be talking about the image of the domain of a function (or its range). Maybe you will find this proof useful:
>
> 1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> Premise
>
> 2. Set(x)
> Split, 1
>
> 3. Set(y)
> Split, 1
>
> 4. ALL(a):[a in x => f(a) in y]
> Split, 1
>
> 5. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in y & EXIST(b):[b in x & f(b)=a]]]
> Subset, 3
>
> 6. Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]
> E Spec, 5
>
> 7. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> => EXIST(imgx):[Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]]]
> Conclusion, 1
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

There are some proper classes f where img(f) is
also set. But then there are some proper classes
where img(f) is not a set. So you cannot prove

this in DC Proof, its not provable:

ALL(f): EXIST(y):ALL(a):[f(a) e y]

Example of an f where img(f) is not a set, is
the f such that ALL(a):[f(a)=a], the identity function.
An example where f is a proper class, and img(f)

is nevertheless a set, is the f such that
ALL(a):[f(a)=c], a constant function.

Have Fun!

Mostowski Collapse schrieb am Dienstag, 26. April 2022 um 23:04:11 UTC+2:
> Its not useful. The idea is to prove this:
> ALL(f): EXIST(y):ALL(a):[f(a) e y]
> You cannot prove it in DC Proof. Because the above theorem
> doesn't work for when f is a proper class. When f is a proper class,
> then there is no y. On the other hand when f is a set,
>
> you can prove it. And then prove will not be logical or using
> only the comprehension axiom of set theory. You need slightly
> more set theory to prove it.
> Dan Christensen schrieb am Dienstag, 26. April 2022 um 21:42:02 UTC+2:
> > Based on your comments here and in other threads, I'm guessing you may be talking about the image of the domain of a function (or its range). Maybe you will find this proof useful:
> >
> > 1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > Premise
> >
> > 2. Set(x)
> > Split, 1
> >
> > 3. Set(y)
> > Split, 1
> >
> > 4. ALL(a):[a in x => f(a) in y]
> > Split, 1
> >
> > 5. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in y & EXIST(b):[b in x & f(b)=a]]]
> > Subset, 3
> >
> > 6. Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]
> > E Spec, 5
> >
> > 7. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > => EXIST(imgx):[Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]]]
> > Conclusion, 1
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, April 26, 2022 at 5:04:11 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 26. April 2022 um 21:42:02 UTC+2:
> > Based on your comments here and in other threads, I'm guessing you may be talking about the image of the domain of a function (or its range). Maybe you will find this proof useful:
> >
> > 1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > Premise
> >
> > 2. Set(x)
> > Split, 1
> >
> > 3. Set(y)
> > Split, 1
> >
> > 4. ALL(a):[a in x => f(a) in y]
> > Split, 1
> >
> > 5. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in y & EXIST(b):[b in x & f(b)=a]]]
> > Subset, 3
> >
> > 6. Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]
> > E Spec, 5
> >
> > 7. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > => EXIST(imgx):[Set(imgx) & ALL(a):[a in imgx <=> a in y & EXIST(b):[b in x & f(b)=a]]]]
> > Conclusion, 1

> Its not useful. The idea is to prove this:
> ALL(f): EXIST(y):ALL(a):[f(a) e y]
> You cannot prove it in DC Proof.

Why would I want to prove such nonsense? I would be worried if I could prove it. Somehow, you need to restrict each of these quantifiers.

ALL(f):[F(f) => EXIST(y):[Y(y) & ALL(a):[A(a) => P(f,y,a)]]] some predicates F, Y and A.

> Because the above theorem
> doesn't work for when f is a proper class. When f is a proper class,
> then there is no y. On the other hand when f is a set,
>

KISS! There is no need for classes other than sets here.

Dan

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

Well the point is, if you cannot prove:

ALL(f): EXIST(y):ALL(a):[f(a) e y]

Then your function symbols are classes.

Got it?

Dan Christensen schrieb am Mittwoch, 27. April 2022 um 00:30:17 UTC+2:
> KISS! There is no need for classes other than sets here.

On Tuesday, April 26, 2022 at 7:49:06 PM UTC-4, Mostowski Collapse wrote:
> Well the point is, if you cannot prove:
> ALL(f): EXIST(y):ALL(a):[f(a) e y]

If I could, it would be a serious bug that I would need to fix.

> Then your function symbols are classes.
>

Either that or your "theorem" here is utter nonsense. (My vote.)

Dan

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

On Tuesday, April 26, 2022 at 11:04:11 PM UTC+2, Mostowski Collapse wrote:
>
> The idea is to prove this:
> ALL(f): EXIST(y):ALL(a):[f(a) e y]

Nice.

The proof for the following

ALL(f): function(f) -> EXIST(y):ALL(a):[f(a) e y]

is quite simple (if not trivial), I'd say.

For any function f "obviosly" Ax(x e dom(f) -> f(x) e img(f)). Moreover Ax(x !e dom(f): f(x) = {}) hence Ax(x e img(f) u {{}}). with other words, EXIST(y):ALL(a):[f(a) e y]. Simple as that. (You already mentioned that simple fact.)

It seems to me that the proof without restricting f to functions is harder.

> [...] You need slightly more set theory to prove it.

Guess so.

On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
>
> If I could, it would be a serious bug that I would need to fix.

The bug is in your head. You clearly do not understand "functions".

On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> >
> > If I could, it would be a serious bug that I would need to fix.
> The bug is in your head. You clearly do not understand "functions".

Are there non-surjective functions with your understanding of functions? There is in mine.

Dan

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

On Tuesday, April 26, 2022 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > >
> > > If I could, it would be a serious bug that I would need to fix.
> > The bug is in your head. You clearly do not understand "functions".
> Are there non-surjective functions with your understanding of functions? There is in mine.

The successor function in Peano's Axioms, for example, is non-surjective.

1. 0 in n
2. ALL(a):[a in n => s(a) in n]
3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n
etc.

Where:
n = the set of natural numbers
s = the successor function on n

How would you handle it in your system where IIUC all functions are surjective? Von Neumann ordinals are out the question in my system. As in the vast majority of math textbooks.

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

On Wednesday, April 27, 2022 at 3:12:05 AM UTC+2, Dan Christensen wrote:
> On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > >
> > > If I could, it would be a serious bug that I would need to fix.
> > >
> > The bug is in your head. You clearly do not understand "functions".
> >
> Are there non-surjective functions with your understanding of functions? There is in mine.

It's SLIGHTLY complicated. (Why s h o u l d it be easy?)

The "function concept" in set theory (usually) differs slightly from that in "math". I already told you that.

For "set theoretic functions" f, g we have f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)), for "mathematical functions" (a la Bourbaki) we have f = g <-> dom(f) = dom(g) & codom(f) = codom(g) & Ax(x e dom(f) -> f(x) = g(x)). (Of course "mathematical functions" can be defined as sets too. See Bourbaki.)

Set theoretic functions have a domain and an image, but no codomain. In other words, we can define the operators dom() and img() for them, but not (in a sensible way) cod().

On the other hand, a mathematical function f has the domain dom(f), the image img(f) and the codomain cod(f). Hence we can define the property of "surjectivity" for them: surjective(f) :<-> img(f) = cod(f).

In the context of "set theoreric functions" we may say that they are functions "in" some set Y iff img(f) c Y and functions "onto" some set Y iff img(f) = Y. But f (a certain set of ordered pairs) does not have an "intrinsic" property we might to call its "codomain" (as we do for "mathematical functions". The definition cod(f) := img(f) doesn't make much sense, imho. Yeah, in this case every function would be "surjective", which is nonsense.)

On Wednesday, April 27, 2022 at 10:49:00 AM UTC+2, Dan Christensen wrote:
> On Tuesday, April 26, 2022 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> > On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > > >
> > > > If I could, it would be a serious bug that I would need to fix.
> > > The bug is in your head. You clearly do not understand "functions".
> > Are there non-surjective functions with your understanding of functions? There is in mine.
> The successor function in Peano's Axioms, for example, is non-surjective.
>
> 1. 0 in n
> 2. ALL(a):[a in n => s(a) in n]
> 3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n
> etc.
>

Yes.

> Where:
> n = the set of natural numbers
> s = the successor function on n

Yes.

> How would you handle it in your system [...]?

When we deal with "set theoretic functions" we may define the notion

surjektive_relative_to(f, Y) :<-> img(f) = Y

for functions f.

Then we may claim that the function f is a surjection from X onto Y iff dom(f) = X & surjektive_relative_to(f, Y).

surjection_from_onto(f, X, Y) :<-> dom(f) = X & surjektive_relative_to(f, Y).

Now we can derive, for example, ~surjection_from_onto(s, IN, IN).

The "problem" of this approach is that "surjectivity" is not a property of the function "allone".

Hence we can't derive (in a sensible way) something like ~surjective(s) here.

(Adopting the "mathematical approach" this is possible.

What happened to the Dan-O-Matik rule, all
quantifiers must be relative to some predication.
The first thing Wikipedia tells me, the usual

formalization would be not ALL(a):[~s(a)=0]:

ALL(a):[a e N => ~s(a)=0]
https://de.wikipedia.org/wiki/Peano-Axiome#Urspr%C3%BCngliche_Formalisierung

This is the cludge you need, to talk about function
symbols f, if you don't have a proper treatment of
f : N->N, you always need to relativize. The proposed

axioms of Wikipedia do not show a proper
treatment of the mapping s : N -> N, for example
they only state:

ALL(a):[a e N => s(a) e N]
https://de.wikipedia.org/wiki/Peano-Axiome#Urspr%C3%BCngliche_Formalisierung

And they use a FOL function symbol. This is because
Peano stuff is pre-modern Set Theory. The German
Wikipedia says "Ursprüngliche Formulierung", i.e.

original formulation. And most of the time these cludges
work. Sometimes they don't work. Deriving DC Proof from
pre-modern Set Theory does of course break hell loose.

You just get shaky stuff on missing foundation. If something
on Wikipedia says "Ursprüngliche Formulierung", i.e.
original formulation, you should spam sci.math and sci.logic

with it. You are just propelling ancient nonsense. Study
what Coq and Isabelle/HOL do. You end up type theoretic
approaches. Or what modern set-theory does, which

avoids types. Or explain what DC poop does.

Dan Christensen schrieb am Mittwoch, 27. April 2022 um 10:49:00 UTC+2:
> 3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n

Corr.: The word "not" was missing

Mostowski Collapse schrieb am Mittwoch, 27. April 2022 um 22:37:18 UTC+2:
> You just get shaky stuff on missing foundation. If something
> on Wikipedia says "Ursprüngliche Formulierung", i.e.
> original formulation, you should not spam sci.math and sci.logic
>
> with it. You are just propelling ancient nonsense. Study
> what Coq and Isabelle/HOL do. You end up type theoretic
> approaches. Or what modern set-theory does, which
>
> avoids types. Or explain what DC poop does.
>
> Dan Christensen schrieb am Mittwoch, 27. April 2022 um 10:49:00 UTC+2:
> > 3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n

On Wednesday, April 27, 2022 at 4:26:04 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 27, 2022 at 10:49:00 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, April 26, 2022 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> > > On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > > > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > > > >
> > > > > If I could, it would be a serious bug that I would need to fix.
> > > > The bug is in your head. You clearly do not understand "functions".
> > > Are there non-surjective functions with your understanding of functions? There is in mine.
> > The successor function in Peano's Axioms, for example, is non-surjective.
> >
> > 1. 0 in n
> > 2. ALL(a):[a in n => s(a) in n]
> > 3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n
> > etc.
> >
> Yes.
> > Where:
> > n = the set of natural numbers
> > s = the successor function on n
> Yes.
>
> > How would you handle it in your system [...]?
>
> When we deal with "set theoretic functions" we may define the notion
>
> surjektive_relative_to(f, Y) :<-> img(f) = Y
>

Can you ever have non-surjective functions in your system?
More sensible might be:

ALL(f):ALL(x):ALL(y):[Set(x) & Set(y) & EXIST(a):a in x & EXIST(a):a in y & ALL(a):[a in x => f(a) in x]

=> [Surjective(f,x,y) <=> EXIST(a):[a in y & ALL(b):[b in x => ~f(b)=a]]]]

> for functions f.
>
> Then we may claim that the function f is a surjection from X onto Y iff dom(f) = X & surjektive_relative_to(f, Y).
>
> surjection_from_onto(f, X, Y) :<-> dom(f) = X & surjektive_relative_to(f, Y).
>
> Now we can derive, for example, ~surjection_from_onto(s, IN, IN).
>
> The "problem" of this approach is that "surjectivity" is not a property of the function "allone".
>
> Hence we can't derive (in a sensible way) something like ~surjective(s) here.
>

It is trivial to show that the successor function on N (in Peano's Axioms) is not surjective.

Dan

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

On Wednesday, April 27, 2022 at 4:26:04 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 27, 2022 at 10:49:00 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, April 26, 2022 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> > > On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > > > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > > > >
> > > > > If I could, it would be a serious bug that I would need to fix.
> > > > The bug is in your head. You clearly do not understand "functions".
> > > Are there non-surjective functions with your understanding of functions? There is in mine.
> > The successor function in Peano's Axioms, for example, is non-surjective.
> >
> > 1. 0 in n
> > 2. ALL(a):[a in n => s(a) in n]
> > 3. ALL(a):~[s(a)=0] <--- non-surjective function s: n --> n
> > etc.
> >
> Yes.
> > Where:
> > n = the set of natural numbers
> > s = the successor function on n
> Yes.
>
> > How would you handle it in your system [...]?
>
> When we deal with "set theoretic functions" we may define the notion
>
> surjektive_relative_to(f, Y) :<-> img(f) = Y
>

Can you ever have non-surjective functions in your system?

More sensible might be:

ALL(f):ALL(x):ALL(y):[Set(x) & Set(y) & EXIST(a):a in x & EXIST(a):a in y & ALL(a):[a in x => f(a) in x]

=> [Surjective(f,x,y) <=> EXIST(a):[a in y & ALL(b):[b in x => ~f(b)=a]]]]

> for functions f.
>
> Then we may claim that the function f is a surjection from X onto Y iff dom(f) = X & surjektive_relative_to(f, Y).
>
> surjection_from_onto(f, X, Y) :<-> dom(f) = X & surjektive_relative_to(f, Y).
>
> Now we can derive, for example, ~surjection_from_onto(s, IN, IN).
>
> The "problem" of this approach is that "surjectivity" is not a property of the function "allone".
>
> Hence we can't derive (in a sensible way) something like ~surjective(s) here.
>

Using the standard definition (see above), it is trivial to show that the successor function S on N (in Peano's Axioms) is not surjective, i.e. that ~Surjective(S, N, N).

Dan

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

On Wednesday, April 27, 2022 at 4:26:04 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, April 27, 2022 at 10:49:00 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, April 26, 2022 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> > > On Tuesday, April 26, 2022 at 8:39:31 PM UTC-4, Fritz Feldhase wrote:
> > > > On Wednesday, April 27, 2022 at 2:20:12 AM UTC+2, Dan Christensen wrote:
> > > > >
> > > > > If I could, it would be a serious bug that I would need to fix.
> > > > The bug is in your head. You clearly do not understand "functions".
> > > Are there non-surjective functions with your understanding of functions? There is in mine.
> > The successor function in Peano's Axioms, for example, is non-surjective.
> >
> > 1. 0 in n
> > 2. ALL(a):[a in n => s(a) in n]
> > 3. ALL(a):[a in n => ~s(a)=0] <--- non-surjective function s: n --> n
> > etc.
> >
> Yes.
> > Where:
> > n = the set of natural numbers
> > s = the successor function on n
> Yes.
>
> > How would you handle it in your system [...]?
>
> When we deal with "set theoretic functions" we may define the notion
>
> surjektive_relative_to(f, Y) :<-> img(f) = Y
>

Can you ever have non-surjective functions in your system?

More sensible might be:

ALL(f):ALL(x):ALL(y):[Set(x) & Set(y) & EXIST(a):a in x & EXIST(a):a in y & ALL(a):[a in x => f(a) in x]

=> [Surjective(f,x,y) <=> ALL(a):[a in y => EXIST(b):[b in x & f(b)=a]]]]

> for functions f.
>
> Then we may claim that the function f is a surjection from X onto Y iff dom(f) = X & surjektive_relative_to(f, Y).
>
> surjection_from_onto(f, X, Y) :<-> dom(f) = X & surjektive_relative_to(f, Y).
>
> Now we can derive, for example, ~surjection_from_onto(s, IN, IN).
>
> The "problem" of this approach is that "surjectivity" is not a property of the function "allone".
>
> Hence we can't derive (in a sensible way) something like ~surjective(s) here.
>

A serious limitation, don't you think?

Using the standard definition (see above), it is trivial to show that the successor function S on N (in Peano's Axioms) is not surjective, i.e. that ~Surjective(S, N, N).

PROOF (skipping some details):

Define: Surjective( )

1. ALL(f):ALL(x):ALL(y):[Set(x) & Set(y) & EXIST(a):a in x & EXIST(a):a in y & ALL(a):[a in x => f(a) in x]
=> [Surjective(f,x,y) <=> ALL(a):[a in y => EXIST(b):[b in x & f(b)=a]]]]
Axiom

2. Set(n)
Axiom

Three Peano Axioms

3. 0 in n
Axiom

4. ALL(a):[a in n => s(a) in n]
Axiom

5. ALL(a):[a in n => ~s(a)=0]
Axiom

[...]

From definition of Surjective(s,n,n)

14. Surjective(s,n,n) <=> ALL(a):[a in n => EXIST(b):[b in n & s(b)=a]]
Detach, 9, 13

[...]

From the contrapositive...

25. EXIST(a):[a in n & ALL(b):[b in n => ~s(b)=a]] => ~Surjective(s,n,n)
Rem DNeg, 24

[...]

Sufficient condition:

27. EXIST(a):[a in n & ALL(b):[b in n => ~s(b)=a]]
E Gen, 26
[...]

As Required:

28. ~Surjective(s,n,n)
Detach, 25, 27

Dan

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

On Thursday, April 28, 2022 at 4:18:16 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 27, 2022 at 4:26:04 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, April 27, 2022 at 10:49:00 AM UTC+2, Dan Christensen wrote:
> > >
> > > The successor function in Peano's Axioms, for example, is non-surjective.
> > >
> > > 1. 0 in n
> > > 2. ALL(a):[a in n => s(a) in n]
> > > 3. ALL(a):[a in n => ~s(a)=0] <--- non-surjective function s: n --> n
> > > etc.
> > >
> > Yes.
> >
> > > Where:
> > > n = the set of natural numbers
> > > s = the successor function on n
> > >
> > Yes.
> >
> > > How would you handle it in your system [...]?
> >
> > When we deal with "set theoretic functions" we may define the notion
> >
> > onto(f, Y) :<-> img(f) = Y
> >
> Can you ever have non-surjective functions in your system?

Just read on.

> > Then we may claim that the function f is a surjection from X onto Y iff dom(f) = X & onto(f, Y).

Got that? Again:

surjection(f, X, Y) :<-> dom(f) = X & onto(f, Y).

> > Now we can derive, for example, ~surjection(s, IN, IN).
> >
> > The "problem" of this approach is that "surjectivity" is not a property of the function "allone".
> >
> > Hence we can't derive (in a sensible way) something like ~surjective(s) here.
> >
> A serious limitation, don't you think?

No, it isn't. Read on.

> Using [DC Proof's] definition[s] it is trivial to show that the successor function S on N (in Peano's Axioms) is not surjective, i.e. that ~Surjective(S, N, N).

So what? The VERY SAME can be done in the (quite standard) "set theoretic" approach just mentioned above.

It's TRIVIAL to prove ~surjection(s, IN, IN).

So we may define for functions f:

injection(f) := AxAy(x e dom(f) & y e dom(f) & f(x) = f(y) -> x = y)
surjection(f, X, Y) :<-> dom(f) = X & img(f) = Y
bijection(f, X, Y) :<-> injection(f) & surjection(f, X, Y).

Too complicated for you to comprehend?

In addition we may define:

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

Useful for proofs concerning functions.