Warning: this is an htmlized version! The original is across this link, and the conversion rules are here.
% (find-angg "LATEX/2017planar-has-2.tex")
% (find-angg "LATEX/2017planar-has-defs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has-2.tex"))
% (defun d () (interactive) (find-xpdfpage "~/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"))
% (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")
%   Â«.J-cubes-as-partial-ordersÂ»	(to "J-cubes-as-partial-orders")
% Â«.valuations-induce-POsÂ»		(to "valuations-induce-POs")
% Â«.comparing-partial-ordersÂ»		(to "comparing-partial-orders")
%   Â«.lindenbaum-fragmentsÂ»		(to "lindenbaum-fragments")
% Â«.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")
%
% Â«.question-marksÂ»			(to "question-marks")
% Â«.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")
%
% Â«.bibliographyÂ»			(to "bibliography")

\documentclass[oneside]{article}
%\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 edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\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_medium = {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_medium, def, spec or tcg_spec) 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\ECube{\mathsf{ECube}}
\def\OCube{\mathsf{OCube}}
\def\FCube{\mathsf{FCube}}
\def\VCube{\mathsf{VCube}}
\def\Exprs{\mathsf{Exprs}}

%  _____ _ _   _
% |_   _(_) |_| | ___
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%
% (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}

\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{comparing-partial-orders} 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 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.

%  ____  _
% |  _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% |  __/| | (_| (__\__ \
% |_|   |_|\___\___|___/
%
% Â«piccs-and-slashingsÂ» (to ".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: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()
$$\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 }
%
$$\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")
$$\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")
%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")
% 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!   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{$\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")
$$\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
$$\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 proved in the next section.

%   ___  _          _                              _
%  / _ \| |____   _(_) ___  _   _ ___    ___ _   _| |__   ___  ___
% | | | | '_ \ \ / / |/ _ \| | | / __|  / __| | | | '_ \ / _ \/ __|
% | |_| | |_) \ 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 cubes in this position:
%
$$\mat{ & 7 & \\ 5 & 3 & 6 \\ 1 & 4 & 2 \\ & 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
%
\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.

%  _____      _ _              _
% |  ___|   _| | |   ___ _   _| |__   ___  ___
% | |_ | | | | | |  / __| | | | '_ \ / _ \/ __|
% |  _|| |_| | | | | (__| |_| | |_) |  __/\__ \
% |_|   \__,_|_|_|  \___|\__,_|_.__/ \___||___/
%
% Â«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 $â$'.

The double-bar rule in sec.\ref{no-Y-cuts-no-L-cuts} is...

\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 13 "full-cubes")
\section{How J-operators interact with connectives: 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})$, 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 will use this convention to number the expressions of $\ECube_â$
% from 0 to 7, and to abbreviate them as $(â)_0, \ldots, (â)_7$:
% %
% $$\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 similary for $\ECube_â$ and $\ECube_â$ and $(â)_0, \ldots, (â)_7, % (â)_0, \ldots, (â)_7$.
%

% The rules $\acz$, $\ocz$ and $\icz$ that we proved in the beginning of
% given by the three obvious'' cubes above; adding them yields the
% cubes below, that will be called the full and-cube'', the full
% or-cube'', and the full implication-cube''.
%
% \bsk
% %
% \myresizebox{$% \pu % \defâ{{\&}} % \defâ{{\lor}} % \defâ{{\to}} % % % % \text{(omitted to make compilation faster)} % \diag{cube-and*-full} % \quad % \diag{cube-or*-full} % \quad % \diag{cube-imp*-full} %$}

\bsk

\newpage

% %      _                  _                             ____   ___
% %     | |       ___ _   _| |__   ___  ___    __ _ ___  |  _ \ / _ \ ___
% %  _  | |_____ / __| | | | '_ \ / _ \/ __|  / _ / __| | |_) | | | / __|
% % | |_| |_____| (__| |_| | |_) |  __/\__ \ | (_| \__ \ |  __/| |_| \__ \
% %  \___/       \___|\__,_|_.__/ \___||___/  \__,_|___/ |_|    \___/|___/
% %
% % Â«J-cubes-as-partial-ordersÂ» (to ".J-cubes-as-partial-orders")
% \section{J-cubes as partial orders}
% \label  {J-cubes-as-partial-orders}
% % Good (ph2p 40 "J-cubes-as-partial-orders")
%
% {
%
% If we number the vertices of the cubes of
% sec.\ref{J-ops-and-connectives} like ths,
% %
% $$\mat{ & 7 & \\ % 5 & 3 & 6 \\ % 1 & 4 & 2 \\ % & 0 & \\ % } %$$
% %
% then we can refer to their nodes as $(â)_0, \ldots, (â)_7$, $(â)_0, % \ldots, (â)_7$, $(â)_0, \ldots,$ $(â)_7$; note that
% %
% $$\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 the same for $(â)_k$ and $(â)_k$.
%
% With this convention we can interpret s set of arrows in a cube as a
% subset of $\{0,\ldots,7\}^2$, and use the positional notation for
% subsets from sec.\ref{positional} to represent that as a grid of 0's
% and 1's:
% %
% %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()
% %
% \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 %$$
%
% This gives us a way to represent explictly the transitive-reflexive
% closure of a set of arrows:
% %
% $$\left(\diag{cube-and*-0}\right)^* % \quad % = % \quad % \foos %$$
%
% The derived rule $\acz$ from sec.\ref{J-ops-and-connectives} proves
% %
% $$(P^*âQ^*)^*=P^*âQ^*=(PâQ)^*, %$$
% %
% that corresponds to arrows $7 \two/-><-/<150> 3 \two/-><-/<150> 4$;
% if we add these arrows to the cube above we get this,
% %
% %D diagram cube-and*-0b
% %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    A3 A6 =
% %D ))
% %D enddiagram
% %
% %D diagram cube-and*-0c
% %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 fooand =
% %R 2/1 1 1 1 1 1 1 1 \
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 0 1 0 0 0 0 0 |
% %R  |1 1 0 0 0 0 0 0 |
% %R  \1 0 0 0 0 0 0 0 /
% %R
% \pu
% $$\diag{cube-and*-0b} \quad ; %$$
%
% We have
% %
% $$\diag{cube-and*-0b} % \quad \neq \quad % \diag{cube-and*-0c} %$$
% %
% but:
% %
% $$\left(\diag{cube-and*-0b}\right)^* % \quad = \quad % \left(\diag{cube-and*-0c}\right)^* % \quad = \quad % \fooand %$$
%
% Let's give a name to this (non-strict) partial order:
% $\astarcuben$'', the numerical version'' of the full and-cube. Now
% we can see more clearly the extent of the rule $\astarcube$ defined in
% the end of sec.\ref{J-ops-and-connectives}: we have
% %:
% %:
% %:   -------------\astarcube
% %:   (â)_iâ(â)_j
% %:
% %:   ^acuberule
% %:
% $$\pu % \ded{acuberule} %$$
% %
% whenever $(i,j)â\astarcuben$.
%
% We have something similar for the or-cube and the implication-cube:
% %
% %D diagram cube-or*-0c
% %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 fooor =
% %R 2/1 1 1 1 1 1 1 1 \
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |1 1 1 1 0 0 0 0 |
% %R  |1 0 1 0 0 0 0 0 |
% %R  |1 1 0 0 0 0 0 0 |
% %R  \1 0 0 0 0 0 0 0 /
% %R
% \pu
% $$\ostarcuben % \quad = \quad % \left(\diag{cube-or*-0c}\right)^* % \quad = \quad % \fooor %$$
%
%
%
% %D diagram cube-imp*-0c
% %D 2Dx     100 +20 +20
% %D 2D  100     A7
% %D 2D  +15 A5  A3  A6
% %D 2D  +15 A1  A4  A2
% %D 2D  +15     A0
% %D 2D
% %D ren     A7      ==>            (P^*âQ^*)^*
% %D ren  A5 A3 A6   ==>  (PâQ^*)^* P^*âQ^*  (P^*âQ)^*
% %D ren  A1 A4 A2   ==>   PâQ^*     (PâQ)^*  P^*âQ
% %D ren     A0      ==>              PâQ
% %D
% %D 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 (( 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
% %
% %R local fooimp =
% %R 2/1 1 1 1 1 1 1 1 \
% %R  |0 0 1 0 0 0 1 0 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |0 0 1 0 1 0 1 0 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  |0 0 1 0 0 0 0 0 |
% %R  |1 1 1 1 1 1 1 1 |
% %R  \1 0 1 0 0 0 0 0 /
% %R
% \pu
% $$\istarcuben % \quad = \quad % \left(\diag{cube-imp*-0c}\right)^* % \quad = \quad % \fooimp %$$
%
% Note that the arrows $2â0$ and $6â4$ in the version for the
% implication-cube above are not mistakes --- they correspond to
% $P^*{â}Q â P{â}Q$ and $(P^*{â}Q)^* â (P{â}Q)^*$.
%
% }

% __     __    _             _   _                       __    ____   ___
% \ \   / /_ _| |_   _  __ _| |_(_) ___  _ __  ___       \ \  |  _ \ / _ \ ___
%  \ \ / / _ | | | | |/ _ | __| |/ _ \| '_ \/ __|  _____\ \ | |_) | | | / __|
%   \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \ |_____/ / |  __/| |_| \__ \
%    \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/      /_/  |_|    \___/|___/
%
% Â«valuations-induce-POsÂ» (to ".valuations-induce-POs")
\section{Valuations induce partial orders}
\label  {valuations-induce-partial-orders}
% Good (ph2p 42 "valuations-induce-POs")

Let $H$ be a ZHA, $J$ be a J-operator on $H$, and $v$ be a
valuation'' that assigns to the variables $P$ and $Q$ values in $H$;
$v$ is a function from $\{P,Q\}$ to $H$, where $P$ and $Q$ are seen as
names. Once we have $(H,J,v)$ we have a natural way to extend $v$ to
make it assign values in $H$ for $P^*$, $Q^*$, and for the expressions
in the nodes of the and-cube, the or-cube and the implication-cube.

We will represent a triple $(H,J,v)$ graphically by something like
this,
%
%L mp = mpnew({def="andCube", 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
$$\andCube$$
%
that shows the ZHA $H$, the slashing on $H$ corresponding to $J$, and
{\sl at least} $v(P)$ and $v(Q)$; sometimes the diagram will show also
$v(P^*)$ and $v(Q^*)$, for convenience. With this information is it
easy to calculate $v(\text{expr})$ for all expr's of the form $(P^? \odot Q^?)^?$, i.e., all the expressions in the nodes of the and-cube,
the or-cube and the implication-cube.

Let's restrict our attention to $â$' at this moment. We have:
%
\def\V#1{v(#1)}
\def\VV#1{v((â)_#1)}
$$\andCube \qquad \begin{array}{rclcrclcl} &&&& \V{PâQ} &=& 11 &=& \VV0 \\ &&&& \V{P^*âQ} &=& 21 &=& \VV1 \\ \V{P} &=& 10 && \V{PâQ^*} &=& 12 &=& \VV2 \\ \V{Q} &=& 01 && \V{P^*âQ^*} &=& 22 &=& \VV3 \\ \V{P^*} &=& 20 && \V{(PâQ)^*} &=& 22 &=& \VV4 \\ \V{Q^*} &=& 02 && \V{(P^*âQ)^*} &=& 22 &=& \VV5 \\ &&&& \V{(PâQ^*)^*} &=& 22 &=& \VV6 \\ &&&& \V{(P^*âQ^*)^*} &=& 22 &=& \VV7 \\ \end{array}$$

This induces a partial order $\ostarcubev(v) â \{0,\ldots,7\}^2$ in
the following way: $i â_v j$ iff $\VV{i} â_H \VV{j}$. One easy way to
calculate this $â_v$' is to replace each number from 0 to 7 in the
cube by $\VV{i}$, and then draw arrows on that to represent the
partial order in $H$, and then bring these arrows back'':
%
%D diagram cube-or*-0v
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     A0
%D 2D
%D ren     A7      ==>            (P^*âQ^*)^*
%D ren  A5 A3 A6   ==>  (PâQ^*)^* P^*âQ^*  (P^*âQ)^*
%D ren  A1 A4 A2   ==>   PâQ^*     (PâQ)^*  P^*âQ
%D ren     A0      ==>              PâQ
%D
%D 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      ==>     22
%D ren  A5 A3 A6   ==>  22 22 22
%D ren  A1 A4 A2   ==>  21 22 12
%D ren     A0      ==>     11
%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*-0vn
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     A0
%D 2D
%D ren     A7      ==>            (P^*âQ^*)^*
%D ren  A5 A3 A6   ==>  (PâQ^*)^* P^*âQ^*  (P^*âQ)^*
%D ren  A1 A4 A2   ==>   PâQ^*     (PâQ)^*  P^*âQ
%D ren     A0      ==>              PâQ
%D
%D 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 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 (( 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
%
%R local fooor =
%R 2/1 1 1 1 1 1 1 1 \
%R  |1 1 1 1 1 1 1 1 |
%R  |1 1 1 1 1 1 1 1 |
%R  |1 1 1 1 1 1 1 1 |
%R  |1 1 1 1 0 0 0 0 |
%R  |1 0 1 0 0 0 0 0 |
%R  |1 1 0 0 0 0 0 0 |
%R  \1 0 0 0 0 0 0 0 /
%R
\pu
$$\mat{ & 7 & \\ 5 & 3 & 6 \\ 1 & 4 & 2 \\ & 0 & \\ } \quad\squigto\quad \mat{ & 22 & \\ 22 & 22 & 22 \\ 21 & 22 & 12 \\ & 11 & \\ } \;\;\squigto\; \left(\diag{cube-or*-0v}\right)^* \squigto\; \left(\diag{cube-or*-0vn}\right)^*$$

We can do this more compactly, as:
%
%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*-a
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     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 (( 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*-b
%D 2Dx     100 +30 +30
%D 2D  100     A7
%D 2D  +20 A5  A3  A6
%D 2D  +20 A1  A4  A2
%D 2D  +20     A0
%D 2D
%D ren     A7      ==>              (P^*{â}Q^*)^*
%D ren  A5 A3 A6   ==>  (P{â}Q^*)^* P^*{â}Q^*  (P^*{â}Q)^*
%D ren  A1 A4 A2   ==>   P{â}Q^*     (P{â}Q)^*  P^*{â}Q
%D ren     A0      ==>                P{â}Q
%D
%D (( A0 A1 ->  A2 A3 ->  A4 A5 =   A6 A7 =
%D    A0 A2 ->  A1 A3 ->  A4 A6 =   A5 A7 =
%D    A0 A4 ->  A1 A5 ->  A2 A6 ->  A3 A7 =
%D ))
%D enddiagram
%
$$\pu \begin{array}{rcl} \ostarcubev\left(\orCube\right) &=& \left(\diag{cube-or*-a}\right)^* \\ \\ &=& \left(\diag{cube-or*-b}\right)^* \\ \end{array}$$
%
which shows that {\sl in this valuation} we have, for example, $\VV3 = \VV7$, i.e., $P^*{â}Q^* = (P^*{â}Q^*)^*$. The important information
that a valuation gives, though, is in its $\notâ$'s. For example,
here we have
%
$$\begin{array}{rclcrcl} \VV1 &<& \VV5 && P{â}Q^* &<& (P{â}Q^*)^* \\ \VV5 &>& \VV1 && (P{â}Q^*)^* &>& P{â}Q^* \\ \VV5 &\notâ& \VV1 && (P{â}Q^*)^* &\notâ& P{â}Q^* \\ \end{array}$$
%
If it were possible to prove --- as in sec.\ref{J-ops-and-connectives}
--- that $(P{â}Q^*)^* â P{â}Q^*$, then that would be true in all
valuations; by showing a valuation where $(P{â}Q^*)^* \notâ P{â}Q^*$
we show that $(P{â}Q^*)^* â P{â}Q^*$ cannot be a theorem, and that all
attempts to find a tree-like proof for $(P{â}Q^*)^* â P{â}Q^*$ are
doomed to fail.

\msk

Note that
%
%L mp = mpnew({def="orCubeTen", scale="11pt"}, "12321L"):addcuts("c 321/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*-c
%D 2Dx     100 +30 +30
%D 2D  100     A7
%D 2D  +20 A5  A3  A6
%D 2D  +20 A1  A4  A2
%D 2D  +20     A0
%D 2D
%D ren     A7      ==>              (P^*{â}Q^*)^*
%D ren  A5 A3 A6   ==>  (P{â}Q^*)^* P^*{â}Q^*  (P^*{â}Q)^*
%D ren  A1 A4 A2   ==>   P{â}Q^*     (P{â}Q)^*  P^*{â}Q
%D ren     A0      ==>                P{â}Q
%D
%D (( A0 A1 ->  A2 A3 ->  A4 A5 =   A6 A7 =
%D    A0 A2 ->  A1 A3 ->  A4 A6 =   A5 A7 =
%D    A0 A4 ->  A1 A5 ->  A2 A6 ->  A3 A7 ->
%D ))
%D enddiagram
%
$$\pu \begin{array}{rcl} \ostarcubev\left(\orCubeTen\right) &=& \left(\diag{cube-or*-c}\right)^* \\ \end{array}$$
%
This new valuation tells us something that the previous one didn't:
that $P^*{â}Q^* < (P^*{â}Q^*)^*$ in some valuation, and so
$(P^*{â}Q^*)^* â P^*{â}Q^*$ cannot be a theorem.

%   ____                                 _               ____   ___
%  / ___|___  _ __ ___  _ __   __ _ _ __(_)_ __   __ _  |  _ \ / _ \ ___
% | |   / _ \| '_  _ \| '_ \ / _ | '__| | '_ \ / _ | | |_) | | | / __|
% | |__| (_) | | | | | | |_) | (_| | |  | | | | | (_| | |  __/| |_| \__ \
%  \____\___/|_| |_| |_| .__/ \__,_|_|  |_|_| |_|\__, | |_|    \___/|___/
%                      |_|                       |___/
%
% Â«comparing-partial-ordersÂ» (to ".comparing-partial-orders")
\section{Comparing partial orders}
\label  {comparing-partial-orders}
% Rewrite (ph2p 44 "comparing-partial-orders")

If we represent the partial orders of the examples of the last section
as subsets of $\{0,\ldots,7\}^2$ we get:
%
%D diagram cube-or*-obv
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     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 (( 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*-a
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     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 (( 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*-c
%D 2Dx     100 +20 +20
%D 2D  100     A7
%D 2D  +15 A5  A3  A6
%D 2D  +15 A1  A4  A2
%D 2D  +15     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 (( 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
%
%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()
%
%L mp = mpnew({def="orCubeTen", scale="11pt"}, "12321L"):addcuts("c 321/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()
%
%R local fooobvious, foofull, foonine =
%R 2/1 1 1 1 1 1 1 1 \, 2/1 1 1 1 1 1 1 1 \, 2/1 1 1 1 1 1 1 1 \
%R  |1 0 1 0 1 0 1 0 |   |1 1 1 1 1 1 1 1 |   |1 1 1 1 1 1 1 1 |
%R  |1 1 0 0 1 1 0 0 |   |1 1 1 1 1 1 1 1 |   |1 1 1 1 1 1 1 1 |
%R  |1 0 0 0 1 0 0 0 |   |1 1 1 1 1 1 1 1 |   |1 1 1 1 1 1 1 1 |
%R  |1 1 1 1 0 0 0 0 |   |1 1 1 1 0 0 0 0 |   |1 1 1 1 1 1 1 1 |
%R  |1 0 1 0 0 0 0 0 |   |1 0 1 0 0 0 0 0 |   |1 0 1 0 0 0 0 0 |
%R  |1 1 0 0 0 0 0 0 |   |1 1 0 0 0 0 0 0 |   |1 1 0 0 0 0 0 0 |
%R  \1 0 0 0 0 0 0 0 /   \1 0 0 0 0 0 0 0 /   \1 0 0 0 0 0 0 0 /
%R
%R local footen = foofull
%
\pu
$$\begin{array}{rclcl} \ostarcubev\left(\orCube \right) &=& \left(\diag{cube-or*-a}\right)^* &=& \foonine \\ \\ \ostarcubev\left(\orCubeTen\right) &=& \left(\diag{cube-or*-c}\right)^* &=& \footen \\ \end{array}$$

\def\ptab#1{\left(\begin{tabular}{c}#1\end{tabular}\right)}

If we represent the transitive-reflexive closures of the obvious
or-cube and the full or-cube of sec.\ref{J-cubes-as-partial-orders} as
subsets of $\{0,\ldots,7\}^2$, we get:
%
$$\begin{array}{rclcl} \ptab{obvious \\ or-cube \\}^* &=& \left(\diag{cube-or*-obv}\right)^* &=& \fooobvious \\ \\ \ptab{full \\ or-cube \\}^* &=& \left(\diag{cube-or*-c} \right)^* &=& \foofull \\ \end{array}$$

If we compare these four partial orders we get:
%
%$$\ptab{obvious \\ or-cube \\}^* % \subsetneq\; % \ptab{full \\ or-cube \\}^* % =\; % \ostarcubev\left(\orCubeTen\right)^* % \subsetneq\; % \ostarcubev\left(\orCube \right)^* %$$
%
$$\begin{array}{llllllll} \ptab{obvious \\ or-cube \\}^* & \!\! \subsetneq \!\! & \ptab{full \\ or-cube \\}^* \\ & \!\! = \!\! & \ostarcubev\left(\orCubeTen\right) % ^* & \!\!\! \subsetneq \!\!\!\! & \ostarcubev\left(\orCube \right) % ^* \end{array}$$

Note that each 1' in the grid of the obvious or-cube tells us
something that we know how to prove; the same for the full or-cube,
and the full or-cube has more 1's in its grid, so it has more
information'' --- about the existence of tree-like theorems --- than
the obvious or-cube. For example, the obvious or-cube tells us that we
know how prove $(P{â}Q)^* â (P^*{â}Q^*)^*$, and the full or-cube tells
us that we know how to prove $(P{â}Q)^* = (P^*{â}Q^*)^*$.

\msk

Each '0' in the grid of a valuation-cube tells us about something that
cannot be be proved as a theorem, because that valuation is a
countermodel'' for it. The first valuation in the beginning of this
section is on a ZHA with 9 elements, and the second one is on a ZHA
with 10 elements; let's refer to them as $(H_9,J_9,v_9)$ and $(H_{10}, J_{10}, v_{10})$, or just as $v_9$ and $v_{10}$. Note that the grid
for $v_{10}$ has more 0's; and $\ostarcubev(v_{10}) \subsetneq \ostarcubev(v_9)$; for example, we have $(7,3)â\ostarcubev(v_9)$ but
%
$$\begin{array}{llllll} (7,3)\notâ\ostarcubev(v_{10}) &â& v_{10}(\VV7) \notâ_{H_{10}} v_{10}(\VV3) \\ &â& v_{10}((P^*{â}Q^*)^*) \notâ_{H_{10}} v_{10}(P^*{â}Q^*) \\ &â& v_{10} \text{ is a countermodel for } (P^*{â}Q^*)^* â P^*{â}Q^* \\ &â& v_{10} \text{ shows that } (P^*{â}Q^*)^* â P^*{â}Q^* \\ && \text{cannot be a theorem}, \end{array}$$
%
so $v_{10}$ has more information'' --- now about the {\sl
non-existence} of tree-like theorems --- than $v_9$.

\msk

The full or-cube is better'' than the obvious or-cube, and the
$v_{10}$-cube is better'' than the $v_9$-cube. Moreover, the full
or-cube and the $v_{10}$-cube coincide, and this means that the status
of every statement of the form $\VV i â \VV j$ can be determined in
the following way: if $\VV i â \VV j$ is true in this partial order
%
$$\diag{cube-or*-c}$$
%
then $\VV i â \VV j$ is a consequence of the obvious or-cube plus
$\ocz$ (sec.\ref{J-ops-and-connectives}); if $\VV i â \VV j$ is not
true in the partial order, then it cannot be proved as a theorem, and
the valuation $v_{10}$ is a countermodel for it.

We can do even better, and extract all information from well-chosen
valuations.

\msk

{\sl Theorem.} Take any statement of the form $\VV i â \VV j$. If it
is true in the valuation below,
%
$$v_{(â)} \quad = \quad v_{10} \quad = \quad \orCubeTen$$
%
then it is a theorem and can be proved using the obvious or-cube and
$\ocz$; if the statement is false in the valuation $v_{(â)}$, then it
cannot be a theorem and $v_{(â)}$ is a countermodel that shows that.

\msk

%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

We also have:

{\sl Theorem.} Take any statement of the form $(P^?{â}Q^?)^? â (P^?{â}Q^?)^?$. If it is true in the valuation below,
%
$$v_{(â)} \quad = \quad \andCube$$
%
then it is a theorem and can be proved using the obvious and-cube and
$\acz$; if the statement is false in the valuation $v_{(â)}$, then it
cannot be a theorem and $v_{(â)}$ is a countermodel that shows that.

{\sl Theorem.} Take any statement of the form $(P^?{â}Q^?)^? â (P^?{â}Q^?)^?$. If it is true in the valuation below,
%
$$v_{(â)} \quad = \quad \impCube$$
%
then it is a theorem and can be proved using the obvious
implication-cube and $\icz$; if the statement is false in the
valuation $v_{(â)}$, then it cannot be a theorem and $v_{(â)}$ is a
countermodel that shows that.

% %  _     _           _            _
% % | |   (_)_ __   __| | ___ _ __ | |__   __ _ _   _ _ __ ___
% % | |   | | '_ \ / _ |/ _ \ '_ \| '_ \ / _ | | | | '_  _ \
% % | |___| | | | | (_| |  __/ | | | |_) | (_| | |_| | | | | | |
% % |_____|_|_| |_|\__,_|\___|_| |_|_.__/ \__,_|\__,_|_| |_| |_|
% %
% % Â«lindenbaum-fragmentsÂ» (to ".lindenbaum-fragments")
% \section{Fragments of Lindenbaum Algebras}
% \label  {lindenbaum-fragments}
% % Bad (ph2p 47 "lindenbaum-fragments")

%  ____       _             _
% |  _ \ ___ | |_   _      | |       ___  _ __  ___
% | |_) / _ \| | | | |  _  | |_____ / _ \| '_ \/ __|
% |  __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_|   \___/|_|\__, |  \___/       \___/| .__/|___/
%               |___/                    |_|
%
% Â«polynomial-J-opsÂ» (to ".polynomial-J-ops")
\section{Polynomial J-operators}
\label  {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

\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}

% (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}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\} \def\li#1 #2 #3 #4 {\text{#1}&#2&#3&#4& } \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
$$\pu % \bhbox{ \begin{array}{c} \\ \foo \\ \\ \end{array} % }$$

% $$% \def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\} % \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

%   ___                  _   _                                    _
%  / _ \ _   _  ___  ___| |_(_) ___  _ __    _ __ ___   __ _ _ __| | _____
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \  | '_  _ \ / _ | '__| |/ / __|
% | |_| | |_| |  __/\__ \ |_| | (_) | | | | | | | | | | (_| | |  |   <\__ \
%  \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|\__,_|_|  |_|\_\___/
%
% Â«question-marksÂ» (to ".question-marks")
% (ph2p 53 "question-marks")
\section{Open sets of a certain form}
\label  {question-marks}

\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}}

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 53 "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 55 "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: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 56 "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()
%
$$\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 = mpnew({def="ZHAJ",  meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%
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 58 "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)$,
% %
% $$???$$
% %

%      _                                               _  _
%     | |       ___  _ __  ___    __ _ ___    __ _  __| |(_)___
%  _  | |_____ / _ \| '_ \/ __|  / _ / __|  / _ |/ _ || / __|
% | |_| |_____| (_) | |_) \__ \ | (_| \__ \ | (_| | (_| || \__ \
%  \___/       \___/| .__/|___/  \__,_|___/  \__,_|\__,_|/ |___/
%                   |_|                                |__/
%

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