Thread by @gro_tsen

OK, I may be guilty of a DoS attack attempt on mathematicians' brains here, so lest anyone waste too much precious brain time decoding this deliberately cryptic statement, let me do it for you. •1/15

https://twitter.com/gro_tsen/status/1360232307983056907

First, as some asked, it is to be parenthesized as: “∀x.∀y.((∀z.((z∈x) ⇒ (((∀t.((t∈x) ⇒ ((t∈z) ⇒ (t∈y))))) ⇒ (z∈y)))) ⇒ (∀z.((z∈x) ⇒ (z∈y))))” (the convention is that ‘⇒’ is right-associative: “P⇒Q⇒R” means “P⇒(Q⇒R)”), but this doesn't clarify much. •2/15

Maybe we can make it a tad less abstruse by using guarded quantifiers (“∀u∈x.(…)” stands for “∀u.((u∈x)⇒(…))”): it is then “∀x.∀y.((∀z∈x.(((∀t∈x.((t∈z) ⇒ (t∈y)))) ⇒ (z∈y))) ⇒ (∀z∈x.(z∈y)))”. •3/15

Maybe a tad clearer again by writing “P(u)” for “u∈y” and leaving out the quantifier on y, viꝫ: “∀x.((∀z∈x.(((∀t∈x.((t∈z) ⇒ P(t)))) ⇒ P(z))) ⇒ (∀z∈x.P(z)))” [✯]. Now it appears as an induction principle: namely, … •4/15

… “in order to prove P(z) for all z∈x, we can assume, when proving P(z), that P(t) is already known for all t∈z∩x” (n.b.: “(∀z.(Q(z)⇒P(z)))⇒(∀z.P(z))” can be read “in order to prove P(z) for all z, we can assume Q(z) known when proving P(z)”). •5/15

This is a principle known as “∈-induction”: it is perhaps clearer when not guarded by x, “((∀z.(((∀t.((t∈z) ⇒ P(t)))) ⇒ P(z))) ⇒ (∀z.P(z)))” [✵], viꝫ “in order to prove P(z) for all z, we can assume, when proving P(z), that P(t) is already known for all t∈z”, … •6/15

… but of course the guarded version [✯] can be deduced from the unguarded [✵] by applying it to (z∈x)⇒P(z) in lieu of P(z). This is a particular case of “well-founded induction”, and the crucial point is that the “∈” relation on sets is indeed well-founded: … •7/15

… this follows (classically) from the axiom of Regularity, one of whose formulations is “∀v.((v≠∅) ⇒ (∃z∈v.(z∩v=∅))))” (“every set v has an element z which is disjoint from it”), or equivalently, “∀v.((∀z∈v.(z∩v≠∅))) ⇒ (v=∅))”: … •8/15

… from this we can easily deduce [✯] above by applying the axiom to v := {z∈x | ¬P(x)}, giving “∀x.((∀z∈x.(¬P(z) ⇒ ∃t∈x.((t∈z)∧¬P(t))))) ⇒ (¬∃z∈x.¬P(z)))” or, after a easy logical manipulations (taking contrapositives and moving negations around), … •9/15

… “∀x.((∀z∈x.(((∀t∈x.((t∈z) ⇒ P(t)))) ⇒ P(z))) ⇒ (∀z∈x.P(z)))” as claimed (and, as explained earlier, the original statement then follows by applying this to “z∈y” in lieu of P(z), or, if we prefer, v := x∖y in the axiom of Regularity). •10/15

(Actually, the unguarded statement “((∀z.(((∀t.((t∈z) ⇒ P(t)))) ⇒ P(z))) ⇒ (∀z.P(z)))” [✵] also follows, but there is a little more work here, essentially constructing the transitive closure, requiring a more set-theoretic power than I have used hitherto. … •11/15

… Conversely, this statement [✵] easily implies the axiom of Regularity by applying it to “z∉v” in lieu of P(z). So all are, in fact, equivalent over a reasonable set theory in classical logic. … •12/15

… But when working in intuitionistic logic it is more reasonable to work with induction principles such as [✵], which don't require moving negations around. Anyway, even classically, Regularity is mostly used for ∈-induction.) •13/15

So anyway, my original statement, “∀x.∀y.((∀z.((z∈x) ⇒ ((∀t.((t∈x) ⇒ (t∈z) ⇒ (t∈y)))) ⇒ (z∈y))) ⇒ (∀z.((z∈x) ⇒ (z∈y))))” was essentially a (perhaps better) rephrasing of the axiom of Regularity (and equivalent to it over the rest of ZF). •14/15

It's a bit recondite, but I think, as a formula, it has a certain gnomic beauty to it — almost poetry, I might say: this is the reason I left “∀z.((z∈x) ⇒ (z∈y)))” as such and not as “x⊆y”: it would spoil the rhyme. 🧐 •15/15