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