|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% 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: