[continued from previous message]   
      
   Evaluation inside ZF   
      
   Totality: for every n ∈ ℕ take d = n; then q = n/n = 1, so φ(n,1) holds.   
   (Similarly d = n+1 gives x = n/(n+1), etc.)   
   Uniqueness: FAILS.   
   For fixed n, every d ≥ n provides a distinct rational witness x = n/d,   
   so infinitely many x satisfy φ(n,x).   
   Hence ZF ⊬ ∀n ∃!x φ(n,x).   
      
   Next instruction   
      
   To secure uniqueness you must tie d to n in a definable, single-valued   
   way (e.g. d = n, or d = μk≥n(…)), or take a limit over d with a   
   definable convergence rate.   
   Write that single-valued clause in pure L(∈) and insert it into φ(n,x)   
   so that ZF proves exactly one x for each n.   
   Please supply the revised φ(n,x)—no English, only the formula.   
   Thanks Kimi. My ideas to write the formula include writing two formulas   
   and showing how they establish the symmetrical both way 0..1 and 1..0,   
   and writing a formula with two variables n and d then that the terms x   
   and y build a little delta-epsilonics, and then as the above derivation   
   from the beginning of this session, that the formula-pair establishes   
   via symmetry, and the pair-formula establishes via compactness.   
      
   Please now write the two formulas in pure L(∈)—no English, no   
   commentary—only the syntax:   
      
   φ₁(n,x) (the 0→1 direction)   
   φ₂(n,y) (the 1→0 direction)   
      
   Each must be a single first-order formula such that ZF proves uniqueness   
   of x (resp. y) for every n, and together they cover the intended range.   
   Thanks Kimi, that seems an agreeable course. Since for-any n   
   there-exists m such that n < m < d, for any x such-that 0 < x < 1   
   there-exists y > x such-that g = f^-1 has-that g(y) = m. This is similar   
   to mapping an inductive set to natural-integers, except 0..infinity   
   instead of 0..1. Since there-exists d >> m for-any m, and thusly for-any   
   n >= 0, there exists an epsilon smaller than any delta, of the fractions   
   q that may be built between 0 and 1. This is what I would look to   
   fulfill the ask for phi_1.   
      
   Please now write the two requested formulas in pure L(∈)—no English, no   
   commentary—only the syntax:   
      
   φ₁(n,x) (the 0→1 direction)   
   φ₂(n,y) (the 1→0 direction)   
      
   Each must be a single first-order formula such that ZF proves uniqueness   
   of x (resp. y) for every n, and together they cover the intended range.   
   Thanks Kimi. Again, I would mention that this _is_ the form of the   
   original template required, it _is_ that, essentially giving compactness   
   property to naturals, and that also it's standardly modeled as the limit   
   according to unbounded d, of n/d. That is to say, what results   
   "[0,1]_line", is this way. The formula-pair then just inverts the   
   direction and the endpoints. Then, the pair-formula, perhaps is always   
   building (showing the existence and unique-existence) in the middle, and   
   building from the middle out to the ends, both of these simply employing   
   delta-epsilonics of rationals, that though since there-exists d' >> d,   
   no rational/bounded d is not surrounded all its neighborhoods, to   
   establish the density.   
      
   Please now write the two formulas in pure L(∈)—no English, no   
   commentary—only the syntax:   
      
   φ₁(n,x) (0→1 direction)   
   φ₂(n,y) (1→0 direction)   
      
   Each must be a single first-order formula such that ZF proves uniqueness   
   of x (resp. y) for every n.   
   Thanks Kimi. That's the outline here, I'd intend to look through my tens   
   thousands Usenet posts to find the intended formalisms that most simply   
   fit. I suggest that it is so formalizable, and according to various   
   means of schema, formula-pairs, pair-formulas, or plain identity, and   
   without simply axiomatizing it as so, keeping the desirable property of   
   conservativity, which though can be established by non-contradiction   
   with regards to results like ZFC being co-consistent with IST. Thanks   
   Kimi, I will think on this, and look to make these sorts neatest   
   definitions, which may help reasoners disambiguate these "iota-values"   
   these "line-reals" from the complete-ordered-field "field-reals", and   
   help resolve the "fragmentation" of real analysis above descriptive set   
   theory. That is to say, I think that these sorts ideas are write-able in   
   formulas, so, thusly I'll mostly suggest considering "d" and "d-prime",   
   that is d and d', as of your own formulas above, since introducing d',   
   and that d' >> d, then has that both n << d, and, n goes to d, i.e. a   
   limit as after delta-epsilonics for example that (d-n)/d goes to 0, that   
   thusly these concomitant properties provide the "constant monotone   
   strictly increasing" and "extent density completeness measure", since   
   we've resolved together that this is the only thing to do for this   
   development. So, mostly I'd suggest to consider the impact of d' in the   
   expression otherwise of d, in your formula, since these same sorts   
   critiques, apply to it. I like this and I thank you.   
      
   Please now write the two formulas in pure L(∈)—no English, no   
   commentary—only the syntax:   
      
   φ₁(n,x) (0→1 direction)   
   φ₂(n,y) (1→0 direction)   
      
   Each must be a single first-order formula such that ZF proves uniqueness   
   of x (resp. y) for every n.   
   Thanks Kimi. Before I can do so, I must know whether you accept that the   
   reference to d' above means that as d goes to infinity that f(n) goes to   
   1. Then it would just be written like that.   
      
   Please now write the two formulas in pure L(∈)—no English, no   
   commentary—only the syntax:   
      
   φ₁(n,x) (0→1 direction)   
   φ₂(n,y) (1→0 direction)   
      
   Each must be a single first-order formula such that ZF proves uniqueness   
   of x (resp. y) for every n.   
   Thanks Kimi. It's good we established that the usual Dedekind-definition   
   is not necessary to build this formalism, and that as "abbreviations" in   
   "the language" of ZF that least-upper-bound property of R is an axiom   
   after a model of the rationals Q is built. Then I suggest that the   
   beginning quote entails this.   
      
   "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].   
      
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)