% This file: (find-LATEX "2019J-ops-logic.tex")
%       See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-logic.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-logic.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-logic.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-logic"))
% (find-pdf-page   "~/LATEX/2019J-ops-logic.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-logic.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-logic.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019J-ops-logic.pdf
%               file:///tmp/2019J-ops-logic.pdf
%           file:///tmp/pen/2019J-ops-logic.pdf
% http://angg.twu.net/LATEX/2019J-ops-logic.pdf
% (find-LATEX "2019.mk")

% «.J-operators»	(to "J-operators")

\directlua{tf_push("2019J-ops-logic.tex")}



%      _                       
%     | |       ___  _ __  ___ 
%  _  | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
%  \___/       \___/| .__/|___/
%                   |_|        
%
% «J-ops-and-regions» (to ".J-ops-and-regions")
% «J-operators»  (to ".J-operators")
% (jonp 8 "J-operators")
% (jol    "J-operators")
% J-regions and J-operators
% (p2lp 1 "J-operators")
% (p2l    "J-operators")
\section{J-operators}
\label  {J-operators}
% Good (ph2p 9 "J-ops-and-regions")

% (fooi "Ω" "H")

A {\sl J-operator} on a Heyting Algebra $H ≡ (H,≤,⊤,⊥,∧,∨,→,↔,¬)$ is a
function $J:H→H$ that obeys the axioms $\J1$, $\J2$, $\J3$ below; we
usually write $J$ as $·^*:H→H$, and write the axioms as rules.
%
%L addabbrevs(".\\eqJ.", " \\eqJ ")
%L addabbrevs("&", "\\&", "vv", "∨", "->", "→")
%L -- addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%:
%:    -----\J1   ------\J2   ------------\J3
%:    P≤P¹       P¹=P²       (P∧Q)¹=P¹∧Q¹
%:
%:    ^J1         ^J2          ^J3
%:
\pu
$$\ded{J1} \qquad \ded{J2} \qquad \ded{J3}$$
\par $\J1$ says that the operation $·^*$ is non-decreasing.
\par $\J2$ says that the operation $·^*$ is idempotent.
\par $\J3$ is a bit mysterious but will have interesting consequences.

\msk

% Note that when $H$ is a ZHA then any slash-operator on $H$ is a
% J-operator on it; see secs.\ref{slash-ops} and
% \ref{slash-ops-property}.
% 
% \msk

A J-operator induces an equivalence relation and equivalence classes
on $H$, like slashings do:
%
$$\begin{array}{rcl}
  P \eqJ Q  &\text{iff}& P^*=Q^* \\[5pt] \relax
  [P]^J &:=&         \setofst{Q∈H}{P^*=Q^*} \\
  \end{array}
$$
%
The equivalence classes of a J-operator $J$ are called {\sl
  $J$-regions}.

\msk

The axioms $\J1$, $\J2$, $\J3$ have many consequences. The first ones
are listed in Figure \ref{fig:J-ops-basic-derived-rules} as derived
rules, whose names mean:

$\Mop$ (monotonicity for products): a lemma used to prove $\Mo$,

$\Mo$ (monotonicity): $P≤Q$ implies $P^*≤Q^*$,

$\Sand$ (sandwiching): all truth values between $P$ and $P^*$ are equivalent,

$\ECa$: equivalence classes are closed by `$\&$',

$\ECv$: equivalence classes are closed by  `$∨$',

$\ECS$: equivalence classes are closed by sandwiching,

% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%:
%:                         ------------\J3   ---------
%:                         (P∧Q)¹=P¹∧Q¹      P¹∧Q¹≤Q¹
%:   ----------\Mop  :=    ---------------------------
%:   (P∧Q)¹≤Q¹            (P∧Q)¹≤Q¹
%:
%:   ^Mop1                 ^Mop2
%:
%:                  P≤Q
%:                  =====
%:                  P=P∧Q
%:                  ---------  ----------\Mop
%:   P≤Q            P¹=(P∧Q)¹  (P∧Q)¹≤Q¹
%:   ------\Mo  :=  ---------------------
%:   P¹≤Q¹                 P¹≤Q¹
%:
%:   ^Mo1                   ^Mo2
%:
%:                                  Q≤P¹
%:                                  -----\Mo  ------\J2
%:                        P≤Q       Q¹≤P²     P²=P¹
%:                       ------\Mo  ---------------
%:   P≤Q≤P¹              P¹≤Q¹            Q¹≤P¹
%:   --------\Sand  :=   ----------------------
%:     P¹=Q¹                   P¹=Q¹
%:
%:     ^Sand1                  ^Sand2
%:
%:
%:                          P¹=Q¹
%:                          ===========   ------------\J3
%:   P¹=Q¹                  P¹=Q¹=P¹∧Q¹   P¹∧Q¹=(P∧Q)¹
%:   ------------\ECa  :=   --------------------------
%:   P¹=Q¹=(P∧Q)¹                 P¹=Q¹=(P∧Q)¹
%:
%:   ^ECa1                        ^ECa2
%:                                                            P¹=Q¹
%:                                                  -----\J1  -----
%:                                                  Q≤Q¹      Q¹=P¹
%:                                        -----\J1  ---------------
%:                                        P≤P¹         Q≤P¹
%:                               -------  -----------------
%:                               P≤P∨Q     P∨Q≤P¹
%:                               ----------------
%:                                    P≤P∨Q≤P¹
%:                                    -----------\Sand
%:   P¹=Q¹                  P¹=Q¹\bk   P¹=(P∨Q)¹
%:   ------------\ECv  :=   ------------------
%:   P¹=Q¹=(P∨Q)¹            P¹=Q¹=(P∨Q)¹
%:
%:   ^ECv1                       ^ECv2
%:
%:                                    P¹=R¹
%:                          ----\J1   -----
%:                   P≤Q≤R  R≤R¹      R¹=P¹
%:                   ----------------------
%:                           P≤Q≤P¹
%:                           --------\Sand
%:   P≤Q≤R  P¹=R¹            P¹=Q¹          P¹=R¹
%:   ------------\ECS  :=    --------------------
%:     P¹=Q¹=R¹                 P¹=Q¹=R¹
%:
%:     ^ECS1                    ^ECS2
%:
\begin{figure}
\pu
  \resizebox{\textwidth}{!}{%
  \fbox{$
  \def\bk{HELLO}
  \def\bk{\hspace{-1cm}}
  \begin{array}{rcl} \\
  \ded{Mop1}  &:=& \ded{Mop2}  \\ \\
  \ded{Mo1}   &:=& \ded{Mo2}   \\ \\
  \ded{Sand1} &:=& \ded{Sand2} \\ \\
  \ded{ECa1}  &:=& \ded{ECa2}  \\
  \ded{ECv1}  &:=& \ded{ECv2} \\ \\
  \ded{ECS1}  &:=& \ded{ECS2}  \\ \\
  \end{array}
  $}
  }
  \caption{J-operators: basic derived rules}
  \label{fig:J-ops-basic-derived-rules}
\end{figure}

\bsk

Take a J-equivalence class, $[P]^J$, and list its elements: $[P]^J =
\{P_1, \ldots, P_n\}$. Let $P_∧ := ((P_1∧P_2)∧\ldots)∧P_n$ and $P_∨ :=
((P_1∨P_2)∨\ldots)∨P_n$. Clearly $P_∧ ≤ P_i ≤ P_∨$ for each $i$, so
$[P]^J ⊆ [P_∧,P_∨]$. We will use the interval notation $[P,R]$ to mean
the set of all elements of $H$ obeying $P≤Q≤R$:
%
$$[P,R] \;\; = \;\; \setofst{Q∈H}{P≤Q≤R}.$$

Using $\ECa$ and $\ECv$ several times we see that:
%
$$\begin{array}{rrr}
                 P_1∧P_2 \eqJ P &&                P_1∨P_2 \eqJ P \\
           (P_1∧P_2)∧P_3 \eqJ P &&          (P_1∨P_2)∨P_3 \eqJ P \\
         \vdots\phantom{mmmm}   &&        \vdots\phantom{mmmm}   \\
  ((P_1∧P_2)∧\ldots)∧P_n \eqJ P && ((P_1∨P_2)∨\ldots)∨P_n \eqJ P \\
                     P_∧ \eqJ P &&                    P_∨ \eqJ P \\[5pt]
                    P_∧ ∈ [P]^J &&                   P_∨ ∈ [P]^J \\
  \end{array}
$$
%
and using $\ECS$ we can see that all elements between $P_∧$ and $P_∨$
are $J$-equivalent to $P$:
%:     
%:               P_∧.\eqJ.P   P_∨.\eqJ.P
%:               ----------   ----------
%:               {P_∧}^*=P^*  {P_∨}^*=P^*  
%:                ----------------------  
%:  P_∧≤Q≤P_∨        {P_∧}^*={P_∨}^*        
%:  --------------------------------\ECS
%:        {P_∧}^*=Q^*={P_∨}^*             {P_∨}^*=P^*
%:        -------------------------------------------
%:                  Q^*=P^*
%:                 ---------
%:                 Q.\eqJ.P
%:
%:                  ^foo
%:
$$\pu
  \ded{foo}
$$
%
so $[P_∧,P_∨] ⊆ [P]^J$. This means that {\sl J-regions are intervals}.






% (find-LATEX "2015planar-has.tex" "J-operators")
% (find-planarhaspage 13 "Part 2:" "J-operators and ZQuotients")
% (find-planarhastext 13 "Part 2:" "J-operators and ZQuotients")
% (find-LATEX "2015planar-has.tex" "J-derived-rules")
% (find-planarhaspage 15 "Derived rules")
% (find-planarhastext 15 "Derived rules")




\directlua{tf_pop()}



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