|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008graphs.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008graphs.tex && latex 2008graphs.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008graphs.tex && pdflatex 2008graphs.tex"))
% (eev "cd ~/LATEX/ && Scp 2008graphs.{dvi,pdf} [email protected]:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008graphs.dvi")
% (find-pspage "~/LATEX/2008graphs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o 2008graphs.ps 2008graphs.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o 2008graphs.ps 2008graphs.dvi")
% (find-pspage "~/LATEX/2008graphs.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008graphs.pdf" (ee-twupfile "LATEX/2008graphs.pdf") 'over)
% (ee-cp "~/LATEX/2008graphs.pdf" (ee-twusfile "LATEX/2008graphs.pdf") 'over)
% (find-angg "LATEX/2008sheaves.tex")
% http://angg.twu.net/LATEX/2008graphs.pdf
% (find-dn4tex-links "2008graphs")
% (defun d () (interactive) (find-dvipage "~/LATEX/2008graphs.dvi"))
% (find-dvipage "~/LATEX/2008graphs.dvi")
% «.nd-to-sc» (to "nd-to-sc")
% «.heyting-algebras» (to "heyting-algebras")
% «.calculating-VimpW» (to "calculating-VimpW")
% «.curry-howard-1» (to "curry-howard-1")
% «.dags-as-heyting-algebras» (to "dags-as-heyting-algebras")
% «.preamble-dgs-and-topologies» (to "preamble-dgs-and-topologies")
% «.preamble-dg-to-topology» (to "preamble-dg-to-topology")
% «.preamble-truth-values» (to "preamble-truth-values")
% «.topological-spaces» (to "topological-spaces")
% «.preorders-and-posets» (to "preorders-and-posets")
% «.minimal-dag» (to "minimal-dag")
% «.presheaves» (to "presheaves")
% «.subtopology-of-R» (to "subtopology-of-R")
% «.coherent-families» (to "coherent-families")
% «.saturation» (to "saturation")
% «.a-presheaf-on-a-dag» (to "a-presheaf-on-a-dag")
% «.presheaf-on-a-dag-germs» (to "presheaf-on-a-dag-germs")
% «.denses-and-stables» (to "denses-and-stables")
% «.subst-for-iff» (to "subst-for-iff")
% «.LT-modalities» (to "LT-modalities")
% «.LT-modalities-and» (to "LT-modalities-and")
% «.LT-modalities-or» (to "LT-modalities-or")
% «.LT-modalities-imp» (to "LT-modalities-imp")
% «.tops-for-or-and-imp» (to "tops-for-or-and-imp")
% «.more-about-not-not» (to "more-about-not-not")
% «.modalities-alt-axioms» (to "modalities-alt-axioms")
% «.LT-modalities-quants» (to "LT-modalities-quants")
% «.embedding» (to "embedding")
% «.sat-cov-fibration» (to "sat-cov-fibration")
% «.geometric-morphisms» (to "geometric-morphisms")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008graphs.dnt
%*
% (eedn4-51-bounded)
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Natural Deduction and Sequent Calculus} {2}
\tocline {Heyting Algebras} {3}
\tocline {Some DAGs are Heyting Algebras} {4}
\tocline {Calculating $V⊃W$} {5}
\tocline {``Mundo funcional'' e ``Mundo l\'ogico'' (Curry-Howard)} {6}
\tocline {Preamble: DGs and topologies} {7}
\tocline {Preamble: each DG induces a topology} {8}
\tocline {Preamble: truth-values} {9}
\tocline {Topological spaces} {10}
\tocline {Preorders and partial orders} {11}
\tocline {The minimal DAG for a topology} {12}
\tocline {Presheaves} {13}
\tocline {A subtopology of $\R $} {14}
\tocline {Coherent families} {15}
\tocline {Saturation and bisaturation} {16}
\tocline {A (bad) presheaf on a DAG} {17}
\tocline {A presheaf on a DAG: its space of germs} {18}
\tocline {Dense and stable truth-values} {19}
\tocline {Substitution principles for `$\Leftrightarrow $'} {20}
\tocline {Lawvere-Tierney Modalities} {21}
\tocline {LT-modalities and `and'} {22}
\tocline {LT-modalities and `or'} {23}
\tocline {LT-modalities and implication} {24}
\tocline {The topologies for `or' and `implies'} {25}
\tocline {More about double negation} {26}
\tocline {Modalities: alternative axioms} {27}
\tocline {LT-modalities and the quantifiers} {28}
\tocline {The fibration of saturated covers} {29}
\tocline {Embedding} {30}
\tocline {Geometric morphisms} {31}
% ----------
% Definitions
\def\bbV{\mathbb{V}}
\def\Nondecr{�{Nondecr}}
\def\emp{\emptyset}
\def\DG{�{DG}}
\def\Vee{\dagVee}
\def\O{\Opens}
\def\OX{\O(X)}
\def\OR{{\Opens(\R)}}
\def\D{\mathbb{D}}
\def\V{\mathbb{V}}
\def\Cinfty{\mathcal{C}^\infty}
\def\bbV{{\mathbb{V}}}
\def\calU{{\mathcal{U}}}
\def\calV{{\mathcal{V}}}
\def\calW{{\mathcal{W}}}
\def\DG {�{DG}}
\def\DAG{�{DAG}}
\def\Top{�{Top}}
\def\TopCAI{�{TopCAI}}
\def\Iinfty{{\bigcap_\infty}}
\def\cai{�{cai}}
\def\dquo#1{\text{``$#1$''}}
%:****^{**}*
%:***^**
%:*<=>*\Bij *
%:*&*\&*
%:*\&*\&*
\newpage
% --------------------
% «nd-to-sc» (to ".nd-to-sc")
% (s "Natural Deduction and Sequent Calculus" "nd-to-sc")
\myslide {Natural Deduction and Sequent Calculus} {nd-to-sc}
%: [P&Q]^1 P&Q|-P&Q
%: ------- ---------
%: [P&Q]^1 Q Q⊃R P&Q|-P&Q P&Q|-Q Q⊃R|-Q⊃R
%: ------- ---------- --------- ----------------
%: P R P&Q|-P Q⊃R,P&Q|-R
%: -------------- -----------------------
%: P&R Q⊃R,P&Q|-P&R
%: ------1 ------------
%: P&Q⊃P&R Q⊃R|-P&Q⊃P&R
%:
%: ^nd-to-sc-1 ^nd-to-sc-2
%:
$$\ded{nd-to-sc-1}$$
$$\ded{nd-to-sc-2}$$
\newpage
% --------------------
% «heyting-algebras» (to ".heyting-algebras")
% (s "Heyting Algebras" "heyting-algebras")
\myslide {Heyting Algebras} {heyting-algebras}
A {\sl Heyting Algebra} is a 7-uple
$(�, �, �, ∧, ∨, ⊃, \vdash)$, where:
\msk
$\begin{array}{rcl}
�, � &�& �, \\
∧, ∨, ⊃ &:& �×� \to �,\\
\vdash &\subseteq& � \\
\end{array}
$
\msk
and the relation $\vdash$ respects the following ``derivation rules'':
%D diagram O(X)-structure
%D 2Dx 100 +25 +25 +15 +20 +25
%D 2D 100 --| p0 |- t0 a0 <==== a1
%D 2D / - \ - - -
%D 2D / | \ | | <--> |
%D 2D v v v v v v
%D 2D +25 p1 <--| p2 |--> p3 t1 a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2 i0
%D 2D - - - -
%D 2D \ | / |
%D 2D \ v / v
%D 2D +25 --> c3 <-- i1
%D 2D
%D (( p0 .tex= P
%D p1 .tex= Q p2 .tex= Q∧R p3 .tex= R
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= P∨Q c2 .tex= Q
%D c3 .tex= R
%D @ 0 @ 1 |-> @ 1 @ 2 <-|
%D @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= �
%D @ 0 @ 1 |->
%D ))
%D (( i0 .tex= � i1 .tex= P
%D @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P∧Q a1 .tex= P
%D a2 .tex= R a3 .tex= Q⊃R
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
\bsk
$\diag{O(X)-structure}$
\bsk
%: P|-Q Q|-R
%: ---------- ----
%: P|-R P|-P
%:
%: ^O(x)-c ^O(x)-id
%:
%: P|-Q P|-R P∧Q|-R
%: ---------- ------ ------ ---- ------(\vbij)
%: P|-Q∧R Q∧R|-Q Q∧R|-R P|-� P|-Q⊃R
%:
%: ^O(X)-1 ^O(X)-2 ^O(X)-3 ^O(X)-4 ^O(X)-5
%:
%: P|-R Q|-R
%: ---------- ------ ------ ----
%: P∨Q|-R P|-P∨Q Q|-P∨Q �|-P
%:
%: ^O(X)-6 ^O(X)-7 ^O(X)-8 ^O(X)-9
%:
$\begin{array}{ccccc}
\ded{O(x)-c} & \ded{O(x)-id} \\ \\
\ded{O(X)-1} & \ded{O(X)-2} & \ded{O(X)-3} & \ded{O(X)-4} & \ded{O(X)-5} \\ \\
\ded{O(X)-6} & \ded{O(X)-7} & \ded{O(X)-8} & \ded{O(X)-9} \\
\end{array}
$
\bsk
Here are three Heyting Algebras:
%D diagram three-HAs
%D 2Dx 100 +40 +20 +20 +30 +20 +20
%D 2D 100 1 111 X
%D 2D
%D 2D +20 110 101 011 U V
%D 2D
%D 2D +20 100 010 001 W
%D 2D
%D 2D +20 0 000 \emp
%D 2D
%D (( 0 1 ->
%D ))
%D (( 000 001 -> 000 010 -> 000 100 ->
%D 001 011 -> 001 101 ->
%D 010 011 -> 010 110 ->
%D 100 101 -> 100 110 ->
%D 011 111 -> 101 111 -> 110 111 ->
%D ))
%D (( X .tex= \dagVee111
%D U .tex= \dagVee101
%D V .tex= \dagVee011
%D W .tex= \dagVee001
%D \emp .tex= \dagVee000
%D \emp W -> W U -> W V -> U X -> V X ->
%D ))
%D enddiagram
%D
$$\diag{three-HAs}$$
Note: consider the partial order induced by the DAGs above -
i.e., the reflexive/transitive closure of the DAGs.
\newpage
% --------------------
% «dags-as-heyting-algebras» (to ".dags-as-heyting-algebras")
% (s "Some DAGs are Heyting Algebras" "dags-as-heyting-algebras")
\myslide {Some DAGs are Heyting Algebras} {dags-as-heyting-algebras}
{\bf Theorem:} if
$(�, �, �, ∧, ∨, ⊃, \vdash)$ and
$(�, �', �', ∧', ∨', ⊃', \vdash)$ are Heyting Algebras, then
we have
$� \bij �'$,
$� \bij �$,
and for any $P, Q � �$,
$P∧Q \bij P∧'Q$,
$P∨Q \bij P∨'Q$,
$P⊃Q \bij P⊃'Q$.
\msk
{\bf Proof} (half of it):
%: ----- -----
%: �|-�' �|-�'
%:
%: ^dagha-1 ^dagha-2
%:
%: ------ ------ ------- -------
%: P&Q|-P P&Q|-Q P|-P∨'Q Q|-P∨'Q
%: --------------- -----------------
%: P&Q|-P&'Q P∨Q|-P∨'Q
%:
%: ^dagha-3 ^dagha-3
%:
%: --------
%: P⊃Q|-P⊃Q
%: ================= ----------
%: (P⊃Q)&'P|-(P⊃Q)&P (P⊃Q)&P|-Q
%: ------------------------------
%: (P⊃Q)&'P|-Q
%: ---------
%: P⊃Q|-P⊃'Q
%:
%: ^dagha-4
%:
$$\ded{dagha-1} \qquad \ded{dagha-2}$$
$$\ded{dagha-3} \qquad \ded{dagha-3}$$
$$\ded{dagha-4}$$
\msk
{\bf Theorem:} if
$(�, �, �, ∧, ∨, ⊃, \vdash)$ and
$(�, �', �', ∧', ∨', ⊃', \vdash)$ are Heyting Algebras and
$(�, \vdash)$ is a DAG, then
$�=�'$, $�=�'$, $∧=∧'$, $∨=∨'$, $⊃=⊃'$.
\ssk
So, if a DAG $(�, \vdash)$ is Heyting Algebra,
then it is a Heyting Algebra in a unique way:
$�, �, ∧, ∨, ⊃$ are well-defined.
% being a Heyting Algebra is a ``property'' of some DAGs,
% not ``extra structure''.
\bsk
{\bf Amazing fact:}
For any topological space $(X, \Opens(X))$,
the DAG $(\Opens(X), \subseteq)$ is a Heyting Algebra.
\newpage
% --------------------
% «calculating-VimpW» (to ".calculating-VimpW")
% (s "Calculating $Vprotect⊃W$" "calculating-VimpW")
\myslide {Calculating $V\protect⊃W$} {calculating-VimpW}
What is $V⊃W$?
Idea: look at all $U$s such that $U\&V \vdash W$.
\bsk
%D diagram calculating-VimpW
%D 2Dx 100 +30
%D 2D 100 \arga∧V <--| \arga
%D 2D | |
%D 2D | <-> |
%D 2D v v
%D 2D +30 W |------> V⊃W
%D 2D
%D (( \arga∧V \arga W V⊃W
%D @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
{
\def\foo#1{\def\arga{#1}\diag{calculating-VimpW}}
$\foo{?}$
\bsk
$\foo{\emp} \quad
\foo{W} \quad
\foo{U}
$
}
\bsk
In $\Opens(\bbV)$, this works for these open sets: $\dagKite01011$.
Define $V⊃W$ as the greatest of them.
More formally:
$V⊃W := \sup \sst{U}{U\&V \vdash W}$
$V⊃W := \bigcup\; \sst{U}{U\&V \vdash W}$
$V⊃W := \bigcup\; \sst{U}{U \cap V \subseteq W}$
$V⊃W := \bigcup\; \sst{A^\bol}{A^\bol \cap V \subseteq W}$
$V⊃W := \bigcup\; \sst{A^\bol}{A^\bol \subseteq W \cup (X \bsl V)}$
$V⊃W := (W \cup (X \bsl V))^\bol$
\newpage
% --------------------
% «curry-howard-1» (to ".curry-howard-1")
% (s "``Mundo funcional'' e ``Mundo lógico'' (Curry-Howard)" "curry-howard-1")
\myslide {``Mundo funcional'' e ``Mundo lógico'' (Curry-Howard)} {curry-howard-1}
Compare a prova abaixo à esquerda, em Dedução Natural, de que $Q⊃R$
implica $P∧Q⊃P∧R$, com a construção do termo
$�d�A{×}B.\ang{d,f('d)}:(A{×}B \to A{×}C)$ em $�$-cálculo simplesmente
tipado:
%:*&*\&*
%:*&*∧*
%:*×*{×}*
%:*<*\langle *
%:*>*\rangle *
%:
%: f�B->C Q->R
%: =============(?) ============(?)
%: f^\#�A×B->A×C (P&Q)->(P&R)
%:
%: ^4-functional? ^4-logical?
%:
%: [P&Q]^1 [d�A×B]^1
%: ------- ---------
%: [P&Q]^1 Q Q⊃R [d�A×B]^1 'd�B f�B->C
%: ------- ---------- --------- ----------------
%: P R d�A f('d)�C
%: -------------- -----------------------
%: P&R <d,f('d)>�A×C
%: ----------1 ------------------------------1
%: (P&Q⊃P&R) �d�A×B.<d,f('d)>:A×B->A×C
%:
%: ^4-logical ^4-functional
%:
$$\ded{4-logical} \qquad \ded{4-functional}$$
As duas têm exatamente a mesma estrutura. Isto é um exemplo do
Isomorfismo de Curry-Howard em funcionamento; ele diz que há uma
bijeção natural entre derivações em Dedução Natural e termos de
$�$-cálculo simplesmente tipado. Repare que na árvore um $�$-cálculo
os termos sempre crescem à medida que descemos; se usamos uma nova
notação --- ``downcased types'' --- podemos não só manter os termos
pequenos, como suprimir os tipos --- os tipos podem ser reconstruídos
``convertendo para maiúsculas'' os termos. Note que os ``conectivos''
também têm que ser convertidos: `,' convertido para maiúscula vira
`$×$', e `$\mto$' convertido para maiúscula vira `$\to$'.
%: [a,b]^1
%: ------- a,b := d
%: [a,b]^1 b b|->c b|->c := f
%: ------- -----------
%: a c a := (a,b)
%: ------------- b := '(a,b)
%: a,c c := (b|->c)(b)
%: --------- a,c := <a,c>
%: a,b|->a,c a,b|->a,c := �(a,b).(a,c)
%:
%: ^4-DNC
%:
$$\cded{4-DNC} \qquad
\begin{array}{rcl}
a,b &:=& d \\
b \mto c &:=& f \\
\\
b &:=& '(a,b) \\
c &:=& (b \mto c)(b) \\
a,c &:=& \ang{a,c} \\
a,b \mto a,c &:=& �(a,b).(a,c) \\
\end{array}
$$
Agrora cada barra da árvore define um novo termo a partir de termos
anteriores; isto gera o dicionário à direita... e a semântica de cada
barra passa a ser: ``se eu sei o significado dos termos acima da
barra, eu sei o significado do termo abaixo da barra'', ou: ``se eu
sei `$a$' e sei `$c$' eu sei `$a,c$'\,'', ``se eu sei `$b$' e `$b \mto
c$' eu sei `$c$'\,'', etc.
Os ``termos'' em DNC funcionam de um modo bem diferente dos termos de
$�$-cálculo. Em DNC nós permitimos nomes longos para variáveis (por
exemplo, `$a,b$'), a distinção sintática entre variáveis e termos
não-primitivos não existe, e, aliás, sem o dicionário não é nem
possível determinar só pelos nomes de dois termos qual é ``mais
primitivo'' que o outro: por exemplo, $b \mto c$ é mais primitivo que
$c$ mas $a,b \mto a,c$ é menos primitivo que $a,c$.
\newpage
% --------------------
% «preamble-dgs-and-topologies» (to ".preamble-dgs-and-topologies")
% (s "Preamble: DGs and topologies" "preamble-dgs-and-topologies")
\myslide {Preamble: DGs and topologies} {preamble-dgs-and-topologies}
A {\sl directed graph} is a set of worlds, $W$,
and a relation $R \subseteq W×W$.
\msk
Important fact:
DGs induce topologies,
topologies induce DGs,
and in the finite case (which is what matters to us)
the correspondence $\DG \leftrightarrows \Top$ is especially
well-behaved.
\msk
This will be our archetypical DAG:
%
$$\bbV := (W, R) := (\sof{\aa,\bb,\cc}, \sof{\aa\to\cc, \bb\to\cc})$$
%
%D diagram Vee-dag
%D 2Dx 100 +15 +15
%D 2D 100 \aa \bb
%D 2D
%D 2D +20 \cc
%D 2D
%D (( \aa \cc -> \bb \cc -> ))
%D enddiagram
%D
$$\bbV \quad \equiv \diag{Vee-dag}$$
This will be the topological space induced by $\bbV$:
%
$$(\bbV, \Opens(\bbV)) :=
(\sof{\aa,\bb,\cc},
\sof{\emp,
\sof{\cc},
\sof{\aa,\cc},
\sof{\bb,\cc},
\sof{\aa,\bb,\cc}
})
$$
We will use the correspondence mainly to represent
finite topological spaces by their associated DGs (or DAGs).
\newpage
% --------------------
% «preamble-dg-to-topology» (to ".preamble-dg-to-topology")
% (s "Preamble: each DG induces a topology" "preamble-dg-to-topology")
\myslide {Preamble: each DG induces a topology} {preamble-dg-to-topology}
A function $f: W \to \sof{0,1}$ is ``{\sl non-decreasing} (on $R$)''
when all arrows in $R$ are ``non-decreasing''.
$$\bbV := (W, R) := (\sof{\aa,\bb,\cc}, \sof{\aa\to\cc, \bb\to\cc})$$
$$\bbV \quad \equiv \diag{Vee-dag}$$
$\Vee100$ decreases on the arrow $\aa\to\cc$: $f(\aa\to\cc) = 1 \to 0$.
$\Vee010$ decreases on $\bb\to\cc$.
$\Vee110$ decreases on both $\aa\to\cc$ and $\bb\to\cc$.
The non-decreasing functions $\bbV \to \sof{0,1}$ are
$\Vee000, \Vee001, \Vee011, \Vee101, \Vee111$.
A ``{\sl non-decreasing subset}'' $W' \subseteq W$ is one whose
characteristic function is non-decreasing (on $R$).
Definition:
%
$$\Nondecr(W,R) := \sst{W' \subseteq W}{\text{$W'$ is non-decreasing on $R$}}$$
For a DG $\bbD := (W,R)$ the induced topological space is:
%
$$(\bbD, \Opens(\bbD)) := (W, \Opens(\bbD)) := (W, \Nondecr(W, R))$$
For the dag $\V$ above, this is:
%
$$(\bbV, \Opens(\bbV)) :=
(\sof{\aa,\bb,\cc},
\sof{\emp,
\sof{\cc},
\sof{\aa,\cc},
\sof{\bb,\cc},
\sof{\aa,\bb,\cc}
})
$$
Fact: topologies induced by DGs are closed by arbitrary intersections
of open sets --- not just by finite intersections.
\newpage
% --------------------
% «preamble-truth-values» (to ".preamble-truth-values")
% (s "Preamble: truth-values" "preamble-truth-values")
\myslide {Preamble: truth-values} {preamble-truth-values}
Abuse of language:
We will often write subsets of $W$ (non-decreasing or not)
as if they were the corresponding functions $W \to \sof{0,1}$.
So, for example:
$\sof{\bb,\cc} \equiv \Vee011$,
$\Opens(\bbV) = \Nondecr(\bbV) \equiv \sof{\Vee000, \Vee001, \Vee011, \Vee101, \Vee111}$.
\bsk
Terminology:
A function $W \to \sof{0,1}$ is a ``{\sl modal truth-value}''.
A non-decreasing function $W \to \sof{0,1}$ is an ``{\sl
intuitionistic truth-value}''.
We will see later that the modal truth-values live in a category $\Set^W$
and that the intuitionistic truth-values live in a category $\Set^\bbD$.
\bsk
\bsk
{\bf Big fact:} we can interpret propositional logic on modal truth-values...
just operate on each world separately, e.g.: $\Vee011 \land \Vee101 = \Vee001$.
On modal truth-values the ``logic'' is boolean but not two-valued.
\msk
{\bf Bigger fact:} the intuitionistic truth-values on a DAG $\D$ form
a ``Heyting algebra'', $\O(\D)$ --- we can interpret propositional logic there,
but it will be {\sl intuitionistic} --- we can't prove $��P⊃P$ there because
that is {\sl not always true}: take $P:=\Vee001$, then $��P \equiv \Vee111$.
\msk
{\bf Mind-blowing fact:} the notion of ``taking the union of all open sets in
a given cover'' can be interpreted as a {\sl new logical operation}, obeying
some axioms: namely, $�^* = �$, $P^{**} = P^*$, $P^*∧Q^* = (P∧Q)^*$.
This ``taking the union...'' operation is a particular case of something much
more general: {\sl Lawvere-Tierney topologies}, that generalize both
{\bf sheaves} and {\bf forcing}.
\msk
We can understand \und{sheaves} through \und{logic}.
\bsk
\bsk
\fbox{
\begin{tabular}{l}
{\bf Tiny, but amazing, fact:} we can understand all these ideas \\
from the cases of the DAGs $\V \equiv \dagVee***$ and $\O(\V)^\op \equiv \dagKite*****$, \\
and then generalizing. This tiny \& amazing fact --- that in a sense \\
is trivial, and is little more than working out in full detail \\
a few chosen exercises from topos theory books --- \\
is the guiding thread for these notes. \\
\end{tabular}
}
\newpage
% --------------------
% «topological-spaces» (to ".topological-spaces")
% (s "Topological spaces" "topological-spaces")
\myslide {Topological spaces} {topological-spaces}
A topological space is a pair $(X,\O(X))$
where $\O(X) \subset \Pts(X)$ is a topology on the set $X$:
(i) $X�\O(X)$, $\emp�\O(X)$,
(ii) $\O(X)$ is closed by arbitrary unions,
(iii) $\O(X)$ is closed by finite intersections.
\msk
Sometimes an $\OX$ is closed by {\bf arbitrary intersections}...
This happens for $(\V,\O(\V))$ and for $(\R,\Pts(\R))$, but not for $(\R,\O(\R))$.
When this happens we say that $\OX$ is an {\sl Alexandroff topology},
and that $(X,\OX)$ is an {\sl Alexandroff space}.
We will refer to these things by more mnemonic names:
$\OX$ is a ``topcai'', $(X,\OX)$ is a ``topcai space''.
\msk
There is an inclusion of categories - a functor:
%
$$\TopCAI \monicto \Top$$
and we can take a topology $\OX$ and look at the set of
arbitrary intersections of its open sets, $\Iinfty\OX$ -
it turns out that $\Iinfty\OX$ is closed by arbitrary unions,
and is a topology - actually a topcai.
\msk
This operation - ``closing by arbitrary intersections'' - is a functor:
$$\begin{array}{rccc}
\cai: & \Top & \to & \TopCAI \\
& (X,\OX) & \mto & (X,\Iinfty\OX) \\
\end{array}
$$
and there is an adjunction $(\monicto) \dashv \cai$.
\msk
($\TopCAI$ is a ``coreflective subcategory'' of $\Top$ -
the inclusion funtor $(\monicto)$ has a right adjoint).
\msk
Note that its counit on $(\R,\O(\R))$ is the
continuous map $\dquo{\id}: (\R,\Pts(\R)) \to (\R,\O(\R))$:
%D diagram counit-R
%D 2Dx 100 +50 +50 +50
%D 2D 100 a0 <---| a1 b0 <---| b1
%D 2D | | | |
%D 2D | <-> | | <-> |
%D 2D v v v v
%D 2D +30 a2 |---> a3 b2 |---> b3
%D 2D
%D 2D +20 a4 <===> a5 b4 <===> b5
%D 2D
%D (( a0 .tex= (X,\OX) a1 .tex= (X,\OX)
%D a2 .tex= (Y,\O(Y)) a3 .tex= (Y,\Iinfty\O(Y))
%D a4 .tex= \Top a5 .tex= \TopCAI
%D a0 a1 <-| a0 a2 -> a1 a3 -> a2 a3 |-> .plabel= b \cai
%D a0 a3 harrownodes nil 20 nil <->
%D a4 a5 <-< sl^ a4 a5 ->> sl_ .plabel= b \cai
%D ))
%D (( b0 .tex= (\R,\Pts(\R)) b1 .tex= (\R,\Pts(\R))
%D b2 .tex= (\R,\O(\R)) b3 .tex= (\R,\Pts(\R))
%D b4 .tex= \Top b5 .tex= \TopCAI
%D b0 b1 <-|
%D b0 b2 -> .plabel= l \dquo{\id}
%D b1 b3 -> .plabel= r \id
%D b2 b3 |-> .plabel= b \cai
%D b0 b3 harrownodes nil 20 nil <->
%D b4 b5 <-< sl^ b4 b5 ->> sl_ .plabel= b \cai
%D ))
%D enddiagram
%D
$$\diag{counit-R}$$
\newpage
% --------------------
% «preorders-and-posets» (to ".preorders-and-posets")
% (s "Preorders and partial orders" "preorders-and-posets")
\myslide {Preorders and partial orders} {preorders-and-posets}
A {\sl preorder} on $W$ is a relation $(\le) \subset W×W$ that is:
(i) reflexive: $a \le a$
(ii) transitive: if $a \le b$ and $b \le c$, then $a \le c$.
A {\sl partial order} is a preorder that is also:
(iii) anti-symmetric: if $a \le b$ and $b \le a$, then $a = b$.
\msk
A directed graph $(W,R)$ induces a preorder $(W,\le) := (W,R^*)$...
Mnemonic: the `$*$' is a Kleene star: if $a R a_1 R a_2 R a_3 R b$ then
$a R^4 b$, and thus $a R^* b$; ``$R^*$'' means ``at least zero `$R$'s''.
More formally: $R^* := R^0 \cup R^1 \cup R^2 \cup R^3 \cup \ldots$,
the reflexive/transitive closure of $R$.
($R^0$ is the diagonal --- $a R^0 b$ iff $a=b$).
\msk
Each cycle in a DG $(W,R)$ becomes a set of
``equivalent elements'' in the induced preorder
Let's consider just DAGs for a while.
DAGs induce partial orders --- aciclicity leads to antisymmetry.
\msk
A DG can be converted to a DAG by identifying the elements
in each cycle:
%D diagram collapsing-cycles
%D 2Dx 100 +10 +10 +10 +40
%D 2D 100 a <===> b \{a,b\}
%D 2D \ |
%D 2D v v
%D 2D +20 c ----> d \{c,d,e\}
%D 2D ^ / |
%D 2D \ v |
%D 2D +20 e |
%D 2D | |
%D 2D v v
%D 2D +20 f \{f\}
%D 2D
%D 2D q
%D 2D +20 \DG -------> \DAG
%D (( a b -> sl^ a b <- sl_
%D a c -> c d -> d e -> e c -> e f ->
%D ))
%D (( \{a,b\} \{c,d,e\} \{f\}
%D @ 0 @ 1 -> @ 1 @ 2 ->
%D ))
%D (( \DG \DAG -> .plabel= a �q
%D enddiagram
%D
$$\diag{collapsing-cycles}$$
\msk
It turns out that the inclusions $\DG^* \monicto \DG$ and $\DAG^* \monicto \DAG$
have left adjoints: in both cases, $* \dashv (\monicto)$,
and the units of the adjunctions take a DG or DAG $(W,R)$
to its reflexive and transitive closure.
\msk
Also, the inclusion $\DAG^* \monicto \DG^*$ have a left adjoint: `$�q$'.
%D diagram DAG-DG-adjunctions
%D 2Dx 100 +15 +20 +15
%D 2D 100 \DG* <=> \DG
%D 2D <=> ->
%D 2D +25 \DAG* <=> \DAG
%D 2D
%D (( \DG* \DG >-> sl_ \DG* \DG <- sl^ .plabel= a *
%D \DAG* \DAG >-> sl_ \DAG* \DAG <- sl^ .plabel= a *
%D \DAG* \DG* >-> sl_ \DAG* \DG* <- sl^ .plabel= l �q
%D \DAG \DG >->
%D ))
%D enddiagram
%D
$$\diag{DAG-DG-adjunctions}$$
\newpage
% --------------------
% «minimal-dag» (to ".minimal-dag")
% (s "The minimal DAG for a topology" "minimal-dag")
\myslide {The minimal DAG for a topology} {minimal-dag}
Each DG $\D = (W,R)$ induces a topcai: $(W, \Nondecr(R))$ -
but several DGs induce the same topcai.
One canonical way to represent a topcai by a DG is to pick the
associated DG${}^*$ - it is the maximal DG generating that topcai.
\msk
For {\sl finite DAGs} - i.e., for finite $T_0$ topological spaces -
there is also a {\sl minimal} DAG generating that topology...
The process to obtain it is to drop all the arrows that are not
``essential''.
Here's an example:
(by the way: $\text{ess} \dashv {}^* \dashv (\monicot)$)
%
%D diagram dag-minimal
%D 2Dx 100 +15
%D 2D 100 a
%D 2D +15 b
%D 2D +15 c
%D 2D
%D (( a b -> b c ->
%D ))
%D enddiagram
%
%D diagram dag-medium
%D 2Dx 100 +15
%D 2D 100 a
%D 2D +15 b
%D 2D +15 c
%D 2D
%D (( a b -> b c ->
%D # a loop (ur,dr)
%D b loop (ul,dl)
%D c loop (ur,dr)
%D ))
%D enddiagram
%
%D diagram dag-full
%D 2Dx 100 +15
%D 2D 100 a
%D 2D +15 b
%D 2D +15 c
%D 2D
%D (( a b -> b c -> a c ->
%D a loop (ur,dr)
%D b loop (ul,dl)
%D c loop (ur,dr)
%D ))
%D enddiagram
%
%D diagram dags
%D 2Dx 100 +70
%D 2D 100 A B
%D 2D
%D 2D +60 C D
%D 2D
%D 2D +60 E F
%D 2D
%D 2D +40 \DAG \DAG*
%D 2D
%D (( A .tex= \usebox{\myboxa}
%D B .tex= \usebox{\myboxc}
%D C .tex= \usebox{\myboxb}
%D D .tex= \usebox{\myboxc}
%D E .tex= \usebox{\myboxc}
%D F .tex= \usebox{\myboxc}
%D A B <-| .plabel= a �{ess}
%D A C -> B D -> A D harrownodes nil 20 nil <->
%D C D |-> .plabel= a *
%D C E -> D F -> C F harrownodes nil 20 nil <->
%D E F <-|
%D ))
%D (( \DAG \DAG*
%D @ 0 @ 1 -> sl^^ .plabel= a �{ess}
%D @ 0 @ 1 <- .plabel= m *
%D @ 0 @ 1 >-> sl__
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\diag{dag-minimal}$}
\savebox{\myboxb}{$\diag{dag-medium}$}
\savebox{\myboxc}{$\diag{dag-full}$}
\diag{dags}
$$
\msk
(The moral is that there is something canonical about
representing topologies ($T_0$, and on finite sets)
by DAGs with very few arrows)
\newpage
% --------------------
% «presheaves» (to ".presheaves")
% (s "Presheaves" "presheaves")
\myslide {Presheaves} {presheaves}
A {\sl presheaf} on $(X,\OX)$ is a
(contravariant) functor $\OX^\op \to \Set$.
A {\sl sheaf} is a presheaf obeying a
``glueing condition'', that we will see later.
Example: $\Cinfty: \Opens(\R)^\op \to \Set$. If $V \subset U$, then:
%
%D diagram presh-1
%D 2Dx 100 +35
%D 2D 100 \Cinfty(V) <--- \Cinfty(U)
%D 2D ^ ^ ^
%D 2D | | |
%D 2D - - -
%D 2D +25 V >------------> U
%D 2D
%D (( \Cinfty(V) \Cinfty(U) V U
%D @ 0 @ 1 <- .plabel= a _V^U
%D @ 0 @ 2 <-| @ 1 @ 3 <-| @ 0 @ 3 varrownodes nil 20 nil <-|
%D @ 2 @ 3 >->
%D ))
%D enddiagram
%D
$$\diag{presh-1}$$
The map $_V^U := \Cinfty(V \monicto U)$ is called the
``restriction function''.
\msk
We will borrow some terminology from the case of functions
defined over open sets: for a presheaf $P: \OX^\op \to \Set$ and
$W \subseteq V \subseteq U$,
%
$$\begin{array}{rl}
p_U \in P(U) & \text{a ``function/element with support $U$''} \\
p_X \in P(X) & \text{a ``global function/element''} \\
_V^U: P(U) \to P(V) & \text{``restriction function''} \\
(_V^U := P(V \monicto U)) & \\
\end{array}
$$
Functoriality means two conditions on restriction maps:
$P(U \monicto U) = \id_{P(U)}$
$P(W \monicto V)�P(V \monicto U) = P(W \monicto U)$
%
%D diagram presh-2
%D 2Dx 100 +25 +25
%D 2D 100 P(W) <----- P(U)
%D 2D <- <-
%D 2D +20 P(V)
%D 2D
%D 2D +15 W >--------> U
%D 2D >-> >->
%D 2D +20 V
%D 2D
%D (( P(W) P(V) P(U)
%D W V U
%D @ 0 @ 1 <- @ 1 @ 2 <- @ 0 @ 2 <-
%D @ 3 @ 4 >-> @ 4 @ 5 >-> @ 3 @ 5 >->
%D @ 0 @ 3 <-| @ 1 @ 4 <-| @ 2 @ 5 <-|
%D ))
%D enddiagram
%D
$$\diag{presh-2}$$
\newpage
% --------------------
% «subtopology-of-R» (to ".subtopology-of-R")
% (s "A subtopology of $\R$" "subtopology-of-R")
\myslide {A subtopology of $\protect\R$} {subtopology-of-R}
The topology on the DAG $\bbV$ can be seen as a subtopology of $\R$...
Consider the quotient $q$ below, or, equivalently, $q'$:
$$\begin{array}{l}
q: \R \to \{(-�,0], \, (0,1), \, [1,�)\} \\
q': \R \to \{\aa, \cc, \bb\}
\end{array}
$$
${q'}^{-1}(\Pts(\{\aa, \cc, \bb\})) \;\subset\; \Pts(\R)$ is a topology on $\R$ with 8 open sets.
${q'}^{-1}(\Pts(\{\aa, \cc, \bb\})) � \OR \;\subset\; \OR \;\subset\; \Pts(\R)$
is a topology on $\R$ with 5 open sets.
Compare:
%
%D diagram UVW-and-R-1
%D 2Dx 100 +12 +12 +20 +12 +12 +30 +12 +12 +27 +12 +12
%D 2D 100 X X'
%D 2D / \ / \
%D 2D +20 \aa \bb U V U' V' \aa' \bb'
%D 2D \ / \ / \ / \ /
%D 2D +20 \cc W W' \cc'
%D 2D | |
%D 2D +20 \emp \emp{}
%D 2D
%D (( X .tex= \{\aa,\bb,\cc\}
%D U .tex= \{\aa,\cc\} V .tex= \{\bb,\cc\}
%D W .tex= \{\cc\}
%D \emp
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D (( X' .tex= (-�,�)
%D U' .tex= (-�,1) V' .tex= (0,�)
%D W' .tex= (0,1)
%D \emp{}
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( \aa' .tex= (-�,0] \bb' .tex= [1,�) \cc' .tex= (0,1)
%D \aa' \cc' -> \bb' \cc' ->
%D ))
%D enddiagram
%D
$$\diag{UVW-and-R-1}$$
We will refer to these open sets as $X$, $U$, $V$, $W$, $\emp$:
%D diagram XUVW-and-bits
%D 2Dx 100 +15 +15 +30 +15 +15
%D 2D 100 \dagVee111 X
%D 2D
%D 2D +20 \dagVee101 \dagVee011 U V
%D 2D
%D 2D +20 \dagVee001 W
%D 2D
%D 2D +20 \dagVee000 \emp
%D 2D
%D 2D +20
%D 2D
%D (( \dagVee111
%D \dagVee101 \dagVee011
%D \dagVee001
%D \dagVee000
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D (( X U V W \emp
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{XUVW-and-bits}$$
Note that $U$ will sometimes mean a specific open set - $\dagVee101$ -,
sometimes an arbitrary open set; same for the other letters.
\newpage
% --------------------
% «coherent-families» (to ".coherent-families")
% (s "Coherent families" "coherent-families")
\myslide {Coherent families} {coherent-families}
Now let $X := \R$, and let's consider two
functions defined on subsets of $X$:
$\begin{array}{rrcl}
x_U: & U & \to & \R \\
& x & \mto & x \\
0_U: & U & \to & \R \\
& x & \mto & 0 \\
\end{array}
$
(I.e., we're defining $x_X, x_U, x_V, x_W, x_\emp$,
$0_X, 0_U, 0_V, 0_W, 0_\emp$).
\msk
We can also consider families of functions,
whose supports are families of open sets -
$\{x_U, x_V\}$ and $\{x_U, 0_V\}$ are families with support $\{U,
V\}$.
Note: $\{x_U, x_V, 0_V\}$ is {\sl not} a family with support $\{U, V\}$
because $V$ has two ``images'': $x_V$ and $0_V$.
\bsk
A function defined on $U$ - say, $x_U$ -
induces a family $\{x_U\}$ defined on $\{U\}$, i.e., on $\dagKite01000$ -
and another family, $\{x_U, x_W, x_\emp,\}$,
defined on all open sets under $U$ -
i.e., on the saturation of $\{U\} = \dagKite01000$, which is
$\dagKite01011$.
\bsk
When we try to extend the family $\{x_U, 0_V\}$
to the saturation of $\dagKite01100$, i.e., to $\dagKite01111$,
we see that we get two different candidates for $W$ -
$x_W \neq 0_W$ - which is not good...
\msk
A family is said to be {\sl coherent} when its extension
to the saturation of its support is well-defined.
$\{x_U, x_V\}$ is coherent, $\{x_U, 0_V\}$ is not.
Here's a way to define formally coherence for families:
a family $a_\U$ is coherent iff $�a_U, a_V � a_\U \; a_U|_{U�V} =
a_V|_{U�V}$.
Note that $\{x_U, 0_V, 0_W\}$ is not coherent.
\newpage
% --------------------
% «saturation» (to ".saturation")
% (s "Saturation and bisaturation" "saturation")
\myslide {Saturation and bisaturation} {saturation}
Notation: the calligraphic letters $\calU, \calV, \calW$
will denote families of open sets, and the annotations
`${}^\bol$', `${}^\bul$', `${}^\dbul$' will indicate how saturated a
family is -
$\calU^\bol$: not necessarily saturated
$\calU^\bul$: saturated
$\calU^\dbul$: bisaturated
We will sometimes use $\bul$, $\dbul$ to denote {\sl operations}:
$\bul$ is ``saturate'', $\dbul$ is ``bisaturate''.
\newpage
% --------------------
% «a-presheaf-on-a-dag» (to ".a-presheaf-on-a-dag")
% (s "A (bad) presheaf on a DAG" "a-presheaf-on-a-dag")
\myslide {A (bad) presheaf on a DAG} {a-presheaf-on-a-dag}
%D diagram UVW-and-R
%D 2Dx 100 +15 +15 +30 +15 +15
%D 2D 100 X X'
%D 2D / \ / \
%D 2D +20 U V U' V'
%D 2D \ / \ /
%D 2D +20 W W'
%D 2D | |
%D 2D +20 \emp \emp{}
%D 2D
%D 2D +20
%D 2D
%D (( X
%D U V
%D W
%D \emp
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D (( X' .tex= (-�,�)
%D U' .tex= (-�,1) V' .tex= (0,�)
%D W' .tex= (0,1)
%D \emp{}
%D @ 0 @ 1 <- @ 0 @ 2 <-
%D @ 1 @ 3 <- @ 2 @ 3 <-
%D @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{UVW-and-R}$$
Here is a presheaf over $(X,\Opens(X))$ (``$P$'') that is
not a sheaf - it violates the two sheaf conditions.
$P$ is not collated - because
$\{p_U, p_{V'}\}$ is a coherent family (on $\{U,V\}$)
that cannot be collated to a global function.
$P$ is not separated - because
there are two different collations for $\{p_U, p_V\}$.
% (find-dn4file "dednat41.lua" "forths[\".PLABEL=\"] =")
% (find-dn4file "dednat41.lua" "storenode =")
%L thereplusxy = function (dx, dy, tag)
%L ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L return ds[1]
%L end
%L forths["there+xy:"] = function ()
%L thereplusxy(getword(), getword(), getword())
%L end
\def\ph#1{\phantom{O}}
\def\ph#1{#1}
\def\ph#1{O}
\def\ph#1{{\color{red}#1}}
\def\ph#1{\phantom{#1}}
%D diagram bad-presheaf
%D 2Dx 100 +15 +15 +30 +15 +15
%D 2D 100 X X'
%D 2D / \ / \
%D 2D +20 U V U' V'
%D 2D \ / \ /
%D 2D +20 W W'
%D 2D | |
%D 2D +20 \emp \emp{}
%D 2D
%D (( X .tex= P(X)
%D U .tex= P(U) V .tex= P(V)
%D W .tex= P(W)
%D \emp .tex= P(\emp)
%D @ 0 @ 1 -> @ 0 @ 2 ->
%D @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -6 0 X'L .tex= \ph{p_X}
%D X' there+xy: 6 0 X'R .tex= \ph{p'_X}
%D V' there+xy: -6 0 V'L .tex= \ph{p_V}
%D V' there+xy: 6 0 V'R .tex= \ph{p'_V}
%D ))
%D (( X' .tex= \{p_X,p'_X\}
%D U' .tex= \{p_U\} V' .tex= \{p_V,p'_V\}
%D W' .tex= \{p_W\}
%D \emp{} .tex= \{p_\emp\}
%D # @ 0 @ 1 -> @ 0 @ 2 ->
%D # @ 1 @ 3 -> @ 2 @ 3 ->
%D # @ 3 @ 4 ->
%D X' place
%D X'L U' -> X'R U' -> X'L V'L -> X'R V'L ->
%D V' place
%D U' W' -> V'L W' -> V'R W' ->
%D W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf}$$
\newpage
% --------------------
% «presheaf-on-a-dag-germs» (to ".presheaf-on-a-dag-germs")
% (s "A presheaf on a DAG: its space of germs" "presheaf-on-a-dag-germs")
\myslide {A presheaf on a DAG: its space of germs} {presheaf-on-a-dag-germs}
Its space of germs is built like this:
for each point in $X$ - i.e., for $\aa, \bb, \gg$; let's look
at $\aa$ - look at all open sets containing $\aa$ (namely:
$U=\{\aa,\cc\}, X=\{\aa,\bb,\cc\}$) and take the colimit of $P$
on these open sets as they get smaller and smaller.
As there is a smallest open set containing $\aa$ - and $\bb$,
and $\cc$ - these colimits/germs are very easy to calculate:
%D diagram bad-presheaf-germs
%D 2Dx 100 +15 +15 +30 +15 +15
%D 2D 100 \aa \bb \aa' \bb'
%D 2D \ / \ /
%D 2D +20 \cc \cc'
%D 2D
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( \bb' there+xy: -6 0 \bb'L .tex= \ph{p_\bb}
%D \bb' there+xy: 6 0 \bb'R .tex= \ph{p'_\bb}
%D ))
%D (( \aa' .tex= \{p_\aa\}
%D \bb' .tex= \{p_\bb,p'_\bb\}
%D \cc' .tex= \{p_\cc\}
%D \aa' \cc' ->
%D \bb' place \bb'L \cc' -> \bb'R \cc' ->
%D ))
%D enddiagram
%D
$$\begin{matrix}
p_\aa := p_U \\
p_\bb := p_V \\
p'_\bb := p'_V \\
p_\cc := p_W \\
\end{matrix}
\qquad
\cdiag{bad-presheaf-germs}
$$
\msk
The projection map $E \to X$ is the obvious one.
We need to put a topology to $E$; it turns out (why?) that the
right topology is the one induced by the obvious graph.
Now this induces a sheaf of sections...
{\bf (I am skipping some steps -)}
%D diagram bad-presheaf-sheaf
%D 2Dx 100 +15 +15 +30 +15 +15
%D 2D 100 X X'
%D 2D / \ / \
%D 2D +20 U V U' V'
%D 2D \ / \ /
%D 2D +20 W W'
%D 2D | |
%D 2D +20 \emp \emp{}
%D 2D
%D 2D +20
%D 2D
%D (( X .tex= S(X)
%D U .tex= S(U) V .tex= S(V)
%D W .tex= S(W)
%D \emp .tex= S(\emp)
%D @ 0 @ 1 -> @ 0 @ 2 ->
%D @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -5 0 X'L .tex= \ph{s_X}
%D X' there+xy: 5 0 X'R .tex= \ph{s'_X}
%D V' there+xy: -5 0 V'L .tex= \ph{s_V}
%D V' there+xy: 5 0 V'R .tex= \ph{s'_V}
%D ))
%D (( X' .tex= \{s_X,s'_X\}
%D U' .tex= \{s_U\} V' .tex= \{s_V,s'_V\}
%D W' .tex= \{s_W\}
%D \emp{} .tex= \{s_\emp\}
%D # @ 0 @ 1 -> @ 0 @ 2 ->
%D # @ 1 @ 3 -> @ 2 @ 3 ->
%D # @ 3 @ 4 ->
%D X' place
%D X'L U' -> X'R U' -> X'L V'L -> X'R V'R ->
%D V' place
%D U' W' -> V'L W' -> V'R W' ->
%D W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf-sheaf}$$
\newpage
% --------------------
% «denses-and-stables» (to ".denses-and-stables")
% (s "Dense and stable truth-values" "denses-and-stables")
\myslide {Dense and stable truth-values} {denses-and-stables}
At the left below we see the representation as a presheaf
of the ``$\dbul$-stable truth-values'', $\sst{Ï}{Ï^\dbul=Ï} \subset �$;
It is a sheaf, and it can be recovered from its ``global elements''.
\msk
%D diagram denses-and-stables
%D 2Dx 100 +25 +25 +40 +25 +25
%D 2D 100 X X'
%D 2D / \ / \
%D 2D +30 U V U' V'
%D 2D \ / \ /
%D 2D +30 W W'
%D 2D | |
%D 2D +30 \emp \emp{}
%D 2D
%D (( X .tex= \sof{\k00001,\k00011,\k00111,\k01011,\k11111}
%D U .tex= \sof{\k�0�01,\k�0�11,\k�1�11} V .tex= \sof{\k��001,\k��011,\k��111}
%D W .tex= \sof{\k���01,\k���11}
%D \emp .tex= \sof{\k����1})
%D @ 0 @ 1 -> @ 0 @ 2 ->
%D @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 3 @ 4 ->
%D ))
%D (( X' .tex= \sof{\k01111,\k11111}
%D U' .tex= \sof{\k�1�11} V' .tex= \sof{\k��111}
%D W' .tex= \sof{\k���11}
%D \emp{} .tex= \sof{\k����0,\k����1}
%D @ 0 @ 1 -> @ 0 @ 2 ->
%D @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 3 @ 4 ->
%D ))
%D enddiagram
%D
$$\def\k{\dagKite}
\diag{denses-and-stables}
$$
\msk
At the right above we see the representation as a presheaf
of the ``$\dbul$-dense truth-values'', $�_\dbul := \sst{Ï}{Ï^\dbul=�} \subset �$.
It is not a sheaf, it can't be recovered from its ``global elements''
as $\sst{Ï}{Ï^\dbul=Ï}$ can; yet - and I have to admit that I found that
{\sl very} surprising - we can recover the modality from
the subobject $�_\dbul \monicto �$, by:
$Ï^\dbul := Ï � �_\dbul$
% \end{document}
\newpage
% --------------------
% «subst-for-iff» (to ".subst-for-iff")
% (s "Substitution principles for `$\Bij$'" "subst-for-iff")
\myslide {Substitution principles for `$\Bij$'} {subst-for-iff}
We will also use the following ``substitution principles'':
if $P$, $Q$, $Q'$, $R$, $R'$ are formulas, and $R'$ is obtained from $R$
by replacing some occurrences of $Q$ in it by $Q'$, then
%: P|-Q<=>Q' P|-Q<=>Q' P|-R
%: ========= ===============
%: P|-R<=>R' and P|-R'
%:
%: ^<=>-subst-1 ^<=>-subst-2
%:
$$\ded{<=>-subst-1} \qquad \ded{<=>-subst-2}$$
\msk
The ``theorems'' above - and the ones in the following slides -
can be proved using just the sequent calculus rules for intuitionistic
propositional logic augmented with the three axioms for `${}^*$'.
\msk
To make the proofs more manageable we will often make use of the
``\,`$\Bij$' trick'': starting from $P \vdash Q \Bij Q'$ and a proof of $P \vdash R$
we can produce a proof of $P \vdash R'$, where $R'$ is $R$
with some occurrences of `$Q$' replaced by `$Q'$'s.
\msk
Example:
(...)
To prove these first theorems ---
and the ones in the next slides ---
we will need some facts about the
biconditional, `$\Bij$', that is defined as:
%
$$P \Bij Q := (P⊃Q)∧(Q⊃P)$$
\newpage
% --------------------
% «LT-modalities» (to ".LT-modalities")
% (s "Lawvere-Tierney Modalities" "LT-modalities")
\myslide {Lawvere-Tierney Modalities} {LT-modalities}
A {\sl (Lawvere-Tierney) modality} is an operation `${}^*$' on
intuitionistic truth-values obeing the following three axioms:
%:
%: P|-Q
%: ---- ------ -------
%: |-�* P*|-Q* P**|-P*
%:
%: ^ax*-1 ^ax*-2 ^ax*-3
%:
$$\ded{ax*-1} \qquad \ded{ax*-2} \qquad \ded{ax*-3}$$
The supersaturation operation, $P^* := P^\dbul$, is an example of an
LT-modality --- but there are others:
\msk
$P^* := P^{��} := ��P$
$P^* := P^{(\aa∨)} := \aa ∨ P$
$P^* := P^{(\bb⊃)} := \bb ⊃ P$
\msk
First theorems:
\ssk
$P \vdash P^*$
\ssk
$(P∧Q)^* \vdash P^*∧Q^*$
\ssk
$P∧Q^* \vdash (P∧Q)^*$
$P^*∧Q^* \vdash (P∧Q)^*$
\msk
From what we already have,
we can prove that $P \Bij Q$ implies
$P^* \Bij Q^*$ in a weak sense:
%:
%: |-P<=>Q |-P<=>Q
%: ------- -------
%: |-P⊃Q |-Q⊃P
%: ----- -----
%: P|-Q Q|-P
%: ------ ------
%: P*|-Q* Q*|-P*
%: ------- -------
%: |-P*⊃Q* |-Q*⊃P*
%: -----------------
%: |-P*<=>Q*
%:
%: ^P<=>Q|-P*<=>Q*-weak
%:
$$\ded{P<=>Q|-P*<=>Q*-weak}$$
But there isn't much that we can do when $P \Bij Q$ is weaker than $�$...
For example, if $P:=\dagVee011$ and $Q:=\dagVee101$, then $P \Bij Q=\dagVee001$.
\msk
We will treat this as an axiom:
%:
%: --------------
%: P<=>Q|-P*<=>Q*
%:
%: ^antisymmetry-star
%:
$$\ded{antisymmetry-star}$$
(Actually this is true for any unary operation
on truth-values of a Heyting algebra).
\newpage
% --------------------
% «LT-modalities-and» (to ".LT-modalities-and")
% (s "LT-modalities and `and'" "LT-modalities-and")
\myslide {LT-modalities and `and'} {LT-modalities-and}
Theorems:
\ssk
$P \vdash P^*$
\ssk
$(P∧Q)^* \vdash P^*∧Q^*$
\ssk
$P∧Q^* \vdash (P∧Q)^*$
$P^*∧Q^* \vdash (P∧Q)^*$
\msk
Proofs:
%: --------
%: P|-�<=>P
%: -------- ----------
%: |-�<=>�* P|-�*<=>P*
%: -----------------------
%: P|-�<=>P*
%: ---------
%: P|-P*
%:
%: ^and*-1
%:
%: ------------
%: P|-Q<=>(P∧Q)
%: ------ ------ ==============
%: P∧Q|-P P∧Q|-Q P|-Q*<=>(P∧Q)*
%: ---------- ---------- --------------
%: (P∧Q)*|-P* (P∧Q)*|-Q* P|-Q*⊃(P∧Q)*
%: ----------------------- ------------
%: (P∧Q)*|-P*∧Q* P∧Q*|-(P∧Q)*
%:
%: ^and*-2 ^and*-3
%:
%: ============
%: P*∧Q|-(P∧Q)*
%: ============== ---------------- ---------------
%: P*∧Q*|-(P*∧Q)* (P*∧Q)*|-(P∧Q)** (P∧Q)**|-(P∧Q)*
%: ---------------------------------------------------
%: P*∧Q*|-(P∧Q)*
%:
%: ^and*-4
%:
$$\ded{and*-1}$$
$$\ded{and*-2} \qquad \ded{and*-3}$$
$$\ded{and*-4}$$
\msk
The cube of modalities for `$∧$' has only four different
truth-values (the case $P^* := P^{��}$, $P = \dagVee011$, $Q = \dagVee101$
shows that they are all distinct):
%
%D diagram and-cube
%D 2Dx 100 +20 +25 +20 +40 +20 +25 +20
%D 2D 100 P∧Q P∧Q* P∧Q' P∧Q*'
%D 2D +20 (P∧Q)* (P∧Q*)* (P∧Q)*' (P∧Q*)*'
%D 2D
%D 2D +20 P*∧Q P*∧Q* P*∧Q' P*∧Q*'
%D 2D +20 (P*∧Q)* (P*∧Q*)* (P*∧Q)*' (P*∧Q*)*'
%D 2D
%D (( P∧Q P*∧Q P∧Q* P*∧Q*
%D (P∧Q)* (P*∧Q)* (P∧Q*)* (P*∧Q*)*
%D @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 =
%D ))
%D (( P∧Q' P*∧Q' P∧Q*' P*∧Q*'
%D (P∧Q)*' (P*∧Q)*' (P∧Q*)*' (P*∧Q*)*'
%D @ 0 .tex= \dagVee001 @ 1 .tex= \dagVee101
%D @ 2 .tex= \dagVee011 @ 3 .tex= \dagVee111
%D @ 4 .tex= \dagVee111 @ 5 .tex= \dagVee111
%D @ 6 .tex= \dagVee111 @ 7 .tex= \dagVee111
%D @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 =
%D ))
%D enddiagram
%D
$$\diag{and-cube}$$
\newpage
% --------------------
% «LT-modalities-or» (to ".LT-modalities-or")
% (s "LT-modalities and `or'" "LT-modalities-or")
\myslide {LT-modalities and `or'} {LT-modalities-or}
Theorems:
\msk
%:
%: ------ ------ -------------
%: P|-P∨Q Q|-P∨Q P*∨Q*|-(P∨Q)*
%: ---------- ---------- -----------------
%: P*|-(P∨Q)* Q*|-(P∨Q)* (P*∨Q*)*|-(P∨Q)**
%: ----------------------- -----------------
%: P*∨Q*|-(P∨Q)* (P*∨Q*)*|-(P∨Q)*
%:
%: ^or*-1 ^or*-2
%:
$$\ded{or*-1} \qquad \ded{or*-2}$$
\msk
The cube of modalities for `$∨$' has only five different
truth-values (the case $P^* := P^{��}$,
$P = \dagHouse00001$, $Q = \dagHouse00010$
shows that they are all distinct):
%
%D diagram or-cube
%D 2Dx 100 +20 +25 +20 +40 +20 +25 +20
%D 2D 100 P∨Q P∨Q* P∨Q' P∨Q*'
%D 2D +20 (P∨Q)* (P∨Q*)* (P∨Q)*' (P∨Q*)*'
%D 2D
%D 2D +20 P*∨Q P*∨Q* P*∨Q' P*∨Q*'
%D 2D +20 (P*∨Q)* (P*∨Q*)* (P*∨Q)*' (P*∨Q*)*'
%D 2D
%D (( P∨Q P*∨Q P∨Q* P*∨Q*
%D (P∨Q)* (P*∨Q)* (P∨Q*)* (P*∨Q*)*
%D @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 ->
%D ))
%D (( P∨Q' P*∨Q' P∨Q*' P*∨Q*'
%D (P∨Q)*' (P*∨Q)*' (P∨Q*)*' (P*∨Q*)*'
%D @ 0 .tex= \dagHouse00011 @ 1 .tex= \dagHouse00111
%D @ 2 .tex= \dagHouse01011 @ 3 .tex= \dagHouse01111
%D @ 4 .tex= \dagHouse11111 @ 5 .tex= \dagHouse11111
%D @ 6 .tex= \dagHouse11111 @ 7 .tex= \dagHouse11111
%D @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 ->
%D ))
%D enddiagram
%D
$$\diag{or-cube}$$
% Here's the tableau that shows that the implication
% (P*⊃Q)*⊃(P⊃Q)*
% can't be strict when P*:=A∨P - i.e., it describes the
% intuitionistic countermodels for (A∨(P⊃Q))⊃(A∨((A∨P)⊃Q)).
%
% (A∨(P⊃Q))⊃(A∨((A∨P)⊃Q))
% 0 a
% 1 � 00 0 �b<-a
% 1∨ 1 b
% 0�1 �c<-b
% 1 �0 �d<-b
% 1∨1 d
%
% �b<-a.(A1b ∨ (�c<-b. P0c∨Q1c)) ∧
% (A0b ∧ (�d<-b. (A1d∨P1d)∧Q0d))
%
% �b<-a. (�c<-b. P0c∨Q1c) ∧
% (A0b ∧ (�d<-b. (A1d∨P1d)∧Q0d))
%
% �b<-a. (�c<-b. P0c) ∧
% (A0b ∧ (�d<-b. (A1d∨P1d)∧Q0d))
%
% �b<-a. P0b ∧
% A0b ∧ (�d<-b. A1d∧Q0d)
\newpage
% --------------------
% «LT-modalities-imp» (to ".LT-modalities-imp")
% (s "LT-modalities and implication" "LT-modalities-imp")
\myslide {LT-modalities and implication} {LT-modalities-imp}
Theorems:
%:
%: ----------
%: (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*
%:
%: ^imp*-1 ^imp*-2
%:
%: --------------- -------
%: P*∧(P⊃Q*)*|-Q** Q**|-Q*
%: ------------- -------------------------
%: (P⊃Q)*|-P*⊃Q* P*∧(P⊃Q*)*|-Q*
%: ------------- --------------
%: P*∧(P⊃Q)*|-Q* (P⊃Q*)*|-P*⊃Q*
%:
%: ^imp*-3 ^imp*-4
%:
$$\ded{imp*-1} \qquad \ded{imp*-2}$$
$$\ded{imp*-3} \qquad \ded{imp*-4}$$
\msk
The cube of modalities for `$⊃$' has only five different truth-values.
The case $P^* := \dagSqr0011 ∨ P$, $P = \dagSqr0010$, $Q = \dagSqr0000$
distinguishes them all:
%
%D diagram imp-cube-Aor
%D 2Dx 100 +20 +25 +20 +40 +20 +25 +20
%D 2D 100 P⊃Q P⊃Q* P⊃Q' P⊃Q*'
%D 2D +20 (P⊃Q)* (P⊃Q*)* (P⊃Q)*' (P⊃Q*)*'
%D 2D
%D 2D +20 P*⊃Q P*⊃Q* P*⊃Q' P*⊃Q*'
%D 2D +20 (P*⊃Q)* (P*⊃Q*)* (P*⊃Q)*' (P*⊃Q*)*'
%D 2D
%D (( P⊃Q P*⊃Q P⊃Q* P*⊃Q*
%D (P⊃Q)* (P*⊃Q)* (P⊃Q*)* (P*⊃Q*)*
%D @ 0 @ 1 <- @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 =
%D @ 4 @ 5 <- @ 4 @ 6 -> @ 5 @ 7 -> @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 = @ 3 @ 7 =
%D ))
%D (( P⊃Q' P*⊃Q' P⊃Q*' P*⊃Q*'
%D (P⊃Q)*' (P*⊃Q)*' (P⊃Q*)*' (P*⊃Q*)*'
%D @ 0 .tex= \dagSqr0101 @ 1 .tex= \dagSqr0000
%D @ 2 .tex= \dagSqr1111 @ 3 .tex= \dagSqr1111
%D @ 4 .tex= \dagSqr0111 @ 5 .tex= \dagSqr0011
%D @ 6 .tex= \dagSqr1111 @ 7 .tex= \dagSqr1111
%D @ 0 @ 1 <- @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 =
%D @ 4 @ 5 <- @ 4 @ 6 -> @ 5 @ 7 -> @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 = @ 3 @ 7 =
%D ))
%D enddiagram
%D
$$\diag{imp-cube-Aor}$$
When the modality is $P^* := ��P$ we can't distinguish the four
truth-values in the front face of the cube (the `$(P^?⊃Q^?)^*$'s)...
The best that we can do is this. For $P^* := ��P$, $P = \dagHouse00001$, $Q = \dagHouse00010$,
%
%D diagram imp-cube-notnot
%D 2Dx 100 +20 +25 +20 +40 +20 +25 +20
%D 2D 100 P⊃Q P⊃Q* P⊃Q' P⊃Q*'
%D 2D +20 (P⊃Q)* (P⊃Q*)* (P⊃Q)*' (P⊃Q*)*'
%D 2D
%D 2D +20 P*⊃Q P*⊃Q* P*⊃Q' P*⊃Q*'
%D 2D +20 (P*⊃Q)* (P*⊃Q*)* (P*⊃Q)*' (P*⊃Q*)*'
%D 2D
%D (( P⊃Q P*⊃Q P⊃Q* P*⊃Q*
%D (P⊃Q)* (P*⊃Q)* (P⊃Q*)* (P*⊃Q*)*
%D @ 0 @ 1 <- @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 =
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 = @ 3 @ 7 =
%D ))
%D (( P⊃Q' P*⊃Q' P⊃Q*' P*⊃Q*'
%D (P⊃Q)*' (P*⊃Q)*' (P⊃Q*)*' (P*⊃Q*)*'
%D @ 0 .tex= \dagHouse01011 @ 1 .tex= \dagHouse00011
%D @ 2 .tex= \dagHouse11111 @ 3 .tex= \dagHouse11111
%D @ 4 .tex= \dagHouse11111 @ 5 .tex= \dagHouse11111
%D @ 6 .tex= \dagHouse11111 @ 7 .tex= \dagHouse11111
%D @ 0 @ 1 <- @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 =
%D @ 4 @ 5 = @ 4 @ 6 = @ 5 @ 7 = @ 6 @ 7 =
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 = @ 3 @ 7 =
%D ))
%D enddiagram
%D
$$\diag{imp-cube-notnot}$$
\newpage
% --------------------
% «tops-for-or-and-imp» (to ".tops-for-or-and-imp")
% (s "The topologies for `or' and `implies'" "tops-for-or-and-imp")
\myslide {The topologies for `or' and `implies'} {tops-for-or-and-imp}
\def\dagRehprime#1#2#3#4#5#6#7{%
\dagpicture(26,60)(-10,-36)[16]{
\dagput( 0, 12){$#1$} % top
\dagput( 0, 0){$#2$} % second line
\dagput(-6,-12){$#3$} % third line, left
\dagput( 6,-12){$#4$} % third line, right
\dagput( 0,-24){$#5$} % fourth line, left
\dagput(12,-24){$#6$} % fourth line, left
\dagput( 6,-36){$#7$} % bottom
}}
$\dagReh0011 ∨ \dagReh???? = \dagReh??11$
$\dagReh0011 ⊃ \dagReh???? = (\dagReh0011 ⊃_c \dagReh????)^o
= (�_c\dagReh0011 ∨_c \dagReh????)^o
= (\dagReh1100 ∨_c \dagReh????)^o
= (\dagReh11??)^o$
The image of an idempotent operator is its fixset.
% $\bhbox{\dagRehprime1234567}$
%D diagram ??
%D 2Dx 100 +20 +20 +20
%D 2D 100 A
%D 2D
%D 2D +25 B
%D 2D
%D 2D +20 C D
%D 2D
%D 2D +20 E F
%D 2D
%D 2D +20 G
%D 2D
%D (( A .tex= \dagReh1111
%D B .tex= \dagReh0111
%D C .tex= \dagReh0101 D .tex= \dagReh0011
%D E .tex= \dagReh0001 F .tex= \dagReh0010
%D G .tex= \dagReh0000
%D A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram
%D diagram ??or
%D 2Dx 100 +20 +20 +20
%D 2D 100 A
%D 2D
%D 2D +25 B
%D 2D
%D 2D +20 C D
%D 2D
%D 2D +20 E F
%D 2D
%D 2D +20 G
%D 2D
%D (( A .tex= \dagRehprime\x\o\o\o\o\o\o
%D B .tex= \dagRehprime\x\x\o\o\o\o\o
%D C .tex= \dagRehprime\x\x\x\o\o\o\o D .tex= \dagRehprime\x\x\o\x\o\o\o
%D E .tex= \dagRehprime\x\x\x\x\x\o\o F .tex= \dagRehprime\x\x\o\x\o\x\o
%D G .tex= \dagRehprime\x\x\x\x\x\x\x
%D A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram
%D diagram ??imp
%D 2Dx 100 +20 +20 +20
%D 2D 100 A
%D 2D
%D 2D +25 B
%D 2D
%D 2D +20 C D
%D 2D
%D 2D +20 E F
%D 2D
%D 2D +20 G
%D 2D
%D (( A .tex= \dagRehprime\x\x\x\x\x\x\x
%D B .tex= \dagRehprime\x\o\x\x\x\x\x
%D C .tex= \dagRehprime\x\o\o\x\o\x\o D .tex= \dagRehprime\x\o\x\o\o\x\x
%D E .tex= \dagRehprime\x\o\o\o\o\x\o F .tex= \dagRehprime\x\o\x\o\o\o\o
%D G .tex= \dagRehprime\x\o\o\o\o\o\o
%D A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram
%D
$$\def\o{\bol}
\def\x{\bul}
\diag{??}
\qquad
\diag{??or}
\qquad
\diag{??imp}
$$
\newpage
% --------------------
% «more-about-not-not» (to ".more-about-not-not")
% (s "More about double negation" "more-about-not-not")
\myslide {More about double negation} {more-about-not-not}
The value of $��P$ depends only on the values of $P$
on the terminal worlds (the ``leaves'').
\msk
How to see this:
\ssk
$�P$ is the opposite of $P$ at the leaf-worlds and is the
biggest possible (i.e., as 1-ish as possible) in the
other worlds;
$��P$ coincides with $P$ at the leaf-worlds and is the
biggest possible in the other worlds.
%D diagram not-on-leaf-worlds
%D 2Dx 100 +40 +40
%D 2D 100 P
%D 2D |-->
%D 2D +25 P' |--> notP |--> notnotP
%D 2D |-->
%D 2D +25 P''
%D 2D
%D (( P .tex= \dagSeven0001100
%D P'' .tex= \dagSeven0101100
%D P' .tex= \dagSeven???1100
%D notP .tex= \dagSeven0010011
%D notnotP .tex= \dagSeven0101100
%D P notP |-> .plabel= a �
%D P' notP |-> .plabel= a �
%D P'' notP |-> .plabel= b �
%D notP notnotP |-> .plabel= a �
%D ))
%D enddiagram
%D
$$\diag{not-on-leaf-worlds}$$
\msk
Let's write (temporarily) `${}^?$' for ``apply `${}^*$' or not''.
$P^?∧Q^?$ stands for: $P∧Q$, $P∧Q^*$, $P^*∧Q$, $P^*∧Q^*$ ---
four truth-values.
\msk
Fact: when ${}^* = ��$,
$(P^?∧Q^?)^*$ is well-defined,
$(P^?∨Q^?)^*$ is well-defined,
$(P^?⊃Q^?)^*$ is well-defined,
$(�P)^*$ is well-defined ---
the outer `${}^*$' dominates everything and makes
all inner applications of `${}^*$'s irrelevant.
\msk
In the cubes from the previous slides,
``the outer `${}^*$' dominates'' means:
``the four truth-values in the front face ---
the `$(P^?\text{ op }Q^?)^*$'s --- are all equivalent''.
This is not true for the modality $P^* = P^{(\aa∨)} = \aa∨P$!
\newpage
% --------------------
% «modalities-alt-axioms» (to ".modalities-alt-axioms")
% (s "Modalities: alternative axioms" "modalities-alt-axioms")
\myslide {Modalities: alternative axioms} {modalities-alt-axioms}
A {\sl Lawvere-Tierney topology} is usually defined as an arrow $j: � \to �$
such that these three diagrams commute:
%:*`*\ign *
\def\ign#1{}
%D diagram LT-topology
%D 2Dx 100 +30 +20 +30 +30 +35
%D 2D t j /\
%D 2D 100 1 ----> �`0 �`2 ----> �`3 �� -------> �
%D 2D \ | \ | | |
%D 2D t \ | j j \ | j j×j | | j
%D 2D \ v \ v v /\ v
%D 2D +30 -> �`1 -> �`4 {��} -----> {�}
%D 2D
%D (( 1 �`0 �`1
%D @ 0 @ 1 -> .plabel= a t
%D @ 0 @ 2 -> .plabel= l t
%D @ 1 @ 2 -> .plabel= r j
%D ))
%D (( �`2 �`3 �`4
%D @ 0 @ 1 -> .plabel= a j
%D @ 0 @ 2 -> .plabel= l j
%D @ 1 @ 2 -> .plabel= r j
%D ))
%D (( �� � {��} {�}
%D @ 0 @ 1 -> .plabel= a {∧}
%D @ 0 @ 2 -> .plabel= l j×j
%D @ 1 @ 3 -> .plabel= r j
%D @ 2 @ 3 -> .plabel= a {∧}
%D ))
%D enddiagram
%D
$$\diag{LT-topology}$$
Which means:
$$ Ï[�]=Ï[�^*] \qquad Ï[P^*]=Ï[P^{**}] \qquad Ï[P^*∧Q^*]=Ï[(P∧Q)^*] $$
%:
%: ----- ------- ------- ------------- -------------
%: �|-�* P*|-P** P**|-P* P*∧Q*|-(P∧Q)* (P∧Q)*|-P*∧Q*
%:
%: ^LT-ax-1 ^LT-ax-2 ^LT-ax-3 ^LT-ax-4 ^LT-ax-5
%:
$$\ded{LT-ax-1} \qquad \ded{LT-ax-2} \qquad \ded{LT-ax-3}$$
$$\ded{LT-ax-4} \qquad \ded{LT-ax-5}$$
\medskip
It is not clear that these axioms (``LT axioms'')
are equivalent to the three axioms (``LT-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 $� \vdash �^*$
and \quad $\cded{ax*-2}$
can be proved from the LT axioms...
\medskip
Here are the proofs:
%:
%: P|-Q
%: ------
%: �|-P⊃Q
%: -------- ============
%: P|-�<=>P �|-P<=>(P∧Q)
%: ---------- ---------------
%: P|-�*<=>P* �|-P*<=>(P*∧Q*)
%: ---------- ---------------
%: P|-�<=>P* �|-P*⊃Q*
%: --------- --------
%: P|-P* P*|-Q*
%:
%: ^LT-equiv-1 ^LT-equiv-2
%:
$$\ded{LT-equiv-1} \qquad \ded{LT-equiv-2}$$
\newpage
% --------------------
% «LT-modalities-quants» (to ".LT-modalities-quants")
% (s "LT-modalities and the quantifiers" "LT-modalities-quants")
\myslide {LT-modalities and the quantifiers} {LT-modalities-quants}
Quantifiers:
%:
%: ------- --------------
%: P|-�x.P �x.P*|-(�x.P)*
%: ----------- ------------------
%: P*|-(�x.P)* (�x.P*)*|-(�x.P)**
%: -------------- ------------------
%: �x.P*|-(�x.P)* (�x.P*)*|-(�x.P)*
%:
%: ^ex*-1 ^ex*-2
%:
%:
%: -------
%: �x.P|-P
%: ----------- ----------------
%: (�x.P)*|-P* (�x.P*)*|-�x.P**
%: -------------- ----------------
%: (�x.P)*|-�x.P* (�x.P*)*|-�x.P*
%:
%: ^fa*-1 ^fa*-2
%:
$$\ded{ex*-1} \qquad \ded{ex*-2}$$
$$\ded{fa*-1} \qquad \ded{fa*-2}$$
%D diagram ex-square
%D 2Dx 100 +40
%D 2D 100 �x.P �x.P*
%D 2D
%D 2D +40 (�x.P)* (�x.P*)*
%D 2D
%D (( �x.P �x.P* ->
%D (�x.P)* (�x.P*)* =
%D �x.P (�x.P)* ->
%D �x.P* (�x.P*)* ->
%D ))
%D enddiagram
%D
%D diagram fa-square
%D 2Dx 100 +40
%D 2D 100 �x.P �x.P*
%D 2D
%D 2D +40 (�x.P)* (�x.P*)*
%D 2D
%D (( �x.P �x.P* ->
%D (�x.P)* (�x.P*)* ->
%D �x.P (�x.P)* ->
%D �x.P* (�x.P*)* =
%D ))
%D enddiagram
%D
$$\diag{ex-square} \qquad \diag{fa-square}$$
\newpage
% --------------------
% «sat-cov-fibration» (to ".sat-cov-fibration")
% (s "The fibration of saturated covers" "sat-cov-fibration")
\myslide {The fibration of saturated covers} {sat-cov-fibration}
\def\bbK{\mathbb{K}}
\def\bbV{\mathbb{V}}
\def\OKop{\Opens(\bbK^\op)}
\def\OOmop{\Opens(�^\op)}
\def\calU{\mathcal{U}}
\def\calV{\mathcal{V}}
For a DAG $\bbD$, define $\bbD' := \Opens(\bbD)^\op \equiv (\Opens(\bbD), \supseteq)$.
For example, when $\bbV := \dagVee***$, we have:
%D diagram satcov-fibration
%D 2Dx 100 +40 +15 +40 +40
%D 2D 100 _X1 _V ->
%D 2D +20 _X0 --------> _W ---> emp1
%D 2D +20 --> _U -------> emp0
%D 2D
%D 2D +20 V --->
%D 2D +20 X ----------> W --> \emp
%D 2D +20 ----> U --------->
%D 2D
%D 2D +20 \bb ->
%D 2D +20 \cc
%D 2D +20 \aa ------>
%D 2D
%D (( _X1 .tex= \dagKite11111 y+= -5
%D _X0 .tex= \dagKite01111
%D _U .tex= \dagKite01011
%D _V .tex= \dagKite00111
%D _W .tex= \dagKite00011
%D emp1 .tex= \dagKite00001
%D emp0 .tex= \dagKite00000 y+= 5
%D _X1 _X0 -> _X0 _U -> _X0 _V -> _U _W -> _V _W -> _W emp1 -> emp1 emp0 ->
%D ))
%D (( X .tex= \foo{X}{\dagVee111}
%D U .tex= \foo{U}{\dagVee101}
%D V .tex= \foo{V}{\dagVee011}
%D W .tex= \foo{W}{\dagVee001}
%D \emp .tex= \foo{\emp}{\dagVee000}
%D X U -> X V -> U W -> V W -> W \emp ->
%D ))
%D (( \aa \cc -> \bb \cc ->
%D ))
%D enddiagram
%D
% {\def\foo#1#2{#1{\equiv}#2}
$\def\foo#1#2{#1{\equiv}#2}
% \foo{A}{B}
\diag{satcov-fibration}
$
% }
\msk
% Fact: when $�$ is a topology
%
% the DAG $\OOmop$ is a fibration over $�$,
%
% with $\bigcup$ as the projection functor.
%
% For example, when $� := \Opens(\bbV)$ we have:
%
%
% \msk
The projection $\bigcup: \OOmop \to �$ respects $∧$ and $∨$, i.e.,
if $\bigcup \calU^\bul = U$ and $\bigcup \calV^\bul = V$ then
$\bigcup(\calU^\bul ∨ \calV^\bul) = U∨V$ (this is easy to see), and also
$\bigcup(\calU^\bul ∧ \calV^\bul) = U∧V$ (look at each $w � \bigcup(\calU^\bul ∧ \calV^\bul)$).
\msk
Each fiber $\bigcup�U$ is a lattice with top element $\calU^\dbul$.
When $�$ comes from a finite topology we can take
the intersection of all saturated covers of $U$,
and this gives a minimal saturated cover for $U$,
that we will call $\calU^\bulm$.
\msk
Fact: $\bulm \dashv \bigcup \dashv \dbul$.
%D diagram OKadj
%D 2Dx 100 +40 +30 +30
%D 2D 100 \OKop AL -> B --> CR
%D 2D ^v^ ^ v ^
%D 2D +30 \bbK A --> BM -> C
%D 2D
%D (( \OKop .tex= \OOmop \bbK .tex= �
%D \OKop \bbK <. sl__ .plabel= l *-
%D \OKop \bbK -> .plabel= m \bigcup
%D \OKop \bbK <- sl^^ .plabel= r **
%D AL .tex= \dagKite01111 A .tex= X
%D B .tex= \dagKite01111 BM .tex= X
%D CR .tex= \dagKite11111 C .tex= X
%D AL B -> B CR -> A BM -> BM C ->
%D AL A <.| .plabel= l *-
%D B BM |-> .plabel= m \bigcup
%D CR C <-| .plabel= r **
%D ))
%D enddiagram
%D
$$\diag{OKadj}$$
\newpage
% --------------------
% «embedding» (to ".embedding")
% (s "Embedding" "embedding")
\myslide {Embedding} {embedding}
A topology is a DAG in a natural way:
if $V, U � \O(X)$, then $V \to U$ iff $V \subseteq U$.
We will prefer $\O(X)^\op$ rather than $\O(X)$, for two
reasons: one is because then we will have a monotonic function
%
$$\begin{array}{rrcl}
\dnto: & \D & \to & \O(\D)^\op \\
& \aa & \mto & \dnto\aa
\end{array}
$$
%D diagram D-to-O(D)op
%D 2Dx 100 +15 +15 +40 +15 +15 +25 +15 +15
%D 2D 100 X X'
%D 2D
%D 2D +20 \aa \bb A B A' B'
%D 2D
%D 2D +20 \cc C C'
%D 2D
%D 2D +20 O O'
%D 2D
%D 2D +20
%D 2D
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( X .tex= \{\aa,\bb,\cc\}
%D A .tex= \{\aa,\cc\} B .tex= \{\bb,\cc\}
%D C .tex= \{\cc\}
%D O .tex= \emp
%D X A -> X B -> A C -> B C -> C O ->
%D ))
%D (( X' .tex= \dagVee111
%D A' .tex= \dagVee101 B' .tex= \dagVee011
%D C' .tex= \dagVee001
%D O' .tex= \dagVee000
%D X' A' -> X' B' -> A' C' -> B' C' -> C' O' ->
%D ))
%D (( \bb relphantom 5 8 A relphantom -10 8 ->
%D B relphantom 8 8 A' relphantom -3 8 =
%D ))
%D enddiagram
%D
$$\diag{D-to-O(D)op}$$
\newpage
% --------------------
% «geometric-morphisms» (to ".geometric-morphisms")
% (s "Geometric morphisms" "geometric-morphisms")
\myslide {Geometric morphisms} {geometric-morphisms}
%:*****
The obvious continuous function $f: 3 \to \bbV$
induces a geometric morphism, $(f^* \dashv f_*): \Set^3 \to \Set^V$.
It is essential: $f^! \dashv f^* \dashv f_*$.
%D diagram gm-1
%D 2Dx 100 +15 +15
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= A_\aa b .tex= A_\bb c .tex= A_\cc
%D a place b place c place
%D ))
%D enddiagram
%D diagram gm-2
%D 2Dx 100 +20 +20
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= A_\aa b .tex= A_\bb c .tex= A_\aa{+}A_\bb{+}A_\cc
%D a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-3
%D 2Dx 100 +15 +15
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= B_\aa b .tex= B_\bb c .tex= B_\cc
%D a place b place c place
%D ))
%D enddiagram
%D diagram gm-4
%D 2Dx 100 +20 +20
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= B_\aa b .tex= B_\bb c .tex= B_\cc
%D a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-5
%D 2Dx 100 +15 +15
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= C_\aa b .tex= C_\bb c .tex= C_\cc
%D a place b place c place
%D ))
%D enddiagram
%D diagram gm-6
%D 2Dx 100 +20 +20
%D 2D 100 a b
%D 2D +20 c
%D 2D
%D (( a .tex= C_\aa{×}C_\cc b .tex= C_\bb{×}C_\cc c .tex= C_\cc
%D a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-example
%D 2Dx 100 +75
%D 2D 100 A B
%D 2D
%D 2D +60 C D
%D 2D
%D 2D +60 E F
%D 2D
%D 2D +40 \Set^3 \Set^bbV
%D 2D
%D (( A .tex= \usebox{\myboxa}
%D B .tex= \usebox{\myboxb}
%D C .tex= \usebox{\myboxc}
%D D .tex= \usebox{\myboxd}
%D E .tex= \usebox{\myboxe}
%D F .tex= \usebox{\myboxf}
%D A B |-> .plabel= a f_!
%D A C -> B D -> A D harrownodes nil 20 nil <->
%D C D <-| .plabel= a f^*
%D C E -> D F -> C F harrownodes nil 20 nil <->
%D E F |-> .plabel= a f_*
%D ))
%D (( \Set^3 \Set^bbV
%D @ 0 @ 1 -> sl^^ .plabel= a f_!
%D @ 0 @ 1 <- .plabel= m f^*
%D @ 0 @ 1 -> sl__ .plabel= b f_*
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\diag{gm-1}$}
\savebox{\myboxb}{$\diag{gm-2}$}
\savebox{\myboxc}{$\diag{gm-3}$}
\savebox{\myboxd}{$\diag{gm-4}$}
\savebox{\myboxe}{$\diag{gm-5}$}
\savebox{\myboxf}{$\diag{gm-6}$}
\diag{gm-example}
$$
A simpler example:
%D diagram gm-example-2
%D 2Dx 100 +40
%D 2D 100 A B
%D 2D
%D 2D +25 C D
%D 2D
%D 2D +25 E F
%D 2D
%D 2D +25 \Set^2 \Set^2{}
%D 2D
%D (( A .tex= (A,A')
%D B .tex= (A+A',0)
%D C .tex= (B,B')
%D D .tex= (B,B)
%D E .tex= (C,C')
%D F .tex= (C×C',1)
%D A B |-> .plabel= a g_!
%D A C -> B D -> A D harrownodes nil 20 nil <->
%D C D <-| .plabel= a g^*
%D C E -> D F -> C F harrownodes nil 20 nil <->
%D E F |-> .plabel= a g_*
%D ))
%D (( \Set^2 \Set^2{}
%D @ 0 @ 1 -> sl^^ .plabel= a g_!
%D @ 0 @ 1 <- .plabel= m g^*
%D @ 0 @ 1 -> sl__ .plabel= b g_*
%D ))
%D enddiagram
%D
$$\diag{gm-example-2}$$
%:****^{**}*
%:***^**
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: