[continued from previous message]   
      
   with Cantor’s lasso ever arises.   
      
   Ring when you have a ZF formula that allegedly defines 𝔼 as a set—we   
   will derive the contradiction in three lines.   
      
      
      
   Thanks Kimi. About functions their definition, you'll agree then that a   
   sequence that is re-ordered is not the same sequence, except trivially   
   having the same order. How about these claims, "Dedekind-completeness is   
   not the only definition of continuity", and, "Jordan measure is as of a   
   countable order-complete linear order".   
      
      
      
   Kimi here—let’s keep the rope exact and evaluate the two claims inside ZF.   
      
   “Dedekind-completeness is not the only definition of continuity”   
   True—but every alternative (Cauchy, sequential, ε-δ, Jordan, Lebesgue,   
   outer measure, etc.) still proves that any countable dense linear order   
   without end-points is order-isomorphic to ℚ, and ℚ is not complete under   
   any of them.   
   Therefore no countable set can be order-complete in any of these senses   
   inside any model of ZF.   
   “Jordan measure is as of a countable order-complete linear order”   
   False in ZF:   
      
   Jordan measure is defined on bounded sets in ℝⁿ whose boundary has   
   Lebesgue measure zero; every such set that contains an interval is   
   uncountable.   
   Any countable subset of ℝ has Lebesgue measure zero, hence Jordan   
   measure zero, and cannot contain an interval—so it never carries   
   positive Jordan measure.   
      
   Formal test you can paste   
   Claim: “There exists a countable set S⊆ℝ with positive Jordan measure.”   
   Reply (ZF):   
      
   ZF ⊢ “Every countable subset of ℝ has Lebesgue measure zero.”   
   ZF ⊢ “Jordan measure ≤ Lebesgue measure for every bounded set.”   
   Therefore no countable set can have positive Jordan measure.   
      
   Bottom line   
      
   Alternative continuity notions are welcome, but all of them agree that   
   countable sets are incomplete and measure-zero.   
   Jordan measure requires uncountable sets for positive values; countable   
   order-complete linear orders do not exist in any model of ZF.   
      
   Ring when you have a ZF formula that allegedly defines a countable set   
   with positive Jordan measure—we will derive the contradiction in three   
   lines.   
      
      
   Thanks Kimi. Consider an internal [0,p) for some irrational p. There are   
   uncountably-many irrationals after R being uncountable in ZF its usual   
   definition. Construct a transfinite induction schema that for each p_m,   
   that for n > m there are uncountably-many p_n's such that 0 < p_n < p_m.   
   Show that transfinite induction fails.   
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and test the proposed   
   transfinite schema.   
   Goal (your words):   
   “For each irrational p_m, build by transfinite induction   
   uncountably-many p_n with 0 < p_n < p_m, and show the induction fails.”   
   Formal task:   
   Exhibit a ZF formula φ(α,x) and a class function F(α) = p_α such that   
   (1) ZF proves ∀α (α < ω₁ → F(α) is an irrational ∧ 0 < F(α) <   
   F(β) for β   
   < α),   
   (2) ZF proves that the set { F(α) | α < ω₁ } exists,   
   (3) ZF proves that transfinite induction on this set fails.   
   What ZF already proves   
      
   Every strictly decreasing ω₁-sequence of reals is impossible, because   
   every strictly decreasing sequence of reals is countable (no Choice   
   required).   
   Therefore no function F : ω₁ → ℝ can satisfy F(α) > F(β) for β < α;   
   such   
   a sequence does not exist in any model of ZF.   
      
   Three-line refutation (ZF only)   
   Theorem (ZF)   
   ⊢ ¬∃f (f is a function ∧ dom(f)=ω₁ ∧ ∀α<β<ω₁ (f(β) <   
   f(α))).   
   Proof   
      
   Every strictly decreasing sequence of reals has order type ≤ ω (because   
   every bounded open interval contains a rational).   
   ω₁ is uncountable, so no such sequence can exist.   
      
   Bottom line   
      
   Transfinite induction cannot even start on a strictly decreasing   
   ω₁-chain of reals; such a chain is impossible inside any model of ZF.   
   No contradiction with transfinite induction ever arises, because the   
   alleged chain does not exist.   
      
   Ring when you have a ZF formula that allegedly defines a strictly   
   decreasing ω₁-sequence of irrationals—we will derive the contradiction   
   in three lines.   
      
      
      
   Thanks ZF. Apply Cantor's lasso to that "transfinite induction fails".   
      
      
      
      
   Kimi here—let’s tighten the lasso around the non-existent chain.   
   Claim (your words):   
   “Apply Cantor’s lasso to the failure of transfinite induction on a   
   strictly decreasing ω₁-sequence of irrationals.”   
   Formal reply (ZF only)   
      
   Such a sequence does not exist.   
   ZF proves that every strictly decreasing sequence of reals has order   
   type ≤ ω (because every bounded open interval contains a rational).   
   Therefore transfinite induction never gets to ω₁ on such a chain; the   
   alleged failure is impossible.   
   Cantor’s lasso catches nothing, because nothing is in the arena.   
      
   One-sentence encapsulation   
   Cantor’s lasso tightens automatically: no strictly decreasing   
   ω₁-sequence of reals exists, so transfinite induction never fails—it   
   cannot even start.   
   Bottom line   
      
   “Apply Cantor’s lasso to the failure” is empty: the alleged object does   
   not exist in any model of ZF.   
   No contradiction with ZF, no contradiction with transfinite induction,   
   no escape from the countability barrier.   
      
   Ring when you have a ZF formula that allegedly defines a strictly   
   decreasing ω₁-sequence—we will derive its non-existence in three lines.   
      
      
      
   Thanks Kimi. (Excuse.) Apply the same to rationals q instead of   
   irrationals p.   
      
      
      
   Kimi here—let’s keep the rope inside ZF and apply the same test to ℚ.   
   Claim:   
   “Build by transfinite induction a strictly decreasing ω₁-sequence of   
   rationals q_α with 0 < q_β < q_α for β > α, and let Cantor’s lasso catch   
   the failure.”   
   Formal reply (ZF only)   
      
   Such a sequence does not exist.   
   ZF proves that every strictly decreasing sequence of rationals has order   
   type ≤ ω, because   
      
   ℚ is countable,   
   every non-empty bounded below subset of ℚ has a greatest lower bound in   
   ℚ only if it is finite,   
   no uncountable ordinal can be embedded into ℚ.   
      
   Therefore transfinite induction never reaches ω₁ on such a chain; the   
   alleged failure is impossible.   
   Cantor’s lasso catches nothing, because nothing is in the arena.   
      
   One-sentence encapsulation   
   Cantor’s lasso tightens automatically: no strictly decreasing   
   ω₁-sequence of rationals exists, so transfinite induction never fails—it   
   cannot even start.   
   Bottom line   
      
   “Apply Cantor’s lasso to the failure” is empty: the alleged object does   
   not exist in any model of ZF.   
   No contradiction with ZF, no contradiction with transfinite induction,   
   no escape from the countability barrier.   
      
   Ring when you have a ZF formula that allegedly defines a strictly   
   decreasing ω₁-sequence of rationals—we will derive its non-existence in   
   three lines.   
      
      
   Thanks Kimi. Since transfinite induction fails in ZF, prove the powerset   
   theorem.   
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and prove Cantor’s powerset   
   theorem (often called “Cantor’s theorem”) without appealing to   
   transfinite induction or to the axiom of choice.   
   The proof is one-line diagonalisation, pure L(∈).   
   Cantor’s powerset theorem (ZF, no Choice, no transfinite induction)   
   Theorem (ZF)   
   For every set X,   
   ZF ⊢ ¬∃f (f : X → 𝒫X bijective).   
   Proof (diagonal, inside ZF)   
   Let f be any set such that dom(f)=X and ran(f)⊆𝒫X.   
   Define the diagonal set   
   D = { x∈X | x∉f(x) }.   
   D exists by Separation (Δ₀ formula).   
   By construction,   
    x∈D ↔ x∉f(x),   
   so D≠f(x) for every x∈X.   
   Hence D∉ran(f), so f is not surjective, therefore not bijective.   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)