Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

"If you are afraid of loneliness, don't marry." -- Chekhov

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?

<229b1177-2db6-4e9d-b4e3-5fd24c2c85fbn@googlegroups.com>

  copy mid

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

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:b8b:: with SMTP id k11mr22554485qkh.746.1638620666138;
Sat, 04 Dec 2021 04:24:26 -0800 (PST)
X-Received: by 2002:a25:80c6:: with SMTP id c6mr25400714ybm.206.1638620665994;
Sat, 04 Dec 2021 04:24:25 -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 04:24:25 -0800 (PST)
In-Reply-To: <dc23e7ca-2cae-4eec-a425-288d444a7932n@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>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <229b1177-2db6-4e9d-b4e3-5fd24c2c85fbn@googlegroups.com>
Subject: Re: DC Proof challenge: Zorn's Lemma, how formalize it?
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Sat, 04 Dec 2021 12:24:26 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Lines: 58
 by: Mostowski Collapse - Sat, 4 Dec 2021 12:24 UTC

Just check wikipedia:

Any subset of the Cartesian product of two sets X and Y defines a
binary relation R ⊆ X × Y between these two sets.
[...]
A function is a **binary relation** that is functional and serial.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Wikipedia also notes your blooper (refering to R ⊆ X × Y):

It is immediate that an arbitrary relation may contain pairs that
violate the necessary conditions for a function given above.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Also the word "functional" is used differently in wikipedia so that
it might also cover partial functions, i.e. when serial is missing.
Basically the EXISTUNIQUE quantifier is split up into, now doing

it class wise like Dan-O-Matik started doing it:

/* serial = existence */
ALL(a):[P(a) => EXIST(b):[Q(b) & F(a,b)]]

/* functional = uniqueness */
ALL(a):[P(a) => ALL(b):[Q(b) => ALL(c):[Q(c) => [F(a,b) & F(a,c) => b = c]]]]

Mostowski Collapse schrieb am Samstag, 4. Dezember 2021 um 13:12:25 UTC+1:
> Dan-O-Matik, your school skipper definition is not
> a correct definition. Your definition does not imply:
>
> ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)].
>
> Even the tree tool can find a counter example:
>
> ∀a(Pa → ∃b(Qb ∧ (Fab ∧ ∀c(Qc → (Fac → c=b))))) → ∀a∀b(Fab → (Pa ∧ Qb)) is invalid.
> Countermodel:
> Domain: { 0 }
> P: { }
> Q: { 0 }
> F: { (0,0) }
> https://www.umsu.de/trees
>
> Your easy definition is an easily wrong definition.
> Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 16:24:51 UTC+1:
> > See my reply just now to your identical posting at sci.logic
> >
> > Dan
> > On Friday, December 3, 2021 at 3:47:54 AM UTC-5, Mostowski Collapse wrote:
> > > Obviously Dan-O-Matik is impaired concerning beginners
> > > mathematics. For example lets use n for {0,1,2,..,n-1},
> > > then everybody knows that these to things are in bijection:
> > >

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

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor