|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008modallogic.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008modallogic.tex && latex 2008modallogic.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008modallogic.tex && pdflatex 2008modallogic.tex"))
% (eev "cd ~/LATEX/ && Scp 2008modallogic.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008modallogic.dvi")
% (find-pspage "~/LATEX/2008modallogic.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008modallogic.ps 2008modallogic.dvi")
% (find-pspage "~/LATEX/2008modallogic.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008modallogic.pdf" (ee-twupfile "LATEX/2008modallogic.pdf") 'over)
% (ee-cp "~/LATEX/2008modallogic.pdf" (ee-twusfile "LATEX/2008modallogic.pdf") 'over)
% «.and-and-box» (to "and-and-box")
% «.cat-struct-1» (to "cat-struct-1")
% «.cat-struct-2» (to "cat-struct-2")
% «.nd-to-cat» (to "nd-to-cat")
% «.reyes-zolfaghari» (to "reyes-zolfaghari")
% «.beta-reductions» (to "beta-reductions")
\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 2008modallogic.dnt
%*
% (eedn4-51-bounded)
Just some trivial notes on Valéria de Paiva and Gavin
Bierman's ``On an Intuitionistic Modal Logic'' (2000).
\url{http://www.cs.bham.ac.uk/~vdp/publications/studia.ps.gz}
% (find-vdpimlpage 1)
% (find-vdpimltext)
\msk
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 {``Box'' commutes with ``and''} {2}
\tocline {Categorical structure (1)} {3}
\tocline {Categorical structure (2)} {4}
\tocline {The natural deduction rules, categorically} {5}
\tocline {Notes on Reyes \& Zolfaghari's paper} {6}
\tocline {Beta-reduction rules} {7}
% --------------------
% Charset and defs
% (ma)
% (eev-math-glyph-names "Delta" 916 "eta" 951 "mu" 956 "nu" 957 "poss" 9671)
% Orig: (eev-math-glyphs-set 'eev-glyph-face-math "nabla " "na" "Ώ")
% (eev-math-glyphs-set 'eev-glyph-face-greek "theta nu" "te nu" " Û")
% Local: (eev-math-glyphs-set 'eev-glyph-face-math "Delta poss" "DD po" "Ώ
")
% (eev-math-glyphs-set 'eev-glyph-face-greek "eta mu" "et mu" " Û")
% (find-vdpimlpage 1)
% (find-vdpimlpage 22)
% (find-vdpimltext)
\catcode`
=13 \def
{\lozenge}
\defΏ{\Delta}
\def{\eta}
\defÛ{\mu}
\def\myttchars{%
\ttchars%
\def
{\ttchar{$\lozenge$}}%
\defΏ{\ttchar{$\Delta$}}%
\def{\ttchar{$\eta$}}%
\defÛ{\ttchar{$\mu$}}%
}
\def\str{{―{str}}}
\def\D{{\mathbb{D}}}
\newpage
% --------------------
% «and-and-box» (to ".and-and-box")
% (s "``Box'' commutes with ``and''" "and-and-box")
\myslide {``Box'' commutes with ``and''} {and-and-box}
$ñ(A×B)⊃(ñA×ñB)$ and $(ñA×ñB)⊃ñ(A×B)$:
%: [ñ(A×B)]^1 [ñ(A×B)]^1
%: ---------- ----------
%: A×B A×B [ñA]^1 [ñB]^1
%: --- --- ------ ------
%: ñ(A×B) A ñ(A×B) B ñA×ñB ñA×ñB A B
%: ----------1 ----------1 ----- ----- ----------
%: ñA ñB ñA ñB A×B
%: -------------------- ----------------------1
%: ñA×ñB ñ(A×B)
%:
%: ^is4-m1 ^is4-m2
%:
$$\ded{is4-m1}$$
$$\ded{is4-m2}$$
but the two maps between $ñ(A×B) \leftrightarrows (ñA×ñB)$
need not be inverses.
\newpage
% --------------------
% «cat-struct-1» (to ".cat-struct-1")
% (s "Categorical structure (1)" "cat-struct-1")
\myslide {Categorical structure (1)} {cat-struct-1}
Monoidal functor:
%D diagram monoidal-functor
%D 2Dx 100 +15 +40 +15 +40 +15 +40 +15
%D 2D 100 ñA×ñ1 --> ñ(A×1) ñ1×ñA --> ñ(1×A)
%D 2D ^ \ ^ \
%D 2D / v / v
%D 2D +20 ñA×1 -----------------> ñA 1×ñA -----------------> ñA{}
%L xs={}
%D 2Dx 100 +70 +55 +50
%D 2D +20 ñA×(ñB×ñC) --> (ñA×ñB)×ñC ñA×ñB --> ñ(A×B)
%D 2D | | | |
%D 2D v v v v
%D 2D +20 ñA×ñ(B×C) ñ(A×B)×ñC ñB×ñA --> ñ(B×A)
%D 2D | |
%D 2D v v
%D 2D +20 ñ(A×(B×C)) -> ñ((A×B)×C)
%D 2D
%D (( ñA×1 ñA×ñ1 ñ(A×1) ñA
%D @ 0 @ 1 -> .plabel= l \id×m_1
%D @ 1 @ 2 -> .plabel= a m
%D @ 2 @ 3 -> .plabel= r ñ
%D @ 0 @ 3 -> .plabel= b
%D ))
%D (( 1×ñA ñ1×ñA ñ(1×A) ñA{}
%D @ 0 @ 1 -> .plabel= l m_1×\id
%D @ 1 @ 2 -> .plabel= a m
%D @ 2 @ 3 -> .plabel= r ñ'
%D @ 0 @ 3 -> .plabel= b '
%D ))
%D (( ñA×(ñB×ñC) (ñA×ñB)×ñC
%D ñA×ñ(B×C) ñ(A×B)×ñC
%D ñ(A×(B×C)) ñ((A×B)×C)
%D @ 0 @ 1 -> .plabel= a \aa
%D @ 0 @ 2 -> .plabel= l \id×m
%D @ 1 @ 3 -> .plabel= r m×\id
%D @ 2 @ 4 -> .plabel= l m
%D @ 3 @ 5 -> .plabel= r m
%D @ 4 @ 5 -> .plabel= b ñ\aa
%D ))
%D (( ñA×ñB ñ(A×B)
%D ñB×ñA ñ(B×A)
%D @ 0 @ 1 -> .plabel= a m
%D @ 0 @ 2 -> .plabel= l \cc
%D @ 1 @ 3 -> .plabel= r ñ\cc
%D @ 2 @ 3 -> .plabel= b m
%D ))
%D enddiagram
%D
$$\diag{monoidal-functor}$$
\bsk
Comonad:
%D diagram comonad
%D 2Dx 100 +30 +30 +35 +40
%D 2D 100 a0
%D 2D | --->
%D 2D +15 | a1 ñA ---> ññA ===> ñññA
%D 2D v <===
%D 2D +15 a2
%D 2D
%D (( a0 .tex= ñA a1 .tex= ññA a2 .tex= ñA
%D a0 a1 -> .plabel= a \dd
%D a2 a1 <- sl^ .plabel= a \ee
%D a2 a1 <- sl_ .plabel= b ñ\ee
%D a0 a2 -> .plabel= l \id
%D ))
%D (( ñA ññA ñññA
%D @ 0 @ 1 -> .plabel= a \dd
%D @ 1 @ 2 -> sl^ .plabel= a \dd
%D @ 1 @ 2 -> sl_ .plabel= b ñ\dd
%D ))
%D enddiagram
%D
$$\diag{comonad}$$
\msk
Monoidal comonad:
%D diagram monoidal-comonad
%D 2Dx 100 +50 +40 +40
%D 2D 100 ñA×ñB ----> ñ(A×B) {}ñA×ñB --> ñ(A×B){}
%D 2D | | \ |
%D 2D v | \ v
%D 2D +20 ññA×ññB | ----> A×B
%D 2D | |
%D 2D v v
%D 2D +20 ñ(ñA×ñB) -> ññ(A×B)
%D 2D
%L xs={}
%D 2Dx 100 +30 +30 +35 +40
%D 2D +20 a0
%D 2D | --->
%D 2D +15 | a1 1 ----> ñ1 ----> ññ1
%D 2D v <---
%D 2D +15 a2
%D 2D
%D (( ñA×ñB ñ(A×B)
%D ññA×ññB
%D ñ(ñA×ñB) ññ(A×B)
%D @ 0 @ 1 -> .plabel= a m
%D @ 0 @ 2 -> .plabel= l \dd×\dd
%D @ 1 @ 4 -> .plabel= r \dd
%D @ 2 @ 3 -> .plabel= l m
%D @ 3 @ 4 -> .plabel= b ñm
%D ))
%D (( {}ñA×ñB ñ(A×B){} A×B
%D @ 0 @ 1 -> .plabel= a m
%D @ 0 @ 2 -> .plabel= l \ee×\ee
%D @ 1 @ 2 -> .plabel= r \ee
%D ))
%D (( a0 .tex= 1 a1 .tex= ñ1 a2 .tex= 1
%D a0 a1 -> .plabel= a m
%D a2 a1 <- .plabel= b \ee
%D a0 a2 -> .plabel= l \id
%D ))
%D (( 1 ñ1 ññ1
%D @ 0 @ 1 -> .plabel= a m
%D @ 1 @ 2 -> sl^ .plabel= a m
%D @ 1 @ 2 -> sl_ .plabel= b ñm
%D ))
%D enddiagram
%D
$$\diag{monoidal-comonad}$$
\newpage
% --------------------
% «cat-struct-2» (to ".cat-struct-2")
% (s "Categorical structure (2)" "cat-struct-2")
\myslide {Categorical structure (2)} {cat-struct-2}
Monad:
%D diagram monad
%D 2Dx 100 +30 +30 +35 +40
%D 2D 100 a0
%D 2D | ===>
%D 2D +15 | a1
A <---
A <===
A
%D 2D v <---
%D 2D +15 a2
%D 2D
%D (( a0 .tex=
A a1 .tex=
A a2 .tex=
A
%D a0 a2 -> .plabel= a \id
%D a0 a1 -> sl^ .plabel= a
%D a0 a1 -> sl_ .plabel= b
%D a1 a2 -> .plabel= b Û
%D ))
%D ((
A
A
A
%D @ 0 @ 1 <- .plabel= a Û
%D @ 1 @ 2 <- sl^ .plabel= a Û
%D @ 1 @ 2 <- sl_ .plabel= b
Û
%D ))
%D enddiagram
%D
$$\diag{monad}$$
\msk
Strength:
%D diagram strength-pi
%D 2Dx 100 +50
%D 2D 100 ñ1×
A ---> 1×
A
%D 2D | |
%D 2D v |
%D 2D +20
(ñ1×A) |
%D 2D | |
%D 2D v v
%D 2D +20
(1×A) --->
A
%D 2D
%D (( ñ1×
A 1×
A -> .plabel= a ×\id
%D ñ1×
A
(ñ1×A) -> .plabel= l \str
%D 1×
A
A -> .plabel= r _2
%D
(ñ1×A)
(1×A) -> .plabel= l
(×\id)
%D ñ1×
A 1×
A -> .plabel= a ×\id
%D
(1×A)
A -> .plabel= l
(_2)
%D
%D ))
%D enddiagram
%D diagram strength-alpha
%D 2Dx 100 +80
%D 2D 100 ñA×(ñB×
C) ----> (ñA×ñB)×
C
%D 2D | |
%D 2D v |
%D 2D +20 ñA×
(ñB×C) |
%D 2D | v
%D 2D +10 | ñ(A×B)×
C
%D 2D v |
%D 2D +10
(ñA×(ñB×C)) |
%D 2D | |
%D 2D v v
%D 2D +20
((ñA×ñB)×C) ---->
(ñ(A×B)×C)
%D 2D
%D 2D +20
%D 2D
%D (( ñA×(ñB×
C) (ñA×ñB)×
C -> .plabel= a \aa
%D (ñA×ñB)×
C ñ(A×B)×
C -> .plabel= r m×\id
%D ñ(A×B)×
C
(ñ(A×B)×C) -> .plabel= r \str
%D ñA×(ñB×
C) ñA×
(ñB×C) -> .plabel= l \id×\str
%D ñA×
(ñB×C)
(ñA×(ñB×C)) -> .plabel= l \str
%D
(ñA×(ñB×C))
((ñA×ñB)×C) -> .plabel= l
\aa
%D
((ñA×ñB)×C)
(ñ(A×B)×C) -> .plabel= b (m×\id)
%D ))
%D enddiagram
%D diagram strength-triang
%D 2Dx 100 +40
%D 2D 100 ñA×B
%D 2D | --->
%D 2D +20 | ñA×
B
%D 2D v <--
%D 2D +20
(ñA×B)
%D 2D
%D (( ñA×B
(ñA×B) -> .plabel= l \eta
%D ñA×B ñA×
B -> .plabel= a \id×\eta
%D ñA×
B
(ñA×B) -> .plabel= b \str
%D ))
%D enddiagram
%D diagram strength-mu
%D 2Dx 100 +60
%D 2D 100 ñA×
B ----> ñA×
B
%D 2D | |
%D 2D v |
%D 2D +20
(ñA×
B) |
%D 2D | |
%D 2D v v
%D 2D +20
(ñA×B) -->
(ñA×B)
%D 2D
%D (( ñA×
B
(ñA×
B) -> .plabel= l \str
%D
(ñA×
B)
(ñA×B) -> .plabel= l
\str
%D
(ñA×B)
(ñA×B) -> .plabel= b \mu
%D ñA×
B ñA×
B -> .plabel= a \id×\mu
%D ñA×
B
(ñA×B) -> .plabel= r \str
%D
%D ))
%D enddiagram
$$\diag{strength-pi} \qquad \diag{strength-mu}$$
$$\diag{strength-alpha}
\quad
\diag{strength-triang}
$$
\newpage
% --------------------
% «nd-to-cat» (to ".nd-to-cat")
% (s "The natural deduction rules, categorically" "nd-to-cat")
\myslide {The natural deduction rules, categorically} {nd-to-cat}
%D diagram nec-intro
%D 2Dx 100 +50
%D 2D 100 \Gamma
%D 2D |
%D 2D v
%D 2D +20 ñA_1×ñA_2 ñ(ñA_1×ñA_2)
%D 2D | ^ |
%D 2D v / v
%D 2D +20 ññA_1×ññA_2 ñ(B)
%D 2D
%D (( \Gamma ñA_1×ñA_2 ->
%D ñA_1×ñA_2 ññA_1×ññA_2 -> .plabel= l \dd×\dd
%D ññA_1×ññA_2 ñ(ñA_1×ñA_2) -> .plabel= m m
%D ñ(ñA_1×ñA_2) ñ(B) ->
%D ))
%D enddiagram
%D diagram nec-elim
%D 2Dx 100
%D 2D 100 ñA
%D 2D
%D 2D +20 A
%D 2D
%D (( ñA A -> .plabel= l \ee
%D ))
%D enddiagram
%D diagram poss-intro
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +20
A
%D 2D
%D (( A
A -> .plabel= l \eta
%D ))
%D enddiagram
%D diagram poss-elim
%D 2Dx 100 +20 +20
%D 2D 100 \Gamma
(ñA×B)
%D 2D | ^ |
%D 2D | / |
%D 2D v / v
%D 2D +20 ñA×
B
(
C)
%D 2D <-
%D 2D +20
C
%D 2D
%D (( \Gamma ñA×
B -> .plabel= l {}
%D ñA×
B
(ñA×B) -> .plabel= m \str
%D
(ñA×B)
(
C) -> .plabel= r {}
%D
(
C)
C -> .plabel= m \mu
%D ))
%D enddiagram
$$\diag{nec-intro}
\qquad
\diag{nec-elim}
$$
$$\diag{poss-intro}
\qquad
\diag{poss-elim}
$$
\newpage
% --------------------
% «reyes-zolfaghari» (to ".reyes-zolfaghari")
% (s "Notes on Reyes & Zolfaghari's paper" "reyes-zolfaghari")
\myslide {Notes on Reyes \& Zolfaghari's paper} {reyes-zolfaghari}
Let $W$ be a set of worlds, and let $\D$ be a DAG on $W$.
$\D$ induces a reflexive and transitive relation $R \subset W×W$ ---
$(\aa \to \bb) \in \D$ iff $\aa R \bb$ --- ``$\aa$ sees $\bb$''.
$\ang{W,R}$ is an S4-ish modal frame.
We can regard $W$ and $\D$ as topological spaces:
$W$ is discrete, $\D$ has the topology in which the open sets are
the ones whose characteristic functions are non-decreasing.
The ``identity'' function $W \to \D$ is continuous.
Consider these toposes: $\Set^W$ and $\Set^\D$.
The truth-values of $\Set^W$ are the things that I call the
``modal truth-values'' on $\D$: they correspond to
arbitrary functions $W \to \{0,1\}$.
The truth-values of $\Set^D$ are the things that I call the
``intuitionistic truth-values'' of $\D$: they correspond to
non-decreasing functions $W \to \{0,1\}$.
There is a geometric morphism $\Set^W \to \Set^\D$.
`$ñ$' and `$
$' are endofunctors that act on the space
of truth-values of $\Set^W$.
The intuitionistic truth-values are the ones that are
stable by the action of $ñ$.
\bsk
Hypothesis:
%D diagram bul-and-box
%D 2Dx 100 +30 +30 +30
%D 2D 100 a |---> b
%D 2D --->
%D 2D +30 c <---| d \Set^W <--< \Set^\D
%D 2D --->
%D 2D +30 e |---> f
%D 2D
%D (( a .tex= \dagReh0100 b .tex= \dagReh0101
%D c .tex= \dagReh0101 d .tex= \dagReh0101
%D e .tex= \dagReh1101 f .tex= \dagReh0101
%D a b |-> .plabel= a \bul
%D a c -> b d ->
%D a d harrownodes nil 20 nil <->
%D c d <-|
%D c e -> d f ->
%D c f harrownodes nil 20 nil <->
%D e f |-> .plabel= b ñ
%D ))
%D (( \Set^W \Set^\D
%D @ 0 @ 1 -> sl^^ .plabel= a \bul
%D @ 0 @ 1 <-<
%D @ 0 @ 1 -> sl__ .plabel= b ñ
%D ))
%D enddiagram
%D
$$\diag{bul-and-box}$$
\newpage
% --------------------
% «beta-reductions» (to ".beta-reductions")
% (s "Beta-reduction rules" "beta-reductions")
\myslide {Beta-reduction rules} {beta-reductions}
\def\fst{{Π{fst}}}
\def\snd{{Π{snd}}}
\def\inl{{Π{inl}}}
\def\inr{{Π{inr}}}
\def\caseofinlinr#1#2#3#4#5{
\textsf{case $#1$ of $\inl(#2) \to #3 \;||\; \inr(#4) \to #5$}}
\def\boxwithfor#1#2#3{\textsf{box $#1$ with $#2$ for $#3$}}
\def\unbox #1{\textsf{unbox $#1$}}
\def\unboxp#1{\textsf{unbox($#1$)}}
\def£{\vec}
\def\I{\mathcal{I}}
\def\E{\mathcal{E}}
\def\betaquad{\quad \rightsquigarrow_\beta \quad}
%: [x:A]^1 \GG
%: :::::::::
%: M:B
%: -------------{⊃\I};1
%: N:A (πx:A.M):A->B N:A \GG
%: ------------------{⊃\E} :::::
%: (πx:A.M)N:B -> M[x:=N]:B
%:
%: ^betared-imp-1 ^betared-imp-2
%:
%: M:A N:B
%: -------------{∧\I}
%: \ang{M,N}:A×B
%: -----------------{∧\E}_1
%: \fst\ang{M,N}:A×B -> M:A
%:
%: ^betared-and1-1 ^betared-and1-2
%:
%: M:A [x:A]^1 \GG [y:B]^1 \DD
%: -----------∨\I ::::: :::::
%: \inl(M):A+B N:C P:C M:A \GG
%: ----------------------------------------∨\E ::::
%: \caseofinlinr{\inl(M)}{x}{N}{y}{P} N[x:=M]:C
%:
%: ^betared-or-1 ^betared-or-2
%:
%: \GG [£x:ñ£A]^1
%: : :
%: £M:ñA N:B \GG
%: -------------------------ñ\I;1 :::
%: \boxwithfor{N}{£M}{£x}:ñB £M:ñ£A
%: ---------------------------ñ\E :::
%: \unboxp{\boxwithfor{N}{£M}{£x}:ñB} N[£x:=£M]:B
%:
%: ^betared-box-1 ^betared-box-2
%:
%: \DD
%: :::
%: \GG N:B [£x:ñ£A\;y:B]^1 \GG \DD
%: ::: -----
\I ::: ::: :::
%: £M:ñA
N:
B P:
C £M:ñA N:B
%: ---------------------------
\E;1 ::::
%: P[£x:=£M,
y:=
N]:
C P[£x:=£M,y:=N]:
C
%:
%: ^betared-poss-1 ^betared-poss-2
%:
$$\ded{betared-imp-1} \qquad \ded{betared-imp-2}$$
$$\ded{betared-and1-1} \betaquad \ded{betared-and1-2}$$
$$\ded{betared-or-1} \betaquad \ded{betared-or-2}$$
$$\ded{betared-box-1} \betaquad \ded{betared-box-2}$$
$$\ded{betared-poss-1} \betaquad \ded{betared-poss-2}$$
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: