Exercise 1.18 (Scott 1981, PRG-19, §1) — consistent subsets and filter

intersections

Scott calls a subset C ⊆ 𝒟 consistent iff every finite subset of C is consistent in 𝒟. This file formalizes (representing finite subsets as finite sequences drawn from C):

• FinitelyConsistent C — every finite sequence from C is Consistent;
• a concrete C = {A, B, Cc} (over Δ = {0,1,2}, all-non-empty-subsets system) with three members, pairwise consistent (family_pairwise_nonempty) but not consistent (not_finitelyConsistent) — A ∩ B ∩ Cc = ∅;
• sInf F hF — the intersection of a non-empty family F of filters is a filter, the greatest lower bound (sInf_le, le_sInf);
• leastFilter C hCsub hC — the least filter containing a consistent C, with subset_leastFilter (C ⊆ it) and leastFilter_le (it is least). The intersection law uses the append of two finite sequences (interUpTo_appendSeq).

Constructive ([propext, Quot.sound]) except the counterexample's finite case-analysis.

def Domain.Neighborhood.appendSeq {α : Type u_1} (X1 : ℕ → Set α) (n1 : ℕ) (X2 : ℕ → Set α) : ℕ → Set α

Concatenation of two finite sequences: the first n1 entries are X1 0, …, X1 (n1-1), then X2 0, X2 1, ….

Equations

• Domain.Neighborhood.appendSeq X1 n1 X2 i = if i < n1 then X1 i else X2 (i - n1)

theorem Domain.Neighborhood.appendSeq_mem {α : Type u_1} {C : Set (Set α)} {X1 : ℕ → Set α} {n1 : ℕ} {X2 : ℕ → Set α} {n2 : ℕ} (h1 : ∀ i < n1, X1 i ∈ C) (h2 : ∀ i < n2, X2 i ∈ C) (i : ℕ) : i < n1 + n2 → appendSeq X1 n1 X2 i ∈ C

Each entry of appendSeq X1 n1 X2 below n1 + n2 is drawn from C.

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_subset_master {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) (n : ℕ) : V.interUpTo X n ⊆ V.master

The finite intersection is contained in the master neighbourhood (its first factor).

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_appendSeq_left {α : Type u_1} (V : NeighborhoodSystem α) (X1 : ℕ → Set α) (n1 : ℕ) (X2 : ℕ → Set α) {k : ℕ} : k ≤ n1 → V.interUpTo (appendSeq X1 n1 X2) k = V.interUpTo X1 k

For a prefix length k ≤ n1, interUpTo of the appended sequence agrees with interUpTo of the first sequence.

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_appendSeq {α : Type u_1} (V : NeighborhoodSystem α) (X1 : ℕ → Set α) (n1 : ℕ) (X2 : ℕ → Set α) {j : ℕ} : V.interUpTo (appendSeq X1 n1 X2) (n1 + j) = V.interUpTo X1 n1 ∩ V.interUpTo X2 j

The key identity: ⋂_{i<n1+n2} (X1 ++ X2)ᵢ = (⋂_{i<n1} X1ᵢ) ∩ (⋂_{i<n2} X2ᵢ).

Finite consistency.

def Domain.Neighborhood.NeighborhoodSystem.FinitelyConsistent {α : Type u_1} (V : NeighborhoodSystem α) (C : Set (Set α)) : Prop

Exercise 1.18 — consistent subset. C ⊆ 𝒟 is finitely consistent iff every finite sequence drawn from C is Consistent in 𝒟.

Equations

• V.FinitelyConsistent C = ∀ (n : ℕ) (X : ℕ → Set α), (∀ i < n, X i ∈ C) → V.Consistent X n

Intersection of a non-empty family of filters (Scott's last claim).

def Domain.Neighborhood.NeighborhoodSystem.sInf {α : Type u_1} (V : NeighborhoodSystem α) (F : Set V.Element) (hF : F.Nonempty) : V.Element

Exercise 1.18 — the intersection of a non-empty family of filters is a filter. sInf F = {X ∣ ∀ x ∈ F, X ∈ x}.

Equations

• V.sInf F hF = { mem := fun (X : Set α) => ∀ x ∈ F, x.mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.sInf_le {α : Type u_1} (V : NeighborhoodSystem α) (F : Set V.Element) (hF : F.Nonempty) {x : V.Element} (hx : x ∈ F) : V.sInf F hF ≤ x

sInf F ⊑ x for every x ∈ F.

theorem Domain.Neighborhood.NeighborhoodSystem.le_sInf {α : Type u_1} (V : NeighborhoodSystem α) (F : Set V.Element) (hF : F.Nonempty) (y : V.Element) (h : ∀ x ∈ F, y ≤ x) : y ≤ V.sInf F hF

sInf F is the greatest lower bound of F.

The least filter containing a consistent C.

def Domain.Neighborhood.NeighborhoodSystem.leastFilter {α : Type u_1} (V : NeighborhoodSystem α) (C : Set (Set α)) (hCsub : ∀ X ∈ C, V.mem X) (hC : V.FinitelyConsistent C) : V.Element

Exercise 1.18 — the least filter containing a consistent C. leastFilter C = {Y ∈ 𝒟 ∣ ⋂_{i<n} Xᵢ ⊆ Y for some finite sequence ⟨Xᵢ⟩ from C}. The intersection law concatenates two finite sequences (interUpTo_appendSeq) and uses finite consistency to keep their combined intersection in 𝒟.

Equations

• V.leastFilter C hCsub hC = { mem := fun (Y : Set α) => V.mem Y ∧ ∃ (n : ℕ) (X : ℕ → Set α), (∀ i < n, X i ∈ C) ∧ V.interUpTo X n ⊆ Y, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.subset_leastFilter {α : Type u_1} (V : NeighborhoodSystem α) (C : Set (Set α)) (hCsub : ∀ X ∈ C, V.mem X) (hC : V.FinitelyConsistent C) {W : Set α} (hW : W ∈ C) : (V.leastFilter C hCsub hC).mem W

C ⊆ leastFilter C: every member of C is in the least filter.

theorem Domain.Neighborhood.NeighborhoodSystem.leastFilter_le {α : Type u_1} (V : NeighborhoodSystem α) (C : Set (Set α)) (hCsub : ∀ X ∈ C, V.mem X) (hC : V.FinitelyConsistent C) (z : V.Element) (hz : ∀ W ∈ C, z.mem W) : V.leastFilter C hCsub hC ≤ z

Exercise 1.18 — leastFilter is least. Any filter z with C ⊆ z contains leastFilter C.

A 3-element pairwise-consistent but not consistent set.

def Domain.Neighborhood.triSys : NeighborhoodSystem (Fin 3)

All non-empty subsets of Δ = {0,1,2} (a positive neighbourhood system).

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.triSys_master : triSys.master = Set.univ

def Domain.Neighborhood.triSys.A : Set (Fin 3)

A = {0,1}.

Equations

• Domain.Neighborhood.triSys.A = {0, 1}

def Domain.Neighborhood.triSys.B : Set (Fin 3)

B = {1,2}.

Equations

• Domain.Neighborhood.triSys.B = {1, 2}

def Domain.Neighborhood.triSys.Cc : Set (Fin 3)

Cc = {0,2}.

Equations

• Domain.Neighborhood.triSys.Cc = {0, 2}

def Domain.Neighborhood.triSys.family : Set (Set (Fin 3))

The three-member family C = {A, B, Cc}.

Equations

• Domain.Neighborhood.triSys.family = {Domain.Neighborhood.triSys.A, Domain.Neighborhood.triSys.B, Domain.Neighborhood.triSys.Cc}

theorem Domain.Neighborhood.triSys.family_pairwise_nonempty (X : Set (Fin 3)) : X ∈ family → ∀ Y ∈ family, (X ∩ Y).Nonempty

Every pair of members of family has non-empty intersection, hence (in the all-non-empty system triSys) every pair is consistent.

def Domain.Neighborhood.triSys.triple : ℕ → Set (Fin 3)

The triple A, B, Cc as a finite sequence.

Equations

• Domain.Neighborhood.triSys.triple i = if i = 0 then Domain.Neighborhood.triSys.A else if i = 1 then Domain.Neighborhood.triSys.B else Domain.Neighborhood.triSys.Cc

theorem Domain.Neighborhood.triSys.triple_mem (i : ℕ) : i < 3 → triple i ∈ family

theorem Domain.Neighborhood.triSys.triple_interUpTo_empty : triSys.interUpTo triple 3 = ∅

theorem Domain.Neighborhood.triSys.not_finitelyConsistent : ¬triSys.FinitelyConsistent family

Exercise 1.18 — family is pairwise consistent but not consistent. Its full triple has empty intersection, so no Z ∈ 𝒟 (i.e. no non-empty Z) lies below it.