|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019planar-has-2-logic.tex")
% (find-angg "LATEX/2019elephant-poster.bib")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019planar-has-2-logic.tex" :end))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2019planar-has-2-logic.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019planar-has-2-logic.pdf"))
% (defun e () (interactive) (find-LATEX "2019planar-has-2-logic.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019planar-has-2-logic"))
% (find-xpdfpage "~/LATEX/2019planar-has-2-logic.pdf")
% (find-sh0 "cp -v ~/LATEX/2019planar-has-2-logic.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019planar-has-2-logic.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019planar-has-2-logic.pdf
% file:///tmp/2019planar-has-2-logic.pdf
% file:///tmp/pen/2019planar-has-2-logic.pdf
% http://angg.twu.net/LATEX/2019planar-has-2-logic.pdf
% (find-TH "math-b" "zhas-for-children-2")
% (find-TH "math-b" "zhas-for-children-2" "second paper")
% http://angg.twu.net/math-b.html#zhas-for-children-2
% Moved to:
% (find-LATEX "2019J-ops.tex" "parts")
% «.defs» (to "defs")
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.J-ops-and-regions» (to "J-ops-and-regions")
% «.J-operators» (to "J-operators")
% «.cuts-stopping-midway» (to "cuts-stopping-midway")
% «.no-Y-cuts-no-L-cuts» (to "no-Y-cuts-no-L-cuts")
% «.cubes» (to "cubes")
% «.valuations» (to "valuations")
% «.valuation-cubes» (to "valuation-cubes")
% «.ZHA-vals-good» (to "ZHA-vals-good")
%\documentclass[oneside]{article}
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\usepackage{xcolor} % (find-es "tex" "xcolor")
%\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\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")
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
\input 2017planar-has-defs.tex % (find-angg "LATEX/2017planar-has-defs.tex")
\def\ECa {\mathsf{EC}{∧}}
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «defs» (to ".defs")
\def\eqP{\underset{P}{\sim}}
\def\eqJ{\underset{J}{\sim}}
\def\eqP{\underset{\scriptscriptstyle P}{\sim}}
\def\eqJ{\underset{\scriptscriptstyle J}{\sim}}
\def\eqP{\sim_P}
\def\eqJ{\sim_J}
\def\eqL{\sim_L}
\def\eqR{\sim_R}
\def\eqS{\sim_S}
\def\eqF{\sim_F}
\def\eqQ{\sim_Q}
\def\eqQp{\sim_{Q'}}
\def\ECube{\mathsf{ECube}} \def\ecube{\mathsf{ecube}}
\def\OCube{\mathsf{OCube}} \def\ocube{\mathsf{ocube}}
\def\FCube{\mathsf{FCube}} \def\fcube{\mathsf{fcube}}
\def\SCube{\mathsf{SCube}} \def\fcube{\mathsf{fcube}}
\def\VCube{\mathsf{VCube}} \def\vcube{\mathsf{vcube}}
\def\Exprs{\mathsf{Exprs}}
\def\Thms{\mathsf{Thms}}
\def\thms{\mathsf{thms}}
\def\vthms{\mathsf{vthms}}
\def\NClasses{\mathsf{NClasses}}
\def\nclasses{\mathsf{nclasses}}
\def\ZHAstar{ZHA${}^*$}
\def\sfE{\mathsf{E}}
\def\sfV{\mathsf{V}}
\def\oand{\varowedge}
\def\oor {\varovee}
\def\oimp{\mathbin{\buildoimp{\ominus}{\to}}}
\def\buildoimp#1#2{\rlap{$#1$}\hbox{$#2$}}
\def\zs{{0\ldots7}}
\catcode`¹=13 \def¹{^{*}}
\catcode`²=13 \def²{^{**}}
\catcode`³=13 \def³{^{***}}
% (find-eev "eev-math-glyphs.el" "faces")
% (eev-glyphs-set-face 'eev-glyph-face-math "RoyalBlue2" "gray20")
% (eev-glyphs-set-face 'eev-glyph-face-math2 "DarkOrange" "gray20")
% (eev-glyphs-set-face 'eev-glyph-face-math2 "DarkOrange" "gray25")
% (eev-glyphs-set-face 'eev-glyph-face-math2 "DarkOrchid2" "gray25")
% (eev-glyphs-set-face 'eev-glyph-face-math2 "DarkOrchid2" "DarkOliveGreen")
% (eev-glyphs-set-face 'eev-glyph-face-math2 "DarkOrchid2" "blue4")
% (eepitch-set-glyph0 ?² ?² 'eev-glyph-face-math)
% (eepitch-set-glyph0 ?² ?² 'eev-glyph-face-math2)
% (progn (find-epalette) (ee-goto-position "RoyalBlue2"))
% (find-LATEX "2017planar-has-defs.tex" "defpido")
% ¹²
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
\title{Planar Heyting Algebras for Children $2_L$: Closure Operators, Logic}
\author{Eduardo Ochs}
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% \begin{abstract}
% A {\sl closure operator}, or a {\sl J-operator}, on a Heyting Algebra
% $H$ is an operator $J:H→H$ obeying $P≤P¹=P²$ and $(P∧Q)¹=P¹∧Q¹$, where
% $P¹$ is a shorthand for $J(P)$. Each J-operator induces an equivalence
% relation, with $P \eqJ Q$ iff $P¹=Q¹$; if we write $[P]^J$ for the
% equivalence class of $P$ it is easy to see that $P¹$ is always the
% maximal element of $[P]^J$.
%
% In this paper we use finite, planar HAs --- ``ZHAs'', in the
% terminology of the preceding paper in this series --- to understand
% visually how J-operators and other related operations work.
%
% Our first result is that the the boundaries between J-equivalence
% classes on a ZHA $H$ are diagonal lines without any ``cuts stopping
% midway'', and, conversely, any ``slashing'' of a ZHA by diagonal cuts
% without any cuts stopping midway induces a J-operator; there is a
% correspondence between J-operators on ZHAs and slashings --- and this
% correspondence yields a nice way to visualize the algebra of
% J-operators on a ZHA.
%
% \end{abstract}
% _
% | | ___ _ __ ___
% _ | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
% \___/ \___/| .__/|___/
% |_|
%
% «J-ops-and-regions» (to ".J-ops-and-regions")
% «J-operators» (to ".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")
A {\sl J-operator} on a Heyting Algebra $H = (Ω,≤,⊤,⊥,∧,∨,→,↔,¬)$ is a
function $J:Ω→Ω$ that obeys the axioms $\J1$, $\J2$, $\J3$ below; we
usually write $J$ as $·^*:Ω→Ω$, 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 $Ω$, like slashings do:
%
$$\begin{array}{rcl}
P \eqJ Q &\text{iff}& P^*=Q^* \\[5pt] \relax
[P]^J &:=& \setofst{Q∈Ω}{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_∨]$.
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")
\msk
% As the operation `$·^*$' is increasing and idempotent, each
% equivalence class $[P]^J$ has exactly one maximal element, which is
% $P^*$; but $P_∨$ is also the maximal element of $[P]^J$, so $P_∨ =
% P^*$, and we can interpret the operation `$·*$' as ``take each $P$
% to the top element in its equivalence class'', which is similar to
% how we defined an(other) operation `$·^*$' on slashings in the
% previous section.
% The operation ``take each $P$ to the bottom element in its
% equivalence class'' will be useful in a few occasions; we will call
% it `$·^{\co*}$' to indicate that it is dual to `$·^*$' in some
% sense. Note that $P^{\co*} = P_∧$.
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
% (p2lp 3 "cuts-stopping-midway")
% (p2l "cuts-stopping-midway")
\subsection{Cuts stopping midway}
\label{cuts-stopping-midway}
Look at the figure below, that shows a partition of a ZHA $A=[00,66]$
into five regions, each region being an interval; this partition does
not come from a slashing, as it has cuts that stop midway. Define an
operation `$·^*$' on $A$, that works by taking each truth-value $P$ in
it to the top element of its region; for example, $30^*=61$.
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234567654321")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
\foo
$$
%
It is easy to see that `$·^*$' obeys $\J1$ and $\J2$; however, it does
{\sl not} obey $\J3$ --- we will prove that in
sec.\ref{no-Y-cuts-no-L-cuts}. As we will see, {\sl the partitons of a
ZHA into intervals that obey $\J1$, $\J2$, $\J3$ ae exactly the
slashings;} or, in other words, {\sl every J-operator comes from a
slashing}.
% _ _ __ __ _
% | \ | | ___ \ \ / / ___ _ _| |_ ___
% | \| |/ _ \ \ V / / __| | | | __/ __|
% | |\ | (_) | | | | (__| |_| | |_\__ \
% |_| \_|\___/ |_| \___|\__,_|\__|___/
%
% «no-Y-cuts-no-L-cuts» (to ".no-Y-cuts-no-L-cuts")
% (p2lp 4 "no-Y-cuts-no-L-cuts")
% (p2l "no-Y-cuts-no-L-cuts")
\subsection{The are no Y-cuts and no $\lambda$-cuts}
\label {no-Y-cuts-no-L-cuts}
% Good (ph2p 12 "no-Y-cuts-no-L-cuts")
We want to see that if a partition of a ZHA $H$ into intervals has
``Y-cuts'' or ``$λ$-cuts'', like these parts of the last diagram in
sec.\ref{cuts-stopping-midway},
%
%R local Y, La =
%R 2/ 22 \, 2/ 25 \
%R |21 12| |24 15|
%R \ 11 / \ 14 /
%R
%R Y :tozmp({def="Ycut", scale="10pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
%R La:tozmp({def="Lcut", scale="10pt"}):addcells():addcuts("00w-00n 00e-10n"):output()
$$\pu
\begin{array}{rcl}
\Ycut &\Leftarrow& \text{this is a Y-cut} \\\\
\Lcut &\Leftarrow& \text{this is a $λ$-cut}\\
\end{array}
$$
%
then the operation $J$ that takes each element to the top of its
equivalence class cannot obey $\J1$, $\J2$ and $\J3$ at the same time.
We will prove that by deriving rules that say that if $11 \eqJ 12$
then $21 \eqJ 22$, and that if $15 \eqJ 25$ then $14 \eqJ 24$;
actually, our rules will say that if $11^* = 12^*$ then $(11∨21)^* =
(12∨21)^*$, and that if $15^*=25^*$ then $(15∧24)^*=(25∧24)^*$. The
rules are:
% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%
%: Q¹=R¹
%: ---------
%: P∨Q¹=P∨R¹
%: ---------------
%: Q¹=R¹ (P∨Q¹)¹=(P∨R¹)¹
%: ---------------\NoYcuts := ===============\ostarcube
%: (P∨Q)¹=(P∨R)¹ (P∨Q)¹=(P∨R)¹
%:
%: ^NoYcuts1- ^NoYcuts2-
%:
%: P¹=Q¹
%: ---------
%: P∨R¹=Q∨R¹
%: ---------------
%: P¹=Q¹ (P∨R¹)¹=(Q∨R¹)¹
%: ---------------\NoYcuts := ================\oor_6=\oor_4
%: (P∨R)¹=(Q∨R)¹ (P∨R)¹=(Q∨R)¹
%:
%: ^NoYcuts1 ^NoYcuts2
%:
%:
%: Q¹=R¹
%: ----------
%: Q¹=R¹ P¹∧Q¹=P¹∧R¹
%: ---------------\NoLcuts := ------------\J3
%: (P∧Q)¹=(P∧R)¹ (P∧Q)¹=(P∧R)¹
%:
%: ^NoLcuts1- ^NoLcuts2-
%:
%: P¹=Q¹
%: ----------
%: P¹=Q¹ P¹∧R¹=Q¹∧R¹
%: ---------------\NoLcuts := ------------\J3
%: (P∧R)¹=(Q∧R)¹ (P∧R)¹=(Q∧R)¹
%:
%: ^NoLcuts1 ^NoLcuts2
%:
$$\pu
\begin{array}{rcl}
\ded{NoYcuts1} &:=& \ded{NoYcuts2} \\ \\
\ded{NoLcuts1} &:=& \ded{NoLcuts2} \\ \\
\end{array}
$$
The expansion of double bar labeled `$\oor_6=\oor_4$' in the top
derivation uses twice the derived rule $\oor_6=\oor_4$, that is easy
to prove using the cubes of sec.\ref{cubes}.
% ___ _ _ _
% / _ \| |____ _(_) ___ _ _ ___ ___ _ _| |__ ___ ___
% | | | | '_ \ \ / / |/ _ \| | | / __| / __| | | | '_ \ / _ \/ __|
% | |_| | |_) \ V /| | (_) | |_| \__ \ | (__| |_| | |_) | __/\__ \
% \___/|_.__/ \_/ |_|\___/ \__,_|___/ \___|\__,_|_.__/ \___||___/
%
% «cubes» (to ".cubes")
% (ph2p 13 "obvious-cubes")
% (p2lp 4 "cubes")
% (p2l "cubes")
\subsection{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
\def∧{{\land}}
\def∨{{\lor}}
\def→{{\to}}
%
% \text{(omitted to make compilation faster)}
\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).
% __ __ _ _ _
% \ \ / /_ _| |_ _ __ _| |_(_) ___ _ __ ___
% \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __|
% \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \
% \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/
%
% «valuations» (to ".valuations")
% (p2lp 7 "valuations")
% (p2l "valuations")
\subsection{Valuations}
\label {valuations}
Let $H_\odot$ and $J_\odot$ be a ZHA and a J-operator on it, and let
$v_\odot$ be a function from the set $\{P,Q\}$ to $H$. By an abuse of
language $v_\odot$ will also denote the triple $(H_\odot, J_\odot,
v_\odot)$ --- and by a second abuse of language $v_\odot$ will also
denote the obvious extension of $v_\odot: \{P,Q\}→H$ to the set of all
valid expressions formed from $P$, $Q$, $·^*$, $⊤$, $⊥$, and the
connectives.
Let $i,j∈\{0,\ldots,7\}$. Then $(\oand_i,\oand_j)∈\SCube^*_\land$
means that $\oand_i ≤ \oand_j$ is a theorem, and so $v_\odot(\oand_i)
≤ v_\odot(\oand_j)$ holds; i.e.,
%
$$\SCube^*_\land
⊆ \setofst {(\oand_i,\oand_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oand_i) ≤ v_\odot(\oand_j)}
$$
%
and the same for:
%
$$\begin{array}{c}
\SCube^*_\lor
⊆ \setofst {(\oor_i,\oor_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oor_i) ≤ v_\odot(\oor_j)}
\\
\SCube^*_\to
⊆ \setofst {(\oimp_i,\oimp_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oimp_i) ≤ v_\odot(\oimp_j)}
\\
\end{array}
$$
Some valuations that turn these `$⊆$'s into `$=$'. Let
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321L"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="andCube", scale="11pt"}, "12321"):addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="impCube", scale="11pt"}, "12R1L"):addcuts("c 2/10 01|2")
%L mp:put(v"10", "P") -- :put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q") -- :put(v"02", "Q*", "Q^*")
%L mp:output()
%
\pu
%
$$\begin{array}{c}
(H_∧, J_∧, v_∧) = \andCube
\qquad
(H_∨, J_∨, v_∨) = \orCube \\
(H_→, J_→, v_→) = \impCube \\
\end{array}
$$
%
then
%
$$\begin{array}{c}
\SCube^*_\land
= \setofst {(\oand_i,\oand_j)}
{i,j∈\{0,\ldots,7\}, \; v_∧(\oand_i) ≤ v_∧(\oand_j)}
\\
\SCube^*_\lor
= \setofst {(\oor_i,\oor_j)}
{i,j∈\{0,\ldots,7\}, \; v_∨(\oor_i) ≤ v_∨(\oor_j)}
\\
\SCube^*_\to
= \setofst {(\oimp_i,\oimp_j)}
{i,j∈\{0,\ldots,7\}, \; v_→(\oimp_i) ≤ v_→(\oimp_j)}
\\
\end{array}
$$
%
or, in more elementary terms:
\newpage
{\sl A very important fact.}
For any $i$ and $j$,
%
$$\pu
\begin{array}{rcl}
\oand_i≤\oand_j & \text{ is a theorem iff it is true in } & \andCube \;\; , \\
\\
\oor_i≤\oor_j & \text{ is a theorem iff it is true in } & \orCube \;\; , \\
\\
\oimp_i≤\oimp_j & \text{ is a theorem iff it is true in } & \impCube \;\; . \\
\end{array}
$$
The very important fact, and the valuations $v_∧$, $v_∨$, $v_→$, give
us:
\begin{itemize}
\item a way to {\sl remember} which sentences of the forms
$\oand_i≤\oand_j$, $\oor_i≤\oor_j$, $\oimp_i≤\oimp_j$ are theorems;
\item countermodels for all the sentences of these forms not in
$\SCube_∧$, $\SCube_∨$, $\SCube_→$. For example, $\oor_7≤\oor_4$ is
not in $\SCube_∨$; and $v_∨(\oor_7)≤v_∨(\oor_4)$, which shows that
$\oor_7≤\oor_4$ can't be a theorem.
\end{itemize}
% (find-books "__cats/__cats.el" "bell")
% (find-books "__cats/__cats.el" "bell" "163")
{\sl An observation.} I arrived at the cubes $\ECube_∧^*$,
$\ECube_∨^*$, $\ECube_→^*$ by taking the material in the corollary 5.3
of chapter 5 in \cite{BellLST} and trying to make it fit into less
mental space (as discussed in \cite{OchsIDARCT}); after that I wanted
to be sure that each arrow that is not in the extended cubes has a
countermodel, and I found the countermodels one by one; then I
wondered if I could find a single countermodel for all non-theorems in
$\ECube_∧^*$ (and the same for $\ECube_∨^*$ and $\ECube_→^*$), and I
tried to start with a valuation that distinguished {\sl some}
equivalence classes in $\ECube_∧^*$, and change it bit by bit, getting
valuations that distinguished more equivalence classes at every step.
Eventually I arrived at $v_∧$, $v_∨$ and at $v_→$, and at the ---
surprisingly nice --- ``very important fact'' above.
% (ph2p 20 "ZHA-vals-good")
% (ph2 "ZHA-vals-good")
Note that this valuation
%
%L mp = mpnew({def="orand", scale="11pt"}, "1234321L"):addcuts("c 432/10 01|23")
%L mp:put(v"20", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"13", "Q*", "Q^*")
%L mp:output()
%
$$(H_{∧∨},J_{∧∨},v_{∧∨}) \;\; = \;\; \pu\orand$$
%
distinguishes all equivalence classes in $\ECube^*_∧$ and in
$\ECube^*_∨$, but not in $\ECube^*_→$... it ``thinks'' that $P→Q$ and
$P^*→Q$ are equal.
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "p2l"
% End: