|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This file: (find-LATEX "2019J-ops-cubes.tex")
% See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-cubes.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-cubes.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-cubes.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-cubes"))
% (find-pdf-page "~/LATEX/2019J-ops-cubes.pdf")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-cubes.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-cubes.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019J-ops-cubes.pdf
% file:///tmp/2019J-ops-cubes.pdf
% file:///tmp/pen/2019J-ops-cubes.pdf
% http://angg.twu.net/LATEX/2019J-ops-cubes.pdf
% (find-LATEX "2019.mk")
% «.cubes» (to "cubes")
\directlua{tf_push("2019J-ops-cubes.tex")}
% ___ _ _ _
% / _ \| |____ _(_) ___ _ _ ___ ___ _ _| |__ ___ ___
% | | | | '_ \ \ / / |/ _ \| | | / __| / __| | | | '_ \ / _ \/ __|
% | |_| | |_) \ V /| | (_) | |_| \__ \ | (__| |_| | |_) | __/\__ \
% \___/|_.__/ \_/ |_|\___/ \__,_|___/ \___|\__,_|_.__/ \___||___/
%
% «cubes» (to ".cubes")
% (jonp 13 "cubes")
% (joc "cubes")
% (ph2p 13 "obvious-cubes")
% (p2lp 4 "cubes")
% (p2l "cubes")
\section{How J-operators interact with connectives}
\label {cubes}
% (find-LATEX "2015planar-has.tex" "J-connectives")
% (find-planarhaspage 16 "How J-operators interact with the connectives")
% (find-planarhastext 16 "How J-operators interact with the connectives")
The axiom $\J3$ says that $(P∧Q)¹=P¹∧Q¹$ --- it says something about
how `$·^*$' interacts with `$∧$'. Let's introduce a shorter notation.
There are eight ways to replace each of the `?'s in $(P^? ∧ Q^?)^?$ by
either nothing or a star. We establish that the three `?'s in $(P^? ∧
Q^?)^?$ are ``worth'' 1, 2 and 4 respectively, and we use $P \oand_n
Q$ to denote $(P^? ∧ Q^?)^?$ with the bits ``that belong to $n$''
replaced by stars. So:
%
$$\begin{array}{rcrcrcr}
\oand_0 &=& P∧Q, && \oand_4 &=& (P∧Q)^*, \\
\oand_1 &=& P^*∧Q, && \oand_5 &=& (P^*∧Q)^*, \\
\oand_2 &=& P∧Q^*, && \oand_6 &=& (P∧Q^*)^*, \\
\oand_3 &=& P^*∧Q^*, && \oand_7 &=& (P^*∧Q^*)^*. \\
\end{array}
$$
We omit the arguments of $\oand_n$ when they are $P$ and $Q$ --- so we
can rewrite $(P∧Q)¹=P¹∧Q¹$ as $\oand_4=\oand_3$. These conventions
also hold for $\oor$ and $\oimp$.
%D diagram cube-and*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-and*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-or*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
\pu
%$$
% \begin{array}{rcl}
% \diag{cube-and*-obvious} && \diag{cube-and*-full} \\ \\
% \diag{cube-or*-obvious} && \diag{cube-or*-full} \\ \\
% \diag{cube-imp*-obvious} && \diag{cube-imp*-full} \\
% \end{array}
%$$
It is easy to prove each one of the arrows in the cubes below ($A
\diagxyto/->/ B$ means $A≤B$):
%
$$\myresizebox{$
\pu
\diag{cube-and*-obvious}
\quad
\diag{cube-or*-obvious}
\quad
\diag{cube-imp*-obvious}
$}
$$
\bsk
Let's write their sets of elements as $\oand_\zs := \{\oand_0, \ldots,
\oand_7\}$, $\oor_\zs := \{\oor_0, \ldots, \oor_7\}$, and $\oimp_\zs
:= \{\oimp_0, \ldots, \oimp_7\}$. The cubes above --- we will call
them the ``obvious and-cube'', the ``obvious or-cube'', and the
``obvious implication-cube'' --- can be interpreted as directed graphs
$(\oand_\zs, \OCube_\land)$, $(\oor_\zs, \OCube_\lor)$, $(\oimp_\zs,
\OCube_\to)$.
The ``extended cubes'' will be the directed graphs with the arrows
above plus the ones coming from these derived rules:
%:
%:
%: =====================\oand_7=\oand_3=\oand_4
%: (P¹∧Q¹)¹=P¹∧Q¹=(P∧Q)¹
%:
%: ^and*-extra-arrow
%:
%: ===============\oor_7≤\oor_3
%: (P¹∨Q¹)¹≤(P∨Q)¹
%:
%: ^or*-extra-arrow
%:
%: =============\oimp_6≤\oimp_3
%: (P→Q¹)¹≤P¹→Q¹
%:
%: ^imp*-extra-arrow
%:
%:
%:
%: ------\J2 ------\J2
%: P²=P¹ Q²=Q¹
%: =============================\J3
%: (P¹∧Q¹)¹=P²∧Q²=P¹∧Q¹=(P∧Q)¹
%: -----------------------------
%: (P¹∧Q¹)¹=P¹∧Q¹=(P∧Q)¹
%:
%: ^and*-extra-arrow-proof
%:
%: ---------
%: P→Q¹≤P→Q¹
%: ----- ----- -----------
%: P≤P∨Q Q≤P∨Q (P→Q¹)∧P≤Q¹
%: ---------\Mo ----------\Mo ---------------\Mo
%: P¹≤(P∨Q)¹ Q¹≤(P∨Q)¹ ((P→Q¹)∧P)¹≤Q²
%: ----------------------- ---------------\J2
%: P¹∨Q¹≤(P∨Q)¹ ((P→Q¹)∧P)¹≤Q¹
%: ---------------\Mo ---------------\J3
%: (P¹∨Q¹)¹≤(P∨Q)² (P→Q¹)¹∧P¹≤Q¹
%: ----------------\J2 --------------
%: (P¹∨Q¹)¹≤(P∨Q)¹ (P→Q¹)¹≤P¹→Q¹
%:
%: ^or*-extra-arrow-proof ^imp*-extra-arrow-proof
%:
%:
$$
\myresizebox{$\pu
\def\bk{HELLO}
\def\bk{\hspace{-0.5cm}}
\begin{array}{rcl}
\multicolumn{3}{l}{\ded{and*-extra-arrow} \quad :=} \\ \\
\multicolumn{3}{r}{\ded{and*-extra-arrow-proof}} \\ \\
\ded{or*-extra-arrow} &:=& \bk \ded{or*-extra-arrow-proof} \\\\
\ded{imp*-extra-arrow} &:=& \ded{imp*-extra-arrow-proof} \\
\end{array}
$}
$$
%
where $\oand_7=\oand_3=\oand_4$ will be interpreted as these arrows:
%
$$(P^*∧Q^*)^* \two/<-`->/<200> P^*∧Q^* \two/<-`->/<200> (P∧Q)^*$$
The directed graphs of these ``extended cubes'' will be called
$(\oand_\zs, \ECube_\land)$, $(\oor_\zs, \ECube_\lor)$, $(\oimp_\zs,
\ECube_\to)$. We are interested in the (non-strict) partial orders
that they generate, and we want an easy way to remember these partial
orders. The figure below shows these extended cubes at the left, and
at the right the ``simplified cubes'', $\SCube_∧$, $\SCube_∨$, and
$\SCube_→$, that generate the same partial orders that the extended
cubes.
%D diagram extended-and-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oand_7
%D ren A5 A3 A6 ==> \oand_5 \oand_3 \oand_6
%D ren A1 A4 A2 ==> \oand_1 \oand_4 \oand_2
%D ren A0 ==> \oand_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 -> sl^ A3 A7 <- sl_
%D A3 A4 -> sl^ A3 A4 <- sl_
%D ))
%D enddiagram
%
%D diagram extended-and-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oand_7
%D ren A5 A3 A6 ==> \oand_5 \oand_3 \oand_6
%D ren A1 A4 A2 ==> \oand_1 \oand_4 \oand_2
%D ren A0 ==> \oand_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram extended-or-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oor_7
%D ren A5 A3 A6 ==> \oor_5 \oor_3 \oor_6
%D ren A1 A4 A2 ==> \oor_1 \oor_4 \oor_2
%D ren A0 ==> \oor_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D A7 A4 -> .slide= 8pt
%D ))
%D enddiagram
%
%D diagram extended-or-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oor_7
%D ren A5 A3 A6 ==> \oor_5 \oor_3 \oor_6
%D ren A1 A4 A2 ==> \oor_1 \oor_4 \oor_2
%D ren A0 ==> \oor_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram extended-imp-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oimp_7
%D ren A5 A3 A6 ==> \oimp_5 \oimp_3 \oimp_6
%D ren A1 A4 A2 ==> \oimp_1 \oimp_4 \oimp_2
%D ren A0 ==> \oimp_0
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D A6 A3 ->
%D ))
%D enddiagram
%
%D diagram extended-imp-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oimp_7
%D ren A5 A3 A6 ==> \oimp_5 \oimp_3 \oimp_6
%D ren A1 A4 A2 ==> \oimp_1 \oimp_4 \oimp_2
%D ren A0 ==> \oimp_0
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
%\begin{figure}
\pu
$$\resizebox{!}{180pt}{%
$
\begin{array}{rcl}
\left( \diag{extended-and-cube-with-arrows} \right)^* &=&
\left( \diag{extended-and-cube-with-equals} \right)^* \\ \\
\left( \diag{extended-or-cube-with-arrows} \right)^* &=&
\left( \diag{extended-or-cube-with-equals} \right)^* \\ \\
\left( \diag{extended-imp-cube-with-arrows} \right)^* &=&
\left( \diag{extended-imp-cube-with-equals} \right)^* \\ \\
\end{array}
$
}
$$
%$}
% \caption{The extended cubes and the simplified cubes.}
% \label{fig:extended-and-simplified-cubes}
%\end{figure}
From these cubes it is easy to see, for example, that we can prove
$\oor_5 = \oor_6$ (as a derived rule).
\directlua{tf_pop()}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "joc"
% End: