RECALL:

A function is often represented as a set of ordered pairs.

Example: Function f = {(0, 0), (1,2), (2, 4)}

The domain of f in this case would be {0, 1, 2}.

The range would be {0, 2, 4}.

The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.

Using the standard function notation, we can write:

f(0) = 0, f(1) = 2 and f(2) = 4

Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:

f = {(a, b) : a in X & b in Y & F(a,b)}

where F is a suitable binary predicate.

Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).

Alternatively, we could write as follows use predicate logic:

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

BURSE'S PARADOX

If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.

We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:

(2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]

Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.

(To be continued)

Comments 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

You can make the "paradox" stronger. Not only outside the
domain, also outside the codomain. Here is the proof
sketch for the butterfly color paradox.

The rest is relatively easy, take some h e F,
you can construct this set:

H = { (x,y) | x e butterfly & y e color & g(x)=y }

Now by Russell construction there is an a,
with ~(a e butterfly) and by the same construction
there is some a b, with ~(b e color).

Now construct this set:

G = H u { (a,b) }

By your Function Axiom there is a function g.
Its easy to show:

i) g e F
ii) ~g(a) e color

Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .

Q.E.D.

Dan Christensen schrieb am Montag, 17. Januar 2022 um 23:24:54 UTC+1:
> RECALL:
>
> A function is often represented as a set of ordered pairs.
>
> Example: Function f = {(0, 0), (1,2), (2, 4)}
>
> The domain of f in this case would be {0, 1, 2}.
>
> The range would be {0, 2, 4}.
>
> The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
>
> Using the standard function notation, we can write:
>
> f(0) = 0, f(1) = 2 and f(2) = 4
>
> Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
>
> f = {(a, b) : a in X & b in Y & F(a,b)}
>
> where F is a suitable binary predicate.
>
> Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
>
> Alternatively, we could write as follows use predicate logic:
>
> (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
>
> BURSE'S PARADOX
>
> If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
>
> We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
>
> (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
>
> Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
>
> (To be continued)
>
> Comments 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

On Monday, January 17, 2022 at 5:35:12 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 17. Januar 2022 um 23:24:54 UTC+1:
> > RECALL:
> >
> > A function is often represented as a set of ordered pairs.
> >
> > Example: Function f = {(0, 0), (1,2), (2, 4)}
> >
> > The domain of f in this case would be {0, 1, 2}.
> >
> > The range would be {0, 2, 4}.
> >
> > The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
> >
> > Using the standard function notation, we can write:
> >
> > f(0) = 0, f(1) = 2 and f(2) = 4
> >
> > Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
> >
> > f = {(a, b) : a in X & b in Y & F(a,b)}
> >
> > where F is a suitable binary predicate.
> >
> > Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
> >
> > Alternatively, we could write as follows use predicate logic:
> >
> > (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
> >
> > BURSE'S PARADOX
> >
> > If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
> >
> > We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
> >
> > (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
> >
> > Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
> >
> > (To be continued)
> >
> > Comments so far?
> >
> >

> You can make the "paradox" stronger. Not only outside the
> domain, also outside the codomain.

Not necessary here.

> Here is the proof
> sketch for the butterfly color paradox.
>
> The rest is relatively easy, take some h e F,
> you can construct this set:
>
> H = { (x,y) | x e butterfly & y e color & g(x)=y }
>
> Now by Russell construction there is an a,
> with ~(a e butterfly) and by the same construction
> there is some a b, with ~(b e color).
>
> Now construct this set:
>
> G = H u { (a,b) }
>
> By your Function Axiom there is a function g.
> Its easy to show:
>
> i) g e F
> ii) ~g(a) e color
>
> Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .
>

Please post your proof using DC Proof, and explain why it is relevant here.
Dan

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

Dan Christensen wrote:

> RECALL: A function is often represented as a set of ordered pairs.
> Example: Function f = {(0, 0), (1,2), (2, 4)}
> The domain of f in this case would be {0, 1, 2}.
> The range would be {0, 2, 4}.

SHOCK VIDEO: NHS Doctor Says “All The Vaccines Will Be Recalled Soon”
https://banned.video/watch?id=61e5c97eaf1fcf7b54e28a0a

REINER FUELLMICH- "THESE BA$TARDS ARE TRYING TO KILL US AND THATS THE
BOTTOM LINE.. WE MUST ACT NOW
https://153news.net/watch_video.php?v=Y9A461YX8HHO

Is This Evidence That All The Jabs In The UK Are Being Pulled?
https://www.bitchute.com/video/Mk8yEdDkk4ua/

On Monday, January 17, 2022 at 5:24:54 PM UTC-5, Dan Christensen wrote:
> RECALL:
>
> A function is often represented as a set of ordered pairs.
>
> Example: Function f = {(0, 0), (1,2), (2, 4)}
>
> The domain of f in this case would be {0, 1, 2}.
>
> The range would be {0, 2, 4}.
>
> The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
>
> Using the standard function notation, we can write:
>
> f(0) = 0, f(1) = 2 and f(2) = 4
>
> Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
>
> f = {(a, b) : a in X & b in Y & F(a,b)}
>
> where F is a suitable binary predicate.
>
> Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
>
> Alternatively, we could write as follows use predicate logic:
>
> (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
>
> BURSE'S PARADOX
>
> If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
>
> We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
>
> (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
>
> Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
>
> (To be continued)
>
> Comments 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

Yeah, the constrained discrete set definitely poses problems.
Still, it is true that calculus can be performed albeit errantly at discrete intervals.
Still, what makes it calculus is its ability to refine arbitrarily.
I just bumped into this in the Boolean sense, thinking maybe I had created a Boolean differential.
I think possibly this discrete form could be taken as an open problem with a bifurcated interpretation:
1. Differential discrete form allowed.
2. No such thing as a differential in discrete form exists.

I suppose then we have to ask whether 1+1=2 in your system?

By claiming such a limited space to work in are you caught further defining that space's qualities?
Or are they inherited from some old assumptions that are going unstated?
The invalid assumption is generally the one of interest.
The bug lays there.

On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:

>
> I suppose then we have to ask whether 1+1=2 in your system?
>

Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.

Dan

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

With Peano unit its much more easier.
Define Zermelo natural numbers as:

b = a <=> b e {a}

Now 0={}, 1={{}}, 2={{{}}}.
Then it is trivial to derive 1+1=2.

Dan Christensen schrieb:
> On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:
>
>>
>> I suppose then we have to ask whether 1+1=2 in your system?
>>
>
> Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

Here is a proof, write i(a) for {a}:

(∀xAxnx ∧ ∀x∀y∀z(Axyz → Axi(y)i(z))) → Ai(n)i(n)i(i(n)) is valid.
https://www.umsu.de/trees/#~6x%28Axnx%29~1~6x~6y~6z%28Axyz~5Axi%28y%29i%28z%29%29~5Ai%28n%29i%28n%29i%28i%28n%29%29

Only 11 proof lines.

Mostowski Collapse schrieb:
> With Peano unit its much more easier.
> Define Zermelo natural numbers as:
>
> b = a    <=>   b e {a}
>
> Now 0={}, 1={{}}, 2={{{}}}.
> Then it is trivial to derive 1+1=2.
>
> Dan Christensen schrieb:
>> On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com
>> wrote:
>>
>>>
>>> I suppose then we have to ask whether 1+1=2 in your system?
>>>
>>
>> Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove
>> the existence of an addition function in my system using basic set
>> theory. (700+ lines of proof) Then define 1 and 2 in N such that
>> 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
>>
>> Dan
>>
>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>> Visit my Math Blog at http://www.dcproof.wordpress.com
>>
>

On Tuesday, January 18, 2022 at 12:33:53 PM UTC-5, Dan Christensen wrote:
> On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:
>
> >
> > I suppose then we have to ask whether 1+1=2 in your system?
> >
> Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
Well, then is 2+1=3?
where is f(3)?
I understand I can't break you here, but it does seem troubling doesn't it?
You want to claim some pure function that works on one and works on two, but refuses to work on 3?
What sort of f'ing f() is this?

Here is a proof, 2+1=3, this time p(_,_) function and not A(_,_,_) relation:

?- prove0('(∀x p(x,n)=x ∧ ∀x∀y∀z(p(x,y)=z ⇒ p(x,i(y))=i(z))) ⇒ p(i(i(n)),i(n))=i(i(i(n)))', 4, unicode), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste22/package..html

1. ∀x p(x, n) = x ∧ ∀x ∀y ∀z (p(x, y) = z ⇒ p(x, i(y)) = i(z)) ⇒ p(i(i(n)), i(n)) = i(i(i(n)))
2. p(i(i(n)), i(n)) = i(i(i(n))) (T⇒2 1)
3. ¬(∀x p(x, n) = x ∧ ∀x ∀y ∀z (p(x, y) = z ⇒ p(x, i(y)) = i(z))) (T⇒1 1)
4. ¬∀x ∀y ∀z (p(x, y) = z ⇒ p(x, i(y)) = i(z)) (F∧2 3)
5. ¬∀x p(x, n) = x (F∧1 3)
6. ¬p(i(i(n)), n) = i(i(n)) (F∀ 5)
7. ¬∀y ∀z (p(i(i(n)), y) = z ⇒ p(i(i(n)), i(y)) = i(z)) (F∀ 4)
8. ¬∀z (p(i(i(n)), n) = z ⇒ p(i(i(n)), i(n)) = i(z)) (F∀ 7)
9. ¬(p(i(i(n)), n) = i(i(n)) ⇒ p(i(i(n)), i(n)) = i(i(i(n)))) (F∀ 8)
10. p(i(i(n)), n) = i(i(n)) (F⇒1 9)
✓ (ax 6, 10)
10. ¬p(i(i(n)), i(n)) = i(i(i(n))) (F⇒2 9)
✓ (ax 10, 2)

timba...@gmail.com schrieb am Dienstag, 18. Januar 2022 um 18:57:37 UTC+1:
> On Tuesday, January 18, 2022 at 12:33:53 PM UTC-5, Dan Christensen wrote:
> > On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:
> >
> > >
> > > I suppose then we have to ask whether 1+1=2 in your system?
> > >
> > Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> Well, then is 2+1=3?
> where is f(3)?
> I understand I can't break you here, but it does seem troubling doesn't it?
> You want to claim some pure function that works on one and works on two, but refuses to work on 3?
> What sort of f'ing f() is this?

On Tuesday, January 18, 2022 at 12:44:00 PM UTC-5, Mostowski Collapse wrote:
> With Peano unit its much more easier.
> Define Zermelo natural numbers as:
>
> b = a <=> b e {a}
>
> Now 0={}, 1={{}}, 2={{{}}}.
> Then it is trivial to derive 1+1=2.

Since the addition function is not defined in the ZFC axioms, you would first have to prove its existence using only the ZFC axioms.

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, January 18, 2022 at 12:57:37 PM UTC-5, timba...@gmail.com wrote:
> On Tuesday, January 18, 2022 at 12:33:53 PM UTC-5, Dan Christensen wrote:
> > On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:
> >
> > >
> > > I suppose then we have to ask whether 1+1=2 in your system?
> > >
> > Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> Well, then is 2+1=3?

Yes. You would first have to define 3 = S(2).

> where is f(3)?
> I understand I can't break you here, but it does seem troubling doesn't it?

Not at all.

> You want to claim some pure function that works on one and works on two, but refuses to work on 3?

"Refuses to work on 3???" Where do you get that idea?

Dan

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

On 1/17/2022 4:24 PM, Dan Christensen wrote:
> RECALL:
>
> A function is often represented as a set of ordered pairs.
>
> Example: Function f = {(0, 0), (1,2), (2, 4)}
>
> The domain of f in this case would be {0, 1, 2}.
>
> The range would be {0, 2, 4}.
>
> The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
>
> Using the standard function notation, we can write:
>
> f(0) = 0, f(1) = 2 and f(2) = 4
>
> Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
>
> f = {(a, b) : a in X & b in Y & F(a,b)}
>
> where F is a suitable binary predicate.
>
> Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
>
> Alternatively, we could write as follows use predicate logic:
>
> (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
>
> BURSE'S PARADOX
>
> If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
>
> We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
>
> (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
>
> Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
>
> (To be continued)
>
> Comments 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

Hi, I guess I always used the "working definition" of a function, BUT;

https://tutorial.math.lamar.edu/Classes/Alg/FunctionDefn.aspx

Definition of Relation: A relation is a set of ordered pairs.

Definition of a Function: A function is a relation for which each value from the set the first components of the ordered pairs is associated with
exactly one value from the set of second components of the ordered pair.

“Working Definition” of Function: A function is an equation for which any x that can be plugged into the equation will yield exactly one y out of the
equation.

SO you are rightamundo!

Ha Ha, the Thread Says "Not just sets of ordered pairs",

But Dan-O-Matic nevertheless rants:
> Since the addition function is not defined in the ZFC
axioms, you would first have to prove its existence
using only the ZFC axioms

If I remember well you use pairs resp. triples for your proof
of existence of addition? But why is then your addition
not just set, since you proved it like that?

The answer is the "Working Practice" uses different cosmetics.

This is what causes Dan-O-Matik a sisyphus. He invented the
Function Axiom, because he does not want to write (x,y) e f,
he prefers that from the outside one sees f(x,y).

The problem is that his Function Axiom transfers a set-like
function into a FOL function symbol. But FOL function symbols
are classes and not sets. But the Function Axiom is

totally unnecessary, I can directly prove:

1. ∀x (x, n, x) ∈ a ∧ ∀x ∀y ∀z ((x, y, z) ∈ a ⇒ (x, i(y), i(z)) ∈ a) ⇒ (i(i(n)), i(n), i(i(i(n)))) ∈ a
2. (i(i(n)), i(n), i(i(i(n)))) ∈ a (T⇒2 1)
3. ¬(∀x (x, n, x) ∈ a ∧ ∀x ∀y ∀z ((x, y, z) ∈ a ⇒ (x, i(y), i(z)) ∈ a)) (T⇒1 1)
4. ¬∀x ∀y ∀z ((x, y, z) ∈ a ⇒ (x, i(y), i(z)) ∈ a) (F∧2 3)
5. ¬∀x (x, n, x) ∈ a (F∧1 3)
6. ¬(i(i(n)), n, i(i(n))) ∈ a (F∀ 5)
7. ¬∀y ∀z ((i(i(n)), y, z) ∈ a ⇒ (i(i(n)), i(y), i(z)) ∈ a) (F∀ 4)
8. ¬∀z ((i(i(n)), n, z) ∈ a ⇒ (i(i(n)), i(n), i(z)) ∈ a) (F∀ 7)
9. ¬((i(i(n)), n, i(i(n))) ∈ a ⇒ (i(i(n)), i(n), i(i(i(n)))) ∈ a) (F∀ 8)
10. (i(i(n)), n, i(i(n))) ∈ a (F⇒1 9)
✓ (ax 6, 10)
10. ¬(i(i(n)), i(n), i(i(i(n)))) ∈ a (F⇒2 9)
✓ (ax 10, 2)

You can further restrict a and show that it exists. But
its NOWHERE NEEDED TO PROVE 2+1=3. You only
more about a when you for example want to prove:

2+1 =\= 4

But it would be more easier to abandon the Function Axiom
and provide some notation based on Peano Apostroph, or
some such. And not run into class problems and

function spaces that are as big as the universal class.

sergio schrieb am Dienstag, 18. Januar 2022 um 19:24:15 UTC+1:
> Hi, I guess I always used the "working definition" of a function, BUT;
>
> https://tutorial.math.lamar.edu/Classes/Alg/FunctionDefn.aspx
>
> Definition of Relation: A relation is a set of ordered pairs.
>
> Definition of a Function: A function is a relation for which each value from the set the first components of the ordered pairs is associated with
> exactly one value from the set of second components of the ordered pair.
>
>
> “Working Definition” of Function: A function is an equation for which any x that can be plugged into the equation will yield exactly one y out of the
> equation.
>
> SO you are rightamundo!

On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> Ha Ha, the Thread Says "Not just sets of ordered pairs",
>
> But Dan-O-Matic nevertheless rants:

> > Since the addition function is not defined in the ZFC
> > axioms, you would first have to prove its existence
> > using only the ZFC axioms

> If I remember well you use pairs resp. triples for your proof
> of existence of addition? But why is then your addition
> not just set, since you proved it like that?
>

I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].

Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.

> The answer is the "Working Practice" uses different cosmetics.
>
> This is what causes Dan-O-Matik a sisyphus. He invented the
> Function Axiom, because he does not want to write (x,y) e f,
> he prefers that from the outside one sees f(x,y).
>

This neatly avoids Burse's Paradox.

> The problem is that his Function Axiom transfers a set-like
> function into a FOL function symbol. But FOL function symbols
> are classes and not sets.

See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach

There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."

G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).

> But the Function Axiom is totally unnecessary...

On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).

Dan

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

WHATS WRONG WITH YOU????
DONT YOU REMEMBER WHAT YOU PROVED YOURSELF???

"common usage" is something informal. If you want to dig deeper
things become much more complicated. And your function axiom
does not guarantee existence of add(_,_,_). It depends on existence

of (_,_,_) e add. Namely the subset axiom or however you created
add. Your function axiom only transfers one existence into another
existence. Its not the primary cause of existence of add in your proof.

You can check your own proof by yourself. Or did you forget what you proved?

You don't have a function axiom that shows existence directly
inside some "common usage" only. You nevertheless fall back to set
theory. You wouldn't be able to show existence of add without set theory.

Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> >
> > But Dan-O-Matic nevertheless rants:
>
> > > Since the addition function is not defined in the ZFC
> > > axioms, you would first have to prove its existence
> > > using only the ZFC axioms
>
> > If I remember well you use pairs resp. triples for your proof
> > of existence of addition? But why is then your addition
> > not just set, since you proved it like that?
> >
> I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
>
> Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > The answer is the "Working Practice" uses different cosmetics.
> >
> > This is what causes Dan-O-Matik a sisyphus. He invented the
> > Function Axiom, because he does not want to write (x,y) e f,
> > he prefers that from the outside one sees f(x,y).
> >
> This neatly avoids Burse's Paradox.
> > The problem is that his Function Axiom transfers a set-like
> > function into a FOL function symbol. But FOL function symbols
> > are classes and not sets.
> See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
>
> There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
>
> G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
>
> > But the Function Axiom is totally unnecessary...
>
> On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

>> If I remember well you use pairs resp. triples for your proof of
>> existence of addition? But why is then your addition not just set,
>> since you proved it like that?
>>
> I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in
> n]. Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in
> n (see Burse's Paradox). Deal with, Jan Burse.

this theory sucks big time. Rand Paul Wonders If YouTube Will "Kiss My
Ass And Apologize" After CDC Admits Cloth Masks Aren't Effective

Here is what you do, instead of only using this here:

∀x (x, n, x) ∈ a ∧ ∀x ∀y ∀z ((x, y, z) ∈ a ⇒ (x, i(y), i(z)) ∈ a) ⇒ (i(i(n)), i(n), i(i(i(n)))) ∈ a

Call a set a, that satisfies the above, an adder-inductive-set,
abbrevatied ais. You make a minimal, in that you define it:

(x,y,z) e a <=> (x,y,z) e N x N x N & (∀a' ais(a) => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973

The above construction primarily uses the Subset Axiom.
The Function Axiom only transfers into your cosmetic,
that you wrongly think is "common usage". The fallacy

is not how you construct add or some such, how you use
set theory. The fallacy in your doing is the function axiom,
since it transfers into FOL function symbols.

You cannot prove:

EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]

You even dont have equality f=g for function symbols f,g.
On the otherhand, what is constructed with the Subset Axiom
is unique. It is easy to prove EXISTUNIQUE(a). Everything that

is constructed with the Subset Axiom is unique.

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 20:42:58 UTC+1:
> WHATS WRONG WITH YOU????
> DONT YOU REMEMBER WHAT YOU PROVED YOURSELF???
>
> "common usage" is something informal. If you want to dig deeper
> things become much more complicated. And your function axiom
> does not guarantee existence of add(_,_,_). It depends on existence
>
> of (_,_,_) e add. Namely the subset axiom or however you created
> add. Your function axiom only transfers one existence into another
> existence. Its not the primary cause of existence of add in your proof.
>
> You can check your own proof by yourself. Or did you forget what you proved?
>
> You don't have a function axiom that shows existence directly
> inside some "common usage" only. You nevertheless fall back to set
> theory. You wouldn't be able to show existence of add without set theory.
> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> > On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> > >
> > > But Dan-O-Matic nevertheless rants:
> >
> > > > Since the addition function is not defined in the ZFC
> > > > axioms, you would first have to prove its existence
> > > > using only the ZFC axioms
> >
> > > If I remember well you use pairs resp. triples for your proof
> > > of existence of addition? But why is then your addition
> > > not just set, since you proved it like that?
> > >
> > I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> >
> > Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > > The answer is the "Working Practice" uses different cosmetics.
> > >
> > > This is what causes Dan-O-Matik a sisyphus. He invented the
> > > Function Axiom, because he does not want to write (x,y) e f,
> > > he prefers that from the outside one sees f(x,y).
> > >
> > This neatly avoids Burse's Paradox.
> > > The problem is that his Function Axiom transfers a set-like
> > > function into a FOL function symbol. But FOL function symbols
> > > are classes and not sets.
> > See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
> >
> > There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
> >
> > G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> >
> > > But the Function Axiom is totally unnecessary...
> >
> > On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Corr.: Typo

(x,y,z) e a <=> (x,y,z) e N x N x N & (∀a' ais(a') => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 21:01:07 UTC+1:
> Here is what you do, instead of only using this here:
> ∀x (x, n, x) ∈ a ∧ ∀x ∀y ∀z ((x, y, z) ∈ a ⇒ (x, i(y), i(z)) ∈ a) ⇒ (i(i(n)), i(n), i(i(i(n)))) ∈ a
> Call a set a, that satisfies the above, an adder-inductive-set,
> abbrevatied ais. You make a minimal, in that you define it:
>
> (x,y,z) e a <=> (x,y,z) e N x N x N & (∀a' ais(a) => (x,y,z) e a')
> https://math.stackexchange.com/a/784504/1002973
>
> The above construction primarily uses the Subset Axiom.
> The Function Axiom only transfers into your cosmetic,
> that you wrongly think is "common usage". The fallacy
>
> is not how you construct add or some such, how you use
> set theory. The fallacy in your doing is the function axiom,
> since it transfers into FOL function symbols.
>
> You cannot prove:
>
> EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
>
> You even dont have equality f=g for function symbols f,g.
> On the otherhand, what is constructed with the Subset Axiom
> is unique. It is easy to prove EXISTUNIQUE(a). Everything that
>
> is constructed with the Subset Axiom is unique.
> Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 20:42:58 UTC+1:
> > WHATS WRONG WITH YOU????
> > DONT YOU REMEMBER WHAT YOU PROVED YOURSELF???
> >
> > "common usage" is something informal. If you want to dig deeper
> > things become much more complicated. And your function axiom
> > does not guarantee existence of add(_,_,_). It depends on existence
> >
> > of (_,_,_) e add. Namely the subset axiom or however you created
> > add. Your function axiom only transfers one existence into another
> > existence. Its not the primary cause of existence of add in your proof.
> >
> > You can check your own proof by yourself. Or did you forget what you proved?
> >
> > You don't have a function axiom that shows existence directly
> > inside some "common usage" only. You nevertheless fall back to set
> > theory. You wouldn't be able to show existence of add without set theory.
> > Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> > > On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > > > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> > > >
> > > > But Dan-O-Matic nevertheless rants:
> > >
> > > > > Since the addition function is not defined in the ZFC
> > > > > axioms, you would first have to prove its existence
> > > > > using only the ZFC axioms
> > >
> > > > If I remember well you use pairs resp. triples for your proof
> > > > of existence of addition? But why is then your addition
> > > > not just set, since you proved it like that?
> > > >
> > > I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> > >
> > > Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > > > The answer is the "Working Practice" uses different cosmetics.
> > > >
> > > > This is what causes Dan-O-Matik a sisyphus. He invented the
> > > > Function Axiom, because he does not want to write (x,y) e f,
> > > > he prefers that from the outside one sees f(x,y).
> > > >
> > > This neatly avoids Burse's Paradox.
> > > > The problem is that his Function Axiom transfers a set-like
> > > > function into a FOL function symbol. But FOL function symbols
> > > > are classes and not sets.
> > > See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
> > >
> > > There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
> > >
> > > G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> > >
> > > > But the Function Axiom is totally unnecessary...
> > >
> > > On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(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 Tuesday, January 18, 2022 at 2:42:58 PM UTC-5, Mostowski Collapse wrote:

>

> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> > On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> > >
> > > But Dan-O-Matic nevertheless rants:
> >
> > > > Since the addition function is not defined in the ZFC
> > > > axioms, you would first have to prove its existence
> > > > using only the ZFC axioms
> >
> > > If I remember well you use pairs resp. triples for your proof
> > > of existence of addition? But why is then your addition
> > > not just set, since you proved it like that?
> > >
> > I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> >
> > Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > > The answer is the "Working Practice" uses different cosmetics.
> > >
> > > This is what causes Dan-O-Matik a sisyphus. He invented the
> > > Function Axiom, because he does not want to write (x,y) e f,
> > > he prefers that from the outside one sees f(x,y).
> > >
> > This neatly avoids Burse's Paradox.
> > > The problem is that his Function Axiom transfers a set-like
> > > function into a FOL function symbol. But FOL function symbols
> > > are classes and not sets.
> > See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
> >
> > There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
> >
> > G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> >
> > > But the Function Axiom is totally unnecessary...
> >
> > On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).

> "common usage" is something informal. If you want to dig deeper
> things become much more complicated. And your function axiom
> does not guarantee existence of add(_,_,_). It depends on existence
>
> of (_,_,_) e add.

This overloading is an issue I addressed in my latest update to DC Proof. The name assigned to a function must now differ from the name of graph set. I can see that it has caused you some confusion. I hope the change will clear things up for you. No, I won't hold my breath!

Dan

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

Its useless nonsense what you are doing. Its not anymore
"common usage". You cannot prove:

EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]

You only read Landau. You didn't read Dedekind:

"Richard Dedekind's theorem 126 of his "Was sind und was sollen
die Zahlen? (1888)". This work was the first to give a proof that
a certain recursive construction defines a unique function.
https://en.wikipedia.org/wiki/Primitive_recursive_function#History

You cannot replicate the above in your "common usage".
There is much missing.

Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 21:07:59 UTC+1:
> On Tuesday, January 18, 2022 at 2:42:58 PM UTC-5, Mostowski Collapse wrote:
>
> >
>
> > Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> > > On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > > > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> > > >
> > > > But Dan-O-Matic nevertheless rants:
> > >
> > > > > Since the addition function is not defined in the ZFC
> > > > > axioms, you would first have to prove its existence
> > > > > using only the ZFC axioms
> > >
> > > > If I remember well you use pairs resp. triples for your proof
> > > > of existence of addition? But why is then your addition
> > > > not just set, since you proved it like that?
> > > >
> > > I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> > >
> > > Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > > > The answer is the "Working Practice" uses different cosmetics.
> > > >
> > > > This is what causes Dan-O-Matik a sisyphus. He invented the
> > > > Function Axiom, because he does not want to write (x,y) e f,
> > > > he prefers that from the outside one sees f(x,y).
> > > >
> > > This neatly avoids Burse's Paradox.
> > > > The problem is that his Function Axiom transfers a set-like
> > > > function into a FOL function symbol. But FOL function symbols
> > > > are classes and not sets.
> > > See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
> > >
> > > There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
> > >
> > > G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> > >
> > > > But the Function Axiom is totally unnecessary...
> > >
> > > On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).
> > "common usage" is something informal. If you want to dig deeper
> > things become much more complicated. And your function axiom
> > does not guarantee existence of add(_,_,_). It depends on existence
> >
> > of (_,_,_) e add.
> This overloading is an issue I addressed in my latest update to DC Proof. The name assigned to a function must now differ from the name of graph set.. I can see that it has caused you some confusion. I hope the change will clear things up for you. No, I won't hold my breath!
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Also there is very poor motivation for these exercises,
since Landau doesn't show anything with an implication
in it, when he talks about some equations.

Just use the equations directly. Here is a proof 1+1 =/= 1:

∀x∀y(s(x)=s(y) → x=y),
∀x¬n=s(x),
∀xp(x,n)=x, /* Landau x+1=x', but with zero */
∀x∀y∀zp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
entails ¬p(s(n),s(n))=s(n).

So why bother and answer on MSE, when the OP showed
equations without an implication. Where does this
implication come from?

[(e,f,g)∈d⟹(e,S(f),S(g))∈d]
https://math.stackexchange.com/a/784504/1002973

Its not a translation of /* Landau x+y' = (x+y)' */.
How do you correctly translate Landau?

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 21:15:33 UTC+1:
> Its useless nonsense what you are doing. Its not anymore
> "common usage". You cannot prove:
>
> EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
>
> You only read Landau. You didn't read Dedekind:
>
> "Richard Dedekind's theorem 126 of his "Was sind und was sollen
> die Zahlen? (1888)". This work was the first to give a proof that
> a certain recursive construction defines a unique function.
> https://en.wikipedia.org/wiki/Primitive_recursive_function#History
>
> You cannot replicate the above in your "common usage".
> There is much missing.
> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 21:07:59 UTC+1:
> > On Tuesday, January 18, 2022 at 2:42:58 PM UTC-5, Mostowski Collapse wrote:
> >
> > >
> >
> > > Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 20:38:11 UTC+1:
> > > > On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> > > > > Ha Ha, the Thread Says "Not just sets of ordered pairs",
> > > > >
> > > > > But Dan-O-Matic nevertheless rants:
> > > >
> > > > > > Since the addition function is not defined in the ZFC
> > > > > > axioms, you would first have to prove its existence
> > > > > > using only the ZFC axioms
> > > >
> > > > > If I remember well you use pairs resp. triples for your proof
> > > > > of existence of addition? But why is then your addition
> > > > > not just set, since you proved it like that?
> > > > >
> > > > I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> > > >
> > > > Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> > > > > The answer is the "Working Practice" uses different cosmetics.
> > > > >
> > > > > This is what causes Dan-O-Matik a sisyphus. He invented the
> > > > > Function Axiom, because he does not want to write (x,y) e f,
> > > > > he prefers that from the outside one sees f(x,y).
> > > > >
> > > > This neatly avoids Burse's Paradox.
> > > > > The problem is that his Function Axiom transfers a set-like
> > > > > function into a FOL function symbol. But FOL function symbols
> > > > > are classes and not sets.
> > > > See https://en.wikipedia.org/wiki/Function_(mathematics)#Relational_approach
> > > >
> > > > There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
> > > >
> > > > G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> > > >
> > > > > But the Function Axiom is totally unnecessary...
> > > >
> > > > On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).
> > > "common usage" is something informal. If you want to dig deeper
> > > things become much more complicated. And your function axiom
> > > does not guarantee existence of add(_,_,_). It depends on existence
> > >
> > > of (_,_,_) e add.
> > This overloading is an issue I addressed in my latest update to DC Proof. The name assigned to a function must now differ from the name of graph set. I can see that it has caused you some confusion. I hope the change will clear things up for you. No, I won't hold my breath!
> > 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, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> Its useless nonsense what you are doing. Its not anymore
> "common usage". You cannot prove:
>
> EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
>

Recently posted here...

Existence of Add Function on N:

EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
& ALL(a):[a in n => add(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]

https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)

Uniqueness of Add Function on N:

ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
& ALL(a):[a in n => add(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]

& ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
& ALL(a):[a in n => add'(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
=> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]

https://dcproof.com/AdditionOnNUnique.htm (84 lines)

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 the same as what you can prove for sets.
You only prove relative equality:

ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]

For the set itself, you can prove absolute equality.
If you have two sets:

ALL(x):[x e s1 <=> x e d & A(x)]

ALL(x):[x e s2 <=> x e d & A(x)]

Then you can prove s1 = s2 absolutely. Try
it, you don't need the a in n & b in n for sets.

Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 22:11:29 UTC+1:
> On Tuesday, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> > Its useless nonsense what you are doing. Its not anymore
> > "common usage". You cannot prove:
> >
> > EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
> >
> Recently posted here...
>
> Existence of Add Function on N:
>
> EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> & ALL(a):[a in n => add(a,0)=a]
> & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
>
> https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
>
> Uniqueness of Add Function on N:
>
> ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> & ALL(a):[a in n => add(a,0)=a]
> & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]
>
> & ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
> & ALL(a):[a in n => add'(a,0)=a]
> & ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
>
> => ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
>
> https://dcproof.com/AdditionOnNUnique.htm (84 lines)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

This absolute uniqueness of the addition function,
how you create it as a set and not as a Dan-O-Matik
function, is a consequence of:
- Extensionality Axiom for Sets
(- And the Subset Axiom itself of course)

You can try yourself:

∀s∀t(∀x(Exs ↔ Ext) → s=t), /* Extensionality */
∀x(Exa ↔ (Exd ∧ px)), /* a is from Subset */
∀x(Exb ↔ (Exd ∧ px)) /* b is from Subset */
entails a=b. /* They are absolutely the same */
https://www.umsu.de/trees/#~6s~6t%28~6x%28Exs~4Ext%29~5s=t%29,~6x%28Exa~4Exd~1p%28x%29%29,~6x%28Exb~4Exd~1p%28x%29%29|=a=b

Unfortunately you cannot prove it, when you would add:
- Extenionality Axiom for Dan-O-Matik function

Because your Function Axiom is nonsense.

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 22:22:42 UTC+1:
> Its not the same as what you can prove for sets.
> You only prove relative equality:
> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> For the set itself, you can prove absolute equality.
> If you have two sets:
>
> ALL(x):[x e s1 <=> x e d & A(x)]
>
> ALL(x):[x e s2 <=> x e d & A(x)]
>
> Then you can prove s1 = s2 absolutely. Try
> it, you don't need the a in n & b in n for sets.
> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 22:11:29 UTC+1:
> > On Tuesday, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> > > Its useless nonsense what you are doing. Its not anymore
> > > "common usage". You cannot prove:
> > >
> > > EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
> > >
> > Recently posted here...
> >
> > Existence of Add Function on N:
> >
> > EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
> >
> > https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
> >
> > Uniqueness of Add Function on N:
> >
> > ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]
> >
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
> > & ALL(a):[a in n => add'(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
> >
> > => ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> >
> > https://dcproof.com/AdditionOnNUnique.htm (84 lines)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com