[continued from previous message]   
      
   and the extent is [0,1] and the density is established and the   
   least-upper-bound is established and the measure is established, or   
   "extent density completeness measure". It's a fair point that it can   
   always just be axiomatized, yet that's deemed not an independent axiom,   
   since it's considered that f ranges between 0 and 1 inclusive, and is   
   "strictly increasing", then that relating that to any of the bounded   
   rational enumerations 0/d, ..., d/d it's "more dense" i.e. has in the   
   neighborhoods more points so establishing density in the extent, then,   
   least-upper-bound is courtesy that any successor in the domain is the   
   least-upper-bound in the range, and that f^-1(1)'s least-upper-bound is   
   1, then as that measure is defined as via the length assignment then   
   that sigma-algebras are as of n-sets or differences in elements from the   
   range, by the fact that the inductive set's elements exist in the   
   domain. So, these properties get attached to what defines the relation   
   phi, then though that the [0,1]_line is _not_ the [0,1]_field, since   
   those must be distinguished, since these are two _different_ models of   
   continuous domains, and line-reals this way are not field-reals the   
   complete-ordered-field, though they agree about 0 and 1.   
      
   φ(n,x) ≡ x∈ℝ ∧ ∀k∈ℕ ∃d≥k (d∈ℕ ∧ n≤d ∧   
   |x−n/d|<1/d)   
   Thanks Kimi. That sort of account makes not "constant monotone" the   
   strictly increasing, since while strictly increasing, it must be   
   "constant monotone", constant differences, to establish density. It's   
   appreciated the form, while though it must be addressed that these are   
   _not_ field operations, to result, and that the definition of [0,1] is   
   its own definition line-reals, with n/d, completing a clock-arithmetic   
   in [0,1], not the same thing as presuming the completion of the   
   complete-ordered-field after the constructible/definable rationals,   
   according to usual accounts of the powerset of integers making for a   
   binary Cantor space, and relating that to [0,1], according to rational   
   bounds or Dedekind. This definition of [0,1] has its own completeness,   
   and need not consider Dedekind completeness. So, then the "constant   
   monotone strictly increasing" properties, would result more of the formula.   
      
   φ(n,x) ≡ x∈ℝ ∧ ∃d∈ℕ (d≥1 ∧ n≤d ∧ x = n/d ∧ ∀m 0, gcd(a,b)=1 (all   
   Δ₀   
   over HF)   
   “x is a real (Cauchy)” : x is a set of rationals coding a Cauchy   
   sequence of rationals with fixed rate 1/k convergence (Δ₁ᵀᴹ).   
   “x ≤ y” for reals: the usual Δ₁ᵀᴹ definition on the codes.   
   “n/m” (rational) : the unique rational q with m·q = n (defined for m ∈   
   ℕ{0}).   
      
   Candidate formula rewritten in pure syntax   
      
   φ(n,x) ≡   
   ∃d ∈ ℕ (d ≥ 1 ∧ n ≤ d ∧ x is a real ∧   
   ∃q (q is a rational ∧ q = n/d ∧ x = q) ∧   
   ∀m ∈ ℕ (m ≤ d → ∃r (r is a rational ∧ r = m/d ∧ 0 ≤ r ≤   
   1)) ∧   
   0 ≤ x ≤ 1)   
   Every quoted notion is explicitly Δ₀/Δ₁ᵀᴹ in ZF, so the whole   
   formula is   
   first-order in L(∈).   
      
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)