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 E₁ on Σ^Q×Σ^Q, is the same as giving a nucleus E on the larger space for which

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 id⊑E=E² and it preserves meets, so we have to prove that

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 E₁. 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

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

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 “∃ q₀<⋯< q_n” is existential quantification over List (Q), not just n+1-fold quantification over Q.

Notice that E₁ is the n≡ 1 disjunct of E, so E₁⊑E.

We begin with some lemmas for managing the sequence.

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

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

Lemma 8.4 For any Φ, and understanding that q₀≡ d and q_n≡ u, the predicate

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< q₁<⋯< q_n−1< u.

[⇐] If θ(d,u) holds by virtue of some sequence d=q₀<⋯< q_n=u, and d< e< t< u, then the same sequence with e and t in place of q₀ and q_n, but omitting any q_i< 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:

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

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

Proof    The expansion of EΦ(δ_d,υ_u) involves δ_d q₀∧υ_u q_n≡(q₀< d< u< q_n). So, by Lemma 8.3, we may assume that d and u occur in the given sequence, say as d≡ q_i, u≡ q_j. But then q₀,…,q_i−2 and q_j+2,…, q_n are redundant, so without loss of generality d≡ q₁ and u≡ q_n−1. Hence by Lemma 8.4,

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 E₁, which is IR. Notice that the expansion of E₁·E in the second result inherits the δ and υ from E₁, so they must also be used in the definition of E in order to obtain the equation E₁·E=E.

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

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

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,

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

Proof    The outer E of E² involves a sequence q₀<⋯< q_n and conjuncts EΦ(δ_qk,υ_qk+1) for each 0≤ k≤ n−1. By Lemma 8.5, the expansion of each of these involves a sequence

with conjuncts Φ(δ_rk,j,υ_rk,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

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

Suppose that EΦ and EΨ are justified by sequences q₀<⋯< q_n and r₀<⋯< r_m respectively. Let

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

be the union of the given sequences q₀<⋯< q_n and r₀<⋯< r_m, 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,

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

and

whilst

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

The second inequality follows from E₁⊑E, and the third, E²⊑E, is Lemma 8.7. Finally, from each E₁Θ⊑EΩ, we deduce EΘ=E(E₁Θ)⊑E²Ω⊑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×ΣQ ∣ E}. 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Φ(δ,υ) ⇔ E₁Φ(δ,υ).

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

where υ q_n⇒υ r_n because υ is upper. As (δ,υ) is located with δ q₀ and υ r_n, we may apply Lemma 6.16 to this sequence. Because of the alternation of letters, it gives

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

since δ_qk⊑δ_rk. Hence, with e≡ q_k< t≡ q_k+1 or e≡ r_k< t≡ r_k+1, we have

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

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

These numbers satisfy δ_q0d⇔⊥, υ_q1u⇔⊤, δ_q1d⇔⊤ and υ_q2u⇔⊥, so

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

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 Φ(δ,υ)⇔E₁Φ(δ,υ) by Proposition 7.12. As it’s also located, EΦ(δ,υ)⇔E₁Φ(δ,υ) by Lemma 8.10, so (δ,υ) is admissible.

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

where the middle implication is Lemma 8.6. Hence (δ,υ) is also admissible for E₁, 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×ΣQ ∣ E} 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.