You are aware that we have 2022, don't you?
I nowhere advocated ZFC/Schonfield.

I wrote explicitly:

Mostowski Collapse schrieb:
> Especially for constructive mathematics there are
> now frameworks, of course different from ZFC/Shoenfield,
> that do not allow to add any axiom.
>
> Just check out what Coq, Isabelle/HOL, etc.. provide.

Whats wrong with you?

Dan Christensen schrieb:
> On Saturday, April 30, 2022 at 4:44:16 PM UTC-4, Mostowski Collapse wrote:
>> For exampe the foundational approach of ZFC is totally
>> different.
>
> DC Proof would be quite useless as an educational aid otherwise. IIUC you can get degree in pure math without ever looking at the ZFC axioms (possible exception: AC). Why do you think that is, Jan Burse?
>
> 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:

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

I bet it's "programmed" in visual basic and crap like that. You uneducated
fool.

Ukraine is being used as a FOOL - South African politician truth bomb
https://www.bitchute.com/video/BiPh52uQC0pj/

Training The Next Generations Of Ukrainian NAZIs
https://www.bitchute.com/video/ge6z7aatj3Pn/

On Saturday, April 30, 2022 at 5:24:17 PM UTC-4, Colin Ohba wrote:
> Dan Christensen wrote:
>
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com Visit my
> > Math
> I bet it's "programmed" in visual basic and crap like that. You uneducated
> fool.
>
> Ukraine is being used as a FOOL - South African politician truth bomb

>
>
> Training The Next Generations Of Ukrainian NAZIs

You keep forgetting, Nazi Boy....

WAR OF AGRESSION = NAZI

No doubt you and your boss will soon be up in front of the Nuremberg War Crimes Tribunal II. You might want to keep a sturdy length of rope hidden away, just in case.

Dan Christensen wrote:

>> > Download my DC Proof 2.0 freeware at http://www.dcproof.com Visit my
>> > Math
>> I bet it's "programmed" in visual basic and crap like that. You
>> uneducated fool.
>>
>> Ukraine is being used as a FOOL - South African politician truth bomb
>> https://www.bitchute.com/video/BiPh52uQC0pj/
>> Training The Next Generations Of Ukrainian NAZIs
>> https://www.bitchute.com/video/ge6z7aatj3Pn/
>
> You keep forgetting, Nazi Boy.... WAR OF AGRESSION = NAZI

this stinking nazi imbecile still doesn't know what war is and what nazi
is. Let's try again, maybe this helps

Atombombe in 106 Sekunden in Berlin
https://www.bitchute.com/video/idkenkbuUmIi/

since supersonic, a few seconds more to cacanada si cacamerica, it's just
the same thing. But you escape the forced "vaccination" mandated by the
young world leader, trudeau. Which works for your benefit, reducing the
poverty, through "healthcare" and "vaccination" depopulation ranging from
10 to 15%.

Why do you assume its useful for education? Could you
for example provide a proof sketch here, the comment
section at the beginning of the proof is a little poor:

> This is how it is done: https://dcproof.com/ConstructAddFunction.htm

Do you suggest for mul, we would need to do the
same, again produce cryptic 700 proof lines. Come
on we have 2022. Is this what Coq, Isabelle/HOL, ... do?

I doubt. To the best of my knowledge there is more
around in logic books, and there are also other
approaches around. Can we dig them out?

Now it seems to me again something from WW2
is presented, some ancient contraption that works,
but that is as useful as radonized water.

You sure this is the state of the art?

Dan Christensen schrieb am Samstag, 30. April 2022 um 23:06:47 UTC+2:
> On Saturday, April 30, 2022 at 4:44:16 PM UTC-4, Mostowski Collapse wrote:
> > For exampe the foundational approach of ZFC is totally
> > different.
> DC Proof would be quite useless as an educational aid otherwise. IIUC you can get degree in pure math without ever looking at the ZFC axioms (possible exception: AC). Why do you think that is, Jan Burse?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, May 1, 2022 at 3:28:43 AM UTC-4, Mostowski Collapse wrote:

> > This is how it is done: https://dcproof.com/ConstructAddFunction.htm
>
> Why do you assume its useful for education?

Just to show it can be done, that you don't have to simply define the addition function; you can actually prove its existence from Peano's Axioms. It is important for math majors to understand this.

> Could you
> for example provide a proof sketch here, the comment
> section at the beginning of the proof is a little poor:
>

Good point. Looks like this was a test run for the new function axiom, not for publication. Will add some additional commentary at the above link.

In a nutshell:

1. Starting from Peano's Axioms, construct the graph set add (a set of ordered triples).

2. Establish certain essential properties of the set add.

3. Prove that add meets the requirements of functionality as given by the Function Axiom.

4. Introduce the function operator faddd.

5. Prove that the function operator fadd satisfies the usual requirements of addition on N.

Dan

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

I am more concerned that your add/3 is only a Half-Function,
and not a Function. It has dark elements. For example we cannot prove:

ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0]

On the other hand if "add" were really add : N x N -> N, we
could prove the above. But with your nonsense

we cannot prove the above.

Dan Christensen schrieb am Sonntag, 1. Mai 2022 um 15:51:20 UTC+2:
> On Sunday, May 1, 2022 at 3:28:43 AM UTC-4, Mostowski Collapse wrote:
>
> > > This is how it is done: https://dcproof.com/ConstructAddFunction.htm
> >
> > Why do you assume its useful for education?

Why can we not prove ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0] ?
Well there is an easy counter example, the addition for positive
and negative integers, call it simply "plus":

plus : Z x Z -> Z

Now we can verify everthing that Dan O Matik stated, namely
we can verify all of this here, which thinks Dan O Matik is
defining property of add : N x N -> N:

EXIST(add):[
1) ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
2) & ALL(a):[a e n => add(a,0)=a]
3) & ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]
https://dcproof.com/ConstructAddFunction.htm

Lets first veryify 1), does plus : Z x Z -> Z satify 1).
Well hell yes, if we only look at the subset of positive
integer numbers we have of course for the addition of

positive and negative integer the following verifiable,
since positive integer plus positive integer gives positive
integers, the negative integers disappear:

1) Check! Ok
ALL(a):ALL(b):[a e N & b e N => plus(a,b) e N]

Lets now verify 2) and 3), based on similar arguments,
we get again all of this verified:

2) Check! Ok
ALL(a):[a e N => plus(a,0)=a]
3) Check! Ok
ALL(a):[a e N & b e N => plus(a,s(b))=s(plus(a,b))]

Now lets look at this formula:

4) Check! Nok
ALL(x):ALL(y):[plus(x,y,0) => x=0 & y=0]

It doesn't hold, we have for example plus(-1,1,0).
So Dan O Matik only defines a Half Function, he nowhere
defined add : N x N -> N. In such an add we have

only one pair of arguments that gives zero, add(0,0,0).

Mostowski Collapse schrieb am Sonntag, 1. Mai 2022 um 21:47:14 UTC+2:
> I am more concerned that your add/3 is only a Half-Function,
> and not a Function. It has dark elements. For example we cannot prove:
>
> ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0]
>
> On the other hand if "add" were really add : N x N -> N, we
> could prove the above. But with your nonsense
>
> we cannot prove the above.
> Dan Christensen schrieb am Sonntag, 1. Mai 2022 um 15:51:20 UTC+2:
> > On Sunday, May 1, 2022 at 3:28:43 AM UTC-4, Mostowski Collapse wrote:
> >
> > > > This is how it is done: https://dcproof.com/ConstructAddFunction.htm
> > >
> > > Why do you assume its useful for education?

Dan Christensen wrote:

> On Sunday, May 1, 2022 at 3:28:43 AM UTC-4, Mostowski Collapse wrote:
>> Why do you assume its useful for education?
>
> Just to show it can be done, that you don't have to simply define the
> addition function; you can actually prove its existence from Peano's
> Axioms. It is important for math majors to understand this.

It appears that the war is already over (former cia). It
was over two days after the russian federation inset. The military
hardware from america is apparently resold in Africa. Big money for the
bidans and the nazi zelenske. The nazis are going to disappear from the
regional territory of russian federation, known as "ukraine".

Scott Ritter Judge - Ukraine is going to lose. Zelensky is choosing to
kill Ukrainians https://www.bitchute.com/video/1vx7TYoT10n1/

next stop might be *_The_Capitalist_Republic_of_Poland_* (CRP, nazi),
switzarland and so on.

I recently saw somebody using FOMO on Twitter.
Now I have FOMO that I cannot use FOMO.
But I did it just now, archivement unlocked.

Nymshifter gibberish:
> Swaziland, hurra I am the first black Nazi

Mostowski Collapse wrote:

> I recently saw somebody using FOMO on Twitter.
> Now I have FOMO that I cannot use FOMO.
> But I did it just now, archivement unlocked.
>
> Nymshifter gibberish:
>> Swaziland, hurra I am the first black Nazi

I almost knew the switzarland is something Africa related.

Its the capital of bitchute land.

Jonas Tanaka schrieb am Sonntag, 1. Mai 2022 um 23:17:21 UTC+2:
> Mostowski Collapse wrote:
>
> > I recently saw somebody using FOMO on Twitter.
> > Now I have FOMO that I cannot use FOMO.
> > But I did it just now, archivement unlocked.
> >
> > Nymshifter gibberish:
> >> Swaziland, hurra I am the first black Nazi
> I almost knew the switzarland is something Africa related.

Mostowski Collapse wrote:

> Its the capital of bitchute land.

in gearmony they can put you in prison, just by denying the nazi
war_crimes of ww2. But guess what, the corrupt government are sending
military weaponry hardware to the nazi now, in "ukraine".

> Jonas Tanaka schrieb am Sonntag, 1. Mai 2022 um 23:17:21 UTC+2:
>> Mostowski Collapse wrote:
>>
>> > I recently saw somebody using FOMO on Twitter.
>> > Now I have FOMO that I cannot use FOMO.
>> > But I did it just now, archivement unlocked.
>> >
>> > Nymshifter gibberish:
>> >> Swaziland, hurra I am the first black Nazi
>> I almost knew the switzarland is something Africa related.

Guess what, you can buy pampers in bitchute land.
Because it seems you are shitting your pants.

Jonas Tanaka schrieb am Sonntag, 1. Mai 2022 um 23:28:52 UTC+2:
> Mostowski Collapse wrote:
>
> > Its the capital of bitchute land.
> in gearmony they can put you in prison, just by denying the nazi
> war_crimes of ww2. But guess what, the corrupt government are sending
> military weaponry hardware to the nazi now, in "ukraine".
> > Jonas Tanaka schrieb am Sonntag, 1. Mai 2022 um 23:17:21 UTC+2:
> >> Mostowski Collapse wrote:
> >>
> >> > I recently saw somebody using FOMO on Twitter.
> >> > Now I have FOMO that I cannot use FOMO.
> >> > But I did it just now, archivement unlocked.
> >> >
> >> > Nymshifter gibberish:
> >> >> Swaziland, hurra I am the first black Nazi
> >> I almost knew the switzarland is something Africa related.

On Sunday, May 1, 2022 at 3:47:14 PM UTC-4, Mostowski Collapse wrote:
> I am more concerned that your add/3 is only a Half-Function,

Nope, a full function:

691. ALL(a):ALL(b):[a in n & b in n => addf(a,b) in n]
Conclusion, 669
....

711. ALL(a):[a e n => addf(a,0)=a]
Conclusion, 692
....

759. ALL(a):ALL(b):[a e n & b e n => addf(a,s(b))=s(addf(a,b))]
Conclusion, 712

> and not a Function. It has dark elements. For example we cannot prove:
>

Maybe in your system where you can make logical inferences about functions outside their domains of inference--among the "dark elements." As you can see, this is impossible in DC Proof, as it is most math textbooks. Deal with it, Jan Burse

> ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0]
>
> On the other hand if "add" were really add : N x N -> N, we
> could prove the above. But with your nonsense we cannot prove the above.

Let's see your proof. It should translate easily in the DC Proof.

Dan

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

On Sunday, May 1, 2022 at 4:05:23 PM UTC-4, Mostowski Collapse wrote:
> Why can we not prove ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0] ?
> Well there is an easy counter example, the addition for positive
> and negative integers, call it simply "plus":
>
> plus : Z x Z -> Z
>

Pay attention, Jan Burse. Why are you nattering on about integers? We are constructing addition on the NATURAL NUMBERS. We need your proof for the NATURAL NUMBERS!

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, May 2, 2022 at 12:47:29 AM UTC+2, Dan Christensen wrote:
> On Sunday, May 1, 2022 at 4:05:23 PM UTC-4, Mostowski Collapse wrote:
> >
> > Why can we not prove ALL(x):ALL(y):[add(x,y)=0 => x=0 & y=0] ?
> >
> > Well there is an easy counter example, the addition for positive
> > and negative integers, call it simply "plus":
> >
> > plus : Z x Z --> Z

Indeed!

> Pay attention, Jan Burse. Why are you nattering on about integers?

Because we m a y do so. There is no law which forbids it, you know.

> We are constructing addition on the NATURAL NUMBERS.

That's just your delusion, idiot.

Actually, YOU DIDN'T DO THAT!

Hint: That's the theorem you proved:

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

Hint: One instance of "add" might just be the "function" plus, MC mentioned above (which is defined on Z x Z such that plus(-1, 1) = plus(0, 0) = 0). Your theorem does not exclude that possibillity. Actually, the following should be provable too:

ALL(a):ALL(b):[a e n & b e n => plus(a,b) e n]
& ALL(a):[a e n => plus(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => plus(a,s(b))=s(plus(a,b))]

where plus is the function MC mentioned above.

But in this case: EXIST(x):EXIST(y):[plus(x,y)=0 & ~(x=0 & y=0)]

Your present treatment of functions in the context of DC Proof is inferior, dumbo.

Hint: Defining functions "recursively" works because of the theorem (schema)

E!f(function(f) & f(0) = a & An(n e IN -> f(n+1) = ...f(n)...))

Where

f(0) = a
f(n+1) = ...f(n)...

are "the defining equations".

In a formal treatment we would have to "introduce" the new constant (which denotes the function we want to define) explicitely. This step is usually omitted in math, there we usually just/already use the new constant (denoting the function) when stating the "defining equations".

As you can see E!f plays an important role here. Now

E!f(Phi(f)) <-> Ef(Phi[f]) & AfAg(Phi[f] & Phi[g] -> f = g).

So ultimately we need an appropriate treatment (definition) of function equality (to ensure uniqueness).

On Sunday, May 1, 2022 at 11:42:29 PM UTC-4, Fritz Feldhase wrote:
> On Monday, May 2, 2022 at 12:47:29 AM UTC+2, Dan Christensen wrote:
> > On Sunday, May 1, 2022 at 4:05:23 PM UTC-4, Mostowski Collapse wrote:
> > >
> > > Why can we not prove ALL(x):ALL(y):[add(x,y)=0 => x=0 & y=0] ?
> > >
> > > Well there is an easy counter example, the addition for positive
> > > and negative integers, call it simply "plus":
> > >
> > > plus : Z x Z --> Z
>
> Indeed!
> > Pay attention, Jan Burse. Why are you nattering on about integers?
> Because we m a y do so. There is no law which forbids it, you know.

> > We are constructing addition on the NATURAL NUMBERS.
>
> Actually, YOU DIDN'T DO THAT!
>

Wrong.

> Hint: That's the theorem you proved:
>
> EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
> & ALL(a):[a e n => add(a,0)=a]
> & ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]

Thanks for confirming that I did indeed prove existence of the add function on N.

> Hint: One instance of "add" might just be the "function" plus, MC mentioned above (which is defined on Z x Z such that plus(-1, 1) = plus(0, 0) = 0). Your theorem does not exclude that possibillity. Actually, the following should be provable too:
>

You are talking nonsense! I defined n (the set of natural numbers) in lines 1-6 using the Peano Axioms. In the statement ALL(a):ALL(b):[a e n & b e n => add(a,b) e n], I have restricted both quantifiers to the set n (the natural numbers here).

The add function here is also unique:

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

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

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

Proof: https://dcproof.com/AdditionOnNUnique.htm

> ALL(a):ALL(b):[a e n & b e n => plus(a,b) e n]
> & ALL(a):[a e n => plus(a,0)=a]
> & ALL(a):ALL(b):[a e n & b e n => plus(a,s(b))=s(plus(a,b))]
>
> where plus is the function MC mentioned above.
>
> But in this case: EXIST(x):EXIST(y):[plus(x,y)=0 & ~(x=0 & y=0)]
>
> Your present treatment of functions in the context of DC Proof is inferior, dumbo.
>
> Hint: Defining functions "recursively" works because of the theorem (schema)
>
> E!f(function(f) & f(0) = a & An(n e IN -> f(n+1) = ...f(n)...))
>
> Where
>
> f(0) = a
> f(n+1) = ...f(n)...
>
> are "the defining equations".
>

I am not simply defining the add function on N, I am proving its existence. Do you understand the difference, Fritz?

> In a formal treatment we would have to "introduce" the new constant (which denotes the function we want to define) explicitely.

I do so on line 668 applying existential specification to previous line:

668. ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=> [addf(a1,a2)=b <=> (a1,a2,b) e add]]
E Spec, 667

> This step is usually omitted in math, there we usually just/already use the new constant (denoting the function) when stating the "defining equations".
>
> As you can see E!f plays an important role here. Now
>
> E!f(Phi(f)) <-> Ef(Phi[f]) & AfAg(Phi[f] & Phi[g] -> f = g).
>
> So ultimately we need an appropriate treatment (definition) of function equality (to ensure uniqueness).

Wrong. It is NOT necessary. See the above link where the uniqueness of the add function on N is proven.

Dan

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

Because you made two category mistakes again. Because you
told us you constructed the natural numbers addition
Function. But your symbol "add" does not capture

that. Its only a Half-Function. You only proved:

EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
Etc...

But you should have proved, note the two differences:

EXISTUNQUE(add):[add : n x n -> n]
Etc...

So you are living in the land of confusion.

Dan Christensen schrieb am Montag, 2. Mai 2022 um 00:47:29 UTC+2:
> On Sunday, May 1, 2022 at 4:05:23 PM UTC-4, Mostowski Collapse wrote:
> > Why can we not prove ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0] ?
> > Well there is an easy counter example, the addition for positive
> > and negative integers, call it simply "plus":
> >
> > plus : Z x Z -> Z
> >
> Pay attention, Jan Burse. Why are you nattering on about integers?

Arturo Magidin might not believe it, but living in the
land of confusion can have grave consequences.

Ronald Reagan confuses Nuke with Nurse
https://www.youtube.com/watch?v=TlBIa8z_Mts

Mostowski Collapse schrieb am Montag, 2. Mai 2022 um 10:21:36 UTC+2:
> Because you made two category mistakes again. Because you
> told us you constructed the natural numbers addition
> Function. But your symbol "add" does not capture
>
> that. Its only a Half-Function. You only proved:
>
> EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
> Etc...
>
> But you should have proved, note the two differences:
>
> EXISTUNQUE(add):[add : n x n -> n]
> Etc...
>
> So you are living in the land of confusion.
> Dan Christensen schrieb am Montag, 2. Mai 2022 um 00:47:29 UTC+2:
> > On Sunday, May 1, 2022 at 4:05:23 PM UTC-4, Mostowski Collapse wrote:
> > > Why can we not prove ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0] ?
> > > Well there is an easy counter example, the addition for positive
> > > and negative integers, call it simply "plus":
> > >
> > > plus : Z x Z -> Z
> > >
> > Pay attention, Jan Burse. Why are you nattering on about integers?

On Monday, May 2, 2022 at 6:42:53 AM UTC+2, Dan Christensen wrote:
> On Sunday, May 1, 2022 at 11:42:29 PM UTC-4, Fritz Feldhase wrote:
> >
> > Hint: One instance of "add" might just be the "function" plus, MC mentioned above (which is defined on Z x Z such that plus(-1, 1) = plus(0, 0) = 0). Your theorem does not exclude that possibillity. Actually, the following should be provable too:
> >
> [...] In the statement ALL(a):ALL(b):[a e n & b e n => add(a,b) e n], I have restricted both quantifiers to the set n (the natural numbers here).

Holy shit! You seem to think that

An e IN: Phi[x]

somehow "restricts" the "valitity" of Phi[x] to IN. What's the matter with you cranks?

Hint:

An e IN: n = n.

Does that mean, that ~(-1 = -1), or what?

> The add function here is also unique:
> ...
> => ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]]

No, you silly idiot!

This does not mean that "add" is unique.

This only means that add(x) = add'(x) for all x in a certain set X. WHAT'S THE MATTER WITH YOU, YOU SILLY IDIOT?!

Can't you read and/or comprehend my posts?

For example, ALL(a):ALL(b):[a e n & b e n => add(a,b)=plus(a,b)]] will hold too. BUT and =/= plus.

Hint:

> > the following should be provable too:
> >
> > ALL(a):ALL(b):[a e n & b e n => plus(a,b) e n]
> > & ALL(a):[a e n => plus(a,0)=a]
> > & ALL(a):ALL(b):[a e n & b e n => plus(a,s(b))=s(plus(a,b))]
> >
> > where plus is the function MC mentioned above.
> >
> > But in this case: EXIST(x):EXIST(y):[plus(x,y)=0 & ~(x=0 & y=0)]
> >
> > Your present treatment of functions in the context of DC Proof is inferior, dumbo.
> >
> > Hint: Defining functions "recursively" works because of the theorem (schema)
> >
> > E!f(function(f) & f(0) = a & An(n e IN -> f(n+1) = ...f(n)...))
> >
> > Where
> >
> > f(0) = a
> > f(n+1) = ...f(n)...
> >
> > are "the defining equations".
> >
> I am not simply defining the add function on N, I am proving its existence

If you say so. BUT

> > In a formal treatment we would have to "introduce" the new constant (which denotes the function we want to define) explicitely.
> >
> I do so on line 668 applying existential specification to previous line:
>
> 668. ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
> => [addf(a1,a2)=b <=> (a1,a2,b) e add]]
> E Spec, 667

"add" isn't a CONSTANT, you silly idiot;

after all your theorem reads:

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

Are you doing the John Gabriel now?

> > This step is usually omitted in math, there we usually just/already use the new constant (denoting the function) when stating the "defining equations".
> >
> > As you can see E!f plays an important role here. Now
> >
> > E!f(Phi(f)) <-> Ef(Phi[f]) & AfAg(Phi[f] & Phi[g] -> f = g).
> >
> > So ultimately we need an appropriate treatment (definition) of function equality (to ensure uniqueness).
> >
> Wrong.

No, not wrong.

> See the above link where the uniqueness of the add function on N is proven.

No, you didn't do so, you silly idiot!

What you need for this is a theorem of the form

E!f(function(f) & ...f...).

On Monday, May 2, 2022 at 10:21:36 AM UTC+2, Mostowski Collapse wrote:

> [...] But your symbol "add" does not capture
> that. Its only a Half-Function. You only proved:
>
> EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
> Etc...

Indeed. It seems to me that he actually thinks that this somehow "restricts" 'add' to IN. What an idiot.

As if [ALL(a):ALL(b):[a e n & b e n => plus(a,b) e n] would not hold too (with plus: Z x Z --> Z, the usual addition on Z).

Moreover, he claims that

ALL(add):ALL(add'):[

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

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

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

proves that "the add function is unique".

Actually, he already commits an error when talking about THE add function in this context.

His "theorem" above amounts to the claim that two funcions which agree an a certain set X agree on the set X. Holy shit!

Yeah, for all x,y e IN: x +_IN y = x +_Z y.

BUT THAT DOES NOT MEAN that +_IN = +_Z.

What's the matter with this guy?

On Monday, May 2, 2022 at 6:42:53 AM UTC+2, Dan Christensen wrote:

> The add function here is also unique:
>
> ALL(add):ALL(add'):[
>
> ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
> & ALL(a):[a e n => add(a,0)=a]
> & ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]
>
> & ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
> & ALL(a):[a e n => add'(a,0)=a]
> & ALL(a):ALL(b):[a e n & b e n => add'(a,s(b))=s(add'(a,b))]
>
> => ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]]

Actually, you already commit an error when you are talking about THE add function in this context.

His "theorem" above amounts to the claim that two functions which agree an a certain set X agree on the set X. Holy shit!

Yeah, for all n,m e IN: n +_IN m = n +_Z m.

BUT THAT DOES NOT MEAN that +_IN = +_Z. (Hint: dom(+_IN) = IN x IN, and dom(+_Z) = Z x Z, and IN =/= Z.)

What's the matter with you?

On Monday, May 2, 2022 at 5:42:29 AM UTC+2, Fritz Feldhase wrote:

Correction. I wrote:

> Hint: Defining functions "recursively" works because of the theorem (schema)
>
> E!f(function(f) & f(0) = a & An(n e IN -> f(n+1) = ...f(n)...))
>
> Where
>
> f(0) = a
> f(n+1) = ...f(n)...
>
> are "the defining equations".

Should read:

| [...] because of the theorem (schema)
| | E!f(function(f) & dom(f) = IN & f(0) = a & An(n e IN -> f(n+1) = ...f(n)...))

This is also a nice alternative add, just take the
usual + : N x N -> N, and then define +' : N' x N' -> N'
where we have, where ? is the sole "dark element":

N' = N u {?}

+' = + u { (?,a,b) | a e N', b something random from N' }
u { (a,?,b) | a e N, b something random from N' }

This shows somehow that add need not be something
that makes "sense". i.e. what we usually know as
plus operations.

What is more difficult, is to find a formula that is
unprovable, but that also has bounded quantifiers.
This here has no bounded quantifiers:

ALL(x):ALL(y):[add(x,y,0) => x=0 & y=0]

I think something with bounded quantifiers might be
also possible. Not 100% sure. Thats the joker that
Dan Christensen always pulls to justify

his nonsense.

Fritz Feldhase schrieb am Montag, 2. Mai 2022 um 12:49:46 UTC+2:
> What's the matter with this guy?