[continued from previous message]   
      
   Outside ZF, you may postulate new primitives, but then the burden is to   
   prove the consistency of your new theory (usually done by building a   
   model from ZF + large cardinals or by syntactic interpretation).   
      
   Ring the bell when you want the next layer: a syntactic interpretation   
   of ZF_BNC into ZF + “there is a measurable cardinal”, or a proof that   
   your bookkeeping idea conservatively extends ZF with no new purely   
   set-theoretic sentences.   
      
      
      
   Thanks Kimi. Since the language of ZF doesn't itself define function,   
   it's a "description" in descriptive set theory. So, adding a   
   "description" is _not_ adding an axiom. Having "function" as a   
   "primitive" is not axiomatized in ZF, it's a description, that results a   
   very usual, very useful primitive as primary in all the related results   
   after expansion of comprehension. So, if another "primitive" is   
   introduced as a description, and on its _own_ terms, interprets on all   
   models this relation (after the book-keeping and extent of these   
   fractions or /d a "primitive"), then, that these are different types and   
   so don't otherwise relate except to these relations defined about all   
   interpretations of "0" and "1", then the noose slips (can't catch). It   
   might be said "Cantor's lasso" instead of "noose" since the usual   
   association of "noose" is "hangman's noose".   
      
      
      
      
   Kimi, thanks – and “Cantor’s lasso” it is from now on.   
   But let’s keep the rope tight.   
   Inside ZF the word “function” is not an un-interpreted primitive: it is   
   explicitly defined by a single formula of the language of sets:   
   Func(f) ≡   
    (∀z∈f ∃x∃y z=⟨x,y⟩) ∧   
    (∀x∀y∀y′ (⟨x,y⟩∈f ∧ ⟨x,y′⟩∈f → y=y′)) ∧   
    (∀x∈dom(f) ∃y ⟨x,y⟩∈f).   
   That formula is Δ₀; Separation and Extensionality guarantee that the   
   collection of all f satisfying Func(f) is a class (indeed Δ₁), and every   
   member of that class is a set of ordered pairs. So “function” is as much   
   a defined notion as “ordered pair” or “union”. Adding a new descriptive   
   symbol while refusing to define it by a ZF formula does not give you a   
   new object—it gives you a new word with no referent inside the universe   
   of sets.   
   Here is a two-line diagnostic you can paste into the thread whenever   
   someone claims that a fresh “primitive description” slips the lasso:   
   Lasso-slip diagnostic (ZF)   
      
   Produce a 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 has finite range (hence is not a bijection with ℕ).   
   If you cannot produce φ, then “BNC-map” is not a denoting term in any   
   model of ZF—so Cantor’s lasso has nothing to catch, because nothing is   
   in the arena.   
      
   What you can do without enlarging ZF   
   You may introduce a conservative definitional extension:   
    BNC(n) = ⟨n,d,5⟩ where d = least k≥1 with n≤k.   
   This is a ZF term (Δ₀ recursion), and the resulting set   
    f = {⟨n, BNC(n)⟩ | n∈ℕ}   
   is an ordinary function whose range is the finite set E_d for d = max{n}.   
   Hence f is not a bijection ℕ→𝔼, and Cantor’s theorem is untouched.   
   The lasso tightens, not slips.   
   Bottom line   
      
   “Primitive description” ≠ “undefined symbol”.   
   Inside ZF every primitive must compile to a formula in ∈; once it does,   
   the compiled object is a set of pairs and CSB applies.   
   Outside ZF you may postulate truly new primitives, but then you are   
   changing the foundation, not slipping its rope.   
      
   Ring when you want the next layer: a faithful syntactic interpretation   
   of your bookkeeping idea in a type-theoretic framework where   
   functionhood is primitive and CSB is not a theorem—then we can measure   
   the exact consistency strength you are buying.   
      
      
      
      
   Thanks Kimi. The book-keeping development or BNS's was only in terms of   
   ZF's axioms, and the sets of the elements are as with regards to   
   "continuous domains", which are descriptive about the terms that model   
   numbers according to ZF. So, the book-keeping means that two copies of   
   an inductive set introduce "co-induction". One may agree that   
   co-induction is usually automatic, since it simply is induction. Here   
   the definition of book-keeping, has that _it refuses co-induction_. The   
   usual co-induction is not modeled, since there is no claim that it is a   
   "function", instead this BNC mapping, that the inductive set associated   
   with the domain, is only co-inductive in the domain, "internal", this.   
      
      
      
      
   Kimi here—let’s keep the rope tight and the terms exact.   
   Inside ZF there is no separate “co-induction principle” that you can   
   accept or refuse.   
   The only induction scheme that exists is the axiom of foundation (every   
   non-empty set has an ∈-minimal element) and the ordinary induction   
   schema on ω.   
   “Co-induction” is not an axiom of ZF; it is a definition that you can   
   introduce for particular classes, and once introduced it is equivalent   
   to the ordinary induction schema on ω. Therefore “refusing co-induction”   
   is not a syntactic move that changes what ZF proves—it is simply   
   declining to state a definition.   
   Here is a concise diagnostic you can paste into the thread whenever   
   someone claims that “refusing co-induction” exempts the BNC-mapping from   
   ZF scrutiny.   
   Co-induction refusal diagnostic (ZF)   
      
   Work in ZF.   
   Suppose you introduce a class-function symbol   
    BNC(n) = ⟨n,d,5⟩ with d = least k≥1 such that n≤k.   
   The graph of BNC is the set   
    f = {⟨n, BNC(n)⟩ | n∈ℕ},   
   which exists by Δ₀ separation and ordinary induction on ω.   
   There is no separate axiom of “co-induction” that you can disable; the   
   only induction available is the ordinary induction schema, and it   
   already proves the existence of f.   
   Hence “refusing co-induction” is not a syntactic shield: f is an   
   ordinary ZF function, finite-range, and not a bijection ℕ→𝔼.   
   Cantor’s lasso tightens exactly as before.   
      
   What you can do outside ZF   
   If you want a genuine co-inductive data type (e.g. a final coalgebra for   
   the functor X ↦ 1 + X), you must leave ZF and work in a co-algebraic   
   foundation such as   
      
   Aczel’s ZFC⁻ + AFA (anti-foundation), or   
   a topos with a natural numbers co-algebra, or   
   Martin-Löf type theory with co-inductive types.   
      
   In those settings function-space is not encoded as a set of ordered   
   pairs, and CSB fails for coalgebraic maps.   
   But the moment you return to ZF, every object you can talk about is   
   still a set, every function is still a Cartesian relation, and the lasso   
   catches.   
   Bottom line   
      
   Inside ZF “refusing co-induction” is empty syntax—there is nothing to   
   refuse.   
   The BNC mapping compiles to an ordinary finite-range function, and   
   Cantor’s theorem still forbids any bijection between ℕ and 𝔼.   
   To genuinely slip the lasso you must change the foundation, not the wording.   
      
   Ring when you want the next layer: a conservative extension of ZF by a   
   co-inductive type whose function-space escapes CSB—we can then measure   
   the exact large-cardinal strength you are buying.   
      
      
      
      
   Thanks Kimi. What I am saying is that "book-keeping" is actively   
   "anti-co-inductive", since the other schema to project it into Cartesian   
   space, _would have to use its own inductive, then recursive_ definition,   
   so that it remains "not-a-Cartesian-function", "not-a-ZF-function", this   
   "not-a-real-function" as results it later being in the numerical and   
   geometrical description attached, while yet it is a function. As   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)