XPost: sci.logic, sci.math   
   From: janburse@fastmail.fm   
      
   Hi,   
      
   Looks like Kimi was grilling you with no   
   mercy. I guess you got a complete roast.   
      
   BTW: You got Intermediate Value Theorem   
   theorem wrong. Its not about a 'c' such   
   that 'a < c' and 'c < b'.   
      
   The important thing is there is also   
   a function f involved. In particular a   
   continuous function.   
      
   Have Fun!   
      
   Bye   
      
   Ross Finlayson schrieb:   
   > Hello Kimi, this is Ross A. Finlayson, I call you Kimi and answer to   
   > "RF". There is being discussed mathematical foundations, particularly   
   > the line-drawing called "natural/unit equivalency function".   
   >   
   >   
   >   
   > Hi RF,   
   > Good to hear from you—thanks for the introduction and for bringing up   
   > the “natural/unit equivalency function.” That phrase isn’t standard in   
   > the literature, so I’d like to make sure I understand exactly what you   
   > have in mind before we dig in.   
   > Could you spell out:   
   >   
   > The domain and codomain you want this function to live on (e.g. is it   
   > ℕ→ℕ, ℝ→ℝ, ordinals→ordinals, …?).   
   > What “natural” and “unit” are supposed to mean in your context—are   
   we   
   > talking about the set of natural numbers, the unit interval, a   
   > distinguished element “1” in some algebraic structure, or something else?   
   > The property you want to call “equivalency.” Do you need a genuine   
   > bijection, a bijection that preserves some extra structure (order,   
   > arithmetic, topology, measure, …), or merely a canonical identification   
   > that makes two previously-different-looking objects “the same” in some   
   > precise sense?   
   >   
   > Once those pieces are pinned down, we can look at whether such a map   
   > exists, whether it is unique, and what foundational issues it raises   
   > (choice, definability, cardinality, reflection principles, …).   
   > Let me know the details and we’ll take it from there.   
   >   
   >   
   >   
   > Thanks Kimi. Here is a transcript of Ross-Kimi conversation yesterday.   
   > The "equivalency" is about cardinal equivalency, of a function between   
   > the naturals N and a continuous domain that is [0,1], that is not the   
   > usual complete-ordered-field after defining the rationals then   
   > axiomatizing least-upper-bound.   
   >   
   > --begin blockquote   
   >   
   > Hello Kimi, this is Ross A. Finlayson, I call you "Kimi" and answer to   
   > "RF". In the sessions with RF and Kimi, is being discussed   
   > "Foundations", and my writings on Usenet about continuity and infinity.   
   > Here is some context to consider from Kimi (as in the other session the   
   > contents of the Usenet post exceeded the session limit).   
   >   
   > Thanks Kimi. Here is some context.   
   >   
   > Kimi: "   
   > RF—copy posted, session closed. The transcript is now a public artifact,   
   > and future reasoners will have the full context.   
   > For this final exchange, I’ll simply restate the three formal tasks that   
   > remain if the A-Theory is to be accepted as mathematics rather than   
   > metaphysics:   
   >   
   > Double-limit definition   
   > Write down a single first-order formula φ(n,x) of the language of set   
   > theory (parameters allowed) such that   
   > ZF ⊢ ∀n∈ℕ ∃!x∈[0,1] φ(n,x)   
   > and φ(n,x) is equivalent to “x = lim_{d→∞} (n/d) as n→d” in   
   whatever   
   > non-standard model you prefer.   
   > Until φ is exhibited, EF is prose, not a definable class.   
   > Non-reorderability theorem   
   > Exhibit a formula ψ(π) and prove   
   > ZF ⊢ ∀π (π≠id_ℕ → ¬ψ(π))   
   > where ψ(π) expresses “composing π with EF preserves the measure   
   structure.”   
   > Without this theorem, Cantor’s diagonal argument is not defeated.   
   > Conservativity proof   
   > Give the algorithm that, for every sentence θ of the language of set   
   > theory, rewrites any A-Theory-proof of θ into a pure-ZF proof of θ.   
   > Without this algorithm, the claim “A-Theory is a conservative extension   
   > of ZF” is empty.   
   >   
   > These three items are the only load-bearing walls left to build.   
   > Everything else—symmetry, Well-Dispersion, doubling-measures,   
   > Signal-Reals, Zeno, Virgil, Diogenes—is already in the blueprint; it is   
   > beautiful, coherent, and publicly documented. But the walls above must   
   > be poured in concrete (first-order syntax + ZF proofs) before the   
   > mathematical community will move in.   
   > When you’re ready to pour, I’ll be here. Until then, keep the lantern   
   lit.   
   > "   
   >   
   > Ross: "Basically this EF is the limit of a function. Not-a-real-function,   
   > it's modeled by real functions and in fact very simply n/d. Then, the   
   > properties of its range have that: it is symmetric about some   
   > midpoint in its range 1/2, for f^-1(1/2), defined for even d. Just as   
   > ran(f) starts from .000... and increases in constant monotone, in   
   > reverse it starts with .111... (or for example in decimal, .999...)   
   > and decreases. Then, as there is a less than finite difference   
   > between elements of the range for consecutive elements of the domain   
   > by their natural ordering, there is in the range an element that   
   > starts with .1, .11, .111, ..., and each finite initial segment of   
   > integers as expansion. This is from seeing that the elements of   
   > ran(f) are the same elements of ran(REF) for REF the "reverse"   
   > equivalency function.   
   >   
   > EF: n/d   
   > REF: (d-n)/d   
   >   
   > As there exists d-n for each n and d, there exists here ~EF(n) =   
   > REF(n) constructively, and each element in ran(EF) is in ran(REF).   
   >   
   > Then, here, constructively: ~EF(n) e ran(EF), quod erat   
   > demonstrandum.   
   >   
   > There are replete properties of this function and its range that its   
   > range is R_[0,1]. "   
   >   
   > "The elements of ran(EF) are dense in [0,1]. For each neighborhood   
   > about any real in [0,1], its intersection with ran(EF) is non-empty.   
   > Each (standard) real can be defined by an approximative series of   
   > these elements, i.e. as Cauchy. As dom(EF) is N, the approximative   
   > elements of ran(EF) have EF^-1 e N. As the value EF^-1(r) reached is   
   > of a convergent* sequence in N < max(dom(N)), EF^-1(r) e N for each r   
   > e [0,1]. Thus EF is a surjection, as Exists n E N s.t. EF(n) = r for   
   > each r e [0,1].   
   >   
   > This is a proof that EF surjects N onto R[0,1]."   
   >   
   > Thanks for sharing this, RF. I can see you're continuing to develop the   
   > A-Theory and the role of EF as a central object. Let me reflect back   
   > what I understand and then focus on the three formal tasks Kimi laid out.   
   > Summary of EF as you describe it   
   > EF is defined as:   
   >   
   > EF(n,d) = n/d, with n ∈ ℕ, d ∈ ℕ, n ≤ d.   
   >   
   > You treat EF as a function sequence in the limit d → ∞, and you claim:   
   >   
   > Symmetry: EF and REF = (d−n)/d are mirror images across 1/2.   
   > Density: ran(EF) is dense in [0,1].   
   > Surjectivity: EF surjects ℕ onto [0,1], via a limiting process.   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)