Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Time is an illusion perpetrated by the manufacturers of space.


tech / sci.math / Re: Formal proofs about functions using DC Proof

SubjectAuthor
* Formal proofs about functions using DC ProofDan Christensen
+* Re: Formal proofs about functions using DC ProofMostowski Collapse
|+* Re: Formal proofs about functions using DC PoopMostowski Collapse
||+* Re: Formal proofs about functions using DC PoopDan Christensen
|||`- Re: Formal proofs about functions using DC PoopEsam Inao
||`* Re: Formal proofs about functions using DC PoopDan Christensen
|| `* Re: Formal proofs about functions using DC PoopJulio Di Egidio
||  `* Re: Formal proofs about functions using DC PoopDan Christensen
||   `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||    +* Re: Formal proofs about functions using DC PoopMostowski Collapse
||    |`* Re: Formal proofs about functions using DC PoopDan Christensen
||    | `* Re: Formal proofs about functions using DC PoopLanny Torii
||    |  `* Re: Formal proofs about functions using DC PoopDan Christensen
||    |   `* Re: Formal proofs about functions using DC PoopLanny Torii
||    |    `* Re: Formal proofs about functions using DC PoopDan Christensen
||    |     `* Re: Formal proofs about functions using DC PoopLanny Torii
||    |      `- Re: Formal proofs about functions using DC PoopDan Christensen
||    +* Re: Formal proofs about functions using DC PoopEsam Inao
||    |`* Re: Formal proofs about functions using DC PoopMostowski Collapse
||    | `- Re: Formal proofs about functions using DC PoopMostowski Collapse
||    `* Re: Formal proofs about functions using DC PoopDan Christensen
||     `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||      `* Re: Formal proofs about functions using DC PoopDan Christensen
||       `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||        +* Re: Formal proofs about functions using DC PoopMostowski Collapse
||        |`- Re: Formal proofs about functions using DC PoopDan Christensen
||        `* Re: Formal proofs about functions using DC PoopDan Christensen
||         `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||          +* Re: Formal proofs about functions using DC PoopDan Christensen
||          |`- Re: Formal proofs about functions using DC PoopLanny Torii
||          `* Re: Formal proofs about functions using DC PoopDan Christensen
||           `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||            +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||            `* Re: Formal proofs about functions using DC PoopDan Christensen
||             `* Re: Formal proofs about functions using DC PoopMostowski Collapse
||              `* Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +* Re: Formal proofs about functions using DC PoopGrant Shirasu
||               |`- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +* Re: Formal proofs about functions using DC PoopMostowski Collapse
||               |`* Re: Formal proofs about functions using DC PoopGrant Shirasu
||               | `- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +* Re: Formal proofs about functions using DC PoopDan Christensen
||               |`- Re: Formal proofs about functions using DC PoopWesi Matsuya
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +- Re: Formal proofs about functions using DC PoopDan Christensen
||               +- Re: Formal proofs about functions using DC PoopMostowski Collapse
||               +* Re: Formal proofs about functions using DC PoopDan Christensen
||               |`- Re: Formal proofs about functions using DC PoopEmmet Shibanuma
||               +* Dan Christensen is Bat Shit CrazyMostowski Collapse
||               |`* Re: Dan Christensen is Bat Shit CrazyEmmet Shibanuma
||               | `* Re: Dan Christensen is Bat Shit CrazyMostowski Collapse
||               |  `- Re: Dan Christensen is Bat Shit CrazyEmmet Shibanuma
||               +- Re: Dan Christensen is Bat Shit CrazyMostowski Collapse
||               +- Re: Dan Christensen is Bat Shit CrazyMostowski Collapse
||               +- Poor, pathetic Jan Burse...Dan Christensen
||               +* Re: Poor, pathetic Jan Burse...Mostowski Collapse
||               |`* Re: Poor, pathetic Jan Burse...Mitch Yamaguchi
||               | +* Re: Poor, pathetic Jan Burse...Dan Christensen
||               | |`* Re: Poor, pathetic Jan Burse...Mitch Yamaguchi
||               | | `* Re: Poor, pathetic Jan Burse...Dan Christensen
||               | |  `- Re: Poor, pathetic Jan Burse...Mitch Yamaguchi
||               | +- Re: Poor, pathetic Jan Burse...Mostowski Collapse
||               | +- Re: Poor, pathetic Jan Burse...Mostowski Collapse
||               | `- Re: Poor, pathetic Jan Burse...Mostowski Collapse
||               `- Dan Christensen is Bat Shit CrazyMostowski Collapse
|`* Re: Formal proofs about functions using DC ProofMathin3D
| `- Re: Formal proofs about functions using DC ProofMostowski Collapse
+* Re: Formal proofs about functions using DC ProofMostowski Collapse
|`* Re: Formal proofs about functions using DC ProofMostowski Collapse
| +- Re: Formal proofs about functions using DC ProofMitch Yamaguchi
| `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|  +- Re: Formal proofs about functions using DC ProofDan Christensen
|  `* Re: Formal proofs about functions using DC ProofDan Christensen
|   `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|    `* Re: Formal proofs about functions using DC ProofDan Christensen
|     `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|      `* Re: Formal proofs about functions using DC ProofDan Christensen
|       `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|        `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|         `* Re: Formal proofs about functions using DC ProofDan Christensen
|          `* Re: Formal proofs about functions using DC ProofMostowski Collapse
|           +* Re: Formal proofs about functions using DC ProofMostowski Collapse
|           |`* Re: Formal proofs about functions using DC ProofMostowski Collapse
|           `* Re: Formal proofs about functions using DC ProofLupe Kaza
+* Re: Formal proofs about functions using DC ProofMostowski Collapse
+- Re: Formal proofs about functions using DC ProofMild Shock
`* Re: Formal proofs about functions using DC ProofArchimedes Plutonium

Pages:1234567
Re: Formal proofs about functions using DC Proof

<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99727&group=sci.math#99727

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:16c2:b0:69f:ca37:f6b5 with SMTP id a2-20020a05620a16c200b0069fca37f6b5mr21064598qkn.48.1652300135038;
Wed, 11 May 2022 13:15:35 -0700 (PDT)
X-Received: by 2002:a25:accf:0:b0:648:6d34:276b with SMTP id
x15-20020a25accf000000b006486d34276bmr24485704ybd.339.1652300134661; Wed, 11
May 2022 13:15:34 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 11 May 2022 13:15:34 -0700 (PDT)
In-Reply-To: <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Wed, 11 May 2022 20:15:35 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 8077
 by: Mostowski Collapse - Wed, 11 May 2022 20:15 UTC

On the other hand the standard definitions passes all
tests. When we use:

ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]

Everything works fine.

Via https://www.umsu.de/trees:

(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(¬Na → ¬Ea) is valid.
(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(¬Na → ¬Oa) is valid.
(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(Na ↔ (Ea ∨ Oa)) is valid.

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 22:11:46 UTC+2:
> ALL(a):[a e {} <=> [Even(a) & Odd(a)]] is provable with
> your definition, but the others are not:
>
> Counter Models to Dans Definition:
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> Via https://www.umsu.de/trees:
>
> Counter Model 1: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
> (∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧
> (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.
> Domain: { 0, 1, 2}
> N: { 0,1 }
> E: { 0,2 }
> O: { 1 }
> D: { 0 }
>
> Counter Model 2: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
> (∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Oa) is invalid.
> Countermodel:
> Domain: { 0, 1, 2 }
> N: { 0,1 }
> E: { 0 }
> O: { 1,2 }
> D: { 0 }
>
> Counter Model 3: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
> (∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(Na ↔ (Oa ∨ Ea)) is invalid.
> Domain: { 0, 1, 2 }
> N: { 0,1 }
> E: { 0,2 }
> O: { 1 }
> D: { 0 }
> Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 20:55:29 UTC+2:
> > Corr.: Typo
> > EvenN = { a e n | a = 0 mod 2 }
> > OddN = { a e n | a = 1 mod 2 }
> > EvenZ = { a e z | a = 0 mod 2 }
> > OddZ = { a e z | a = 1 mod 2 }
> > This is in case you have an application where you
> > also want to have a notion of odd/even integer.
> > Or some other EvenX/OddX. But to have a well
> >
> > defined definition you need to be specific.
> >
> > https://en.m.wikipedia.org/wiki/Well-defined
> > Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 20:53:31 UTC+2:
> > > With the standard definition you can prove
> > > everything, that you cannot prove with your Dan
> > > Christensen nonsense. Examples that become provable
> > >
> > > not using the Dan Christensen nonsense:
> > >
> > > ALL(a):[~a in n => ~Even(a)]
> > > ALL(a):[~a in n => ~Odd(a)]
> > > ALL(a):[a e n <=> [Even(a) v Odd(a)]]
> > > ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
> > > Etc…
> > >
> > > On the other hand with Dan Christensen syphilitic brain
> > > definition one cannot prove these things, one is bugged with
> > > dark elements. If you want you can be also
> > >
> > > more specific and distinguish:
> > >
> > > EvenN = { a e n | a = 0 mod 2 }
> > > OddN = { a e n | a = 1 mod 2 }
> > > EvenZ = { a e n | a = 0 mod 2 }
> > > OddZ = { a e n | a = 1 mod 2 }
> > >
> > > This is in case you have an application where you
> > > also want to have a notion of odd/even integer.
> > > Or some other EvenX/OddX. But to have a well
> > >
> > > defined definition you need to be specific.
> > >
> > > https://en.m.wikipedia.org/wiki/Well-defined
> > > Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 20:47:36 UTC+2:
> > > > On Wednesday, May 11, 2022 at 12:07:22 PM UTC-4, Mostowski Collapse wrote:
> > > > > I am not advocating lumping. I try to understand what
> > > > > Dan Christensen means by evenness and why he
> > > > > oposes to these two definitions for even and
> > > > >
> > > > > odd natural numbers:
> > > > > Even = { a e n | a = 0 mod 2 }
> > > > > Odd = { a e n | a = 1 mod 2 }
> > > > Liar. Not my idea, and never wrote that, but at least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown.. Don't you feel silly now?
> > > >
> > > > As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:
> > > >
> > > > 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > > > 2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> > > >
> > > > Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).
> > > >
> > > > I hope this helps.
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Formal proofs about functions using DC Proof

<f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99749&group=sci.math#99749

 copy link   Newsgroups: sci.math
X-Received: by 2002:ad4:5f89:0:b0:45a:f6d9:41c1 with SMTP id jp9-20020ad45f89000000b0045af6d941c1mr20808644qvb.50.1652315450998;
Wed, 11 May 2022 17:30:50 -0700 (PDT)
X-Received: by 2002:a25:8207:0:b0:64a:475:83b3 with SMTP id
q7-20020a258207000000b0064a047583b3mr26061337ybk.628.1652315450750; Wed, 11
May 2022 17:30:50 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 11 May 2022 17:30:50 -0700 (PDT)
In-Reply-To: <d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Thu, 12 May 2022 00:30:50 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 3541
 by: Dan Christensen - Thu, 12 May 2022 00:30 UTC

On Wednesday, May 11, 2022 at 4:15:42 PM UTC-4, Mostowski Collapse wrote:
> On the other hand the standard definitions passes all
> tests. When we use:
>

Nothing "standard" about it, Jan Burse.

> ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]
>
> Everything works fine.
>

Well, there is the small matter of everything that isn't a number being odd. And even. Other than that...

All this silliness can be avoided by defining the predicates Even and Odd, as it is usually done, by restricting our attention to ONLY the natural numbers and forgetting about Jan Burse's "dark elements" all together.

1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
2. ALL(a):[Odd(a) <=> ~EVEN(a)]

If that's too complicated, perhaps you should try constructing subsets of N, Jan Burse. Subsets seem to be a bit more fool-proof. Or should I say, more Jan-Burse-proof, with less leeway to make silly mistakes.

Dan

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

Re: Formal proofs about functions using DC Proof

<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99751&group=sci.math#99751

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:1a9c:b0:2f3:d873:4acc with SMTP id s28-20020a05622a1a9c00b002f3d8734accmr17339171qtc.424.1652316519894;
Wed, 11 May 2022 17:48:39 -0700 (PDT)
X-Received: by 2002:a25:5546:0:b0:64a:a5c5:7c34 with SMTP id
j67-20020a255546000000b0064aa5c57c34mr21963532ybb.154.1652316519655; Wed, 11
May 2022 17:48:39 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 11 May 2022 17:48:39 -0700 (PDT)
In-Reply-To: <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 00:48:39 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 4326
 by: Mostowski Collapse - Thu, 12 May 2022 00:48 UTC

You are subject to your own clown circus, trapped
in an infine loop of dense stupidity:

Dan Christensen schrieb am Montag, 9. Mai 2022 um 06:11:47 UTC+2:
> CASE 1
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> CASE 2
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/1WIQ11zEAQAJ

Maybe if you had written instead, you would get
out of your loop, I cannot help you otherwise:

CASE 1
ALL(a):[a in n => [Evenness(a) <=> EXIST(b):[b in n & a=2*b]]]
CASE 2
ALL(a):[Evennumber(a) <=> a in n & EXIST(b):[b in n & a=2*b]

LMAO!

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 02:30:55 UTC+2:
> On Wednesday, May 11, 2022 at 4:15:42 PM UTC-4, Mostowski Collapse wrote:
> > On the other hand the standard definitions passes all
> > tests. When we use:
> >
> Nothing "standard" about it, Jan Burse.
> > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]
> >
> > Everything works fine.
> >
> Well, there is the small matter of everything that isn't a number being odd. And even. Other than that...
>
> All this silliness can be avoided by defining the predicates Even and Odd, as it is usually done, by restricting our attention to ONLY the natural numbers and forgetting about Jan Burse's "dark elements" all together.
> 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> 2. ALL(a):[Odd(a) <=> ~EVEN(a)]
>
> If that's too complicated, perhaps you should try constructing subsets of N, Jan Burse. Subsets seem to be a bit more fool-proof. Or should I say, more Jan-Burse-proof, with less leeway to make silly mistakes.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen is Bat Shit Crazy

<66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99753&group=sci.math#99753

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:10a8:b0:69f:8b8b:36d9 with SMTP id h8-20020a05620a10a800b0069f8b8b36d9mr21614729qkk.93.1652317295417;
Wed, 11 May 2022 18:01:35 -0700 (PDT)
X-Received: by 2002:a25:d64c:0:b0:649:e6e6:8a84 with SMTP id
n73-20020a25d64c000000b00649e6e68a84mr27174667ybg.212.1652317295186; Wed, 11
May 2022 18:01:35 -0700 (PDT)
Path: i2pn2.org!rocksolid2!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 11 May 2022 18:01:34 -0700 (PDT)
In-Reply-To: <75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
Subject: Dan Christensen is Bat Shit Crazy
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 01:01:35 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 4895
 by: Mostowski Collapse - Thu, 12 May 2022 01:01 UTC

Now I am waiting that the clown zampano which goes
by the name Dan Christensen calls this wonky:

ALL(a):[~a e n => ~Evennumber(a)]
ALL(a):[~a e n => ~Oddnumber(a)]

He earned already a ticket for the lunatic asylum by his infinite
looping. If he calls the above wonky, he will earn something more.

No more ticket out of the lunatic asylum.

Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 02:48:44 UTC+2:
> You are subject to your own clown circus, trapped
> in an infine loop of dense stupidity:
>
> Dan Christensen schrieb am Montag, 9. Mai 2022 um 06:11:47 UTC+2:
> > CASE 1
> > ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> > CASE 2
> > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
> https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/1WIQ11zEAQAJ
>
> Maybe if you had written instead, you would get
> out of your loop, I cannot help you otherwise:
>
> CASE 1
> ALL(a):[a in n => [Evenness(a) <=> EXIST(b):[b in n & a=2*b]]]
> CASE 2
> ALL(a):[Evennumber(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>
> LMAO!
> Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 02:30:55 UTC+2:
> > On Wednesday, May 11, 2022 at 4:15:42 PM UTC-4, Mostowski Collapse wrote:
> > > On the other hand the standard definitions passes all
> > > tests. When we use:
> > >
> > Nothing "standard" about it, Jan Burse.
> > > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > > ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]
> > >
> > > Everything works fine.
> > >
> > Well, there is the small matter of everything that isn't a number being odd. And even. Other than that...
> >
> > All this silliness can be avoided by defining the predicates Even and Odd, as it is usually done, by restricting our attention to ONLY the natural numbers and forgetting about Jan Burse's "dark elements" all together.
> > 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > 2. ALL(a):[Odd(a) <=> ~EVEN(a)]
> >
> > If that's too complicated, perhaps you should try constructing subsets of N, Jan Burse. Subsets seem to be a bit more fool-proof. Or should I say, more Jan-Burse-proof, with less leeway to make silly mistakes.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Dan Christensen is Bat Shit Crazy

<ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99799&group=sci.math#99799

 copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:5ad4:0:b0:2f3:e0fb:df1c with SMTP id d20-20020ac85ad4000000b002f3e0fbdf1cmr13847090qtd.267.1652349696891;
Thu, 12 May 2022 03:01:36 -0700 (PDT)
X-Received: by 2002:a25:8f90:0:b0:648:84d1:1431 with SMTP id
u16-20020a258f90000000b0064884d11431mr25275226ybl.483.1652349696701; Thu, 12
May 2022 03:01:36 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 03:01:36 -0700 (PDT)
In-Reply-To: <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com> <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com>
Subject: Re: Dan Christensen is Bat Shit Crazy
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 10:01:36 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 6062
 by: Mostowski Collapse - Thu, 12 May 2022 10:01 UTC

Well for Euclids predicates Evennumber this is provable:
|- ALL(a):[~a e n => ~Evennumber(a)]

On the other hand for Dan Christensens Evenness you cannot prove it,
|/- ALL(a):[~a e n => ~Evenness(a)]

there is an obstancle in the way,
the Dan Christensens definitions are not well defined:

"In mathematics, a well-defined expression or unambiguous expression
is an expression whose definition assigns it a unique interpretation or value."
https://en.wikipedia.org/wiki/Well-defined_expression

If you do the following for Dan Christensens definitions, make it twice:

ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]

For Dan Christensens one cannot prove:
|/- ALL(a):[Evenness1(a) <=> Evenness2(a)]

On the other hand for Euclids one can prove:
|- ALL(a):[Evennumber1(a) <=> Evennumber2(a)]

See the difference dumbo?

Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 03:01:40 UTC+2:
> Now I am waiting that the clown zampano which goes
> by the name Dan Christensen calls this wonky:
>
> ALL(a):[~a e n => ~Evennumber(a)]
> ALL(a):[~a e n => ~Oddnumber(a)]
>
> He earned already a ticket for the lunatic asylum by his infinite
> looping. If he calls the above wonky, he will earn something more.
>
> No more ticket out of the lunatic asylum.
> Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 02:48:44 UTC+2:
> > You are subject to your own clown circus, trapped
> > in an infine loop of dense stupidity:
> >
> > Dan Christensen schrieb am Montag, 9. Mai 2022 um 06:11:47 UTC+2:
> > > CASE 1
> > > ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> > > CASE 2
> > > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
> > https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/1WIQ11zEAQAJ
> >
> > Maybe if you had written instead, you would get
> > out of your loop, I cannot help you otherwise:
> >
> > CASE 1
> > ALL(a):[a in n => [Evenness(a) <=> EXIST(b):[b in n & a=2*b]]]
> > CASE 2
> > ALL(a):[Evennumber(a) <=> a in n & EXIST(b):[b in n & a=2*b]
> >
> > LMAO!
> > Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 02:30:55 UTC+2:
> > > On Wednesday, May 11, 2022 at 4:15:42 PM UTC-4, Mostowski Collapse wrote:
> > > > On the other hand the standard definitions passes all
> > > > tests. When we use:
> > > >
> > > Nothing "standard" about it, Jan Burse.
> > > > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > > > ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]
> > > >
> > > > Everything works fine.
> > > >
> > > Well, there is the small matter of everything that isn't a number being odd. And even. Other than that...
> > >
> > > All this silliness can be avoided by defining the predicates Even and Odd, as it is usually done, by restricting our attention to ONLY the natural numbers and forgetting about Jan Burse's "dark elements" all together.
> > > 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > > 2. ALL(a):[Odd(a) <=> ~EVEN(a)]
> > >
> > > If that's too complicated, perhaps you should try constructing subsets of N, Jan Burse. Subsets seem to be a bit more fool-proof. Or should I say, more Jan-Burse-proof, with less leeway to make silly mistakes.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Jan Burse is Bat Shit Crazy

<14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99812&group=sci.math#99812

 copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:58d6:0:b0:2f3:d35c:4ef8 with SMTP id u22-20020ac858d6000000b002f3d35c4ef8mr21883885qta.265.1652361244729;
Thu, 12 May 2022 06:14:04 -0700 (PDT)
X-Received: by 2002:a25:c548:0:b0:649:73e4:185d with SMTP id
v69-20020a25c548000000b0064973e4185dmr27333233ybe.545.1652361244567; Thu, 12
May 2022 06:14:04 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 06:14:04 -0700 (PDT)
In-Reply-To: <ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com> <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
<ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>
Subject: Re: Jan Burse is Bat Shit Crazy
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Thu, 12 May 2022 13:14:04 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 3228
 by: Dan Christensen - Thu, 12 May 2022 13:14 UTC

On Thursday, May 12, 2022 at 6:01:42 AM UTC-4, Mostowski Collapse wrote:
> Well for Euclids predicates Evennumber this is provable:
> |- ALL(a):[~a e n => ~Evennumber(a)]
>

Jan Burse's new little buddy and fellow troll JG (a match made in heaven!) really seems to be getting to him, what with the sense utter desperation, even the silly references to Euclid!

To salvage what's left of his pet theory, poor Jan Burse here insists that evenness be determined not only for the natural numbers, but also for every object in the universe (his DARK ELEMENTS). Really quite pathetic.

Dan

Re: Jan Burse is Bat Shit Crazy

<ed501094-7f59-46eb-b0e7-5c4f0b5f4d8cn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99815&group=sci.math#99815

 copy link   Newsgroups: sci.math
X-Received: by 2002:ad4:5bec:0:b0:45a:a030:cdc7 with SMTP id k12-20020ad45bec000000b0045aa030cdc7mr26801094qvc.93.1652361892066;
Thu, 12 May 2022 06:24:52 -0700 (PDT)
X-Received: by 2002:a25:cdc7:0:b0:648:f57d:c0ed with SMTP id
d190-20020a25cdc7000000b00648f57dc0edmr27860575ybf.480.1652361891839; Thu, 12
May 2022 06:24:51 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 06:24:51 -0700 (PDT)
In-Reply-To: <14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com> <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
<ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com> <14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <ed501094-7f59-46eb-b0e7-5c4f0b5f4d8cn@googlegroups.com>
Subject: Re: Jan Burse is Bat Shit Crazy
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 13:24:52 +0000
Content-Type: text/plain; charset="UTF-8"
 by: Mostowski Collapse - Thu, 12 May 2022 13:24 UTC

Because Euclid is the ancestor of nowadays mathematics.
And he defines Evennumber, whereas you have only an
axiom about Evenness which is not a definition.

With Euclids definition we can of course prove:

|- ALL(a):[~a e n => ~Evennumber(a)]

Or in natural language:

"Everything that is not a natural number is also not an even natural number"

Which is the same as saying:

"Everything that is not a car is not also not an electro car"

Pretty simple, but too much for dumbo?

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 15:14:10 UTC+2:
> On Thursday, May 12, 2022 at 6:01:42 AM UTC-4, Mostowski Collapse wrote:
> > Well for Euclids predicates Evennumber this is provable:
> > |- ALL(a):[~a e n => ~Evennumber(a)]
> >
> Jan Burse's new little buddy and fellow troll JG (a match made in heaven!) really seems to be getting to him, what with the sense utter desperation, even the silly references to Euclid!
>
> To salvage what's left of his pet theory, poor Jan Burse here insists that evenness be determined not only for the natural numbers, but also for every object in the universe (his DARK ELEMENTS). Really quite pathetic.
>
> Dan

Re: Jan Burse is Bat Shit Crazy

<17b40871-5115-4d95-bf66-18c5678c8e40n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99820&group=sci.math#99820

 copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:5fd4:0:b0:2f3:f0d7:757a with SMTP id k20-20020ac85fd4000000b002f3f0d7757amr7008404qta.557.1652362212489;
Thu, 12 May 2022 06:30:12 -0700 (PDT)
X-Received: by 2002:a0d:d58c:0:b0:2f7:d506:ba8d with SMTP id
x134-20020a0dd58c000000b002f7d506ba8dmr19085ywd.422.1652362212249; Thu, 12
May 2022 06:30:12 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 06:30:12 -0700 (PDT)
In-Reply-To: <ed501094-7f59-46eb-b0e7-5c4f0b5f4d8cn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com> <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
<ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com> <14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>
<ed501094-7f59-46eb-b0e7-5c4f0b5f4d8cn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <17b40871-5115-4d95-bf66-18c5678c8e40n@googlegroups.com>
Subject: Re: Jan Burse is Bat Shit Crazy
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 13:30:12 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 4389
 by: Mostowski Collapse - Thu, 12 May 2022 13:30 UTC

Its quite straight to derive from Euclid:

ALL(a):[Evennumber(a) <=> a e n & EXIST(b):[b e n & a=b+b]]

This here:

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

And then its a matter of contraposition:

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

Nevertheless Dan Christensen, high as a kite and bat shit crazy,
claims the result is wonky.

LMAO!

Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 15:24:57 UTC+2:
> Because Euclid is the ancestor of nowadays mathematics.
> And he defines Evennumber, whereas you have only an
> axiom about Evenness which is not a definition.
>
> With Euclids definition we can of course prove:
> |- ALL(a):[~a e n => ~Evennumber(a)]
> Or in natural language:
>
> "Everything that is not a natural number is also not an even natural number"
>
> Which is the same as saying:
>
> "Everything that is not a car is not also not an electro car"
>
> Pretty simple, but too much for dumbo?
> Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 15:14:10 UTC+2:
> > On Thursday, May 12, 2022 at 6:01:42 AM UTC-4, Mostowski Collapse wrote:
> > > Well for Euclids predicates Evennumber this is provable:
> > > |- ALL(a):[~a e n => ~Evennumber(a)]
> > >
> > Jan Burse's new little buddy and fellow troll JG (a match made in heaven!) really seems to be getting to him, what with the sense utter desperation, even the silly references to Euclid!
> >
> > To salvage what's left of his pet theory, poor Jan Burse here insists that evenness be determined not only for the natural numbers, but also for every object in the universe (his DARK ELEMENTS). Really quite pathetic.
> >
> > Dan

Re: Jan Burse is Bat Shit Crazy

<ea8aa0aa-0f38-4c48-9bcd-bf5dd40c89dan@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99822&group=sci.math#99822

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:6214:621:b0:432:5e0d:cb64 with SMTP id a1-20020a056214062100b004325e0dcb64mr26747672qvx.65.1652362461058;
Thu, 12 May 2022 06:34:21 -0700 (PDT)
X-Received: by 2002:a05:6902:389:b0:633:31c1:d0f7 with SMTP id
f9-20020a056902038900b0063331c1d0f7mr27264597ybs.543.1652362460806; Thu, 12
May 2022 06:34:20 -0700 (PDT)
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!2.eu.feeder.erje.net!feeder.erje.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 06:34:20 -0700 (PDT)
In-Reply-To: <17b40871-5115-4d95-bf66-18c5678c8e40n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t56ne3$70oi$1@solani.org> <t56nob$70vp$1@solani.org> <t56o95$713a$3@solani.org>
<c1f711b3-3c93-4ee6-8cdb-32e90e97c416n@googlegroups.com> <ab3b0c11-c3ea-4276-ae96-2ca009e628ccn@googlegroups.com>
<2f35b2cf-7351-40e6-8e96-95dc0bd52b53n@googlegroups.com> <6940eaaf-e903-4ca8-af76-b75d1028e492n@googlegroups.com>
<7776fd13-06a9-4361-8f72-797ff9ed0dcdn@googlegroups.com> <e74d0fd9-a39b-4ac2-9650-21b520d2e4bdn@googlegroups.com>
<e74a4ed5-7da3-4c08-9842-b54adfd0d725n@googlegroups.com> <edb91900-0e56-4592-b479-8d141fe262fcn@googlegroups.com>
<90aa7914-c3b2-4b39-985a-6db05580ac4bn@googlegroups.com> <pan$83cee$e6673bc8$a5be40ee$79467c67@pvgxcvuw.gb>
<607fbf2b-46cb-4b02-a1f2-49127e82804an@googlegroups.com> <t59hj3$8as$1@dont-email.me>
<d47af19c-b6b2-440c-99fa-377e666e1f04n@googlegroups.com> <837fbcbf-1315-4825-9575-11f66e3c1edfn@googlegroups.com>
<f8245090-a7c6-49b8-8775-8634ceb55ae0n@googlegroups.com> <674612b2-7efe-4736-844f-f9d038d042den@googlegroups.com>
<c0c9a9a7-68b7-479c-b173-5a5c3aefacb8n@googlegroups.com> <788352d7-b82b-462a-a36d-b4465f3291e3n@googlegroups.com>
<113b1f2a-44ae-4916-b153-3235b8d6babdn@googlegroups.com> <30443f00-2a51-4d9d-a915-5f7ab1318421n@googlegroups.com>
<d955f6a7-0aff-4d08-bee9-31d1e45af28fn@googlegroups.com> <f0022a5d-b596-4fae-b6c9-b932b85d81fan@googlegroups.com>
<75a512ce-1e29-441c-ac60-56e1471e24b1n@googlegroups.com> <66452043-b35d-47f9-b169-e984d2ceda11n@googlegroups.com>
<ca7af71e-fb1e-4106-8e24-0bb0910e6c9bn@googlegroups.com> <14f9df49-ca20-4d1a-9f77-374f085c9525n@googlegroups.com>
<ed501094-7f59-46eb-b0e7-5c4f0b5f4d8cn@googlegroups.com> <17b40871-5115-4d95-bf66-18c5678c8e40n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <ea8aa0aa-0f38-4c48-9bcd-bf5dd40c89dan@googlegroups.com>
Subject: Re: Jan Burse is Bat Shit Crazy
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 13:34:21 +0000
Content-Type: text/plain; charset="UTF-8"
 by: Mostowski Collapse - Thu, 12 May 2022 13:34 UTC

If it is not determined, it is not well defined.
BTW: Some Sigmund Freud found this definition:

ALL(a):[Wonky(a) <=> ~Danish(a)]

This means that practically all of mathematics
is wonky, because Dan Christensen doesn't

have the slightest clue..

Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 15:30:18 UTC+2:
> Its quite straight to derive from Euclid:
>
> ALL(a):[Evennumber(a) <=> a e n & EXIST(b):[b e n & a=b+b]]
>
> This here:
>
> ALL(a):[Evennumber(a) => a e n]
>
> And then its a matter of contraposition:
> ALL(a):[~a e n => ~Evennumber(a)]
> Nevertheless Dan Christensen, high as a kite and bat shit crazy,
> claims the result is wonky.
>
> LMAO!
> Mostowski Collapse schrieb am Donnerstag, 12. Mai 2022 um 15:24:57 UTC+2:
> > Because Euclid is the ancestor of nowadays mathematics.
> > And he defines Evennumber, whereas you have only an
> > axiom about Evenness which is not a definition.
> >
> > With Euclids definition we can of course prove:
> > |- ALL(a):[~a e n => ~Evennumber(a)]
> > Or in natural language:
> >
> > "Everything that is not a natural number is also not an even natural number"
> >
> > Which is the same as saying:
> >
> > "Everything that is not a car is not also not an electro car"
> >
> > Pretty simple, but too much for dumbo?
> > Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 15:14:10 UTC+2:
> > > On Thursday, May 12, 2022 at 6:01:42 AM UTC-4, Mostowski Collapse wrote:
> > > > Well for Euclids predicates Evennumber this is provable:
> > > > |- ALL(a):[~a e n => ~Evennumber(a)]
> > > >
> > > Jan Burse's new little buddy and fellow troll JG (a match made in heaven!) really seems to be getting to him, what with the sense utter desperation, even the silly references to Euclid!
> > >
> > > To salvage what's left of his pet theory, poor Jan Burse here insists that evenness be determined not only for the natural numbers, but also for every object in the universe (his DARK ELEMENTS). Really quite pathetic.
> > >
> > > Dan

Re: Formal proofs about functions using DC Proof

<t5j30s$euv8$3@solani.org>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99825&group=sci.math#99825

 copy link   Newsgroups: sci.math
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: janbu...@fastmail.fm (Mostowski Collapse)
Newsgroups: sci.math
Subject: Re: Formal proofs about functions using DC Proof
Date: Thu, 12 May 2022 15:45:01 +0200
Message-ID: <t5j30s$euv8$3@solani.org>
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 12 May 2022 13:45:00 -0000 (UTC)
Injection-Info: solani.org;
logging-data="490472"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:68.0) Gecko/20100101
Firefox/68.0 SeaMonkey/2.53.12
Cancel-Lock: sha1:bnBFAdEvq3XeBDHK5NMZv9GR/Q4=
X-User-ID: eJwNyEcBwDAMBDBKOccTjlf4Q2j1lFyFtrGKsjx54YE8Sopc4ahBbXRfKmyuJbE4MFxzmiydbLzSDuVffPEBTyQVdg==
In-Reply-To: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
 by: Mostowski Collapse - Thu, 12 May 2022 13:45 UTC

If you cannot prove:

/* Doesn't work for Dan Christensens Case 1 */
ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]
=> ALL(a):[Evenness1(a) <=> Evenness2(a)]

Then Evenness is not self synonymous. And therefore
it is not well defined. And therefore its not a definition.

This means it has a lot of dark elements. Basically it
means, you have extended your practice of poop mathematics to:
- Half-Predicates
- Black Hole Properties
- Non-Definition Definitions
- Ask the Chrystal Ball Axioms
- More Ad-Hoc Axioms Boom Boom
- I am gonna ignore Euclid mathematics
- Wonky is the new Black
-

Re: Formal proofs about functions using DC Proof

<25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99826&group=sci.math#99826

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:1007:b0:2f3:ce52:25cb with SMTP id d7-20020a05622a100700b002f3ce5225cbmr23700107qte.575.1652364341401;
Thu, 12 May 2022 07:05:41 -0700 (PDT)
X-Received: by 2002:a25:dcb:0:b0:648:df89:a5b3 with SMTP id
194-20020a250dcb000000b00648df89a5b3mr28371745ybn.485.1652364341096; Thu, 12
May 2022 07:05:41 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 07:05:40 -0700 (PDT)
In-Reply-To: <t5j30s$euv8$3@solani.org>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com> <t5j30s$euv8$3@solani.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Thu, 12 May 2022 14:05:41 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 1993
 by: Dan Christensen - Thu, 12 May 2022 14:05 UTC

On Thursday, May 12, 2022 at 9:45:11 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> If you cannot prove:
>
> /* Doesn't work for Dan Christensens Case 1 */
> ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
> ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]
> => ALL(a):[Evenness1(a) <=> Evenness2(a)]
>
> Then Evenness is not self synonymous.

Given:

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

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

Since evenness is only determined for the natural numbers, it would suffice to prove:

ALL(a):[a in N => [Even'(a) <=> Even(a)]]

A trivial proof in DC Proof. Deal with it, 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

Re: Formal proofs about functions using DC Proof

<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99835&group=sci.math#99835

 copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:5f83:0:b0:2f3:dc9e:bb43 with SMTP id j3-20020ac85f83000000b002f3dc9ebb43mr215957qta.171.1652368602180;
Thu, 12 May 2022 08:16:42 -0700 (PDT)
X-Received: by 2002:a25:4244:0:b0:64b:3af3:45a9 with SMTP id
p65-20020a254244000000b0064b3af345a9mr306497yba.536.1652368601725; Thu, 12
May 2022 08:16:41 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 08:16:41 -0700 (PDT)
In-Reply-To: <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 15:16:42 +0000
Content-Type: text/plain; charset="UTF-8"
 by: Mostowski Collapse - Thu, 12 May 2022 15:16 UTC

You didn't prove:

ALL(a):[Even'(a) <=> Even(a)]

Anyway, you are allowed to do whatever you want.
Only your nonsense is not a definition, only an axiom.

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 16:05:49 UTC+2:
> On Thursday, May 12, 2022 at 9:45:11 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > If you cannot prove:
> >
> > /* Doesn't work for Dan Christensens Case 1 */
> > ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
> > ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]
> > => ALL(a):[Evenness1(a) <=> Evenness2(a)]
> >
> > Then Evenness is not self synonymous.
> Given:
>
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
>
> ALL(a):[a in N => [Even'(a) <=> EXIST(b):[b in N & a=2*b]]]
>
> Since evenness is only determined for the natural numbers, it would suffice to prove:
>
> ALL(a):[a in N => [Even'(a) <=> Even(a)]]
>
> A trivial proof in DC Proof. Deal with it, 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

Re: Formal proofs about functions using DC Proof

<b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99844&group=sci.math#99844

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:4054:b0:6a0:6f88:9cd9 with SMTP id i20-20020a05620a405400b006a06f889cd9mr357592qko.747.1652370813037;
Thu, 12 May 2022 08:53:33 -0700 (PDT)
X-Received: by 2002:a81:5085:0:b0:2f4:d6fb:f76f with SMTP id
e127-20020a815085000000b002f4d6fbf76fmr821730ywb.190.1652370812828; Thu, 12
May 2022 08:53:32 -0700 (PDT)
Path: i2pn2.org!i2pn.org!aioe.org!news.mixmin.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 08:53:32 -0700 (PDT)
In-Reply-To: <2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Thu, 12 May 2022 15:53:33 +0000
Content-Type: text/plain; charset="UTF-8"
 by: Dan Christensen - Thu, 12 May 2022 15:53 UTC

On Thursday, May 12, 2022 at 11:16:47 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 16:05:49 UTC+2:
> > On Thursday, May 12, 2022 at 9:45:11 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > > If you cannot prove:
> > >
> > > /* Doesn't work for Dan Christensens Case 1 */
> > > ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
> > > ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]
> > > => ALL(a):[Evenness1(a) <=> Evenness2(a)]
> > >
> > > Then Evenness is not self synonymous.
> > Given:
> >
> > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> >
> > ALL(a):[a in N => [Even'(a) <=> EXIST(b):[b in N & a=2*b]]]
> >
> > Since evenness is only determined for the natural numbers, it would suffice to prove:
> >
> > ALL(a):[a in N => [Even'(a) <=> Even(a)]]
> >
> > A trivial proof in DC Proof. Deal with it, Jan Burse.

> You didn't prove:
>
> ALL(a):[Even'(a) <=> Even(a)]
>

Irrelevant. As usual, you are grasping at straws, 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

Re: Formal proofs about functions using DC Proof

<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99889&group=sci.math#99889

 copy link   Newsgroups: sci.math
X-Received: by 2002:a0c:e906:0:b0:456:540b:4e87 with SMTP id a6-20020a0ce906000000b00456540b4e87mr1496011qvo.47.1652387541569;
Thu, 12 May 2022 13:32:21 -0700 (PDT)
X-Received: by 2002:a81:4782:0:b0:2eb:1cb1:5441 with SMTP id
u124-20020a814782000000b002eb1cb15441mr1965083ywa.479.1652387541379; Thu, 12
May 2022 13:32:21 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 13:32:21 -0700 (PDT)
In-Reply-To: <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 12 May 2022 20:32:21 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2213
 by: Mostowski Collapse - Thu, 12 May 2022 20:32 UTC

The summer time sadness of Dan Christensen. He
cannot prove the following with his approach:

/* not provable */
|/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

But dont be sad, you can still prove this here with
your approach, isn't this great?

/* provable */
|- ALL(a):[a e n => (Evenness(a) => Oddness(Successness(a)))]

Its stil a little vexing, since the unprovable formula
has the form ALL(_):[P(_) => ....] so according to
Dan Christensens rule of non-wonky formulas, it

should be non-wonky. But I guess ALL(_):[P(_) => ....]
alone does not help, P(_) needs to be also well defined,
to have more inferential punch. What is well defined?

"In mathematics, a well-defined expression or unambiguous
expression is an expression whose definition assigns it
a unique interpretation or value."
https://en.wikipedia.org/wiki/Well-defined_expression

Re: Formal proofs about functions using DC Proof

<0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99909&group=sci.math#99909

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:6214:262c:b0:45a:97e8:68df with SMTP id gv12-20020a056214262c00b0045a97e868dfmr2603331qvb.52.1652409206025;
Thu, 12 May 2022 19:33:26 -0700 (PDT)
X-Received: by 2002:a25:d64c:0:b0:649:e6e6:8a84 with SMTP id
n73-20020a25d64c000000b00649e6e68a84mr2830117ybg.212.1652409205722; Thu, 12
May 2022 19:33:25 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 12 May 2022 19:33:25 -0700 (PDT)
In-Reply-To: <4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Fri, 13 May 2022 02:33:26 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2153
 by: Dan Christensen - Fri, 13 May 2022 02:33 UTC

On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
> The summer time sadness of Dan Christensen. He
> cannot prove the following with his approach:
>
> /* not provable */
> |/- ALL(a):[Evenness(a) => Oddness(Successness(a))]
>

Weird. In the natural numbers, an odd number ALWAYS directly follows an even number.

> But dont be sad, you can still prove this here with
> your approach, isn't this great?
>
> /* provable */
> |- ALL(a):[a e n => (Evenness(a) => Oddness(Successness(a)))]
>

It is obviously a true statement, but that doesn't mean it is easy to prove.

Dan

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

Re: Formal proofs about functions using DC Proof

<t5mclk$18gv$1@gioia.aioe.org>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99965&group=sci.math#99965

 copy link   Newsgroups: sci.math
Path: i2pn2.org!i2pn.org!aioe.org!Epfvj1XTJoTo8WyxQ3cphg.user.46.165.242.75.POSTED!not-for-mail
From: dau...@dkdkouao.de (Davee Okuda)
Newsgroups: sci.math
Subject: Re: Formal proofs about functions using DC Proof
Date: Fri, 13 May 2022 19:48:04 -0000 (UTC)
Organization: Aioe.org NNTP Server
Message-ID: <t5mclk$18gv$1@gioia.aioe.org>
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org>
<25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com>
<b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com>
<0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Injection-Info: gioia.aioe.org; logging-data="41503"; posting-host="Epfvj1XTJoTo8WyxQ3cphg.user.gioia.aioe.org"; mail-complaints-to="abuse@aioe.org";
User-Agent: PiaoHong/1.68 (NetBSD)
X-Notice: Filtered by postfilter v. 0.9.2
 by: Davee Okuda - Fri, 13 May 2022 19:48 UTC

Dan Christensen wrote:

> On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
>> The summer time sadness of Dan Christensen. He cannot prove the
>> following with his approach: /* not provable */
>> |/- ALL(a):[Evenness(a) => Oddness(Successness(a))]
>
> Weird. In the natural numbers, an odd number ALWAYS directly follows an
> even number.

You talk like an *_EinsatzgruppenFuhrer_*.

Re: Formal proofs about functions using DC Proof

<t5mdh0$ql1$1@dont-email.me>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99967&group=sci.math#99967

 copy link   Newsgroups: sci.math
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: nom...@afraid.org (FromTheRafters)
Newsgroups: sci.math
Subject: Re: Formal proofs about functions using DC Proof
Date: Fri, 13 May 2022 13:02:34 -0700
Organization: Peripheral Visions
Lines: 13
Message-ID: <t5mdh0$ql1$1@dont-email.me>
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com> <t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com> <2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com> <4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
Reply-To: erratic.howard@gmail.com
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-15"; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 13 May 2022 20:02:40 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="f6d9b4ebfcb6dc45d64d9b05a36b878c";
logging-data="27297"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+7+jSHOH/I/6v/xkGloPNJ8k16K392xLk="
Cancel-Lock: sha1:vc/3P57SI0enkD7ecb492NvB5Ig=
X-Newsreader: MesNews/1.08.06.00-gb
X-ICQ: 1701145376
 by: FromTheRafters - Fri, 13 May 2022 20:02 UTC

on 5/12/2022, Dan Christensen supposed :
> On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
>> The summer time sadness of Dan Christensen. He
>> cannot prove the following with his approach:
>>
>> /* not provable */
>>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
>>
>
> Weird. In the natural numbers, an odd number ALWAYS directly follows an even
> number.

Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99971&group=sci.math#99971

 copy link   Newsgroups: sci.math
X-Received: by 2002:a37:4454:0:b0:69f:c339:e2dc with SMTP id r81-20020a374454000000b0069fc339e2dcmr4725586qka.771.1652473536835;
Fri, 13 May 2022 13:25:36 -0700 (PDT)
X-Received: by 2002:a25:5546:0:b0:64a:a5c5:7c34 with SMTP id
j67-20020a255546000000b0064aa5c57c34mr6903534ybb.154.1652473536673; Fri, 13
May 2022 13:25:36 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 13 May 2022 13:25:36 -0700 (PDT)
In-Reply-To: <t5mdh0$ql1$1@dont-email.me>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
<t5mdh0$ql1$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Fri, 13 May 2022 20:25:36 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2564
 by: Mostowski Collapse - Fri, 13 May 2022 20:25 UTC

Yes, we are possibly not yet at a faithful translation
of Euclid, since Euclid had possibly only the positive
natural numbers in mind, and then this phrase here:

6. An even number is that which is divisible into two equal parts.
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.
http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html

Could mean +/- 1 unit, i.e. not necessarely always
adding a unit, maybe sometimes subtracting a unit.
Also Euclid has possibly an "iff" and not only "if".

FromTheRafters schrieb am Freitag, 13. Mai 2022 um 22:02:50 UTC+2:
> on 5/12/2022, Dan Christensen supposed :
> > On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
> >> The summer time sadness of Dan Christensen. He
> >> cannot prove the following with his approach:
> >>
> >> /* not provable */
> >>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
> >>
> >
> > Weird. In the natural numbers, an odd number ALWAYS directly follows an even
> > number.
> Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<9b5b2b89-9e7d-4d43-be78-fea1201b85fen@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99976&group=sci.math#99976

 copy link   Newsgroups: sci.math
X-Received: by 2002:a37:b742:0:b0:6a0:5e42:2fa8 with SMTP id h63-20020a37b742000000b006a05e422fa8mr5036176qkf.274.1652474229021;
Fri, 13 May 2022 13:37:09 -0700 (PDT)
X-Received: by 2002:a25:dcb:0:b0:648:df89:a5b3 with SMTP id
194-20020a250dcb000000b00648df89a5b3mr6850215ybn.485.1652474228827; Fri, 13
May 2022 13:37:08 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 13 May 2022 13:37:08 -0700 (PDT)
In-Reply-To: <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
<t5mdh0$ql1$1@dont-email.me> <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <9b5b2b89-9e7d-4d43-be78-fea1201b85fen@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Fri, 13 May 2022 20:37:09 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 3273
 by: Mostowski Collapse - Fri, 13 May 2022 20:37 UTC

A Proof of (in N):

~EXIST(b):[a=b+b] => EXIST(c):[a=c+c+1]

How would this work? I came up already with
one step. Namely trying to show:

ALL(b):ALL(c):[b+b =\= c+c+1]

There are two cases:

Case 1: b=<c, then you can use subtraction and get:
0 =\= (c-b)+(c-b)+1
Which is one of the Peano Axioms, s(x)=\=0.

Case 2: b>c, then you can use subtraction and get:
(b-c-1)+(b-c-1)+1=\=0
Which is one of the Peano Axioms, s(x)=\=0.

Just some beginnings to prove the thingy...

Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:25:41 UTC+2:
> Yes, we are possibly not yet at a faithful translation
> of Euclid, since Euclid had possibly only the positive
> natural numbers in mind, and then this phrase here:
>
> 6. An even number is that which is divisible into two equal parts.
> 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.
> http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html
>
> Could mean +/- 1 unit, i.e. not necessarely always
> adding a unit, maybe sometimes subtracting a unit.
> Also Euclid has possibly an "iff" and not only "if".
> FromTheRafters schrieb am Freitag, 13. Mai 2022 um 22:02:50 UTC+2:
> > on 5/12/2022, Dan Christensen supposed :
> > > On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
> > >> The summer time sadness of Dan Christensen. He
> > >> cannot prove the following with his approach:
> > >>
> > >> /* not provable */
> > >>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
> > >>
> > >
> > > Weird. In the natural numbers, an odd number ALWAYS directly follows an even
> > > number.
> > Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<5b118228-e5a6-4425-af6a-cef0749c5c66n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99980&group=sci.math#99980

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:795:b0:69f:d074:6067 with SMTP id 21-20020a05620a079500b0069fd0746067mr4928976qka.527.1652474485922;
Fri, 13 May 2022 13:41:25 -0700 (PDT)
X-Received: by 2002:a81:4f01:0:b0:2f8:ea79:9ada with SMTP id
d1-20020a814f01000000b002f8ea799adamr7989396ywb.512.1652474485777; Fri, 13
May 2022 13:41:25 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 13 May 2022 13:41:25 -0700 (PDT)
In-Reply-To: <9b5b2b89-9e7d-4d43-be78-fea1201b85fen@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
<t5mdh0$ql1$1@dont-email.me> <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
<9b5b2b89-9e7d-4d43-be78-fea1201b85fen@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <5b118228-e5a6-4425-af6a-cef0749c5c66n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Fri, 13 May 2022 20:41:25 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3989
 by: Mostowski Collapse - Fri, 13 May 2022 20:41 UTC

When we have done that, we can move on to:

Euclid proved that 2^(p−1=(2^p − 1) is an even perfect number
whenever 2^p − 1 is prime. This is the final result on number
theory in Euclid's Elements;
https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem

LoL

Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:37:15 UTC+2:
> A Proof of (in N):
>
> ~EXIST(b):[a=b+b] => EXIST(c):[a=c+c+1]
>
> How would this work? I came up already with
> one step. Namely trying to show:
>
> ALL(b):ALL(c):[b+b =\= c+c+1]
>
> There are two cases:
>
> Case 1: b=<c, then you can use subtraction and get:
> 0 =\= (c-b)+(c-b)+1
> Which is one of the Peano Axioms, s(x)=\=0.
>
> Case 2: b>c, then you can use subtraction and get:
> (b-c-1)+(b-c-1)+1=\=0
> Which is one of the Peano Axioms, s(x)=\=0.
>
> Just some beginnings to prove the thingy...
> Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:25:41 UTC+2:
> > Yes, we are possibly not yet at a faithful translation
> > of Euclid, since Euclid had possibly only the positive
> > natural numbers in mind, and then this phrase here:
> >
> > 6. An even number is that which is divisible into two equal parts.
> > 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.
> > http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html
> >
> > Could mean +/- 1 unit, i.e. not necessarely always
> > adding a unit, maybe sometimes subtracting a unit.
> > Also Euclid has possibly an "iff" and not only "if".
> > FromTheRafters schrieb am Freitag, 13. Mai 2022 um 22:02:50 UTC+2:
> > > on 5/12/2022, Dan Christensen supposed :
> > > > On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
> > > >> The summer time sadness of Dan Christensen. He
> > > >> cannot prove the following with his approach:
> > > >>
> > > >> /* not provable */
> > > >>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
> > > >>
> > > >
> > > > Weird. In the natural numbers, an odd number ALWAYS directly follows an even
> > > > number.
> > > Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<a8fb10ad-de7c-4242-a255-6320444b7f69n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=99982&group=sci.math#99982

 copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:5c8b:0:b0:2f3:dd2f:b512 with SMTP id r11-20020ac85c8b000000b002f3dd2fb512mr6331022qta.625.1652474787017;
Fri, 13 May 2022 13:46:27 -0700 (PDT)
X-Received: by 2002:a81:5085:0:b0:2f4:d6fb:f76f with SMTP id
e127-20020a815085000000b002f4d6fbf76fmr8352786ywb.190.1652474786850; Fri, 13
May 2022 13:46:26 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!news.freedyn.de!newsreader4.netcologne.de!news.netcologne.de!feeder1.cambriumusenet.nl!feed.tweak.nl!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 13 May 2022 13:46:26 -0700 (PDT)
In-Reply-To: <5b118228-e5a6-4425-af6a-cef0749c5c66n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.70; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.70
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
<t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com>
<2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com>
<4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com>
<t5mdh0$ql1$1@dont-email.me> <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
<9b5b2b89-9e7d-4d43-be78-fea1201b85fen@googlegroups.com> <5b118228-e5a6-4425-af6a-cef0749c5c66n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a8fb10ad-de7c-4242-a255-6320444b7f69n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Fri, 13 May 2022 20:46:27 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Mostowski Collapse - Fri, 13 May 2022 20:46 UTC

But I am not that optimistic, since:

This theorem was included in a web listing of the "top 100
mathematical theorems", dating from 1999, which later became
used by Freek Wiedijk as a benchmark set to test the power of
different proof assistants. As of 2021, the proof of the Euclid–Euler
theorem had been formalized in 5 of the 10 proof assistants
recorded by Wiedijk.
https://www.cs.ru.nl/~freek/100/

Also Dan did not yet prove Zorns lemma...

Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:41:31 UTC+2:
> When we have done that, we can move on to:
>
> Euclid proved that 2^(p−1=(2^p − 1) is an even perfect number
> whenever 2^p − 1 is prime. This is the final result on number
> theory in Euclid's Elements;
> https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem
>
> LoL
> Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:37:15 UTC+2:
> > A Proof of (in N):
> >
> > ~EXIST(b):[a=b+b] => EXIST(c):[a=c+c+1]
> >
> > How would this work? I came up already with
> > one step. Namely trying to show:
> >
> > ALL(b):ALL(c):[b+b =\= c+c+1]
> >
> > There are two cases:
> >
> > Case 1: b=<c, then you can use subtraction and get:
> > 0 =\= (c-b)+(c-b)+1
> > Which is one of the Peano Axioms, s(x)=\=0.
> >
> > Case 2: b>c, then you can use subtraction and get:
> > (b-c-1)+(b-c-1)+1=\=0
> > Which is one of the Peano Axioms, s(x)=\=0.
> >
> > Just some beginnings to prove the thingy...
> > Mostowski Collapse schrieb am Freitag, 13. Mai 2022 um 22:25:41 UTC+2:
> > > Yes, we are possibly not yet at a faithful translation
> > > of Euclid, since Euclid had possibly only the positive
> > > natural numbers in mind, and then this phrase here:
> > >
> > > 6. An even number is that which is divisible into two equal parts.
> > > 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.
> > > http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html
> > >
> > > Could mean +/- 1 unit, i.e. not necessarely always
> > > adding a unit, maybe sometimes subtracting a unit.
> > > Also Euclid has possibly an "iff" and not only "if".
> > > FromTheRafters schrieb am Freitag, 13. Mai 2022 um 22:02:50 UTC+2:
> > > > on 5/12/2022, Dan Christensen supposed :
> > > > > On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
> > > > >> The summer time sadness of Dan Christensen. He
> > > > >> cannot prove the following with his approach:
> > > > >>
> > > > >> /* not provable */
> > > > >>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
> > > > >>
> > > > >
> > > > > Weird. In the natural numbers, an odd number ALWAYS directly follows an even
> > > > > number.
> > > > Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<t5mnfr$vdb$1@dont-email.me>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=100000&group=sci.math#100000

 copy link   Newsgroups: sci.math
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: nom...@afraid.org (FromTheRafters)
Newsgroups: sci.math
Subject: Re: Formal proofs about functions using DC Proof
Date: Fri, 13 May 2022 15:52:37 -0700
Organization: Peripheral Visions
Lines: 29
Message-ID: <t5mnfr$vdb$1@dont-email.me>
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com> <t5j30s$euv8$3@solani.org> <25717703-6dcb-4ea0-a001-4bdb1c08af70n@googlegroups.com> <2a2b1008-c426-4f2c-acfc-6fdae2a4cc0cn@googlegroups.com> <b6cfb54e-a98e-46f9-a9cb-f641e0b457fdn@googlegroups.com> <4f0d8985-6806-4f37-9517-c251b49dfb3fn@googlegroups.com> <0ffa197b-b8cf-41d9-a2db-e692c3eb319an@googlegroups.com> <t5mdh0$ql1$1@dont-email.me> <54263c07-13c0-407c-9e6b-28dd52bbc5a3n@googlegroups.com>
Reply-To: erratic.howard@gmail.com
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-15"; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 13 May 2022 22:52:44 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="2e238afbd2e0661fafb8dbb2c6baf21a";
logging-data="32171"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19CRtz0EI2Hq41CHOVhtb/iTb2nBnmj4u0="
Cancel-Lock: sha1:74sxqS+FSwAKlhON6LBMRIc7p/U=
X-Newsreader: MesNews/1.08.06.00-gb
X-ICQ: 1701145376
 by: FromTheRafters - Fri, 13 May 2022 22:52 UTC

That works for integers too, bonus!

Mostowski Collapse has brought this to us :
> Yes, we are possibly not yet at a faithful translation
> of Euclid, since Euclid had possibly only the positive
> natural numbers in mind, and then this phrase here:
>
> 6. An even number is that which is divisible into two equal parts.
> 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.
> http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html
>
> Could mean +/- 1 unit, i.e. not necessarely always
> adding a unit, maybe sometimes subtracting a unit.
> Also Euclid has possibly an "iff" and not only "if".
>
> FromTheRafters schrieb am Freitag, 13. Mai 2022 um 22:02:50 UTC+2:
>> on 5/12/2022, Dan Christensen supposed :
>>> On Thursday, May 12, 2022 at 4:32:27 PM UTC-4, Mostowski Collapse wrote:
>>>> The summer time sadness of Dan Christensen. He
>>>> cannot prove the following with his approach:
>>>>
>>>> /* not provable */
>>>>> /- ALL(a):[Evenness(a) => Oddness(Successness(a))]
>>>>
>>>
>>> Weird. In the natural numbers, an odd number ALWAYS directly follows an
>>> even number.
>> Naturals w/zero only.

Re: Formal proofs about functions using DC Proof

<87de3c8c-010e-4505-b6c7-275666df98c7n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=138571&group=sci.math#138571

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:6214:3a07:b0:62d:eaa8:bdf6 with SMTP id nw7-20020a0562143a0700b0062deaa8bdf6mr4187890qvb.3.1687541132165;
Fri, 23 Jun 2023 10:25:32 -0700 (PDT)
X-Received: by 2002:a0d:ec07:0:b0:56d:791:d1a4 with SMTP id
q7-20020a0dec07000000b0056d0791d1a4mr9637587ywn.7.1687541131868; Fri, 23 Jun
2023 10:25:31 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 23 Jun 2023 10:25:31 -0700 (PDT)
In-Reply-To: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.44; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.44
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <87de3c8c-010e-4505-b6c7-275666df98c7n@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: burse...@gmail.com (Mild Shock)
Injection-Date: Fri, 23 Jun 2023 17:25:32 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3688
 by: Mild Shock - Fri, 23 Jun 2023 17:25 UTC

Why is there no temporal logic involved. Peano
add can be used to compute 2+2=4, and we start
with 2+2 and THEN we obtained 4. You did use

temporal logic, which is surely wrong, since the
logic you used, i.e. FOL can only refer to the present,
there is no time parameter. But in calculation and

thus Peano the input 2+2 comes first snd THEN the
output 4 is computed.

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

Re: Formal proofs about functions using DC Proof

<c9c66e5f-faec-4e41-9a98-477708ecea0bn@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=138584&group=sci.math#138584

 copy link   Newsgroups: sci.math
X-Received: by 2002:ad4:55e8:0:b0:62f:efde:159c with SMTP id bu8-20020ad455e8000000b0062fefde159cmr2402538qvb.2.1687544476644;
Fri, 23 Jun 2023 11:21:16 -0700 (PDT)
X-Received: by 2002:a05:6870:b7b0:b0:1a9:84a5:bd1a with SMTP id
ed48-20020a056870b7b000b001a984a5bd1amr5202844oab.0.1687544476359; Fri, 23
Jun 2023 11:21:16 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 23 Jun 2023 11:21:15 -0700 (PDT)
In-Reply-To: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=2600:387:c:5511:0:0:0:5;
posting-account=fsC03QkAAAAwkSNcSEKmlcR-W_HNitEd
NNTP-Posting-Host: 2600:387:c:5511:0:0:0:5
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <c9c66e5f-faec-4e41-9a98-477708ecea0bn@googlegroups.com>
Subject: Re: Formal proofs about functions using DC Proof
From: plutoniu...@gmail.com (Archimedes Plutonium)
Injection-Date: Fri, 23 Jun 2023 18:21:16 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 8612
 by: Archimedes Plutonium - Fri, 23 Jun 2023 18:21 UTC

Which has more intelligence? Jan Burse's dog or Jan Burse?
29 views
Subscribe

Archimedes Plutonium's profile photo
Archimedes Plutonium
4:00 AM (9 hours ago)



to
He calls himself now Mild Shock, far better than his previous name Mostowski Collapse. But is there some Freudian slip interpretation of this?

But I think his dog has more intelligence than Jan Burse, for his dog uses only one eye to see you and reserves his other eye. Maybe the BBC can do a animal story of Jan's dog-- a dog smarter than its owner.

I think a better name for Jan Burse for his new rounds of hate spew, would have been "Mild Cock" instead of Mild Shock, and certainly, a blunt Freudian slip in sci.math. And how much Freudian slips occur in sci.math?? Perhaps 1 per day are Freudian slips, like WM's dark numbers. That would be well with Jan Burse posting into a Earle Jones thread, with his logo picture showing Earle sucking on a cock-- an alltime record holder of Freudian slips. So masterful is Earle's Freudian slip, his inner longings, that Earle is oblivious dumb to the slip he made. As daffy duck would say-- "nay, I am sure, am sure".

So if Jan Burse would post into a Earle Jones thread, would complete the circle-- Jan Burse Mild Cock and Earle sucking on a cock. What Dan Christensen would lecture on as a union of sets, but get it wrong in his presentation, gurgling all over his shirt.

Somehow we have to get the dark personality of Dan Christensen in on this, with his dark logo picture of DC Proof. Dan is your logo picture the Freudian slip wannabe that of a arsehole? For your posts are arseholish.

And of course Kibo Parry (Moron-Volney) must get in on the Freudian slip action, his constant posts of failure, worse than "I sik, I cri" out of Portugal.

So what is Kibo's gargantuan Freudian slip?? Why yes of course, the made up fake name of "kibo" itself, being derived from "kook" a baby kook is a kibo. But in the romance languages "kibo" comes from kock, or cock and is Kibo's perverse way of hiding his Freudian slip of cock. This is what Kibo learned in his first week in CIA and caused him to blow his cover in just a few days upon entry into the CIA, a record not broken since Kibo entered.

And here is Kibo in 1997, making gay advances on the King of Science AP, for which AP was insulted at the time. For AP is asexual, above sex, in a higher plane of orbit-- science. Not Kibo's vulgar brains between his legs and a vacuum skull.

Kibo in CIA
> > > > > > Kibo Parry Moroney in 1997 blows his CIA cover-- to the entire world, mind you---
> > > > > > Re: Archimedes Vanadium, America's most beloved poster
> > > > > > >> In article <5nefan$i06$9...@news.thecia.net> kibo greps <ki....@shell.thecia.net> writes:

Kibo had a Freudian slip with blowing his cover on the first day at the job with CIA. Then another Freudian slip with his moniker -- Kibo, although his allies tried to convince him to chose Turbo, more masculine. No, kibo ended up with Kibo, and now in older age-- 60s?? Kibo is realizing his poor choice of nicknames, and thinking of changing it to Arky. Why Arky,,... Kibo?? Is it Joan of Arc to clean and scrub your life, your miserable dark and dank life you lead so far, and that Joan of Arc saint would clean some of that filth off of you.

AP, King of Science, especially Physics

Dogelog Player's profile photo
Dogelog Player
4:19 AM (9 hours ago)

Hi, I am the dog of Mild Shock. I think your nick- name should be Small Cock, or Micro Penis. Bye
Mild Shock's profile photo
Mild Shock
4:22 AM (9 hours ago)

Yes, my dog is right. He is surely more intelligent than me. And I guess he is right your nick-name
Volney's profile photo
Volney
8:56 AM (4 hours ago)

🌪️ of Math and 🌀 of Physics Archimedes "Meckling Village Idiot" Plutonium <plutonium.
Fritz Feldhase's profile photo
Fritz Feldhase
9:14 AM (4 hours ago)

On Friday, June 23, 2023 at 11:00:57 AM UTC+2, Archimedes Plutonium wrote: "Which has more
Mild Shock's profile photo
Mild Shock
11:34 AM (2 hours ago)

Freud would possibly only need the picture of the „one eyed [snake]“ to diagnose Archimedes Plutonium
Archimedes Plutonium's profile photo
Archimedes Plutonium
1:14 PM (1 minute ago)



to
Gangs in a science, make a mockery and degradation of that science. Whether a sex-gang, a money-gang, a ethnic-gang. Science and gangs just are totally incompatible.

Recently I started to include the Scientific Method in my books and my discussions.

Which of the principles of the Scientific Method is repulsed by "gang behavior" in that particular science???

--- quoting recent book of mine ---
to Plutonium Atom Universe
Up until now, I have not included or made mention of the Method of Science. And I need to go back into all my textbooks and state this method where appropriate. Funny how doing psychology and sociology of math mistakes calls the Scientific Method into action.

The Scientific Method is something I learned early in High School.

Source: Wikipedia.

Observation/ question

Research Topic

Hypothesis

Test with Experiment

Analyze data

Report conclusions

I do not recall if Feynman goes through the Scientific Method in one of his books-- perhaps "Character of Physical Law". Perhaps he mentions the Scientific Method in bits and pieces throughout his "Lectures on Physics".

Here is a slightly different take on Scientific Method from Internet (the ladders dot com)

Systematic observation

experimenting

measuring

testing

formulating

modifying a hypothesis

What I am going to do is apply the Scientific Method to mathematics and why errors in math sometimes abandon the Scientific Method. What I am focusing on is the math error of trigonometry of making one axis be different from the other axis in making graphs. In calculus, I am focusing on the abandonment of the Scientific Method in Calculus, when numbers are cobbled together to make Numbers, such as the Reals, and when functions are cobbled together and called functions when cobbling together is seen as science, when it is not.

--- end quote ---

So, what principle or principles does "gang activity" violate the Scientific Method?? I would say all the principles for gang activity is totally counter to the activities of science. The reward of Science is truth. The reward of gang activity is -- sex, or money, or power (be it military, political or interpersonal).

The newsgroups, sci.math and sci.physics would be better newsgroups if the "gangs" that infest them are removed. For instance, when one of the gang members forged necrophilia upon AP, not only should he be removed-- and he was removed, but also the entire gang network that operates with him, be removed.

Science does not mix with gang activity.

AP

STUDENTS BEWARE: Don't be a victim of AP's fake math and science

<4da40a84-b276-44f2-a76f-c5dd55322336n@googlegroups.com>

 copy mid

https://www.novabbs.com/tech/article-flat.php?id=138603&group=sci.math#138603

 copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:15c5:b0:3fd:d29e:5d37 with SMTP id d5-20020a05622a15c500b003fdd29e5d37mr7448887qty.1.1687551641936;
Fri, 23 Jun 2023 13:20:41 -0700 (PDT)
X-Received: by 2002:a05:6830:4c8:b0:6b5:dc78:2d26 with SMTP id
s8-20020a05683004c800b006b5dc782d26mr1804297otd.0.1687551641676; Fri, 23 Jun
2023 13:20:41 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 23 Jun 2023 13:20:41 -0700 (PDT)
In-Reply-To: <c9c66e5f-faec-4e41-9a98-477708ecea0bn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <e71afb93-d0e7-408b-8d84-3faa2c5c54e2n@googlegroups.com> <c9c66e5f-faec-4e41-9a98-477708ecea0bn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4da40a84-b276-44f2-a76f-c5dd55322336n@googlegroups.com>
Subject: STUDENTS BEWARE: Don't be a victim of AP's fake math and science
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Fri, 23 Jun 2023 20:20:41 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Dan Christensen - Fri, 23 Jun 2023 20:20 UTC

STUDENTS BEWARE: Don't be a victim of AP's fake math and science

On Friday, June 23, 2023 at 2:21:20 PM UTC-4, Archimedes Plutonium wrote:

[snip]

> ... Dan Christensen ...

[snip]

Time for another spanking, Archie Poo! When will you learn? Once again...

From his antics here at sci.math, it is obvious that AP has abandoned all hope of being recognized as a credible personality. He is a malicious internet troll who now wants only to mislead and confuse students. He may not be all there, but his fake math and science can only be meant to promote failure in schools. One can only guess at his motives. Is it revenge for his endless string of personal failures in life? Who knows?

In AP's OWN WORDS that, over the years here, he has NEVER renounced or withdrawn:

"Negative numbers are the witches and hobgoblins of insane kook mathematicians. "
--Dec. 7, 2022

“Primes do not exist, because the set they were borne from has no division.”
--June 29, 2020

“The last and largest finite number is 10^604.”
--June 3, 2015

“0 appears to be the last and largest finite number”
--June 9, 2015

“0/0 must be equal to 1.”
-- June 9, 2015

“0 is an infinite irrational number.”
--June 28, 2015

“No negative numbers exist.”
--December 22, 2018

“Rationals are not numbers.”
--May 18, 2019

According to AP's “chess board math,” an equilateral triangle is a right-triangle.
--December 11, 2019

Which could explain...

“The value of sin(45 degrees) = 1.” (Actually 0.707)
--May 31, 2019

AP deliberately and repeatedly presented the truth table for OR as the truth table for AND:

“New Logic
AND
T & T = T
T & F = T
F & T = T
F & F = F”
--November 9, 2019

AP seeks aid of Russian agents to promote failure in schools:

"Please--Asking for help from Russia-- russian robots-- to create a new, true mathematics [sic]. What I like for the robots to do, is list every day, about 4 Colleges ( of the West) math dept, and ask why that math department is teaching false and fake math, and if unable to change to the correct true math, well, simply fire that math department until they can find professors who recognize truth in math from fakery...."
--November 9, 2017

And if that wasn't weird enough...

“The totality, everything that there is [the universe], is only 1 atom of plutonium [Pu]. There is nothing outside or beyond this one atom of plutonium.”
--April 4, 1994

“The Universe itself is one gigantic big atom.”
--November 14, 2019

AP's sinister Atom God Cult of Failure???

“Since God-Pu is marching on.
Glory! Glory! Atom Plutonium!
Its truth is marching on.
It has sounded forth the trumpet that shall never call retreat;
It is sifting out the hearts of people before its judgment seat;
Oh, be swift, my soul, to answer it; be jubilant, my feet!
Our God-Pu is marching on.”
--December 15, 2018 (Note: Pu is the atomic symbol for plutonium)

Updated version (repetition removed):

"Oh Atom Plutonium, as great as you are
How great thou are, are, are, are.
Oh Atom Plutonium, the God that you are
How beautiful is your world of science
Your science is the world
How beautiful is your world of science
Your science is the world
Oh Atom Plutonium, Great God of Atoms
Atom of Atoms
Oh Atom Plutonium, as great as thou art"
--March 24, 2023

Dan

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

Pages:1234567
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor