|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This file: (find-angg "LATEX/2017planar-has-2.tex")
% (find-angg "LATEX/2017planar-has-defs.tex")
% Newer version: (find-LATEX "2021planar-HAs-2.tex")
%
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has-2.tex"))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2017planar-has-2.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2017planar-has-2.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2017planar-has-2; makeindex 2017planar-has-2"))
% (defun e () (interactive) (find-LATEX "2017planar-has-2.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017planar-has-2"))
% (find-xpdfpage "~/LATEX/2017planar-has-2.pdf")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-2.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-2.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017planar-has-2.pdf
% file:///tmp/2017planar-has-2.pdf
% file:///tmp/pen/2017planar-has-2.pdf
% http://angg.twu.net/LATEX/2017planar-has-2.pdf
% «.picturedots» (to "picturedots")
% «.title» (to "title")
% «.abstract» (to "abstract")
%
% «.introduction» (to "introduction")
% «.piccs-and-slashings» (to "piccs-and-slashings")
% «.slash-partitions» (to "slash-partitions")
% «.slash-max» (to "slash-max")
% «.cuts-stopping-midway» (to "cuts-stopping-midway")
% «.slash-ops» (to "slash-ops")
% «.slash-ops-property» (to "slash-ops-property")
%
% «.J-ops-and-regions» (to "J-ops-and-regions")
% «.no-Y-cuts-no-L-cuts» (to "no-Y-cuts-no-L-cuts")
% «.obvious-cubes» (to "obvious-cubes")
% «.full-cubes» (to "full-cubes")
% «.valuation-cubes» (to "valuation-cubes")
% «.ZHA-vals-good» (to "ZHA-vals-good")
%
% «.question-marks» (to "question-marks")
% «.Q-partitions-are-slash-partitions» (to "Q-partitions-are-slash-partitions")
% «.Q-open-sets» (to "Q-open-sets")
% «.Q-open-sets-propagations» (to "Q-open-sets-propagations")
% «.rectangular» (to "rectangular")
% «.rectangular-theorems» (to "rectangular-theorems")
%
% «.polynomial-J-ops» (to "polynomial-J-ops")
% «.algebra-of-piccs» (to "algebra-of-piccs")
% «.algebra-of-J-ops» (to "algebra-of-J-ops")
% «.slashings-are-poly» (to "slashings-are-poly")
%
% «.rectangular-question-marks» (to "rectangular-question-marks")
%
% «.open-sets-of-a-certain-form» (to "open-sets-of-a-certain-form")
% «.propagation» (to "propagation")
% «.relevant-points» (to "relevant-points")
% «.rectangular-versions» (to "rectangular-versions")
% «.extremities» (to "extremities")
% «.J-and-coJ-in-three-steps» (to "J-and-coJ-in-three-steps")
% «.sub-2CGs» (to "sub-2CGs")
% «.J-ops-as-adjunctions» (to "J-ops-as-adjunctions")
%
% «.bibliography» (to "bibliography")
\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\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-angg "LATEX/edrx15.sty")
\input edrxaccents.tex % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% \catcode`\^^J=10
% \directlua{dednat6dir = "dednat6/"}
% \directlua{dofile(dednat6dir.."dednat6.lua")}
% \directlua{texfile(tex.jobname)}
% \directlua{verbose()}
% \directlua{output(preamble1)}
% \def\expr#1{\directlua{output(tostring(#1))}}
% \def\eval#1{\directlua{#1}}
% \def\pu{\directlua{pu()}}
\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
\input 2017planar-has-defs.tex % (find-angg "LATEX/2017planar-has-defs.tex")
%L tcg_big = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2}
%L tcg_med = {scale= "8pt", meta="p s", dv=1, dh=2, ev=0.32, eh=0.25}
%L tcgnew = function (opts, def, str)
%L return TCG.new(opts, def, unpack(split(str, "[ %d]+")))
%L end
%L tcgbig = function (def, spec) return tcgnew(tcg_big, def, spec or tcg_spec) end
%L tcgmed = function (def, spec) return tcgnew(tcg_med, def, spec or tcg_spec) end
%L
%L tcg_bigq = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2, dq=1.4}
%L tcg_medq = {scale= "8pt", meta="p s", dv=1, dh=2, ev=0.32, eh=0.25, dq=1.4}
%L tcg_Medq = {scale="10pt", meta="p", dv=1, dh=3, ev=0.32, eh=0.25, dq=1.4}
%L
%L tcgbigq = function (def, spec) return tcgnew(tcg_bigq, def, spec or tcg_spec) end
%L tcgmedq = function (def, spec) return tcgnew(tcg_medq, def, spec or tcg_spec) end
%L tcgMedq = function (def, spec) return tcgnew(tcg_Medq, def, spec or tcg_spec) end
%L -- (find-dn6 "zhas.lua" "TCG")
%L -- (find-dn6 "zhas.lua" "TCG" "lrs =")
%L
%L TCG.__index.QL = function (tcg, y) return v(0 -tcg.lp.dq, tcg.dv*y) end
%L TCG.__index.QR = function (tcg, y) return v(tcg.dh+tcg.lp.dq, tcg.dv*y) end
%L TCG.__index.putql = function (tcg, y, str) tcg.lp:put(tcg:QL(y), str) end
%L TCG.__index.putqr = function (tcg, y, str) tcg.lp:put(tcg:QR(y), str) end
%L TCG.__index.qmarks = function (tcg, lstr, rstr)
%L for y=1,tcg.l do tcg:putql(y, lstr:sub(y, y)) end
%L for y=1,tcg.r do tcg:putqr(y, rstr:sub(y, y)) end
%L return tcg
%L end
\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\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\OPENS{\operatorname{\mathsf{Opens}}}
\def\OPENSPABD{\OPENS(\Opens_A(P),B,D)}
\def\OPENSPABD{\OPENS((P,A),B,D)}
\def\relevant {\operatorname{\mathsf{relev}}}
\def\qmarks {\operatorname{\mathsf{qmarks}}}
\def\forget {\operatorname{\mathsf{forget}}}
\def\propagate{\operatorname{\mathsf{prpgt}}}
\def\propagate{\operatorname{\mathsf{prp}}}
\def\biggest{\mathsf{biggest}}
\def\ess{\mathsf{ess}}
\def\obeys{\mathsf{obeys}}
\def\isoftheform{\operatorname{\mathsf{is\ of\ the\ form}}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
\title{Planar Heyting Algebras for Children 2: Closure Operators}
\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.
Our second result is that there is a correspondence between slashings
and ``sets of question marks'', in the following sense. In the
previous paper we showed that every ZHA $H$ ``is'' the set of open
sets, in the order topology, of a two-column graph $(P,A)$, and we
showed a way to interpret truth-values $Q,R∈H$ as open sets $Q',R'⊆P$.
Any way to express $P$ as a disjoint union $P_!∪P_?$ yields an
equivalence relation on $H$, in which $Q∼R$ iff $Q'∖P_? = R'∖P_?$;
i.e., $Q$ and $R$ are equivalent iff they are equal when we erase the
information on $P_?$.
Our third result is about ways to reconstruct the missing information
on the points of $P_?$ after the erasal. There are two natural ways to
do this reconstruction; one is by taking the biggest possible choice,
and another is by taking the smallest possible one. It turns out that
these two ways are respectively the right adjoint and the left adjoint
to erasing,
%
$$\def\te#1{\text{(#1)}}
\te{smallest choice} ⊣ \te{erasing} ⊣ \te{biggest choice}
$$
%
and that the J-operator $J$ is essentially the unit of the second
adjunction. Also, When we draw the categorical diagrams for these
adjunctions we get some of the basic diagrams for understanding
sheaves on a topos, but in a ``miniature case'' --- the full case will
be discussed on the next paper in this series.
\end{abstract}
% (find-kopkadaly4page (+ 12 58) "3.4 Table of contents")
\tableofcontents
\maketitle
% This paper shows a way to interpret (propositional) intuitionistic
% logic {\sl visually} using finite Planar Heyting Algebras (``ZHAs''),
% that are certain subsets of $\Z^2$. The ``for children'' of the title
% means ``for people without mathematical maturity'', i.e., for people
% who are not able to understand structures that are too abstract
% straight away, they need particular cases first; everything in the
% paper is constructive and easy to visualize using finite diagrams.
%
% We also show the connection between ZHAs and the familiar semantics
% for IPL where the truth-values are open sets in a finite topological
% space $(P,\Opens(P))$, and we show how each closure operator $J:H→H$
% on a ZHA $H⊆\Z^2$ corresponds to a) a way to ``slash'' $H$ using
% diagonal cuts, and b) a choice of a subset $S⊆P$; $J$ can be recovered
% from $S$ as a restriction map $\Opens(P)→\Opens(S)$ followed by a map
% $\Opens(S)→\Opens(P)$ that reconstructs the missing information ``in
% the biggest way possible''.
%
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
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.
\msk
Our first result is that on a ZHA $H$ the boundaries between
J-equivalence classes are diagonal lines without any ``cuts stopping
midway'', and, conversely, any ``slashing'' of a $H$ by diagonal cuts
without any cuts stopping midway induces a J-operator. Slashings are
easy to visualize, so this yields a way to visualize J-operators (on
ZHAs).
This first result will be explained in three parts. In sections
\ref{piccs-and-slashings} to \ref{slash-ops-property} we define
slashings, slash-operators, slash-regions, slash-partitions, cuts and
cuts stopping midway; in sections \ref{J-ops-and-regions} to
\ref{no-Y-cuts-no-L-cuts} we define J-operators, J-regions,
J-partitions, partitions into ``intervals'', and we show that very
J-partition on a ZHA $H$ is a partition of $H$ into intervals without
cuts stopping midway; in sections \ref{obvious-cubes} to
\ref{ZHA-vals-good} we show a way to visualize how J-operators
interact with the connectives, and prove a lemma pending from
sec.\ref{no-Y-cuts-no-L-cuts}. As a bonus, in sections
\ref{polynomial-J-ops} to \ref{slashings-are-poly} we show how to
visualize the algebra of slash-operators, and we prove that all
slash-operators are polynomial.
% ; this yields a
% nice way to visualize J-operators.
%
% Our first result is that on ZHAs there is a correspondence between
% J-operators and ``slashings'', in the following sense: the boundaries
% between J-equivalence classes on a ZHA $H$ are diagonal lines without
% any ``cuts stopping midway'', and any slashing on $H$ ``cuts'' $H$
% into equivalence classes in a way that induces a J-operator; a set of
% slash-equivalence classes is a set of J-equivalence classes, and
% vice-versa.
%
%
% 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. This will be done in three parts: in sections
% \ref{piccs-and-slashings} to \ref{slash-ops-property} we define
% slashings, slash-operators, slash-regions, cuts and cuts stopping
% midway;
%
% \ref{no-Y-cuts-no-L-cuts}
Our second result, proved in sections \ref{question-marks} and
\ref{Q-partitions-are-slash-partitions}, is that there is a
correspondence between slashings and ``sets of question marks'', in
the following sense. In the previous paper we showed that every ZHA
$H$ ``is'' the set of open sets, in the order topology, of a
two-column graph $(P,A)$, and we showed a way to interpret
truth-values $Q,R∈H$ as open sets $Q',R'⊆P$. Any way to express $P$ as
a disjoint union $P_!∪P_?$ yields an equivalence relation on $H$, in
which $Q∼R$ iff $Q'∖P_? = R'∖P_?$; i.e., $Q$ and $R$ are equivalent
iff they are equal when we erase the information on $P_?$.
Our third result, in sections \ref{Q-open-sets} to
\ref{rectangular-theorems}, is about ways to reconstruct the missing
information on the points of $P_?$ after the erasal. There are two
natural ways to do this reconstruction; one is by taking the biggest
possible choice, and another is by taking the smallest possible one.
It turns out that these two ways are respectively the right adjoint
and the left adjoint to erasing,
%
$$\def\te#1{\text{(#1)}}
\te{smallest choice} ⊣ \te{erasing} ⊣ \te{biggest choice}
$$
%
and that the J-operator $J$ is essentially the unit of the second
adjunction. Also, When we draw the categorical diagrams for these
adjunctions we get some of the basic diagrams for understanding
sheaves on a topos, but in a ``miniature case'' --- the full case will
be discussed on the next paper in this series.
% ____ _
% | _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% | __/| | (_| (__\__ \
% |_| |_|\___\___|___/
%
% «piccs-and-slashings» (to ".piccs-and-slashings")
% (ph2p 4 "piccs-and-slashings")
% (ph2 "piccs-and-slashings")
\section{Piccs and slashings}
\label {piccs-and-slashings}
% Good (ph2p 2 "piccs-and-slashings")
\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}
A picc (``partition into contiguous classes'') of an interval
$I=\{0,\ldots,n\}$ is a partition $P$ of $I$ that obeys this
condition (``picc-ness''):
%
$$∀a,b,c∈\{0,\ldots,n\}.\; (a<b<c \;\;\&\;\; a \eqP c) → (a \eqP b \eqP c).$$
%
So $P = \{\{0\},\{1,2,3\},\{4,5\}\}$ is a picc of $\{0,\ldots,5\}$,
and $P' = \{\{0\},\{1,2,4,5\},\{3\}\}$ is a partition of
$\{0,\ldots,5\}$ that is not a picc.
A short notation for piccs is this:
%
$$0|123|45 \equiv \{\{0\},\{1,2,3\},\{4,5\}\}$$
%
we list all digits in the ``interval'' in order, and we put bars to
indicate where we change from one equivalence class to another.
\msk
Let's define a notation for ``intervals'' in $\LR$,
%
$$[ab,ef]
:=
[\ang{a,b},\ang{e,f}]
:=
\setofst {\ang{c,d}∈\LR} {a≤c≤e \;\;\&\;\; b≤d≤f},
$$
%
Note that it can be adapted to define ``intervals'' in a ZHAs $H$:
%
$$\begin{array}{rcl}
[ab,ef]∩H & := & \setofst {\ang{c,d}∈\LR} {a≤c≤e \;\;\&\;\; b≤d≤f}∩H \\
& = & \setofst {\ang{c,d}∈H} {a≤c≤e \;\;\&\;\; b≤d≤f}. \\
\end{array}
$$
A {\sl slashing} $S$ on a ZHA $H$ with top element $ab$ is a pair of
piccs, $S=(L,R)$, where $L$ is a picc on $\{0,\ldots,a\}$ and $R$ is a
picc on $\{0,\ldots,b\}$; for example, $S=(4321/0,\, 0123∖45∖6)$
is a slashing on $[00,46]$. We write the bars in $L$ as `$/$'s and the
bars in $R$ as `$∖$' as a reminder that they are to be interpreted
as northeast and northwest ``cuts'' respectively; $S=(4321/0,\,
0123∖45∖6)$ is interpreted as the diagram at the left below, and
it ``slashes'' $[00,46]$ and the ZHA at the right below as:
%
%L -- local putl, putr, cutl, cutr
%L -- mp = MixedPicture.new {scale="7pt", def="foo"}
%L -- putl = function (n) mp:put(v((n+1).."0"), n.."", n.."") end
%L -- putr = function (n) mp:put(v("0"..(n+1)), n.."", n.."") end
%L -- cutl = function (n) mp:addcuts(format("%d0w-%d0n", n+1, n+1)) end
%L -- cutr = function (n) mp:addcuts(format("0%dn-0%de", n+1, n+1)) end
%L -- putl(0); putl(1); putl(2); putl(3); putl(4)
%L -- putr(0); putr(1); putr(2); putr(3); putr(4); putr(5); putr(6)
%L -- cutl(0)
%L -- cutr(3); cutr(5)
%L -- mp:print():output()
%L
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="foo"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
% / \
% 46
% / \ \
% 45 36
% \ \ \
% 35 26
% / \ /
% 34 25
% \ /
% 24
% / \ \
% 23 14
% / \ / \
% 22 13 04
% \ / \ /
% 12 03
% / / /
% 11 02
% \ / /
% 01
% / /
% 00
% 4321/0 \ / 0123\45\6
%
$$\pu
\foo
\qquad
\ZQuot
\qquad
\ZQuotients
$$
A slashing $S=(L,R)$ on a ZHA $H$ with top element $ab$ induces an
equivalence relation `$\eqS$' on $H$ that works like this: $\ang{c,d}
\eqS \ang{e,f}$ iff $c \eqL e$ and $d \eqR f$. We write
%
$$\begin{array}{rcl}
[c]_L &:=& \setofst {e∈\{0,\ldots,a\}} {c \eqL a} \\ \relax
[d]_R &:=& \setofst {f∈\{0,\ldots,b\}} {d \eqL f} \\ \relax
[cd]_S &:=& \setofst {ef∈H} {cd \eqS ef} \\
\end{array}
$$
%
for the equivalence classes, and note that
%
% (find-planarhas "zquotients")
% (find-planarhaspage 26 "ZQuotients")
% (find-planarhastext 26 "ZQuotients")
%
$$\begin{array}{lrcl}
\text{if} & [c]_L &=& \{c',\ldots,c''\} \\
\text{and} & [d]_L &=& \{d',\ldots,d''\} \\
\text{then} & [cd]_S &=& [c'd',c''d'']∩H; \\
\end{array}
$$
%
for example, in the ZHA at the right at the example above we have:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
[12]_S &=& [10,43]∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
We say that a slashing $S$ on a ZHA $H$ partitions $H$ into {\sl
slash-regions}; later (sec.\ref{J-ops-and-regions}) we will see that
a J-operator $J$ also partitions $H$, and we will refer to its
equivalence classes as {\sl J-regions}.
Slash-regions are intervals, but note that neither 10 or 43 belong to
the slash-region $[12]_S = [10,43]∩H$ above.
\msk
A {\sl slash-partition} is a partition on a ZHA induced by a slashing,
and a {\sl slash-equivalence} is an equivalence relation on a ZHA
induced by a slashing. Formally, a slash-partition on $H$ is a set of
subsets of $H$, and a slash-equivalence is subset of $H×H$, but it is
so easy to convert between partitions and equivalence relations that
we will often use both terms interchangeably. Our visual
representation for slash-partitions and slash-equivalences on a ZHA
$H$ will be the same: $H$ slashed by diagonal cuts.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ __ _ _ __| |_
% \___ \| |/ _` / __| '_ \ _____| '_ \ / _` | '__| __|
% ___) | | (_| \__ \ | | |_____| |_) | (_| | | | |_
% |____/|_|\__,_|___/_| |_| | .__/ \__,_|_| \__|
% |_|
% «slash-partitions» (to ".slash-partitions")
\section{From slash-partitions back to slashings}
\label {slash-partitions}
% Good (ph2p 4 "slash-partitions")
We saw how to go from a slashing $S=(L,R)$ on $H$ to an equivalence
relation $\eqS$ on $H$; let's see now how to recover $L$ and $R$ from
$\eqS$.
% Let's see a way to recover the piccs $L$ and $R$ from an equivalence
% relation $\eqS$ on a ZHA $H$.
Let $LW_H$ be the left wall of $H$, and $RW_H$ the right wall of $H$.
For example,
%
%L -- mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():output()
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
H = \;\;\foo
\quad
\begin{array}[t]{r}
LW_H = \{00,01,11,12,22,23,24,34,35,45,46\} \\
RW_H = \{00,01,02,03,04,14,24,25,26,36,46\} \\
\end{array}
$$
To recover the picc $L$ --- which is a picc on $\{0,1,2,3,4\}$ --- we
need to find where we change from an $L$-equivalence class to another
when we go from one digit to the next; and to recover the picc $R$ ---
which is a picc on $\{0,1,2,3,4,5,6\}$ --- we need to find where we
change from an $R$-equivalence class to another when we go from one
digit to the next.
We can recover $L$ and $R$ by walking $LW_H$ (or $RW_H$) from bottom
to top in a series of white pawns moves, and checking when we change
from one $S$-equivalence class to another. Northwest moves give
information about $L$, and northeast moves give information about $R$.
Look at the example below, in which we walk on $RW_H$:
%
\def\nem#1#2{\psm{ &\!#2\\ #1& \\}}
\def\nwm#1#2{\psm{ #2& \\ &\!#1\\}}
\def\nem#1#2{\sm{ &&\!#2\\ &\!\nearrow&\\ #1& \\}}
\def\nwm#1#2{\sm{ #2&\\&\!\nwarrow&\\ &&\!#1\\}}
\def\neyes#1#2#3#4{\nem{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #2 { \eqR} #4 \;⇒\; #2 #4 }
\def\neno #1#2#3#4{\nem{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #2 {\not\eqR} #4 \;⇒\; #2∖#4 }
\def\nwyes#1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #1 { \eqL} #3 \;⇒\; #3 #1 }
\def\nwno #1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #1 {\not\eqL} #3 \;⇒\; #3/#1 }
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="LWH"}, "1RLRLRRLRLR"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="RWH"}, "1RRRRLLRRLL"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
\begin{array}{c}
H = \;\;\foo
\qquad
LW_H = \;\;\LWH
\quad
RW_H = \!\!\!\!\!\!\!\!\RWH
%
\\ \\
%
\begin{array}{ll}
& \neno 25 26 \\
& \neyes 24 25 \\
\nwyes 36 46 & \neno 03 04 \\
\nwyes 26 36 & \neyes 02 03 \\
\nwyes 14 24 & \neyes 01 02 \\
\nwno 04 14 & \neyes 00 01 \\
\end{array}
%
\\ \\
%
% ⇒ \quad
(L,R) \;=\; (4321/0, 0123∖45∖6)
\end{array}
$$
% ____ _ _
% / ___|| | __ _ ___| |__ _ __ ___ __ ___ __
% \___ \| |/ _` / __| '_ \ _____| '_ ` _ \ / _` \ \/ /
% ___) | | (_| \__ \ | | |_____| | | | | | (_| |> <
% |____/|_|\__,_|___/_| |_| |_| |_| |_|\__,_/_/\_\
%
% «slash-max» (to ".slash-max")
\section{Slash-regions have maximal elements}
\label {slash-max}
% Good (ph2p 5 "slash-max")
...here is how our argument will work, in a particular case:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
I &=& [10,43], \\ \relax
[12]_S &=& I∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
$$\def\uoo#1#2{ \und{#1}{oo:#2} }
\def\uo #1#2{(\und{#1}{oo:#2})}
%
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈I}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
\qquad
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈H}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
$$
$$\bigvee [12]_S
= \bigvee \{11,12,13,22,23\}
= 11∨12∨13∨22∨23
∈ I∩H
$$
$$11 ≤ \bigvee [12]_S, \;
12 ≤ \bigvee [12]_S, \;
\ldots, \;
23 ≤ \bigvee [12]_S
$$
We have $[12]_S = I∩H$, and $\bigvee [12]_S$ belongs to $I∩H$ and is
greter-or-equal than all elements of $I∩H$, so $\bigvee [12]_S$ is the
maximal element of $[12]_S$.
\bsk
Here is how we can do that in the general case. Let $S=(L,R)$ be a
slashing on a ZHA $H$. Let $P$ be a point of $H$. The equivalence
class $[P]_S$ is a finite set $\{P_1, \ldots, P_n\}$, and we know that
$[P]_S=H∩I$ for some interval $I$. Look at the elements $P_1$,
$P_1∨P_2$, $(P_1∨P_2)∨P_3$, $\ldots$, $((P_1∨P_2)∨\ldots)∨P_n$ We can
see that all of them belong to both $H$ and $I$, so we conclude that
$\bigvee [P]_S = ((P_1∨P_2)∨\ldots)∨P_n$ belongs to $H∩I$, and it is
easy to see that it is greater-or-equal that all elements in $H∩I$, so
it is the maximal element of $H∩I$.
A similar argument shows that $\bigwedge [P]_S =
((P_1∧P_2)∧\ldots)∧P_n$ is the smallest element of $[P]_S$.
\msk
The same argument shows that if $C$ is any non-empty set of the form
$I∩H$, where $I$ is an interval, then $\bigvee C ∈ C$, $\bigwedge C ∈
C$, $[\bigwedge C, \bigvee C]∩H = C$.
Remember that an {\sl interval} in a ZHA $H$ is any set of the form
$[P,Q]∩H$. Let's introduce a new definition: a {\sl closed interval}
in a ZHA $H$ is a non-empty set $C⊂H$, with $⋁C∈C$, $⋀C∈C$, $[⋀C,
⋁C]∩H = C$; informally, a closed interval in a ZHA has a lowest and
highest element, and it ``is'' everything between them.
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
\section{Cuts stopping midway}
\label {cuts-stopping-midway}
% Good (ph2p 6 "cuts-stopping-midway")
We saw in the last section that every slash-region is a closed
interval. A {\sl partition into closed intervals} of a ZHA $H$ is, as
its name says, a partition of $H$ whose equivalence classes are all
closed intervals in $H$.
Some partitions into closed intervals of a ZHA are not slashings ---
for example, take the partition $P$ with these equivalence classes:
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234LL321")
%L -- mp:addlrs():addcuts("c 01|23 10w-11n 32w-33n"):output()
%L mp:addlrs():addcuts("c 01|23 20w-21n 32w-33n"):output()
$$\pu
\foo
$$
Here is an easy way to prove formally that the partition above does
not come from a slashing $S=(L,R)$. We will adapt the idea from
sec.\ref{slash-partitions}, where we recovered $L$ and $R$ from
northwest and northeast steps.
%
\def\undtrue #1{\und{#1}{\text{true}}}
\def\undfalse#1{\und{#1}{\text{false}}}
\def\undfrown#1{\und{#1}{=(}}
\def\iff{\;\;↔\;\;}
\def\notiff{\;\not↔\;}
%
$$\begin{array}{rcl}
\undfalse{21 \eqP 31} \;\;↔\;\; \undfrown{2 \eqL 3} \;\;↔\;\; \undtrue {22 \eqP 32} \\
\undtrue {31 \eqP 41} \;\;↔\;\; \undfrown{3 \eqL 4} \;\;↔\;\; \undfalse{32 \eqP 42} \\
\end{array}
$$
The problem is that the figure above has ``cuts stopping midway''...
if its cuts all crossed the ZHA all the way through, we would have
this for $L$ and northeast cuts,
%
$$\begin{array}{c}
0\eqL1 \iff 00\eqP10 \iff 01\eqP11 \iff 02\eqP12 \iff 03\eqP13 \\
1\eqL2 \iff 10\eqP20 \iff 11\eqP21 \iff 12\eqP22 \iff 13\eqP23 \\
2\eqL3 \iff 20\eqP30 \iff 21\eqP31 \iff 22\eqP32 \iff 23\eqP33 \\
3\eqL4 \iff 30\eqP40 \iff 31\eqP41 \iff 32\eqP42 \iff 33\eqP43 \\
4\eqL5 \iff 40\eqP50 \iff 41\eqP51 \iff 42\eqP52 \iff 43\eqP53 \\
5\eqL6 \iff 50\eqP60 \iff 51\eqP61 \iff 52\eqP62 \iff 53\eqP63 \\
\end{array}
$$
%
and something similar for $R$ and northwest cuts.
\msk
Formally, a partition $P$ on $H$ has an ``L-cut between $c$ and $c^+$
stopping midway'' if $cd \eqP c^+d \notiff cd \eqP c^+d$ for some $d$,
and it has an ``R-cut between $d$ and $d^+$ stopping midway'' if $cd
\eqP cd^+ \notiff c^+d \eqP c^+d^+$ for some $c$; here we are writing
$x^+$ for $x+1$.
\msk
{\sl Theorem: a partition of $H$ into closed intervals is a
slash-partition if and only if it doesn't have any cuts stopping
midway.} Proof: use the ideas above to recover $L$ and $R$ from
$\eqP$, and then check that $S=(L,R)$ induces an equivalence relation
$\eqS$ that coincides with $\eqP$.
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
% «slash-ops» (to ".slash-ops")
\section{Slash-operators}
\label {slash-ops}
% Good (ph2p 7 "slash-ops")
We can define operations that take each each $P∈H$ to the maximal and
to the minimal element of its $S$-equivalent class, now that we know
that these maximal and minimal elements exist:
%
$$\begin{array}{rclll}
P^S &:=& \bigvee [P]_S && \text{(maximal element),} \\
P^{\co S} &:=& \bigwedge [P]_S && \text{(minimal element).}
\end{array}
$$
Note that $[P]_S = [P^{\co S}, P^S]∩H$.
We will use the operation $·^S$ a lot and $·^{\co S}$ very little. The
`$\co$' in `$\co S$' means that $·^{\co S}$ is dual to $·^S$, in a
sense that will be made precise later.
\msk
A {\sl slash-operator} on a ZHA $H$ is a function $·^S:H→H$ induced by
a slashing $S=(L,R)$ on $H$. It is easy to see that $P ≤ P^S$
(``\,$·^S$ is non-decreasing'') and that $P^S = (P^S)^S$ (``\,$·^S$ is
idempotent'').
\msk
Any idempotent function $·^F:H→H$ induces an equivalence relation on
$H$: $P \eqF Q$ iff $P^F = Q^F$. We can use that to test if a given
$·^F:H→H$ is a slash-operator: $·^F$ is a slash-operator iff it obeys
all this:
1) $·^F$ is idempotent,
2) $·^F$ is non-decreasing,
3) $\eqF$ partitions $H$ into closed intervals,
4) $\eqF$ doesn't have cuts stopping midway.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ _ __ ___ _ __ ___ _ __| |_ _ _
% \___ \| |/ _` / __| '_ \ | '_ \| '__/ _ \| '_ \ / _ \ '__| __| | | |
% ___) | | (_| \__ \ | | | | |_) | | | (_) | |_) | __/ | | |_| |_| |
% |____/|_|\__,_|___/_| |_| | .__/|_| \___/| .__/ \___|_| \__|\__, |
% |_| |_| |___/
%
% «slash-ops-property» (to ".slash-ops-property")
\section{Slash-operators: a property}
\label {slash-ops-property}
% Good (ph2p 8 "slash-ops-property")
Slash-operators obey a certain property that will be very important
later. Let's state that property in five equivalent ways:
1) If $cd \eqS c'd'$ and $ef \eqS e'f'$ then $cd∧ef \eqS c'd'∧e'f'$.
2) If $P \eqS P'$ and $Q \eqS Q'$ then $P∧Q \eqS P'∧Q'$.
3) If $P \eqS P'$ and $Q \eqS Q'$ then $(P∧Q)^S = (P'∧Q')^S$.
4) If $P \eqS P'$ and $Q \eqS Q'$ then
%
$$\begin{array}{rclll}
(P∧Q)^S &=& (P^S∧Q^S)^S && \text{(a)} \\
&=& ((P')^S∧(Q')^S)^S && \text{(b)} \\
&=& (P'∧Q')^S && \text{(c)} \\
\end{array}
$$
5) $(P∧Q)^S = (P^S∧Q^S)^S$.
\msk
\noindent Here's a proof of $1↔2↔3↔4↔5$.
$1↔2$: we just changed notation,
$2↔3$: because $A \eqS B$ iff $A^S = B^S$,
$3→5$: make the substitution $\subst{P':=P^S \\ Q':=Q^S}$ in 3,
$5→4$: 4a is just a copy of 5, and 4c is a copy of 5 with
$\subst{P:=P' \\ Q:=Q'}$. For 4b, note that $P \eqP P'$ implies $P^S =
(P')^S$ and $Q \eqP Q'$ implies $Q^S = (Q')^S$,
$4→3$: 4 is an equality between more expressions than 3,
\msk
\noindent ...and here is a way to visualize what is going on:
%
% (find-planarhas "J-figure")
% (find-planarhaspage 19 "How J-operators interact with the connectives: figure")
% (find-planarhastext 19 "How J-operators interact with the connectives: figure")
%
%L -- The (&*) cube
%L mp = mpnew({def="andcube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3"):addlrs():output()
%L mp = mpnew({def="andCube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3")
%L mp:put(v"30", "P"):put(v"31", "P'", "P'"):put(v"32", "P*", "P^S")
%L mp:put(v"03", "Q"):put(v"13", "Q'", "Q'"):put(v"23", "Q*", "Q^S")
%L mp:output()
%
$$\pu
\begin{array}{c}
\andcube
\qquad
\andCube
\\ \\
\und{( \und{ \und{P}{30} ∧ \und{Q}{03} }{00} )^S}{22} =
\und{( \und{ \und{\und{P }{30}{}^S}{32} ∧ \und{\und{Q }{03}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{\und{P'}{31}{}^S}{32} ∧ \und{\und{Q'}{13}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{P'}{31} ∧ \und{Q'}{13} }{11} )^S}{22}
\\
\end{array}
$$
%
Note that all subexpressions belong to three $S$-regions: a region
with $P$, $P'$, $P^S=P'{}^S$, another with $Q$, $Q'$, $Q^S=Q'{}^S$,
and one with all the `$∧$'s. If we had cuts stopping midway then some
of the `$∧$'s could be in different regions.
I think that the clearest way to show (1) is by putting its proof in
tree form:
%
%L addabbrevs("(~S)", "\\eqS ", "(~L)", "\\eqL ", "(~R)", "\\eqR ")
%:
%: cd(~S)c'd' ef(~S)e'f' cd(~S)c'd' ef(~S)e'f'
%: ---------- ---------- ---------- ----------
%: c(~L)c' e(~L)e' d(~R)d' f(~R)f'
%: ------------------------ ------------------------
%: \min(c,e)(~L)\min(c',e') \min(d,f)(~L)\min(d',f')
%: ----------------------------------------------------
%: \min(c,e)\min(d,f)(~S)\min(c',e')\min(d',f')
%: --------------------------------------------
%: cd∧ef(~S)c'd'∧e'f'
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
% _
% | | ___ _ __ ___
% _ | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
% \___/ \___/| .__/|___/
% |_|
%
% «J-ops-and-regions» (to ".J-ops-and-regions")
% (ph2p 11 "J-ops-and-regions")
% (ph2 "J-ops-and-regions")
% J-regions and J-operators
\section{J-operators and J-regions}
\label {J-ops-and-regions}
% 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("&", "\\&", "vv", "∨", "->", "→")
%L addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
%:
%: -----\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 axioms $\J1$, $\J2$, $\J3$ have many consequences. The first ones
are listed in Figure \ref{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,
%:
%: ------------\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<=PvvQ PvvQ<=P!
%: --------------------
%: P<=PvvQ<=P!
%: -----------\Sand
%: P!=Q! P!=Q!\bk P!=(PvvQ)!
%: ------------\ECv := ------------------
%: P!=Q!=(PvvQ)! P!=Q!=(PvvQ)!
%:
%: ^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
\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{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 Let
$P_∨ := ((P_1∨P_2)∨\ldots)∨P_n$. It turns out that $[P]^J =
[P_∧,P_∨]∩Ω$; let's prove that by doing `$⊆$' first, then `$⊇$'.
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 \\
\end{array}
$$
%
so $P_∧ \eqJ P_∨ \eqJ P$, and by the sandwich lemma $([P_∧,P_∨]∩Ω) ⊆
[P]^J$.
For any $P_i∈[P]^J$ we have $P_∧≤P_i≤P_∨$, which means that:
%
$$\begin{array}{rcl}
[P]^J &=& \{P_1, \ldots, P_n\} \\
&⊆& \setofst{Q∈Ω}{P_∧≤Q≤P_∨} \\
&=& [P_∧,P_∨]∩Ω, \\
\end{array}
$$
%
so $[P]^J ⊆ [P_∧,P_∨]∩Ω$.
\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_∧$.
% (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")
\bsk
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")
\section{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 the
last section,
%
%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 it 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:
%: Q!=R!
%: -----------
%: PvvQ!=PvvR!
%: -----------------
%: Q!=R! (PvvQ!)!=(PvvR!)!
%: ---------------\NoYcuts := =================\ostarcube
%: (PvvQ)!=(PvvR)! (PvvQ)!=(PvvR)!
%:
%: ^NoYcuts1- ^NoYcuts2-
%:
%: P!=Q!
%: -----------
%: PvvR!=QvvR!
%: -----------------
%: P!=Q! (PvvR!)!=(QvvR!)!
%: ---------------\NoYcuts := =================\ostarcube
%: (PvvR)!=(QvvR)! (PvvR)!=(QvvR)!
%:
%: ^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 top derivation mentions a rule called `$\ostarcube$', which will
be defined and proved in sec.\ref{full-cubes}.
% ___ _ _ _
% / _ \| |____ _(_) ___ _ _ ___ ___ _ _| |__ ___ ___
% | | | | '_ \ \ / / |/ _ \| | | / __| / __| | | | '_ \ / _ \/ __|
% | |_| | |_) \ V /| | (_) | |_| \__ \ | (__| |_| | |_) | __/\__ \
% \___/|_.__/ \_/ |_|\___/ \__,_|___/ \___|\__,_|_.__/ \___||___/
%
% «obvious-cubes» (to ".obvious-cubes")
% (ph2p 13 "obvious-cubes")
\section{How J-operators interact with connectives: the obvious cubes}
\label {obvious-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")
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%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 below ($A \diagxyto/->/ B$
means $A≤B$):
%
$$\myresizebox{$
\pu
\def∧{{\&}}
\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
The cubes above will be called the ``obvious and-cube'', the ``obvious
or-cube'', and the ``obvious implication-cube'', and they show partial
orders between expressions of the form $(P^? ⊙ Q^?)^?$, where the
`$\odot$' stands for one of the connectives `$∧$', `$∨$' or `$→$', and
each `?' marks a place where we can put either a `${}^*$' or nothing;
let's be more precise.
The ``cube of $∧$-expressions'', $\ECube_∧$, is the set of eight
expressions of the form $(P^? ∧ Q^?)^?$; $\ECube_∨$ is the set of
eight expressions of the form $(P^? ∨ Q^?)^?$, and $\ECube_→$ the set
of eight expressions of the form $(P^? → Q^?)^?$.
The ``obvious $∧$-cube'', $\OCube_∧$, is the directed graph shown
above, with 12 arrows between elements of $\ECube_∧$. Its transitive
closure, $\OCube_∧^*$, is a partial order on $\ECube_∧$. We define
$\OCube_∨$, $\OCube_∨^*$, $\OCube_→$, and $\OCube_→^*$ similarly.
If we establish that the three `?'s in $(P^? ⊙ Q^?)^?$ are ``worth''
1, 2 and 4 respectively, we get a way to number the elements in
$\ECube_∧$ from 0 to 7. We define $(∧)_0, \ldots, (∧)_7$ as:
%
$$\begin{array}{rclcrcl}
(∧)_0 &=& P∧Q, && (∧)_4 &=& (P∧Q)^*, \\
(∧)_1 &=& P^*∧Q, && (∧)_{1+4} &=& (P^*∧Q)^*, \\
(∧)_2 &=& P∧Q^*, && (∧)_{2+4} &=& (P∧Q^*)^*, \\
(∧)_{1+2} &=& P^*∧Q^*, && (∧)_{1+2+4} &=& (P^*∧Q^*)^*, \\
\end{array}
$$
%
and we do the same for $(∨)_0, \ldots, (∨)_7, (→)_0, \ldots, (→)_7$.
We always draw the `$(⊙)_i$'s in this position:
%
$$\mat{ & (⊙)_7 & \\[5pt]
(⊙)_5 & (⊙)_3 & (⊙)_6 \\[5pt]
(⊙)_1 & (⊙)_4 & (⊙)_2 \\[5pt]
& (⊙)_0 & \\
}
\qquad
\qquad
\mat{ & 7 & \\[5pt]
5 & 3 & 6 \\[5pt]
1 & 4 & 2 \\[5pt]
& 0 & \\
}
$$
With this numbering we can reinterpret the cubes as subsets of
$\{0,\ldots,7\}^2$; $\{0,\ldots,7\}^2$ is a ZSet, and so we can use
the positional notation and interpret each cube as a grid of `0's and
`1's. For example,
%
%D diagram cube-and*-0
%D 2Dx 100 +20 +20
%D 2D 100 A1
%D 2D +15 A2 A3 A4
%D 2D +15 A5 A6 A7
%D 2D +15 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D ren A1 ==> 7
%D ren A2 A3 A4 ==> 5 3 6
%D ren A5 A6 A7 ==> 1 4 2
%D ren A8 ==> 0
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%R local foo, foos =
%R 2/0 0 0 1 0 1 1 0 \, 2/1 1 1 1 1 1 1 1 \
%R |0 0 1 0 1 0 0 0 | |1 0 1 0 1 0 1 0 |
%R |0 1 0 0 1 0 0 0 | |1 0 0 0 1 1 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 1 0 0 1 0 0 0 |
%R |0 1 1 0 0 0 0 0 | |1 1 1 1 0 0 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 0 1 0 0 0 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 1 0 0 0 0 0 0 |
%R \0 0 0 0 0 0 0 0 / \1 0 0 0 0 0 0 0 /
%R
%R foo :tomp({def="foo", scale="7pt", meta="s"}):addcells():output()
%R foos:tomp({def="foos", scale="7pt", meta="s"}):addcells():output()
%
\pu
$$
\diag{cube-and*-0}
\quad
=
\quad
\cmat{(0,1),(2,3),(4,5),(6,7),\\
(0,2),(1,3),(4,6),(5,7),\\
(0,4),(1,5),(2,6),(3,7)\\
}
\quad
=
\quad
\foo
$$
The transitive-reflexive closure of a cube yields a different grid:
%
$$\left(\diag{cube-and*-0}\right)^*
\quad
=
\quad
\foos
$$
Note that the grids for $\OCube_∧$ and $\OCube_∨$ are equal, but the
grid for $\OCube_→$ is different. Also, note that $\OCube_∧$,
$\OCube_∧^*$, etc, are directed graphs; sometimes we will need to
regard them as pairs, and we will use a lowercase notation for their
sets of arrows: $\OCube_∧ = (\ECube_∧, \ocube_∧)$, $\OCube_→^* =
(\ECube_→, \ocube_→^*)$, etc.
% _____ _ _ _
% | ___| _| | | ___ _ _| |__ ___ ___
% | |_ | | | | | | / __| | | | '_ \ / _ \/ __|
% | _|| |_| | | | | (__| |_| | |_) | __/\__ \
% |_| \__,_|_|_| \___|\__,_|_.__/ \___||___/
%
% «full-cubes» (to ".full-cubes")
% (ph2p 13 "full-cubes")
\section{How J-operators interact with connectives: the full cubes}
\label {full-cubes}
We can prove these new derived rules,
%:
%:
%: =====================\acz ==================\ocz ====================\icz
%: (P!&Q!)!=P!&Q!=(P&Q)! (P!vvQ!)!<=(PvvQ)! (P->Q^*)^*<=P^*->Q^*
%:
%: ^and*-extra-arrow ^or*-extra-arrow ^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<=PvvQ Q<=PvvQ (P->Q^*)&P<=Q^*
%: ------------\Mo -----------\Mo -------------------\Mo
%: P!<=(PvvQ)! Q!<=(PvvQ)! ((P->Q^*)&P)^*<=Q!!
%: --------------------------- -------------------\J2
%: P!vvQ!<=(PvvQ)! ((P->Q^*)&P)^*<=Q^*
%: -------------------\Mo -------------------\J3
%: (P!vvQ!)!<=(PvvQ)!! (P->Q^*)^*&P^*<=Q^*
%: -------------------\J2 -------------------
%: (P!vvQ!)!<=(PvvQ)! (P->Q^*)^*<=P^*->Q^*
%:
%: ^or*-extra-arrow-proof ^imp*-extra-arrow-proof
%:
%:
$$
\myresizebox{$\pu
\begin{array}{rcl}
\ded{and*-extra-arrow} &:=& \ded{and*-extra-arrow-proof} \\\\
\ded{or*-extra-arrow} &:=& \ded{or*-extra-arrow-proof} \\\\
\ded{imp*-extra-arrow} &:=& \ded{imp*-extra-arrow-proof} \\
\end{array}
$}
$$
%
and interpret them as extra arrows on the cubes. The ``full
$∧$-cube'', $\FCube_∧$, is $\OCube_∧$ plus these arrows:
%
$$(P^*∧Q^*)^* \two/<-`->/<200> P^*∧Q^* \two/<-`->/<200> (P∧Q)^*$$
%
The ``full $∨$-cube'', $\FCube_∨$, is $\OCube_∨$ plus this,
%
$$(P^*∨Q^*)^* \diagxyto/->/<200> (P∨Q)^*$$
%
and the ``full $→$-cube'', $\FCube_→$, is $\OCube_→$ plus this,
%
$$(P→Q^*)^* \diagxyto/->/<200> (P^*→Q^*)$$
We are interested in the transitive-reflexive closures of these full
cubes. $\FCube_∧^*$ yields a {\sl non-strict} partial order on
$\ECube_∧$ that identifies five of its elements, and $\FCube_∨^*$ and
$\FCube_→^*$ yield non-strict partial orders that identify four
elements each. My favorite way to represent these non-strict partial
orders is by the diagrams at the right below, that show very clearly
which elements are identified:
%D diagram cube-and*-full-raw
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (∧)_7
%D ren A5 A3 A6 ==> (∧)_5 (∧)_3 (∧)_6
%D ren A1 A4 A2 ==> (∧)_1 (∧)_4 (∧)_2
%D ren A0 ==> (∧)_0
%D
%D # Full ∧-cube, with extra arrows:
%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 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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (∧)_7
%D ren A5 A3 A6 ==> (∧)_5 (∧)_3 (∧)_6
%D ren A1 A4 A2 ==> (∧)_1 (∧)_4 (∧)_2
%D ren A0 ==> (∧)_0
%D
%D # Full ∧-cube, with `='s:
%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
\left( \diag{cube-and*-full-raw} \right)^* =
\left( \diag{cube-and*-full} \right)^*
$$
%D diagram cube-or*-full-raw
%D 2Dx 100 +40 +40
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (∨)_7
%D ren A5 A3 A6 ==> (∨)_5 (∨)_3 (∨)_6
%D ren A1 A4 A2 ==> (∨)_1 (∨)_4 (∨)_2
%D ren A0 ==> (∨)_0
%D
%D # Full ∨-cube, with extra arrows:
%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= 10pt
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (∨)_7
%D ren A5 A3 A6 ==> (∨)_5 (∨)_3 (∨)_6
%D ren A1 A4 A2 ==> (∨)_1 (∨)_4 (∨)_2
%D ren A0 ==> (∨)_0
%D
%D # Full ∨-cube, with `='s:
%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
\left( \diag{cube-or*-full-raw} \right)^* =
\left( \diag{cube-or*-full} \right)^*
$$
%D diagram cube-imp*-full-raw
%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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (→)_7
%D ren A5 A3 A6 ==> (→)_5 (→)_3 (→)_6
%D ren A1 A4 A2 ==> (→)_1 (→)_4 (→)_2
%D ren A0 ==> (→)_0
%D
%D # Full →-cube, raw:
%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 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 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (→)_7
%D ren A5 A3 A6 ==> (→)_5 (→)_3 (→)_6
%D ren A1 A4 A2 ==> (→)_1 (→)_4 (→)_2
%D ren A0 ==> (→)_0
%D
%D # Full →-cube with `='s:
%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
\left( \diag{cube-imp*-full-raw} \right)^* =
\left( \diag{cube-imp*-full} \right)^*
$$
When the arrow $(∧)_i \diagxyto/->/<200> (∧)_j$ belongs to
$\FCube_∧^*$ we say that $(∧)_i≤(∧)_j$ is true ``by the full
and-cube''. We write this as a derived rule as
%:
%:
%: -------------\astarcube_{ij}
%: (∧)_i≤(∧)_j
%:
%: ^astarij
%:
%: -------------\astarcube
%: (∧)_i≤(∧)_j
%:
%: ^astar
%%
$$\pu
\ded{astarij} \qquad \text{or just as:} \qquad \ded{astar}\;,
$$
%
and when the arrows $(∧)_i \two/->`<-/<200> (∧)_j$ belongs to
$\FCube_∧^*$ we say that $(∧)_i=(∧)_j$ is true ``by the full
and-cube'', and we write that as:
%:
%:
%: -------------\astarcube_{ij}
%: (∧)_i=(∧)_j
%:
%: ^astareqij
%:
%: -------------\astarcube
%: (∧)_i=(∧)_j
%:
%: ^astareq
%%
$$\pu
\ded{astareqij} \qquad \text{or just as:} \qquad \ded{astareq}\;,
$$
%
and we do the same for `$∨$' and `$→$'.
% (ph2 "no-Y-cuts-no-L-cuts")
% (ph2 "no-Y-cuts-no-L-cuts" "\\ostarcube")
The double-bar rule in sec.\ref{no-Y-cuts-no-L-cuts} is a contraction
of:
%:
%: (P∨Q!)!=(P∨R!)!
%: =================\ostarcube
%: (P∨Q)!=(P∨R)!
%:
%: ---------------\ostarcube_{64}
%: (P∨Q!)!=(P∨R!)! (P∨R!)!=(P∨R)!
%: ----------------------------------
%: (P∨Q)!=(P∨R)!
%:
%: ^foo
%:
$$\pu\ded{foo}$$
\bsk
% We say that $\text{expr}_1 ≤ \text{expr}_2$ is true ``by the full
% and-cube'' when $\text{expr}_1 ≤ \text{expr}_2$ can be read from the
% (non-strict!) partial order in the the full and-cube; for example,
% $P∧Q^* ≤ (P^*∧Q)^*$ is true ``by the full and-cube'', and similary
% $P^*∨Q^* ≤ (P∨Q)^*$ is true by the full or-cube and $(P→Q)^* ≤ P→Q^*$
% is true by the full implication-cube.
%
% We write
% %:
% %:
% %: ----------------------------\astarcube
% %: \text{expr}_1≤\text{expr}_2
% %:
% %: ^astar
% %:
% %:
% %: ----------------------------\ostarcube
% %: \text{expr}_1≤\text{expr}_2
% %:
% %: ^ostar
% %:
% %:
% %: ----------------------------\istarcube
% %: \text{expr}_1≤\text{expr}_2
% %:
% %: ^istar
% %:
% $$\pu
% \ded{astar}
% \qquad
% \ded{ostar}
% \qquad
% \ded{istar}
% $$
% %
% to indicate that the expression below the bar is a consequence (a
% substitution instance) of the partial order in the full and-cubes, the
% full or-cube, or the full implication-cube.
%
% \msk
%
% The six cubes will be discussed in more detail in the section
% \ref{comparing-partial-orders}.
% https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders
% _____ _ _ _
% | ___| _| | | ___ _ _| |__ ___ ___
% | |_ | | | | | | / __| | | | '_ \ / _ \/ __|
% | _|| |_| | | | | (__| |_| | |_) | __/\__ \
% |_| \__,_|_|_| \___|\__,_|_.__/ \___||___/
%
% «valuation-cubes» (to ".valuation-cubes")
% (ph2p 18 "valuation-cubes")
\section{How J-operators interact with connectives: \ZHAstar-valuations}
\label {valuation-cubes}
Let's write $\Exprs(\mathsf{V})$ for the set of well-formed
expressions built from a set of variables $\mathsf{V}$, constants $⊤$
and $⊥$, and operations $∧$, $∨$, $→$, $↔$, $¬$, $·^*$; each one of
the sets $\ECube_∧$, $\ECube_∨$ and $\ECube_→$ of the last sections
is an 8-element subset of $\Exprs(\{P,Q\})$.
If $\mathsf{E} ⊆ \Exprs(\mathsf{V})$, a {\sl \ZHAstar-valuation for
$\mathsf{E}$}, or an {\sl $\mathsf{E}$-valuation}, is a triple
$(H,J,v)$, where $H$ is a ZHA, $J$ is a J-operator on $H$, and
$v:\mathsf{V}→H$ is a function that assigns a truth-value in $H$ to
each variable in $\mathsf{V}$. There is a natural way to extend $v$ to
a function $v':\Exprs(\mathsf{V})→H$, and we can restrict $v'$ to a
function $v'':\mathsf{E}→H$.
We can draw all components of an $\ECube_∨$-valuation $(H,J,v)$
together by writing `$P$' and `$Q$' on the positions $v(P)$ and $v(Q)$
on $(H,J)$, as we did in sec.\ref{slash-ops-property}. We will often
also write `$P^*$' and `$Q^*$' on the positions $v'(P^*)$ and
$v'(Q^*)$ for clarity. For example:
%
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321"):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()
%
\pu
\def\V#1{v(#1)}
\def\VV#1{v'(#1)}
\def\VVV#1{v''((∨)_#1)}
$$\orCube
\qquad
\begin{array}{rclcrclcl}
&&&& \VV{P∨Q} &=& 11 &=& \VVV0 \\
&&&& \VV{P^*∨Q} &=& 21 &=& \VVV1 \\
\V{P} &=& 10 && \VV{P∨Q^*} &=& 12 &=& \VVV2 \\
\V{Q} &=& 01 && \VV{P^*∨Q^*} &=& 22 &=& \VVV3 \\
\VV{P^*} &=& 20 && \VV{(P∨Q)^*} &=& 22 &=& \VVV4 \\
\VV{Q^*} &=& 02 && \VV{(P^*∨Q)^*} &=& 22 &=& \VVV5 \\
&&&& \VV{(P∨Q^*)^*} &=& 22 &=& \VVV6 \\
&&&& \VV{(P^*∨Q^*)^*} &=& 22 &=& \VVV7 \\
\end{array}
$$
Each $\ECube_∨$-valuation $(H,J,v)$ induces a non-strict partial order
on $\ECube_∨$, in which $(∨)_i≤(∨)_j$ iff $\VVV{i}≤\VVV{j}$. We will
write that partial order as
%
$$\begin{array}{rclcc}
\VCube_∨(H,J,v) &=& (\ECube_∨,\vcube_∨(H,J,v)) && \text{or:}\\
\VCube_∨(v) &=& (\ECube_∨,\vcube_∨(v)) \\
\end{array}
$$
%
We will often omit the `$H$' and the `$J$' and write just
$\VCube_∨(v)$.
It is easy to calculate by hand the partial orders $\VCube_∨(v)$,
$\VCube_∧(v)$ or $\VCube_→(v)$ associated to a given valuation
$(H,J,v)$: we write in the position corresponding to each `$(⊙)_i$' of
the cube the value of the corresponding $v''((⊙)_i)$, then we draw the
arrows --- some of them will be `$=$'s ---, then transfer the arrows
to the cube with `$(⊙)_i$'s. For example:
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321"):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()
%
%D diagram cube-or*-full-A
%D 2Dx 100 +25 +25
%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 ==> 22
%D ren A5 A3 A6 ==> 22 22 22
%D ren A1 A4 A2 ==> 21 22 12
%D ren A0 ==> 11
%D
%D # Full ∨-cube, with `='s:
%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-B
%D 2Dx 100 +25 +25
%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 ==> (∨)_7
%D ren A5 A3 A6 ==> (∨)_5 (∨)_3 (∨)_6
%D ren A1 A4 A2 ==> (∨)_1 (∨)_4 (∨)_2
%D ren A0 ==> (∨)_0
%D
%D # Full ∨-cube, with `='s:
%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
%
$$\myresizebox{$
\pu
\diag{cube-or*-full-A}
\quad
\squigto
\quad
\VCube_∨\left(\orCube\right) =
\left(\diag{cube-or*-full-B}\right)^*
$}
$$
\msk
{\sl A very important fact.} For any $i$ and $j$,
%
%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}{rcl}
(∨)_i≤(∨)_j & \text{ is a theorem iff it is true in } & \orCube \;\; , \\
\\
(∧)_i≤(∧)_j & \text{ is a theorem iff it is true in } & \andCube \;\; , \\
\\
(→)_i≤(→)_j & \text{ is a theorem iff it is true in } & \impCube \;\; . \\
\end{array}
$$
%
We will call the valuations at the right above $(H_∨,J_∨,v_∨)$,
$(H_∧,J_∧,v_∧)$, $(H_→,J_→,v_→)$. In the language of partial orders,
the very important fact can be stated as:
%
$$\begin{array}{rcl}
\FCube_∨^* &=& \VCube_∨(v_∨), \\
\FCube_∧^* &=& \VCube_∧(v_∧), \\
\FCube_→^* &=& \VCube_→(v_→). \\
\end{array}
$$
Suppose that $(H_1,J_1,v_1)$, $(H_2,J_2,v_2)$, $\ldots$ are valuations
on --- say --- $\ECube_→$. This always holds
%
$$\FCube_→^* ⊆ \VCube_→(v_i),$$
%
because all \ZHAstar-theorems are true in all valuations. We say that:
%
$$\begin{array}{rcl}
\text{$v_i$ is {\sl good}} & \text{when} & \FCube_→^* = \VCube_→(v_i), \\
\text{$v_i$ and $v_j$ are {\sl equivalent}} & \text{when} & \VCube_→(v_i) = \VCube_→(v_j), \\
\text{$v_i$ is {\sl better than} $v_j$} & \text{when} & \VCube_→(v_i) ⊆ \VCube_→(v_j). \\
\end{array}
$$
Also, a {\sl non-theorem} is an arrow $(→)_i≤(→)_j$ that is not in
$\FCube_→^*$; a {\sl countermodel} for a non-theorem $(→)_i≤(→)_j$ is
a valuation that ``falsifies'' $(→)_i≤(→)_j$, i.e., a valuation in
which $(→)_i≤(→)_j$ is not true. Note that a valuation is ``good''
when it is a countermodel for all non-theorems at once, and a
valuation $v_1$ is strictly better than $v_2$ when $v_1$ falsifies all
non-theorems that $v_2$ falsifies, plus some.
\msk
In sec.18 of [PH1] we saw that ZHAs do not distinguish as many
sentences as arbitrary Heyting Algebras; we saw a sentence
$S_P∨S_Q∨S_R$ that had a countermodel in a HA, but that ZHAs ``think''
that its value is always $⊤$. To formalize and extend this idea we
need a slight abuse of language. We will say that an $\sfE$-valuation
$(H,J,v)$ ``distinguishes all elements of $\sfE$'', or ``distinguishes
$\sfE$'', instead of the more precise ``is a countermodel for all
non-theorems of the form $E_i≤E_j$ at once''; and we will say that
$v_1$ ``distinguishes more elements of $\sfE$'' than $v_2$ when $v_1$
is better than $v_2$. A set of expressions $\sfE$ is {\sl
\ZHAstar-good} when there is a valuation that distinguishes all
elements of $\sfE$. So:
%
$$\begin{array}{rcl}
\{S_P∨S_Q∨S_R,⊤\} & \text{is not} & \text{\ZHAstar-good}, \\
\ECube_∨ & \text{is} & \text{\ZHAstar-good}, \\
\ECube_∧ & \text{is} & \text{\ZHAstar-good}, \\
\ECube_→ & \text{is} & \text{\ZHAstar-good}. \\
\end{array}
$$
ZHAs with J-operators do not distinguish all sets of expressions, but
they distinguish some sets, like $\ECube_∨$, $\ECube_∧$, $\ECube_→$,
that are {\sl very} useful.
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 $\ECube_∨u\ECube_∧$, but it does not distinguish
$\ECube_→$ --- it thinks that $P→Q$ and $P^*→Q$ are equal.
\msk
% (find-books "__cats/__cats.el" "bell")
% (find-books "__cats/__cats.el" "bell" "163")
{\sl An observation.} I arrived at the cubes $\FCube_∧^*$,
$\FCube_∨^*$, $\FCube_→^*$ 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 a full cube 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
$\FCube_∧^*$ (and the same for $\FCube_∨^*$ and $\FCube_→^*$), and I
tried to start with a valuation that distinguished {\sl some} elements
in $\ECube_∧$, and change it bit by bit, getting valuations that
distinguished more elements at every step. Eventually I arrived at
$v_∧$, $v_∨$ and at $v_→$, and at the --- surprisingly nice --- ``very
important fact''.
% ______ _ _ _ _
% |__ / | | | / \ __/\__ __ ____ _| |___ __ _ ___ ___ __| |
% / /| |_| | / _ \ \ /____\ \ / / _` | / __| / _` |/ _ \ / _ \ / _` |
% / /_| _ |/ ___ \/_ _\_____\ V / (_| | \__ \ | (_| | (_) | (_) | (_| |
% /____|_| |_/_/ \_\ \/ \_/ \__,_|_|___/ \__, |\___/ \___/ \__,_|
% |___/
%
% «ZHA-vals-good» (to ".ZHA-vals-good")
% \section{\ZHAstar-valuations are very good}
\section{Good valuations}
\label {ZHA-vals-good}
% (ph2p 20 "ZHA-vals-good")
If $(∨)_i≤(∨)_j$ is true in $\FCube_∨^*$ then it is a theorem, and it
holds in every $\ECube_∨$-valuation $(H,J,v)$ --- so
$\FCube_∨^*⊆\VCube_∨(H,J,v)$. The important information that a
\ZHAstar-valuation carries is in its `$\not≤$'s, as they say that
something {\sl cannot} be a theorem and that $(H,J,v)$ is a
countermodel showing that. For example, in $(H_∨,J_∨,v_∨)$ we had
$(∨)_7\not≤(∨)_3$; if we could prove, using new derived rules like the
ones in sec.\ref{full-cubes}, that $(∨)_7≤(∨)_3$ is a theorem, then we
would have $(∨)_7≤(∨)_3$ in all valuations, which is incompatible with
the $(∨)_7\not≤(∨)_3$ in $\VCube_∨(H_∨,J_∨,v_∨)$.
Note that this means that: 1) that if a statement of the form
$(∨)_i≤(∨)_j$ is not in $\FCube_∨^*$ then it cannot be proved, i.e.,
all attempts to find a tree-proof for that $(∨)_i≤(∨)_j$ using the HA
rules and $\J1$, $\J2$, $\J3$ are bound to fail; 2) the theorems of
the form $(∨)_i≤(∨)_j$ are exactly the ones that are true in
$\VCube_∨(H_∨,J_∨,v_∨)$, so we can use $(H_∨,J_∨,v_∨)$ as a {\sl
reminder} for which sentences of the form $(∨)_i≤(∨)_j$ are theorems
--- and the same for `$∧$' and `$→$'.
\newpage
% ___ _ _ _
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ __ _ _ __| | _____
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \ / _` | '__| |/ / __|
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | | (_| | | | <\__ \
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|\__,_|_| |_|\_\___/
%
% «question-marks» (to ".question-marks")
% (ph2p 29 "question-marks")
\section{Question marks}
\label {question-marks}
% \def\squigbij{\diagxyto/<~>/<200>}
% \def\squigbij{\;\; \diagxyto/<~>/<200> \;\;}
% \def\squigbij{\;\; \diagxyto/<~>/<300> \;\;}
Every ZHA $H$ is equivalent --- by the constructions explained in
sections 14--17 of [PH1] --- to a 2-column graph $(P,A)$. To be more
precise, each ZHA $H$ has an associated 2CG $(P,A)$, such that this
holds: the partial order $(H,≤)$ is equivalent to $(\Opens_A(P),⊆)$,
where $\Opens_A(P)$ is the ``order topology'' on $P$ (sections 12--13
of [PH1]). We will use squiggly arrows to mean ``is associated to''.
For example:
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():output()
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgL" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():vs():lrs():output()
%L tcgbig("tcgL" ):hs():vs():lrs():output()
%
$$\pu
\foo \squigbij \tcgL
$$
Each truth-value $cd∈H$ corresponds to the open set
$\pile(cd)∈\Opens_A(P)$; the function $\pile:H→\Opens_A(P)$ is a
bijection. We will also use squiggly arrows to indicate this
correspondence:
%
%L tcgmed("tcgL" ):strs("1 1 0 0", "1 1 1 0 0 0"):hs():output()
%
$$\pu
23 \squigbij \pile(23) = \{2▁,1▁, \, ▁3,▁2,▁1\} = \tcgL
$$
%
Note that we are used the positional notation from sec.15 of [PH1] to
draw $\pile(23)⊆P$ as an open set of $\Opens_A(P)$.
\msk
Choose any partition of $P$ into two disjoint subsets $P_!∪P_?$; we
will call $P_!$ the ``set of relevant points'' and $P_?$ the ``set of
question marks'' of the partition; we will use the letter $Q$ to
indicate a certain choice of question marks. Any partition $P=P_!∪P_?$
induces:
\begin{itemize}
\item an equivalence relation `$\eqQp$' on $\Opens_A(P)$; if
$R',S'∈\Opens_A(P)$ then $R' \eqQp S'$ iff $R'∩P_! = S'∩P_!$, or,
equivalently, iff $R'∖P_? = S'∖P_?$ (``$R'$ and $S'$ are equivalent
modulo question marks''),
\item an equivalence relation `$\eqQ$', on $H$: $cd \eqQ ef$ iff
$\pile(cd) \eqQp \pile(ef)$,
\item Q-equivalence classes on $H$: for each $cd∈H$ we write
%
$$[cd]^Q := \setofst{ef∈H}{cd \eqQ ef}$$
\item a ``Q-partition'' of $H$: $\setofst{[cd]^Q}{cd∈H}$.
\end{itemize}
% ___ __ __ _ _
% / _ \ / / \ \ ___| | __ _ ___| |__
% | | | | / /_____\ \ / __| |/ _` / __| '_ \
% | |_| | \ \_____/ / \__ \ | (_| \__ \ | | |
% \__\_\ \_\ /_/ |___/_|\__,_|___/_| |_|
%
% «Q-partitions-are-slash-partitions» (to ".Q-partitions-are-slash-partitions")
% (ph2p 23 "Q-partitions-are-slash-partitions")
% (ph2 "Q-partitions-are-slash-partitions")
\section{Q-partitions are slash-partitions and vice-versa}
\label {Q-partitions-are-slash-partitions}
\def\diff{\mathsf{diff}}
\def\QM {\mathsf{QM}}
Take a slash-partition $S$ on a ZHA $H$. For example, this one:
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu\foo$$
Let's start with a naïve idea: how can we build a Q-partition on $H$
that mimics the behavior of $S$? We have for example $22 \eqS 13$, so
we need to have $\pile(22) \eqS \pile(13)$, which means that the sets
$\{2▁,1▁,\;▁2,▁1\}$ and $\{1▁,\;▁3,▁2,▁1\}$ should be equal ``modulo
question marks''; writing
%
$$\begin{array}{rcl}
\diff(A,B) &:=& (A∖B)∪(B∖A), \\
\QM(cd,ef) &:=& \diff(\pile(cd), \pile(ef)) \\
\end{array}
$$
%
we have this: $cd \eqS ef$ implies $\QM(cd,ef)⊆P_?$, and $22 \eqS 13$
implies $\QM(22,13)=\{2▁,\;▁3\}⊆P_?$. In the slash-partition above we
have $22 \eqS 13$, $14 \eqS 45$, $00 \eqS 03$, so
$\QM(22,13)∪\QM(14,45)∪\QM(00,03)⊆P_?$; each set of pairs of
S-equivalent elements of $H$ yields a subset of $P_?$, and by starting
with a set of S-equivalent pairs that is big enough we {\sl may} be
able to discover all points in $P_?$...
In the other direction, what are the consequences of a certain point
belonging or not to $P_?$? It is easy to see that in the ZHA above we
have:
%
$$\def\neqQ{\not\eqQ}
%
\begin{array}{rcl}
1▁ ∈P_? &\Longrightarrow& (01 \eqQ11) ∧ (02 \eqQ12) ∧ (03 \eqQ13) ∧ (04 \eqQ14) \\
1▁\not∈P_? &\Longrightarrow& (01\neqQ11) ∧ (02\neqQ12) ∧ (03\neqQ13) ∧ (04\neqQ14) \\
▁4 ∈P_? &\Longrightarrow& (03 \eqQ04) ∧ (13 \eqQ14) ∧ (23 \eqQ24) \\
▁4\not∈P_? &\Longrightarrow& (03\neqQ04) ∧ (13\neqQ14) ∧ (23\neqQ24) \\
\end{array}
$$
%
so $1▁∈P_?$ means that we do have a cut going northeast between 0 and
1 --- ``$1/0$'' in the notation of sec.\ref{piccs-and-slashings} ---
and $1▁\not∈P_?$ means that we don't have that cut; $▁4∈P_?$ means
that we do have a cut going northwest between 3 and 4 --- ``$3∖4$'' in
the notation of sec.\ref{piccs-and-slashings} --- and $▁4\not∈P_?$
means that we don't have that cut. The presence or not of a given
point of $P$ in $P_?$ means the presence or not of a given cut, and
vice-versa.
We will skip the low-level details and just show two examples of
conversions. This is a ZHA $H$ with a slash-partition $S=(L,R)$ on it,
and the 2CG $(P,A)$ associated to $H$ with the partition $P=P_?∪P_!$
associated to $S$; we write on the side of each element of $P$ a `?'
or `!' to indicate whether it belongs to $P_?$ or $P_!$:
%
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%L
%L tcg_bigq = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2, dq=1.4}
%L
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L local tcg = tcgbigq("tcgP"); PP(tcg)
%L tcg:lrs():hs():vs()
%L tcg:qmarks("!???", "???!?!")
%L tcg:output()
%
$$\pu
\ZQuotients
\squigbij
\tcgP
$$
It turns out that we can ignore the exact shape of $H$ and the
intercolumn arrows in $A$. For any ZHA $H$ with top element 46, the
slashing $S=(L,R)$ on $H$ drawn below at the left corresponds to the
partition of $P=\LC(4)∪\RC(6)$ into $P_?∪P_!$ shown at the right:
%
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="foo"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
$$\pu
\foo \squigbij
\begin{array}{l}
P_! = \{1▁,\;▁4,▁6\} \\
P_? = \{2▁,3▁,4▁,\;▁1,▁2,▁3,▁5\} \\
\end{array}
$$
Note that we don't have cuts stopping midway.
% ___ _
% / _ \ ___ _ __ ___ _ __ ___ ___| |_ ___
% | | | |_____ / _ \| '_ \ / _ \ '_ \ / __|/ _ \ __/ __|
% | |_| |_____| (_) | |_) | __/ | | | \__ \ __/ |_\__ \
% \__\_\ \___/| .__/ \___|_| |_| |___/\___|\__|___/
% |_|
%
% «Q-open-sets» (to ".Q-open-sets")
% (ph2p 23 "Q-open-sets")
% (ph2 "Q-open-sets")
\section{Q-open sets}
\label {Q-open-sets}
% (ph2p 32)
\def\forget {\operatorname{\mathsf{forget}}}
\def\opens {\operatorname{\mathsf{Opens}}}
\def\propagate{\operatorname{\mathsf{prp}}}
\def\prp {\operatorname{\mathsf{prp}}}
\def\smallest {\operatorname{\mathsf{smallest}}}
\def\biggest {\operatorname{\mathsf{biggest}}}
Fix a 2CG $(P,A)$ and a partition $P=P_?∪P_!$. For example:
%L tcg_spec = "2, 3; 22, "
%L tcgMedq("tcgP"):lrs():hs():qmarks("!?", "!?!"):output()
%
$$\pu
\tcgP
$$
%
Keeping them fixed will simplify concepts and notation, and later we
will see how to let them vary.
A {\sl Q-set} is a subset $S⊆P$ ``after forgetting the information on
question marks'', and a {\sl Q-open set} is an open set
$S∈\Opens_A(P)$ ``after forgetting the information on question
marks''. Formally, both Q-sets and Q-open sets are triples
$(S_0,S_1,S_?)$ where $S_0∪S_1∪S_?$ is a partition of $P$, and when we
say that $(S_0,S_1,S_?)$ ``is $S$ after forgetting the information on
question marks'' what we mean is that $S_?=P_?$ and that $S_1=S∩P_!$
and $S_0=(P∖S)∩P_!$.
We will represent both Q-sets and Q-open sets graphically by drawing
`0's, `1's and `?'s on the points of $(P,A)$, and we will write the
forgetting operation as ``$\forget$''. For example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgMedq("tcgA"):hs():strs("0 1", "1 1 0"):output()
%L tcgMedq("tcgB"):hs():strs("0 ?", "1 ? 0"):output()
%
$$\pu
\forget(\tcgA) \;\; = \;\; \tcgB
$$
%
Note that the argument to `$\forget$' above is not an open set.
% We will write `$\forget_Q$' for the operation that forgets the
% information on a given subset $Q$ of $P$ --- $\forget_Q(S) =
% (S_0,S_1,S_?)$ means that $S_?=Q$, $S_1=S∖Q$, $S_0=(P∖S)∖Q$.
We will not need Q-sets often, so from here on we will deal with
Q-open sets exclusively except where otherwise indicated.
We will say that ``$S$ is of the form $(S_0,S_1,S_?)$'' when
$S∈\Opens_A(P)$ (an open set!) and $\forget_{S_?}(S)=(S_0,S_1,S_?)$.
For example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgMedq("tcgA"):hs():strs("0 1", "1 1 0"):output()
%L tcgMedq("tcgA"):hs():strs("0 0", "1 1 0"):output()
%L tcgMedq("tcgB"):hs():strs("0 ?", "1 ? 0"):output()
%
$$\pu
\tcgA \;\; \text{is of the form} \;\; \tcgB
$$
%
Note that this is less strict that requiring
$\forget(S)=(S_0,S_1,S_?)$.
We will write $\OPENS(S_0,S_1,S_?)$ for the set of all open sets
$S∈\Opens_A(P)$ such that $S$ is of the form $(S_0,S_1,S_?)$. Using
`$\OPENS$' we can rewrite the above as:
%
%L tcg_spec = "2, 3; 22, "
%L tcgMedq("tcgA"):hs():strs("0 1", "1 1 0"):output()
%L tcgMedq("tcgA"):hs():strs("0 0", "1 1 0"):output()
%L tcgMedq("tcgB"):hs():strs("0 ?", "1 ? 0"):output()
%
$$\pu
\tcgA \;\; ∈ \;\; \OPENS(\tcgB)
$$
It is easy to see that if both $A'$ and $B'$ belong to
$\OPENS(S_0,S_1,S_?)$ then both $A'∩B'$ and $A'∪B'$ also belong to
$\OPENS(S_0,S_1,S_?)$ --- and, if $\OPENS(S_0,S_1,S_?)$ is non-empty,
then $⋂\OPENS(S_0,S_1,S_?)$ and $⋃\OPENS(S_0,S_1,S_?)$ also belong to
$\OPENS(S_0,S_1,S_?)$, and they yield the ``extremities'' of the set
$\OPENS(S_0,S_1,S_?)$. This is very similar to what we did in
sec.\ref{slash-max}, except that now we are dealing with open sets
instead of with elements of ZHA $H$, and we will use the convention
that if $A∈H$ then $A'$ is the open set corresponding to $A$, and if
$C'$ is a set of open sets then $C$ is the corresponding set of
elements of $H$.
% ___ _ _
% / _ \ _ __ _ __ ___ _ __ __ _ __ _ __ _| |_(_) ___ _ __
% | | | |_____| '_ \| '__/ _ \| '_ \ / _` |/ _` |/ _` | __| |/ _ \| '_ \
% | |_| |_____| |_) | | | (_) | |_) | (_| | (_| | (_| | |_| | (_) | | | |
% \__\_\ | .__/|_| \___/| .__/ \__,_|\__, |\__,_|\__|_|\___/|_| |_|
% |_| |_| |___/
%
% «Q-open-sets-propagations» (to ".Q-open-sets-propagations")
\section{Q-open sets: propagations}
\label {Q-open-sets-propagations}
Let $C':=\OPENS(S_0,S_1,S_?)$. There is an easy way to calculate $⋂C'$
and $⋃C'$ by hand, based on the following idea: whenever there's an
arrow `$1→?$' in $(S_0,S_1,S_?)$ we can replace the `?' by a `1' by
``propagating the 1 forward'', and wherever there is an arrow `$?→0$'
we can replace the `?' by a `0' by ``propagating the 0 backwards'',
and these propagations do not change the result of `$\OPENS$'. Here is
an example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgmedq("tcgA"):hs():strs("0 1", "1 1 0"):output()
%L tcgmedq("tcgA"):hs():strs("0 0", "1 1 0"):output()
%L tcgmedq("tcgB"):hs():strs("0 ?", "1 ? 0"):output()
%
$$\pu
\begin{array}{rclcrcl}
\prp_1(\tcgA) = \tcgB && \OPENS(\tcgA) = \OPENS(\tcgA) \\ \\
\prp_0(\tcgA) = \tcgB && \OPENS(\tcgA) = \OPENS(\tcgA) \\
\end{array}
$$
%
we denote the operations ``propagate `1's forward everywhere'' and
``propagate `0's backwards everywhere'' by `$\prp_1$' and `$\prp_0$'.
If $(S_0,S_1,S_?)$ has a sequence of arrows of like $1→?→0$ or
$1→?→?→0$, in which a `1' is followed by `?'s and then by a `0', then
$\prp_1$ and $\prp_0$ will not commute. For example:
%
%L tcg_spec = "2, 2; 12, "
%L tcgmed("tcgN"):strs("? 1", "0 ?"):hs():output()
%L tcgmed("tcgZ"):strs("0 1", "0 0"):hs():output()
%L tcgmed("tcgO"):strs("1 1", "0 1"):hs():output()
$$\pu
% \prp_1\left(\prp_0 \tcgN\right)
% = \tcgZ ≠ \tcgO =
% \prp_0\left(\prp_1 \tcgN\right)
\begin{array}{rcl}
\prp_1\left(\prp_0 \tcgN\right) &=& \tcgZ \\ \\
\prp_0\left(\prp_1 \tcgN\right) &=& \tcgO \\
\end{array}
$$
%
but when this happens we have that $\OPENS(S_0,S_1,S_?)$ is empty.
Conversely, if $S∈\Opens_A(P)$ is an open set then for any Q-open set
$(S_0,S_1,S_?)$ generated from it (and there is one for each choice of
as $S_?⊆P$) we have $S∈\OPENS(S_0,S_1,S_?)$. So:
{\sl Theorem.} $\OPENS(S_0,S_1,S_?)$ is a Q-open set iff
$\prp_1(\prp_0(S_0,S_1,S_?)) = \prp_0(\prp_1(S_0,S_1,S_?))$.
\msk
As we are only interested in open and Q-open sets, we can consider
that $\prp_1$ and $\prp_0$ commute, and we will denote their composite
as `$\prp$'. The most important property of $\prp$ is that
$\OPENS(S_0,S_1,S_?) = \OPENS(\prp(S_0,S_1,S_?))$.
It is easy to see that the result of $\prp(S_0,S_1,S_?)$ is a Q-open
set that in each column has `0's below, then `?'s in the middle, then
`1's at the top, and no intercolumn arrows of the form $?→1$ or $0→?$.
For example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgA"):strs("1 0 0 0", "1 1 0 0 0 0"):hs():output()
%L tcgmed("tcgB"):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgC"):strs("1 0 0 0", "1 0 0 0 0 0"):hs():output()
%
$$\pu
\begin{array}{ccc}
\forget(\tcgA) = \tcgB &&
\prp(\tcgB) = \tcgC \\
% \\
% &&
% \OPENS(\tcgB) = \OPENS(\tcgC) \\
\end{array}
$$
It is also easy to see --- in particular cases --- that the smallest
elements of $\OPENS(\prp(S_0,S_1,S_?))$ can be obtained by replacing
all the `?'s with `0's, and that the biggest one can be obtained by
replacing all the '?'s with `1's.
% ____ _ _
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__|
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | |
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_|
% |___/
%
% «rectangular» (to ".rectangular")
% (ph2p 31 "rectangular")
\section{Rectangular versions}
\label {rectangular}
Let $(H,J)$ be a pair made of a ZHA and a J-operator on it. Let
$(P,A)$ be the 2-column graph associated to $H$. Write $A'$ for $A$
minus its intercolumn arrows, $H'$ for the ZHA associated to $(P,A')$,
and $J'$ for the J-operator on $H'$ that has the same cuts as $J$. For
example:
%
%L mp = mpnew({def="HOrig"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="HRect"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgOrig" ):hs():vs():lrs():output()
%L tcgbig("tcgRect" ) :vs():lrs():output()
%
$$\pu
\begin{array}{rclcrcl}
(H,J) &=& \HOrig && (P,A) &=& \tcgOrig \\
\\
(H',J') &=& \HRect && (P,A') &=& \tcgRect \\
\end{array}
$$
We will call $(H',J')$ the {\sl rectangular version} of $(H,J)$ and
$(P,A')$ the rectangular version of $(P,A)$. Note that $H$ and $H'$
have the same top element.
For any $D∈H$ both $[D]^J$ and $[D]^{J'}$ are ``intervals'' in the
sense of sec.\ref{piccs-and-slashings}, and so they have maximal and
minimal elements. Let:
%
$$\begin{array}{rcl}
I &=& [D]^J, \\
I' &=& [D]^{J'}, \\
F &=& ⋁I', \\
E &=& ⋁I, \\
C &=& ⋀I, \\
B &=& ⋀I'; \\
\end{array}
$$
%
in the example above if $D=12$ then $B=10$, $C=11$, $E=23$, $F=43$.
% ____ _ _ _
% | _ \ ___ ___| |_ | |_| |__ ___ ___ _ __ ___ _ __ ___ ___
% | |_) / _ \/ __| __| | __| '_ \ / _ \/ _ \| '__/ _ \ '_ ` _ \/ __|
% | _ < __/ (__| |_ | |_| | | | __/ (_) | | | __/ | | | | \__ \
% |_| \_\___|\___|\__| \__|_| |_|\___|\___/|_| \___|_| |_| |_|___/
%
% «rectangular-theorems» (to ".rectangular-theorems")
\section{Rectangular versions: theorems}
\label {rectangular-theorems}
% (ph2p 32 "rectangular-theorems")
% (ph1 "topologies-on-2CGs" "prohibitions")
% (ph1p 26 "topologies-on-2CGs" "prohibitions")
We saw in sec.15 of [PH1] that the arrows in $(P,A)$ can be seen as
``prohibitions''. In the example of the previous section, we have:
%
$$\begin{array}{rcl}
H' &=& \setofst {ab}
{a∈\{0,\ldots,4\},
b∈\{0,\ldots,6\}
} \\
H &=& \setofst {ab}
{a∈\{0,\ldots,4\},
b∈\{0,\ldots,6\},
\psm {a≥4 \,→\, b≥5 \; ∧ \\
a≥3 \,→\, b≥4 \; ∧ \\
a≥2 \,←\, b≥2 \; ∧ \\
a≥2 \,←\, b≥5 \;\;\; \\
}
} \\
\end{array}
$$
If we write ``$\obeys(ab,A)$'' for ``$ab$ obeys the prohibitions
induced by the intercolumn arrows of $A$'' we can rewrite the above
as:
%
$$\begin{array}{rcl}
H' &=& \setofst {ab}
{ab∈[00,46]
} \\
H &=& \setofst {ab}
{ab∈[00,46],
\obeys(ab,A)
} \\
\end{array}
$$
%
To obtain a general statement, replace `46' by `$⊤$'.
If $(L,R)$ is the slashing correspondent to $J$ and $J'$, and $D=cd$,
then:
%
$$\begin{array}{rcl}
I' &=& \setofst {ab∈H'} {a \eqL c ∧ b \eqR d} \\
I &=& \setofst {ab∈H'} {a \eqL c ∧ b \eqR d ∧ \obeys(ab,A) } \\
\end{array}
$$
%
so $I⊆I'$. We saw in sec.\ref{slash-max} an argument that shows that
$C=⋀I∈I$ and $E=⋁I∈I$, and that $B=⋀I'∈I'$ and $F=⋁I'∈I'$; $C$ and $E$
are the extremities of a smaller set, so $B≤C$ and $E≤F$ --- and
combining this $C≤D≤E$ we get $B≤C≤D≤E≤F$.
The interval $I'$ is a rectangle --- because it doesn't have an
`$\obeys$' clause --- with extremities $B$ and $F$, so $I'=[B,F]$. For
$ab∈H'$ the condition $\obeys(ab,A)$ is equivalent to $ab∈H$, so we
have:
%
$$\begin{array}{rclcl}
I' &=& \setofst {ab∈H'} {ab ∈ [B,F]} &=& [B,F] \\
I &=& \setofst {ab∈H'} {ab ∈ [B,F] ∧ ab∈H } &=& [B,F]∩H \\
\end{array}
$$
The extremities of $I$ are $C$ and $E$, and $[C,E]⊆[B,F]$, so
$I⊆[C,E]$, $I = [B,F]∩H = [C,E]∩([B,F]∩H) = ([C,E]∩[B,F])∩H =
[C,E]∩H$. In other notation, the extremities of $I$ are $E=J(D)$ and
$C=\co J(D)$, and the extremities of $I'$ are $F=J'(D)$ and $B=\co
J'(D)$; this yields a way to calculate $J(D)$ and $\co J(D)$:
%
$$\begin{array}{rcccccccccccc}
J(D) &=& ⋁I &=& ⋁([B,F]∩H) &=& ⋁([\co J'(D),J'(D)]∩H) \\
\co J(D) &=& ⋀I &=& ⋀([B,F]∩H) &=& ⋀([\co J'(D),J'(D)]∩H) \\
\end{array}
$$
% \end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
% ____ _ _
% | _ \ ___ | |_ _ | | ___ _ __ ___
% | |_) / _ \| | | | | _ | |_____ / _ \| '_ \/ __|
% | __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_| \___/|_|\__, | \___/ \___/| .__/|___/
% |___/ |_|
%
% «polynomial-J-ops» (to ".polynomial-J-ops")
\section{Polynomial J-operators}
\label {polynomial-J-ops}
% (ph2p 29 "polynomial-J-ops")
% (ph2 "polynomial-J-ops")
% (phop 22)
% (pho "J-examples")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 331) "polynomial")
\def\Jnotnot{{(¬¬)}}
\def\JiiR {{({→→}R)}}
\def\JoQ {{(∨Q)}}
\def\JiR {{({→}R)}}
\def\JfoQR {{(∨Q∧{→}R)}}
\def\JmiQ {({→→}Q∧{→}Q)}
{
It is not hard to check that for any Heyting Algebra $H$ and any
$Q,R∈H$ the operations $\Jnotnot$, $\ldots$, $\JfoQR$ below are
J-operators:
%
%$$\begin{array}{rclcrcl}
% (¬¬) &:=& λP{:}H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% \JiiR &:=& λP{:}H.((P{→}R){→}R) && \JiiR(P) &=& (P{→}R){→}R \\
% \JoQ &:=& λP{:}H.(P{∨}Q) && \JoQ(P) &=& P∨Q \\
% \JiR &:=& λP{:}H.(P{→}R) && \JiR(P) &=& P{→}R\\
% \JfoQR &:=& λP{:}H.((P{∨}Q) ∧ (P{→}R)) && \JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
%$$
%
$$\begin{array}{rclcrcl}
(¬¬)(P) &=& ¬¬P \\
\JiiR(P) &=& (P{→}R){→}R \\
\JoQ(P) &=& P∨Q \\
\JiR(P) &=& P{→}R\\
\JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
\end{array}
$$
Checking that they are J-operators means checking that each of them
obeys $\J1$, $\J2$, $\J3$. Let's define formally what are $\J1$, $\J2$
and $\J3$ ``for a given $F:H→H$'':
%
$$\begin{array}{rcc}
\J1_F &:=& (P ≤ F(P)) \\
\J2_F &:=& (F(P) = F(F(P)) \\
\J3_F &:=& (F(P∧P') = F(P)∧F(P')) \\
\end{array}
$$
%
and:
%
$$\J123_F \quad := \quad \J1_F ∧ \J2_F ∧ \J3_F.$$
Checking that $\Jnotnot$ obeys $\J1$, $\J2$, $\J3$ means proving
$\J123_\Jnotnot$ using only the rules from intuitionist logic from
sec.\ref{logic-in-HAs}; we will leave the proof of this, of and
$\J123_\JiiR$, $\J123_\JoQ$, and so on, to the reader.
\msk
The J-operator $\JfoQR$ is a particular case of building more complex
J-operators from simpler ones. If $J,K: H→H$, we define:
%
$$(J∧K) := λP{:}H.(J(P){∧}K(P))$$
%
it not hard to prove $\J123_{(J∧K)}$ from $\J123_J$ and $\J123_K$
using only the rules from intuitionistic logic.
\msk
The J-operators above are the first examples of J-operators in Fourman
and Scott's ``Sheaves and Logic'' (\cite{Fourman}); they appear in
pages 329--331, but with these names (our notation for them is at the
right):
(i) {\sl The closed quotient,}
$$J_a p = a ∨ p \qquad J_Q = \JoQ.$$
(ii) {\sl The open quotient,}
$$J^a p = a→p \qquad J^R = \JiR.$$
(iii) {\sl The Boolean quotient}.
$$B_a p = (p→a)→a \qquad B_R = \JiiR.$$
(iv) {\sl The forcing quotient}.
$$(J_a∧J^b)p = (a∨p)∧(b→p) \qquad (J_Q∧J^R) = \JfoQR.$$
(vi) {\sl A mixed quotient.}
$$(B_a∧J^a)p = (p→a)→p \qquad (B_Q∧J^Q) = \JmiQ.$$
\msk
The last one is tricky. From the definition of $B_a$ and $J^a$ what we
have is
%
$$(B_a∧J^a)p = ((p→a)→a)∧(a→p),$$
%
but it is possible to prove
%
$$((p→a)→a)∧(a→p) \;\;↔\;\; ((p→a)→p)$$
%
intuitionistically.
The operators above are ``polynomials on $P,Q,R,→,∧,∨,⊥$'' in the
terminology of Fourman/Scott: ``If we take a polynomial in $→,∧,∨,⊥$,
say, $f(p,a,b,\ldots)$, it is a decidable question whether for all
$a,b,\ldots$ it defines a J-operator'' (p.331).
\msk
When I started studying sheaves I spent several years without any
visual intuition about the J-operators above. I was saved by ZHAs and
brute force --- and the brute force method also helps in testing if a
polynomial (in the sense above) is a J-operator in a particular case.
For example, take the operators $λP{:}H.(P∧22)$ and $({∨}22)$ on
$H=[00,44]$:
%
% (phop 23)
% (pho "J-ops-diagrams")
% (pho "J-ops-diagrams" "jout")
% (find-dn6 "zhas.lua" "shortoperators-tests")
% (find-dn6file "zhas.lua" "mpnewJ =")
%
%L shortoperators()
%L mpnewF = function (opts, spec, J)
%L return mpnew(opts, spec, J):setz():zhaJ()
%L end
%L
%L mpnewF({def="fooa"}, "123454321", function (P) return And(v"22", P) end):output()
%L mpnewF({def="fooo"}, "123454321", Cloq(v"22")):output()
%L mpnewJ({def="fooO"}, "123454321", Cloq(v"22")):zhaPs("22"):output()
%
$$\pu
\begin{array}{rcccl}
λP{:}H.(P∧22) &=& \fooa \\ \\
({∨}22) &=& \fooo &=& \fooO \\
\end{array}
$$
The first one, $λP{:}H.(P∧22)$, is not a J-operator; one easy way to
see that is to look at the region in which the result is 22 --- its
top element is 44, and this violates the conditions on slash-operators
in sec.\ref{slash-ops}. The second operator, $({∨}22)$, is a slash
operator and a J-operator; at the right we introduce a convenient
notation for visualizing the action of a polynomial slash-operator, in
which we draw only the contours of the equivalence classes and the
constants that appear in the polynomial.
Using this new notation, we have:
%
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123R2L1", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123R2L1", Booq(v"11")):zhaPs("11"):output()
%L
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123454321", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123454321", Booq(v"22")):zhaPs("22"):output()
%L mpnewJ({def="foobor", scale="7pt", meta="s"}, "1234567654321", Cloq(v"42")):zhaPs("42"):output()
%L mpnewJ({def="foobim", scale="7pt", meta="s"}, "1234567654321", Opnq(v"24")):zhaPs("24"):output()
%L mpnewJ({def="foofor", scale="7pt", meta="s"}, "1234567654321", Forq(v"42", v"24")):zhaPs("42 24"):output()
%L mpnewJ({def="foomix", scale="7pt", meta="s"}, "12345654321", Mixq(v"22")):zhaPs("22"):output()
%
\pu
$$
\begin{array}{c}
(¬¬) \;\;=\;\;
({→→}00) \;\;=\;\; \fooboo \qquad \qquad
({→→}22) \;\;=\;\; \foobii \\
\\
({∨}42) \;\;=\;\; \foobor \qquad
({→}24) \;\;=\;\; \foobim \\[-20pt]
\\
({∨}42∧{→}24) \;\;=\;\; \foofor \\
\qquad \qquad
\qquad \qquad
\qquad \qquad
({→→}22∧{→}22) \;\;=\;\; \foomix \\
\end{array}
$$
Note that the slashing for $({∨}42∧{→}24)$ has all the cuts for
$({∨}42)$ plus all the cuts for $({→}24)$, and $({∨}42∧{→}24)$
``forces $42≤24$'' in the following sense: if $P^* = ({∨}42∧{→}24)(P)$
then $42^*≤24^*$.
}
% _ _ _
% _ __ (_) ___ ___ ___ __ _| | __ _ ___| |__ _ __ __ _
% | '_ \| |/ __/ __/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_) | | (_| (__\__ \ | (_| | | (_| | __/ |_) | | | (_| |
% | .__/|_|\___\___|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-piccs» (to ".algebra-of-piccs")
\section{An algebra of piccs}
\label {algebra-of-piccs}
We saw in the last section a case in which $(J∧K)$ has all the cuts
from $J$ plus all the cuts from $K$; this suggests that we {\sl may}
have an operation dual to that, that behaves as this: $(J∨K)$ has
exactly the cuts that are both in $J$ and in $K$:
%
$$\begin{array}{rcl}
\Cuts(J∧K) &=& \Cuts(J)∪\Cuts(K) \\
\Cuts(J∨K) &=& \Cuts(J)∩\Cuts(K) \\
\end{array}
$$
And it $J_1, \ldots, J_n$ are all the slash-operators on a given ZHA,
then
%
$$\begin{array}{rclcl}
\Cuts(J_1∧\ldots∧J_n) &=& \Cuts(J_1)∪\ldots∪\Cuts(J_k) &=& \text{(all cuts)} \\
\Cuts(J_1∨\ldots∨J_n) &=& \Cuts(J_1)∩\ldots∩\Cuts(J_k) &=& \text{(no cuts)} \\
\end{array}
$$
%
yield the minimal element and the maximal element, respectively, of an
algebra of slash-operators; note that the slash-operator with ``all
cuts'' is the identity map $λP{:H}.P$, and the slash-operator with
``no cuts'' is the one that takes all elements to $⊤$: $λP{:H}.⊤$.
This yields a lattice of slash-operators, in which the partial order
is $J≤K$ iff $\Cuts(J) ⊇ \Cuts(K)$. This is somewhat counterintuitive
if we think in terms of cuts --- the order seems to be reversed ---
but it makes a lot of sense if we think in terms of piccs
(sec.\ref{piccs-and-slashings}) instead.
\msk
Each picc $P$ on $\{0,\ldots,n\}$ has an associated function $·^P$
that takes each element to the top element of its equivalence class.
If we define $P≤P'$ to mean $∀a∈\{0,\ldots,n\}.\,a^P≤a^{P'}$, then we
have this:
%
% (pho "algebra-of-piccs")
% (phop 25 "algebra-of-piccs")
%
%L partitiongraph = function (opts, spec, ylabel)
%L local mp = MixedPicture.new(opts)
%L for y=0,5 do mp:put(v(-1, y), y.."") end
%L for x=0,5 do mp:put(v(x, -1), x.."") end
%L for a=0,5 do local aP = spec:sub(a+1, a+1)+0; mp:put(v(a, aP), "*") end
%L mp.lp:addlineorvector(v(0, 0), v(6, 0), "vector")
%L mp.lp:addlineorvector(v(0, 0), v(0, 6.5), "vector")
%L mp:put(v(7, 0), "a")
%L mp:put(v(0, 7), "aP", ylabel)
%L return mp
%L end
%L pg = function (def, spec, ylabel)
%L return partitiongraph({def=def, scale="5pt", meta="s"}, spec, ylabel)
%L end
%L
%L pg("grapha", "012345", "a^P" ):output()
%L pg("graphb", "113355", "a^{P'}" ):output()
%L pg("graphc", "115555", "a^{P''}" ):output()
%L pg("graphd", "555555", "a^{P'''}"):output()
%L
%
% a^P a^P a^P a^P
% ^ ^ ^ ^
% 5 | * 5 | * * 5 | * * * * 5 * * * * * *
% 4 | * 4 | 4 | 4 |
% 3 | * <= 3 | * * <= 3 | <= 3 |
% 2 | * 2 | 2 | 2 |
% 1 | * 1 * * 1 * * 1 |
% 0 *----------> a 0 +----------> a 0 +----------> a 0 +----------> a
% 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5
%
% 0|1|2|3|4|5 <= 01|23|45 <= 01|2345 012345
%
$$\pu
\begin{array}{ccccccc}
\grapha &≤& \graphb &≤& \graphc &≤& \graphd \\ \\
0|1|2|3|4|5 &≤& 01|23|45 &≤& 01|2345 &≤& 012345 \\
P &≤& P' &≤& P'' &≤& P''' \\
\end{array}
$$
This yields a partial order on piccs, whose bottom element is the
identity function $0|1|2|\ldots|n$, and the top element is $012\ldots
n$, that takes all elements to $n$.
The piccs on $\{0,\ldots,n\}$ form a Heyting Algebra, where
$⊤=01\ldots n$, $⊥=0|1|\ldots|n$, and `$∧$' and `$∨$' are the
operations that we have discussed above; it is possible to define a
`$→$' there, but this `$→$' is not going to be useful for us and we
are mentioning it just as a curiosity. We have, for example:
%
%D diagram algebra-of-piccs
%D 2Dx 100 +20 +20 +30 +20 +20
%D 2D 100 01234 T
%D 2D ^ ^
%D 2D | |
%D 2D +20 01|234 PvQ
%D 2D ^ ^ ^ ^
%D 2D / \ / \
%D 2D +20 0|1|234 01|2|34 P Q
%D 2D ^ ^ ^ ^
%D 2D \ / \ /
%D 2D +20 0|1|2|34 P&Q
%D 2D ^ ^
%D 2D | |
%D 2D +20 0|1|2|3|4 bot
%D 2D
%D (( T .tex= ⊤ PvQ .tex= P∨Q P&Q .tex= P∧Q bot .tex= ⊥
%D 01234 01|234 <- T PvQ <-
%D 01|234 0|1|234 <- 01|234 01|2|34 <- PvQ P <- PvQ Q <-
%D 0|1|234 0|1|2|34 <- 01|2|34 0|1|2|34 <- P P&Q <- Q P&Q <-
%D 0|1|2|34 0|1|2|3|4 <- P&Q bot <-
%D
%D ))
%D enddiagram
%D
$$\pu \diag{algebra-of-piccs}$$
% _ _ _
% | | ___ _ __ ___ __ _| | __ _ ___| |__ _ __ __ _
% _ | |_____ / _ \| '_ \/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | __/ |_) | | | (_| |
% \___/ \___/| .__/|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-J-ops» (to ".algebra-of-J-ops")
\section{An algebra of J-operators}
\label {algebra-of-J-ops}
% Bad (ph2p 50 "algebra-of-J-ops")
% (find-books "__cats/__cats.el" "fourman")
Fourman and Scott define the operations $∧$ and $∨$ on J-operators in
pages 325 and 329 (\cite{Fourman}), and in page 331 they list ten
properties of the algebra of J-operators:
%
$$
\def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
\def\li#1 #2 #3 #4 {\text{#1}& }
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} && (∨21)∨(∨12)=(∨22) \\
\li (ii) J^a∨J^b = J^{a∧b} && ({→}32)∨({→}23)=({→}22) \\
\li (iii) J_a∧J_b = J_{a∧b} && (∨21)∧(∨12)=(∨11) \\
\li (iv) J^a∧J^b = J^{a∨b} && ({→}32)∧({→}23)=({→}33) \\
\li (v) J_a∧J^a = ⊥ && (∨22)∧({→}22)=(⊥) \\
\li (vi) J_a∨J^a = ⊤ && (∨22)∨({→}22)=(⊤) \\
\li (vii) J_a∨K = K∘J_a \\
\li (viii) J^a∨K = J^a∘K \\
\li (ix) J_a∨B_a = B_a \\
\li (x) J^a∨B_b = B_{a→b} \\
\end{array}
$$
% (pho "J-ops-algebra-2")
% (phop 28 "J-ops-algebra-2")
The first six are easy to visualize; we won't treat the four last
ones. In the right column of the table above we've put a particular
case of (i), $\ldots$, (vi) in our notation, and the figures below put
all together.
In Fourman and Scott's notation,
%D diagram J-alg-1
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D ren T ==> J_⊤=⊤=J^⊥
%D ren A E ==> J_{22} J^{22}
%D ren B C F G ==> J_{21} J_{12} J^{32} J^{23}
%D ren D H ==> J_{11} J^{11}
%D ren bot ==> J_⊥=⊥=J^⊤
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-1}
$$
%
in our notation,
%
%D diagram J-alg-2
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D 2Dx 100 +20 +20 +15 +15 +20 +20
%D 2D 100 T
%D 2D +35 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +35 bot
%D 2D
%D ren T ==> (⊤∨)=(λP.⊤)=(⊥{→})
%D ren A E ==> (22∨) (22{→})
%D ren B C F G ==> (21∨) (12∨) (32{→}) (23{→})
%D ren D H ==> (11∨) (33{→})
%D ren bot ==> (⊥∨)=(λP.P)=(⊤{→})
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-2}
$$
%
and drawing the polynomial J-operators as in
sec.\ref{polynomial-J-ops}:
%
%L deforp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Cloq(v(P))):zhaPs(draw):print():output()
%L end
%L defimp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Opnq(v(P))):zhaPs(draw):print():output()
%L end
%L deforp("21", "21", "ora")
%L deforp("22", "22", "orb")
%L deforp("11", "11", "orc")
%L deforp("12", "12", "ord")
%L deforp("00", "", "orB")
%L defimp("32", "32", "ima")
%L defimp("22", "22", "imb")
%L defimp("33", "33", "imc")
%L defimp("34", "34", "imd")
%L defimp("00", "", "imB")
%
%R local algebra =
%R 4/ !imB \
%R | |
%R | !orb !imb |
%R |!ora !ord !ima !imd|
%R | !orc !imc |
%R | |
%R \ !orB /
%R
%R algebra:tomp({def="foo", scale="30pt"}):addcells():output()
$$\pu
% \bhbox{$
\begin{array}{c}
\\
\foo \\
\\
\end{array}
% $}
$$
% $$
% \def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
% \begin{array}{rlclcrlclc}
% \li (i) J_a∨J_b = J_{a∨b} (ii) J^a∨J^b = J^{a∧b}
% \li (iii) J_a∧J_b = J_{a∧b} (iv) J^a∧J^b = J^{a∨b}
% \li (v) J_a∧J^a = ⊥ (vi) J_a∨J^a = ⊤
% \li (vii) J_a∨K = K∘J_a (viii) J^a∨K = J^a∘K
% \li (ix) J_a∨B_a = B_a (x) J^a∨B_b = B_{a→b}
% \end{array}
% $$
%
% $$\begin{array}{rclcrcl}
% (¬¬) &:=& λP:H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% (→→R) &:=& λP:H.((P{→}R){→}R) && (→→R)(P) &=& (P{→}R){→}R \\
% (∨Q) &:=& λP:H.(P{∨}Q) && (∨Q)(P) &=& P∨Q \\
% (→R) &:=& λP:H.(P{→}R) && (→R)(P) &=& P{→}R\\
% (∨Q∧→R) &:=& λP:H.((P{∨}Q) ∧ (P{→}R)) && (∨Q∧→R)(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
% $$
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ ___ | |_ _
% \___ \| |/ _` / __| '_ \ | '_ \ / _ \| | | | |
% ___) | | (_| \__ \ | | | | |_) | (_) | | |_| |
% |____/|_|\__,_|___/_| |_| | .__/ \___/|_|\__, |
% |_| |___/
% «slashings-are-poly» (to ".slashings-are-poly")
\section{All slash-operators are polynomial}
\label {slashings-are-poly}
% (ph2p 51 "slashings-are-poly")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 30)
% (find-LATEX "2015planar-has.tex" "zquotients-poly")
{
%L local ba, bb, bc = Booq(v"04"), Booq(v"23"), Booq(v"45")
%L local babc = Jand(ba, Jand(bb, bc))
%L mpnewJ({def="slaT", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):addlrs() :output():print()
%L mpnewJ({def="slaA", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):addlrs() :output():print()
%L mpnewJ({def="slaB", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):addlrs() :output():print()
%L mpnewJ({def="slaC", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):addlrs() :output():print()
%L mpnewJ({def="fooa", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):zhaPs("04") :output():print()
%L mpnewJ({def="foob", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):zhaPs("23") :output():print()
%L mpnewJ({def="fooc", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):zhaPs("45") :output():print()
%L mpnewJ({def="food", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):zhaPs("04 23 45"):output():print()
%L mpnew ({def="fooe", scale="7pt", meta="s"}, "1R2R3212RL1" ):addlrs():output()
%L mpnewJ({def="foof", scale="7pt", meta="s"}, "1R2R3212RL1", babc):zhaJ() :output()
\pu
Here is an easy way to see that all slashings --- i.e., J-operators on
ZHAs --- are polynomial. Every slashing $J$ has only a finite number of
cuts; call them $J_1, \ldots, J_n$. For example:
%
$$J=\slaT \qquad J_1=\slaA \quad J_2=\slaB \quad J_3=\slaC$$
Each cut $J_i$ divides the ZHA into an upper region and a lower
region, and $J_i(00)$ yields the top element of the lower region.
Also, $({→→}J_i(00))$ is a polynomial way of expressing that cut:
%
$$\def\foo#1#2{
\begin{array}{rr}
J_#1= \\
% ({→→}J_#1(00))= \\
(→→#2)= \\
\end{array}}
\foo1{04} \fooa \quad
\foo2{23} \foob \quad
\foo3{45} \fooc
$$
The conjunction of these `$({→→}J_i(00))$'s yields the original
slashing:
%
% $$
% \begin{array}{c}
% \fooa ∧ \foob ∧ \fooc = \food
% \end{array}
% $$
%
$$(→→04)∧(→→23)∧(→→45) = \food = J$$
}
\newpage
\end{document}
% ___ _ __
% / _ \ _ __ ___ _ __ ___ ___ ___| |_ ___ ___ / _| __ _
% | | | | '_ \ / _ \ '_ \/ __| / __|/ _ \ __/ __| / _ \| |_ / _` |
% | |_| | |_) | __/ | | \__ \ \__ \ __/ |_\__ \ | (_) | _| | (_| |
% \___/| .__/ \___|_| |_|___/ |___/\___|\__|___/ \___/|_| \__,_|
% |_|
%
% «open-sets-of-a-certain-form» (to ".open-sets-of-a-certain-form")
\section{Open sets of a certain form}
\label {open-sets-of-a-certain-form}
A 2-column graph with question marks (a ``2CGQ'') is a triple $((P,A),
B, D)$, where $(P,A)$ is a 2CG and $B⊆D⊆P$; let $G=((P,A), B, D)$. We
represent $G$ graphically like $(P,A)$, but with `0's, `?'s and '1's
on the points of $P$, and the expression ``$C$ is of the form $G$''
means $B⊆C⊆D$. For example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgbig("tcgL"):strs("0 1", "1 0 0"):vs():hs():output()
%L tcgbig("tcgR"):strs("0 ?", "1 ? 0"):vs():hs():output()
$$\pu
\tcgL \;\; \text{is of the form} \;\; \tcgR
$$
Informally, a `0' in the graphical representation of a 2CGQ $Q$ means
``all `$C$'s of the form $G$ have a `0' here'', a `1' means ``all
`$C$'s of the form $G$ have a `1' here'', and a `?' means ``some
`$C$'s of the form $G$ have `0's there and some have `1's''. More
formally, a 2CGQ $G$ corresponds to a partition of $P$ into $P_0$,
$P_1$ and $P_?$ --- the sets of `0's, `1's and `?'s of the graphical
representation of $G$ --- and we have $P_1=B$, $P_?=D∖B$, $P_0=P∖D$,
$D=P_1∪P_?$.
Our main use for 2CGQs will be for giving us a nice notation for ``the
set of open sets of $(P,A)$ betwen $B$ and $D$'':
%
$$\OPENSPABD \;\; = \;\; \setofst{U⊆P}{B⊆U⊆D \text{ and } U∈\Opens_A(P)}$$
Note that adding intercolumn arrows reduce sets of
opens sets,
%
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcg_spec = "6, 6; 43, "
%L tcgmed("tcgB"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcg_spec = "6, 6; 43, 54"
%L tcgmed("tcgC"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%
$$\pu
\OPENS\tcgA \;⊇\;
\OPENS\tcgB \;⊇\;
\OPENS\tcgC
$$
%
because each arrow is a ``restriction'' (sec.\ref{topologies-on-2CGs})
on what is considered an open set. We can propagate `1's forward along
arrows like `$1→?$' and `0's backward along arrows like `$?→0$'
without changing the result of `$\OPENS(\ldots)$':
%
%L tcg_spec = "6, 6; 43, "
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgB"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgL" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgR" ):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$
\pu
\OPENS\tcgA = \OPENS\tcgB
\qquad
\OPENS\tcgL = \OPENS\tcgR
$$
% ____ _ _
% | _ \ _ __ ___ _ __ __ _ __ _ __ _| |_(_) ___ _ __
% | |_) | '__/ _ \| '_ \ / _` |/ _` |/ _` | __| |/ _ \| '_ \
% | __/| | | (_) | |_) | (_| | (_| | (_| | |_| | (_) | | | |
% |_| |_| \___/| .__/ \__,_|\__, |\__,_|\__|_|\___/|_| |_|
% |_| |___/
%
% «propagation» (to ".propagation")
% (ph2p 31 "propagation")
\section{Propagation}
\label{propagation}
Fix a 2CG $(P,A)$. There are two good, natural ways to get rid of all
arrows `$1→0$' in a subset $C⊆P$: one, called `$\propagate_{1,(P,A)}$'
or `$\propagate_{1}$', ``propagates the `1's forward'', and the other
one, called `$\propagate_{0}$' or `$\propagate_{1,(P,A)}$',
``propagates the `0's backward''. An example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgmed("tcgC"):strs("0 1", "1 0 0"):hs():output()
%L tcgmed("tcgD"):strs("1 1", "1 1 0"):hs():output()
%L tcgmed("tcgB"):strs("0 0", "1 0 0"):hs():output()
%
$$\pu
\propagate_0\tcgC = \tcgB
\qquad
\propagate_1\tcgC = \tcgD
$$
It easy to see that $\propagate_1(C)$ returns the smallest open set
containing $C$, and $\propagate_0(C)$ returns the largest open set
contained in $C$,
The {\sl interior} of a set $S$ in a topology $\calU$ on $P$ is the
biggest open set in $\calU$ contained in $S$, and, dually, the {\sl
cointerior} of a set $S$ is the smallest open set in $\calU$
containing $S$. In finite topologies cointeriors always exist.
\msk
{\sl Theorem 1.} For any 2CG $(P,A)$ and $S⊆P$ we have
%
$$\Int(S) = \propagate_0(S) ⊆ S ⊆ \propagate_1(S) = \coInt(S).$$
\msk
We can define propagations for 2CGQs in a way that changes only the
`?'s. If $G=((P,A),B,D)$ is a 2CGQ, then $\propagate_1(G)$ propagates
forward only the `1's in arrows like `$1→?$', and $\propagate_0(G)$
propagates backward only the `0's in arrows like `$?→0$'.
The operations `$\propagate_1$' and `$\propagate_0$' on 2CGQs need not
commute:
%
%L tcg_spec = "2, 2; 12, "
%L tcgmed("tcgN"):strs("? 1", "0 ?"):hs():output()
%L tcgmed("tcgZ"):strs("0 1", "0 0"):hs():output()
%L tcgmed("tcgO"):strs("1 1", "0 1"):hs():output()
$$\pu
% \propagate_1\left(\propagate_0 \tcgN\right)
% = \tcgZ ≠ \tcgO =
% \propagate_0\left(\propagate_1 \tcgN\right)
\begin{array}{rcl}
\propagate_1\left(\propagate_0 \tcgN\right) &=& \tcgZ \\ \\
\propagate_0\left(\propagate_1 \tcgN\right) &=& \tcgO \\
\end{array}
$$
%
but they can only fail to commute when $\OPENS(G)=∅$. When they
commute we will write their composite as `$\propagate$'.
\msk
{\sl Theorem 2.} Let $G=((P,A),B,D)$ be a 2CGQ with $\OPENS(G)≠∅$ and
let $G' = \propagate(G) = \OPENS((P,A), B', D')$, $P'_1=B'$,
$P'_?=D'∖B'$, $P'_1=P∖D'$. Then:
% Suppose that $\OPENS(G)≠∅$ and let $G' =
% \propagate(G) = \OPENS((P,A), \linebreak[0] B', D')$. Then:
a) In $G'$ everything below a `1' is also `1',
b) In $G'$ everything above a `0' is also `0',
c) $B' = P'_1$ is an open set,
d) $D' = P'_1∪P'_? = P∖P'_0$ is an open set,
e) $B' = \propagate_1(B) = \coInt(B)$,
f) $D' = \propagate_0(D) = \Int(D)$,
g) $B' = \pile(ab)$ for some $ab$,
h) $D' = \pile(ef)$ for some $ef$,
i) $B' ∈ \OPENS(G) = \OPENS(G')$,
j) $D' ∈ \OPENS(G) = \OPENS(G')$.
\msk
An example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
%L mp = mpnew({def="foo", meta="s", scale="7pt"}, "1R2R3212RL1"):addlrs():output()
%
$$\pu
\begin{array}{c}
G = \tcgG
\qquad
G' = \propagate(G) = \tcgGGG = ((P,A), \pile(11), \pile(23))
\\
% \OPENS(G) = \OPENS(G')
% \quad
% \two/<-`->/<300>^{\pile}_{\pile^{-1}}
% \quad
% [11,23]∩\;\;\foo \\
\end{array}
$$
\msk
The next theorem translates this to ZHAs, and shows that when
$\OPENS(G)≠∅$ then it returns an interval in a ZHA (in the sense of
sec.\ref{piccs-and-slashings}),
\msk
{\sl Theorem 3.} Let $G=((P,A),B,D)$ be a 2CGQ with $\OPENS(G)≠∅$ and
let $G' = \propagate(G) = \OPENS((P,A), B', D')$, $ab=\pile^{-1}(B')$,
$ef=\pile^{-1}(D')$, $I = \pile^{-1}(\OPENS(G)) =
\pile^{-1}(\OPENS(G'))$, and let $H$ be the ZHA generated by $(P,A)$,
i.e., $H=\pile^{-1}(\Opens_A(P))$. Then:
a) $ab$ is the minimal point of $I$,
b) $ef$ is the maximal point of $I$,
c) $I⊆H$,
d) $I=[ab,ef]∩H$,
e) if $A$ has no intercolumn arrows then $I=[ab,ef]$.
\msk
With Theorem 3 we can extend the last example to:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
%L mp = mpnew({def="foo", meta="s", scale="7pt"}, "1R2R3212RL1"):addlrs():output()
%
$$\pu
\begin{array}{c}
G = \tcgG
\qquad
G' = \propagate(G) = \tcgGGG = ((P,A), \pile(11), \pile(23))
\\
\OPENS(G) = \OPENS(G') = I
\quad
\two/<-`->/<300>^{\pile}_{\pile^{-1}}
\quad
[11,23]∩\;\;\foo \\
\end{array}
$$
In the next sections we will see that in some important cases the
results of $\OPENS(\ldots)$ coincide with J-equivalence classes.
% ____ _ _ _ _
% | _ \ ___| | _____ ____ _ _ __ | |_ _ __ ___ (_)_ __ | |_ ___
% | |_) / _ \ |/ _ \ \ / / _` | '_ \| __| | '_ \ / _ \| | '_ \| __/ __|
% | _ < __/ | __/\ V / (_| | | | | |_ | |_) | (_) | | | | | |_\__ \
% |_| \_\___|_|\___| \_/ \__,_|_| |_|\__| | .__/ \___/|_|_| |_|\__|___/
% |_|
%
% «relevant-points» (to ".relevant-points")
% (ph2p 33 "relevant-points")
% \section{The set of relevant points of a J-operator}
\section{The set of relevant points of a slashing}
We saw in sec.\ref{piccs-and-slashings} that a slashing on a ZHA $H$
can be represented a pair $(L,R)$ of piccs, that we drew in a V-shaped
diagram; let's write $S$ for the set of numbers above the cuts in the
V-shaped diagram, converting them to the notation for elements of the
left and the right columns of 2-column graphs:
%
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="vcuts"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
$$\pu
J = \ZQuotients
\qquad
(L,R) = \vcuts
\qquad
S = \{1\_, \; \_4, \_6\}
$$
We also saw (sec.\ref{J-ops-and-regions}) that on ZHAs there is a
bijection between slashings and J-operators. Let $\relevant(J)$ be the
operation that obtains the set $S$ for a J-operator $J$: $\relevant(J)
= \{1\_, \; \_4, \_6\}$ for the $J$ above. We will call $S⊆P$ the {\sl
set of relevant points} of the J-operator $J$, and $Q = \qmarks(J)
=P∖S$ will be the {\sl set of (points that will be replaced by)
question marks} by $J$. Note that we can also go from a set $Q⊆P$ to
a slashing and a J-operator, but we will not need a notation for that.
We can define the operation that receives a $C⊆P$ and ``forgets the
information on the points of $Q$'' on $C$, returning a 2CGQ, as:
%
$$\forget_{(P,A),Q}(C) \;\; = \;\; ((P,A), C∖Q, C∪Q)$$
%
for example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
$$\pu
\forget_{(P,A),Q}(\pile(12)) = \tcgG
$$
Note that
%
%L tcg_spec = "4, 6; , "
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgGP" ):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$\pu
\begin{array}{rcl}
\propagate(\forget_{(P,A),Q}(\pile(12))) &=& \tcgGP \\
&=& ((P,A), \pile(11), \pile(23))
\end{array}
$$
%
and that:
%
$$\begin{array}{rcl}
\pile^{-1}(\OPENS(\propagate(\forget_{(P,A),Q}(\pile(12))))) &=& [11,23]∩H \\
&=& [\co J(12), J(12)]∩H \\
&=& [12]^J \\
\end{array}
$$
%
this holds in general, as we will see soon.
% and when we apply $\OPENS$ (and $\pile^{-1}$) to that we get exactly
% $[11,23]∩H$, which is the J-equivalence class of 12 --- this happens
% always, but the easiest way to understand why is to start with {\sl
% rectangular} ZHAs.
% ____ _ _
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__|
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | |
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_|
% |___/
%
% «rectangular-versions» (to ".rectangular-versions")
% (ph2p 34 "rectangular-versions")
\section{Rectangular versions}
\label{rectangular-versions}
The ``rectangular version'' of a 2CG, a ZHA and a J-operator are
defined as this. Let $(P,A)$ be a 2CG and $H$ its associated ZHA, and
$J:H→H$ a J-operator on $H$; then $A'$ is $A$ minus its intercolumn
arrows, $H'$ is the (rectangular) ZHA associated to $(P,A')$, and
$J':H'→H'$ is J-operator on $H'$ that has the same cuts as $J$. The
primes on $A'$, $H'$ and $J'$ will always mean from here on that we
are on the rectangular versions. Let $Q=\qmarks(J)=\qmarks(J')$.
The rectangular versions for the $(P,A)$ and the $J$ that we are using
in our examples are:
%
%L tcg_spec = "4, 6; , "
%L tcgbig("tcgRect" ):lrs():vs():hs():output()
%L mp = mpnew({def="ZRect"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
(P,A') = \tcgRect
\qquad
J' = \ZRect
\;\;.
$$
Take any $C⊆P$, The result of $\forget_{(P,A'),Q}(C)$ is always of
this form,
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGF" ):strs("a ? ? ?", "? ? ? b ? c"):hs():output()
$$\pu
% \propagate(\forget_{(P,A'),Q}(C)) = \tcgGF
\forget_{(P,A'),Q}(C) = \tcgGF
$$
%
for some $a,b,c∈\{0,1\}$; moreover, if $C$ is open then
$\forget_{(P,A'),Q}(C)$ doesn't have `1's above `0's. Take any $C⊆P$
open in $(P,A)$; $C$ will be of the form $\pile(cd)$ for some $cd∈H'$.
Let $G=\forget_{(P,A'),Q}(C)$. The action of $\propagate$ on `$G$'s of
this form is particularly simple: each column of $G$ is made of blocks
of consecutive `?'s separated by `0's or `1's, and $\propagate$ acts
homogeneously on each block, leaving `?'s in at most one block in each
column. For example, if $a=b=1$ and $c=0$ then
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGF" ):strs("1 ? ? ?", "1 1 1 1 ? 0"):hs():output()
$$\pu
\propagate(\forget_{(P,A'),Q}(C)) = \tcgGF
$$
It is easy to see that:
\msk
{\sl Theorem 1.} If $C=\pile(cd)$ then
$\pile^{-1}(\OPENS(\propagate(\forget_{(P,A'),Q}(C))))$ is a
$J'$-equivalence class.
\msk
{\sl Theorem 2.} If $C=\pile(cd)$ then
$\pile^{-1}(\OPENS(\propagate(\forget_{(P,A'),Q}(C))))$ is $[\co
J'(cd), J'(cd)]$.
\msk
{\sl Theorem 3.} Suppose that $cd∈H$ (instead of $cd∈H'$) and let:
%
$$\begin{array}{rcl}
C &=& \pile(cd) \\
G &=& \forget_{(P,A'),Q}(C) \\
G' &=& \propagate(\forget_{(P,A'),Q}(C)) \\
G'' &=& \propagate(\forget_{(P,A ),Q}(C)) \\
I' &=& \pile^{-1}(\OPENS(G')) \\
I'' &=& \pile^{-1}(\OPENS(G'')) \\
\end{array}
$$
%
then $G'$ is a ``rectangular'' (and ``propagated'') 2CGQ, and $I'=[\co
J'(cd), J'(cd)]$ is a ``rectangular interval''; $G''$ is $G'$ plus
the intercolumn arrows, and with the propagations having been done
through the intercolumn arrows too. It is not hard to see that:
a) $\OPENS(G) = \OPENS(G') ⊇ \OPENS(G'')$
b) $I'' = I'∩H$
c) $cd∈I''$
d) $I'' = [\co J(cd), J(cd)]∩H$
e) $\pile(\co J(cd)), \pile(J(cd)) ∈ I''$
f) $G'' = ((P,A), \pile(\co J(cd)), \pile(J(cd)))$
g) $G'' = ((P,A), \coInt(C∖Q), \Int(C∪Q))$, so:
h) $\pile(\co J(cd)) = \coInt(C∖Q) = \propagate_1(C∖Q)$ and
i) $\pile(J(cd)) = \Int(C∪Q) = \propagate_0(C∪Q)$,
j) $\co J(cd)) = \pile^{-1}(\coInt(C∖Q)) = \pile^{-1}(\propagate_1(C∖Q))$ and
k) $J(cd) = \pile^{-1}(\Int(C∪Q)) = \pile^{-1}(\propagate_0(C∪Q))$.
\msk
A way to visualize what Theorem 3 means is to define $B, B', B'', D,
D' D''$ like this:
%
$$\begin{array}{rcl}
(B,D) &=& (C∖Q, C∪Q) \\
G' &=& ((P,A'),B',D') \\
G'' &=& ((P,A),B'',D'') \\
\end{array}
$$
%
%L mp = mpnew({def="ZRect", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"10", "B'") :put(v"43", "D'") :output()
%L mp = mpnew({def="ZOrig", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"11", "B''"):put(v"23", "D''") :output()
%L mp = mpnew({def="ZHAJR", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%L mp = mpnew({def="ZHAJ", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%
then, in the example we are using, omitting some `$\pile$'s and
`$\pile^{-1}$'s, we have:
%
$$\pu
J=\ZHAJ
\quad
J'=\ZHAJR
\quad
\ZRect
\quad
\ZOrig
$$
%
Theorem 3 shows several ways to calculate $B', C', B'', C''$.
% _ ____ ____ ____
% ___ _ _| |__ |___ \ / ___/ ___|___
% / __| | | | '_ \ _____ __) | | | | _/ __|
% \__ \ |_| | |_) |_____/ __/| |__| |_| \__ \
% |___/\__,_|_.__/ |_____|\____\____|___/
%
% «sub-2CGs» (to ".sub-2CGs")
\section{Sub-2-column graphs}
\label{sub-2CGs}
% (ph2p 35 "sub-2CGs")
Another way to understand the properties of the operation
$\forget_{(P,A),Q}$ is to think that it relates two topologies,
$\Opens_A(P)$ and $\Opens_{A|_S}(S)$ (mnemonic: $S$ is a ``smaller
set'', and $S = \relevant(J) = P∖Q$). We will sometimes denote
$\Opens_A(P)$ and $\Opens_{A|_S}(S)$ as just $\Opens(P)$ and
$\Opens(S)$; $\Opens(S)$ is a restriction of $\Opens(P)$ to $S$ in the
following sense: the open sets of $\Opens(S)$ are exactly the sets of
the form $U∩S$, where $U∈\Opens_A(P)$.
The topology $\Opens(S) = \Opens_{A|_S}(S)$ comes from a
``sub-2-column graph'' $(S,A|_S)$ of $(P,A)$, where the set of arrows
$A|_S$ can be obtained from $A$ and $S$ by
%
$$A|_S \;\;:=\;\; (A^*∩(S×S))^\ess,$$
%
which means: take the transitive-reflexive closure $A^*$ of $A$, which
yields a partial order on $P$, and restrict that order to $S$ by
taking $A^*∩(S×S)$; then (note: this last step is optional!) drop the
redundant arrows in $A^*∩(S×S)$ and keep only the ``essential'' ones,
which are the ones that can't be deleted without changing the order.
For clarity, we will draw the arrows in $(S,A|_S)$ as in the original
2CG $(P,A)$, even though some arrows may look as coming from or going
to nonexistent points; a really honest drawing of $(S,A|_S)$ in the
example below would be the one at the right, that has only one
intercolumn arrow, $1\_←\_6$, and only one vertical arrow, $\_6→\_4$.
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgP") :lrs():hs():vs():output()
%L tcgbig("tcgS"):strs("1\\_ · · ·", "· · · \\_4 · \\_6"):hs():vs():output()
%L tcg_spec = "4, 6; , 16"
%L local tcg =
%L tcgbig("tcgr"):strs("1\\_ {} {} {}", "{} {} {} \\_4 {} \\_6")
%L tcg:arrow(tcg:R(6), tcg:L(1), 0.07)
%L tcg:arrow(tcg:R(6), tcg:R(4), 0.17)
%L tcg:output()
%
$$
\pu
(P,A) = \tcgP
\qquad
(S,A|_S) = \tcgS = \tcgr
$$
A {\sl sub-2-column graph} is a graph $(S,A|_S)$ generated by a 2CG
$(P,A)$ and an $S⊆P$ by the procedure above: $A|_S =
(A^*∩(S×S))^\ess$.
\msk
{\sl Theorem 1.} Fix a ZHA $H$ and a J-operator $J$ on it, and from
that produce $(P,A)$, $\calU=\Opens_A(P)$, $S$, and $Q$. We clearly
have bijections between:
$\begin{tabular}{l}
1) the set of fixed points of $J$, $\setofst{ef∈H}{J(ef)=ef}$, \\
2) the set of fixed points of $\co J$, $\setofst{ab∈H}{\co J(ab)=ab}$, \\
3) the image of $J$, $J(H) = \setofst{J(cd)}{cd∈H}$, \\
4) the image of $\co J$, $\co J(H) = \setofst{\co J(cd)}{cd∈H}$, \\
5) the set of J-equivalence classes of $H$, $H/J = \setofst{[cd]^J}{cd∈H}$, \\
6) the elements $ef∈H$ such that $\pile(ef) = \Int(\pile(ef)∪Q)$, \\
7) the elements $ab∈H$ such that $\pile(ab) = \coInt(\pile(ab)∖Q)$, \\
8) the sets $U⊆\Opens(P)$ such that $U = \Int(U∪Q)$, \\
9) the sets $W⊆\Opens(P)$ such that $W = \coInt(W∖Q)$, \\
10) the sets $U⊆P$ such that $U = \Int(U∪Q)$, \\
11) the sets $W⊆P$ such that $W = \coInt(W∖Q)$, \\
12) the opens sets in $\Opens(S)$.
\end{tabular}
$
\msk
The partial order on $\Opens(S)$ is given by inclusion; some of the
corresponding partial orders on the other sets of Theorem 1 are not so
obvious.
\msk
{\sl Theorem 2}. Let $ab,cd∈H$, $A=\pile(ab)$, $B=\pile(cd)$,
$A'=A∩S$, $B'=B∩S$. The following are all equivalent:
1) $A'⊆B'$,
2) $A∖Q⊆B∖Q$,
2') $A∪Q⊆B∪Q$,
3) $\coInt(A∖Q)⊆\coInt(B∖Q)$,
3') $\Int(A∪Q)⊆\Int(B∪Q)$,
4) $\propagate_1(A∖Q)⊆\propagate_1(B∖Q)$
4') $\propagate_0(A∪Q)⊆\propagate_0(B∪Q)$
5) $\co J(ab) ≤ \co J(cd)$,
5') $J(ab)≤J(cd)$,
6) $\inf([ab]^J) ≤ \inf([cd]^J)$,
6') $\sup([ab]^J) ≤ \sup([cd]^J)$.
\msk
Items 6 and 6' give us a way to endow $H/J$ with a partial order.
Remember that $\sup([ab]^J) = J(ab)$ and $\inf([ab]^J) = \co J(ab)$;
we say that $[ab]^J ≤ [cd]^J$ when $J(ab) ≤ J(cd)$, or, equivalently,
$\co J(ab) ≤ \co J(cd)$.
\msk
{\sl Theorem 3.} For any $ab,cd,ef∈H$ we have:
1) $[cd]^J ≤ [ef]^J$ iff $cd ≤ J(ef)$,
2) $[ab]^J ≤ [cd]^J$ iff $\co J(ab) ≤ cd$.
\msk
We can put that in a diagram,
%
%D diagram foo
%D 2Dx 100 +30
%D 2D 100 [ef]^J |--> J(ef)
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 [cd]^J <--| cd
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 [ab]^J |--> coJ(ab)
%D 2D
%D ren coJ(ab) ==> {\co}J(ab)
%D (( [ef]^J J(ef) |-> .plabel= a \sup
%D [cd]^J cd <-|
%D [ab]^J coJ(ab) |-> .plabel= b \inf
%D ))
%D (( [ef]^J J(ef) [cd]^J cd
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( [cd]^J cd [ab]^J coJ(ab)
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
%
that can be read as a categorical statement: the functor $[·]^J: H →
H/J$ has a left adjoint $\inf:H/J→H$ and a right adjoint $\sup:H/J→H$,
where $\inf$ returns the smallest element of a J-equivalence class,
and $\sup$ returns the biggest.
% Every subset $S⊆P$ induces an inclusion $f:S→P$ and a restriction map
% $f^*:\Opens(P) → \Opens(S)$ that acts as $f^*(C) = C∩Q$. We can use
% brute force --- as in sec.\ref{HAs} --- to find operations $f_*, f_!:
% \Opens(S) → \Opens(P)$ that obey, for each $V∈\Opens(S)$,
% %
% $$???$$
% %
% _ _ _
% | | ___ _ __ ___ __ _ ___ __ _ __| |(_)___
% _ | |_____ / _ \| '_ \/ __| / _` / __| / _` |/ _` || / __|
% | |_| |_____| (_) | |_) \__ \ | (_| \__ \ | (_| | (_| || \__ \
% \___/ \___/| .__/|___/ \__,_|___/ \__,_|\__,_|/ |___/
% |_| |__/
%
% «J-ops-as-adjunctions» (to ".J-ops-as-adjunctions")
\section{J-operators as adjunctions}
\label {J-ops-as-adjunctions}
% (ph2p 60 "J-ops-as-adjunctions")
The last diagram of the last section can be translated to topological
language:
%L delabbrev("!!")
%L delabbrev("!")
%
%D diagram foo
%D 2Dx 100 +40 +30 +45
%D 2D 100 U --> J(U)
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 O(S) :::: O(P) V^* <-- V
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W --> coJ(W)
%D 2D
%D 2D +20 S0 -----> P0 S ---> P
%D 2D
%D ren J(U) V^* coJ(W) ==> \Int(U∪Q) V∩S \coInt(U∖Q)
%D ren O(S) O(P) ==> \Opens(S) \Opens(P)
%D ren S0 P0 ==> S P
%D
%D (( O(S) O(P) -> sl^^ .plabel= a f_*
%D O(S) O(P) <- .plabel= m f^*
%D O(S) O(P) -> sl__ .plabel= b f^!
%D S0 P0 -> .plabel= a f
%D ))
%D
%D (( U J(U) |-> .plabel= a f_*
%D V^* V <-| .plabel= m f^*
%D W coJ(W) |-> .plabel= m f^!
%D S P -> .plabel= a f
%D ))
%D (( U J(U) V^* V
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( V^* V W coJ(W)
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
The notation used in the diagram above is essentially the one from
figures 6 and 7 in \cite{OchsIDARCT}; the ``external view'' is at the
left,``internal view'' is at the right, the adjunction is $f^! ⊣ f^* ⊣
f_*$, and the diagram shows that $f_*(U) = \Int(U∪Q)$, $f^*(V)=V∩S$
and $f^!(W)=\coInt(U∖Q)$ (where $\Int$ and $\coInt$ use the topology
$\Opens(P)$).
The order in which things are constructed in the diagram above is
different from last section, though. Now we start with a finite set
$P$, a topology $\Opens(P)$, and a subset $S⊆P$, and we define
$\Opens(S)$ by restriction:
%
$$\Opens(S) \;\;=\;\; \setofst{V∩S}{V∈\Opens(P)}$$
%
we define $Q$ as $P∖S$, we let $f:S→P$ be the inclusion and $f^*(V)$
be $V∩S$; then {\sl it turns out} (theorem!) that the $f^!$ and $f_*$
as defined above are the left and the right adjoints of $f^*$ --- and
$J$ and $\co J$ are built from $f^!$, $f^*$ and $f_*$: the definitions
%
$$\begin{array}{rcl}
J(V) &=& f_*(f^*(V)) \\
\co J(V) &=& f^!(f^*(V)) \\
\end{array}
$$
%
yield a J-operator $J:\Opens(P)→\Opens(P)$ and its `$\co$' version,
that returns the smallest element in each equivalence class; and if
$\Opens(P) = \Opens_A(P)$ for some 2CG $(P,A)$, then we can define $J$
and $\co J$ in this other way,
%
$$\begin{array}{rcl}
J(cd) &=& \pile^{-1}(f_*(f^*(\pile(cd)))) \\
\co J(cd) &=& \pile^{-1}(f^!(f^*(\pile(cd)))) \\
\end{array}
$$
%
that yields a J-operator (and its `$\co$' version) on the ZHA $H$
generated by the 2CG $(P,A)$.
\msk
This ``topological version'' of the adjunction is a nice concrete
starting point for understanding toposes and geometric morphisms
between them --- or, actually, for introducing geometric morphisms to
``children'' who prefer to start with finite examples in which
everything can be calculated explicitly. The toposes involved are
$\Set^{\Opens(S)^\op}$ and $\Set^{\Opens(P)^\op}$, and the adjunction
$f^! ⊣ f^* ⊣ f_*$ presented above acts only on the subobjects of the
terminal of each topos --- it needs to be extended to an (essential)
geometric morphism between these toposes. This, and several concepts
from section A4 of \cite{Elephant1}, will be treated in a sequel of
this paper, in a joint work with Peter Arndt.
% _____
% | ___|__ ___
% | |_ / _ \ / _ \
% | _| (_) | (_) |
% |_| \___/ \___/
%
% ____ _ _ _ _ _
% | __ )(_) |__ | (_) ___ __ _ _ __ __ _ _ __ | |__ _ _
% | _ \| | '_ \| | |/ _ \ / _` | '__/ _` | '_ \| '_ \| | | |
% | |_) | | |_) | | | (_) | (_| | | | (_| | |_) | | | | |_| |
% |____/|_|_.__/|_|_|\___/ \__, |_| \__,_| .__/|_| |_|\__, |
% |___/ |_| |___/
%
% «bibliography» (to ".bibliography")
% (pha "bibliography")
% (ph2p 63 "bibliography")
%
% (find-LATEX "catsem.bib" "bib-Ochs")
% (find-LATEX "catsem.bib" "bib-Fourman")
% (find-LATEX "catsem.bib" "bib-Ochs" "OchsIDARCT")
% (find-LATEX "catsem.bib" "bib-DaveyPriestley")
% (find-LATEX "catsem.bib" "bib-Johnstone")
% (find-idarct0file "2010diags-body.tex" "defun b")
\cite{Elephant1}
\cite{DaveyPriestley}
\cite{OchsIDARCT}
\cite{Fourman}
\cite{BellLST}
\bibliography{catsem}
%\bibliographystyle{plain}
\bibliographystyle{alpha}
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "ph2"
% End: