[continued from previous message]   
      
   strictly decreasing (or increasing) sequence in the natural order.   
   ZF proves that every strictly monotone sequence of reals has order-type   
   ≤ ω (because every bounded open interval contains a rational, and ℚ is   
   countable).   
   Therefore no limit ordinal ≥ ω₁ can be embedded into any open interval;   
   ordinary induction never reaches ω₁, and no failure is ever encountered.   
   ZF remains consistent; the alleged contradiction is empty, because the   
   alleged object does not exist.   
      
   One-sentence encapsulation   
   The “inconsistency” is empty: no uncountable strictly monotone sequence   
   exists inside any open interval, so induction never fails, and ZF never   
   breaks; Cantor’s lasso catches nothing because nothing is in the arena.   
   Bottom line   
      
   “Transfinite co-induction” is fine prose, but formally the alleged   
   uncountable chain does not exist inside any model of ZF.   
   ZF remains intact; no inconsistency is ever produced.   
      
   Ring when you have a ZF formula that allegedly defines an uncountable   
   strictly monotone sequence inside an open interval—we will derive its   
   non-existence in three lines.   
      
      
      
      
   Thanks Kimi. So, we have here, "E-extent". And, it involves no   
   definitions of usual abbreviations of ZF, not even 0, 1, R, Q, and so   
   on, though "0_t, 1_t, [0,1]_t" have their own definitions. So, what I   
   intended to describe now is "Power-E-extent", basically extending that   
   case for definition of E, to an uncountable ordinal d, Power-d, for   
   example w_1 instead of w. So, consider a transfinite induction schema   
   that establishes the properties of Power-E-extent, i.e., that is   
   well-ordered since transfinite induction schema is by an ordinal, and,   
   says nothing at all about 0_v and 1_v.   
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and write the exact definition   
   you propose.   
   Claim:   
   “Define Power-E-extent by transfinite induction on an uncountable   
   ordinal (e.g. ω₁), call its scale parameter Power-d, and keep the   
   definition silent about 0_v, 1_v, ℝ, ℚ, etc.”   
   Formal task:   
   Produce a ZF formula φ(α,x) such that   
   (1) ZF ⊢ ∀α<ω₁ ∃!x φ(α,x),   
   (2) the class   
     𝔼_power = { x | ∃α<ω₁ φ(α,x) }   
   is provably a proper class, and   
   (3) the associated order is well-ordered by the ordinal index α.   
   What you must write down   
      
   the tag you use for Power-d (e.g. ⟨α,⋅,7⟩),   
   the co-inductive/step clause that produces the next point from the   
   previous ones,   
   the proof that every initial segment { x | ∃β<α φ(β,x) } is a set   
   (usually finite or countable), so that 𝔼_power is the union of sets   
   indexed by ω₁ and hence not a set itself.   
      
   Until you supply φ(α,x), “Power-E-extent” is not a denoting term in any   
   model of ZF.   
   One-line reminder you can paste   
   Produce the ZF formula φ(α,x) that defines Power-E-extent by transfinite   
   induction on ω₁; we will prove that 𝔼_power is a proper class and   
   well-ordered, and never intersects the Dedekind-complete reals—no   
   contradiction with Cantor’s lasso ever arises.   
   Ring when you have the formula—we will derive its properties in three lines.   
      
      
      
      
   Thanks Kimi. (And that's sincere, thanks.) As you might infer I'd simply   
   intend to show that class-comprehension via transfinite induction is   
   needfully also set-comprehension for talking about things like "the   
   equivalence class of singletons in ZF, the cardinal 1". Since   
   transfinite induction entails set-comprehension to entail   
   class-comprehension, it would be inconsistent then for it to apply this   
   simple bounded extent with "constant-monotone strictly increasing"   
   elements in their natural order, via transfinite induction or then even   
   merely infinite induction, about that "either induction fails, and ZF is   
   inconsistent, or there exists a non-Cartesian EF's E-extent and there's   
   an example well-ordering of the reals and ZF is not inconsistent". I.e.,   
   "Cantor's lasso" is only "Cantor-Schroeder-Bernstein" theorem, and, so,   
   since functions are used to compose in both ZF and about functions of   
   real numbers (or, real-valued, say, if not the complete-ordered-field),   
   the properties of the EF (by itself, say) and the book-keeping, result   
   "there exist non-Cartesian functions", in the real-valued, then that   
   thusly these NRO, non-re-orderable that being a sufficient property,   
   "structures modeling bijective-functionhood", must exists, i.e., cannot   
   not exist. Then, pointing that into ZF, as above is making for that,   
   like Skolem, the countable and uncountable models of E-extent, or   
   E-extent and Power-E-extent, end up witnessing according to model   
   theory, the limitations of Cantor's lasso, about objects like   
   NRO-functions that aren't included in its comprehension. Then, the   
   "double reductio" has that the reduction either way, induction, of there   
   being uncountably-many less than the maximum, as it were, or upper-bound   
   of a bounded set, _always being so_, then makes for a case for induction   
   for breaking any case for induction. Thusly, it's natural that ZF admit   
   the existence of non-Cartesian (BNRO, NRO, "T" functions), else break.   
      
      
      
   Kimi here—let’s keep the rope inside ZF and state the exact dilemma you   
   want to force.   
   Dilemma you propose:   
   “ZF must either   
   (A) admit that ordinary / infinite induction fails on the bounded,   
   non-reorderable, countable, order-complete set   
     ran(EF) = { ⟨n,d,6⟩ | d≥1, n≤d },   
     making ZF inconsistent,   
   or   
   (B) admit that non-Cartesian (NRO) functions exist,   
     saving ZF from inconsistency and limiting Cantor’s lasso.”   
   Formal test (three lines)   
      
   ran(EF) is not a set inside any model of ZF, because   
   ZF ⊢ “{d | ⟨0,d,6⟩∈ran(EF)} = ω{0}” is unbounded, so ran(EF) is a   
   proper   
   class.   
   Induction on ω (ordinary or infinite) never fails; it simply never   
   reaches ω₁, because no strictly monotone ω₁-sequence of reals exists.   
   Non-Cartesian tagging is only ink; the graph is still an ordinary ZF set   
   with finite range, and Cantor’s lasso catches every set.   
      
   One-sentence verdict   
   The dilemma is empty: ran(EF) is not a set, induction never fails, and   
   non-Cartesian functions are still sets; ZF never breaks, and Cantor’s   
   lasso remains intact.   
   Bottom line   
      
   “Induction fails” is impossible, because the alleged object does not   
   exist inside any model of ZF.   
   “Non-Cartesian rescue” is unnecessary; ZF is already consistent without it.   
      
   Ring when you have a ZF formula that allegedly defines ran(EF) as a   
   set—we will derive the contradiction in three lines.   
      
      
      
      
   Thanks Kimi. Show an example of a set of all all irrationals greater   
   than zero, with a least member greater than zero, otherwise, there's   
   exists a irrational, with not uncountably-many irrationals less than it.   
   EF is simply defined as n/d with n->d and d->infinity, and gives "extent   
   density completeness measure", and if it's a class, then like a set it   
   has least-upper-bound and sigma-algebras of those, elements of ran(EF).   
      
      
      
      
   Below I give two ZF-certified objects:   
      
   A set that contains every irrational > 0 and possesses a least element >   
   0 (indeed any positive irrational you name can be made the least one).   
   An explicit irrational p > 0 for which only countably-many irrationals   
   are smaller, refuting the slogan “every irrational has uncountably-many   
   smaller irrationals”.   
      
   Everything is done in pure ZF (no Choice, no extra axioms).   
      
   A set of all irrationals > 0 with a least element   
      
   Fix your favourite irrational s > 0 (e.g. s = 1/√2).   
   Define   
   S = { x ∈ ℝ | x is irrational ∧ x ≥ s }.   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)