   ## 8  The real line as a space in ASD

We are at last ready to construct R as a Σ-split subspace of the bounded interval predomain IR, and hence of ΣQ×ΣQ.

Remark 8.1 Because of Lemma 5.11, the process of defining R by means of a nucleus E on IR, where IR is in turn defined by a nucleus E1 on ΣQ×ΣQ, is the same as giving a nucleus E on the larger space for which

 E·E1   =  E  =  E·E  =  E1· E.

Naturally, it will simplify the proof if we can restrict attention to (δ,υ):IR, i.e. pseudo-cuts that are rounded, bounded and disjoint, thereby isolating locatedness.

However, another reason for considering R as a subspace of IR is that E then becomes a nucleus in the sense of both ASD and locale theory (Definition 5.5). The latter says that idE=E2 and it preserves meets, so we have to prove that

 Φ(δ,υ) ⇔ E1Φ(δ,υ)  ⇒ EΦ(δ,υ)   and   EΦ(δ,υ) ∧ EΨ(δ,υ)  ⇒ E(Φ∧Ψ)(δ,υ),

on the assumption that (δ,υ):IR. (Only the last of these actually remains to be done.) We use Proposition 7.10 to eliminate this hypothesis, by applying E1. In Proposition 8.9 we shall deduce the equations in Lemma 5.4 from these results.

Notation 8.2 As the formula in Proposition 2.17 only involves variables ranging over Q, ΣQ and ΣΣQ×ΣQ, we may import it into the logic of ASD. However, we prefer to use

E Φ(δ,υ)  ≡   ∃ n≥ 1. ∃ q0<⋯< qn
 δ
q0
 υ
qn ∧  ⋀k=0n−1  Φ(δqk,  υqk+1),

with δ and υ instead of δ and υ, and no n≡0 term (which would be ∇). The reason is the same as for the choice of E1 in preference to E1′ or Erdb, namely that it commutes with Er and preserves ⊥ (Exercises 7.15f). Propositions 2.15 and 2.17 could be adapted to this choice by replacing I there with

 I V  ≡  {(D,U) ∣ ∃ d e u t.d< e∧ e∈ D∧[d,u]⊂ V∧ t∈ U∧ t< u}.

We have already said in Remark 6.15 that equality on Q must be decidable in order to use ASD’s methods of “discrete mathematics”. In particular, note that “∃ q0<⋯< qn” is existential quantification over List (Q), not just n+1-fold quantification over Q.

Notice that E1 is the n≡ 1 disjunct of E, so E1E.

We begin with some lemmas for managing the sequence.

Lemma 8.3 For any (δ,υ), suppose EΦ(δ,υ) holds by virtue of the sequence q0<⋯< qn, and that q0rqn. Then EΦ(δ,υ) also holds by virtue of the sequence obtained by inserting r.

Proof    If qk < r < qk+1 then Φ(δqk, υqk+1)  ⇒  Φ(δqk, υr) ∧ Φ(δr, υqk+1).         ▫

Lemma 8.4 For any Φ, and understanding that q0d and qnu, the predicate

 θ(d,u)≡∃ d< q1<⋯< qn−1< u. ⋀k=0n−1Φ(δqk,υqk+1)

is rounded, in the sense that θ(e,t)  ⇔ ∃ d u.(d< e)∧(t< u)∧θ(d,u) =⇒ e< t.

Proof    First, θ(d,u)⇒ d< u because there are d< q1<⋯< qn−1< u.

[⇐] If θ(d,u) holds by virtue of some sequence d=q0<⋯< qn=u, and d< e< t< u, then the same sequence with e and t in place of q0 and qn, but omitting any qi< e or > u, justifies θ(e,t).

[⇒] By Lemma 8.3, we may assume that n≥ 3 in the expansion of θ. The idea is to separate the left- and rightmost conjuncts from the rest, and then enlarge them using Proposition 7.12:

 θ(d,u) ⇔ ∃ d< e< t< u. Φ(δd,υe)∧θ(e,t)∧Φ(δt,υu) ⇔ ∃ c< d< e< t< u< w. Φ(δc,υe)∧θ(e,t)∧Φ(δt,υw) ⇒ ∃ c< d< u< w.θ(c,w).         ▫

This was the condition in Proposition 7.13 for θ to extend from intervals with rational endpoints to more general rounded, bounded and disjoint ones:

Lemma 8.5 If d< u then

 EΦ(δd,υu) ⇔ ∃ d< q1⋯< qn−1< u. ⋀k=0n−1 Φ(δqk,υqk+1).

Although θ(d,u)⇔⊥ when du, we shall see in Propositions 8.12 and 10.5 that, in this case,

 EΦ(δx,υx) ⇔ Φ(δx,υx)     and     EΦ(δd,υu) ⇔ ∃ x:[u,d].Φ(δx,υx).

Proof    The expansion of EΦ(δdu) involves δd q0∧υu qn≡(q0< d< u< qn). So, by Lemma 8.3, we may assume that d and u occur in the given sequence, say as dqi, uqj. But then q0,…,qi−2 and qj+2,…, qn are redundant, so without loss of generality dq1 and uqn−1. Hence by Lemma 8.4,

 EΦ(δd,υu)  ⇔ ∃ q0< d< u< qn.θ(q0,qn)  ⇔ θ(d,u).         ▫

We can now carry out the plan in Remark 8.1. The first two results say that the subspace R that will be defined by E is contained in that defined by E1, which is IR. Notice that the expansion of E1·E in the second result inherits the δ and υ from E1, so they must also be used in the definition of E in order to obtain the equation E1·E=E.

Lemma 8.6    E(E1Φ)(δ,υ)  ⇔ EΦ(δ,υ)   and   E1(EΦ)(δ,υ)  ⇔ EΦ(δ,υ).

Proof    The first part involves the conjuncts E1Φ(δqkqk+1) that occur in the expansion of the formula for E(E1Φ)(δ,υ). Such (δqkqk+1) are rounded, bounded and disjoint, so

 E1Φ(δqk,υqk+1)  ⇔ Φ(δqk,υqk+1)

by Proposition 7.12. These are the same conjuncts that are used in the expansion of EΦ(δ,υ).

In the second part, using Lemma 8.5,

E1(EΦ)(δ,υ)
∃ du.
 δ
d
 υ
uEΦ(δdu)

∃ du.
 δ
d
 υ
u∧ ∃ dq1⋯< qn−1u. ⋀k=0n−1Φ(δqkqk+1)
EΦ(δ,υ).         ▫

Lemma 8.7 E2Φ(δ,υ)=⇒EΦ(δ,υ).

Proof    The outer E of E2 involves a sequence q0<⋯< qn and conjuncts EΦ(δqkqk+1) for each 0≤ kn−1. By Lemma 8.5, the expansion of each of these involves a sequence

 qk = rk,0<⋯< rk,mk = qk+1

with conjuncts Φ(δrk,jrk,j+1). All of these sequences can be concatenated, to yield one that justifies EΦ(δ,υ).         ▫

The final preparatory result is the one that says that E is a nucleus on IR in the sense of locale theory, as well as that of ASD.

Proposition 8.8 If (δ,υ) are rounded, bounded and disjoint then

 E⊤(δ,υ)  ⇔ ⊤     and     EΦ(δ,υ) ∧ EΨ(δ,υ)  =⇒ E(Φ∧Ψ)(δ,υ).

Proof    As (δ,υ) are rounded and bounded, ⊤⇔E1⊤(δ,υ)⇒E⊤(δ,υ) by Lemma 7.7.

Suppose that EΦ and EΨ are justified by sequences q0<⋯< qn and r0<⋯< rm respectively. Let

 d ≡ max(q0,r0)    and    u≡ min(qn,rm),

so d is either q0 or r0, which both satisfy δ, so δ d holds, as similarly does υ u. Since (δ,υ) are rounded and disjoint, d< u by Lemma 7.5. Now let

 d ≡  s0< ⋯ < sℓ ≡  u

be the union of the given sequences q0<⋯< qn and r0<⋯< rm, removing duplicates and those terms < d or > u. Such outlying points were already redundant in the expansion of EΦ(δ,υ) and of EΨ(δ,υ), whilst by Lemma 8.3 we may adjoin the members of one sequence to the other. Hence the new combined sequence serves for both EΦ(δ,υ) and EΨ(δ,υ), and therefore for E(Φ∧Ψ)(δ,υ) too.         ▫

Proposition 8.9 E is a nucleus (Definition 5.5), as it satisfies, for Φ,Ψ:ΣΣQ×ΣQ,

 E(Φ∧ Ψ)  =  E(E Φ∧E Ψ)   and   E(Φ∨ Ψ)  =  E(E Φ∨E Ψ).

Proof    For (δ,υ):IR, Proposition 7.12 gives Φ(δ,υ)⇔ E1Φ(δ,υ) ⇒ EΦ(δ,υ), so

 (Φ∧Ψ)(δ,υ) ⇒  (EΦ∧EΨ)(δ,υ)     (Φ∨Ψ)(δ,υ) ⇒  (EΦ∨EΨ)(δ,υ)

and

 EΦ(δ,υ)∨EΨ(δ,υ)  ⇒  E(Φ∨Ψ)(δ,υ),

whilst

 EΦ(δ,υ)∧EΨ(δ,υ)  ⇒  E(Φ∧Ψ)(δ,υ)

by Proposition 8.8. Then we use Proposition 7.10 to eliminate the hypothesis (δ,υ):IR, and obtain the first inequality in each row:

 E1   (Φ∧  Ψ) ⊑ E1 (EΦ∧EΨ) ⊑ E (EΦ∧EΨ) E1   (Φ∨   Ψ) ⊑ E1 (EΦ∨ EΨ) ⊑ E (EΦ∨ EΨ) E1 (EΦ∧EΨ) ⊑ E1(E(Φ∧  Ψ)) ⊑ E2   (Φ∧  Ψ) ⊑ E     (Φ∧  Ψ) E1 (EΦ∨ EΨ) ⊑ E1(E(Φ∨   Ψ)) ⊑ E2   (Φ∨   Ψ) ⊑ E     (Φ∨   Ψ).

The second inequality follows from E1E, and the third, E2E, is Lemma 8.7. Finally, from each E1Θ⊑EΩ, we deduce EΘ=E(E1Θ)⊑E2Ω⊑EΩ by Lemmas 8.6 and 8.7.         ▫

This fulfils the obligation that we have before invoking the ASD technology in Section 5, so we can now introduce the type R≡{ΣΣQ×ΣQE}. We still have to characterise its admissible terms, i.e. to show that the equalisers in Remarks 5.2 and 6.9 are isomorphic.

The following is the main lemma to do this. In it, (δ,υ) need not be disjoint, so it may represent a back-to-front interval like those in Remark 2.20, which we shall use to compute existential quantifiers. In the proof, we have to switch back from using abutting closed intervals to overlapping open ones, cf. the proof of Proposition 2.17.

Lemma 8.10 If (δ,υ) is located then EΦ(δ,υ) ⇔ E1Φ(δ,υ).

Proof    [⇐] is trivial. For [⇒], we use Proposition 7.12 to widen the argument of each conjunct Φ a little towards the right, from [qk,qk+1] to [qk,rk+1], for any qk+1< rk+1< qk+2:

EΦ(δ,υ)
∃ q0<⋯< qn.
 δ
q0
 υ
qn∧ ⋀k=0n−1 Φ(δqkqk+1)

∃ q0r0q1r1<⋯ < qnrn.
 δ
q0
 υ
rn∧ ⋀k=0n−1 Φ(δqkrk+1),

where υ qnυ rn because υ is upper. As (δ,υ) is located with δ q0 and υ rn, we may apply Lemma 6.16 to this sequence. Because of the alternation of letters, it gives

k=0n−1(
 δ
qk
 υ
qk+1)  ∨ ⋁k=0n−1(
 δ
rk
 υ
rk+1).

We already have the corresponding Φ(δqkqk+1) from the original abutting expansion, whilst the one with overlapping intervals provides

 Φ(δqk,υrk+1)  =⇒  Φ(δrk,υrk+1),

since δqk⊑δrk. Hence, with eqk< tqk+1 or erk< trk+1, we have

EΦ(δ,υ)  =⇒  ∃ et.
 δ
e
 υ
t∧ Φ(δet)  ≡  E1Φ(δ,υ).         ▫

Lemma 8.11 If (δ,υ) is rounded and bounded, and EΦ(δ,υ)=⇒E1Φ(δ,υ) for all Φ, then (δ,υ) is located.

Proof    For any d< u, there is a sequence of rationals

 q0< d< q1< u< q2   with   δ q0   and   υ q2.

These numbers satisfy δq0d⇔⊥, υq1u⇔⊤, δq1d⇔⊤ and υq2u⇔⊥, so

 ∃ q0< q1< q2. δ q0 ∧ υ q2  ∧ (δq0d∨υq1u)  ∧ (δq1d∨υq2u).

This is the n≡ 2 disjunct of EΦ(δ,υ), where Φ(α,β)≡α d∨β u. By hypothesis, this implies E1Φ(δ,υ), where

 E1Φ(δ,υ) ≡ ∃ e< t.δ e∧υ t∧Φ(δe,υt) ≡ ∃ e< t.δ e∧υ t∧(d< e∨ t< u)   ⇒  δ d∨υ u.         ▫

Proposition 8.12 (δ,υ) is a cut iff it is admissible for E.

Proof    If it’s a cut then in particular it’s rounded, bounded and disjoint, so Φ(δ,υ)⇔E1Φ(δ,υ) by Proposition 7.12. As it’s also located, EΦ(δ,υ)⇔E1Φ(δ,υ) by Lemma 8.10, so (δ,υ) is admissible.

Conversely, admissibility of (δ,υ) for E with respect to both Φ and E1Φ, give

 Φ(δ,υ) ⇔ EΦ(δ,υ)  ⇔ E(E1Φ)(δ,υ) ⇔ E1Φ(δ,υ),

where the middle implication is Lemma 8.6. Hence (δ,υ) is also admissible for E1, so it is rounded, bounded and disjoint by Theorem 7.14. It is also located, by Lemma 8.11.         ▫

Theorem 8.13 The type R≡{ΣΣQ×ΣQE} is the equaliser in Remark 6.9, i.e. its terms are Dedekind cuts, and the inclusion R↣ΣΣQ×ΣQ is Σ-split.         ▫

In the following two sections, we shall show that this construction does make the real line Dedekind-complete and the closed interval compact.   