There are two ways to formally introduce a function in DC Proof:

1. Simply define it without any justification.

EXAMPLE

To define addition on the natural natural numbers, you can introduce an axiom in a single line, something like:

1. ALL(a):ALL(b):[a in n & b in n => a+b in n]
& ALL(a):[a in n => a+0=a]
& ALL(a):ALL(b):[a in n & b in n => a+(b+1)=(a+b)+1
Axiom

Where n is the set of natural numbers.

2. Actually prove the existence of the required function, using previously introduced axiom(s) at beginning of your proof, the axioms of set theory (on the Sets menu) and the rules of logic (on the Logic menu). Could take hundreds of lines of formal proof. (Not for the faint of heart!)

EXAMPLE

Given Peano's Axioms for the natural numbers, prove:

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

Where n is the set of natural numbers and s is the successor function from Peano's Axioms.

https://dcproof.com/ConstructAddFunction.htm (762 lines--I warned you!)

Then you may also want to prove that there is only one such function of the set of natural numbers:

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 (only another 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

Well if I want to see dark elements, I only have to read
a post by Dan Christensen. After radonized water, and
then snake oil, he is now dealing with Half-Functions.

Latest example:

ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
https://groups.google.com/g/sci.math/c/sYkWEHylBAA/m/7ZKj0kk0AgAJ

You only proved that two extensions agree on NxN.
We still dont know whether there is an add that doesnt extend.

Cringe! LMAO!

Dan Christensen schrieb am Dienstag, 3. Mai 2022 um 21:09:08 UTC+2:
> There are two ways to formally introduce a function in DC Proof:
>
> 1. Simply define it without any justification.
>
> EXAMPLE
>
> To define addition on the natural natural numbers, you can introduce an axiom in a single line, something like:
>
> 1. ALL(a):ALL(b):[a in n & b in n => a+b in n]
> & ALL(a):[a in n => a+0=a]
> & ALL(a):ALL(b):[a in n & b in n => a+(b+1)=(a+b)+1
> Axiom
>
> Where n is the set of natural numbers.
>
> 2. Actually prove the existence of the required function, using previously introduced axiom(s) at beginning of your proof, the axioms of set theory (on the Sets menu) and the rules of logic (on the Logic menu). Could take hundreds of lines of formal proof. (Not for the faint of heart!)
>
> EXAMPLE
>
> Given Peano's Axioms for the natural numbers, prove:
>
> 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))]]
>
> Where n is the set of natural numbers and s is the successor function from Peano's Axioms.
>
> https://dcproof.com/ConstructAddFunction.htm (762 lines--I warned you!)
>
> Then you may also want to prove that there is only one such function of the set of natural numbers:
>
> 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 (only another 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

So what went wrong? My critique was, this here is nonesense:

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

He should prove:

EXISTUNIQUE(add):[add : N x N -> 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))]]

What did he do? Practically nothing!

For the upteenth time add : N x N -> N means that add doesnt extend
outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
he has such an add inside his proof. But the problem is that his

function axiom is nonsense. It doesnt give a function that does not extend.
It rather gives a whole bunch of function that extend. He should it
call function extension axiom, or half-function axiom.

Mostowski Collapse schrieb am Mittwoch, 4. Mai 2022 um 01:04:24 UTC+2:
> Well if I want to see dark elements, I only have to read
> a post by Dan Christensen. After radonized water, and
> then snake oil, he is now dealing with Half-Functions.
>
> Latest example:
> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> https://groups.google.com/g/sci.math/c/sYkWEHylBAA/m/7ZKj0kk0AgAJ
>
> You only proved that two extensions agree on NxN.
> We still dont know whether there is an add that doesnt extend.
>
> Cringe! LMAO!
> Dan Christensen schrieb am Dienstag, 3. Mai 2022 um 21:09:08 UTC+2:
> > There are two ways to formally introduce a function in DC Proof:
> >
> > 1. Simply define it without any justification.
> >
> > EXAMPLE
> >
> > To define addition on the natural natural numbers, you can introduce an axiom in a single line, something like:
> >
> > 1. ALL(a):ALL(b):[a in n & b in n => a+b in n]
> > & ALL(a):[a in n => a+0=a]
> > & ALL(a):ALL(b):[a in n & b in n => a+(b+1)=(a+b)+1
> > Axiom
> >
> > Where n is the set of natural numbers.
> >
> > 2. Actually prove the existence of the required function, using previously introduced axiom(s) at beginning of your proof, the axioms of set theory (on the Sets menu) and the rules of logic (on the Logic menu). Could take hundreds of lines of formal proof. (Not for the faint of heart!)
> >
> > EXAMPLE
> >
> > Given Peano's Axioms for the natural numbers, prove:
> >
> > 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))]]
> >
> > Where n is the set of natural numbers and s is the successor function from Peano's Axioms.
> >
> > https://dcproof.com/ConstructAddFunction.htm (762 lines--I warned you!)
> >
> > Then you may also want to prove that there is only one such function of the set of natural numbers:
> >
> > 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 (only another 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

> So what went wrong? My critique was, this here is nonesense:
> 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))]]

It works, Jan Burse. Must be frustrating as hell for you.

> He should prove:
>
> EXISTUNIQUE(add):[add : N x N -> 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))]]

It's all there, Jan Burse. Read 'em and weep!

> What did he do? Practically nothing!
>
> For the upteenth time add : N x N -> N means that add doesnt extend
> outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> he has such an add inside his proof. But the problem is that his
>
> function axiom is nonsense.

The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences outside of a function's domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because they UNDEFINED there. Jan Burse still doesn't get it..

It all works, Jan Burse. Deal with it.

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, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> So what went wrong? My critique was, this here is nonesense:
> 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))]]

It works, Jan Burse. Must be frustrating as hell for you.

> He should prove:
>
> EXISTUNIQUE(add):[add : N x N -> 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))]]

It's all there, Jan Burse. Read 'em and weep!

> What did he do? Practically nothing!
>
> For the upteenth time add : N x N -> N means that add doesnt extend
> outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> he has such an add inside his proof. But the problem is that his
>
> function axiom is nonsense.

The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.

It all works, Jan Burse. Deal with it.

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, 4 May 2022 at 02:17:06 UTC+2, Dan Christensen wrote:
> On Tuesday, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> > So what went wrong? My critique was, this here is nonesense:
> > 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))]]
> It works, Jan Burse. Must be frustrating as hell for you.
> > He should prove:
> >
> > EXISTUNIQUE(add):[add : N x N -> 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))]]
> It's all there, Jan Burse. Read 'em and weep!
> > What did he do? Practically nothing!
> >
> > For the upteenth time add : N x N -> N means that add doesnt extend
> > outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> > he has such an add inside his proof. But the problem is that his
> >
> > function axiom is nonsense.
> The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.
>
> It all works, Jan Burse. Deal with it.

You still don't know what you are talking about:
<https://en.wikipedia.org/wiki/Partial_function>

A "function" that doesn't come with domain and codomain
attached is simply not a "function". The same already goes
for "relations". As I have explained recently in another thread.

Julio

On Tuesday, May 3, 2022 at 9:00:11 PM UTC-4, ju...@diegidio.name wrote:
> On Wednesday, 4 May 2022 at 02:17:06 UTC+2, Dan Christensen wrote:
> > On Tuesday, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> > > So what went wrong? My critique was, this here is nonesense:
> > > 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))]]
> > It works, Jan Burse. Must be frustrating as hell for you.
> > > He should prove:
> > >
> > > EXISTUNIQUE(add):[add : N x N -> 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))]]
> > It's all there, Jan Burse. Read 'em and weep!
> > > What did he do? Practically nothing!
> > >
> > > For the upteenth time add : N x N -> N means that add doesnt extend
> > > outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> > > he has such an add inside his proof. But the problem is that his
> > >
> > > function axiom is nonsense.
> > The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.
> >
> > It all works, Jan Burse. Deal with it.
> You still don't know what you are talking about:
> <https://en.wikipedia.org/wiki/Partial_function>
>
> A "function" that doesn't come with domain and codomain
> attached is simply not a "function". The same already goes
> for "relations". As I have explained recently in another thread.
>

In this case, the domain was NxN and the codomain was N. These were used to construct the graph.

Dan

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

You did not prove and display for add from your theorem:

dom(add) = NxN

Its not a problem of partial functions, i.e. functions
having a smaller domain than NxN, its a problem of
function extensions, i.e larger domain than NxN.

Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 03:20:11 UTC+2:
> On Tuesday, May 3, 2022 at 9:00:11 PM UTC-4, ju...@diegidio.name wrote:
> > On Wednesday, 4 May 2022 at 02:17:06 UTC+2, Dan Christensen wrote:
> > > On Tuesday, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> > > > So what went wrong? My critique was, this here is nonesense:
> > > > 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))]]
> > > It works, Jan Burse. Must be frustrating as hell for you.
> > > > He should prove:
> > > >
> > > > EXISTUNIQUE(add):[add : N x N -> 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))]]
> > > It's all there, Jan Burse. Read 'em and weep!
> > > > What did he do? Practically nothing!
> > > >
> > > > For the upteenth time add : N x N -> N means that add doesnt extend
> > > > outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> > > > he has such an add inside his proof. But the problem is that his
> > > >
> > > > function axiom is nonsense.
> > > The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.
> > >
> > > It all works, Jan Burse. Deal with it.
> > You still don't know what you are talking about:
> > <https://en.wikipedia.org/wiki/Partial_function>
> >
> > A "function" that doesn't come with domain and codomain
> > attached is simply not a "function". The same already goes
> > for "relations". As I have explained recently in another thread.
> >
> In this case, the domain was NxN and the codomain was N. These were used to construct the graph.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

We need this:
dom(add) = NxN

for add : NxN -> N, it is equivalent to:
dom(add) ⊆ NxN and NxN ⊆ dom(add)

what you proved:
ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]

Might imply NxN ⊆ dom(add), but where is dom(add) ⊆ NxN ?

Mostowski Collapse schrieb am Mittwoch, 4. Mai 2022 um 08:19:52 UTC+2:
> You did not prove and display for add from your theorem:
>
> dom(add) = NxN
>
> Its not a problem of partial functions, i.e. functions
> having a smaller domain than NxN, its a problem of
> function extensions, i.e larger domain than NxN.
> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 03:20:11 UTC+2:
> > On Tuesday, May 3, 2022 at 9:00:11 PM UTC-4, ju...@diegidio.name wrote:
> > > On Wednesday, 4 May 2022 at 02:17:06 UTC+2, Dan Christensen wrote:
> > > > On Tuesday, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> > > > > So what went wrong? My critique was, this here is nonesense:
> > > > > 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))]]
> > > > It works, Jan Burse. Must be frustrating as hell for you.
> > > > > He should prove:
> > > > >
> > > > > EXISTUNIQUE(add):[add : N x N -> 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))]]
> > > > It's all there, Jan Burse. Read 'em and weep!
> > > > > What did he do? Practically nothing!
> > > > >
> > > > > For the upteenth time add : N x N -> N means that add doesnt extend
> > > > > outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> > > > > he has such an add inside his proof. But the problem is that his
> > > > >
> > > > > function axiom is nonsense.
> > > > The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.
> > > >
> > > > It all works, Jan Burse. Deal with it.
> > > You still don't know what you are talking about:
> > > <https://en.wikipedia.org/wiki/Partial_function>
> > >
> > > A "function" that doesn't come with domain and codomain
> > > attached is simply not a "function". The same already goes
> > > for "relations". As I have explained recently in another thread.
> > >
> > In this case, the domain was NxN and the codomain was N. These were used to construct the graph.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

ɯosʇoʍsʞı ɔoןןɐdsǝ ʍɹoʇǝ:

> ʎon pıp uoʇ dɹoʌǝ ɐup pısdןɐʎ ɟoɹ ɐpp ɟɹoɯ ʎonɹ ʇɥǝoɹǝɯ:
>
> poɯ(ɐpp) = uxu
>
> ıʇs uoʇ ɐ dɹoqןǝɯ oɟ dɐɹʇıɐן ɟnuɔʇıous, ı.ǝ. ɟnuɔʇıous ɥɐʌıuƃ ɐ sɯɐןןǝɹ
> poɯɐıu ʇɥɐu uxu, ıʇs ɐ dɹoqןǝɯ oɟ ɟnuɔʇıou ǝxʇǝusıous, ı.ǝ ןɐɹƃǝɹ poɯɐıu
> ʇɥɐu uxu.
>
> pɐu ɔɥɹısʇǝusǝu sɔɥɹıǝq ɐɯ ɯıʇʇʍoɔɥ, 4. ɯɐı 2022 nɯ 03:20:11 nʇɔ+2:

amazing dork persons, you two. Nobody undrestand anything. Where is your
mathematics, where are your curved manifolds. And tensors, I don't see
tensors anywhere. You guys, no *mathematical_beauty* anywhere.

Now they found the passport of Adolf Hitler. It
says special features: "kleiner Penis"
Адольф Гитлер по паспорту
https://cont.ws/@levmyshkin/2277192
Just like nymshifter.
Esam Inao schrieb am Mittwoch, 4. Mai 2022 um 12:30:45 UTC+2:
> ɯosʇoʍsʞı ɔoןןɐdsǝ ʍɹoʇǝ:
>
> > ʎon pıp uoʇ dɹoʌǝ ɐup pısdןɐʎ ɟoɹ ɐpp ɟɹoɯ ʎonɹ ʇɥǝoɹǝɯ:
> >
> > poɯ(ɐpp) = uxu
> >
> > ıʇs uoʇ ɐ dɹoqןǝɯ oɟ dɐɹʇıɐן ɟnuɔʇıous, ı.ǝ. ɟnuɔʇıous ɥɐʌıuƃ ɐ sɯɐןןǝɹ
> > poɯɐıu ʇɥɐu uxu, ıʇs ɐ dɹoqןǝɯ oɟ ɟnuɔʇıou ǝxʇǝusıous, ı.ǝ ןɐɹƃǝɹ poɯɐıu
> > ʇɥɐu uxu.
> >
> > pɐu ɔɥɹısʇǝusǝu sɔɥɹıǝq ɐɯ ɯıʇʇʍoɔɥ, 4. ɯɐı 2022 nɯ 03:20:11 nʇɔ+2:
>
> amazing dork persons, you two. Nobody undrestand anything. Where is your
> mathematics, where are your curved manifolds. And tensors, I don't see
> tensors anywhere. You guys, no *mathematical_beauty* anywhere.

Must be a very authentic passport then, it really says
"kleiner Penis" (= small penis) in the "Personenbeschreibung"
(= Person description) box of Adolf Hitler:
https://ribalych.com/wp-content/uploads/2014/03/2373.jpg
LMAO!
Mostowski Collapse schrieb am Mittwoch, 4. Mai 2022 um 12:44:11 UTC+2:
> Now they found the passport of Adolf Hitler. It
> says special features: "kleiner Penis"
>
> Адольф Гитлер по паспорту
> https://cont.ws/@levmyshkin/2277192
>
> Just like nymshifter.
> Esam Inao schrieb am Mittwoch, 4. Mai 2022 um 12:30:45 UTC+2:
> > ɯosʇoʍsʞı ɔoןןɐdsǝ ʍɹoʇǝ:
> >
> > > ʎon pıp uoʇ dɹoʌǝ ɐup pısdןɐʎ ɟoɹ ɐpp ɟɹoɯ ʎonɹ ʇɥǝoɹǝɯ:
> > >
> > > poɯ(ɐpp) = uxu
> > >
> > > ıʇs uoʇ ɐ dɹoqןǝɯ oɟ dɐɹʇıɐן ɟnuɔʇıous, ı.ǝ. ɟnuɔʇıous ɥɐʌıuƃ ɐ sɯɐןןǝɹ
> > > poɯɐıu ʇɥɐu uxu, ıʇs ɐ dɹoqןǝɯ oɟ ɟnuɔʇıou ǝxʇǝusıous, ı.ǝ ןɐɹƃǝɹ poɯɐıu
> > > ʇɥɐu uxu.
> > >
> > > pɐu ɔɥɹısʇǝusǝu sɔɥɹıǝq ɐɯ ɯıʇʇʍoɔɥ, 4. ɯɐı 2022 nɯ 03:20:11 nʇɔ+2:
> >
> > amazing dork persons, you two. Nobody undrestand anything. Where is your
> > mathematics, where are your curved manifolds. And tensors, I don't see
> > tensors anywhere. You guys, no *mathematical_beauty* anywhere.

Dan Christensen wrote:

>> So what went wrong? My critique was, this here is nonesense:
>> 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))]]
>
> It works, Jan Burse. Must be frustrating as hell for you.

Canadian General captured in Mariupol and transferred to Moscow?
https://www.thetruthseeker.co.uk/wordpress/wp-content/uploads/2022/05/Gen-General-Trevor-Kadie.jpg
https://www.thetruthseeker.co.uk/?p=253053

Russian rouble hits more than 2-year high vs euro
https://www.thetruthseeker.co.uk/?p=253018
If these US sanctions come in, then you can kiss your ass to any type of economy, apart from a war economy.

It’s coming, sheeple in their garden sheds making widgets that were once made in China, they might make £10 per day, cus this is where its going. By next Winter, sheeple will be standing in the street huddled around their IKEA fueled fire moaning to their neighbours about the fact that the Chinese have cheap gas and oil as the Asian economy explodes. Germany is finished, if they ban all Ruusian gas.

Crackpot is back to crackpotting. And you ma''am, stick to bashing DC Poop and stay out of topics dealing with Euro-Asian history - you know nothing on that. OK???

On Tuesday, May 3, 2022 at 7:04:24 PM UTC-4, Mostowski Collapse wrote:
> Well if I want to see dark elements, I only have to read
> a post by Dan Christensen. After radonized water, and
> then snake oil, he is now dealing with Half-Functions.
>
> Latest example:
> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> https://groups.google.com/g/sci.math/c/sYkWEHylBAA/m/7ZKj0kk0AgAJ
>
> You only proved that two extensions agree on NxN.
> We still dont know whether there is an add that doesnt extend.
>
> Cringe! LMAO!
> Dan Christensen schrieb am Dienstag, 3. Mai 2022 um 21:09:08 UTC+2:
> > There are two ways to formally introduce a function in DC Proof:
> >
> > 1. Simply define it without any justification.
> >
> > EXAMPLE
> >
> > To define addition on the natural natural numbers, you can introduce an axiom in a single line, something like:
> >
> > 1. ALL(a):ALL(b):[a in n & b in n => a+b in n]
> > & ALL(a):[a in n => a+0=a]
> > & ALL(a):ALL(b):[a in n & b in n => a+(b+1)=(a+b)+1
> > Axiom
> >
> > Where n is the set of natural numbers.
> >
> > 2. Actually prove the existence of the required function, using previously introduced axiom(s) at beginning of your proof, the axioms of set theory (on the Sets menu) and the rules of logic (on the Logic menu). Could take hundreds of lines of formal proof. (Not for the faint of heart!)
> >
> > EXAMPLE
> >
> > Given Peano's Axioms for the natural numbers, prove:
> >
> > 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))]]
> >
> > Where n is the set of natural numbers and s is the successor function from Peano's Axioms.
> >
> > https://dcproof.com/ConstructAddFunction.htm (762 lines--I warned you!)
> >
> > Then you may also want to prove that there is only one such function of the set of natural numbers:
> >
> > 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 (only another 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

One idiot more who needs pampers because he shat his pants.

Mathin3D schrieb am Mittwoch, 4. Mai 2022 um 14:44:44 UTC+2:
> Crackpot is back to crackpotting. And you ma''am, stick to bashing DC Poop and stay out of topics dealing with Euro-Asian history - you know nothing on that. OK???

On Wednesday, May 4, 2022 at 2:19:52 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 03:20:11 UTC+2:
> > On Tuesday, May 3, 2022 at 9:00:11 PM UTC-4, ju...@diegidio.name wrote:
> > > On Wednesday, 4 May 2022 at 02:17:06 UTC+2, Dan Christensen wrote:
> > > > On Tuesday, May 3, 2022 at 7:12:27 PM UTC-4, Mostowski Collapse wrote:
> > > > > So what went wrong? My critique was, this here is nonesense:
> > > > > 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))]]
> > > > It works, Jan Burse. Must be frustrating as hell for you.
> > > > > He should prove:
> > > > >
> > > > > EXISTUNIQUE(add):[add : N x N -> 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))]]
> > > > It's all there, Jan Burse. Read 'em and weep!
> > > > > What did he do? Practically nothing!
> > > > >
> > > > > For the upteenth time add : N x N -> N means that add doesnt extend
> > > > > outside of N x N , i.e. dom(add) = N x N and nothing bigger. I think
> > > > > he has such an add inside his proof. But the problem is that his
> > > > >
> > > > > function axiom is nonsense.
> > > > The crank, Jan Burse, is pissed off that the function axiom, as is the common practice, won't let him make logical inferences about a function outside of its domain of definition -- his DARK ELEMENTS. As every first year math student knows, that's because functions are UNDEFINED there. Jan Burse still doesn't get it.
> > > >
> > > > It all works, Jan Burse. Deal with it.
> > > You still don't know what you are talking about:
> > > <https://en.wikipedia.org/wiki/Partial_function>
> > >
> > > A "function" that doesn't come with domain and codomain
> > > attached is simply not a "function". The same already goes
> > > for "relations". As I have explained recently in another thread.
> > >
> > In this case, the domain was NxN and the codomain was N. These were used to construct the graph.

> You did not prove and display for add from your theorem:
>
> dom(add) = NxN
>

Not necessary. Again, I proved: ALL(a):ALL(b):[a in n & b in n => add(a,b) in n] where n is the set of natural numbers.

> Its not a problem of partial functions, i.e. functions
> having a smaller domain than NxN, its a problem of
> function extensions, i.e larger domain than NxN.

It is not a problem in this case. We are not talking about your "dark elements," just the set of all 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

This doesn't give you a function space member:

(Ordinary) function space:
f : X -> Y :<=> dom(f)=X & ...

It only gives you a extension function space member:

Extension function space:
f : X => Y :<=> X⊆dom(f) & ...

See the difference?

Dan Christensen schrieb:
>> You did not prove and display for add from your theorem:
>>
>> dom(add) = NxN
>>
>
> Not necessary. Again, I proved: ALL(a):ALL(b):[a in n & b in n => add(a,b) in n] where n is the set of natural numbers.

On Wednesday, May 4, 2022 at 2:31:39 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> We need this:
> dom(add) = NxN
>

Nope. See my previous reply to you.

> for add : NxN -> N, it is equivalent to:
> dom(add) ⊆ NxN and NxN ⊆ dom(add)
>
> what you proved:
> ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]

> Might imply NxN ⊆ dom(add), but where is dom(add) ⊆ NxN ?

It should be obvious even to you, Jan Burse, that we are talking about and ONLY about the set of natural numbers. Sorry, your "dark elements" simply don't enter into it.

Maybe you could concoct your own function axiom that would allow you to make logical inferences about functions outside of their domains of definition.. Use the Axiom Rule on the Logic menu.

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, May 4, 2022 at 9:37:10 AM UTC-4, Mostowski Collapse wrote:
> This doesn't give you a function space member:
>

Who said anything about function spaces? Are you hearing voices in your head, Jan Burse?

We are talking here about and ONLY about addition on the set of natural numbers. Why is that such a problem for you?

Dan

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

About your Peano:

s : Q -> Q

Does also satisfy the axioms?

Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 16:23:18 UTC+2:
> I use:
>
> 1. Set(n)
> Axiom
>
> 2. 0 in n
> Axiom
>
> 3. ALL(a):[a in n => s(a) in n]
> Axiom
>
> 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> Axiom
>
> 5. ALL(a):[a in n => ~s(a)=0]
> Axiom
> 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in a => s(b) in a]
> => ALL(b):[b in n => b in a]]]
> Axiom
> Where n is the set of natural numbers.
> Dan

Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 15:58:50 UTC+2:
> On Wednesday, May 4, 2022 at 9:37:10 AM UTC-4, Mostowski Collapse wrote:
> > This doesn't give you a function space member:
> >
> Who said anything about function spaces? Are you hearing voices in your head, Jan Burse?
>
> We are talking here about and ONLY about addition on the set of natural numbers. Why is that such a problem for you?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So you cannot prove this here, assuming that we
use Fritz application and extend {} to make =< false,
when it appears LHS or RHS of =<:

ALL(a):[1 =< s(a) & s(a) =< 2 => 1 = s(a) v 2 = s(a)]

LMAO!

P.S.: Maybe there is a simpler example?

P.P.S.: Ok thats extremely challenging, this dealing
with elements outside of the domain of a function.
But you need it in calculus, look at John Gabriel

and his division by zero.

Mostowski Collapse schrieb am Mittwoch, 4. Mai 2022 um 20:55:35 UTC+2:
> About your Peano:
>
> s : Q -> Q
>
> Does also satisfy the axioms?
>
> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 16:23:18 UTC+2:
> > I use:
> >
> > 1. Set(n)
> > Axiom
> >
> > 2. 0 in n
> > Axiom
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > Axiom
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > Axiom
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > Axiom
> > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> > Axiom
> > Where n is the set of natural numbers.
> > Dan
> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 15:58:50 UTC+2:
> > On Wednesday, May 4, 2022 at 9:37:10 AM UTC-4, Mostowski Collapse wrote:
> > > This doesn't give you a function space member:
> > >
> > Who said anything about function spaces? Are you hearing voices in your head, Jan Burse?
> >
> > We are talking here about and ONLY about addition on the set of natural numbers. Why is that such a problem for you?
> > 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, May 4, 2022 at 2:55:35 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 16:23:18 UTC+2:
> > I use:
> >
> > 1. Set(n)
> > Axiom
> >
> > 2. 0 in n
> > Axiom
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > Axiom
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > Axiom
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > Axiom
> > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> > Axiom
> > Where n is the set of natural numbers.
> > Dan
> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 15:58:50 UTC+2:
> > On Wednesday, May 4, 2022 at 9:37:10 AM UTC-4, Mostowski Collapse wrote:
> > > This doesn't give you a function space member:
> > >
> > Who said anything about function spaces? Are you hearing voices in your head, Jan Burse?
> >
> > We are talking here about and ONLY about addition on the set of natural numbers. Why is that such a problem for you?

> About your Peano:
>
> s : Q -> Q
>
> Does also satisfy the axioms?
>

No.

s(1/2) is undefined.

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, May 4, 2022 at 2:56:23 PM UTC-4, Mostowski Collapse wrote:
> So you cannot prove this here, assuming that we
> use Fritz application and extend {} to make =< false,
> when it appears LHS or RHS of =<:
>
> ALL(a):[1 =< s(a) & s(a) =< 2 => 1 = s(a) v 2 = s(a)]
>

Seems trivial enough, assuming you are quantifying over N. You have a=0 => a=0 v a=1.

What's your point, 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

s(1/2)=3/2 is possible.

It doesn't violate any of your axioms.

Which axiom is violated?

Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 21:14:00 UTC+2:
> On Wednesday, May 4, 2022 at 2:55:35 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 16:23:18 UTC+2:
> > > I use:
> > >
> > > 1. Set(n)
> > > Axiom
> > >
> > > 2. 0 in n
> > > Axiom
> > >
> > > 3. ALL(a):[a in n => s(a) in n]
> > > Axiom
> > >
> > > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > > Axiom
> > >
> > > 5. ALL(a):[a in n => ~s(a)=0]
> > > Axiom
> > > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > > => [0 in a & ALL(b):[b in a => s(b) in a]
> > > => ALL(b):[b in n => b in a]]]
> > > Axiom
> > > Where n is the set of natural numbers.
> > > Dan
> > Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 15:58:50 UTC+2:
> > > On Wednesday, May 4, 2022 at 9:37:10 AM UTC-4, Mostowski Collapse wrote:
> > > > This doesn't give you a function space member:
> > > >
> > > Who said anything about function spaces? Are you hearing voices in your head, Jan Burse?
> > >
> > > We are talking here about and ONLY about addition on the set of natural numbers. Why is that such a problem for you?
>
> > About your Peano:
> >
> > s : Q -> Q
> >
> > Does also satisfy the axioms?
> >
> No.
>
> s(1/2) is undefined.
> 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, May 4, 2022 at 4:28:07 PM UTC-4, Mostowski Collapse wrote:
> s(1/2)=3/2 is possible.
>

You could certainly construct another successor on Q.

> It doesn't violate any of your axioms.
>

You wouldn't be able to apply the usual successor function. It's, for all elements in N, etc. Not for all elements in Q.

Dan

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