Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Last yeer I kudn't spel Engineer. Now I are won.

tech / sci.math / Re: DC Proof challenge: Zorn's Lemma, how formalize it?

SubjectAuthor
o Re: DC Proof challenge: Zorn's Lemma, how formalize it?Mostowski Collapse

1
Re: DC Proof challenge: Zorn's Lemma, how formalize it?

<38c9830d-1c27-4516-a2a9-d0b011c01503n@googlegroups.com>

  copy mid

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

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:120e:: with SMTP id y14mr30320039qtx.671.1638676845263;
Sat, 04 Dec 2021 20:00:45 -0800 (PST)
X-Received: by 2002:a25:80c6:: with SMTP id c6mr29616269ybm.206.1638676845082;
Sat, 04 Dec 2021 20:00:45 -0800 (PST)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Sat, 4 Dec 2021 20:00:44 -0800 (PST)
In-Reply-To: <71cfe3b3-35e0-4ea9-82b0-8b69b5fd47e4n@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: <c8fa5e22-ad54-4a3b-bcbc-b0f2b15e4460o@googlegroups.com>
<9d99b7d7-9b7e-44b2-91cd-56dca4804239n@googlegroups.com> <012dc517-1687-4181-92eb-71a42639ae1en@googlegroups.com>
<286db615-3932-40c1-985f-6af056880c3fn@googlegroups.com> <c75274ae-9bc7-4f17-ac74-2e6bc19927d9n@googlegroups.com>
<01011a91-6375-4fb1-92be-c7536ea0bbf6n@googlegroups.com> <6ca3fcbc-b9c0-4ba0-8c5d-d3673ae90428n@googlegroups.com>
<ca6af1ca-afa6-419f-9ae5-f1c460619113n@googlegroups.com> <7de38370-aa8a-4cba-af19-227347f9abe2n@googlegroups.com>
<eb52040e-965d-4456-9c69-0aaf674821b0n@googlegroups.com> <1cc73c9e-dc15-46f9-b16c-76dc78c5353bn@googlegroups.com>
<c7938015-fafc-49d3-82cd-1b5e27d03263n@googlegroups.com> <c6a97583-01aa-4daf-9110-1d46f66e33fdn@googlegroups.com>
<s38i0t$7r1$1@gioia.aioe.org> <9074cdff-a481-4848-8a4e-88e8e5e5cdd5n@googlegroups.com>
<62a02843-ac03-4d5d-9a13-978474f45b1an@googlegroups.com> <b541a02a-5dee-4f05-a9eb-166b5cd2995en@googlegroups.com>
<6058fb16$0$16170$426a74cc@news.free.fr> <1e07b240-8c55-453a-ace0-54280d1ba270n@googlegroups.com>
<a4ab7bbb-40fd-404d-8407-f936075cf844n@googlegroups.com> <a383133f-aa6c-479a-99b0-8e8ca29c53e5n@googlegroups.com>
<62a157d9-5c23-4df1-9b9d-7e6578ea0f0bn@googlegroups.com> <1afe1819-8501-4825-b88f-e10ab71ecf82n@googlegroups.com>
<1c0e8046-af8b-4e0b-afda-b2951eb660a5n@googlegroups.com> <bc9d8112-a06a-4ea6-a570-b84ed192a64fn@googlegroups.com>
<0983427d-a164-4642-9fb3-e60fa205eb6dn@googlegroups.com> <1658a085-4353-4834-87fe-e36ac3314ff5n@googlegroups.com>
<b5080eb0-1c74-439a-ad1f-8912b014c069n@googlegroups.com> <bea63878-1937-43e9-a01b-7ff1ce0b4960n@googlegroups.com>
<8fffe4a4-319b-486b-b799-adc003c74fc0n@googlegroups.com> <4d2f3baa-834b-4037-aa2e-35ae2f3e4684n@googlegroups.com>
<602f169b-77fc-429f-b398-bbaa3d6e0e47n@googlegroups.com> <2f11dff8-5d44-4016-a7a6-0d2bf517da04n@googlegroups.com>
<1494fdc0-9206-40cb-a9d0-f81933bb1b79n@googlegroups.com> <7ed84b80-3865-4496-b276-e6a4ce4a3412n@googlegroups.com>
<27f5614c-cf70-43ff-85ad-1619a6c7e3f1n@googlegroups.com> <d4a736f0-e97d-4526-ab41-dfb75394ab0cn@googlegroups.com>
<ef6df3ae-724c-4ad5-9d11-26b738d9bdean@googlegroups.com> <0abbbeeb-21a7-4c10-92ea-52b7df675e98n@googlegroups.com>
<004fe500-5f8d-4395-b8c0-6ed353116be2n@googlegroups.com> <30f07c49-3382-4309-abba-e20b6b01e82dn@googlegroups.com>
<73c374a8-127e-479c-b285-4d4290c043acn@googlegroups.com> <e57d5f20-c109-4d4d-92f5-628b991f5decn@googlegroups.com>
<c9ee204f-64d7-413c-a71e-d9e402cffca3n@googlegroups.com> <82b11c4a-fb59-4753-935b-d1d951f12201n@googlegroups.com>
<3bd0e16d-5425-4371-bff5-1551f72b2f09n@googlegroups.com> <4a4b1bd1-9ce0-491c-aac2-e27eba7ef9c3n@googlegroups.com>
<30039210-baf3-4c84-93a9-0502f6395c67n@googlegroups.com> <1d7e39e3-a661-47cf-92ff-ba22e44715e3n@googlegroups.com>
<1ba07780-ca0e-4586-984f-7b064e846170n@googlegroups.com> <26210090-1878-45d7-929d-6a6c608315a8n@googlegroups.com>
<ef178e2f-3337-4771-ba7f-30950f11baf5n@googlegroups.com> <3121b575-30b4-4ad6-a002-ab25b715b294n@googlegroups.com>
<50f70c95-af25-410d-aaff-29610ed3cebfn@googlegroups.com> <7ea265fd-19e6-46b8-9c19-48d4eb32ca62n@googlegroups.com>
<592e9bd7-604d-4bec-8d8b-0591bb0a8efbn@googlegroups.com> <50eb6906-e7d2-444d-a110-e01b4bc7a3e6n@googlegroups.com>
<e7bb6a16-17a4-4ed1-89d0-7cfa7107f314n@googlegroups.com> <76fb51c4-631e-4c1b-90f3-481a70cf3aacn@googlegroups.com>
<cd1d328f-0d0b-4fd0-962b-d7ed4d55adf9n@googlegroups.com> <7230a698-4cfb-4a20-b5ae-590a0fc13ecdn@googlegroups.com>
<9fe155e8-6eae-4b5e-b46e-c621b7ce25dcn@googlegroups.com> <c8336cba-4eb2-4f42-88f0-1c36c31975cbn@googlegroups.com>
<b59c64e7-4546-4c36-84b2-d4ecddb87276n@googlegroups.com> <9990290f-3c8b-4cc9-99bf-6ee47fb5b6d9n@googlegroups.com>
<c9538649-1433-43d5-990c-179c3a63ec96n@googlegroups.com> <f9503b2e-f3d6-4da9-8643-79dd03f51726n@googlegroups.com>
<a62f295c-dff6-4d82-b06c-eac2126569e3n@googlegroups.com> <82d1c250-1f07-4861-9f00-ca62413e925fn@googlegroups.com>
<ca6888b3-a467-4ba4-92a3-6c42066ab77dn@googlegroups.com> <281f121b-c052-4045-b67f-15843e858e3bn@googlegroups.com>
<b8070683-4a8a-45d9-bd5b-acb61f4be833n@googlegroups.com> <d5de0edb-72e7-42e1-98ba-5519e206ecb9n@googlegroups.com>
<a04798bd-d401-4558-a736-88a753bf069fn@googlegroups.com> <33cab9f8-2ee1-4efa-aa1c-2a2559a1aa25n@googlegroups.com>
<1e803f11-4f79-4902-876c-8055a899d26bn@googlegroups.com> <200c85e7-98b2-456b-9e4c-ce2271208ca3n@googlegroups.com>
<dc23e7ca-2cae-4eec-a425-288d444a7932n@googlegroups.com> <b13ccbaa-d11b-4be5-984e-e4e3f2909824n@googlegroups.com>
<3281c7aa-72d3-4417-ae0c-965fcf68dc65n@googlegroups.com> <1bb0aec6-2648-4af0-8032-9d2eaf379349n@googlegroups.com>
<71cfe3b3-35e0-4ea9-82b0-8b69b5fd47e4n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <38c9830d-1c27-4516-a2a9-d0b011c01503n@googlegroups.com>
Subject: Re: DC Proof challenge: Zorn's Lemma, how formalize it?
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Sun, 05 Dec 2021 04:00:45 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Lines: 70
 by: Mostowski Collapse - Sun, 5 Dec 2021 04:00 UTC

You cannot prove with your chimpansee definition:

(**) Def(F) & Def(G) => F = G

Here is a counter model:

∀a(a=z → ∃b(b=z ∧ (Fab ∧ ∀c(c=z → (Fac → c=b))))) ∧
∀a(a=z → ∃b(b=z ∧ (Gab ∧ ∀c(c=z → (Gac → c=b)))))
does not entail
∀a∀b(Fab ↔ Gab).
https://www.umsu.de/trees

Countermodel:
Domain: { 0, 1 }
z: 0
F: { (0,0), (1,0) }
G: { (0,0), (1,1) }

But a graph for any F : {0} -> {0} looks always the same:

Dom Co-Dom
( ) ( )
( 0-)---------(>0 )
( ) ( )

So we want a definition in math, like the one on Wikipedia,
that results in something welldefined, and not a chimpansee definition.

https://en.wikipedia.org/wiki/Well-defined_expression

Mostowski Collapse schrieb am Sonntag, 5. Dezember 2021 um 04:49:19 UTC+1:
> You can make another experiment to show that your
> definition is nonsense. There is only one function F : {0} -> {0}.
> So if Def(F) expresses F : {0} -> {0}, then this here should
>
> be provable:
>
> (**) Def(F) & Def(G) => F = G
>
> Can you prove it with your definition?
>
> Or more precisely can you prove from this 3 axioms:
>
> (1) ALL(a):[S(a) <=> a=0]
>
> (2) ALL(a):[S(a) => EXIST(b):[S(b) & F(a,b) & ALL(c):[S(c) => [F(a,c) => c=b]]]]
>
> (3) ALL(a):[S(a) => EXIST(b):[S(b) & G(a,b) & ALL(c):[S(c) => [G(a,c) => c=b]]]]
>
> That this follows theorem follows:
>
> ALL(a):ALL(b):[F(a,b) <=> G(a,b)] ?
> Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 03:34:44 UTC+1:
> > On Saturday, December 4, 2021 at 7:39:49 PM UTC-5, Mostowski Collapse wrote:
> > > Dang your stupid, the link says:
> > > > Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
> > > https://www.dcproof.com/FunctionUndefinedV2.htm
> > >
> > > Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
> > > already follows from F ⊆ {0} x {0}.
> > See my reply just now to your identical posting at sci.logic
> >
> > Dan

1
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor