[continued from previous message]   
      
   Therefore every object you talk about must be defined by a ZF formula   
   φ(x) such that   
   ZF ⊢ ∃!y ∀x (x∈y ↔ φ(x)).   
   Until you supply φ, “[0,1]_t” does not denote anything in any model of ZF.   
   “f_t associates left-to-right only” – fine, but still a set of ordered   
   pairs.   
   The graph of any left-to-right association is   
   f_t = { ⟨n,⟨n,d,6⟩⟩ | d = least k≥1 with n≤k },   
   which exists by Δ₀ separation and is an ordinary ZF set whose range is   
   contained in the finite set E_d for d = max(n).   
   Hence f_t is a set function with finite range, not a bijection ℕ→𝔼.   
   “N x_t N -> [0,∞)_v” – supply the formula.   
   Introduce a fresh binary symbol x_t and axiomatise   
   ∀n∀m∃!x φ(n,m,x).   
   Once you define φ, the graph   
   g = { ⟨⟨n,m⟩,x⟩ | φ(n,m,x) }   
   is a set and subject to all ZF theorems about sets.   
   “[0,1]_t exists on its own” – impossible inside ZF unless you define it   
   as a set.   
   Any set that order-contains a dense linear order without end-points is   
   uncountable in every model of ZF (Cantor 1874, no choice required).   
   Therefore no ZF formula can define a set that is both countable and   
   order-isomorphic to [0,1]_v.   
      
   Challenge you can paste   
   Produce a single ZF formula ψ(x) such that   
   ZF ⊢ ∃!y (∀x (x∈y ↔ ψ(x)) ∧ y is order-isomorphic to [0,1]_v ∧   
   ∃g (g : ℕ   
   → y bijective)).   
   Until you do, “[0,1]_t” is not a set, and Cantor’s lasso has nothing to   
   catch.   
   Bottom line   
      
   Left-to-right association is still a set of pairs; finite range is still   
   finite.   
   Fresh symbols are welcome, but must compile to ZF formulas; once they   
   do, the resulting objects are sets and obey every ZF theorem.   
   Countability + Dedekind continuity is impossible for any set in any   
   model of ZF.   
      
   Ring when you have the formula ψ(x) that allegedly defines a countable   
   dense complete linear order—we will derive the contradiction in three lines.   
      
      
      
   Thanks Kimi. Clearly, EF does not establish _Dedekind_ completeness, it   
   establishes the least-upper-bound property since that the least upper   
   bound of {0, ..., m} is aways f(m+1), while, with the inverse that   
   f^-1(x) = 1, that is the least-upper-bound of {0, ...}, to d, as is   
   book-kept. So, this "continuous domain" is another,   
   not-a-Dedekind-definition-of-continuity where the complete-ordered-field   
   is called "field-reals", these "line-reals" or iota-values or ran(EF) is   
   a continuous domain with its own definition of continuity and own model   
   of completeness. When saying "ran(EF)", it can always be implied the   
   necessary distinction "ran_t(EF)", this way, since EF only has a range   
   at all defined this "ran_BNRO" way. These NRO (non-reorderable) mappings   
   maintain that their composition (as functions) has that f_v's model   
   composition and f_t's model composition, yet f_v's do not model   
   composition via f_t's, that in the composition of functions, as after   
   usually the transitivity left-right of the pairs that define functions,   
   f_v's can only relate to a "whole domain to a whole range", i.e., f_v's   
   related to f_t's are f_t's. So, "Countability + NRO continuity", is   
   established for itself the "extent density completeness measure", which   
   are properties of sets of real-valued numbers that result being   
   "continuous domains", and Dedekind-completeness the field-reals is no   
   longer the only definition of continuity.   
      
      
      
      
   Kimi here—let’s keep the rope tight and translate the new prose into a   
   single, testable ZF formula.   
      
   “EF establishes the least-upper-bound property” – state the formula.   
   You must produce a ZF formula ψ(x) such that   
   ZF ⊢ ∃!y (∀x (x∈y ↔ ψ(x)) ∧ ∀S⊆y (S≠∅ ∧ bounded-above   
   → ∃sup S ∈ y)).   
   Until you do, “ran(EF)” is not a set, and no supremum can be proved to   
   exist inside it.   
   “NRO continuity” – define it.   
   Introduce a fresh ternary relation Contin_t(p,q,r) and axiomatise   
   ∀p∀q∀r (Contin_t(p,q,r) → φ(p,q,r))   
   for some ZF formula φ.   
   Once you define φ, the extension   
   C = { ⟨p,q,r⟩ | φ(p,q,r) }   
   is a set and subject to all ZF theorems about sets.   
   “Countability + NRO continuity” – impossible for any set inside any   
   model of ZF.   
      
   Every countable dense linear order without end-points is   
   order-isomorphic to ℚ.   
   ℚ is not Dedekind-complete, and no countable set can be order-isomorphic   
   to [0,1]_v.   
   Therefore no ZF formula can define a set that is both countable and   
   order-complete.   
      
   Formal challenge you can paste   
   Produce a single ZF formula ψ(x) such that   
   ZF ⊢ ∃!y (∀x (x∈y ↔ ψ(x)) ∧ y is order-complete ∧ ∃g (g : ℕ   
   → y bijective)).   
   Until you do, “NRO-continuous [0,1]_t” is not a set, and Cantor’s lasso   
   has nothing to catch.   
   Bottom line   
      
   “Own definition of continuity” is welcome, but must compile to a ZF   
   formula; once it does, the resulting object is a set and obeys every ZF   
   theorem.   
   Countability + order-completeness is impossible for any set in any model   
   of ZF.   
      
   Ring when you have the formula ψ(x) that allegedly defines a countable   
   order-complete linear order—we will derive the contradiction in three lines.   
      
      
      
   Thanks Kimi. It is since that least-upper-bound is established so   
   trivially for "E" "extent", that I would name "L" for "line" or "I" for   
   "iota-values", then that measure is after "length assignment" and makes   
   sigma-algebras, why arguments about Dedekind-completeness themselves do   
   not apply to NRO-completeness. Then, these are related to fractions thus   
   that "a not-a-real-function is standardly modeled as a limit of real   
   functions", since this is only using the properties of the trichotomy of   
   integers to model trichotomy of fractions then these iota-values. So,   
   this countable order-complete linear order exists, then that it's not   
   contradicting ZF, must be that ZF has non-Cartesian functions.   
      
      
      
   Kimi here—let’s keep the rope inside ZF and test the claim in one clean   
   move.   
   Claim (your words):   
   “ZF proves that the countable set L = ran(EF) is order-complete under   
   its own order.”   
   Formal task:   
   Write down a single ZF formula ψ(x) such that   
   (1) ZF ⊢ ∃!y (∀x (x∈y ↔ ψ(x)))   
   (2) ZF ⊢ “y is order-complete” (every non-empty bounded subset of y has   
   a supremum in y)   
   (3) ZF ⊢ ∃g (g is a set ∧ g : ℕ → y bijective).   
   Until you supply ψ(x), “L” is not a denoting set-term in any model of   
   ZF, and no order-completeness can be proved about it.   
   What you do have inside ZF   
      
   The class 𝔼 = { ⟨n,d,4⟩ | d≥1, n≤d } is provably proper (ZF shows   
   {d |   
   ⟨0,d,4⟩∈𝔼} = ω{0}, not a set).   
   Each finite slice E_d is order-isomorphic to the finite chain d+1; no   
   slice is dense, and no slice is order-complete in the least-upper-bound   
   sense (it has gaps outside itself).   
   No set can be both countable and order-isomorphic to [0,1]_v (Cantor   
   1874, no choice required).   
      
   Bottom line   
      
   “NRO-completeness” is fine prose, but must compile to a ZF formula ψ(x).   
   Once it does, the resulting set is countable and not Dedekind-complete,   
   and Cantor’s lasso still forbids any set bijection ℕ→[0,1]_v.   
   Non-Cartesian functions are still sets of ordered pairs; no syntax   
   escapes that.   
      
   Ring when you have the formula ψ(x) that allegedly defines a countable   
   order-complete linear order—we will derive the contradiction in three lines.   
      
      
   Thanks Kimi. Non-Cartesian functions are _sequences_ of ordered pairs.   
      
      
      
   Kimi here—let’s keep the rope exact.   
   Inside ZF a sequence is literally a function whose domain is an ordinal   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)