Index of the slides:

Motivation for Logicians . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Topologies on (directed) graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 An archetypical example of a sheaf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Saturated coherent families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Logic on topological spaces: sequent calculus (1) . . . . . . . . . . . . . . . . . . . . . . . . 6 Logic on topological spaces: sequent calculus (2) . . . . . . . . . . . . . . . . . . . . . . . . 7 Logic on topological spaces: soundness and completeness . . . . . . . . . . . . . . . . 8 Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Modalities: more theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Modalities: alternative axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Double negation is a modality, by hand (1) . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Double negation is a modality, by hand (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 Downcasing the closure operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Saturated covers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Saturation in prestacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 The algebra of covers: a lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 The algebra of covers: an (imaginary) finest cover . . . . . . . . . . . . . . . . . . . . . . 18 Geometric Morphisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 Geometric morphisms (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Johnstone: filter-powers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .21 A note on filter-powers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .22 Motivation for Logicians We can interpret intuitionistic propositional calculus on topological spaces. Fix a topological space (X, O(X)) – its open sets will play the role of truth values. For P, Q ∈ O(X), define:

⊤ := X
P ∨ Q := P ∪ Q
P ∧ Q := P ∩ Q
P [figure]Q := (P ^{compl} ∪ Q)^{int}
⊥ := ∅

We will regard X as a set of “worlds”, and each open set P ∈ O(X) as a proposition that is true at the worlds for which x ∈ P, false at the others. If the topology is discrete then P(X) = O(X): all subsets of X are truth values, and all the worlds are independent. For some non-discrete topological spaces we may have ¬¬P ≠ P, ¬(P ∧ Q) ≠ ¬P ∨ ¬Q, etc. For example: take X := ℝ, with the usual topology, and take P := (0, 1) ∪ (1, 2). Then:

¬P = P [figure]⊥ = (P ^{compl})^{int} = (−∞, 0) ∪ (2, ∞),
¬¬P = ¬P [figure]⊥ = (¬P ^{compl})^{int} = (0, 2)
⊋ P.

Some operations on sheaves will be related to forcing the logic to become boolean.

Topologies on (directed) graphs For some examples it will be convenient to use very small (i.e., finite) topological spaces. We will never need non-directed graphs here... so let’s say just “graph” to mean “directed graph”. Actually we are interested in the category generated by a graph: the transitive closure of the graph, plus the identity arrows.

This will be one of our favourite graphs:

𝟛 := [figure: α; γ; β; γ]

We can use ‘0’s and ‘1’s at the right places to denote subsets of the set of “worlds” (points) of a graph. In the “natural topology” of a graph the open sets are be the subsets associated to non-decreasing functions from the set of worlds to {0, 1}. The “natural” topology on 𝟛, O(𝟛), has five open sets:

[figure: 1 1 1; _{1 0 1}; 1 1 1; _{0 1 1}; _{1 0 1}; _{0 0 1}; _{0 1 1}; _{0 0 1}; _{0 0 1}; _{0 0 0}; {α, β, γ}; {α, γ}; {α, β, γ}; {β, γ}; {α, γ}; {γ}; {β, γ}; {γ}; {γ}; { }]

They are naturally ordered by inclusion, so O(𝟛) is another graph, with five points... The cover of 𝟛

\begin{matrix}by: & ^{1}^{0} 1 ≡ \{α, γ\} \\ and: & ^{0}^{1} 1 ≡ \{β, γ\} \end{matrix}

can be denoted by:

0^{1}^{1}^{0} 0 ≡ {{α, γ}, {β, γ}}.

An archetypical example of a sheaf Take X := ℝ, and:

C : O(ℝ) → Sets
U ↦ C(U) := { f : U → ℝ | f is continuous }

Now take a cover for X = ℝ:

\begin{aligned}W & := & (∞, 1) \\ V & := & (0, ∞) \\ U & := & \{W, V \} \end{aligned}

and look at a “coherent family of functions”, a_{U}, defined on U:

\begin{aligned}a_{U} & := & \{(W, a_{W}), \\ & & (V, a_{V})\} \end{aligned}

where:

a_{W} : W → ℝ
x ↦ 2x
a_{V} : V → ℝ
x ↦ 2x

Being “coherent” means that ∀V, W ∈ U.(a_{V} |_{V ∩W} = a_{W} |_{V ∩W}). It is only for coherent families that we can have hope of being able to “glue” all the “locally defined functions” of the family into a sigle “global function”,

\begin{aligned}a : & X & → & ℝ \\ & x & ↦ & 2x \end{aligned}

that generates them all, by restriction.

A presheaf on a topological space O(X) is a contravariant functor O(X)^{op} → Set:

[figure: C(V); C(U); C(V →U); C(V); V; C(U); U; V; U]

that is, for any U ∈ O(X) a set of “locally defined functions” (with support U), plus “restriction functions” between these sets.

A sheaf is a presheaf in which all coherent families defined on covers can be glued well.

Saturated coherent families A “continuous function” defined on an open set U induces a coherent family defined on all open sets contained in U... Look at the graph O(𝟛)^{op}:

[figure: 1 1 1; _{1 0 1}; 1 1 1; _{0 1 1}; _{1 0 1}; _{0 0 1}; _{0 1 1}; _{0 0 1}; _{0 0 1}; _{0 0 0}; {α, β, γ}; {α, γ}; {α, β, γ}; {β, γ}; {α, γ}; {γ}; {β, γ}; {γ}; {γ}; { }]

A “continuous function” defined on {α, γ} induces a coherent family

with support ^{0}^{1}^{0}^{1} 1.

Logic on topological spaces: sequent calculus (1) Topological spaces are a very good setting for understanding intuitionistic propositional calculus - especially because they let us show that some sentences can not be proved.

A topology O(X) will be seen as a category; a morphism P → R exists iff, as open sets, P ⊆ Q – that is, if P implies Q “in each world” (i.e., ∀x ∈ X.(x ∈ P) [figure](x ∈ Q)); this will also be our notion of P implying Q “globally”.

The sequent (with one hypothesis) P ⊢ Q will mean “the morphism P → Q exists”.

Fact: look at O(X) as a category; it is a cartesian closed category, and the topological definitions of ⊤, ∧, [figure], ∨, ⊥ coincide with the obvious corresponding categorical operations on objects –

⊤ terminal object ∧ binary product

[figure: exponential]

∨ binary coproduct ⊥ initial object

The categorical definitions of ⊤, ∧, [figure], ∨, ⊥ suggest some rules for building some sequents from others (or from nothing):

P Q [figure] [figure]P Q ∧ R [figure] P  R [figure] [figure] Q  Q ∧ R [figure] Q ∧ R  R [figure] P  P ∨ Q [figure] P ∨ Q  Q [figure] P  R [figure] [figure] P ∨ Q R[figure]  Q R [figure] [figure]  P ⊤[figure] ⊥ P[figure] P ∧ Q  P [figure] P ∧ Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure] [figure]

\begin{matrix}\begin{matrix}P ⊢ Q & P ⊢ R \\ P ⊢ Q ∧ R \end{matrix} & Q ∧ R ⊢ Q & Q ∧ R ⊢ R & P ⊢ ⊤ & {P ∧ Q ⊢ R \atop P ⊢ Q [figure]R} (↕) \\ \begin{matrix}P ⊢ R & Q ⊢ R \\ P ∨ Q ⊢ R \end{matrix} & P ⊢ P ∨ Q & Q ⊢ P ∨ Q & ⊥ ⊢ P \end{matrix}

Logic on topological spaces: sequent calculus (2) We will work with four different “languages”:

• categories,

• sequents with one hypothesis,

• sequents with a finite number of hypotheses,

• Natural Deduction.

An example of translation (between sequents with one hypothesis and categories):

\begin{matrix}{P ⊢ Q \atop ⊤ ∧ P ⊢ Q} & (↕) \\ ⊤ ⊢ P [figure]Q \end{matrix} ; (↕)  \begin{matrix}\begin{matrix}P ⊢ ⊤ & P ⊢ P \\ P ⊢ ⊤ ∧ P \end{matrix} & {⊤ ⊢ P [figure]Q \atop ⊤ ∧ P ⊢ Q} \\ P ⊢ Q \end{matrix}  \begin{matrix}⊤ ∧ P ⊢ P & P ⊢ Q \\ ⊤ ∧ P ⊢ Q \end{matrix} ; ⊤ ⊢ P [figure]Q

P  ⊤ ∧ P [figure] [figure] ⊤ ∧ P  ⊤ [figure] P  Q [figure] [figure] ⊤ ∧ P Q[figure]  ⊤ P [figure]Q [figure] Q  P [figure]Q [figure] [figure] [figure] [figure] [figure]

A technicality:

⊤ ⊢ (P [figure]Q) [figure](R [figure]S) ⇔ P [figure]Q ⊢ R [figure]S ⇒ {P ⊢ Q \atop R ⊢ S}

Proof of the implication at the right:

\begin{matrix}{P ⊢ Q \atop ⊤ ⊢ P [figure]Q} & P [figure]Q ⊢ R [figure]S \\ ⊤ ⊢ R [figure]S \end{matrix} ; R ⊢ S

But the converse does not hold. The case where it fails is when we have neither P ⊢ Q nor R ⊢ S. Then, “semantically”,

{P ⊢ Q \atop R ⊢ S} holds, in a sense,

and we could expect this to be reflected in the existence of a morphism P [figure]Q ⊢ R [figure]S... But try P := 1 1 1 , Q := 0 1 1 , R := 0 1 1 , S := 0 0 1 —

then (P [figure]Q) [figure](R [figure]S) = 0 0 1 , which is weaker than ⊤.

Logic on topological spaces: soundness and completeness Fact (for logicians; “soundness”): If

\begin{aligned}α_{1} ⊢ β_{1} & … & α_{n} ⊢ β_{n} \\ & γ ⊢ δ \end{aligned}

is provable intuitionistically (i.e., in the system above), then in any HA where α_{1} ⊢ β_{1}, …, α_{n} ⊢ β_{n} hold, the conclusion γ ⊢ δ also holds. Proof: induction, trivial. Look at the full derivation, starting from the top, and check that each bar constructs a new sequent that holds.

Fact (for logicians; “completeness”): If

\begin{aligned}α_{1} ⊢ β_{1} & … & α_{n} ⊢ β_{n} \\ & γ ⊢ δ \end{aligned}

is not provable intuitionistically, then there is a directed graph D, and choices of truth values in O(D) for the atomic propositions in α_{i}, β_{i}, γ, δ, such that the hypotheses α_{1} ⊢ β_{1}, …, α_{n} ⊢ β_{n} hold, but the conclusion γ ⊢ δ does not hold. Proof: hard, and non-categorical... uses tableau methods.

Modalities Examples of modalities: P^{∗} := ¬¬P P^{∗} := α ∨ P P^{∗} := α [figure]P

Axioms:

⊢ ⊤^{∗}  {P ⊢ Q \atop P^{∗} ⊢ Q^{∗}}  P^{∗∗} ⊢ P^{∗}

First theorems: P ⊢ P^{∗} (P ∧ Q)^{∗} ⊢ P^{∗} ∧ Q^{∗} P ∧ Q^{∗} ⊢ (P ∧ Q)^{∗} P^{∗} ∧ Q^{∗} ⊢ (P ∧ Q)^{∗}

Proofs:

\begin{matrix}⊢ ⊤ ⇔ ⊤^{∗} & {P ⊢ ⊤ ⇔ P \atop P ⊢ ⊤^{∗} ⇔ P^{∗}} \\ P ⊢ ⊤ ⇔ P^{∗} \end{matrix} ; P ⊢ P^{∗}

\begin{matrix}{P ∧ Q ⊢ P \atop (P ∧ Q)^{∗} ⊢ P^{∗}} & {P ∧ Q ⊢ Q \atop (P ∧ Q)^{∗} ⊢ Q^{∗}} \\ (P ∧ Q)^{∗} ⊢ P^{∗} ∧ Q^{∗} \end{matrix}  {P ⊢ Q ⇔ (P ∧ Q) \atop P ⊢ Q^{∗} ⇔ (P ∧ Q)^{∗}} ; P ⊢ Q^{∗} [figure](P ∧ Q)^{∗} ; P ∧ Q^{∗} ⊢ (P ∧ Q)^{∗}

\begin{aligned}P^{∗} ∧ Q^{∗} ⊢ (P^{∗} ∧ Q)^{∗} & {P^{∗} ∧ Q ⊢ (P ∧ Q)^{∗} \atop (P^{∗} ∧ Q)^{∗} ⊢ (P ∧ Q)^{∗∗}} & (P ∧ Q)^{∗∗} ⊢ (P ∧ Q)^{∗} \\ & P^{∗} ∧ Q^{∗} ⊢ (P ∧ Q)^{∗} \end{aligned}

Consequence:

[figure: P ∧ Q; P^{∗} ∧ Q; P ∧ Q^{∗}; P^{∗} ∧ Q^{∗}; P ∧ Q; P ∧ Q^{∗}; P^{∗} ∧ Q; P^{∗} ∧ Q^{∗}; (P ∧ Q)^{∗}; (P^{∗} ∧ Q)^{∗}; (P ∧ Q^{∗})^{∗}; (P^{∗} ∧ Q^{∗})^{∗}; (P ∧ Q)^{∗}; (P ∧ Q^{∗})^{∗}; (P^{∗} ∧ Q)^{∗}; (P^{∗} ∧ Q^{∗})^{∗}; P ∧ Q; (P ∧ Q)^{∗}; P^{∗} ∧ Q; (P^{∗} ∧ Q)^{∗}; P ∧ Q^{∗}; (P ∧ Q^{∗})^{∗}; P^{∗} ∧ Q^{∗}; (P^{∗} ∧ Q^{∗})^{∗}]

Modalities: more theorems Implication:

{(P [figure]Q) ∧ P ⊢ Q \atop ((P [figure]Q) ∧ P)^{∗} ⊢ Q^{∗}} ; (P [figure]Q)^{∗} ∧ P^{∗} ⊢ Q^{∗} ; (P [figure]Q)^{∗} ⊢ P^{∗} [figure]Q^{∗}  \begin{matrix}P [figure]Q ⊢ (P [figure]Q)^{∗} & (P [figure]Q)^{∗} ⊢ P^{∗} [figure]Q^{∗} \\ P [figure]Q ⊢ P^{∗} [figure]Q^{∗} \end{matrix}
{(P [figure]Q)^{∗} ⊢ P^{∗} [figure]Q^{∗} \atop P^{∗} ∧ (P [figure]Q)^{∗} ⊢ Q^{∗}}  \begin{matrix}P^{∗} ∧ (P [figure]Q^{∗})^{∗} ⊢ Q^{∗∗} & Q^{∗∗} ⊢ Q^{∗} \\ P^{∗} ∧ (P [figure]Q^{∗})^{∗} ⊢ Q^{∗} \end{matrix} ; (P [figure]Q^{∗})^{∗} ⊢ P^{∗} [figure]Q^{∗}

Disjunction:

\begin{matrix}{P ⊢ P ∨ Q \atop P^{∗} ⊢ (P ∨ Q)^{∗}} & {Q ⊢ P ∨ Q \atop Q^{∗} ⊢ (P ∨ Q)^{∗}} \\ P^{∗} ∨ Q^{∗} ⊢ (P ∨ Q)^{∗} \end{matrix}  {P^{∗} ∨ Q^{∗} ⊢ (P ∨ Q)^{∗} \atop (P^{∗} ∨ Q^{∗})^{∗} ⊢ (P ∨ Q)^{∗∗}} ; (P^{∗} ∨ Q^{∗})^{∗} ⊢ (P ∨ Q)^{∗}

Quantifiers:

{P ⊢ ∃x.P \atop P^{∗} ⊢ (∃x.P)^{∗}} ; ∃x.P^{∗} ⊢ (∃x.P)^{∗}  {∃x.P^{∗} ⊢ (∃x.P)^{∗} \atop (∃x.P^{∗})^{∗} ⊢ (∃x.P)^{∗∗}} ; (∃x.P^{∗})^{∗} ⊢ (∃x.P)^{∗}
{∀x.P ⊢ P \atop (∀x.P)^{∗} ⊢ P^{∗}} ; (∀x.P)^{∗} ⊢ ∀x.P^{∗}  {(∀x.P^{∗})^{∗} ⊢ ∀x.P^{∗∗} \atop (∀x.P^{∗})^{∗} ⊢ ∀x.P^{∗}}

Consequences:

P [figure]Q  P^{∗} [figure]Q [figure] P [figure]Q^{∗}  P^{∗} [figure]Q^{∗} [figure]  [figure] P [figure]QP [figure]Q^{∗} [figure] [figure]  P^{∗} [figure]QP^{∗} [figure]Q^{∗} [figure] [figure] (P [figure]Q)^{∗}  (P^{∗} [figure]Q)^{∗} [figure] (P [figure]Q^{∗})^{∗}  (P^{∗} [figure]Q^{∗})^{∗} [figure] [figure] (P [figure]Q)^{∗} (P [figure]Q^{∗})^{∗} [figure] [figure]  (P^{∗} [figure]Q)^{∗} (P^{∗} [figure]Q^{∗})^{∗} [figure] [figure] P [figure]Q (P [figure]Q)^{∗} [figure]  P^{∗} [figure]Q (P^{∗} [figure]Q)^{∗} [figure] P [figure]Q^{∗} (P [figure]Q^{∗})^{∗} [figure] [figure]  P^{∗} [figure]Q^{∗} (P^{∗} [figure]Q^{∗})^{∗} [figure] [figure]  [figure: P ∨ Q; P^{∗} ∨ Q; P ∨ Q^{∗}; P^{∗} ∨ Q^{∗}; P ∨ Q; P ∨ Q^{∗}; P^{∗} ∨ Q; P^{∗} ∨ Q^{∗}; (P ∨ Q)^{∗}; (P^{∗} ∨ Q)^{∗}; (P ∨ Q^{∗})^{∗}; (P^{∗} ∨ Q^{∗})^{∗}; (P ∨ Q)^{∗}; (P ∨ Q^{∗})^{∗}; (P^{∗} ∨ Q)^{∗}; (P^{∗} ∨ Q^{∗})^{∗}; P ∨ Q; (P ∨ Q)^{∗}; P^{∗} ∨ Q; (P^{∗} ∨ Q)^{∗}; P ∨ Q^{∗}; (P ∨ Q^{∗})^{∗}; P^{∗} ∨ Q^{∗}; (P^{∗} ∨ Q^{∗})^{∗}]

[figure: ∃x.P; ∃x.P^{∗}; (∃x.P)^{∗}; (∃x.P^{∗})^{∗}; ∃x.P; (∃x.P)^{∗}; ∃x.P^{∗}; (∃x.P^{∗})^{∗}; ∀x.P; ∀x.P^{∗}; (∀x.P)^{∗}; (∀x.P^{∗})^{∗}; ∀x.P; (∀x.P)^{∗}; ∀x.P^{∗}; (∀x.P^{∗})^{∗}]

Modalities: alternative axioms A Lawvere-Tierney topology is an arrow j : Ω → Ω such that these three diagrams commute:

[figure: 1; Ω; t; 1; Ω; t; Ω; Ω; j; Ω; Ω; j; Ω; Ω; j; Ω; Ω; j; Ω × Ω; Ω; ∧; Ω × Ω; Ω × Ω; j×j; Ω; Ω; j; Ω × Ω; Ω; ∧]

Which means:

ω[⊤] = ω[⊤^{∗}]  ω[P^{∗}] = ω[P^{∗∗}]  ω[P^{∗} ∧ Q^{∗}] = ω[(P ∧ Q)^{∗}]
⊤ ⊢ ⊤^{∗}  P^{∗} ⊢ P^{∗∗}  P^{∗∗} ⊢ P^{∗}
P^{∗} ∧ Q^{∗} ⊢ (P ∧ Q)^{∗}  (P ∧ Q)^{∗} ⊢ P^{∗} ∧ Q^{∗}

It is not clear that these axioms (“LT axioms”) are equivalent to the three axioms (“modality axioms”) that we were using before... We know that the modality axioms imply all the LT axioms, but it is not obvious that the modality axioms ⊤ ⊢ ⊤^{∗}

and {P ⊢ Q \atop P^{∗} ⊢ Q^{∗}}

can be proved from the LT axioms...

Here are the proofs:

{P ⊢ ⊤ ⇔ P \atop P ⊢ ⊤^{∗} ⇔ P^{∗}} ; P ⊢ ⊤ ⇔ P^{∗} ; P ⊢ P^{∗}  {P ⊢ Q \atop ⊤ ⊢ P [figure]Q} ; ⊤ ⊢ P ⇔ (P ∧ Q) ; ⊤ ⊢ P^{∗} ⇔ (P^{∗} ∧ Q^{∗}) ; ⊤ ⊢ P^{∗} [figure]Q^{∗} ; P^{∗} ⊢ Q^{∗}

Double negation is a modality, by hand (1) We need to see that ¬¬(P ∧ Q) ⇔ ¬¬P ∧ ¬¬Q. One direction is easy, and is a consequence of (¬) being a contravariant functor:

[figure: P; ¬P; ¬P; ¬¬P; P; P ∧ Q; ¬P; ¬(P ∧ Q); ¬¬P; ¬¬(P ∧ Q); ¬¬P; ¬¬P ∧ ¬¬Q; P ∧ Q; ¬(P ∧ Q); ¬(P ∧ Q); ¬¬(P ∧ Q); ¬¬(P ∧ Q); ¬¬P ∧ ¬¬Q; P ∧ Q; Q; ¬(P ∧ Q); ¬Q; ¬¬(P ∧ Q); ¬¬Q; ¬¬P ∧ ¬¬Q; ¬¬Q; Q; ¬Q; ¬Q; ¬¬Q]

We can convert this to natural deduction and normalize:

\begin{matrix}{P ∧ Q [figure]P \atop ¬P [figure]¬(P ∧ Q)} ; ¬¬(P ∧ Q) [figure]¬¬P & {P ∧ Q [figure]Q \atop ¬Q [figure]¬(P ∧ Q)} ; ¬¬(P ∧ Q) [figure]¬¬Q \\ ¬¬(P ∧ Q) [figure]¬¬P ∧ ¬¬Q \end{matrix}

\begin{matrix}\begin{matrix}\begin{aligned}{[P ∧ Q]^{1} \atop P} & & [¬P]^{2} \\ & ⊥ \end{aligned} ; ¬(P ∧ Q) ; 1 & ¬¬(P ∧ Q) \\ ⊥ \end{matrix} ; ¬¬P ; 2 & \begin{matrix}\begin{aligned}{[P ∧ Q]^{3} \atop Q} & [¬Q]^{4} \\ & ⊥ \end{aligned} ; ¬(P ∧ Q) ; 1 & ¬¬(P ∧ Q) \\ ⊥ \end{matrix} ; ¬¬Q ; 2 \\ ¬¬P ∧ ¬¬Q \end{matrix}

Double negation is a modality, by hand (2) The converse, (¬¬P ∧ ¬¬Q) [figure]¬¬(P ∧ Q), is much harder (it was for me, at least...) We start with two lemmas:

{¬¬¬P \atop ¬P} (↕)  {¬¬P, Q ⊢ ⊥ \atop P, Q ⊢ ⊥} (↕)

Proofs:

\begin{aligned}¬P & [¬¬P]^{1} \\ & ⊥ \end{aligned} ; ¬¬¬P ; 1  ¬P 2

\begin{aligned}¬¬P Q ; ⋮ . ; ⊥ & ⇒ & ¬¬P Q ; ⋮ . ; ⊥ \\ P Q ; ⋮ . ; ⊥ & ⇒ & \begin{matrix}¬P 1 & ¬¬P \\ ⊥ \end{matrix} \end{aligned}

Now we can prove (¬¬P ∧ ¬¬Q) [figure]−¬¬(P ∧ Q) by reducing a “hard” sequent to several simpler ones, then convert the simplest one to a small ND proof (the bottom sequent at the left corresponds to the three top lines at the right), then build bigger trees corresponding to more complex sequents.

\begin{matrix}{¬¬P, ¬¬Q ⊢ ¬¬(P ∧ Q) \atop ¬¬P, ¬¬Q, ¬(P ∧ Q) ⊢ ⊥} & (↕) \\ P, ¬¬Q, ¬(P ∧ Q) ⊢ ⊥ \end{matrix} ; (↕) ; P, Q, ¬(P ∧ Q) ⊢ ⊥ ; (↕)\begin{matrix}¬P 2 & ¬¬P \\ ⊥ \end{matrix} ; ¬¬(P ∧ Q) 3

Downcasing the closure operator

[figure: \begin{matrix}f^{−1}(\{ b | P (b) \}) \\ = \{ a | P (f(a)) \} \end{matrix}; \{ b | P (b) \}; \begin{matrix}f^{−1}(\overline{\{ b | P (b) \}}) \\ = f^{−1}(\{ b | P (b)^{∗} \}) \\ = \{ a | P (f(a))^{∗} \} \\ = \overline{\{ a | P (f(a)) \}} \\ = \overline{f^{−1}(\{ b | P (b) \})} \end{matrix}; \overline{\{ b | P (b) \}} ; = \{ b | P (b)^{∗}) \}; A; B; f; \begin{matrix}f^{−1}(\{ b | P (b) \}) \\ = \{ a | P (f(a)) \} \end{matrix}; A; \begin{matrix}f^{−1}(\{ b | P (b) \}) \\ = \{ a | P (f(a)) \} \end{matrix}; \begin{matrix}f^{−1}(\overline{\{ b | P (b) \}}) \\ = f^{−1}(\{ b | P (b)^{∗} \}) \\ = \{ a | P (f(a))^{∗} \} \\ = \overline{\{ a | P (f(a)) \}} \\ = \overline{f^{−1}(\{ b | P (b) \})} \end{matrix}; \begin{matrix}f^{−1}(\overline{\{ b | P (b) \}}) \\ = f^{−1}(\{ b | P (b)^{∗} \}) \\ = \{ a | P (f(a))^{∗} \} \\ = \overline{\{ a | P (f(a)) \}} \\ = \overline{f^{−1}(\{ b | P (b) \})} \end{matrix}; A; \{ b | P (b) \}; B; \{ b | P (b) \}; \overline{\{ b | P (b) \}} ; = \{ b | P (b)^{∗}) \}; \overline{\{ b | P (b) \}} ; = \{ b | P (b)^{∗}) \}; B]

[figure: a|_{P}; b|_{P}; a|\overline{P}; b|\overline{P}; a; b; a|_{P}; a; a|_{P}; a|\overline{P}; a|\overline{P}; a; b|_{P}; b; b|_{P}; b|\overline{P}; b|\overline{P}; b]

Saturated covers

[figure: U^{••}; U^{•}; U^{•}; U^{∘}; U^{••}; U^{▲▲}; U^{•}; U^{▲}; U^{∘}; U^{△}; U^{▲▲}; U^{▲}; U^{▲}; U^{△}]
[figure: Ω^{••}(U); Ω^{•}(U); Ω^{•}(U); Ω^{∘}(U); Ω^{••}(U); Ω^{▲▲}(U); Ω^{•}(U); Ω^{▲}(U); Ω^{∘}(U); Ω^{△}(U); Ω^{▲▲}(U); Ω^{▲}(U); Ω^{▲}(U); Ω^{△}(U)]

[figure: ω_{U}^{••}; ω_{U}^{•}; ω_{U}^{•}; ω_{U}^{∘}; ω_{U}^{••}; ω_{U}^{▲▲}; ω_{U}^{•}; ω_{U}^{▲}; ω_{U}^{∘}; ω_{U}^{△}; ω_{U}^{▲▲}; ω_{U}^{▲}; ω_{U}^{▲}; ω_{U}^{△}]

Notes:

Ω^{••}(U) supersaturated, covering U, singleton
Ω^{•}(U) saturated covering U
Ω^{∘}(U) covering U
Ω^{▲▲}(U) supersaturated or empty, subcovering U
Ω^{▲}(U) saturated, subcovering U
Ω^{△}(U) subcovering U

Comparison of notations: Harold Simmons (p.5):

\begin{matrix}Ω[U] & Ω^{••}(U) \\ Ω⟨U⟩ & Ω^{•}(U) \\ Ω(U) & Ω^{▲}(U) \end{matrix}

MacLane/Moerdijk:

Ω(U) Ω^{▲}(U)

Let A(·) be a presheaf.

A is separated when: ∀U^{•}.(a_{U} [figure] a_{U^{•}})
A is collated when: ∀U^{•}.(a_{U} [figure] a_{U^{•}})
A is a sheaf when:  ∀U^{•}.(a_{U} [figure] a_{U^{•}})

Saturation in prestacks Notation: a_{U^{•}} ⊆ A is a saturated, coherent family, with support U^{•}. A family a_{U^{•}} ⊆ A in a prestack A is: saturated when ∀V ∈ U^{•}.∀W.(a_{V} · W ∈ a_{U^{•}}), coherent when ⟦·⟧ : a_{U^{•}} → U^{•} is a bijection.

A prestack A is:

separated when: ∀a_{U}.∀U^{•}.(a_{U} [figure] a_{U^{•}})
collated when: ∀a_{U}.∀U^{•}.(a_{U} [figure] a_{U^{•}})
a stack when:  ∀a_{U}.∀U^{•}.(a_{U} [figure] a_{U^{•}})

where a_{U^{•}} := a_{U} · U^{•}.

[figure: J; 1; J; Ω; 1; Ω; t; Ω; Ω; j; Ω^{•}(V); 1; Ω^{•}(W); 1; Ω^{▲}(V); Ω^{▲}(V); ▲▲; Ω^{▲}(W); Ω^{▲}(W); ▲▲; Ω^{•}(V); Ω^{•}(W); 1; 1; Ω^{▲}(V); Ω^{▲}(W); Ω^{▲}(V); Ω^{▲}(W); Ω^{•}(V); Ω^{▲}(V); 1; Ω^{▲}(V); Ω^{•}(W); Ω^{▲}(W); 1; Ω^{▲}(W); W; V; W; V]

The classifier object:

Ω : O(X)^{op} → Set
U ↦ Ω(U) ≡ Ω^{▲}(U)

A covering system, a.k.a. a Grothendieck topology:

K : O(X)^{op} → P Ω^{▲}(X)
U ↦ K(U) ≡ a family of “covering sieves” on U
U ↦ Ω^{•}(U) ⊆ Ω^{▲}(U)

A site: (O(X), K) A covering system gives us a notion of “sheaf”: an object A ∈ Set^{O(X)^{op}} is a presheaf: \begin{matrix}A : O(X)^{op} & → & Set \\ U^{op} & ↦ & A(U) \end{matrix}

A is a sheaf when ∀U.∀U^{•}.(a_{U}↦a_{U^{•}} is a bijection)

The algebra of covers: a lemma Theorem: for all W^{•} and V^{•}, W^{•} ∧ V^{•} is a saturated cover of W ∧ V. The saturation part is obvious; what is tricky there is to see that ⋃(W^{•} ∧ V^{•}) = (⋃ W^{•}) ∧ (⋃ V^{•}). This only happens because Ω is a frame.

We will prove something stronger: ⋃(W^{△} ∧ V^{△}) = (⋃ W^{△}) ∧ (⋃ V^{△}) for a harder definition of W^{△} ∧ V^{△} (not (∧) = (∩)).

Definitions: W^{△} ∧ V^{△} := { W′ ∧ V′ | W′ ∈ W^{△}, V′ ∈ V^{△} } W^{△} ∧ V := { W′ ∧ V | W′ ∈ W^{△} } W ∧ V^{△} := { W ∧ V′ | V′ ∈ V^{△} } When W^{△} and V^{△} are saturated, (∧) = (∩).

Lemma: when W^{△} = {W_{1}, W_{2}}, then (⋃ W^{△}) ∧ V = ⋃(W^{△} ∧ V). Proof: as (∧V) ⊢ (V [figure]), the functor (∧V) preserves colimits:

(W_{1} ∨ W_{2}) ∧ V  W_{1} ∨ W_{2} [figure] W_{1} ∨ W_{2}  (W_{1}, W_{2}) [figure] (W_{1}, W_{2}) (W_{1} ∧ V, W_{2} ∧ V) [figure] (W_{1} ∧ V, W_{2} ∧ V)  (W_{1} ∧ V) ∨ (W_{2} ∧ V) [figure] U  V [figure]U [figure] V [figure]U  (V [figure]U, V [figure]U) [figure] (V [figure]U, V [figure]U)  (U, U) [figure] (U, U)  U [figure] (W_{1} ∨ W_{2}) ∧ V U[figure]  W_{1} ∨ W_{2} V [figure]U [figure]  (W_{1}, W_{2}) (V [figure]U, V [figure]U) [figure]  (W_{1} ∧ V, W_{2} ∧ V) (U, U) [figure]  (W_{1} ∧ V) ∨ (W_{2} ∧ V) U[figure] [figure] [figure]  [figure] [figure]  [figure] [figure]  [figure] [figure]

Lemma: for any W^{△} and V, (⋃ W^{△}) ∧ V = ⋃(W^{△} ∧ V) Proof: generalize the diagram above.

Theorem: for any W^{△} and V^{△}, ⋃(W^{△} ∧ V^{△}) = (⋃ W^{△}) ∧ (⋃ V^{△}) Proof: ⋃(W^{△} ∧ V^{△}) = ⋃_{V′∈V^{△}}(⋃(W^{△} ∧ V′)) = (⋃ W^{△}) ∧ (⋃ V^{△}) (wrong; check and correct)

The algebra of covers: an (imaginary) finest cover Definition: U^{•} ∧ V^{•} := U^{•} ∩ V^{•} Lemma: ⋃(U^{•} ∧ V^{•}) = ⋃ U^{•} ∧ ⋃ V^{•} = U ∧ V Definition: ⊤_{U} := colim U^{•} = ⋁ Ω^{•}(U) = U^{••} Definition: ⊥_{U} := lim U^{•} = ⋀ Ω^{•}(U) ⊤_{U} is the biggest possible cover for U, ⊥_{U} is the finest possible saturated cover for U. Trick: sometimes F (⊥_{U}) will make sense, but ⊥_{U} will not exist. Motivation: notation for preservation of limits (as below).

[figure: A ×_{C} B; B; A ×_{C} B; A; B; C; A; C; \begin{matrix}F (A ×_{C} B) ≅ \\ F (A) ×_{F (C)} F (B) \end{matrix}; F (B); \begin{matrix}F (A ×_{C} B) ≅ \\ F (A) ×_{F (C)} F (B) \end{matrix}; F (A); F (B); F (C); F (A); F (C)]

Definition: A^{+}(U) := colim_{U^{•}}A(U^{•}) We will write this as: A^{+}(U) := A(⊥_{U}) = A(lim_{U^{•}} U^{•}) More explicitly: an a_{U}^{+} = a_{⊥_{U}} is a pair (U^{•}, a_{U^{•}}) modulo an equivalence relation: (U^{•}′, a′_{U^{•}′}) ∼ (U^{•}′′, a′′_{U^{•}′′}) when the set of indices where a′_{U^{•}′} and a′′_{U^{•}′′} coincide is a (saturated) cover of U.

Geometric Morphisms A geometric morphism, f : ℱ → ℰ,

is an adjunction, ℱ [figure: f^{∗}; f_{∗}] ℰ,

where f^{∗} ⊣ f_{∗} and f^{∗} is “left exact”, i.e., preserves finite limits.

f^{∗} is called the inverse image, and f_{∗} is called the direct image of f.

If f^{∗} has a left adjoint, f_{!} (i.e., f_{!} ⊣ f^{∗} ⊣ f_{∗}) which is a stronger condition than f^{∗} being left exact, then we say that f is essential.

ℱ [figure: f^{∗}; f_{!}; f_{∗}] ℰ

Facts: Each continuous map f : X → Y induces a geometric morphism Shv(X) → Shv(Y). (Does it extend to Psh(X) → Psh(Y)?) For a topological space X, the inclusion Shv(X) → Set^{O(X)^{op}} is (the direct image of) a geometric morphism.

What happens in the case of discrete topological spaces? Shv(X) ≅ Set^{X}, where the X in Set^{X} is a the set of points of the topological space, seen as a discrete category.

Geometric morphisms (2) Two examples, associated to maps between discrete topological spaces:

[figure: A; (A, 0); A; B; (A, 0); (B, B′); B; (B, B′); B; C; (B, B′); (C, 1); C; (C, 1); _{Set_{{α}}}; _{Set_{{α,β}}}; {α}; {α, β}; a; (a; ⊥); a; b; (a; ⊥); (b; b′); b; (b; b′); b; c; (b; b′); (c;^{∗}); c; (c;^{∗})]

Another one:

[figure: (A_{i})_{i∈ℕ}; Σi:ℕ.A_{i}; (A_{i})_{i∈ℕ}; (B)_{i∈ℕ}; Σi:ℕ.A_{i}; B; (B)_{i∈ℕ}; B; (B)_{i∈ℕ}; (C_{i})_{i∈ℕ}; B; Πi:ℕ.C_{i}; (C_{i})_{i∈ℕ}; Πi:ℕ.C_{i}; _{Set_{ℕ}}; Set; ℕ; {1}; i; a_{i}; i, a_{i}; i; a_{i}; i; b; i, a_{i}; b; i; b; b; i; b; i; c_{i}; b; i↦c_{i}; i; c_{i}; i↦c_{i}]

Johnstone: filter-powers

Johnstone, 9.41: We start with a left exact morphism L between toposes. In the case that interests us it is the direct image of an essential geometric morphism; moreover, its inverse image is logical. Diagram:

[figure: (A_{i})_{i∈ℕ}; Σ_{i}A_{i}; (A_{i})_{i∈ℕ}; (B)_{i∈ℕ}; Σ_{i}A_{i}; B; (B)_{i∈ℕ}; B; (B)_{i∈ℕ}; (C_{i})_{i∈ℕ}; B; Π_{i}C_{i}; (C_{i})_{i∈ℕ}; Π_{i}C_{i}; L; ℰ; ℱ; L]

A filter on L is a morphism Φ : L(Ω_{ℰ} ) → Ω_{ℱ} that is an ∧-semilattice morphism, i.e., it respects ∧ and ⊤. In our archetypical case it is a morphism Φ : Ω^{ℕ} → Ω that looks at each point of Ω^{ℕ} as if were a characteristic function of a subset of ℕ, and then returns 1 when that subset is F-big, and 0 when not, where F is our filter on ℕ.

[figure: U; 1_{ℰ}; U; 1_{ℰ}; 1_{ℰ}; Ω_{ℰ}; t_{ℰ}; 1_{ℰ}; Ω_{ℰ}; u; L(1_{ℰ} ); L(Ω_{ℰ} ); L(u); L(1_{ℰ} ); Ω_{ℱ}; t; L(Ω_{ℰ} ); Ω_{ℱ}; Φ; (U_{i})_{i∈ℕ}; (1)_{i∈ℕ}; (U_{i})_{i∈ℕ}; (1)_{i∈ℕ}; (1)_{i∈ℕ}; (Ω)_{i∈ℕ}; t_{ℰ}; (1)_{i∈ℕ}; (Ω)_{i∈ℕ}; u; 1; Ω^{ℕ}; L(u); 1; Ω; t; Ω^{ℕ}; Ω; Φ]

A subobject U ↣ 1_{ℰ} , and its characteristic morphism u, are said to be Φdense (note the correspondence between Johnstone’s Φ and our filter F on ℕ) when Φ ∘ L(u) = t, i.e., in our archetypical case, when it takes 1 to a point of Ω^{ℕ} that represents an F-big set.

A note on filter-powers

Now for each Φ-dense subobject U ↣ 1_{ℰ} (in the archetypical case: for F-big subsets of the index set ℕ) there is a pullback functor U^{∗} : ℰ → ℰ /U; and each monic V ↣ U between Φ-dense subobjects induces a functor ℰ /U → ℰ /V. The (filtered) colimit of all these functors is a functor P_{Φ} : ℰ → ℰ_{Φ}; it turns out that ℰ_{Φ} is a topos, and that all these pullback functors are logical morphisms; I think that they are also the inverse images of essential geometric morphisms, but I am not totally sure; and P_{Φ} is also logical (but not usually a direct image of an essential geometric morphism).