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