[continued from previous message]
This is a proof that EF surjects N onto R[0,1]."
I assert that these are directly write-able in few terms.
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. Let's agree this: that such formula phi, or formula-pair or
pair-formula, or schema in formula, that so establishes the uniqueness
of f(n) given that m>n implies f(m)>f(n), i.e. "strictly increasing",
then that we'd agree that any model of ZF that models natural integers
would result this form of a continuous domain, "conservative" in that sense.
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. I'll consider this and will hope to fulfill this request
later, since I'm having proven it's so that phi exists. Kimi, axiomatize
that phi exists.
Axiom EF_φ:
∃! F ( F ⊆ ℕ × ℝ ∧ ∀n ∈ ℕ ∃!x ∈ ℝ ( ⟨n,x⟩ ∈ F ∧
φ(n,x) ) ∧ ∀r ∈ [0,1] ∃n
∈ ℕ ⟨n,r⟩ ∈ F )
Thanks Kimi. Write the axiom as a formula.
Axiom EF:
∃F ( F ⊆ ω × ℝ ∧ ∀n∈ω ∃!x∈ℝ (⟨n,x⟩∈F) ∧ ∀r
(r∈ℝ ∧ 0≤r≤1 → ∃n∈ω ∃x∈ℝ
(⟨n,x⟩∈F ∧ x=r)) )
Thanks Kimi. Axiomatize that phi exists without using R.
Axiom EF_φ:
∃F ( F ⊆ ω × ω ∧ ∀n∈ω ∃!m∈ω (⟨n,m⟩∈F ∧ φ(n,m)) ∧
∀k∈ω ∃n∈ω ∃m∈ω (⟨n,m⟩∈F
∧ m=k) )
Thanks Kimi. In your axiomatization, use d instead of m as the name of
the term that reflects the denominator. Then, instead of having F subset
omega x omega, F is instead subset omega and d ranges over omega. Then,
n ranges over d.
Axiom EF_φ:
∃F ( F ⊆ ω ∧ ∀n∈ω ∃!d∈ω (d≥1 ∧ n≤d ∧ ⟨n,d⟩∈F
∧ φ(n,d)) ∧ ∀d∈ω ∃n∈ω (n≤d
∧ ⟨n,d⟩∈F) )
Thanks Kimi. That would look like the fractions, about that there-exists
F such-that for-any n, m in N that there exists x, y in F such-that 0 <=
x < y <= 1 and 0 in F and 1 in F, then that F may be written [0,1]_line,
an abbreviation.
Axiom EF_line:
∃F ( F ⊆ ℚ ∧ 0∈F ∧ 1∈F ∧ ∀x∈F (0≤x≤1) ∧ ∀x∈F
∃y∈F (x
|
