% (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:
