Editing User:Michiexile/MATH198/Lecture 10 (section)

===Exercises===

No homework at this point. However, if you want something to think about, a few questions and exercises:

# Prove the relations showing that <math>\leq_1</math> is indeed a partial order on <math>[U\to\Omega]</math>.
# Prove the universal quantifier theorem.
# The ''extension'' of a formula <math>\phi</math> over a list of variables <math>x</math> is the sub-object of the product of domains <math>A_1\times\dots\times A_n</math> for the variables <math>x_1,\dots,x_n=x</math> classified by the interpretation of <math>\phi</math> as a morphism <math>A_1\times\dots\times A_n\to\Omega</math>. A formula is ''true'' if it classifies the entire product. A ''sequent'', written <math>\Gamma:\phi</math> is the statement that using the set of formulae <math>\Gamma</math> we may prove <math>\phi</math>, or in other words that the intersection of the extensions of the formulae in <math>\Gamma</math> is contained in the extension of <math>\phi</math>. If a sequent <math>\Gamma:\phi</math> is true, we say that <math>\Gamma</math> ''entails'' <math>\phi</math>. (some of the questions below are almost embarrassingly immediate from the definitions given above. I include them anyway, so that a ''catalogue'' of sorts of topoidal logic inferences is included here)
## Prove the following entailments:
### Trivial sequent: <math>\phi:\phi</math>
### True: <math>:true</math> (note that true classifies the entire object)
### False: <math>false:\phi</math> (note that false classifies the global minimum in thepreorder of subobjects)
## Prove the following inference rules:
### Implication: <math>\Gamma,\phi:\psi</math> is equivalent to <math>\Gamma:\phi\Rightarrow\psi</math>.
### Thinning: <math>\Gamma:\phi</math> implies <math>\Gamma,\psi:\phi</math>
### Cut: <math>\Gamma,\psi:\phi</math> and <math>\Gamma:\psi</math> imply <math>\Gamma:\phi</math> if every variable free in <math>\psi</math> is free in <math>\Gamma</math> or in <math>\phi</math>.
### Negation: <math>\Gamma, \phi: false</math> is equivalent (implications both ways) to <math>\Gamma: \neg\phi</math>.
### Conjunction: <math>\Gamma:\phi</math> and <math>\Gamma:\psi</math> together are equivalent to <math>\Gamma:\phi\wedge\psi</math>.
### Disjunction: <math>\Gamma,\phi:\theta</math> and <math>\Gamma,\psi:\theta</math> together imply <math>\Gamma, \phi\vee\psi: \theta</math>.
### Universal: <math>\Gamma:\phi</math> is equivalent to <math>\Gamma:\forall x.\phi</math> if <math>x</math> is not free in <math>\Gamma</math>.
### Existential: <math>\Gamma,\phi: \psi</math> is equivalent to <math>\Gamma,\exists x.\phi:\psi</math> if <math>x</math> is not free in <math>\Gamma</math> or <math>\psi</math>.
### Equality: <math>:q=q</math>.
### Biconditional: <math>(v\Rightarrow w)\wedge(w\Rightarrow v):v=w</math>. We usually write <math>v\Leftrightarrow w</math> for <math>v=w</math> if <math>v,w:A\to\Omega</math>.
### Product: <math>p_1u = p_1u', p_2u = p_2u' : u = u'</math> for <math>u,u'\in A\times B</math>.
### Product revisited: <math>:(p_1(s\times s')=s)\wedge(p_2(s\times s')=s')</math>.
### Extensionality: <math>\forall x\in A. f(x) = g(x) : f = g</math> for <math>f,g\in[A\to B]</math>.
### Comprehension: <math>(\lambda x\in A. s)x = s</math> for <math>x\in A</math>.
## Prove the following results from the above entailments and inferences -- or directly from the topoidal logic mindset:
### <math>:\neg(\phi\wedge\neg\phi)</math>.
### <math>:\phi\Rightarrow\neg\neg\phi</math>.
### <math>:\neg(\phi\vee\psi)\Rightarrow(\neg\phi\wedge\neg\psi)</math>.
### <math>:(\neg\phi\wedge\neg\psi)\Rightarrow\neg(\phi\wedge\psi)</math>.
### <math>:(\neg\phi\vee\neg\psi)\Rightarrow\neg(\phi\vee\psi)</math>.
### <math>\phi\wedge(\theta\vee\psi)</math> is equivalent to <math>(\phi\wedge\theta)\vee(\phi\wedge\psi)</math>.
### <math>\forall x.\neg\phi</math> is equivalent to <math>\neg\exists x.\phi</math>.
### <math>\exists x\phi\Rightarrow\neg\forall x.\neg\phi</math>.
### <math>\exists x\neg\phi\Rightarrow\neg\forall x.\phi</math>.
### <math>\forall x\phi\Rightarrow\neg\exists x.\neg\phi</math>.
### <math>\phi:\psi</math> implies <math>\neg\psi:\neg\phi</math>.
### <math>\phi:\psi\Rightarrow\phi</math>.
### <math>\phi\Rightarrow\not\phi:\not\phi</math>.
### <math>\not\phi\vee\psi:\phi\Rightarrow\psi</math> (but not the converse!).
### <math>\neg\neg\neg\phi</math> is equivalent to <math>\neg\phi</math>.
### <math>(\phi\wedge\psi)\Rightarrow\theta</math> is equivalent to <math>\phi\Rightarrow(\psi\Rightarrow\theta)</math> (currying!).
## Using the Boolean negation rule: <math>\Gamma,\neg\phi:false</math> is equivalent to <math>\Gamma:\phi</math>, prove the following additional results:
### <math>\neg\neg\phi:\phi</math>.
### <math>:\phi\vee\neg\phi</math>.
## Show that either of the three rules above, together with the original negation rule, implies the Boolean negation rule.
### The converses of the three existential/universal/negation implications above.
## The restrictions introduced for the cut rule above block the deduction of an entailment <math>:\forall x.\phi\Rightarrow\exists x.\phi</math>. The issue at hand is that <math>A</math> might not actually have members; so choosing one is not a sound move. Show that this entailment can be deduced from the premise <math>\exists x\in A. x=x</math>.
## Show that if we extend our ruleset by the quantifier negation rule <math>\forall x\Leftrightarrow \neg\exists x.\neg</math>, then we can derive the entailment <math>:\forall w: w=t \vee w = false</math>. From this derive <math>:\phi\vee\neg\phi</math> and hence conclude that this extension gets us Boolean logic again.
# A ''topology'' on a topos <math>E</math> is an arrow <math>j:\Omega\to\Omega</math> such that <math>j\circ true=true</math>, <math>j\circ j=j<math> and <math>j\circ\wedge = \wedge\circ j\times j</math>. For a subobject <math>S\subseteq A</math> with characteristic arrow <math>\chi_S:A\to\Omega</math>, we define its <math>j</math>-closure as the subobject <math>\bar S\subseteq A</math> classified by <math>j\circ\chi_S</math>.
## Prove:
### <math>S\subseteq\bar S</math>.
### <math>\bar S = \bar{\bar S}</math>.
### <math>\bar{S\cap T} = \bar S\cap\bar T</math>.
### <math>S\subseteq T</math> implies <math>\bar S\subseteq\bar T</math>.
### <math>\bar{f^{-1}(S)} = f^{-1}(\bar S)</math>.
## We define <math>S</math> to be <math>j</math>-closed if <math>S=\bar S</math>. It is <math>j</math>-dense if <math>\bar S=A</math>. These terms are chosen due to correspondences to classical pointset topology for the topos of sheaves over some space. For a logical standpoint, it is more helpful to look at <math>j</math> as a modality operator: "''it is <math>j</math>-locally true that''" Given any <math>u:1\to\Omega</math>, prove that the following are topologies:
### <math>(u\to -): \Omega\to\Omega</math> (the ''open topology'', where such a <math>u</math> in a sheaf topos ends up corresponding to an open subset of the underlying space, and the formulae picked out are true on at least all of that subset).
### <math>u\vee -): \Omega\to\Omega</math> (the closed topology, where a formula is true if its disjunction with <math>u</math> is true -- corresponding to formulae holding over at least the closed set complementing the subset picked out)
### <math>\neg\neg: \Omega\to\Omega</math>. This may, depending on the topos, end up being interpreted as ''true so far as global elements are concerned'', or ''not false on any open set'', or other interpretations.
### <math>1_\Omega</math>.
## For a topos <math>E</math> with a topology <math>j</math>, we define an object <math>A</math> to be a ''sheaf'' iff for every <math>X</math> and every <math>j</math>-dense subobject <math>S\subseteq X</math> and every <math>f:S\to A</math> there is a unique <math>g:X\to A</math> with <math>f=g\circ s</math>. In other words, <math>A</math> is an object that cannot see the difference between <math>j</math>-dense subobjects and objects. We write <math>E_j</math> for the full subcategory of <math>j</math>-sheaves. 
### Prove that any object is a sheaf for <math>1_\Omega</math>.
### Prove that a subobject is dense for <math>\neg\neg</math> iff its negation is empty. Show that <math>true+false:1+1\to\Omega</math> is dense for this topology. Conclude that <math>1+1</math> is dense in <math>\Omega_{\neg\neg}</math> and thus that <math>E_{\neg\neg}</math> is Boolean.