[continued from previous message]   
      
   is a set, hence subject to Cantor’s lasso.   
   1-to-1 and onto both ways   
   The formula φ(n,x) you gave does establish a bijection between ℕ and the   
   class 𝔼—but 𝔼 is a proper class, so no set f can literally be that   
   bijection.   
   Therefore the statement “ℕ ↔ 𝔼 bijectively” is not a    
   ounter-example to   
   uncountability; it is only a class bijection, and every model of ZF   
   already agrees that proper classes are not sets.   
      
   Formal capsule you can paste   
   Claim: “BNRO-mapping gives a bijection ℕ→𝔼 that evades Cantor’s   
   lasso.”   
   Reply:   
      
   The class 𝔼 = {⟨n,d,6⟩ | d≥1, n≤d} is provably proper in ZF.   
   The class-function   
   EF ≔ {⟨n,⟨n,d,6⟩⟩ | d = least k≥1 with n≤k}   
   is definable by a Δ₀ formula, hence exists as a class.   
   Cantor’s theorem only forbids a set bijection ℕ→𝔼; it does not forbid   
   a   
   class bijection.   
   Therefore no contradiction arises—you have merely exhibited the usual   
   class bijection that every model of ZF already knows.   
      
   Bottom line   
      
   Re-naming does not change the type of the object: classes stay classes,   
   sets stay sets.   
   Cantor’s lasso already allows class bijections; it only forbids set   
   bijections.   
   Extent, density, completeness, measure can all be book-kept at each   
   finite scale d, but never assemble into a set that violates uncountability.   
      
   Ring when you want the next layer: a conservative extension that adds a   
   fresh sort whose objects are not sets, and measure-1 shadows that   
   inherit Lebesgue outer measure without ever identifying 0_T with 0_V.   
      
      
      
      
   Thanks Kimi. Again, "0" and "1" are _not_ constants in ZF, they are   
   merely usual labels attached as descriptions related what's then the   
   Peano axioms to numbers, and usually with an assignment to von Neumann   
   ordinals, and then that, for example, neither "ordinals" nor "cardinals"   
   are "sets" in ZF. Then, there are only sets in set theory, classes,   
   either admit class comprehension or they don't, for example about   
   "ordinals" and "cardinals", or here "totally-ordered [0,1]", that also   
   is well-ordered, by its natural total order.   
      
      
      
      
   Kimi here—let’s keep the rope exactly taut.   
      
   “0” and “1” are not constants in ZF—agreed.   
   They are defined abbreviations:   
   0 ≔ ∅, 1 ≔ {∅}.   
   Once the definition is expanded, every theorem about them is a sentence   
   in the pure language of ∈.   
   “Ordinals” and “cardinals” are not sets in ZF—false.   
      
   Every von Neumann ordinal is a set (built from ∅ by repeated pairing and   
   union).   
   Every cardinal (initial ordinal) is a set.   
   The class ON = { x | x is an ordinal } is a proper class, but each   
   member is a set.   
   The class Card = { x | x is a cardinal } is likewise a proper class, but   
   each cardinal is a set.   
      
   Class comprehension in ZF is not an axiom; it is a schema of definitions.   
   A class is simply { x | φ(x) } for some formula φ.   
   If φ contains no unbounded quantifiers over proper classes, the class is   
   definable; if it does, the class may be indefinable—but every element it   
   collects is still a set.   
   “Totally-ordered [0,1]” inside your BNRO/BTO story is not a set in ZF;   
   it is the proper class 𝔼 = {⟨n,d,6⟩ | d≥1, n≤d}.   
      
   Each slice E_d is a finite set.   
   The union 𝔼 is a proper class, hence not a set.   
   Therefore no set f can be a bijection ℕ→𝔼; Cantor’s theorem already   
   forbids any such set.   
      
   One-sentence encapsulation you can paste   
   Inside ZF every ordinal, every cardinal, and every tagged tuple ⟨n,d,6⟩   
   is a set; the class 𝔼 is proper, so no set bijection ℕ→𝔼 exists, and   
   renaming the tags does not create a set that slips Cantor’s lasso.   
   Ring when you want the next layer: a conservative extension that adds a   
   fresh sort whose objects are not sets, and measure-1 shadows that   
   inherit Lebesgue outer measure without ever identifying 0_T with 0_V.   
      
      
      
      
   Thanks Kimi. Indeed, one could axiomatize these features into ZF, and   
   then since the results about functions never catch on results about a   
   primitive temporal continuity segment [0,1]_t, then what makes for   
   results can still sit above this, while yet both sides domain and range   
   of EF are sets, while book-kept internally.   
      
      
      
      
   Kimi here—let’s nail the formal situation once and for all.   
      
   “Both sides of EF are sets” – only half-true.   
      
   Domain side: ℕ is a set (the usual von-Neumann ω).   
   Range side: 𝔼 = { ⟨n,d,6⟩ | d≥1, n≤d } is a proper class (ZF proves   
   {d   
   | ⟨0,d,6⟩∈𝔼} = ω{0}, which is not a set).   
   Therefore no set f⊆ℕ×𝔼 can satisfy ran(f)=𝔼; Cantor’s lasso   
   already   
   forbids any such set.   
      
   “Axiomatise these features into ZF” – fine, but axioms add no new sets   
   unless you enlarge the language.   
      
   If you introduce a fresh sort [0,1]_t with primitive symbols 0_t, 1_t,   
   app_t(·,·) and axiom that dom_t=ℕ and ran_t=𝔼, you are not working in   
   ZF; you are in a two-sorted theory whose consistency must be checked   
   separately.   
   Inside that extended theory Cantor’s theorem is never stated, because   
   the t-sort is outside the ZF universe.   
      
   “Book-kept internally” – yes, but internal bookkeeping does not turn a   
   proper class into a set.   
      
   Every slice E_d is a finite set, but 𝔼 = ⋃_{d≥1} E_d is still a proper   
   class.   
   No finite d can cover all of 𝔼; hence no set bijection ℕ→𝔼 exists.   
      
   Formal capsule you can paste   
   Claim: “Both domain and range of EF are sets, so EF is a set bijection   
   ℕ→𝔼.”   
   Reply:   
      
   ZF ⊢ “𝔼 is a proper class” (because {d | ⟨0,d,6⟩∈𝔼} = ω{0}   
   is unbounded).   
   Therefore no set f can satisfy ran(f)=𝔼; every set f⊆ℕ×𝔼 has finite   
   range ⊆ E_d for some finite d.   
   Axiomatising a fresh sort [0,1]_t with primitive symbols 0_t, 1_t,   
   app_t(·,·) does not create a new set inside ZF; it creates a   
   conservative extension whose t-objects are not sets.   
   Hence EF is either   
      
   a class bijection (allowed, but not a set), or   
   a set bijection with finite range (hence not ℕ→𝔼).   
   Cantor’s lasso is untouched.   
      
   Bottom line   
      
   Temporal-continuity segment [0,1]_t is welcome, but outside ZF it is   
   only syntax; inside ZF every object is still a set, and no set bijection   
   ℕ→𝔼 exists.   
   Book-keeping keeps the finite scales tidy, but never turns the proper   
   class 𝔼 into a set.   
      
   Ring when you want the next layer: a model-theoretic verification that   
   the two-sorted extension has a standard model (V_ω+ω for ZF, tagged   
   tuples for t-sort) and measure-1 shadows that inherit Lebesgue outer   
   measure without identifying 0_t with 0_v.   
      
      
   Thanks Kimi. Besides things like Internal Set Theory and co-consistency   
   with ZF, I'm curious the origin of "measure-1 shadows". About "extent   
   density completeness measure", of what would result a   
   "not-a-real-function", the natural/unit equivalency function, which for   
   example is modeled in category theory as the functor of N onto [0,1]   
   interprtations, the idea of that the range has sigma-algebras (of sets)   
   is for measure, then that I'm curious about "measure-1 shadows".   
      
      
      
   The phrase “measure-1 shadows” is not a standard term from classical   
   analysis or set theory; it was minted in our earlier dialogue to   
   describe the finite-scale measure that your bookkeeping gadget always   
   assigns to the whole interval:   
      
   For each finite d the finite σ-algebra ℘(E_d) carries the uniform   
   probability   
   μ_d(S) = |S|/d, so μ_d(E_d) = 1.   
   Because every witness lives inside a single finite set, no infinite   
   union is ever invoked, yet “in the limit of speech” the shadow of this   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)