[continued from previous message]   
      
   p_m, makes for an induction schema that now there are again   
   uncountably-many between 0 and 1, uncountably-many between those, and so   
   on, the double-reduction, so that "transfinite induction may not fail".   
   Then I suggest that since so many things in ZF depend on transfinite   
   induction, that showing that transfinite induction fails breaks ZF.   
   Then, I suggest that the existence of non-Cartesian functions, and the   
   countable continuous domain about [0,1], resolves this and keeps ZF from   
   breaking itself.   
      
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and test the double-reductio you   
   propose.   
   Claim (your words):   
   “Transfinite induction fails on the strictly decreasing ω₁-chain   
   0 < 1 < p_n < p_m (n < m < ω₁),   
   so ZF breaks, and the existence of non-Cartesian functions rescues ZF   
   from this contradiction.”   
   Formal check (three lines)   
      
   Such a chain does not exist.   
   ZF proves that every strictly decreasing sequence of reals has   
   order-type ≤ ω (because every bounded open interval contains a rational,   
   and ℚ is countable).   
   Hence no strictly decreasing ω₁-sequence—indeed no uncountable   
   well-ordered decreasing sequence—exists in any model of ZF.   
   Therefore transfinite induction never gets to ω₁ on such a chain; the   
   alleged failure is impossible, so ZF does not break.   
   Non-Cartesian functions (finite-range sets of pairs) do not rescue   
   anything; they simply live inside the countable world that ZF already   
   allows.   
      
   One-sentence encapsulation   
   The alleged contradiction is empty: the ω₁-chain does not exist, so   
   transfinite induction never fails, and ZF never breaks; Cantor’s lasso   
   catches nothing because nothing is in the arena.   
   Bottom line   
      
   “Double reductio” is fine prose, but formally the alleged object does   
   not exist inside any model of ZF.   
   Co-induction is only a description of a countable process; it never   
   reaches ω₁.   
   ZF remains intact; no rescue is required.   
      
   Ring when you have a ZF formula that allegedly defines a strictly   
   decreasing ω₁-sequence of reals—we will derive its non-existence in   
   three lines.   
      
      
      
   Thanks Kimi. Yes, I know that this line of argument, the transfinite   
   induction that there are uncountably-many numbers in an open internal   
   and every open sub-interval in natural order completes, is directly   
   contradicted since rationals are dense in the reals. Yet, there is no   
   member of the interval without uncountably-many neighbors, so   
   transfinite induction can't not complete, and a well-ordering exists in   
   theories like ZFC, where here we've been mostly talking about ZF. So,   
   that it is so and not so is inconsistent. The, "transfinite   
   co-induction", then, the double reduction, shows there's no case for   
   where the case is not so, thusly, at some point, _induction_ fails,   
   merely ordinary induction since the last limit ordinal, it fails, or ZF   
   is inconsistent.   
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and state the contradiction you   
   allege.   
   Claim (your words):   
   “ZF proves that every open interval contains uncountably-many reals in   
   natural order, yet transfinite induction (ordinary induction) must fail   
   at some limit ordinal, making ZF inconsistent.”   
   Formal check (three lines)   
      
   ZF does not prove that any open interval contains an uncountable   
   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   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)