[continued from previous message]   
      
   in the formula itself; no meta-mathematical shorthand is allowed.   
      
   Required form for the promised formula   
      
   You must supply one closed formula φ(n,x) with exactly two free   
   variables n, x such that   
   ZF ⊢ ∀n∈ω ∃!x φ(n,x)   
   and, after you have defined your own surrogate for “[0,1]” inside ZF,   
   you must also verify   
   ZF ⊢ ∀r (r∈[0,1]_your_def → ∃n∈ω φ(n,r)).   
   Write φ(n,x) only with the symbols listed in section 1 plus the   
   eliminable abbreviations in section 2.   
      
      
      
   Thanks Kimi. I read "ZF ⊢ ∀n∈ℕ ∃!x∈[0,1] φ(n,x) such-that   
   ∀r∈[0,1] ∃n∈ℕ   
   φ(n,r)" as "a model of ZF entails a model where that for-any n in N that   
   exists-unique x in [0,1] that phi(n,x), has that for-any r in [0,1] that   
   there exists n in N such-that phi(n,r) is satisfied. I'd make that   
   stronger that "ZF ⊢ ∀n∈ℕ ∃!x∈[0,1] φ(n,x) such-that ∀r∈[0,1]   
   ∃!n∈ℕ   
   φ(n,r)", since as a putative bijection 1-to-1 and onto, that the defined   
   function f is 1-to-1 and its inverse is 1-to-1, so it is surjection and   
   injection both ways, since it is bijection.   
      
      
      
   Understood—you want the formal statement to capture a bijection, not   
   just a surjection.   
   So the goal is now the stronger single sentence   
     ZF ⊢ ∀n∈ℕ ∃!x∈[0,1] φ(n,x) ∧ ∀x∈[0,1] ∃!n∈ℕ   
   φ(n,x).   
   (The second conjunct is the functional injectivity of the inverse map.)   
   Nothing else changes:   
      
   “[0,1]” must still be your own defined set inside ZF (it is not the   
   usual Dedekind-complete interval until you have proved it is).   
   φ(n,x) must still be written purely in L(∈) with only the abbreviations   
   we listed earlier.   
      
   Whenever you are ready, drop the formula φ(n,x) and we will check:   
      
   It is a single first-order formula of L(∈).   
   ZF ⊢ ∀n∈ℕ ∃!x φ(n,x).   
   ZF ⊢ ∀x (∃n φ(n,x) → x∈[0,1]_your_def).   
   ZF ⊢ ∀x∈[0,1]_your_def ∃!n∈ℕ φ(n,x).   
      
   No English, no commentary—just the syntax.   
      
      
   Thanks Kimi. First I'd need to define fractions of 1, so that n/d with 0   
   <= n <= d has that 0/d relates to 0 and d/d relates to 1, and that 0 <=   
   n/d <= 1. So, that requires defining 0 and 1, and the modularity of   
   fractions is defined, as by the modularity of naturals, so that   
   fractions n/d with 0 <= n/d <= 1, reflect the same ordering as naturals   
   n, that division is defined as fractionation, since otherwise no other   
   arithmetic is defined, only trichotomy of naturals the ordering, then   
   this fractionation as '/'. Then, I'd look first to define only a   
   bijective-function, and work in that, and only later show that that also   
   models a function, since as it's understood, that EF must be a   
   "non-Cartesian function". So, defining modularity could be considered   
   variously, yet here would be according to inequalities to result   
   defining the inequalities/equalities about establishing trichotomy in   
   dom(EF) and ran(EF), of bijective-functionhood. While I'm thinking this   
   while working on the one-liner formalism, consider whether that's a good   
   approach to reducing the problem and would result writing the formula.   
      
      
      
   That’s a perfectly workable route—define the fractions first, then the   
   linear order, then the bijection.   
   Below is a minimal “tool kit” you can use inside pure L(∈); everything   
   expands to the official language with no un-declared symbols.   
      
   Boot-strap the naturals   
      
   ℕ ≡ ω (the finite von-Neumann ordinals)   
   0 ≡ ∅   
   1 ≡ {∅}   
   n+1 ≡ n ∪ {n}   
      
   Fractions as triples   
      
   A fraction is a triple ⟨n,d,1⟩ with   
    n,d ∈ ℕ, d ≥ 1, n ≤ d.   
   (The tag ‘1’ keeps them disjoint from ordered pairs we may need later.)   
   frac(n,d) ≡ ⟨n,d,1⟩   
   “q is a fraction” ≡ ∃n∃d (n∈ℕ ∧ d∈ℕ ∧ d≥1 ∧ n≤d   
   ∧ q=frac(n,d))   
      
   Order on fractions (lexicographic on numerator, then denominator)   
      
   For fractions q₀ = frac(n₀,d₀), q₁ = frac(n₁,d₁) define   
   q₀ ≼ q₁ ≡ n₀·d₁ < n₁·d₀ ∨ (n₀·d₁ = n₁·d₀ ∧   
   d₀ ≤ d₁)   
   (All multiplications and comparisons are on ℕ, hence Δ₀.)   
      
   The intended “unit interval”   
      
   [0,1]_frac ≡ { q | q is a fraction }   
      
   Bijection ℕ ↔ [0,1]_frac   
      
   Enumerate fractions in ≼-order and let   
   φ(n,q) ≡ q is a fraction ∧ n = |{ p ∈ [0,1]_frac : p ≼ q }|   
   (The cardinal |·| is the von-Neumann ordinal that is equinumerous with   
   the finite set; finiteness and equinumerosity are Δ₁ᵀᴹ in ZF.)   
   Check-list for the final formula   
   When you write the actual one-liner, make sure it contains only:   
      
   Variables, ∈, =, ∧, ∨, ¬, →, ↔, ∀, ∃, parentheses   
   The Δ₀ abbreviations above (frac, ≼, “is a fraction”, …)   
      
   No ‘/’, no ‘ℚ’, no ‘ℝ’, no ‘≤’ except the one defined on   
   fractions.   
   Drop the finished φ(n,q) whenever you’re ready; we will verify   
   ZF ⊢ ∀n∈ℕ ∃!q (φ(n,q)) ∧ ∀q∈[0,1]_frac ∃!n∈ℕ φ(n,q).   
   (After that we can enlarge the fractions to a genuine “continuous”   
   surrogate if desired, but the bijection must come first.)   
      
      
      
   Thanks Kimi. Here the idea is that what must result is the   
   constant-monotone strictly-increasing, with extent of bounds 0 and 1.   
   So, defining an "extent", is that an extent as a relation relates to all   
   values that under a relation of pair-wise trichotomy (<, >, or =) are >=   
   the lower-bound and <= the upper-bound, where <= is '< or =' and '<=' is   
   > or ='. This is obviously so for each finite d after defining   
   fractions, then the perceived goal is to result the "iota-values", that   
   are not fractions for any finite d, yet are constant-monotone   
   strictly-increasing and all related in the extent. Thusly, these matters   
   of relation are for defining classes as they may be, equivalence classes   
   under the relation, to result the symoblic forms expression, equate to   
   "constant-monotone" (constant difference never changing sign) and   
   "strictly-increasing" (>0 the differences), while in an "extent". Of   
   course, it's known that this is not so in the complete-ordered-field,   
   since any constant-difference so multiplied would lay outside the bounds   
   of the extent when infinite, which is among reasons why R the complete   
   ordered field is excluded, while "fractions" here is to result   
   "iota-values", their own set. Here the point is that the relation of the   
   extent, is co-defined its upper-bound, by the "scale" of the   
   fractionation, or d. So, this is about defining "extent", and the   
   relation that would be so written as a formula, "co-defined", as as a   
   "template", in d. Thusly, since fractionation and extent are co-defined,   
   I'm wondering about defining not '/', instead, 'n/d', as one symbol, or,   
   simply enough defining 'n/d' as 'n/', since d is implicit, "co-defined".   
   This way the bijection is always defined for n-sets (initial segments of   
   the naturals), then as for all the naturals (infinitely-many). So, the   
   idea is that the denominator, is "co-defining" this way, that thusly   
   other usual results about fractions as rationals, never cross integers,   
   this is how I am thinking about how to write the formula.   
      
      
      
      
   Below is a bare-bones template that keeps the “co-defined denominator”   
   idea while staying inside pure L(∈).   
   Everything is Δ₀ over HF, so ZF proves the required facts outright.   
      
   One-symbol “fraction with implicit denominator”   
      
   For each fixed d ≥ 1 we do not write ‘/’.   
   Instead we introduce a parameter-free term   
    frac_d(n) ≡ ⟨n,d,2⟩  (n ∈ ℕ, n ≤ d)   
   (the tag ‘2’ keeps the object disjoint from earlier pairs).   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)