# 7.4 Toposes#

```
from IPython.display import Image
```

## 7.4.1 The subobject classifier Ξ© in a sheaf topos#

### βοΈ One-point Ξ©#

See also Exercise 7.52.

```
Image('raster/solution-7-52.png')
```

## Show code cell output

### βοΈ Exercise 7.53#

See also Exercise 7.53.

```
Image('raster/solution-7-53.png')
```

## Show code cell output

### Ξ© satisfies sheaf condition#

To see that \(\Omega\) as defined in Eq. (7.50) satisfies the sheaf condition (see Definition 7.35), suppose that we have a cover \(U=\cup_{i\in I}U_{i}\), and suppose weβre given an element \(V_i β \Omega(U_i)\), i.e. an open set \(V_i β U_i\), for each \(i β I\). Suppose further that for all \(i,j β I\), it is the case that \(V_i β© U_j = V_j β© U_i\), i.e. that the elements form a matching family. Define \(V:=\cup_{i\in I}V_{i}\); it is an open subset of \(U\), so we can consider \(V\) as an element of \(\Omega(π)\). The following verifies that \(V\) is indeed a gluing for the \((V_{i})_{i\in I}\):

\[ V\cap U_{j}=\left(\bigcup_{i\in I}V_{i}\right)\cap U_{j}=\bigcup_{i\in I}(V_{i}\cap U_{j})=\bigcup_{i\in I}(V_{i}\cap U_{i}))=\left(\bigcup_{i\in I}U_{i}\right)\cap V_{j}=V_{j} \]In other words \(π β© π_π = π_π\) for any \(π β πΌ\). So our \(\Omega\) has been upgraded from presheaf to sheaf!

To be clear, the \(V_i\) are the sections \(s_i\). A term like \(s_i|_{U_iβ©U_j}\) can then be rewritten \(V_i|_{U_iβ©U_j}\) or \(V_iβ©(U_iβ©U_j)\) and because we know \(V_i β U_i\) this reduces to \(V_iβ©U_j\). This proof shows that a gluing exists, but not that it is unique (there is at most one gluing). Weβll take that on trust.

### Sheaf morphism for true#

The section Subobject classifier Β§ Sheaves of sets provides an equivalent definition:

The category of sheaves of sets on a topological space \(X\) has a subobject classifier \(Ξ©\) which can be described as follows: For any open set \(U\) of \(X\), \(Ξ©(U)\) is the set of all open subsets of \(U\). The terminal object is the sheaf 1 which assigns the singleton \(\{*\}\) to every open set \(U\) of \(X\). The morphism \(Ξ·:1 β Ξ©\) is given by the family of maps \(Ξ·_UΒ : 1(U) β Ξ©(U)\) defined by \(Ξ·_U(*)=U\) for every open set \(U\) of \(X\).

We could alternatively describe {1} as the Constant presheaf with value {1} (or \(\{*\}\)), which happens to also be a sheaf. Hereβs a visualization of the natural transformation `true`

(in purple) on the two-element discrete topological space:

Notice that `true`

always points to the βlargest open setβ that it can, as the author suggests. Itβs not hard to imagine `true`

for the SierpiΕski space; to imagine it for the three-element discrete topological space one might want to draw the open subsets in a cube.

### Upshot#

Upshot: Truth values are open sets.The point is that the truth values in the topos of sheaves on a space \((π, \textbf{Op})\) are the open sets of that space. When someone says βis property \(π\) true?,β the answer is not yes or no, but βit is true on the open subset \(π\).β If this \(π\) is everything, \(π = π\), then \(π\) is really true; if \(π\) is nothing, \(π = β \), then \(π\) is really false. But in general, itβs just true some places and not others.

See a similar βupshotβ in Subobject classifier Β§ Sheaves of sets:

Roughly speaking an assertion inside this topos is variably true or false, and its truth value from the viewpoint of an open subset

Uis the open subset ofUwhere the assertion is true.

See also Truth value Β§ In other theories; a truth-valued function is not necessarily a Truth function. That is, a truth-valued function must only return a truth value while a truth function must both accept and return a truth function (see also Section 7.4.5). The author will soon start to use the language of βtruth valueβ heavily.

### β Example 7.54#

### Inconsistent β?β notation#

The author seems to be inconsistently using the β?β notation. Should we fill the ? with the monic morphism \(m\) as in (7.13), or the subobject \(H\) as in Example 7.54? The article Subobject classifier is also inconsistent, using \(Ο_A\) where \(A\) is the subobject at the start, then \(Ο_j\) where \(j\) is the monic morphism. See also Quasi-quotation and List of logic symbols.

### βοΈ Exercise 7.55#

See also Exercise 7.55.

```
Image('raster/solution-7-55.png')
```

## Show code cell output

The authorβs solution seems to replace \(H\) with \(G'\).

## 7.4.2 Logic in a sheaf topos#

Letβs consider the logical connectives \(\text{AND}\), \(\text{OR}\), \(\text{IMPLIES}\), and \(\text{NOT}\). Suppose we have a topological space \(X \in \textbf{Op}\). Given two open sets \(U, V\), considered as truth values \(U, V \in \Omega(X)\), then their conjunction

`U AND V`

is their intersection, and their disjunction`U OR V`

is their union:\[\begin{split} \begin{align*} (U \wedge V) &:= U \cap V \\ (U \vee V) &:= U \cup V \\ \end{align*} \end{split}\]These formulas are easy to remember, because β§ looks like β© and β¨ looks like βͺ. The implication \(U β V\) is the largest open set \(R\) such that \(R β© U β V\), i.e.

\[ (U \Rightarrow V) := \bigcap_{R \in \textbf{Op} \mid R \cap U \subseteq V} R \]In general, it is not easy to reduce this last equation further, so implication is the hardest logical connective to think about topologically.

The author writes \(U,V β \Omega(X)\) when previously he was using \(\Omega(U)\) alongside \(U'\) for the open subsets. Presumably \(X\) is the whole set, so that \(U,V\) should be seen as elements of \(Ξ©(X)\) (sections) rather than as elements in the open set poset. Of course, these lists of open subsets of \(X\) will be the same.

Compare (7.57) to the proof of Proposition 2.98 in Section 2.5. An arguably simpler definition than (7.57), from Heyting algebra Β§ Examples:

Every topology provides a complete Heyting algebra in the form of its open set lattice. In this case, the element \(AβB\) is the interior of the union of \(A^c\) and \(B\), where \(A^c\) denotes the complement of the open set \(A\). Not all complete Heyting algebras are of this form. These issues are studied in pointless topology, where complete Heyting algebras are also called

framesorlocales.

Another name for this concept is the Relative pseudocomplement. A relative pseudocomplement of *a* with respect to *b* is a maximal element *c* such that *a*β§*c*β€*b*. This operation is denoted *a*β*b*. If we know that *a*β*b*, then we know we are in a world where given an *a* we can always construct a *b*. That is, it should be the case that \(aβ§(aβb)β€b\).

The author is introducing Β¬ as a symbol for the Pseudocomplement; from that article:

If

Xis a topological space, the (open set) topology onXis a pseudocomplemented (and distributive) lattice with the meet and join being the usual union and intersection of open sets. The pseudocomplement of an open setAis the interior of the set complement ofA.

Using Β¬ for a pseudocomplement is potentially dangerous, because we may expect it to act like a complement (see Exercise 7.59).

The pseudocomplement is defined as the greatest element \(x^* β L\) with the property that \(x β§ x^* = 0\). By taking the complement, we ensure that \(x β§ x^* = 0\). However, we also need to ensure that we return an open set (the complement must be a closed set, but is not guaranteed to be open). The interior of a set is the largest open set contained in a set, so by applying it we get the greatest element satisyfing our condition that is also an open set.

We take the interior as part of the calculation of the Relative pseudocomplement above for the same reason.

### β Example 7.58#

### Implies in the standard β sheaf topos#

Another way to define the Material conditional (implies) \(p β q\) is as \(q β¨ Β¬p\), though this translation requires reading it backwards. You can think about implication in Example 7.58 by imagining two number lines on top of each other with the antecedent on the bottom; when the top line is false and the bottom is true the result is not part of the resulting open set. Equivalently, the resulting open set is all parts of the line where the top line is true or the bottom line is false.

This strategy works for the standard topology on the real line, but would break down with more exotic topologies on it.

### βοΈ Exercise 7.59#

See also Exercise 7.59.

```
Image('raster/solution-7-59.png')
```

## Show code cell output

### βοΈ Exercise 7.60#

```
Image('raster/solution-7-60.png')
```

## Show code cell output

### β Example 7.61#

For a longer list of internal logics associated to their categories, see Heyting category in nLab. A similar list is in internal logic in nLab.

See also differential geometry - Applications of Topos Theory to the theory of bundles. - MSE, though thereβs little here other than a request for more information.

## 7.4.3 Predicates#

In English, a predicate is the part of the sentence that comes after the subject. For example ββ¦ is evenβ or ββ¦ likes the weatherβ are predicates. Not every subject makes sense for a given predicate; e.g. the sentence β7 is evenβ may be false, but it makes sense. In contrast, the sentence β2.7 is evenβ does not really make sense, and β2.7 likes the weatherβ certainly doesnβt. In computer science, they might say βThe expression β2.7 likes the weatherβ does not type check.β

The point is that each predicate is associated to a type, namely the type of subject that makes sense for that predicate. When we apply a predicate to a subject of the appropriate type, the result has a truth value: β7 is evenβ is either true or false. Perhaps βBob likes the weatherβ is true some days and false on others. In fact, this truth value might change by the year (bad weather this year), by the season, by the hour, etc. In English, we expect truth values of sentences to change over time, which is exactly the motivation for this chapter. Weβre working toward a logic where truth values change over time.

### Disambiguate: Proposition and predicate#

The author will soon use the terms βpropositionβ and βpredicateβ in a more βgeneralβ way than it is used elsewhere; letβs review some original meanings before we try to generalize it. As discussed in Proposition (disambiguation) and Proposition, the word has a long history (itβs used as a translation of concepts going back to Aristotle):

Propositions have played a large role throughout the history of logic, linguistics, philosophy of language, and related disciplines. Some researchers have doubted whether a consistent definition of propositionhood is possible, David Lewis even remarking that βthe conception we associate with the word βpropositionβ may be something of a jumble of conflicting desiderataβ. The term is often used broadly and has been used to refer to various related concepts.

See also Proposition Β§ Objections to propositions. Weβll avoid the unadorned terms βpropositionβ and βpredicateβ but define βset propositionβ and βset predicateβ in a way related to the common definition:

Formally, propositions are often modeled as functions which map a possible world to a truth value. For instance, the proposition that the sky is blue can be modeled as a function which would return the truth value \(T\) if given the actual world as input, but would return \(F\) if given some alternate world where the sky is green. However, a number of alternative formalizations have been proposed, notably the

structured propositionsview.

See also Propositional function. So a proposition is essentially a nullary function (defined by the function name) and a predicate is a unary, binary, etc. function (defined by both the name and the mapping). This definition roughly agrees with Propositional calculus, the models defined in forall x: Part V First-order logic and forall x: Part VI Interpretations, and Predicate (mathematical logic).

### Topological predicate#

In a topos \(\mathcal{E} = \textbf{Shv}(X, \textbf{Op})\), a predicate is a sheaf morphism \(p: S β \Omega\) where \(S β \mathcal{E}\) is a sheaf and \(\Omega β \mathcal{E}\) is the subobject classifier, the sheaf of truth values. By Definition 7.35 we get a function \(p(U) : S(U) β \Omega(U)\) for any open set \(U β X\). In the above example - which we will discuss more carefully in Section 7.5 - if π is the sheaf of people (people come and go over time), and \(Bob β S(U)\) is a person existing over a time \(U\), and \(p\) is the predicate ββ¦ likes the weatherβ then \(p(Bob)\) is the set of times during which \(Bob\) likes the weather. So the answer to βBob likes the weatherβ is something like βin summers yes, and also in April 2018 and May 2019 yes, but in all other times no.β Thatβs \(p(Bob)\), the temporal truth value obtained by applying the predicate \(p\) to the subject Bob.

Given the author previously used \(P\) for a presheaf, the \(S\) in this section likely stands for sheaf.

### βοΈ Exercise 7.62#

Just now we described how a predicate \(π: π β Ξ©\), such as ββ¦ likes the weatherβ acts on sections \(π β π(π)\), say \(π = Bob\). But by Definition 7.12, any predicate \(π: π β Ξ©\) also defines a subobject of \(\{π\;|\;π\} β π\). Describe the sections of this subsheaf.

See Exercise 7.62; the answer to this question may not be obvious if youβve not read Section 7.5.

### π΄ The subobjects poset#

The poset of subobjects.For a topos \(\mathcal{E} = \textbf{Shv}(X, \textbf{Op})\) and object (sheaf) \(S β \mathcal{E}\), the set of \(S\)-predicates \(|\Omega^S| = \mathcal{E}(S, \Omega)\) is naturally given the structure of a poset, which we denote:\[ (|\Omega^{S}|,\leq^{S}) \]

### π΄ Power object#

The content of Example 7.54 is also discussed in Power set Β§ Power object, using similar variable names:

Certain classes of algebras enjoy both of these properties. The first property is more common; the case of having both is relatively rare. One class that does have both is that of multigraphs. Given two multigraphs

GandH, a homomorphismhΒ :GβHconsists of two functions, one mapping vertices to vertices and the other mapping edges to edges. The set \(H^G\) of homomorphisms fromGtoHcan then be organized as the graph whose vertices and edges are respectively the vertex and edge functions appearing in that set. Furthermore, the subgraphs of a multigraphGare in bijection with the graph homomorphisms fromGto the multigraph Ξ© definable as the complete directed graph on two vertices (hence four edges, namely two self-loops and two more edges forming a cycle) augmented with a fifth edge, namely a second self-loop at one of the vertices. We can therefore organize the subgraphs ofGas the multigraph \(Ξ©^G\), called thepower objectofG.

Notice the notational similarity to what the author is calling the subobjects poset. Weβll often prefer the term βpower objectβ to βsubobjects posetβ going forward. Weβll also avoid the vertical bar on either side of Ξ© that seems to be preferred by the author; this conflicts with e.g. Power set where adding vertical bars indicates a reference to the cardinality of the set of functions rather than the set of functions.

Per Elementary topoi Β§ Formal definition, the defining characteristic of an elementary topos is that every object (in this case, sheaf) has a power object.

### Topological LTE#

Given two predicates \(p,q : S β \Omega\), we say that \(p β€^S q\) if the first implies the second. More precisely, for any \(U β \textbf{Op}\) and section \(π β S(U)\) we obtain two open subsets \(p(π ) β π\) and \(q(π ) β π\). We say that \(p β€^π q\) if \(p(π ) β q(π )\) for all \(U β \textbf{Op}\) and \(π β π(π)\). We often drop the superscript from \(β€^S\) and simply write \(β€\). In formal logic notation, one might write \(p β€^S q\) using the β’ symbol, e.g. in one of the following ways:

\[\begin{split} \begin{align} \\ s:S\mid p(s) & \vdash q(s) \\ p(s) & \vdash_{s:S}\;q\big(s\big) \end{align} \end{split}\]In particular, if \(S = 1\) is the terminal object, we denote \(|\Omega^S|\) by \(|\Omega|\), and refer to elements \(p β |\Omega|\) as propositions. They are just morphisms \(p : 1 β \Omega\).

This preorder is partially ordered β a poset β meaning that if \(p β€ q\) and \(q β€ p\) then \(p = q\). The reason is that for any subsets \(U,V β X\), if \(U β V\) and \(V β U\) then \(U = V\).

The author uses the language βthe first implies the secondβ but we prefer to desymbolize β€ to βif either the second or not the firstβ or simply the βfirst is less than or equal to the secondβ (when it means the material conditional). To decode \(p β€^S q\), or equivalently \(p β’_S q\), we might say β\(p(s)\) is a subset of \(q(s)\) for all \(s\) in \(S(U)\), for all \(U\) in \(\textbf{Op}\)β (see also Python Β§ 5.1.4. Nested List Comprehensions).

### β Set propositions#

See Propositional calculus and in particular the sections on truth-functional propositional logic (and Truth-functional logic: Calgary for an introduction). In **Set** these are maps from the one-object category to the booleans, true and false. A picture to have in mind is (see also Exercise 7.52):

A proposition like βThe dog is brown.β is often simply assigned to a letter in logic, such as \(B\) (see the βsymbolization keyβ introduced in Chapter 4 Β§ Atomic sentences). We can see Ξ· (trivially a natural transformation) in this scenario as that letter. If we had mapped \(*\) to the empty set, then the proposition would be `false`

.

We can then define operators like \(β§\) on sets to get the rest of TFL. For example, the author defined \((U \wedge V) := U \cap V\) above. If we define the symbolization key:

\(A\): Alice is quick

\(B\): Bob is quick

Then in a model where both of these are mapped to true, we have that \((A \wedge B) := A \cap B = \{1\} \cap \{1\} = \{1\}\) which is `true`

. Itβs not hard to check that β works as expected as well.

If youβve worked through forall x then you may be expecting to use multiple terms on the left side of the Sequent as in \(A,B β’ C\). As discussed in sequent, the \(A,B\) in \(A,B β’ C\) can be replaced by \(Aβ©B\). At the start of the proof, you can then simply use logical Conjunction elimination twice to separate A and B.

### β Set predicates#

Weβll start with an example in an interpretation with only two names. Does \(p\) entail \(q\)? The two set predicates:

The same data in a more visual form:

We need only consider two sections, A and B. In both cases \(p(s) β q(s)\), so weβd say that \(p β’ q\) or more verbosely that \(p(π ) β’_{π :π} q(π )\). It is not the case that \(q β’ p\), so a βpartial subobjects posetβ is p β q. Given the drawing above it may be clearer to write q β p; this is the subobjects poset because the green arrows point to something to the right or the same as the purple arrows.

Our partial subobjects poset p β q is βpartialβ because \(Ξ©^S\) is defined for all possible \(S\)-predicates, not just the first two that we think of. There are only two more possible predicates:

It may be tempting to simplify the model above by merely listing what objects a predicate is to be true of; this corresponds to the method of stipulating the extension of a predicate via enumeration discussed in forall x Β§ Chapter 30 Extensionality. See also Exercise 2.36.

Perhaps uninterestingly, this makes it clear the βsubobjects posetβ \(Ξ©^S\) (that we will often be calling, as discussed above, the βpower objectβ) is equivalent to the power set of \(S\). That is, alternative notations for this power object might be \(\Omega^{\{A,B\}}\) or \(2^{\{A,B\}}\). In the language of the definition above, we would say that the set of \(\{A,B\}\)-predicates \(|\Omega^{\{A,B\}}|\) is \(\{p,q,r,s\}\):

Letβs say that A stands for Alice, and B stands for Bob. Weβll also define \(p\) to mean Peruvian and \(q\) to mean quick. As a table of observations:

```
import pandas as pd
pd.DataFrame({'p': [False, True], 'q': [True, True]}, index=['A', 'B'])
```

p | q | |
---|---|---|

A | False | True |

B | True | True |

Assigning βsemanticsβ like this (linking to the real world) makes it clear that using this model will likely fail when itβs forced to generalize out of the training set. If we were to add a third piece of data (world) perhaps associated with a person named Carlos, it would likely contradict our earlier/simpler model. The maps \(p\) and \(q\) will simply change so that they no longer imply one another. This is a weakness of the material conditional; itβs simple and can hence only fit simple data (if the goal is a perfect fit).

What are \(A\) and \(B\) in this context? We could see them as people (Alice and Bob) that we map to truth values. We could see them as possible worlds as mentioned above and explained in Proposition:

Formally, propositions are often modeled as functions which map a possible world to a truth value. For instance, the proposition that the sky is blue can be modeled as a function which would return the truth value \(T\) if given the actual world as input, but would return \(F\) if given some alternate world where the sky is green.

In this view, these are βpossible peopleβ and in our world there are only two possible people. We could also (as the author mentions) see \(S\) as a type and the sections \(s β S\) as possible values that the type can take on. So if we define \(p\) as ββ¦likes the weatherβ then while β2.7 likes the weatherβ doesnβt type check, the statement βBob likes the weatherβ should because \(p\) is an instance of a \(Person\)-predicate (where \(Person\) is a type).

### β Topological propositions#

Letβs move on to a more complicated example of a proposition, now in the context of the two-point discrete topological space. The requirement that these be a Natural transformation is going to start to limit what counts as a proposition. Consider the following non-example:

This infranatural transformation is not a proposition because it is not a natural transformation. Using the following from Natural transformation Β§ Definition:

We always have that \(F(f) = 1(f)\) is the identity on the one object in **1**, so this reduces to:

While this is true for \(Ξ·_{\{1\}} = G(f) β Ξ·_{\{0,1\}}\) (using part of the green restriction morphism) this fails for \(Ξ·_{\{0\}} = G(f) β Ξ·_{\{0,1\}}\) (using part of the red restriction morphism). In the following we fix this issue:

Why must a morphism of sheaves be a natural transformation? From Sheaf (mathematics) Β§ Morphisms:

Morphisms of sheaves are, roughly speaking, analogous to functions between them. In contrast to a function between sets, which is simply an assignment of outputs to inputs, morphisms of sheaves are also required to be compatible with the localβglobal structures of the underlying sheaves. This idea is made precise in the following definition.

The article goes on to essentially define a morphism of sheaves as a natural transformation. The end of the section e.g. defines an isomorphism of sheaves as a natural isomorphism.

#### More than true and false#

We now have more than just βtrueβ and βfalseβ that can be assigned to a proposition; even in this simple example there are two propositions that are neither true or false and are furthermore unequal to each other. We could say that each should be assigned a value of 0.5, for example, such as if we wanted to reduce our observation to a probabilistic framework. Still, this loses information because there are two different ways for something to be βhalf trueβ and weβve lost in which way it is half true. As discussed in Degree of truth, it may be more helpful to see probability as the preferred paradigm for handling uncertainty (and there is no uncertainty here). Said yet another way, probability is a function of our current state of knowledge.

In our example, we interpet half true to mean true βhalf the timeβ i.e. at only tβ (timestamp 0) rather than at {tβ,tβ}. Letβs call \(t_1 = Ξ·\) and \(t_0\) the only natural transformation 1 β Ξ© that sends \(*\) to the section \(\{0\}\) of \(\Omega(\{0,1\})\). Then we can see `true`

as the sheaf morphism that sends \(*\) to the section \(\{0,1\}\) of \(\Omega(\{0,1\})\). The power object Ξ©:

### β Topological predicate#

See Exercise 7.64.

### βοΈ Exercise 7.64#

Give an example of a space π, a sheaf \(π β \textbf{Shv(π)}\), and two predicates \(p, q : π β Ξ©\) for which \(p(π ) β’_{π :π} q(π )\) holds. You do not have to be formal.

See Exercise 7.64.

### Logical symbols in power object#

From Heyting algebra:

Heyting algebras serve as the algebraic models of propositional intuitionistic logic in the same way Boolean algebras model propositional classical logic. The internal logic of an elementary topos is based on the Heyting algebra of subobjects of the terminal object 1 ordered by inclusion, equivalently the morphisms from 1 to the subobject classifier Ξ©.

The open sets of any topological space form a complete Heyting algebra. Complete Heyting algebras thus become a central object of study in pointless topology.

The open sets of any topological space form a complete Heyting algebra because the empty/full set provide a meet/join for all finite subsets. The pointless topology article discusses the lattices of open sets denoted Ξ©(X) and Ξ©(Y).

Also, from Heyting algebra Β§ Examples:

The global elements of the subobject classifier Ξ© of an elementary topos form a Heyting algebra; it is the Heyting algebra of truth values of the intuitionistic higher-order logic induced by the topos. More generally, the set of subobjects of any object

Xin a topos forms a Heyting algebra.

## 7.4.4 Quantification#

Quantification comes in two flavors: universal and existential, or βfor allβ and βthere exists.β Each takes in a predicate of π +1 variables and returns a predicate of π variables.

### π΄ Uniqueness quantification#

See also Quantifier (logic). A third important kind of quantification is Uniqueness quantification, but this is defined in terms of the other two quantifiers. See Chapter 28 Definite descriptions β£ forall x: Calgary for Russellβs analysis of what it means for something to be unique. See Glossary of mathematical jargon Β§ Proof terminology for the related jargon, which again points to Uniqueness quantification.

In the context of equivalence classes we think in terms of Essentially unique instead. That is, sometimes we donβt care about the differences between all the objects (in an equivalence class).

### β Example 7.65#

Suppose we have two sheaves \(π,π β \textbf{Shv}(π, \textbf{Op})\) and a predicate \(π: πΓπ β \Omega\). Letβs say \(π\) represents whatβs considered newsworthy and \(π\) is again the sheaf of people. So for a subset of time \(π\), a section \(π‘ β π(π)\) is something thatβs considered newsworthy throughout the whole of \(π\), and a section \(π β π(π)\) is a person that lasts throughout the whole of \(π\). Letβs imagine the predicate \(π\) as βπ is worried about π‘.β Now recall from Section 7.4.3 that a predicate \(π\) does not simply return true or false; given a person \(π \) and a news-item \(π‘\), it returns a truth value corresponding to the subset of times on which \(π(π ,π‘)\) is true.

The choice of \(t\) for a news item is a little unfortunate, because most people assume \(t\) stands for a time. It seems this was a result of \(T\) simply being the next letter after \(S\).

βFor all π‘ in π, β¦ is worried about π‘β is itself a predicate on just one variable, \(π\), which we denote:

\[ β(π‘ : π). π(π , π‘) \]

The author says each βtakes in a predicate of \(n+1\) variables and returns a predicate of \(n\) variablesβ above. In this case, \(n\) is 1 i.e. \(p(s,t)\) is a predicate of two variables that we pass to the universal quantifier to get a predicate of one variable, namely \(β(t:T).p(s,t)\). The one variable is \(s\), because \(t\) is already bound. Taking a function of \(n+1\) variables and returning a function of \(n\) variables looks superficially similar to currying, but this is not currying because we directly return a truth value rather than another function (for a similar discussion see Currying Β§ Contrast with partial function application). It also looks superficially similar to partial application, but this is not partial application because we do not supply one of the two arguments.

In all these examples, you can think about the ββ¦β (ellipsis) as a variable. So we could have represented the predicate βFor all π‘ in π, β¦ is worried about π‘β as \(q(s)\): βFor all π‘ in π, \(s\) is worried about π‘β in a strange notational mix.

Applying this predicate to a person π returns the times when that person is worried about everything in the news. Similarly, βthere exists π‘ in π such that π is worried about π‘β is also a predicate on π, which we denote \(β(π‘: π). π(π ,π‘)\). If we apply this predicate to a person π , we get the times when person π is worried about at least one thing in the news.

### βοΈ Exercise 7.66#

In the topos \(\textbf{Set}\), where \(Ξ© = πΉ\), consider the predicate \(p: βΓβ€\to πΉ\) given by

\[\begin{split} \begin{align*} p(n, z) &= \begin{cases} \text{true} & \text{if } n \leq |z| \\ \text{false} & \text{if } n > |z| \end{cases} \end{align*} \end{split}\]

What is the set of \(n \in β\) for which the predicate \(\forall(z: β€). p(n, z)\) holds?

What is the set of \(n \in β\) for which the predicate \(\exists(z: β€). p(n, z)\) holds?

What is the set of \(z \in β€\) for which the predicate \(\forall(n: β). p(n, z)\) holds?

What is the set of \(z \in β€\) for which the predicate \(\exists(n: β). p(n, z)\) holds?

See Exercise 7.66.

### π΄ Universal quantification#

Given a predicate \(π: πΓπ β \Omega\), the universally-quantified predicate \(β(π‘: π). π(π ,π‘)\) takes a section \(π β π(π)\), for any open set \(π\), and returns a certain open set \(π β Ξ©(π)\). Namely, it returns the largest open set \(π β π\) for which \(π(π |_π, π‘) = π\) holds for all \(π‘ β π(π)\).

### βοΈ Exercise 7.67#

Suppose \(π \) is a person alive throughout the interval \(π\). Apply the above definition to the example \(π(π ,π‘)\) = βperson \(π \) is worried about news \(π‘\)β from Example 7.65. Here, \(π(π)\) is the set of items that are in the news throughout the interval \(π\).

What open subset of \(π\) is \(β(π‘: π). π(π ,π‘)\) for a person \(π \)?

Does it have the semantic meaning youβd expect, given the less formal description in Section 7.4.4?

See Exercise 7.67.

### β Set universal quantifier#

See also Example 1.117, which points to Universal quantification Β§ As adjoint, which points to this line in Presheaf (category theory):

For any morphism \(f: X β Y\) of \(\widehat{C}\), the pullback functor of subobjects \(f^β: Sub_{\widehat{C}}(Y) β Sub_{\widehat{C}}(X)\) has a right adjoint, denoted \(β_f\), and a left adjoint, \(β_f\). These are the universal and existential quantifiers.

In this context, \(\widehat{C} = \mathbf{Set}^{C^\mathrm{op}}\) which is roughly equivalent to \(\textbf{Shv}(X, \textbf{Op})\) (both functor categories).

### π΄ Existential quantification#

Given a predicate \(π: π Γ π β \Omega\), the existentially quantified predicate \(β(π‘: π). π(π ,π‘)\) takes a section \(π β π(π)\), for any open set \(π\), and returns a certain open set \(π β \Omega(π)\), namely the union \(V=\bigcup_{i}V_{i}\) of all the open sets \(π_π\) for which there exists some \(π‘_π β π(π_π)\) satisfying \(π(π |_{π_i}, π‘_π) = π_π\). If the result is \(π\) itself, you might be tempted to think βah, so there exists some \(π‘ β π(π)\) satisfying \(π(π‘)\),β but that is not necessarily so. There is just a cover of \(π = \bigcup π_π\) and local sections \(π‘_π β π(π_π)\), each satisfying \(π\), as explained above. Thus the existential quantifier is doing a lot of work βunder the hood,β taking coverings into account without displaying that fact in the notation.

Itβs not clear what the author means by \(p(t)\) in this context, because \(p\) was already defined as a function of two variables. One possible interpretation is that the author meant that a reader might be tempted to think that there is some \(π‘ β π(π)\) satisfying \(p(s|_V,t) = U\).

### βοΈ Exercise 7.68#

Apply the above definition to the βperson \(π \) is worried about news \(π‘\)β predicate from Example 7.65.

What open set is \(β(π‘: π). π(π ,π‘)\) for a person \(π \)?

Does it have the semantic meaning youβd expect?

See Exercise 7.68.

## 7.4.5 Modalities#

Back in Example 1.123 we discussed modal operators - also known as modalities - saying they are closure operators on preorders which arise in logic. The preorders we were referring to are the ones discussed in Eq. (7.63): for any object \(π β π\) there is the poset \((|\Omega^π|, β€_π)\) of predicates on \(π\), where \(|\Omega^π| = π(π,\Omega)\) is just the set of morphisms \(π β \Omega\) in the category \(π\).

### π΄ Topological modality#

See Seven Sketches Β§ Definition 7.69:

A modality in \(\textbf{Shv}(π)\) is a sheaf morphism \(π: \Omega β \Omega\) satisfying three properties for all \(π β π\) and \(π,π β \Omega(π)\):

β (a) Β \(π β€ π(π)\)

β (b) Β \((π β¨ π)(π) β€ π(π)\)

β (c) Β \(π(π β§ π) = π(π) β§ π(π)\)

It looks like \(j\) is inflationary based on `(a)`

. But then applying it again in `(b)`

results in something smaller, i.e. it appears that \(j\) is deflationary. A review of Definition 1.120 in Section 1.4 seems to indicate the author meant \((jβ¨j)(p) β
j(p)\) for `(b)`

. The purpose of Exercise 7.70 seems to be to show that these are equivalent requirements.

See also Proposition 1.111 in Section 1.4; part `(c)`

may indicate that a modality is also a right adjoint because it preserves meets.

### βοΈ Modalities are closures#

Suppose \(π: \Omega β \Omega\) is a morphism of sheaves on \(π\), such that \(π β€ π(π)\) holds for all \(π β π\) and \(π β \Omega(π)\). Show that for all \(π β \Omega(π)\) we have \(π(π(π)) β€ π(π)\) iff \(π(π(π)) = π(π)\).

See Exercise 7.70.

### π£ Types of modalities#

In Example 1.123 we informally said that for any proposition \(π\), e.g. βBob is in San Diego,β there is a modal operator βassuming \(π\), β¦β Now we are in a position to make that formal.

Proposition 7.71 gives three kinds of modalities:

Fix a proposition \(π β |Ξ©|\). Then:

β (a) the sheaf morphism \(\Omega β \Omega\) given by sending \(π\) to \(π β π\) is a modality.

β (b) the sheaf morphism \(\Omega β \Omega\) given by sending \(π\) to \(π β¨ π\) is a modality.

β (c) the sheaf morphism \(\Omega β \Omega\) given by sending \(π\) to \((π β π) β π\) is a modality.We cannot prove Proposition 7.71 here, but we give references in Section 7.6.

The author means to imply the βAssuming Bob is in San Diego β¦β modal operator is of type `(a)`

in the above. We often use the word βassumingβ with the β symbol, especially in TFL and FOL saying that e.g. A β B means that B holds assuming that A holds. In this case, β is defined as in the start of 7.4.2 but the meaning intends to generalize the concept from TFL and FOL.

### βοΈ Modality for βassumingβ#

Let \(π\) be the sheaf of people as in Section 7.4.3, and let \(π: \Omega β \Omega\) be βassuming Bob is in San Diego β¦β

Name any predicate \(π: π β \Omega\), such as βlikes the weather.β

Choose a time interval \(π\). For an arbitrary person \(π β π(π)\), what sort of thing is \(π(π )\), and what does it mean?

What sort of thing is \(π(π(π ))\) and what does it mean?

Is it true that \(π(π ) β€ π(π(π ))\)? Explain briefly.

Is it true that \(π(π(π(π ))) = π(π(π ))\)? Explain briefly.

Choose another predicate \(π: π β \Omega\). Is it true that \(π(π β§ π) = π(π) β§ π(π)\)? Explain briefly.

See Exercise 7.72.

## 7.4.6 Type theories and semantics#

We have been talking about the logic of a topos in terms of open sets, but this is actually a conflation of two ideas that are really better left unconflated. The first is logic, or formal language, and the second is semantics, or meaning. The formal language looks like this:

\[ β(π‘ : π). β(π : π). π (π ) = π‘ \hspace{4em} (7.73) \]and semantic statements are like βthe sheaf morphism π : π β π is an epimorphism.β In the former, logical world, all statements are linguistic expressions formed according to strict rules and all proofs are deductions that also follow strict rules. In the latter, semantic world, statements and proofs are about the sheaves themselves, as mathematical objects.

To

provide semanticsfor a logical system means to provide a compiler that converts each logical statement in the formal language into a mathematical statement about particular sheaves and their relationships. A computer can carry out logical deductions without knowing what any of them βmeanβ about sheaves. We say that semantics issoundif every formal proof is converted into a true fact about the relevant sheaves.Every topos can be assigned a formal language, often called its

internal language, in which to carry out constructions and formal proofs. This language has a sound semanticsβa sort of logic-to-sheaf compilerβwhich goes under the namecategorical semanticsorKripke-Joyal semantics. We gave the basic ideas in Section 7.4; we give references to the literature in Section 7.6.

See also Kripke semantics Β§ KripkeβJoyal semantics.

### β Example 7.74#

In every topos \(π\), and for every \(π: π β π\) in \(π\), the morphism \(π\) is an epimorphism if and only if Eq. (7.73) holds. For example, consider the case of database instances on a schema \(π\), say with 100 tables (one of which might be denoted \(π β Ob(π)\)) and 500 foreign key columns (one of which might be denoted \(π : π β π'\) in \(π\)); see Eq. (3.2).

If \(π\) and \(π\) are two instances and \(π\) is a natural transformation between them, then we can ask the question of whether or not Eq. (7.73) holds. This simple formula is compiled by the Kripke-Joyal semantics into asking:

Is it true that for every table \(π β Ob(C)\) and every row \(π β π(π)\) there exists a row \(π‘ β π(π)\) such that \(π(π ) = π‘\)?

This last statement does not seem to match Eq. (7.73). It should likely read:

Is it true that for every table \(π β Ob(C)\) and every row \(t β T(π)\) there exists a row \(s β S(π)\) such that \(π(π ) = π‘\)?

Without this change, the sentence seems to only be stating that \(f\) is total (is defined for all inputs).

This is exactly what it means for \(π\) to be surjective. Maybe this is not too impressive, but whether one is talking about databases or topological spaces, or complex ideas from algebraic geometry, Eq. (7.73) always compiles into the question of surjectivity. For topological spaces it would say something like:

Is it true that for every open set \(π β π\) and every section \(π β π(π)\) of the bundle \(π\), there exists an open cover \(\{π_π\}_{πβπΌ}\) of \(π\) and a section \(π‘_π β π(π_π)\) of the bundle \(π\) for each \(π β πΌ\), such that \(π(π‘_π) = π |_{π_i}\) is the restriction of \(π \) to \(π_π\)?