Formal proofs about functions using DC Proof

[Dan Christensen]

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

[Mostowski Collapse]

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!

[Mostowski Collapse]

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.

[Dan Christensen]

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.

[Julio Di Egidio]

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

[Dan Christensen]

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

[Mostowski Collapse]

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.

[Mostowski Collapse]

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 ?

[Esam Inao]

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

[Mostowski Collapse]

Now they found the passport of Adolf Hitler. It
says special features: "kleiner Penis"

Адольф Гитлер по паспорту
https://cont.ws/@levmyshkin/2277192

Just like nymshifter.

[Mostowski Collapse]

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!

[Esam Inao]

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.

[Mathin3D]

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

[Mostowski Collapse]

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

[Dan Christensen]

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

[Mostowski Collapse]

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:

[Dan Christensen]

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

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?

[Mostowski Collapse]

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

[Mostowski Collapse]

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.

[Dan Christensen]

No.

s(1/2) is undefined.

[Dan Christensen]

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?

[Mostowski Collapse]

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

It doesn't violate any of your axioms.

Which axiom is violated?

[Dan Christensen]

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.

And the Induction Axiom wouldn't hold.

[Lanny Torii]

Dan Christensen wrote:

> 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

you gave that "program" the initials of your name, are you insane? Who
does that. You look like a slavic nazi turned anglo-saxon overnight.

[Lanny Torii]

Dan Christensen wrote:

> On Wednesday, May 4, 2022 at 2:31:39 AM UTC-4, Mostowski Collapse (aka

>> We need this: dom(add) = NxN
>
> Nope. See my previous reply to you.

No. See this first.


String of suicides prompts relocation of US aircraft carrier sailors
https://cdni.russiatoday.com/files/2022.05/l/62728dce85f5407a436ac8a6.jpg
https://www.rt.com/news/554961-george-washington-sailors-suicide/
Over 200 sailors have been re-housed from the USS George Washington
aircraft carrier

US training Ukrainians at ex-Nazi Wehrmacht base
https://www.rt.com/russia/554975-training-ukraine-troops-germany/
The US has been training Ukrainian forces for eight years and is using a
major base in Germany to continue doing so, a top general said

'An act of genocide': A witness recalls the 2014 Odessa massacre
https://www.rt.com/russia/554946-tragedy-odessa-protests-ukraine/

[Dan Christensen]

WAR OF AGRESSION = NAZI

How's that Blitzkrieg going, Nazi Boy? (Hee, hee!)

[Mostowski Collapse]

Why would your induction axiom not hold if s(1/2)=3/2.

You only say:

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

So you talk about sets b which are subset of n.

[Mostowski Collapse]

Corr.: Typo

So you talk about sets a which are subset of n.

[Lanny Torii]

Dan Christensen wrote:

>> US training Ukrainians at ex-Nazi Wehrmacht base
>> https://www.rt.com/russia/554975-training-ukraine-troops-germany/
>> The US has been training Ukrainian forces for eight years and is using
>> a major base in Germany to continue doing so, a top general said
>>
>> 'An act of genocide': A witness recalls the 2014 Odessa massacre
>> https://www.rt.com/russia/554946-tragedy-odessa-protests-ukraine/
>
> WAR OF AGRESSION = NAZI
> How's that Blitzkrieg going, Nazi Boy? (Hee, hee!)

no such thing, but the western europe and cacanada, did lost huge storage
of nazi_armament, a few generals and alot of nazi illegal combatants, in
the process. It stays by the mainstream media tv and newspapers. And they
want to lose more. The prices on food and fuel already exceed the double,
food shortage, heat shortage, detergent shortages and so on. How blitz
would be that??

[Dan Christensen]

On Wednesday, May 4, 2022 at 5:29:19 PM UTC-4, Mostowski Collapse wrote:
> Why would your induction axiom not hold if s(1/2)=3/2.
>

You would have to introduce quite a different successor function to capture all of the rationals.

> You only say:
> > 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]]]
> So you talk about sets b which are subset of n.

Not subsets of Q.

[Dan Christensen]

On Wednesday, May 4, 2022 at 5:37:19 PM UTC-4, Lanny Torii wrote:
> Dan Christensen wrote:
>
> >> US training Ukrainians at ex-Nazi Wehrmacht base
> >> https://www.rt.com/russia/554975-training-ukraine-troops-germany/
> >> The US has been training Ukrainian forces for eight years and is using
> >> a major base in Germany to continue doing so, a top general said
> >>
> >> 'An act of genocide': A witness recalls the 2014 Odessa massacre
> >> https://www.rt.com/russia/554946-tragedy-odessa-protests-ukraine/
> >
> > WAR OF AGRESSION = NAZI
> > How's that Blitzkrieg going, Nazi Boy? (Hee, hee!)

> no such thing, but the western europe and cacanada...

Just keep that sturdy length of rope handy, Nazi Boy. You may need it.

[Lanny Torii]

What cacanada, you have to move from cacanada, immigrant. Provable you are
a nazi individual, born like that, in a family where nazism was built in
the system. Here some other proofs. Watch carefully the blitz, because you
don't know what you do.

UKRAINE WAR IN 17 SEC IT STARTS WHEN THE CAMERA IS ON AND IT STOPS WHEN
THE CAMERA IS OFF GET IT https://www.bitchute.com/video/CTYjHQsAj3VL/

[Dan Christensen]

On Wednesday, May 4, 2022 at 6:12:08 PM UTC-4, Lanny Torii wrote:
> Dan Christensen wrote:
>
> >> >> US training Ukrainians at ex-Nazi Wehrmacht base
> >> >> https://www.rt.com/russia/554975-training-ukraine-troops-germany/
> >> >> The US has been training Ukrainian forces for eight years and is
> >> >> using a major base in Germany to continue doing so, a top general
> >> >> said
> >> >>
> >> >> 'An act of genocide': A witness recalls the 2014 Odessa massacre
> >> >> https://www.rt.com/russia/554946-tragedy-odessa-protests-ukraine/
> >> >
> >> > WAR OF AGRESSION = NAZI How's that Blitzkrieg going, Nazi Boy? (Hee,
> >> > hee!)
> >> no such thing, but the western europe and cacanada...
> >
> > Just keep that sturdy length of rope handy, Nazi Boy. You may need it.
> What cacanada, you have to move from cacanada, immigrant. Provable you are
> a nazi individual, born like that, in a family where nazism was built in
> the system. Here some other proofs. Watch carefully the blitz, because you
> don't know what you do.
>

Looks like you might be turning in your keyboard for a spiffy SS uniform in the next week or so, Nazi Boy!

[Mostowski Collapse]

Nothing prevents your Peano axioms from being satisfied by for example:

s : Q -> Q

So they are nonsens…

[Dan Christensen]

On Thursday, May 5, 2022 at 1:06:26 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 23:50:27 UTC+2:
> > On Wednesday, May 4, 2022 at 5:29:19 PM UTC-4, Mostowski Collapse wrote:
> > > Why would your induction axiom not hold if s(1/2)=3/2.
> > >
> > You would have to introduce quite a different successor function to capture all of the rationals.
> > > You only say:
> > > > 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]]]

> > > So you talk about sets b which are subset of n.
> > Not subsets of Q.

> Nothing prevents your Peano axioms from being satisfied by for example:
>
> s : Q -> Q
>

s(-1) = ???

Can't be 0. That would contradict the 4th Axiom.

[Mostowski Collapse]

Since when is -1 e n ? Your axiom only says:

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

So its possible to have s(-1)=0, which would be the case if s : Q -> Q.

[Grant Shirasu]

Dan Christensen wrote:

> s(-1) = ??? Can't be 0. That would contradict the 4th Axiom. Dan
> Download my DC Proof 2.0 freeware at http://www.dcproof.com Visit my
> Math Blog at http://www.dcproof.wordpress.com

how could you ever be "programming" something like that.

the problem you have is that the nazi "ukrainians" may be nazis, educating
their children in being strong nazis, but if one came along saying it,
then *aioe.org* would exclud *sci.physics.relativity* from posting. I
believe a nazi bitch named *Thomas_Pointedhead* / *Big_Dog* did it. This
world is fucked up, my friend. Try again.

Another Ukraine Citizens About Ukraine Nazi Forces
https://www.bitchute.com/video/XzJR1vo222cT/

HITLER'S NEW AGE RELIGION 'CROSSDRESSER NAZI SOLDIERS'
https://www.bitchute.com/video/t8yOLyjNcAFB/
one more proof, the khazar zelenske is a nazi.

2022.05.04 Russian Sanctions On Europe
https://www.bitchute.com/video/i2e0EBj6PmiX/
you have to move away from fake_money western europe, now as you can. The
*fake_money* took their corrupt minds in a parallel world. They truly
believe in their fake_money, which is historically.

[Dan Christensen]

On Thursday, May 5, 2022 at 10:23:33 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 5. Mai 2022 um 15:50:56 UTC+2:
> > On Thursday, May 5, 2022 at 1:06:26 AM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Mittwoch, 4. Mai 2022 um 23:50:27 UTC+2:
> > > > On Wednesday, May 4, 2022 at 5:29:19 PM UTC-4, Mostowski Collapse wrote:
> > > > > Why would your induction axiom not hold if s(1/2)=3/2.
> > > > >
> > > > You would have to introduce quite a different successor function to capture all of the rationals.
> > > > > You only say:
> > > > > > 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]]]
> >
> > > > > So you talk about sets b which are subset of n.
> > > > Not subsets of Q.
> > > Nothing prevents your Peano axioms from being satisfied by for example:
> > >
> > > s : Q -> Q
> > >
> > s(-1) = ???
> >
> > Can't be 0. That would contradict the 4th Axiom.

> Since when is -1 e n ? Your axiom only says:
>
> ALL(a):[a in n => ~s(a)=0]

> So its possible to have s(-1)=0, which would be the case if s : Q -> Q.

What do you imagine is the next rational number after 0, Jan Burse? Can't be 1 since there are infinitely many rational numbers between 0 and 1. How will you get to 1/2 starting from 0?

[Dan Christensen]

On Thursday, May 5, 2022 at 11:03:10 AM UTC-4, Grant Shirasu wrote:

>
> the problem you have is that the nazi "ukrainians" may be nazis, educating

WAR OF AGRESSION = NAZI

Looks like you may soon be turning in your keyboard for a spiffy new SS uniform on your way to the Ukrainian front, Nazi Boy. Won't you have fun raping and murdering Ukrainian women and children!

[Mostowski Collapse]

I dont have to get to 1/2, I only said s : Q -> Q, does
also satisfy your axioms. I did nowhere say that your
axioms construct Q. But every s : A -> B, with:

s | N = succ

Satisfies your axioms, where succ : N -> N is the
usual successor function on the natural numbers.
f | A is a notation from set theory, it denotes

the function f restricted to the domain A.

[Grant Shirasu]

Mostowski Collapse wrote:

> I dont have to get to 1/2, I only said s : Q -> Q, does also satisfy
> your axioms. I did nowhere say that your axioms construct Q. But every s
> : A -> B, with: s | N = succ

yet another *Sulky_Liver_Sausage*.

https://youtu.be/R7MOsliXbtc

the problem you have is that the nazi "ukrainians" may be nazis, educating

their children in being strong nazis, but if one came along saying it,

then *aioe.org* would exclude *sci.physics.relativity* from posting. I

[Mostowski Collapse]

The proof is pretty easy, just observe that
because s | N = succ we have of course:

/* Restriction Lemma */
ALL(a):[a e N => s(a) = succ(a)]

Now since all your axioms are of the form
ALL(a):[a e N => … ] and since the induction
axiom only talks about subsets of N,

we see it is enough for a function s : A -> B
to satisfy s | N = succ to then satisfy your
axioms. If I am not totally mistaken, the

converse can be also shown.

[Dan Christensen]

On Thursday, May 5, 2022 at 1:39:37 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 5. Mai 2022 um 17:15:18 UTC+2:
> > On Thursday, May 5, 2022 at 10:23:33 AM UTC-4, Mostowski Collapse wrote:
> >
> > > So its possible to have s(-1)=0, which would be the case if s : Q -> Q.
> > What do you imagine is the next rational number after 0, Jan Burse? Can't be 1 since there are infinitely many rational numbers between 0 and 1. How will you get to 1/2 starting from 0?

> I dont have to get to 1/2,

Actually, you do, Jan Burse. If you claim to have a successor function on Q, you must be able to get from 0 to 1/2 by means of repeated application of that function. Otherwise, you don't really have a successor function on Q.

[snip]

[Mostowski Collapse]

Well the predecessor of 1/2 is -1/2. But I dont have to
reach 1/2 from some natural number as you wrote:

Dan Christensen after sniffing one kilogram cocaine:

> What do you imagine is the next rational number
after 0, Jan Burse? Can't be 1 since there are infinitely
many rational numbers between 0 and 1. How will

you get to 1/2 starting from 0.
https://groups.google.com/g/sci.math/c/sYkWEHylBAA/m/aJnhQLDEAgAJ

LoL

BTW: There are many many functions satisfying
your „Peano Axioms“, like for example:

succZ : Z -> Z, x |-> x+1
succQ : Q -> Q, x |-> x+1
succR : R -> R, x |-> x+1
succC : C -> C, x |-> x+1

C are the complex numbers. These functions all satisfy
your „Peano Axioms“ because these functions all satisfy

succZ | N = succQ | N = succR | N = succC | N = succN

and because of the way you wrote down your axioms.

[Mostowski Collapse]

Because succQ(-1/2)=1/2 we have succQ^(-1)(1/2)=-1/2.
Too much math in one day, or whats the prololoblem?

LMAO!

[Dan Christensen]

On Thursday, May 5, 2022 at 2:51:37 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 5. Mai 2022 um 20:12:44 UTC+2:
> > On Thursday, May 5, 2022 at 1:39:37 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Donnerstag, 5. Mai 2022 um 17:15:18 UTC+2:
> > > > On Thursday, May 5, 2022 at 10:23:33 AM UTC-4, Mostowski Collapse wrote:
> > > >
> > > > > So its possible to have s(-1)=0, which would be the case if s : Q -> Q.
> > > > What do you imagine is the next rational number after 0, Jan Burse? Can't be 1 since there are infinitely many rational numbers between 0 and 1. How will you get to 1/2 starting from 0?
> > > I dont have to get to 1/2,
> > Actually, you do, Jan Burse. If you claim to have a successor function on Q, you must be able to get from 0 to 1/2 by means of repeated application of that function. Otherwise, you don't really have a successor function on Q.
> >

> Well the predecessor of 1/2 is -1/2. But I dont have to
> reach 1/2 from some natural number as you wrote:
>

Otherwise, induction doesn't work on the rational numbers. (It doesn't.) Deal with it, Jan Burse.

> Dan Christensen after sniffing one kilogram cocaine:
> > What do you imagine is the next rational number
> after 0, Jan Burse? Can't be 1 since there are infinitely
> many rational numbers between 0 and 1. How will
> you get to 1/2 starting from 0.

So you can't do it. Thought so.

> LoL
>
> BTW: There are many many functions satisfying
> your „Peano Axioms“, like for example:
>
> succZ : Z -> Z, x |-> x+1
> succQ : Q -> Q, x |-> x+1
> succR : R -> R, x |-> x+1
> succC : C -> C, x |-> x+1
>

Sadly for you, none of these supposed "successor functions" can be used as a basis for proof by induction on any of these sets. Just admit you are wrong, Jan Burse. You are looking like a complete idiot here.

[Mostowski Collapse]

Nothing magical. Its really a no brainer.
They only explain why you cannot prove the following:

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

From your "Peano Axioms".

[Dan Christensen]

On Thursday, May 5, 2022 at 4:44:09 PM UTC-4, Mostowski Collapse wrote:
> Nothing magical. Its really a no brainer.
> They only explain why you cannot prove the following:
>
> ALL(a):ALL(b):[s(a)=b => a e n & b e n]
>
>

There would be a serious bug in my program if you could prove such nonsense.

[Mostowski Collapse]

Well the explanation that you cannot prove the below:

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

That your Peano Axioms have models, where there
are pairs a,b with s(a)=b and ~(a e n) or ~(a e n).

One such model is for example:

s : Q -> Q, x |-> x+1

You can take a=-1/2 and b=1/2, we can verify:

s(a)=b
~(a e n)
~(b e n)

Easy exercise, based on the way you formulated
your Peano Axioms.

[Dan Christensen]

On Thursday, May 5, 2022 at 2:51:37 PM UTC-4, Mostowski Collapse wrote:
>
> BTW: There are many many functions satisfying
> your „Peano Axioms“, like for example:
>
> succZ : Z -> Z, x |-> x+1
> succQ : Q -> Q, x |-> x+1
> succR : R -> R, x |-> x+1
> succC : C -> C, x |-> x+1
>

None of these supposed "successor functions" satisfy Peano's Axioms. In each case, there exists x in the respective set such that x+1=0. This effectively violates the 4th Peano Axiom that S(x)=/=0. Deal with it, Jan Burse. Just admit you were wrong.

[Mostowski Collapse]

Well they all satisfy your Peano Axioms. You can go
through each axiom and check whether its satisfied.
Which Axiom is not satisfied. And what are the

instantiations of the Axiom that render it false?
For example if you set s = succQ, which Axiom is
not satisfied, and how is it not satisfied?

Just curious....

[Mostowski Collapse]

For example this axiom is satisfied:

ALL(a):[a e n => ~s(a)=0]

by s = succQ. Which value for the variable "a" do
you take to make it false? The axiom gets false
if you have the following:

(a e n) True
~s(a)=0 False

Can you tell us? Here is material implication, this
the truth table of the => sign in your Axiom:

A B (A → B)
F F T
F T T
T F F
T T T
https://web.stanford.edu/class/cs103/tools/truth-table-tool/

To make the axiom false, you need to provoke row
Nr. 3 of the truth table. Thats the only way to make
material implication false. In row Nr 3. you find

A = T and B = F. So you need to find a value for
the variable "a" that makes (a e n) true and ~s(a)=0
false. How would you do that with s = succQ

Just curious....

[Dan Christensen]

On Thursday, May 5, 2022 at 5:39:10 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 5. Mai 2022 um 23:30:20 UTC+2:
> > On Thursday, May 5, 2022 at 2:51:37 PM UTC-4, Mostowski Collapse wrote:
> > >
> > > BTW: There are many many functions satisfying
> > > your „Peano Axioms“, like for example:
> > >
> > > succZ : Z -> Z, x |-> x+1
> > > succQ : Q -> Q, x |-> x+1
> > > succR : R -> R, x |-> x+1
> > > succC : C -> C, x |-> x+1
> > >
> > None of these supposed "successor functions" satisfy Peano's Axioms. In each case, there exists x in the respective set such that x+1=0. This effectively violates the 4th Peano Axiom that S(x)=/=0. Deal with it, Jan Burse. Just admit you were wrong.

> Well they all satisfy your Peano Axioms.

Wrong again, Jan Burse. Perhaps you are not familiar with Peano's Axioms. Some references:

https://mathworld.wolfram.com/PeanosAxioms.html
https://www.britannica.com/science/Peano-axioms
https://brilliant.org/wiki/peano-axioms/
https://encyclopediaofmath.org/wiki/Peano_axioms
https://proofwiki.org/wiki/Axiom:Peano%27s_Axioms

From DC Proof:

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


Neither of your supposed "successor functions" above satisfies the Peano's Axioms. Each violates 2 of those axioms:

1. There does not exist x in the underlying set such that x + 1 = 0.

In each of the underlying sets, we have -1. And -1 + 1 = 0.

2. For all subsets P of the underlying set, if 0 in P and for all x in P, x+1 is also in P, then P includes all of the underlying set. (Induction)

N is a subset of the each underlying set. 0 in N. For all x in N, x+1 is also in N. And yet, N does NOT include all of the underlying set. It does NOT include -1, which an element of each of the underlying sets.

[Mostowski Collapse]

Since when is -1 e n, dumbo?

Whats wrong with you. For the milllionst time I do not
change n, I only change s. s = succQ perfectly well
satisfies your axioms. You are going bonkers.

I nowhere wrote to change n.

If I would want to change n I would write so. But I only
make a point that you can vary s considerably, and your
Peano Axioms are still satisfied.

Thats pretty easy to see. All these functions:

succZ : Z -> Z, x |-> x+1
succQ : Q -> Q, x |-> x+1
succR : R -> R, x |-> x+1
succC : C -> C, x |-> x+1

Satisfy your Peano Axioms when you set s = succX and
keep n what it is. Do you deny that? The symbol n doesnt change,
how do you want to falsify this axiom with succX:

ALL(a):[a e n => ~s(a)=0]

You cannot falsify it with any of the succX. They all agree
on this fact. We do not have -1 e n.

[Mostowski Collapse]

Dumbo, you have everything right before your eyes, you write it yourself:

Dan Christensen schrieb am Freitag, 6. Mai 2022 um 02:01:53 UTC+2:

> It [you mean N] does NOT include -1
https://groups.google.com/g/sci.math/c/sYkWEHylBAA/m/yU7JqmzhAgAJ

You can still not see that this axiom stays true for succX?

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

Maybe see a doctor and order a new prescription of psychopharmaca.

LMAO!

[Wesi Matsuya]

Dan Christensen wrote:


> Wrong again, Jan Burse. Perhaps you are not familiar with Peano's
> Axioms. Some references:

sure, but the stupid *homepage_designer* nazi wanker Thomas
'PointedEars' Lahn <Point...@web.de> is *facepalm*ing himself now
repeatedly complaining about his own complains. What a fucking idiot. The
nazis of "ukraine" are calling his canceler for *a_sulky_liver_sausage*
and the wankers, the former largest economy of europe, still want to go to
a nazi shithole of a "country" for *kissing_the_ring* of the nazi khazar
zelenske. This is incredible.

[Dan Christensen]

> > 1. [Peano Axiom 4] There does not exist x in the underlying set such that x + 1 = 0.

> >
> > In each of the underlying sets, we have -1. And -1 + 1 = 0.
> >

> > 2. [Peano Axiom 5] For all subsets P of the underlying set, if 0 in P and for all x in P, x+1 is also in P, then P includes all of the underlying set. (Induction)

> >
> > N is a subset of the each underlying set. 0 in N. For all x in N, x+1 is also in N. And yet, N does NOT include all of the underlying set. It does NOT include -1, which an element of each of the underlying sets.

> Since when is -1 e n, dumbo?
>

Geez, yer dumb, Jan Burse!

-1 is NOT an element N, but it is an element of each of the underlying sets of your supposed "successor functions" here. Perhaps you didn't know, but -1 + 1 = 0.

Not only do your supposed "successor functions" violate the axiom that 0 has no predecessor, but as I have shown here, they also violate the induction axiom.

[Mostowski Collapse]

I do not violate any axiom. Do you have a proof that
I violate an axiom. I dont think so. You are only loud
mouthing that something is violated.

But so far you didn't produce a proof. Ok, lets make
the problem dumbo compatible, so that crazy Dan
Christensen also understands it.

Can you prove the alleged axiom violation:

~ALL(a):[a e n => ~s(a)=0]

in set theory and natural deduction, from these axioms here:

1. Your "Peano Axioms"
2. New Axiom: ~(-1 e n)
3. New Axiom: s(-1) = 0

Just curious, how would you prove it? Please show
us a formal DC Proof, so that it is a computer
verified proof, and not some halucination.

Thanks in advance.

[Dan Christensen]

On Friday, May 6, 2022 at 10:40:13 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 6. Mai 2022 um 16:25:28 UTC+2:
> > On Friday, May 6, 2022 at 3:10:32 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > Geez, yer dumb, Jan Burse!
> >
> > -1 is NOT an element N, but it is an element of each of the underlying sets of your supposed "successor functions" here. Perhaps you didn't know, but -1 + 1 = 0.
> >
> > Not only do your supposed "successor functions" violate the axiom that 0 has no predecessor, but as I have shown here, they also violate the induction axiom.

> I do not violate any axiom. Do you have a proof that
> I violate an axiom. I dont think so. You are only loud
> mouthing that something is violated.
>

Still in denial, I see. HA, HA, HA!!!!

Dan

[Mostowski Collapse]

No denial, I don't need to deny anything, because there
is nothing to deny. Only hot vapor. I am waiting for your
proof. Where is your proof? Can you prove the

alleged axiom violation:

~ALL(a):[a e n => ~s(a)=0]

in set theory and natural deduction, from these axioms here:

1. Your "Peano Axioms"
2. New Axiom: ~(-1 e n)
3. New Axiom: s(-1) = 0

Just curious, how would you prove it? Please show
us a formal DC Proof, so that it is a computer
verified proof, and not some halucination.

Thanks in advance.

[Mostowski Collapse]

if you cannot write minus one -1 in DC Proof,
you can also use the constant m, maybe this
is easier for you:

Can you prove the alleged axiom violation:

~ALL(a):[a e n => ~s(a)=0]

in set theory and natural deduction, from these axioms here:

1. Your "Peano Axioms"

2. New Axiom: ~(m e n)
3. New Axiom: s(m) = 0

0 might be the first element in n. But what prevents
m outside of n, being the predecessor of 0. Can
you please tell us, via some proof?

LoL

[Dan Christensen]

On Friday, May 6, 2022 at 10:59:17 AM UTC-4, Mostowski Collapse wrote:
> No denial, I don't need to deny anything, because there

<yawn>

EOD

[Mostowski Collapse]

So you cannot prove the axiom violation:

~ALL(a):[a e n => ~s(a)=0]

Congratulations! Well s=succQ satisfies your
Peano Axioms. There is no proof that s=succQ
doesn't satisfy the Peano Axioms, not from

your side so far, against all your claims.

LMAO!

[Dan Christensen]

On Friday, May 6, 2022 at 11:07:33 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> So you cannot prove the axiom violation:
> ~ALL(a):[a e n => ~s(a)=0]
> Congratulations! Well s=succQ satisfies your
> Peano Axioms.

What I said about the integers also applies for the rational numbers. Yesterday, you wrote "Because succQ(-1/2)=1/2 ..."

So, you also have succQ(-1) = 0, right?

Oooopsie... that would violate Peano's 4th Axiom. Likewise, Peano's 5th Axiom (Induction) is violated. Sorry, but (Q, succQ, 0) simply does NOT satisfy Peano Axioms.

Dan

[Mostowski Collapse]

I have of course succQ(-1)=0. But I have also ~(-1 e N).
Whats your point? Do you still believe this axiom is
violated for s = succQ and n = N?

ALL(a):[a e n => ~s(a)=0]

By which value of a? Or do you believe this axiom is
violated for s = succQ and n = N?

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

By which value of a? Can you please show us the witnesses
of these violations?

Thanks in advance.

[Mostowski Collapse]

The set Q is the set of rational numbers, you might write
down rational numbers as a/b, in as far 2/3 and 4/6

are the same rational numbers. The rational numbers
contain the natural numbers, like 10/2 is the same as 5.

+Q is usually defined in school as, assuming positive denominator:

a/b +Q c/d := (a *Z d +Z c *Z b) / (b *N d)

You can make this more precise because an equivalence
relation is involved. This is only a sketch. You need
operations on Z, the positive and negative numbers,

since the numerator can be negative. Now you can show:

x e N & y e N => x +Q y = x +N y

Another way to express this is to say:

+Q | NxN = +N

[Mostowski Collapse]

Since +Q agrees on NxN with +N. You also have that
succQ agrees on N with succN. Just observe that
succQ can be defined as follows:

succQ(x) := x +Q 1.

Now since we had this lemma:

/* +Q agrees on NxN with +N */

> x e N & y e N => x +Q y = x +N y

We can also prove this lemma:

x e N => succQ(x) = succN(x)

And therefore succQ satisfies all Peano Axioms
because the particular way they are written
in the form ALL(v):[v e N => ...] and because

the induction axiom only talks about subsets

of N. Of course the Peano Axioms are not change
in my claim, they still have n in it, we do not

replace n by Q. This would violate Occams
Razor, since I nowhere said change n. Changing
n as well is an idee fix of Dan Christensen.

I nowhere shared the idea to change n as well.
This violates Occams Razor to also assume n
is changed, since I didn't state change n:

Occam's razor
is the problem-solving principle that "entities should
not be multiplied beyond necessity".
https://en.wikipedia.org/wiki/Occam's_razor

[Emmet Shibanuma]

Dan Christensen wrote:

> On Friday, May 6, 2022 at 11:07:33 AM UTC-4, Mostowski Collapse (aka Jan
> Burse) wrote:
>> So you cannot prove the axiom violation: ~ALL(a):[a e n => ~s(a)=0]
>> Congratulations! Well s=succQ satisfies your Peano Axioms.
>
> What I said about the integers also applies for the rational numbers.
> Yesterday, you wrote "Because succQ(-1/2)=1/2 ..."

Danenko Christeskij puts the foot in his mouth.

nevermind, this american citizen is saying you slavic nazis turned anglo-
saxons overnight, have to prepare for no water, no food, no heat and
probably also for atomic war. Not my fault. Deal with the american.

Germany and Switzerland suddenly urge citizens to become PREPPERS
https://www.bitchute.com/video/SNUZmNoQ7OH5/

Natalia Usmanova Woman From Azovstal
https://www.bitchute.com/video/Y2VYQgQ5G0jr/

A captured militant of the Armed Forces of Ukraine about the crimes of the
Ukrainian command. https://www.bitchute.com/video/69xwcmk3acmf/

[Emmet Shibanuma]

Mostowski Collapse wrote:

> 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]]]
>
> By which value of a? Can you please show us the witnesses of these
> violations? Thanks in advance.
>
> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 07:46:21 UTC+2:

nevermind, you Janeko Burseski, this american citizen is saying you slavic
nazis turned anglo-saxons overnight, have to prepare for no water, no

[Mostowski Collapse]

Is that all you found today in your bitchute cocaine delirium?

Emmet Shibanuma schrieb am Samstag, 7. Mai 2022 um 13:28:30 UTC+2:
> I dont want to live in this world anymore,
> I am an italian comrad and my ass hurts
> from beeing fucked by Putin.
>

[Emmet Shibanuma]

the man is american, you dementia hit brainless idiot. You are going to starve in cold big time. Not my words. Not my fault. You disgusting fake_money nazi Janeko Burseskij.

lol, slavic fake_money nazi switzerland turned anglo-saxon, starving in cold, unable to steal gas and oil on fake_money anymore!!

LIVE UPDATES: US Authorities Should Be Held Accountable for Kiev's Crimes in Ukraine - Duma Speaker
https://sputniknews.com/20220506/live-updates-biden-announces-more-security-aid-to-ukraine-including-artillery-munitions--radar-1095322099.html
"For the crimes committed in Ukraine by the Kyiv Nazi regime, the leadership of the United States should also be held accountable, joining the list of war criminals", the speaker of the Russian State Duma Vyacheslav Volodin said.
He noted that Washington has confessed that the US is coordinating the Ukrainian military, and therefore de-facto participating in the conflict, fighting against Russia.

[Dan Christensen]

On Saturday, May 7, 2022 at 5:23:13 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> I have of course succQ(-1)=0. But I have also ~(-1 e N).

Of course (N, S, 0) satisfies PA, where S is the usual successor function on N. Sadly for you, and contrary to your outrageous claim, (Q, succQ, 0) where succQ(x)=x+1 on Q, does NOT satisfy PA since succQ(-1)=0. When will you learn, Jan Burse?

[Mostowski Collapse]

I did not claim (Q, succQ, 0) satisfies the Peano axioms,
in the sense that N would be replaced by Q.

Thats your idee fix. Sorry I cannot help you.

[Mostowski Collapse]

Maybe see a doctor, it seems you have some reading
disability or some other mental health problem.

[Mitch Yamaguchi]

Mostowski Collapse wrote:

> I did not claim (Q, succQ, 0) satisfies the Peano axioms,
> in the sense that N would be replaced by Q.
>
> Thats your idee fix. Sorry I cannot help you.
>
> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:

You two lovers should go to kievj and kiss the ring of the nazi home
zelenskej, like everybody else. Big governments kissed the ring of
zelenske, why not you??

https://cdni.russiatoday.com/files/2022.05/l/62753b4085f54049e92af89d.jpg

[Dan Christensen]

On Saturday, May 7, 2022 at 2:20:47 PM UTC-4, Mitch Yamaguchi wrote:
> Mostowski Collapse wrote:
>
> > I did not claim (Q, succQ, 0) satisfies the Peano axioms,
> > in the sense that N would be replaced by Q.
> >
> > Thats your idee fix. Sorry I cannot help you.
> >
> > Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:
> You two lovers should go to kievj and kiss the ring of the nazi home
> zelenskej, like everybody else. Big governments kissed the ring of
> zelenske, why not you??
>

You have it backwards, Nazi boy. Remember:

WAR OF AGRESSION = NAZI

If you have free access the internet (somehow I doubt it), check the English-language news from your closest ally, China. It is obvious that, while they do not outright call them "war crimes," there is coverage of Russia atrocities. Today, they report:

"Two months of war in Ukraine have left 7.7 million people internally displaced and driven over 5.5 million people across international borders, including nearly two-thirds of all children in Ukraine. Hundreds of children have been killed and many more have been injured," he pointed out.

"Nearly 200 attacks have been reported against health care facilities, and schools continue to be impacted by strikes."

Makes you real proud, don't it, Nazi boy? Doesn't look like even your best friends are much influenced by your lies.

So, are you ready to be a hero at the front? Something tells me there will be a shortage of bullet-proof vests. Don't expect your spiffy new SS uniform to offer much protection. Save at least one bullet in your pocket, for, well... you know.

[Mostowski Collapse]

This substitution, which is only a way of speaking,
for having a model with s = succZ, works also in
your DC Proof tool. Using dcpsetup9.exe I get:

1 succZ=s
Axiom

2 ALL(a):[a ε n => ~s(a)=0]
Axiom

3 ALL(a):[a ε n => ~succZ(a)=0]
Substitute, 1, 2

Thats just equality in a proof tool, in the case of
DC Proof equality is also available for function symbols.
At least what the usual equality laws concerns, you do not really

need to define axioms for f=g in DC Proof. You only need to
define more axioms when you want more function symbols
to be equal, than the quality that is already available in

DC Proof. But the available equality is sufficient to explain
what the replacement is, there is no automatic replacment of
n=z, if you do not say so. Same for any s=succX, which shows

that your Peano Axioms are an open formulation, since one
can easily verify that all of your Peano Axioms are still satisfied
when succ | N = succN.

[Mostowski Collapse]

In an open formulation this here is not provable:

/* not provable because of use of open formalism */
ALL(a):ALL(b):[s(a)=b => a e n & a e n]

In a closed formulation, it can be made provable.

/* with some grafting of function application */
ALL(a):ALL(b):[s(a)=b => a e n & a e n]

Dan Christensens Peano Axioms lacks the so called
"closed world assumption", CWA:

https://en.wikipedia.org/wiki/Closed-world_assumption

[Mostowski Collapse]

Why is the closed world assumption missing?
Well because he uses:

ALL(a):[a e n => s(a) e n]

And not the more common:

s : n -> n

If he would use the more common s : n -> n, and if
he had a system with some grafting of function

application he could also exclude all dom(succX) =\= n.

[Mitch Yamaguchi]

Dan Christensen wrote:

idiot, it just reveals your incompetency. Engilsh written by a chinese, in
science papers, is absurd.

> "Two months of war in Ukraine have left 7.7 million people internally
> displaced and driven over 5.5 million people across international
> borders, including nearly two-thirds of all children in Ukraine.
> Hundreds of children have been killed and many more have been injured,"
> he pointed out. "Nearly 200 attacks have been reported against health
> care facilities, and schools continue to be impacted by strikes."

all, admittedly, done by the nazi ukraine, you lying nazi pig. You know
what I say is true. It stays everywhere. Your country is a capitalist
shithole. You forgot the link, nazi.

A captured militant of the Armed Forces of Ukraine about the crimes of the

Ukrainian command https://www.bitchute.com/video/69xwcmk3acmf/

[Dan Christensen]

On Saturday, May 7, 2022 at 3:54:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> This substitution, which is only a way of speaking,
> for having a model with s = succZ, works also in
> your DC Proof tool. Using dcpsetup9.exe I get:

Latest is dcpsetup12.exe dated 2022-04-19

>
> 1 succZ=s
> Axiom
>
> 2 ALL(a):[a ε n => ~s(a)=0]
> Axiom
>
> 3 ALL(a):[a ε n => ~succZ(a)=0]
> Substitute, 1, 2
>

Not sure what point you are tying to make. The only requirement of an axiom is that it be syntactically correct. There is no check for logical consistency. You could even have an axiom P & ~P just to see what would happen.

> Thats just equality in a proof tool, in the case of
> DC Proof equality is also available for function symbols.
> At least what the usual equality laws concerns, you do not really
>
> need to define axioms for f=g in DC Proof. You only need to
> define more axioms when you want more function symbols
> to be equal, than the quality that is already available in
>
> DC Proof. But the available equality is sufficient to explain
> what the replacement is, there is no automatic replacment of
> n=z, if you do not say so. Same for any s=succX, which shows
>
> that your Peano Axioms are an open formulation, since one
> can easily verify that all of your Peano Axioms are still satisfied
> when succ | N = succN.

Maybe you don't understand it is means for (x f, x0) to satisfy Peano's Axioms. It means only that we have:

1. Set(x)
Axiom

2. x0 in x
Axiom

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

4. ALL(a):ALL(b): [a in X & b in x => [f(a)=f(b) => a=b]]

5. ALL(a):[a in x => ~f(a)=x0]

6. ALL(a):[Set(a) & ALL(b):[b in a => b in x] => [x0 in a & ALL(b):[b in a => f(b) in a] => a=x]]]


While Jan Burse has finally conceded that my formalization of Peano's Axioms is not incorrect (some progress!), to save face, he now bizarrely maintains (elsewhere) I should be able to derive from it the following nonsensical result:

ALL(a):ALL(b):[s(a)=b => a in n & b in n] (where n = the set of natural numbers, s = the successor function on n).

(Or will you now withdraw this silliness as well?)

I tried to explain to him that he has it backwards, and that the quantifiers should be restricted to the set of natural numbers (e.g. ALL(a):ALL(b):[a in n & b in n => ...), but he persists in his idiocy. Maybe he wants to use the integers instead? Who knows with Jan Burse?

[Dan Christensen]

On Saturday, May 7, 2022 at 4:23:21 PM UTC-4, Mitch Yamaguchi wrote:
> Dan Christensen wrote:
>
> idiot, it just reveals your incompetency. Engilsh written by a chinese, in
> science papers, is absurd.
> > "Two months of war in Ukraine have left 7.7 million people internally
> > displaced and driven over 5.5 million people across international
> > borders, including nearly two-thirds of all children in Ukraine.
> > Hundreds of children have been killed and many more have been injured,"
> > he pointed out. "Nearly 200 attacks have been reported against health
> > care facilities, and schools continue to be impacted by strikes."

> all, admittedly, done by the nazi ukraine, you lying nazi pig.

Wow, you really are a useful idiot! Not even the Chinese are buying into that shit. Maybe they are hoping to buy up Russia after the war. Should go fairly cheaply.

You are now truly alone in the world and will be for several generations, comrade. Not even the Chinese will trust you.

[Mostowski Collapse]

Well the point is that you can classify axiom systems into CWA
and OWA. Depending on how they see for example:

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

Your Peano Axioms tend towards OWA. Since your Peano Axioms
are satisfiable by any function s where s agrees on N with the

successor on the natural numbers.

For CWA / OWA see here:
https://en.wikipedia.org/wiki/Closed-world_assumption

[Mitch Yamaguchi]

Dan Christensen wrote:

>> > he pointed out. "Nearly 200 attacks have been reported against health
>> > care facilities, and schools continue to be impacted by strikes."
>
>> all, admittedly, done by the nazi ukraine, you lying nazi pig.
>
> Wow, you really are a useful idiot! Not even the Chinese are buying into
> that shit. Maybe they are hoping to buy up Russia after the war. Should
> go fairly cheaply.
>
> You are now truly alone in the world and will be for several
> generations, comrade. Not even the Chinese will trust you.

you are lying your ass out. Put the link, I bet you push mainstream
propaganda, confusing a capitalist site with china. China capitalist too,
but you are lying.

Here, if you know "ukrainian" as I do, from the people, you hear "nazis"
and zelenske, the nazi puppet.

a mariopol "ukrainian" horror guilt
https://www.bitchute.com/video/7eh7ZODlMyRW/

you won't call that for a country, would you.

[Mostowski Collapse]

Other names for OWA axioms systems are:
- dark elements tsunami
- extrensic intrinsic confusion
- Russell swirling in his grave
- You are using my ALL(_) wrong
- black matter hell

- blame it on the empty set
- Half-Functions
- extension function spaces

- ad hoc axioms boom boom
- Poop-Mathematics
- Etc...

LMAO!

Mostowski Collapse schrieb:

[Mitch Yamaguchi]

Mostowski Collapse wrote:

> Other names for OWA axioms systems are:
> - dark elements tsunami - extrensic intrinsic confusion - Russell
> swirling in his grave - You are using my ALL(_) wrong - black matter
> hell

that's exactly a blackhole bellow the event horizon. Try again.

[Mostowski Collapse]

OWA axioms systems have their justification
when you study classes of different
mathematical structure.

But I wouldn't know that Peano Structures
form a larger class of different
mathematical structures.

Since there is this theorem, isn't it?
- All Peano Structures are isomorphic?

You can only prove the theorem if you
use s : n -> n, it doesn't work if you
use ALL(a):[a e n => s(a) e n].

Mostowski Collapse schrieb:

[Dan Christensen]

On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> OWA axioms systems have their justification
> when you study classes of different
> mathematical structure.
>
> But I wouldn't know that Peano Structures
> form a larger class of different
> mathematical structures.
>
> Since there is this theorem, isn't it?
> - All Peano Structures are isomorphic?
>

Yes.

If we have Peano systems (n,0,next) and (n',0',next') then there existence a unique function f mapping n to n' such that
1. f(0)=0'
2. f(next(x)) = next'(f(x))
http://dcproof.com/PeanoThm1.htm (723 lines)

The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
http://dcproof.com/PeanoThm2.htm (188 lines)

The bijective mapping from n to n' preserves the successor relations on n and n'
http://dcproof.com/PeanoThm3.htm (167 lines)

[Mostowski Collapse]

Still utter nonsense, you use extrensic parameters.
You only proved:

next | n1 ~ next‘ | n2

Where f | A denotes f restricted to A. You didnt show
next ~ next‘, or do you for example claim

succQ ~ succN

which are both satisfied by your Peano Axioms and
where ~ denotes isomorphism?

LoL

P.S.: For isomorphism you need to have f : dom(next) ->
dom(next‘) and not your nonsense ALL(a):[a e n1 => f(a) e n2].

[Dan Christensen]

On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:

> P.S.: For isomorphism you need to have f : dom(next) ->
> dom(next‘) and not your nonsense ALL(a):[a e n1 => f(a) e n2].
> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 06:17:03 UTC+2:
> > On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> > > OWA axioms systems have their justification
> > > when you study classes of different
> > > mathematical structure.
> > >
> > > But I wouldn't know that Peano Structures
> > > form a larger class of different
> > > mathematical structures.
> > >
> > > Since there is this theorem, isn't it?
> > > - All Peano Structures are isomorphic?
> > >
> > Yes.
> >
> > If we have Peano systems (n,0,next) and (n',0',next') then there existence a unique function f mapping n to n' such that
> > 1. f(0)=0'
> > 2. f(next(x)) = next'(f(x))
> > http://dcproof.com/PeanoThm1.htm (723 lines)
> >
> > The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
> > http://dcproof.com/PeanoThm2.htm (188 lines)
> >
> > The bijective mapping from n to n' preserves the successor relations on n and n'
> > http://dcproof.com/PeanoThm3.htm (167 lines)

> Still utter nonsense, you use extrensic parameters.

This from a crank who believes he can make logical inferences about a function outside of it domain of definition, i.e. where it is undefined -- your DARK ELEMENTS!

> You only proved:
>
> next | n1 ~ next‘ | n2
>

I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.

[Mostowski Collapse]

Not the same next and next', only restricted to n1 and n2.
This has some consequences, for example you cannot prove:

~EXIST(a):[next(a)=0]

[Dan Christensen]

On Sunday, May 8, 2022 at 11:27:05 AM UTC-4, Mostowski Collapse (akawrote:

> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 17:21:24 UTC+2:
> > On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:
> > I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.

> Not the same next and next', only restricted to n1 and n2.

Pay attention, Jan Burse! I am comparing different structures, each including a set, an element of that set and a function with certain properties on that set.

> This has some consequences, for example you cannot prove:
>
> ~EXIST(a):[next(a)=0]

Why would I want to prove such nonsense? Perhaps you are confusing it with one of Peano's Axioms: ALL(a):[a in n => ~s(a)=0] or equivalently ~EXIST(a):[a in n & s(a)=0]. In mathematics, you almost always want to restrict every quantifier. You usually don't want to be talking about every object in the universe.

[Mostowski Collapse]

Try proving:

ALL(a):[~Even(a) => Even(next(a))]

LoL

[Mostowski Collapse]

Wait, I am trying to make a better example with Even.
Ok, this is the better example, which corresponds
to the usual expectation we have about Even(_):

ALL(a):[Even(a) => ~Even(next(a))]

Can you prove it from Your Peano Axioms and
from Your Even Axiom? I guess no. What if
a = -1, one of the Dark Elements,

that could be found in your Even(_) sometimes?

[Dan Christensen]

On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> Wait, I am trying to make a better example with Even.
> Ok, this is the better example, which corresponds
> to the usual expectation we have about Even(_):
>
> ALL(a):[Even(a) => ~Even(next(a))]
>

You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.

[Mostowski Collapse]

Thats not how Euclid formulates it:

7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.

He also uses the definition format with Even(_) in front:

6. An even number is that which is divisible into two equal parts.

Which translates to:

ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]

Even(a): An even number
<=>: is
Number(a): that which [number]
EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts

Very easy....