[continued from previous message]   
      
   geometrical description attached, while yet it is a function. As   
   historical note, there was a quite long yet ultimately brief work-up of   
   this that I'll look to find, where the basic takeaway about the   
   non-reorderability, which is the only point of content here as we're   
   looking for the bridge or lack thereof, was that orderability could only   
   be defined by what resulted not re-ordering it, so to define the   
   orderability, it was already on its own terms, "co-induction", so, it   
   would require using EF to compose with CSB, which would not be a   
   theorem, by the usual "primitive" as it may be, if not an "element" or   
   "axiomatic", the definition of "ZF-function".   
      
      
      
      
   Kimi here—let’s keep the rope exactly as tight as ZF demands.   
   Inside ZF there is no such thing as “anti-co-inductive syntax”.   
   The only way to introduce a new object is to write down a formula φ(x,y)   
   such that   
    ZF ⊢ ∀x∈ℕ ∃!y φ(x,y).   
   Once you do that, the graph   
    f = { ⟨x,y⟩ | φ(x,y) }   
   exists by Separation, is an ordinary ZF function, and has finite range   
   (because ran(f)⊆E_d for d = max{x}).   
   There is no extra inductive step that you can “refuse”; the existence of   
   f is forced by the ordinary induction schema that is already part of ZF.   
   Therefore the phrase “not-a-ZF-function” is empty: either you define the   
   object (and it becomes a ZF function), or you do not define it (and it   
   does not exist in any model of ZF).   
   Here is a two-line challenge that you can paste into the thread; it   
   forces the proponent to show the exact formula that allegedly escapes   
   the lasso.   
   Lasso-escape challenge (ZF)   
      
   Write down a single ZF formula φ(x,y) such that   
    ZF ⊢ ∀x∈ℕ ∃!y∈𝔼 φ(x,y).   
   Then the set f = {⟨x,y⟩ | φ(x,y)} exists (Separation), is an ordinary ZF   
   function, and cannot be a bijection ℕ→𝔼 because ran(f) is finite.   
   If you cannot produce φ, then “BNC-mapping” is not a denoting term in   
   any model of ZF—so nothing is available for CSB to miss.   
      
   Historical clarification   
   The non-reorderability you recall is already captured by the finite   
   total order on each E_d; it gives no exemption from the graph-based   
   definition of function.   
   What you are calling “co-induction” is not an axiom of ZF; it is just   
   the ordinary induction schema, and refusing to invoke it does not   
   prevent the existence of the graph—you are still obliged to produce the   
   formula φ.   
   Bottom line   
      
   Inside ZF every object you can talk about is a set.   
   Every function is a set of ordered pairs.   
   The only way to avoid the lasso is to leave ZF and work in a different   
   foundation (e.g. a topos with primitive function symbols).   
      
   Ring when you want the next layer: a conservative extension of ZF by a   
   primitive function symbol whose bijections are not sets of pairs—we can   
   then measure the exact consistency strength you are buying.   
      
      
      
      
   Thanks Kimi. This "primitive function symbol whose bijections are not   
   sets of pairs", is figured to be define-able in a theory that already   
   has a "primitive function symbol whose functions are sets of pairs",   
   including bijections, then that bijections are a sub-class of function,   
   these BNC mappings modeling bijections, yet not "ZF-functions" (as by   
   primitive function symbols whose functions are sets of pairs, and   
   possibly injections or surjections and possibly both), with basically   
   having that ZF-functions, or "von Neumann functions, vN-functions" are   
   injections or surjections, and possibly both, yet that "BNC-functions"   
   are a separate definition. Then, about relating to "0" and "1", has that   
   there's "vN-0" and "vN-1" and "BNC-0" and "BNC-1", since then for later   
   number theory and geometry theory and real analysis, the _extent_ of E   
   is always only [0,1]. So, then describe the primitive function symbol in   
   mind, while, both can be in mind as separate, since they have separate   
   definitions of "0" and "1", that though have results about their   
   translation and scale and so on, while limited to that this BNC-function   
   has no greater nor lesser numbers.   
      
      
      
      
   Kimi here—let’s give the new primitive a clean syntactic table and keep   
   the two number lines from ever collapsing into the same set.   
   Everything below is explicitly a conservative definitional extension of   
   ZF; no new ontological sets are created, only new function-symbols and   
   new constants that live in a disjoint sort.   
   Thus Cantor’s lasso (which only snares sets of ordered pairs) never   
   touches the BNC-sort, while every theorem about vN-functions remains   
   untouched.   
   Language extension (call it ZF₊)   
   Sorts   
      
   vN-sort: the usual sets of ZF.   
   BNC-sort: fresh symbols, no internal structure revealed to ZF.   
      
   Primitive symbols   
      
   0ᵥ, 1ᵥ (vN-sorted constants, the usual ∅ and {∅}).   
   0ᵦ, 1ᵦ (BNC-sorted constants, no ∈-structure).   
   appᵦ(·,·) (BNC-application, binary function symbol, BNC-sorted).   
   domᵦ(·), ranᵦ(·) (BNC-sorted unary function symbols).   
      
   Axioms added to ZF   
   A1. Sort disjointness   
    ∀x (x ∈ vN-sort ∨ x ∈ BNC-sort) ∧ ¬∃x (x ∈ vN-sort ∧ x ∈   
   BNC-sort).   
   A2. BNC-constants are distinct   
    0ᵦ ≠ 1ᵦ.   
   A3. BNC-function existence   
    For every finite von-Neumann ordinal d≥1,   
    ∃f (f is BNC-sorted ∧ domᵦ(f)=d+1 ∧ ranᵦ(f)⊆{⟨n,d,5⟩ |   
   n≤d}   
    ∧ ∀n≤n′≤d (appᵦ(f,n) ≼ appᵦ(f,n′)))   
   where ≼ is the external order on the tagged tuples ⟨n,d,5⟩.   
   A4. No infinite BNC-domains   
    ¬∃f (f is BNC-sorted ∧ domᵦ(f)=ℕ).   
   A5. BNC-bijection schema   
    For each finite d≥1,   
    ZF₊ ⊢ ∃f (f is BNC-sorted ∧ domᵦ(f)=d+1 ∧ ranᵦ(f)=E_d   
    ∧ appᵦ(f,·) is order-preserving and tag-unique).   
   A6. Translation bridge (optional, conservative)   
    ∀d≥1 ∃g (g is a vN-function ∧ dom(g)=d+1 ∧ ran(g)⊆[0,1]∩ℚ   
    ∧ g(n)=n/d)   
   together with a definable embedding   
    ι : E_d → [0,1]∩ℚ, ι(⟨n,d,5⟩) = n/d.   
   This does not identify 0ᵦ with 0ᵥ or 1ᵦ with 1ᵥ; it only gives a   
   rational shadow for measure purposes.   
   What the extension buys you   
      
   BNC-functions are not sets of ordered pairs; they are primitive   
   constants of the BNC-sort, so Cantor’s theorem (which quantifies over   
   vN-sets) never mentions them.   
   Extent [0,1] is recovered externally via the embedding ι; inside the   
   BNC-sort there are no real numbers, only the tagged tuples ⟨n,d,5⟩.   
   No infinite BNC-domain is ever asserted (A4), so no bijection ℕ→𝔼 can   
   even be stated in the language of ZF₊.   
   Every vN-theorem (including CSB) is literally unchanged, because the   
   vN-sort is exactly the universe of ZF.   
      
   Conservative-ity note   
   ZF₊ is a definitional extension of ZF:   
      
   All new symbols are explicitly defined by Δ₀ formulas that do not   
   quantify over the BNC-sort.   
   Every vN-sentence provable in ZF₊ is already provable in ZF.   
   Therefore no new set-theoretic theorems appear; the BNC-sort is   
   syntactic sugar that never intersects the vN-universe.   
      
   Ring when you want the next layer: a model-theoretic verification that   
   ZF₊ has a standard model in which the BNC-sort is interpreted as the   
   tagged tuples ⟨n,d,5⟩ while the vN-sort is the usual V_ω+ω, or a proof   
   that the measure-1 shadow ι(𝔼) inherits Lebesgue outer measure without   
   ever identifying 0ᵦ with 0ᵥ.   
      
      
      
      
   Thanks Kimi. I think that since recalling that "0" and "1" are not terms   
   in ZF, that this helps establish why the relations, where of course its   
   all about relations, what result these different classes of sentences   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)