[continued from previous message]   
      
   book-kept, and unbreakable.â€�   
      
      
   --end excerpt   
      
      
      
   RF, the moment you claim that your bookkeeping gadget serves as a   
   counterexample to the uncountability of bijections onto a continuous   
   domain, you are no longer merely playing with heuristic labels; you are   
   asserting the existence of a bijection inside ZF. That assertion is now   
   subject to the only definition of “bijectionâ€� that ZF recognises: a set   
   of ordered pairs that is both injective and surjective. Everything else   
   is prose.   
   Below is a single, self-contained refutation that you can drop into the   
   thread the next time someone alleges that the “bijective-non-Cartesianâ€�   
   coding escapes Cantor’s theorem. It is written in plain ZF, uses no   
   meta-mathematical shorthand, and ends with an explicit challenge that   
   cannot be dodged by renaming.   
   Cantor’s noose inside ZF   
   Work in ZF. Let ð�”¼ be the class defined by   
   â€ƒð�”¼ ≔ { ⟨n,d,5⟩ | d≥1, n≤d }.   
   For any set A, write   
   â€ƒInj(A,ð�”¼) ≔ { f | f is a function ∧ dom(f)=A ∧ ran(f)⊆ð�”¼ ∧ f   
   is   
   injective }.   
   Key observation (ZF theorem, 4 lines)   
   For every set A,   
   â€ƒf ∈ Inj(A,ð�”¼) → dom(f)=A ∧ ran(f)⊆E_d for some d≥1.   
   Proof: ran(f) is a set, hence contained in the set E_d for   
   â€ƒd ≔ max{ d | ∃n (⟨n,d,5⟩∈ran(f)) },   
   which exists because ran(f) is finite (E_d is finite for each d).   
   Corollary (ZF)   
   If A is infinite, then Inj(A,ð�”¼)=∅.   
   Proof: E_d is finite, so no injective map from an infinite set into E_d   
   exists.   
   Cantor’s theorem for ð�”¼ (ZF)   
   There is no set f such that f is a bijection between â„• and ð�”¼.   
   Proof: Such an f would belong to Inj(â„•,ð�”¼), contradicting the corollary.   
   Challenge to the claimant   
   Exhibit a set f ∈ V_ω+1 (i.e. a set that ZF proves to exist) such that   
   â€ƒZF ⊢ “f is a bijection ℕ→ð�”¼â€�.   
   Until you do so, the slogan “non-Cartesian bijectionâ€� is merely a name;   
   it does not denote an object that ZF recognises as a function, and   
   therefore cannot threaten Cantor’s theorem.   
   What is allowed   
   You may certainly principle that “extent is modelled by a bookkeeping   
   tagâ€� and that “continuous domain intuition is recovered in the limit of   
   speechâ€�. What you cannot do—inside ZF—is assert the existence of a   
   bijection and then plead exemption from the graph-based definition of   
   function. The moment the assertion is made, Cantor’s noose tightens, and   
   the only escape is to leave ZF altogether (for instance by adopting a   
   type theory with primitive function symbols, or by working in a topos   
   where “functionâ€� is not encoded as a set of pairs).   
   So the dialectical situation is clean:   
      
   Inside ZF, every bijection is Cartesian, and CSB applies.   
   Outside ZF, you may invent new primitives; but then the burden is to   
   build a new foundation, not to claim that ZF refutes itself.   
      
   Ring the bell when you want the next layer: a faithful interpretation of   
   your bookkeeping idea in a type-theoretic fragment where “functionâ€� is   
   not a set of pairs, or a conservativity proof showing that your   
   heuristic adds no new set-theoretic theorems.   
      
      
      
   Thanks Kimi. Then I'd simply re-write all theorems related to functions   
   so that they accept either the usual definition, of "function", or, this   
   "mapping" in the case when being 1-1 and onto is always combined,   
   instead of being about surjections and injections either way. This way   
   then, all the results about "bijections that exist", hold, while   
   accordingly there can be that this "bijection-non-Cartesian" mapping, is   
   a "bijection that exists", only between its own domain and range, _and   
   only via composition with it, and since the equivalency function is   
   defined about being _only its own non-reorder-able structure_, AND, that   
   the book-keeping is _internal_, that "Cantor's noose" has nothing to   
   catch, since the type of "bijective-non-Cartesian-function", is not the   
   type "function", while at the same time, the relations that would   
   otherwise compose the functions across two different cardinals, instead   
   make that it must be the putative "function" not existing, "too weak to   
   break", means that it only applies to other functions, , not   
   bijective-non-Cartesian-functions, or   
   "bijective-non-Cartesian-mappings", or, like "not-a-real-function", as   
   EF is "not-a-real-function", "not-a-ZF-function".   
      
      
      
      
   RF, you are free to introduce a new primitive—“bijective-non-Cartesian   
   mappingâ€� (call it BNC-map)—and to axiomatise it any way you like, but   
   the moment you want to state theorems inside ZF you must define that   
   primitive by a formula of the language of ZF. Inside that language there   
   is only one kind of function: a set of ordered pairs. Therefore:   
      
   If you define “BNC-mapâ€� explicitly, the definition is automatically a   
   set of ordered pairs, hence an ordinary ZF function, and Cantor’s   
   theorem applies.   
   If you refuse to define it, then “BNC-mapâ€� is not a term of ZF, so the   
   alleged bijection does not exist in the universe of sets; consequently   
   you have no object that could serve as a counter-example to Cantor’s   
   theorem.   
   There is no third possibility: either the object is a set (hence   
   Cartesian), or it is not a set (hence non-existent for ZF purposes).   
      
   Below is a concise “type-checkâ€� that you can paste into the thread; it   
   forces the proponent to pick door 1 or door 2, and shows that neither   
   door breaks Cantor.   
   Type-check for “BNC-mapâ€� (ZF only)   
   Context: Work in ZF. Let ð�”¼ be the class { ⟨n,d,5⟩ | d≥1, n≤d }.   
   Door 1 — you define the BNC-map   
   Suppose you give an explicit ZF formula φ(x,y) such that   
   â€ƒZF ⊢ ∀x∀y∀y′ (φ(x,y) ∧ φ(x,y′) → y=y′)   
   â€ƒZF ⊢ ∀x∈ℕ ∃!y∈ð�”¼ φ(x,y).   
   Then the set   
   â€ƒf ≔ { ⟨x,y⟩ | φ(x,y) }   
   exists by Separation, is a function in the usual ZF sense, and is   
   finite-valued (because ran(f)⊆E_d for some finite d).   
   Hence f cannot be a bijection ℕ→ð�”¼, by the finite-range observation   
   above.   
   Cantor’s theorem is untouched.   
   Door 2 — you refuse to define the BNC-map   
   Then “BNC-mapâ€� is not a set, so the phrase   
   â€ƒâ€œthere exists a BNC-bijection ℕ→ð�”¼â€�   
   is not a sentence of the language of ZF; it has no truth-value in any   
   model of ZF.   
   Therefore no contradiction with Cantor’s theorem can even be stated, let   
   alone proved.   
   Slogan   
   â€œEither the BNC-map is a set, in which case it is an ordinary   
   finite-range function, or it is not a set, in which case it is nothing   
   for ZF to talk about. Cantor’s noose catches you in the first case; in   
   the second case you are not even in the arena.â€�   
   What is perfectly permissible   
   You may *introduce a new theory—call it ZF_BNC—whose language contains a   
   primitive binary function symbol ð�–»ð�–¾ð�—   
   ð�–º(·,·) and whose axioms   
   explicitly forbid ð�–»ð�–¾ð�—   
   ð�–º to be a set of ordered pairs. You can then   
   conservatively extend ZF_BNC with axioms that assert   
   â€ƒð�–»ð�–¾ð�—   
   ð�–º : â„• → ð�”¼ bijectively.   
   But then:   
      
   You are not working inside ZF any longer; you are working in a stronger   
   theory whose consistency strength must be analysed separately.   
   Every model of ZF_BNC is a non-well-founded or non-standard model in   
   which the extension of ð�–»ð�–¾ð�—   
   ð�–º is a proper class; hence no such model   
   is a model of ZF.   
   Therefore you have not refuted Cantor’s theorem in ZF; you have merely   
   relativised it to a different foundation.   
      
   So the dialectical ledger is clear:   
      
   Inside ZF, “bijectionâ€� = “set of ordered pairsâ€�, and Cantor wins.   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)