Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% (find-LATEX "2019modalities-in-S4.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019modalities-in-S4.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019modalities-in-S4.pdf"))
% (defun e () (interactive) (find-LATEX "2019modalities-in-S4.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019modalities-in-S4"))
% (find-pdf-page   "~/LATEX/2019modalities-in-S4.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019modalities-in-S4.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019modalities-in-S4.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019modalities-in-S4.pdf
%               file:///tmp/2019modalities-in-S4.pdf
%           file:///tmp/pen/2019modalities-in-S4.pdf
% http://angg.twu.net/LATEX/2019modalities-in-S4.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% See:
% (find-LATEX "2015oppositions.tex")
% (find-pdf-page "~/LATEX/2015oppositions.pdf")
% https://mail.google.com/mail/ca/u/0/#search/from%3Ame+to%3Alogica-l%40dimap.ufrn.br+S4/FMfcgxcmtSzkBPKFSSsnPvknfTzGWtDz
% https://mail.google.com/mail/ca/u/0/#search/from%3Ame+to%3Alogica-l%40dimap.ufrn.br+S4/FMfcgxmScvfJKvrHLmsWqHfTcGQCwBzq
% (find-books "__modal/__modal.el" "chellas")
% (find-es "googlegroups" "logica-l")
% https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/JxptOElKnI0/h-ZX6qmvDwAJ
% https://groups.google.com/a/dimap.ufrn.br/forum/#!msg/logica-l/JxptOElKnI0/h-ZX6qmvDwAJ use this!
% https://groups.google.com/a/dimap.ufrn.br/forum/#!topic/logica-l/UujFOXoKTy4 announcement, 2019sep18

% (ph1p 23 "topologies")
% (ph1     "topologies")
% (ph1     "topologies" "house")

% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L WB = "1.2.3|.4.5..67"
%L mp = MixedPicture.new({def="dagWB", meta="s", scale="5pt"}):zfunction(WB):output()
\pu
% $\dagWB 1234567$


Let our Kripke frame $(W,R)$ be the transitive-reflexive closure of this:
%
%D diagram WB-frame
%D 2Dx     100 +20 +20 +20 +20 +20   +20
%D 2D  100 1       2       3
%D 2D        \   /   \   /
%D 2D         v v     v v
%D 2D  +20     4       5       6 <-> 7
%D 2D
%D (( 1 4 -> 2 4 -> 2 5 -> 3 5 -> 6 7 <->
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{WB-frame}
$$




% (find-LATEXgrep "grep --color -nH -e zdef *.tex")
% (find-dednat6 "dednat6/zhas.lua" "mpnew")



%         1     2     3
%          \   / \   /
% (W,R) =   v v   v v
%            4     5    6<->7
%
%       = {(1,2,3,4,5,6,7),
%          {(1,4), (2,4), (2,5), (3,5), (6,7), (7,6)}
%         }
%
% v(   P) = {    3,4,    7}
% v(  ◻P) = {      4      }
% v( ⋄◻P) = {1,2,  4      }
% v(◻⋄◻P) = {1,   4      }
% v(  ⋄P) = {1,2,3,4,  6,7}
% v( ◻⋄P) = {1,    4,  6,7}
% v(⋄◻⋄P) = {1,2,  4,  6,7}
%
%           1 1 1
%            1 0  11
%            ^    ^
%           /      \
%          /        \                         ⋄P
%      1 1 0         \                       ^  ^
%       1 0  11       \                     /    \
%       ^   ^          \                 ⋄◻⋄P     \
%      /     \          \                ^  ^      \
%     /       \          \              /    \      \
% 1 0 0      1 1 0       0 0 1       ◻⋄P     ⋄◻P     P
%  1 0  11    1 0  00     1 0  01       ^    ^      ^
%     ^         ^        ^               \  /      /
%      \       /        /                ◻⋄◻P     /
%       \     /        /                   ^     /
%       1 0 0         /                     \   /
%        1 0  00     /                       ◻P
%           ^       /
%            \     /
%             \   /
%            0 0 0
%             1 0  00

\bsk

The diagram of S4 modalities from p.149 of Chellas

and its values when $A=\{3,4,7\}⊆W$:
%
%D diagram S4-mods-A
%D 2Dx     100 +20 +20    +40
%D 2D  100         DA      
%D 2D            ^   ^     
%D 2D           /     \    
%D 2D  +20    DBDA     \   
%D 2D         ^  ^      \   
%D 2D        /    \      \     
%D 2D  +20 DBA    BDA     A 
%D 2D        ^    ^      ^
%D 2D         \  /      /   
%D 2D  +20    BDBA     /   
%D 2D            ^    /   
%D 2D             \  /    
%D 2D  +20         BA     
%D 2D
%D ren        DA      ==>        ⋄A
%D ren    DBDA        ==>    ⋄◻⋄A
%D ren DBA    BDA  A  ==> ⋄◻A    ◻⋄A  A
%D ren    BDBA        ==>    ◻⋄◻A
%D ren        BA      ==>        ◻A
%D
%D (( DBDA DA ->
%D    DBA DBDA -> BDA DBDA ->
%D    BDBA DBA -> BDBA BDA -> 
%D    BA BDBA ->
%D    A DA -> BA A ->
%D ))
%D enddiagram
%D
%D diagram S4-mods-v
%D 2Dx     100 +20 +20    +40
%D 2D  100         DA      
%D 2D            ^   ^     
%D 2D           /     \    
%D 2D  +20    DBDA     \   
%D 2D         ^  ^      \   
%D 2D        /    \      \     
%D 2D  +20 DBA    BDA     A 
%D 2D        ^    ^      ^
%D 2D         \  /      /   
%D 2D  +20    BDBA     /   
%D 2D            ^    /   
%D 2D             \  /    
%D 2D  +20         BA     
%D 2D
%D ren        DA      ==>                           \dagWB1111011
%D ren    DBDA        ==>              \dagWB1101011
%D ren DBA    BDA  A  ==> \dagWB1101000             \dagWB1001011  \dagWB0011001
%D ren    BDBA        ==>              \dagWB1001000
%D ren        BA      ==>                           \dagWB0001000
%D
%D (( DBDA DA ->
%D    DBA DBDA -> BDA DBDA ->
%D    BDBA DBA -> BDBA BDA -> 
%D    BA BDBA ->
%D    A DA -> BA A ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{S4-mods-A}
  \qquad
  \diag{S4-mods-v}
$$

\bsk

See:
\url{https://groups.google.com/a/dimap.ufrn.br/forum/\#!msg/logica-l/JxptOElKnI0/h-ZX6qmvDwAJ}


\newpage


Let our Kripke frame $(W,R)$ be the transitive-reflexive closure of this:
%
%D diagram WB-frame
%D 2Dx     100 +20 +20 +20 +20 +20   +20
%D 2D  100 1       2       3
%D 2D        \   /   \   /
%D 2D         v v     v v
%D 2D  +20     4       5       6 <-> 7
%D 2D
%D (( 1 4 -> 2 4 -> 2 5 -> 3 5 -> 6 7 <->
%D
%D ))
%D enddiagram
%D
\pu
$$
  \diag{WB-frame}
$$

\def\vDA{\dagWB1111011}
\def \vA{\dagWB0011001}
\def\vBA{\dagWB0001000}
\def\vDBA{\dagWB1101000}
\def\vBDA{\dagWB1001011}
\def\vDBDA{\dagWB1101011}
\def\vBDBA{\dagWB1001000}

%L forths["=="] = function () pusharrow("==") end

These implications are easy to prove:

%D diagram ??
%D 2Dx     100  +35  +35 +35 +0  +0  +35 +35 +35
%D 2D  100      DBDA     DA
%D 2D           
%D 2D  +35 BDBDA     BDA     A       DBA     DBDBA
%D 2D           
%D 2D  +35                       BA      BDBA
%D 2D
%D ren DA BDA DBDA BDBDA ==> ⋄A ◻⋄A ⋄◻⋄A ◻⋄◻⋄A
%D ren BA DBA BDBA DBDBA ==> ◻A ⋄◻A ◻⋄◻A ⋄◻⋄◻A
%D
%D (( DBDA BDBDA <- DBDA BDA <- DA BDA <- DA A <-
%D    A BA <- DBA BA <- DBA BDBA <- DBDBA BDBA <-
%D    # BDBDA BDA == DBA DBDBA ==
%D    # DBDA DA -->
%D    # BA BDBA -->
%D    # DA DBA <--
%D    # BDA BA <--
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

If $A=\{3,4,7\}⊆W$ we get some conjectures...
%
%D diagram ??
%D 2Dx     100  +35  +35 +35 +0  +0  +35 +35 +35
%D 2D  100      DBDA     DA
%D 2D           
%D 2D  +35 BDBDA     BDA     A       DBA     DBDBA
%D 2D           
%D 2D  +35                       BA      BDBA
%D 2D
%D ren A                 ==> \vA
%D ren DA BDA DBDA BDBDA ==> \vDA \vBDA \vDBDA \vBDA
%D ren BA DBA BDBA DBDBA ==> \vBA \vDBA \vBDBA \vDBA
%D
%D (( DBDA BDBDA <- DBDA BDA <- DA BDA <- DA A <-
%D    A BA <- DBA BA <- DBA BDBA <- DBDBA BDBA <-
%D    BDBDA BDA == DBA DBDBA ==
%D    DBDA DA -->
%D    BA BDBA -->
%D    DA DBA <--
%D    BDA BA <--
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

%D diagram ??
%D 2Dx     100  +35  +35 +35 +0  +0  +35 +35 +35
%D 2D  100      DBDA     DA
%D 2D           
%D 2D  +35 BDBDA     BDA     A       DBA     DBDBA
%D 2D           
%D 2D  +35                       BA      BDBA
%D 2D
%D ren DA BDA DBDA BDBDA ==> ⋄A ◻⋄A ⋄◻⋄A ◻⋄◻⋄A
%D ren BA DBA BDBA DBDBA ==> ◻A ⋄◻A ◻⋄◻A ⋄◻⋄◻A
%D
%D (( DBDA BDBDA <- DBDA BDA <- DA BDA <- DA A <-
%D    A BA <- DBA BA <- DBA BDBA <- DBDBA BDBA <-
%D    BDBDA BDA == DBA DBDBA ==
%D    DBDA DA -->
%D    BA BDBA -->
%D    DA DBA <--
%D    BDA BA <--
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$





















\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "NONE"
% End: