Equideductive Topology

Paul Taylor

15 February 2011

Abstract We introduce a new, two-level, logical calculus for open and general subspaces in computable general topology. The leading model is the category of all sober topological spaces.

In [equdcl] the “external” logic was motivated by equalisers targeted at exponentials in an enclosing cartesian closed category. It was developed into a “predicate calculus” with universally quantified implications between equations between lambda terms. A kind of existential quantifier may also be defined.

Here we ask when the fundamental object of this category is a dominance and show how this question leads to an “internal” logic of open subspaces. Discrete, compact, overt and Hausdorff spaces are those form which the external (in)equality or quantifier is represented by a lambda term.

In particular, the category is a topos if this representation always exists, i.e. the external and internal logics coincide.

                      www.PaulTaylor.EU/ASD/equideductive/

1 A language for topology

Equideductive topology is a new language for computable general topology. Whereas Abstract Stone Duality provided an account of locally compact spaces, the leading model of the new theory is the category of all sober topological spaces (in the traditional sense). See Equideductive Categories and their Logic for a general introduction to the equideductive topology programme.

The programme is motivated by analogies with the way in which the notion of an elementary topos captures set theory in categorical form. Recall that a topos has an object Ω with an internal algebraic structure that classifies subobjects and their logic in the category. In set theory there is only one notion of subset, but in topology we have both open subspaces and general ones. As is now well known, the properties of Ω in a topos may be adapted to describe open subspaces in topology.

In order to provide a theory of general subspaces, we must re-examine the external logic of subobjects in a category, following the situation in a topos but without relying on the internal algebraic structure of Ω (here re-named Σ). This was done in [equdcl] by axiomatising equalisers targeted at exponentials, E ↪ X ⇉ Σ^{Y}, which led to a logic with ∀ and =▷ that was based on equations between λ-terms of type Σ. Then it was shown in [existential] how an existential quantifier could be defined from the universal one. This agrees with the epis in the category but only satisfies the usual logical rules with severe restrictions, for which reason it was written with an unusual symbol, �.

There is also a cartesian closed extension. In fact, it was by asking what logic is needed to perform Scott’s construction of equilogical spaces that I was led to equideductive logic in the first place. Briefly, an equideductive category is one that “lies nicely” within its cartesian closed extension. This extension is therefore with us “in spirit”, even though we only consider the smaller category explicitly here.

In this paper we add a single axiom to the basic logic, namely what is required to make the object Σ a dominance, classifying “open” subobjects. This new axiom has the effect of adding internal algebraic structure to Σ that is related to the external structure as follows:

external: ⊤ & ∀ =▷ ⊥ ⋎ �
internal: ⋆ ∧ U ⩽ ⊥ ∨ ∃

By this we mean that, in some cases, the external logic is represented by terms of type Σ in the internal one. In Section 9 we shall show that, if we do this in all cases, we recover set theory in the sense that the category is a topos.

But by making this identification in just some cases, we obtain a theory that has many of the features of general topology and provides several of its definitions:

(a) an open subspace is one whose defining predicate is represented by a term of type Σ (Section 3);

(b) a discrete space is one whose (Leibnizian) equality between incoming morphisms is represented by a term of type Σ (Section 4);

(c) a compact space is one for which the equideductive universal quantifier ∀ for predicates is represented by a term (Section 5);

(d) an overt space is one for which the equideductive existential quantifier � for predicates is represented by a term (Section 7).

2 Equideductive logic

See Equideductive Categories and their Logic for both the general introduction to the equideductive topology programme and also the foundations of the logic.

Remark 2.1 Equideductive predicates are formed as conjunctions of quantified implications of the form

∀y⃗. 𝔮⃗ (y⃗) =▷ (αx⃗y⃗ = βx⃗y⃗),

where the 𝔮⃗(y⃗) are in a similar form. The equations on the right are between λ-terms of type Σ.

Several definitional extensions were made in [equdcl] and [existential] and more will be added in this paper, but any predicate may be rewritten in this normal form.

The symbols ∀, =▷ and & obey the usual rules, except that predicates must obey the variablebinding rule: any variable that occurs on the left of =▷ must be bound by the quantifier. This rule arises from the categorical use of this notation for an equaliser targeted at an exponential. The restriction is also essential to some of the results in the two logically preceding papers. However, we shall find here that it can be relaxed to one level for antecedents of the form ϕx = ⊤ and to arbitrary depth for variables of discrete type.

3 Classifying open subspaces

In set theory, arbitrary subobjects (monos) U ↪ X are classified by (maps ϕ : X → Ω to) the object Ω of an elementary topos that was introduced by Bill Lawvere and Myles Tierney [?, ?].

[figure: U; 1; X; i; ∩; ϕ; Σ or Ω; ⊤]

Giuseppe Rosolini generalised this for topology and recursion theory by considering a class (“dominion”) of special (“open”) monos that must be closed under composition and inverse images. Then Ω is replaced by an object (“dominance”) Σ that is to have the same classification property [?]. The key point is that not all monos need be expressible in this form in Rosolini’s generalisation, but if U ↪ X is expressible then there is a unique ϕ : X → Σ that provides this pullback.

Lemma 3.1 Any dominance Σ carries a semilattice structure (⊤, ∧), where ⊤ classifies the whole object and ϕ ∧ ψ classifies the intersection (pullback) ϕ^{−1}(⊤) ∩ ψ^{−1}(⊤). Any semilattice carries an order relation ⩽ such that

α ⩽ β  ≡ α ∧ β = α
α ∧ β = ⊤ ⊣⊢ α = ⊤ & β = ⊤
α = β  ⊣⊢ α ⩽ β & β ⩽ α.

Proof See, e.g., [geohol,§2] for the diagrams and further introduction. □

Remark 3.2 The equations on the right of =▷ in the normal form for equideductive predicates (Remark 2.1) are between terms of urtype Σ. Now that this object is a semilattice it is more convenient to use inequalities like

∀y⃗. 𝔮⃗ (y⃗) =▷ (αx⃗y⃗ ⩽ βx⃗y⃗)

instead as the standard form for predicates. In fact, we shall see in this section that ⩽ is itself a special case of =▷.

Remark 3.3 Conversely to Lemma 3.1, given a semilattice (Σ, ⊤, ∧) in a category with all finite limits, we may define the “open” inclusions i : U ↪ X to be exactly those that can be expressed as pullbacks of ⊤ : 1 → Σ along maps ϕ : X → Σ. (Recall that an equideductive category has all finite limits.) Open inclusions therefore automatically have inverse images, where f^{−1}(U) is classified by ϕ · f, whilst the inverse image of ⊤ : X → 1 → Σ is the entire subobject X ⊂ X.

However, we still also need

(a) (the isomorphism class of) U ↪ X to determine ϕ uniquely (up to equality) and

(b) any composite V ↪ U ↪ X of open inclusions also to be expressible in this way. It is more convenient to generalise the first property to a relationship between inclusions U ⊂ V

and inequalities ϕ ⩽ ψ:

Lemma 3.4 If (Σ, ⊤, ∧) is a dominance in an equideductive category then it also satisfies the rule

x : A, 𝔭(x), ϕx = ⊤ ⊢ ψx = ⊤ = x : A, 𝔭(x) ⊢ ϕx ⩽ ψx for any terms ⊢ ϕ, ψ : Σ^{A} without parameters, where 𝔭(x) is a predicate on the urtype A. Proof Such terms define parallel morphisms ϕ, ψ : X ⇉ Σ with pullbacks U, V ⊂ X as shown:

[figure: U ≡ {x : A | 𝔭(x) & ϕx = ⊤}; .; .; .; .; .; .; .; .; .; .; .; V ≡ {x : A | 𝔭(x) & ψx = ⊤}; 1; X ≡ {x : A | 𝔭(x)}; i; ∩; = = = = = =; X ≡ {x : A | 𝔭(x)}; j; ∩; ψ; ϕ; Σ; ⊤]

The premise of the rule says that the identity on the urtype A represents is a morphism U → V. Hence U ≅ U ∩ V, where this intersection is classified by ϕ ∧ ψ by Lemma 3.1. Then ϕ = ϕ ∧ ψ since classifiers are unique, so ϕ ⩽ ψ. □

Since this argument is reversible, we have the converse:

Remark 3.5 If Σ in an equideductive category is a semilattice and obeys this rule then the “open” monos that it generates according to Remark 3.3 are uniquely classified. However, in this we mean that the morphism X ≡ {A | 𝔭} → Σ, rather than the term A → Σ that represents it, is unique. Terms ⊢ ϕ, ψ : Σ^{A} represent the same morphism X → Σ and classify the same open inclusion U ↪ X if

x : A, 𝔭(x) ⊢ ϕx = ψx : Σ.  □

Finally, injectivity of Σ and its semilattice structure provide composition of open inclusions:

Lemma 3.6 If the object Σ in an equideductive category is a semilattice and satisfies the rule in Lemma 3.4 then it is a dominance. Proof It remains to show that if ϕ : V → Σ classifies the inclusion U ↪ V (top right) and ψ : X → Σ classifies V ↪ U (bottom left) then the composite U ↪ V ↪ X also has a classifier (right-hand rectangle).

[figure: Γ; .; .; .; .; .; .; .; .; .; .; u; U ≡ {x : A | 𝔭(x) & ϕx = ⊤ & ψx = ⊤}; !; 1]
[figure: x; ...........................; v]
[figure: 1; !; V ≡ {x : A | 𝔭(x) & ψx = ⊤}; i; ∩; ϕ; Σ; ⊤]

[figure: Σ; ⊤; ψ; X ≡ {x : A | 𝔭(x)}; j; ∩; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ϕ ∧ ψ; Σ; ‖]

Using injectivity of Σ, which is one of the axioms of an equideductive category, the map ϕ : V → Σ lifts to X → Σ. I claim that ϕ ∧ ψ : X → Σ classifies U ⊂ X.

Let x : Γ → U and ! : Γ → 1 have equal composites as far as Σ, i.e.

Γ ⊢ x : {A | 𝔭} with Γ ⊢ 𝔭(x), ϕx ∧ ψx = ⊤.

Then ϕx = ⊤ and ψx = ⊤ by Lemma 3.1. Since V is classified by ψ, we have x = j · v for some unique v : Γ → V. Then ϕv = ϕx = ⊤, so v = i · u for some unique u : Γ → U since ϕ classifies U.

Hence x = j · i · u as required and u is unique since i and j are monos. The classifier ϕ ∧ ψ is unique by Lemma 3.4. □

Axiom 3.7 The open Gentzen rule is

Γ, α = ⊤ ⊢ β ⩽ γ = Γ ⊢ α ∧ β ⩽ γ

for any terms Γ ⊢ α, β, γ : Σ that may now contain parameters and depend on predicates.

Theorem 3.8 The fundamental object Σ of an equideductive category is a dominance iff it carries a semilattice structure that satisfies the open Gentzen rule. Proof The rule in Lemma 3.4 is the special case of the new one where ϕ ≡ α, β ≡ ⊤ and ψ ≡ γ, so it remains to derive the Gentzen rule from the Lemma.

For definiteness, and since equideductive logic has products of urtypes, let the context Γ be [x : A, 𝔮(x)] and write the terms as αx, βx and γx. Then the judgements

x : A, 𝔮(x), αx = ⊤  ⊢ βx ⩽ γx
x : A, 𝔮(x), αx = ⊤, βx = ⊤ ⊢ γx = ⊤
x : A, 𝔮(x), αx = ⊤ & βx = ⊤ ⊢ γx = ⊤
x : A, 𝔮(x), (αx ∧ βx) = ⊤  ⊢ γx = ⊤
x : A, 𝔮(x)  ⊢ (αx ∧ βx) ⩽ γx

are equivalent: The first two lines are linked (upside down) by the version of the rule in Lemma 3.4 with 𝔭(x) ≡ 𝔮(x) & (αx = ⊤), ϕ ≡ β and ψ ≡ γ. Similarly, the last two lines use it (the right way up) with 𝔭 ≡ 𝔮, ϕ ≡ α ∧ β and ψ ≡ γ. The middle three lines use Lemma 3.1 about & and ∧. □

Corollary 3.9 This rule entails the Euclidean principle,

σ : Σ, F : Σ^{Σ} ⊢ σ ∧ F σ = σ ∧ F ⊤.

Proof By the equality-transmission law λE=_{1} we have σ = ⊤ ⊢ F σ = F ⊤. From this we deduce σ ∧ F σ ⩽ F ⊤ and σ ∧ F ⊤ ⩽ F σ by the open Gentzen rule. See [geohol, §3] for a diagrammatic proof of this from Rosolini’s notion of a dominance. □

Lemma 3.10 Then open inclusion i : U ↪ X classified by ϕ is Σ-split by (−) ∧ ϕ. Proof According to the definition in [equdcl], we require

x : A, θ : Σ^{A}, 𝔭(x), ϕx = ⊤ ⊢ Iθ(ix) ≡ θx ∧ ϕx = θx
θ, θ′ : Σ^{A}, ∀x. 𝔭(x) & (ϕx = ⊤) =▷ θx = θ′x ⊢ ∀x. 𝔭(x) =▷ ϕx ∧ θx = ϕx ∧ θ′x,

which follow from the open Gentzen rule. □

Recall that the variable-binding rule of equideductive logic (Remark 2.1) required all variables on the left of =▷ to be bound by ∀. This would appear to limit the scope of this notation to closed terms on the left of ⩽, but we find that this is not the case:

Proposition 3.11 Open antecedents are exempt from the variable-binding rule.

Proof Using the Gentzen rule and those for ∀ =▷, the judgements

𝔪(x), 𝔭(y),  αxy = ⊤ ⊢ ∀z. 𝔮(z) =▷ (βxyz ⩽ γxyz)
𝔪(x), 𝔭(y), 𝔮(z), αxy = ⊤ ⊢ βxyz ⩽ γxyz
𝔪(x), 𝔭(y), 𝔮(z)  ⊢ (αxy ∧ βxyz) ⩽ γxyz
𝔪(x)  ⊢ ∀yz. 𝔭(y) & 𝔮(z) =▷ (αxy ∧ βxyz) ⩽ γxyz

are equivalent. Hence we may make a definitional extension of equideductive logic in which the right hand side of the last line defines

∀y. 𝔭(y) & αxy =▷ (∀z. 𝔮(z) =▷ (βxyz ⩽ γxyz)),

which is the key case in the recursive definition of a general implication from an open predicate with a free variable x (Remark 3.2). □

Warning 3.12 This exemption only postpones binding the variable by one level. Since equideductive predicates are built up from open ones (terms of type Σ) using the logical connectives, relaxing the variable-binding rule for them at arbitrary levels would eliminate it altogether, but then it would not be valid in the category of sober topological spaces.

Example 3.13 With B ≡ C ≡ 1, 𝔭 ≡ 𝔮 ≡ ⊤, α ≡ ϕ, β ≡ ⊤ and γ ≡ ψ,

(ϕx = ⊤) =▷ (ψx = ⊤) is defined as ϕx ⩽ ψx or ϕx = ϕx ∧ ψx.

It would be tempting to use this equivalence as the axiom that is the subject of this section. However, without the Proposition, it would violate the variable-binding rule. Moreover, it is not justified â priori by Lemma 3.4 because the variables x above and below the line in the rule there are quantified separately.

Notation 3.14 The foregoing results justify identifying

(a) any term x : A ⊢ ϕx : Σ with the predicate 𝔭(x) ≡ (ϕx = ⊤) on A, in which case we call 𝔭(x) an open predicate and {A | 𝔭} ⊂ A an open subspace;

(b) in particular, the term ⊤ : Σ with the true equideductive predicate;

(c) the semilattice operation ∧ on Σ with (a special case of) equideductive conjunction &; and (d) the order relation ⩽ on Σ with (a special case of) equideductive implication =▷. So, for example, the equivalent judgements in the Theorem are all written Γ ⊢ α & β =▷ γ and the normal form for a predicate in Remark 3.2 becomes

𝔭(x⃗) ≡ ∀y⃗. 𝔮⃗ ( y⃗) & α x⃗ y⃗ =▷ β x⃗ y⃗.

4 Discrete spaces

The next part of the external logic that we identify with an internal form is equality. Even as a predicate, this is not primitive in equideductive logic for general urtypes: it is defined from equality on Σ using the Leibnizian formula

x = y ≡ ∀ϕ. (ϕx = ϕy).

Definition 4.1 A space N ≡ {x : A | 𝔭(x)} is discrete if this formula is represented by an term ϵ : Σ^{A×A},

x, y : A, 𝔭(x), 𝔭(y) ⊢ (ϵxy = ⊤) ◁=▷ ∀ϕ. (ϕx = ϕy),

which we call internal equality. In this paper we retain the ϵ for the internal equality for clarity, but afterwards we will write x = y instead, even though this will make the notation ambiguous.

Lemma 4.2 The term ϵ is the internal equality for the discrete object N ≡ {x : A | 𝔭(x)} iff it satisfies reflexivity and substitution:

x : A, 𝔭(x)  ⊢ ϵxx
x, y : A, ϕ : Σ^{A}, 𝔭(x), 𝔭(y) ⊢ ϵxy ∧ ϕx =▷ ϕy.

In this case, ϵ is also symmetric and transitive:

x, y : A, 𝔭(x), 𝔭(y)  ⊢ ϵxy =▷ ϵyx
x, y, z : A, 𝔭(x), 𝔭(y), 𝔭(z) ⊢ ϵxy ∧ ϵyz =▷ ϵxz.

Proof Reflexivity follows from the backward direction of the Definition and substitution from the forward one. We deduce symmetry from these using ϕ ≡ λw. ϵwx and transitivity using ϕ ≡ λw. ϵwz. Substitution gives ϵxy =▷ ∀ϕ. ϕx =▷ ϕy and hence by symmetry the Definition. □

Remark 4.3 More precisely, the Lemma is about representability of the Σ-order,

x ⊑ y ≡ ∀ϕ. ϕx =▷ ϕy,

but the symmetry result shows that if this order is representable then it is discrete anyway.

Proposition 4.4 Any predicate respects internal equality:

x, y : A, 𝔭(x), 𝔭(y), 𝔯(x), ϵxy ⊢ 𝔯(y).

Proof By Notation 3.14, it suffices to consider

𝔯(x) ≡ ∀z. 𝔰(z) & αzx =▷ βzx.

Then, for x, y : A with 𝔭(x), 𝔭(y) and ϵxy and z with 𝔰(z), the second rule for ϵ gives

αzy =▷ αzx =▷ βzx =▷ βzy,

so the result follows using ∀I and ∀E. □

Proposition 4.5 Variables of discrete type are exempt from the variable-binding rule, where

∀y⃗. 𝔯(x, y⃗) =▷ 𝔰(x, y⃗, z⃗) is defined as ∀x′y⃗. 𝔭(x′, y⃗) & 𝔯(x′) & ϵxx′ =▷ 𝔰(x, y⃗, z⃗).

Unlike the case of open predicates, this exemption is valid to any depth, in any kind of sub-formula, not just open ones. Proof As in Proposition 3.11, we mean that there is a definitional extension of equideductive logic. The judgements

𝔱⃗(z⃗), 𝔭(x),  𝔯(x, y⃗) ⊢ 𝔰(x, y⃗, z⃗)
𝔱⃗(z⃗), 𝔭(x), 𝔭(x′), ϵxx′, 𝔯(x, y⃗) ⊢ 𝔰(x, y⃗, z⃗)
𝔱⃗(z⃗), 𝔭(x), 𝔭(x′), ϵxx′, 𝔯(x′, y⃗) ⊢ 𝔰(x, y⃗, z⃗)
𝔱⃗(z⃗), 𝔭(x)  ⊢ ∀x′. 𝔭(x′) & 𝔯(x′, y⃗) & ϵxx′ =▷ 𝔰(x, y⃗, z⃗)

are equivalent, where the last formula is well formed by Proposition 3.11 because ϵxx′ is an open predicate. The first line entails the second by weakening and conversely by contraction and reflexivity of ϵ. The second and third lines are equivalent by the previous lemma. The last two lines are equivalent by the rules for ∀ =▷. □

Remark 4.6 This result could be the basis of a theory of dependent types in which the spaces may have discrete (or Hausdorff) parameters.

Discreteness also has a categorical meaning:

Proposition 4.7 An object N of an equideductive category is discrete iff the diagonal N → N ×N is an open inclusion,

[figure: N ≡ {x : A | 𝔭(x)}; 1; N × N; ∩; ϵ; Σ.; ⊤]

classified by the term ϵ. Proof Discreteness is equivalent to the property

x, y : A, , 𝔭(x), 𝔭(y), ϵxy ⊢ x = y.

This in turn is exactly what is required to make the diagonal and either of the projections into an isomorphism

N ≡ {x : A | 𝔭(x)} ≅ {N × N | ϵ} ≡ {x, y : A | 𝔭(x) & 𝔭(y) & ϵxy = ⊤}.  □

Corollary 4.8 The internal equality ϵ is unique in the sense of Remark 3.5. □

Lemma 4.9 Let M be a discrete space and f : N → M a morphism. If N is also discrete then internal equality is preserved:

x, y : A, 𝔭(x), 𝔭(y) ⊢ ϵ_{N}xy =▷ ϵ_{M}(fx)(fy).

If f is mono then N is discrete, with ϵ_{N}xy ≡ ϵ_{M}(fx)(fy). Proof In both parts, x = y ⊢ fx = fy ⊣⊢ ϵ_{M}(fx)(fy) = ⊤. If N is discrete, let ϕ ≡ λw. ϵ_{M}(fx)(fw) in Lemma 4.2. If f is mono, the first ⊢ is ⊣⊢, so ϵ_{M}(fx)(fy) serves for ϵ_{N}xy. □

Examples 4.10

(a) 1 is discrete, with ϵ_{1} ≡ λxx′. ⊤;

(b) if N and M are discrete then so is M × M, with ϵ_{N×M}⟨x, y⟩⟨x′, y′⟩ ≡ ϵ_{N}xx′ ∧ ϵ_{M}yy′;

(c) for 0 and sums we require the lattice structure on Σ (Section 6);

(d) Σ is discrete iff it is an internal Heyting algebra (Proposition 9.8).

Remark 4.11 Points and the diagonal of a discrete space are open, but arbitrary subspaces are not.

5 Compact spaces

Next we consider those objects for which the equideductive quantifier ∀ for predicates is represented by an term.

Definition 5.1 The type K ≡ {A | 𝔭} is compact if there is an term ⊢ □ : Σ^{Σ^{A}} such that

ϕ : Σ^{A} ⊢ (∀x:A. 𝔭(x) =▷ (ϕx = ⊤)) ◁=▷ (□ ϕ) = ⊤.

We call the term □ a necessity operator but later we shall write Ux:K. ϕx for □ ϕ.

Lemma 5.2 The necessity operator □ for a compact space is unique. Proof Compactness says that the subspace {ϕ : Σ^{A} | ∀x. 𝔭(x) =▷ ϕx} ↪ Σ^{A} is open and that □ classifies it. However, unlike in Remark 3.5, the term is unique up to λ-equality, without an equivalence relation. [geohol, 7.11]. □

Lemma 5.3 The Definition is equivalent to the more general form

ϕ : Σ^{A}, σ : Σ ⊢ (∀x:A. 𝔭(x) =▷ (σ ⩽ ϕx)) ◁=▷ (σ ⩽ □ ϕ),

so in this sense □ ϕ = ⋀ {ϕx | 𝔭(x)}. Proof We deduce the σ-form from its special case with σ ≡ ⊤ by

σ = ⊤, (∀x. 𝔭(x) =▷ σ ⩽ ϕx) ⊢ ∀x. 𝔭(x) =▷ ⊤ ⩽ ϕx ⊢ □ ϕ = ⊤
σ ⩽ □ ϕ, 𝔭(x), σ ⊢ □ ϕ, 𝔭(x) ⊢ ϕx = ⊤

together with the ∀- and open Gentzen rules. □

Corollary 5.4 The term □ makes K ≡ {A | 𝔭} compact iff

for Γ ⊢ ϕ : Σ^{A} and Γ ⊢ σ : Σ,  Γ, x : A, 𝔭(x) ⊢ σ ⩽ ϕx ; = ; Γ ⊢ σ ⩽ □ ϕ

The forward direction of the Definition gives the introduction rule for □ considered as a quantifier,

ϕ : Σ^{A}, ∀x. 𝔭(x) =▷ ϕx ⊢ □ ϕ

and the backward direction gives the elimination rule:

x : A, ϕ : Σ^{A}, 𝔭(x), □ ϕ ⊢ ϕx.  □

Lemma 5.5 Necessity operators commute. Proof Let K ≡ {A | 𝔭} and L ≡ {B | 𝔮} be compact spaces with necessity operators [𝔭] and [𝔮]. Using Definition 5.1,

[𝔭](λx. [𝔮](λy. θxy)) = ⊤ ⟺ ∀x. 𝔭(x) =▷ ([𝔮](λy. θxy) = ⊤)
⟺ ∀x. 𝔭(x) =▷ (∀y. 𝔮(y) =▷ (θxy = ⊤))
⟺ ∀xy. 𝔭(x) & 𝔮(y) =▷ (θxy = ⊤)
⋯  ⟺ [𝔮](λy. [𝔭](λx. θxy)) = ⊤

using the definition of ∀x. 𝔭(x) =▷ (∀y. · · ·). Alternatively, using Lemma 5.3,

σ ⩽ [𝔭](λx. [𝔮](λy. θxy)) ⟺ ∀x. 𝔭(x) =▷ (σ ⩽ [𝔮](λy. θxy))
⟺ ∀x. 𝔭(x) =▷ (∀y. 𝔮(y) =▷ (σ ⩽ θxy))
⟺ ∀y. 𝔮(y) =▷ (∀x. 𝔭(x) =▷ (σ ⩽ θxy))
⟺ σ ⩽ [𝔮](λy. [𝔭](λx. θxy)).  □

Corollary 5.6 If K and L are compact then so is K × L. Proof The formulae in the preceding proof are also equivalent to

∀xy. 𝔭(x) & 𝔮(y) =▷ (σ ⩽ θxy),

so the double quantifier provides that for the product. □

Lemma 5.7 □ ⊤ = ⊤ and □(ϕ ∧ ψ) = □ ϕ ∧ □ ψ. Proof These are also corollaries of Lemma 5.5, with L ≡ 0 and L ≡ 2. Briefly,

σ ⩽ □(ϕ ∧ ψ) ⊣⊢ (∀x. 𝔭(x) =▷ (σ ⩽ ϕx)) & (∀x. 𝔭(x) =▷ (σ ⩽ ψx))
⊣⊢ σ ⩽ (□ ϕ ∧ □ ψ).  □

Proposition 5.8 If K ≡ {A | 𝔭} and L ≡ {B | 𝔮} are compact spaces with necessity operators [𝔭] and [𝔮] then K + L is also compact. Its necessity operator is given by

□ θ ≡ [𝔭](θ · ν_{0}) ∧ [𝔮](θ · ν_{1}).

Proof By the properties of coproducts in the � paper,

∀z:K + L. σ ⩽ θz ⊣⊢ ∀x. 𝔭(x) =▷ σ ⩽ θ(ν_{0}x) & ∀y. 𝔮(y) =▷ σ ⩽ θ(ν_{1}y)
⊣⊢ σ ⩽ [𝔭](θ · ν_{0}) & σ ⩽ [𝔮](θ · ν_{1})
⊣⊢ σ ⩽ [𝔭](θ · ν_{0}) ∧ [𝔮](θ · ν_{1}).  □

Example 5.9 The types 0, 1 and 2 are compact, with

[0] ≡ ⊤,  [1]ϕ ≡ (ϕ⋆) and [2]ϕ ≡ (ϕ0 ∧ ϕ1).  □

Lemma 5.10 The term □ : Σ^{Σ^{A}} satisfies 𝔭̄(□). Proof Let ϕ, ψ : Σ^{A} satisfy ∀x. 𝔭(x) =▷ (ϕx = ψx). Then

□ ψ ⩽ □ ψ ⊢ ∀x. 𝔭(x) =▷ □ ψ ⩽ ψx
⊢ ∀x. 𝔭(x) =▷ □ ψ ⩽ ϕx ⊢ □ ψ ⩽ □ ϕ

and similarly □ ψ ⩽ □ ψ so □ ϕ = □ ψ. □

Notation 5.11 Conversely, for any term ⊢ □ : Σ^{Σ^{A}}, define

𝔨(x) ≡ ∀ϕ:Σ^{A}. □ ϕ ⇒ ϕx and K ≡ {x : A | 𝔨(x)}.

Lemma 5.12 If □ is the necessity operator for {x : A | 𝔭(x)} then 𝔭 ⊢ 𝔨 and □ is also the necessity operator for {x : A | 𝔨(x)}, which is called the saturation of the given space. Proof Covariance of the rules. □

Lemma 5.13 The term ⊢ □ : Σ^{Σ^{A}} is the necessity operator for some space iff

ϕ : Σ^{A}, ∀x. (∀ψ. □ ψ =▷ ψx) =▷ ϕx ⊢ □ ϕ.

In this, since □ ψ is an open sub-formula, □ need not be bound with ∀ψ, but it does have to be bound with ∀x. That is, it can only have discrete or Hausdorff parameters, cf. Remark 4.6. This condition is idempotent. Note, however, that □ occurs covariantly on the left. □

6 Lattice structure

Next we identify equideductive falsity and disjunction with the least element and lattice disjunction operation on Σ. Note that the results in this section are still valid in any topos.

Axiom 6.1 The object Σ is a distributive lattice.

Remark 6.2 Coproducts of discrete spaces.

7 Overt spaces

Just as Section 5 defined a compact space to be one for which the equideductive universal quantifier ∀ is represented by a term □, so an overt space has a term ♢ that represents the equideductive existential quantifier �. However, we saw in [exiqt] that working with � is extremely delicate because it does not obey all of the usual rules. Indeed, representability of � appears to be weaker than the property that ♢ is a join that is dual to Lemma 5.3.

Definition 7.1 A space N ≡ {A | 𝔭} is overt if there is an term ⊢ ♢ : Σ^{Σ^{A}}, called a possibility operator, such that

ϕ : Σ^{A}, σ : Σ ⊢ (♢ ϕ ⩽ σ) ◁=▷ (∀x:A. 𝔭(x) =▷ (ϕx ⩽ σ)),

so in this sense ♢ ϕ = ⋁ {ϕx | 𝔭(x)}. Later we shall write ∃x:N . ϕx for ♢ ϕ.

Lemma 7.2 The space N ≡ {A | 𝔭} is overt with possibility operator ♢ iff

for terms Γ ⊢ ϕ : Σ^{X} and Γ ⊢ σ : Σ,  Γ, x : A, 𝔭(x) ⊢ ϕx ⩽ σ ; = ; Γ ⊢ ♢ ϕ ⩽ σ

In particular, 𝔭(x) & ϕx =▷ ♢ ϕ. Proof The top line is Γ ⊢ ∀x. 𝔭(x) =▷ ϕx ⩽ σ. We obtain the Lemma from the Definition using cuts to substitute formulae for the variables σ and ϕ in this. Conversely, we use Γ ≡ [σ : Σ, ϕ : Σ^{A}, 𝔰(σ, ϕ)] where 𝔰 is one side or the other of the Definition. □

This generalises from an open predicate σ ≡ ⊤ on the right to a general one 𝔮 that may depend on the free variables in the context Γ but not on x : A:

Lemma 7.3 The space N ≡ {A | 𝔭} is overt with possibility operator ♢ iff

for any term Γ ⊢ ϕ : Σ^{X},  Γ, x : A, 𝔭(x), ϕx ⊢ 𝔮 ; = ; Γ, ♢ ϕ ⊢ 𝔮

Proof For definiteness, let Γ ≡ [w : D, 𝔰(w)] and 𝔮(w) ≡ ∀y:B. 𝔯(y) & αyw =▷ βyw, using Notation 3.14 for the normal form of a predicate. Then the following are equivalent,

w : D, 𝔰(w),  x : A, 𝔭(x), ϕx ⊢ ∀y. 𝔯(y) & αyw =▷ βyw
w : D, 𝔰(w), y : B, 𝔯(y), αyw, x : A, 𝔭(x), ϕx ⊢ βyw
w : D, 𝔰(w), y : B, 𝔯(y), αyw, x : A, 𝔭(x)  ⊢ ϕx ⩽ βyw
w : D, 𝔰(w), y : B, 𝔯(y), αyw  ⊢ ♢ ϕ ⩽ βyw
w : D, 𝔰(w), y : B, 𝔯(y),  ♢ ϕ ⊢ αyw ⩽ βyw
w : D, 𝔰(w),  ♢ ϕ ⊢ ∀y. 𝔯(y) & αyw =▷ βyw,

using the previous lemma with Γ ≡ [w : D, 𝔰(w), y : B, 𝔯(y), αyw] and σ ≡ βyw for the middle lines and the ∀ and open Gentzen rules elsewhere. □ Proposition 7.4 If the space N ≡ {A | 𝔭} is overt then its possibility operator ♢ represents �:

ϕ : Σ^{A} ⊢ (�x:A. 𝔭(x) & (ϕx = ⊤)) ◁=▷ (♢ ϕ) = ⊤.

Proof The previous result is more general than the rules for �, in which we must have (w ≡ ϕ and) 𝔰(w) ≡ ⊤. □ Corollary 7.5 The possibility operator ♢ for an overt space is unique. Proof It classifies the open subspace {ϕ : Σ^{A} | �x. 𝔭(x) & ϕx} ↪ Σ^{A}. □ Proposition 7.6 The so-called Frobenius law holds:

ϕ : Σ^{A}, τ : Σ ⊢ ♢(τ ∧ ϕ) = τ ∧ ♢ ϕ.

Proof From ∀x. 𝔭(x) =▷ ϕx ⩽ ♢ ϕ we deduce ∀x. 𝔭(x) =▷ τ ∧ ϕx ⩽ τ ∧ ♢ ϕ and so ♢(τ ∧ ϕ) ⩽ τ ∧ ♢ ϕ. The other inequality follows from

ϕ : Σ^{A}, τ : Σ, τ = ⊤ ⊢ ♢ ϕ ⩽ ♢(τ ∧ ϕ)

and the open Gentzen rule, or from the Euclidean principle (Corollary 3.9). □ Proposition 7.7 Any open subspace of an overt space is overt. Proof Let the space be {A | 𝔭} with possibility operator ♢ and let the subspace be classified by θ. Then by Definition 7.1 for ♢ and the open Gentzen rule,

∀x. 𝔭(x) & θx =▷ ϕx ⩽ σ ⊣⊢ ♢(ϕ ∧ θ) ⩽ σ,

so the possibility operator for the subspace is ♦ ϕ ≡ ♢(ϕ ∧ θ). □ Lemma 7.8 Possibility operators commute:

[𝔭](λx. [𝔮](λy. θxy)) = [𝔮](λy. [𝔭](λx. θxy)).

Proof This follows from Definition 7.1, reversing the order in the proof of Lemma 5.5. □ Corollary 7.9 If N and M are overt then so is N × M.

Proof The doubly quantified formulae in the preceding proof provides the possibility operator for the product because they are ⩽ σ iff ∀xy. 𝔭(x) & 𝔮(y) =▷ (θxy ⩽ σ). □

Lemma 7.10 ♢ ⊥ = ⊥ and ♢(ϕ ∨ ψ) = ♢ ϕ ∨ ♢ ψ. Proof The dual of Lemma 5.7. □

Proposition 7.11 If N ≡ {A | 𝔭} and M ≡ {B | 𝔮} are overt spaces with possibility operators ⟨𝔭⟩ and ⟨𝔮⟩ then K + L is also overt. Its possibility operator is given by

♢ θ ≡ ⟨𝔭⟩(θ · ν_{0}) ∨ ⟨𝔮⟩(θ · ν_{1}).

Proof The dual of Proposition 5.8. □

Example 7.12 The types 0, 1 and 2 are overt, with

⟨0⟩ ≡ ⊥,  ⟨1⟩ϕ ≡ (ϕ⋆) and ⟨2⟩ϕ ≡ (ϕ0 ∨ ϕ1).  □

Lemma 7.13 The term ♢ : Σ^{Σ^{A}} satisfies 𝔭̄(♢), cf. Lemma 5.10. □

Notation 7.14 For any term ⊢ ♢ : Σ^{Σ^{A}}, define

𝔢(x) ≡ ∀ϕ:Σ^{A}. ϕx =▷ ♢ ϕ and N ≡ {x : A | 𝔢(x)}.

Lemma 7.15 If ♢ is the possibility operator for {x : A | 𝔭(x)} then 𝔭 ⊢ 𝔢 and ♢ is also the possibility operator for {x : A | 𝔢(x)}. This is called the weak closure or saturation of {A | 𝔭}. Proof Covariance of the rules. □

Lemma 7.16 A term ⊢ ♢ : Σ^{Σ^{A}} is the possibility operator for some space iff

ϕ : Σ^{A}, ♢ ϕ ⊢ �x. (∀ψ. ψx =▷ ♢ ψ) & ϕx.

In this, ♢ can only have discrete or Hausdorff parameters (Propositions 4.5 and 10.9). Note, however, that ♢ occurs covariantly on the right. This condition is idempotent and is a coclosure condition on ♢.

8 Overt discrete spaces

Lemma 8.1 In any overt discrete space {A | 𝔭},

x : A, 𝔭(x)  ⊢ ⊤ = ϵxx = ♢(λy. ϵxy)
x : A, 𝔭(x), ϕ : Σ^{A} ⊢ ϕx = ♢(λy. ϕy ∧ ϵxy).

Proof Lemmas 4.2 and 7.2 give the first. By these and the Frobenius law (Proposition 7.6,

♢(λy. ϕy ∧ ϵxy) = ♢(λy. ϕx ∧ ϵxy) = ϕx ∧ ♢(λy. ϵxy) = ϕx.  □

Proposition 8.2 Any mono from an overt space to a discrete one is an open inclusion.

Proof Let X ≡ {A | 𝔭} be overt with possibility operator ♢ : Σ^{Σ^{A}} and let Y ≡ {B | 𝔯} be discrete with internal equality δ : B × B → Σ. If the morphism f : X ↣ Y is mono then X is also discrete, by Lemma 4.9, with internal equality

ϵxx′ ≡ δ(fx)(fx′).

Defining F : Σ^{A} → Σ^{B} by F ϕ ≡ λy. ♢ (λx. ϕx ∧ δ(fx)y), if 𝔭(x) then

F ϕ(fx) ≡ ♢ (λx′. ϕx′ ∧ δ(fx′)(fx))
≡ ♢ (λx′. ϕx′ ∧ ϵx′x) = ϕx

by Lemma 8.1. Hence f : X ↣ Y is Σ-split, with nucleus

E ≡ F · Σ^{f} ≡ λψy. F (λx. ψ(fx)) y
≡ λψy. ♢ (λx. ψ(fx) ∧ δ(fx)y)
= λψy. ♢ (λx. ψy ∧ δ(fx)y)
= λψy. ψy ∧ ♢ (λx. δ(fx)y) ≡ λψ. ψ ∧ θ

where θ ≡ λy. ♢ (λx. δ(fx)y), by Lemma 4.2 and the Frobenius law. Since ∀ψ. Eψx ≡ ψx ∧ θx = ψx iff θx, the subspace is open and classified by θ:

X′ ≡ {y : B | 𝔯(y) & θy = ⊤} ↪ {B | 𝔯} ≡ Y.

Then X ≅ X′ by [equdcl]. □

Corollary 8.3 In any overt discrete space, a subspace is open iff it is overt. □

Notice that in equideductive logic there is a general (ā priori) notion of subspace that can be open or overt as a secondary property. In ASD, on the other hand, these two kinds of subspace were defined separately and then had to be shown to be isomorphic [lamcra].

Theorem 8.4 Any overt discrete space N is exponentiable and N is a Σ-split subspace of Σ^{N}. Proof We begin with the second part because it provides the idea for the first. Let

i : N ↣ Σ^{N} by ix ≡ λy. ϵxy and I : Σ^{N} ↣ Σ^{Σ^{N}} by Iϕ ≡ λξ. ♢(λy. ϕy ∧ ξy),

so ix ≡ {x} is the singleton open subspace. Then by Lemma 8.1,

x : N, ϕ : Σ^{N} ⊢ Iϕ(ix) ≡ ♢(λy. ϕy ∧ ϵxy) = ϕx,

so N is a Σ-split subspace of Σ^{N}, which in turn is a retract of Σ^{Σ^{N}}.

If N ≡ {A | 𝔭} then the object {Σ^{Σ^{A}} | 𝔭̄} serves for Σ^{Σ^{N}}, where

𝔭̄(F) ≡ ∀ϕψ. (∀x. 𝔭(x) =▷ ϕx = ψx) =▷ F ϕ = F ψ.

We therefore define

S ≡ {F : Σ^{Σ^{A}} | 𝔭̄(F) & 𝔰(F)} where 𝔰(F) ≡ ∀ξ. F ξ = ♢ (λx. ξx ∧ F (λy. ϵxy))

and claim that there is a natural bijection between morphisms

F : Γ ≡ {w : D | 𝔮(w)} → S and θ : Γ × N ≡ {⟨w, x⟩ : D × A | 𝔮(w) & 𝔭(x)} → Σ.

Given F, which satisfies 𝔮(w) ⊢ 𝔭̄(F w) & 𝔰(F w), define θ_{F} wx ≡ F w(λy. ϵxy). The term F represents the same morphism as G if ∀w. ∀ξ. 𝔮(w) =▷ F wξ = Gwξ, from which we deduce ∀wx. 𝔭(x) & 𝔮(w) =▷ θ_{F} wx = θ_{G}wx, which is the condition for θ_{F} to represent the same morphism as θ_{G}.

Conversely, given θ, define F_{θ}wξ ≡ ♢(λx. ξx ∧ θwx). Then, for σ : Σ and ξ, ξ′ : Σ^{A} with ∀x. 𝔭(x) =▷ ξx = ξ′x,

F_{θ}wξ ⩽ σ ≡ ♢(λx. ξx ∧ θwx) ⩽ σ
⟺ ∀x. 𝔭(x) =▷ ξx ∧ θwx ⩽ σ
⟺ ∀x. 𝔭(x) =▷ ξ′x ∧ θwx ⩽ σ
⟺ F_{θ}wξ′ ⩽ σ,

whence 𝔭̄(F_{θ}w). Also, by Lemma 8.1,

∀x. 𝔭(x) =▷ θwx = ♢(λy. ϵxy ∧ θwy),

so by Lemma 7.13,

F_{θ}wξ ≡ ♢(λx. ξx ∧ θwx)
= ♢ (λx. ξx ∧ ♢(λy. ϵxy ∧ θwy))
≡ ♢ (λx. ξx ∧ F_{θ}w(λy. ϵxy))

so 𝔰(F_{θ}w). If θ and θ′ agree as above then for σ : Σ and w : D with 𝔮(w),

F_{θ}wξ ⩽ σ ≡ ♢(λx. ξx ∧ θwx) ⩽ σ
⟺ ∀x. 𝔭(x) =▷ ξx ∧ θwx ⩽ σ
⟺ ∀x. 𝔭(x) =▷ ξx ∧ θ′wx ⩽ σ
⟺ F_{θ′}wξ ⩽ σ,

so F_{θ} and F_{θ′} represent the same morphism.

Passing from θ to F and back recovers θ because, by Lemma 8.1, if 𝔭(x) then

θ_{F_{θ}}wx ≡ ♢(λy. ϵxy ∧ θwy) = θwx.

Passing from F to θ and back recovers F because, since 𝔰(F w),

F_{θ_{F}} wξ ≡ ♢ (λx. ξx ∧ F w(λy. ϵxy)) = F wξ.

The transformations θ ↦ F_{θ} and F ↦ θ_{F} are natural because they admit substitution for the variable w. Hence S has the universal property of the exponential Σ^{N}.

The singleton map ix ≡ λy. ϵxy is an example of this transformation with Γ ≡ N and θ ≡ ϵ. It gives

F wξ ≡ ♢(λx. ξx ∧ ϵwx) = ξw,

so i ≡ F ≡ η_{A} : A → Σ^{Σ^{A}}. □

9 When do we have a topos?

The characterisation of a topos appears to be a tautology in this setting because many of the ideas that lie behind the constructions of elementary topos theory have been incorporated into the more general calculus of equideductive topology. The fundamental results ar those of Section 3.

Definition 9.1 A topos is an equideductive category in which every object is exponentiable and Σ ≡ Ω is a dominance, classifying arbitrary subobjects.

Proposition 9.2 Every object of a topos is overt.

Proof Since any object X of a topos is exponentiable we may form the subobject

{ϕ : Σ^{X} | �x. ϕx} ↪ Σ^{X},

where � is the equideductive existential quantifier. Since Ω classifies all monos, there is a term ♢ : Σ^{Σ^{X}} that satisfies Proposition 7.4. □

Proposition 9.3 Every object of a topos is discrete. Proof The diagonal subobject X ↪ X × X is classified by ϵ. □

Theorem 9.4 If the fundamental object Σ of an equideductive category is a dominance and every object is both overt and discrete then the category is a topos. Proof An equideductive category has all finite limits by definition. Every object is exponentiable by Theorem 8.4 and every mono is open by Proposition 8.2.

We can adapt this result to the situation where the overt discrete objects do not exhaust the category but form a coreflective subcategory. This is the situation for sets considered as objects with the discrete order or topology as a subcategory of Pos or Sob, where the right adjoint to the inclusion is known as the underlying set functor.

Theorem 9.5 If the full subcategory of overt discrete objects is coreflective then it forms a topos. Proof Any mono U ↪ X between overt discrete objects is open and so classified by a map X → Σ. However, Σ is not overt discrete, but UΣ is and any map X → Σ factors through it. Hence Ω ≡ UΣ is the subobject classifier. □

There is another characterisation of the topos situation using compactness (the universal quantifier) instead of overtness.

Proposition 9.6 Every object of a topos is compact. Proof As in the case of overtness, we may form the subobject

{ϕ : Σ^{X} | ∀x. ϕx} ↪ Σ^{X},

where ∀ is the equideductive quantifier. Since Ω classifies all monos, there is a term □ : Σ^{Σ^{X}} that satisfies Definition 5.1. □

It is tempting to think that compactness is enough on its own since Definition 5.1 apparently says that any equideductive predicate in normal form (Notation 3.14) is represented by a term □. However, this is not so:

Example 9.7 The category Pos is equideductive, Σ ≡ Ω is a dominance classifying upper subobjects and every object is both overt and compact, but not discrete. □

The problem with the definition of compactness is that it only allows the operator □ to have discrete parameters (Lemma 5.13). We therefore need to consider discreteness too.

Proposition 9.8 The object Σ of an equideductive category is discrete iff its external Heyting implication (Notation 3.14(d)) is represented by a term, which we call (→):

σ =▷ τ ≡ (σ = ⊤) =▷ (τ = ⊤) ⊣⊢ (σ → τ) = ⊤.

for σ, τ : Σ.

Proof We use Lemma 3.1 and Example 3.13. If Σ is discrete then by Definition 4.1 there is a term ϵ : Σ × Σ → Σ such that

x = y ⊣⊢ ϵxy = ⊤.

Then (x → y) ≡ ϵx(x ∧ y) represents implication because

x =▷ y ≡ x ⩽ y ≡ x = x ∧ y ⊣⊢ ϵx(x ∧ y) = ⊤.

Conversely, ϵxy ≡ (x → y) ∧ (y → x) satisfies

x = y ⊣⊢ x ⩽ y & y ⩽ x ⊣⊢ (x =▷ y) & (y =▷ x)
⊣⊢ (x → y) = ⊤ & (y → x) = ⊤ ⊣⊢ ϵxy = ⊤.  □

Although it follows that all powers of Σ are Heyting algebras, (ϵ^{X}) : Σ^{X} × Σ^{X} → Σ^{X} has the wrong type to be the equality predicate.

Lemma 9.9 If Σ is discrete and Σ^{X} is compact then Σ^{Σ^{X}} is also discrete. Proof F =Σ^{Σ^{X}} G iff ∀ϕ:Σ^{X} . F ϕ =_{Σ} Gϕ. □

Lemma 9.10 If Σ^{Σ^{X}} is discrete then so is X. Proof By Lemma 4.9, since η_{X} : X → Σ^{Σ^{X}} is mono because all exponentiable objects of an equideductive category are sober. □

Lemma 9.11 If Σ is discrete and both Σ and X are compact then X is overt. Proof Proposition 7.4. □

Theorem 9.12 An equideductive category is a topos iff Σ is a dominance and every object is both compact and discrete. □

10 Classifying closed subspaces

In Section 3 we investigated the situation where the top element of Σ classifies some class of monos. The four examples of this are: all subobjects in a topos, open subspaces in general topology, upper subsets in order theory and recursively enumerable ones in computability. However, it is also the case the bottom element classifies closed subspaces in intuitionistic topology and co-RE subsets in computability. Assuming excluded middle, ⊥ ∈ 2 also classifies arbitrary subsets of sets and lower subsets of posets.

In this section, therefore, we repeat the results that we have already proved, but in the lattice dual notation, starting with those in Section 3.

Axiom 10.1 The closed Gentzen rule is

Γ, α = ⊥ ⊢ β ⩽ γ = Γ ⊢ β ⩽ α ∨ γ

for any terms Γ ⊢ α, β, γ : Σ that may contain parameters and depend on predicates.

Proposition 10.2 The fundamental object Σ is a dominance iff it carries a semilattice structure (Σ, ⊥, ∨) that satisfies the closed Gentzen rule, cf. Theorem 3.8. □

Definition 10.3 The inverse image of ⊥ along ϕ : X → Σ, which is {x : A | ϕx = ⊥}, is called a closed subspace. We also call ϕx = ⊥ a closed predicate and write ¬ϕx for it, but beware that we mean “closed” in the topological sense, not the syntactic one that there are no free variables. Another way of writing the closed Gentzen rule is therefore

¬α & β =▷ γ ⊣⊢ β =▷ α ∨ γ.

Proposition 10.4 Closed antecedents are exempt from the variable-binding rule, to one level, cf. Proposition 3.11. □

Proposition 10.5 The closed Gentzen rule entails the dual Euclidean principle, cf. Corollary 3.9:

σ : Σ, F : Σ^{Σ} ⊢ σ ∨ F σ = σ ∨ F ⊥.  □

Lemma 10.6 The closed subspace co-classified by ϕ is Σ-split by (−) ∨ ϕ, cf. Lemma 3.10. □

Next we consider the dual of discreteness from Section 4.

Definition 10.7 Dually to Definition 4.1, a space H ≡ {x : A | 𝔭(x)} is Hausdorff if equality is represented negatively by an term (≠) : Σ^{A×A},

x, y : A, 𝔭(x), 𝔭(y) ⊢ (x ≠ y) = ⊥ ◁=▷ ∀ϕ. (ϕx = ϕy),

which we call internal inequality. This is equivalent to saying that the diagonal H ↣ H × H is a closed subspace coclassified by ≠, cf. Proposition 4.7, so ≠ is unique in the sense of Remark 3.5. Hausdorffness may also be characterised in a dual way to Lemma 4.2:

Lemma 10.8 The term (≠) is the internal inequality for the Hausdorff object H ≡ {x : A | 𝔭(x)} iff it is irreflexive and cosubstitutive:

x : A, 𝔭(x)  ⊢ (x ≠ x) = ⊥
x, y : A, ϕ : Σ^{A}, 𝔭(x), 𝔭(y) ⊢ ϕx =▷ (x ≠ y) ∨ ϕy.

In this case, ≠ is also symmetric and cotransitive:

x, y : A, 𝔭(x), 𝔭(y)  ⊢ (x ≠ y) =▷ (y ≠ x)
x, y, z : A, 𝔭(x), 𝔭(y), 𝔭(z) ⊢ (x ≠ z) =▷ (x ≠ y) ∨ (y ≠ z).  □

Proposition 10.9 Variables of Hausdorff type are exempt from the variable-binding rule, cf. Proposition 4.5. □

Lemma 10.10 Any predicate respects internal inequality, cf. Proposition 4.4:

x, y : A, 𝔭(x), 𝔭(y), 𝔯(x), (x ≠ y) = ⊥ ⊢ 𝔯(y).

Lemma 10.11 Let K be a Hausdorff space and f : H → K a morphism. If H is also Hausdorff then f reflects inequality:

x, y : A, 𝔭(x), 𝔭(y) ⊢ (fx) ≠_{K} (fy) =▷ x ≠_{H} y.

If f is mono then H is Hausdorff, with (x ≠_{H} y) ≡ (fx) ≠_{K} (fy), cf. Lemma 4.9. □

Examples 10.12

(a) 0 is Hausdorff, with x ≠_{1} y ≡ ⊥;

(b) 1 is Hausdorff, with x ≠_{1} y ≡ ⊥;

(c) 2 is Hausdorff, with (0 ≠ 1) = (1 ≠ 0) = ⊤ and (0 ≠ 0) = (1 ≠ 1) = ⊥;

(d) if H and K are Hausdorff then so is H ×K, with ⟨x, y⟩ ≠_{N×M} ⟨x′, y′⟩ ≡ (x ≠_{N} x′)∨(y ≠_{M} y′);

(e) if H and K are Hausdorff then so is H + K. □

Remark 10.13 Discrete spaces need not be Hausdorff. Discuss decidable equality.

The duals of the results in Sections 7 and 8 about overt spaces tell us more about compact ones. Beware that, whilst this interchanges the internal quantifiers U and ∃, the external ones ∀ and � stay the same.

Lemma 10.14 The space K ≡ {A | 𝔭} is compact iff there is an term ⊢ □ : Σ^{Σ^{A}} such that such that

ϕ : Σ^{A} ⊢ (�x:A. 𝔭(x) & (ϕx = ⊥)) ◁=▷ (□ ϕ) = ⊥.  □

Lemma 10.15 The (dual) Frobenius law: □(λx. σ ∨ ϕx) ⟺ σ ∨ □ ϕ.

Lemma 10.16 Any closed subspace of a compact space is compact. □

Lemma 10.17 In any compact Hausdorff space,

x : A, 𝔭(x)  ⊢ ⊥ = x ≠ x = □(λy. x ≠ y)
x : A, 𝔭(x), ϕ : Σ^{A} ⊢ ϕx = □(λy. ϕy ∨ x ≠ y).  □

Proposition 10.18 Any mono from a compact space to a Hausdorff one is a closed inclusion. □

Corollary 10.19 In a compact Hausdorff space, a subspace is closed iff it is compact. □

Theorem 10.20 Any compact Hausdorff space K is exponentiable and K is a Σ-split subspace of Σ^{K}. □

Conversely, the results in Section 5 about compact spaces are also applicable to overt ones. The notable point is that these negative statements are sufficient.

Proposition 10.21 If a space N ≡ {A | 𝔭} has an term ⊢ ♢ : Σ^{Σ^{A}} such that either

ϕ : Σ^{A} ⊢ (∀x. 𝔭(x) =▷ (ϕx = ⊥)) ◁=▷ (♢ ϕ) = ⊥

or ϕ : Σ^{A} ⊢ ((�x. 𝔭(x) & ϕx)) =▷ ⊥) ◁=▷ (♢ ϕ) = ⊥

then N is overt, with possibility operator ♢. Proof The first is the special case σ ≡ ⊥ of Definition 7.1, but it is equivalent to the general one by the dual of Lemma 5.3. We deduce the second using the de Morgan law. □

11 The Phoa principle

Add monotonicity to the open and closed Gentzen rules.

My plan with this paper is to add things to it and develop it in parallel with editing the original ASD papers.

The middle level of ASD, i.e. the development of topology using the (finitary) Phoa principle but not the (infinitary) Scott principle, was rather badly written up. This was because [geohol] was published long before I had the whole picture of the re-axiomatisation of topology and [nonagr] was premature. On the other hand, when I obtained the characterisation of computably based locally compact spaces I then moved straight on to real analysis without filling in the earlier parts. Besides this, numerous lemmas and idioms have arisen that ought to be collected into a single development.

Therefore, besides introducing a new foundation to replace that of ASD, this paper is intended to provide better documentation of topology with the Phoa principle. This means that the text is likely to undergo repeated structural changes before it is completed.