Warning: this is an htmlized version! The original is across this link, and the conversion rules are here.
% (find-angg "LATEX/2016planar-has.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016planar-has.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016planar-has.pdf"))
% (defun e () (interactive) (find-LATEX "2016planar-has.tex"))
% (find-xpdfpage "~/LATEX/2016planar-has.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016planar-has.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016planar-has.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016planar-has.pdf
%               file:///tmp/2016planar-has.pdf
%           file:///tmp/pen/2016planar-has.pdf
% http://angg.twu.net/LATEX/2016planar-has.pdf

% Â«.picturedotsÂ»			(to "picturedots")
% Â«.titleÂ»				(to "title")
% Â«.introductionÂ»			(to "introduction")
%
% Â«.positionalÂ»				(to "positional")
% Â«.ZDAGsÂ»				(to "ZDAGs")
% Â«.LR-coordsÂ»				(to "LR-coords")
% Â«.ZHAsÂ»				(to "ZHAs")
% Â«.prop-calcÂ»				(to "prop-calc")
% Â«.prop-calc-ZHAÂ»			(to "prop-calc-ZHA")
% Â«.HAsÂ»				(to "HAs")
% Â«.logic-in-HAsÂ»			(to "logic-in-HAs")
% Â«.derived-rulesÂ»			(to "derived-rules")
% Â«.topologiesÂ»				(to "topologies")
% Â«.topologies-on-ZSetsÂ»		(to "topologies-on-ZSets")
% Â«.topologies-as-partial-ordersÂ»	(to "topologies-as-partial-orders")
% Â«.where-do-ZHAs-come-fromÂ»		(to "where-do-ZHAs-come-from")
% Â«.2CGsÂ»				(to "2CGs")
% Â«.topologies-on-2CGsÂ»			(to "topologies-on-2CGs")
% Â«.converting-ZHAs-2CAGsÂ»		(to "converting-ZHAs-2CAGs")
%
% Â«.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")
% Â«.slash-regions-and-opsÂ»		(to "slash-regions-and-ops")
% Â«.J-ops-and-regionsÂ»			(to "J-ops-and-regions")
% Â«.J-ops-and-connectivesÂ»		(to "J-ops-and-connectives")
% Â«.J-regs-and-slashingsÂ»		(to "J-regs-and-slashings")

% Â«.childrenÂ»				(to "children")
% Â«.comprehensionÂ»			(to "comprehension")

\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}
\usepackage{proof}                % (find-dn6 "preamble6.lua" "preamble0")
%
\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

% Â«picturedotsÂ» (to ".picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "comprehension-gab")
% (gaap 5)
%
\def\beginpicture(#1,#2)(#3,#4){\expr{beginpicture(v(#1,#2),v(#3,#4))}}
\def\pictaxes{\expr{pictaxes()}}
\def\pictdots#1{\expr{pictdots("#1")}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\picturedots(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
%\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}

\def\sa{\rightsquigarrow}
\def\BPM{\mathsf{BPM}}
\def\WPM{\mathsf{WPM}}
\def\ZHAG{\mathsf{ZHAG}}

\def\catTwo{\mathbf{2}}
%\def\Pts{\mathcal{P}}
\def\calS{\mathcal{S}}

\def\und#1#2{\underbrace{#1}_{#2}}

\def\subst#1{\left[\begin{array}{rcl}#1\end{array}\right]}
\def\subst{\bsm}

% (find-LATEXfile "2015planar-has.tex" "\\def\\Mop")

\def\MP{\mathsf{MP}}

\def\J   {\mathsf{J}}
\def\Mo  {\mathsf{Mo}}
\def\Mop {\mathsf{Mop}}
\def\Sand{\mathsf{Sand}}
\def\ECa {\mathsf{EC}{\&}}
\def\ECv {\mathsf{EC}{â}}
\def\ECS {\mathsf{ECS}}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\Int{{\operatorname{int}}}
%
\def\NoLcuts{\mathsf{No}»\mathsf{cuts}}
\def\NoYcuts{\mathsf{NoYcuts}}
\def\astarcube{{\&}^*\mathsf{Cube}}
\def\ostarcube{{â}^*\mathsf{Cube}}
\def\istarcube{{â}^*\mathsf{Cube}}
%
%\catcodeâ=13 \defâ{\mathop{\&}}

%  _____ _ _   _
% |_   _(_) |_| | ___
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% Â«titleÂ» (to ".title")

\title{Planar Heyting Algebras for Children}

\author{Eduardo Ochs}

% \begin{abstract}
% Not yet
% \end{abstract}

\maketitle

%  ___       _            _            _   _
% |_ _|_ __ | |_ ___   __| |_   _  ___| |_(_) ___  _ __
%  | || '_ \| __/ _ \ / _ | | | |/ __| __| |/ _ \| '_ \
%  | || | | | || (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__\___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% Â«introductionÂ» (to ".introduction")

This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} (see section \ref{prop-calc-ZHA}).

The for children'' in the title has a precise, but somewhat unusual,
meaning, that is explained in sec.\ref{children}.

%  ____           _ _   _                   _
% |  _ \ ___  ___(_) |_(_) ___  _ __   __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _ | |
% |  __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_|   \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% Â«positionalÂ» (to ".positional")
\section{Positional notations}
\label  {positional}
% (phap 1)

% (laq 2)
% (laq 3)
% (gaap 5)
% (to "picturedots")

\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}

Definition: a {\sl ZSet} is a finite, non-empty subset of $\N^2$ that
touches both axes, i.e., that has a point of the form $(0,\_\_)$ and a
point of the form $(\_\_,0)$. We will often represent ZSets using a
bullet notation, with or without the axes and ticks. For example:
%
$$K = \csm{ & (1,3), & \\ (0,2), & & (2,2), \\ & (1,1), & \\ & (1,0) & \\ } = \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; = \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;$$

We will use the ZSet above a lot in examples, so let's give it a short
name: $K$ (kite'').

The condition of touching both axes is what lets us represent ZSets
unambiguously using just the bullets:
%
$$\;\picturedotsa(0,0)(4,4){ 3,4 2,3 4,3 3,2 3,1 }\; \sa \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; \sa \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; \quad =\!( \qquad \qquad \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; \sa \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; \sa \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\; \quad =)$$

We can use a positional notation to represent functions {\sl from} a
ZSet. For example, if
%
$$\begin{array}{ccrcl} f &:& K &â& \N \\ & & (x,y) &â& x \\ \end{array}$$
%
then
%
$$f = \csm{ & ((1,3),1), & \\ ((0,2),0), & & ((2,2),2), \\ & ((1,1),1), & \\ & ((1,0),1) & \\ } = \sm{ & 1 & \\ 0 & & 2 \\ & 1 & \\ & 1 & \\ }$$

We will sometimes use $»$-notation to represent functions compactly.
For example:
%
$$»(x,y){:}K.x = \csm{ & ((1,3),1), & \\ ((0,2),0), & & ((2,2),2), \\ & ((1,1),1), & \\ & ((1,0),1) & \\ } = \sm{ & 1 & \\ 0 & & 2 \\ & 1 & \\ & 1 & \\ }$$
%
$$»(x,y){:}K.y = \csm{ & ((1,3),3), & \\ ((0,2),2), & & ((2,2),2), \\ & ((1,1),1), & \\ & ((1,0),0) & \\ } = \sm{ & 3 & \\ 2 & & 2 \\ & 1 & \\ & 0 & \\ }$$

The reading order'' on the points of a ZSet $S$ lists'' the points
of $S$ starting from the top and going from left to right in each
line. More precisely, if $S$ has $n$ points then
$r_S:Sâ\{1,\ldots,n\}$ is a bijection, and for example:
%
$$r_K = \sm{ & 1 & \\ 2 & & 3 \\ & 4 & \\ & 5 & \\ }$$

Subsets of a ZSet are represented with a notation with $\bullet$'s
and $\cdot$', and partial functions from a ZSet are represented with
$\cdot$'s where they are not defined. For example:
%
$$\sm{ & â & \\ Â & & â \\ & â & \\ & Â & \\ } \qquad \sm{ & 1 & \\ Â & & 3 \\ & 4 & \\ & Â & \\ }$$

%L kite  = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W     = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex   = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite",  meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW",     meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex",   meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu

The {\sl characteristic function} of a subset $S'$ of a ZSet $S$ is
the function $\chi_{S'}:Sâ\{0,1\}$ that returns 1 exactly on the
points of $S'$; for example, $\dagKite10110$ is the characteristic
function of $\dagKiteâÂââÂ â \dagKiteâââââ$. We will sometimes denote
subsets by their characteristic functions because this makes them
easier to pronounce'' by reading aloud their digits in the reading
order --- for example, $\dagKite10110$ is one-zero-one-one-zero''
(see sec.\ref{where-do-ZHAs-come-from}).

%  _________    _    ____
% |__  /  _ \  / \  / ___|___
%   / /| | | |/ _ \| |  _/ __|
%  / /_| |_| / ___ \ |_| \__ \
% /____|____/_/   \_\____|___/
%
% Â«ZDAGsÂ» (to ".ZDAGs")
\section{ZDAGs}
\label  {ZDAGs}
% (phap 2)

We will sometimes use the bullet notation for a ZSet $S$ as a {\sl
shorthand} for one of the two DAGs induced by $S$: one with its
arrows going up, the other one with them going down. For example:
sometimes
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
%
%R local K =
%R 1/ o \
%R  |o o|
%R  | o |
%R  \ o /
%R -- mp:output()
%
\pu
$$%\pu \Kb \;\;\;\;\text{will stand for:}\;\; \KB = \Kn =$$
$$\pmat{ \csm{ & (1,3), & \\ (0,2), & & (2,2), \\ & (1,1), & \\ & (0,0) & \\ }, \csm{ ((1,3),(0,2)), ((1,3),(2,2)), \\ ((0,2),(1,1)), ((2,2),(1,1)), \\ ((1,1),(0,0)) \\ } }$$

\msk

Let's formalize this.

Consider a game in which black and white pawns are placed on points of
$\Z^2$, and they can move like this:
%
%R local B, W = 2/    bp    \, 2/wp  wp  wp\
%R               |  swsose  |   |  nwnone  |
%R               \bp  bp  bp/   \    wp    /
%R
%R local T = {bp="\\bullet", wp="\\circ",
%R            sw="â", so="â", se="â",
%R            nw="â", no="â", ne="â"}
$$\pu \Bmne \qquad \Wmne$$

Black pawns can move from $(x,y)$ to $(x+k,y-1)$ and white pawns from
$(x,y)$ to $(x+k,y+1)$, where $kâ\{-1,0,1\}$. The mnemonic is that
black pawns are solid'', and thus heavy'', and they sink'', so
they move down; white pawns are hollow'', and thus light'', and
they float'', so they move up.

Let's now restrict the board positions to a ZSet $S$. Black pawns can
move from $(x,y)$ to $(x+k,y-1)$ and white pawns from $(x,y)$ to
$(x+k,y+1)$, where $kâ\{-1,0,1\}$, but only when the starting and
ending positions both belong to $S$. The sets of possible black pawn
moves and white pawn moves on $S$ can be defined formally as:
%
$$\mat{ \BPM(S) = \setofst {((x,y),(x',y'))âS^2} {x-x'â\{-1,0,1\}, y'=y-1} \\ \WPM(S) = \setofst {((x,y),(x',y'))âS^2} {x-x'â\{-1,0,1\}, y'=y+1} \\ }$$
%
...and now please forget everything else you expect from a game ---
like starting position, capturing, objective, winning... the idea of a
game'' was just a tool to let us explain $\BPM(S)$ and $\WPM(S)$
quickly.

\msk

A {\sl ZDAG} is a DAG of the form $(S,\BPM(S))$ or $(S,\WPM(S))$,
where $S$ is a ZSet.

A {\sl ZPO} is partial order of the form $(S,\BPM(S)^*)$ or
$(S,\WPM(S)^*)$, where $S$ is a ZSet and the ${}^*$' denotes the
transitive-reflexive closure of the relation.

\msk

Sometimes, when this is clear from the context, a bullet diagram like
$\Kmini$ will stand for either the ZDAGs $(\Kmini,\BPM(\Kmini))$ or
$(\Kmini,\WPM(\Kmini))$, or for the ZPOs $(\Kmini,\BPM(\Kmini)^*)$ or
$(\Kmini,\WPM(\Kmini)^*)$ (sec.\ref{ZHAs}), or even for the ZPOs seen
as categories (section $\_\_\_$).

%  _     ____                            _ _             _
% | |   |  _ \    ___ ___   ___  _ __ __| (_)_ __   __ _| |_ ___  ___
% | |   | |_) |  / __/ _ \ / _ \| '__/ _ | | '_ \ / _ | __/ _ \/ __|
% | |___|  _ <  | (_| (_) | (_) | | | (_| | | | | | (_| | ||  __/\__ \
% |_____|_| \_\  \___\___/ \___/|_|  \__,_|_|_| |_|\__,_|\__\___||___/
%
% Â«LR-coordsÂ» (to ".LR-coords")
\section{LR-coordinates}
\label  {LR-coords}
% (phap 4)

\def\LR{\mathbb{LR}}

The {\sl lr-coordinates} are useful for working on quarter-plane of
$\Z^2$ that looks like $\N^2$ turned $45Â°$ to the left. Let $\ang{l,r} := (-l+r,l+r)$; then (the bottom part of)
$\setofst{\ang{l,r}}{l,râ\N}$ is:
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
%
%R local zhav =
%R 1/o o o o o\
%R  | o o o o |
%R  |  o o o  |
%R  |   o o   |
%R  \    o    /
%R mplr = zhav:tomp({def="mplr", scale="14pt", meta="s"})
%R mpxy = zhav:tomp({def="mpxy", scale="14pt", meta="s"})
%R f = function (p) local l,r = p:to_l_r(); return "\\ang{"..l..","..r.."}" end
%R for p,str in mplr:points() do mplr:put(p, f(p-v(4,0))) end
%R for p,str in mpxy:points() do mpxy:put(p, (p-v(4,0)):xy()) end
%R mplr:output()
%R mpxy:output()
%
$$\pu \mplr \quad = \quad \mpxy$$

Sometimes we will write $lr$ instead of $\ang{l,r}$. So:
%
%R local zhav =
%R 1/o o o o o\
%R  | o o o o |
%R  |  o o o  |
%R  |   o o   |
%R  \    o    /
%R mplr = zhav:tomp({def="mplr", scale="13.5pt", meta="s"})
%R mpxy = zhav:tomp({def="mpxy", scale="14pt", meta="s"})
%R f = function (p) local l,r = p:to_l_r(); return l..r end
%R for p,str in mplr:points() do mplr:put(p, f(p-v(4,0))) end
%R for p,str in mpxy:points() do mpxy:put(p, (p-v(4,0)):xy()) end
%R mplr:output()
%R mpxy:output()
%
$$\pu \mplr \quad = \quad \mpxy$$

Let $\LR = \setofst{\ang{l,r}}{l,râ\N}$.

%  ______   _    _
% |__  / | | |  / \   ___
%   / /| |_| | / _ \ / __|
%  / /_|  _  |/ ___ \\__ \
% /____|_| |_/_/   \_\___/
%
% Â«ZHAsÂ» (to ".ZHAs")
\section{ZHAs}
\label  {ZHAs}
% (phap 5)

A {\sl ZHA} is a subset of $\LR$ between a left and a right wall'',
as we will see.

\msk

A triple $(h,L,R)$ is a height-left-right-wall'' when:

1) $hâ\N$

2) $L:\{0,\ldots,h\}â\Z$ and $R:\{0,\ldots,h\}â\Z$

3) $L(h)=R(h)$ (the top points of the walls are the same)

4) $L(0)=R(0)=0$ (the bottom points of the walls are the same, $0$)

5) $âyâ\{0,\ldots,h\}.\,L(y)âR(y)$ (left'' is left of right'')

6) $âyâ\{1,\ldots,h\}.\,L(y)-L(y-1)=\pm1$ (the left wall makes no jumps)

7) $âyâ\{1,\ldots,h\}.\,R(y)-R(y-1)=\pm1$ (the right wall makes no jumps)

\msk

The {\sl ZHA generated by} a height-left-right-wall $(h,L,R)$ is the
set of all points of $\LR$ with valid height and between the left and
the right walls. Formally:

$$\ZHAG(h,L,R) = \setofst {(x,y)â\LR} {yâh, L(y)âxâR(y)}.$$

A {\sl ZHA} is a set of the form $\ZHAG(h,L,R)$, where the triple
$(h,L,R)$ is a height-left-right-wall.

Here is an example of a ZHA (with the white pawn moves on it):
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
%
%R local zhav =
%R 1/ o    \  -- L(9)=1 R(9)=1   maxy=9  L(maxy)=R(maxy)
%R  |o o   |
%R  | o    |
%R  |  o   |
%R  |   o  |
%R  |  o o |
%R  | o o o|
%R  |  o o |
%R  |   o o|  -- L(1)=3 R(1)=5
%R  \    o /  -- L(0)=4 R(0)=4   L(0)=R(0)=x_0=4
%R local L = {[0]=0,-1,-2,-3,-2,-1,-2,-3,-4,-3}
%R local R = {[0]=0, 1, 0, 1, 0,-1,-2,-3,-2,-3}
%R local x = {L=8, R=10.5, a=13.5, b=16.5}
%R local x = {L=4, R=7, a=10, b=12.5}
%R for y=0,9 do
%R   mp:put(v(x.L, y), "L"..y, "L("..y..")="..L[y])
%R   mp:put(v(x.R, y), "R"..y, "R("..y..")="..R[y])
%R end
%R mp:put(v(x.b, 9), "=", "h=9")
%R mp:put(v(x.a, 9), "=", "L(9)=R(9)")
%R mp:put(v(x.a, 0), "=", "\\;\\;\\;\\;L(0)=R(0)=0")
%R mp:output()
%
$$\pu \zhav$$

We will see later (section \ref{prop-calc-ZHA}) that ZHAs (with white
pawn moves) are Heyting Algebras.

\msk

We can use a bullet notation to denote ZHAs, but look at what happens
using the convention from sec.\ref{positional}:
%
$$\quad\picturedotsa(-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad \sa \quad\picturedots (-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad \sa \quad\picturedotsa (0,0)(4,5){ 2,0 3,1 4,2 1,1 2,2 3,3 0,2 1,3 2,4 1,5 }\quad$$
%
we get a ZSet whose bottom point is $(2,0)$, but the bottom point of
our original ZHA was $(0,0)$... let's refine that convention. From
this point on, it will be: when it is clear from the context that a
bullet diagram represents a ZHA, then the $(0,0)$ is its bottom point;
otherwise the $(0,0)$ is the point that makes the diagram fit in
$\N^2$ and touch both axes.

The new convention also applies to functions from ZHAs, and for
partial functions and subsets. For example:
%
%L local mpB = mpnew({def="fooB", scale="5pt", meta="s"}, "12321L")
%L local mpx = mpnew({def="foox", scale="5pt", meta="s"}, "12321L")
%L local mpl = mpnew({def="fool", scale="5pt", meta="s"}, "12321L")
%L local mpr = mpnew({def="foor", scale="5pt", meta="s"}, "12321L")
%L f = function (n) return "\\text{"..n.."}" end
%L mpx:zhalrf0("P -> f(P[1])"):output()
%L mpl:zhalrf0("P -> P:xytolr()[1]"):output()
%L mpr:zhalrf0("P -> P:xytolr()[2]"):output()
$$\pu \begin{array}{lll} B = \fooB \quad \text{(a ZHA)} & \phantom{m} & »(x,y){:}B.x = \foox \\ \\ »\ang{l,r}{:}B.l = \fool & & »\ang{l,r}{:}B.r = \foor \\ \end{array}$$

We will often denote ZHAs by the identity function on them:
%
%L local mpB = mpnew({def="fooB", scale="5pt", meta="s"}, "12321L")
%L local mp  = mpnew({def="foo",  scale="7pt", meta="s"}, "12321L")
$$\pu »\ang{l,r}{:}B.\ang{l,r} \;=\; »lr{:}B.lr \;=\; \foo \qquad \quad B \;=\; \foo$$
%
Note that we are using the compact notation from the end of section
\ref{LR-coords}: $lr$' instead of $\ang{l,r}$'.

%  to denote ZHAs and
% functions from ZHAs compactly, but we have to modify the convention
% for adding the axes back.
%
% %R local zhav =
% %R 1/ o   \
% %R  |  o  |
% %R  | o o |
% %R  |o o o|
% %R  | o o |
% %R  \  o  /
% %R zhav:tomp ({def="zb", scale="15pt", meta=nil}):addxys():output()
% %
% $$\pu % \za \qquad \sa \qquad \zb %$$

%  ____                              _
% |  _ \ _ __ ___  _ __     ___ __ _| | ___
% | |_) | '__/ _ \| '_ \   / __/ _ | |/ __|
% |  __/| | | (_) | |_) | | (_| (_| | | (__
% |_|   |_|  \___/| .__/   \___\__,_|_|\___|
%                 |_|
%
% Â«prop-calcÂ» (to ".prop-calc")
\section{Propositional calculus}
\label  {prop-calc}
% (phap 5)

A {\sl PC-structure} is a tuple
%
$$L = (Ω,â,â,â,â,â,â,â,Â),$$
%
where:

$Ω$ is the set of truth values'',

$â$ is a relation on $Ω$,

$â$ and $â$ are two elements of $Ω$,

$â$, $â$, $â$, $â$ are functions from $ΩÃΩ$ to $Ω$,

$Â$ is a function from $Ω$ to $Ω$.

\msk

Classical Logic is'' a PC-structure, with $Ω=\{0,1\}$, $â=1$, $â=0$,
$â=\{(0,0),(0,1),(1,0)\}$, $â=\csm{((0,0),0), ((0,1),0), \\ ((1,0),0), ((1,1),1)}$, etc.

PC-structures let us interpret expressions from Propositional
Calculus, and let us define a notion of {\sl tautology}. For example,
in Classical Logic,
%
\begin{itemize}
\item $ÂÂPâP$ is a tautology because it is valid (i.e., it yields $â$)
for all values of $P$ in $Ω$,

\item $Â(PâQ)â(ÂPâÂQ)$ s a tautology because it is valid for all
values of $P$ and $Q$ in $Ω$,

\item but $PâQâPâQ$ is {\sl not} a tautology, because when $P=0$ and
$Q=1$ the result is not $â$:
%
$$\und{\und{\und{P}0 â \und{Q}1}{1} â \und{\und{P}0 â\und{Q}1}{0}}{0}$$
\end{itemize}

%  ____                              _        ______   _    _
% |  _ \ _ __ ___  _ __     ___ __ _| | ___  |__  / | | |  / \
% | |_) | '__/ _ \| '_ \   / __/ _ | |/ __|   / /| |_| | / _ \
% |  __/| | | (_) | |_) | | (_| (_| | | (__   / /_|  _  |/ ___ \
% |_|   |_|  \___/| .__/   \___\__,_|_|\___| /____|_| |_/_/   \_\
%                 |_|
%
% Â«prop-calc-ZHAÂ» (to ".prop-calc-ZHA")
\section{Propositional calculus in a ZHA}
\label  {prop-calc-ZHA}
% (phap 6)

Let $Ω$ be the set of points of a ZHA and $â$ the default partial
order on it. The {\sl default meanings for $â,â,â,â,â,â,Â$} are these
ones:
%
$$\def\o#1{\mathop{\mathsf{#1}}} \def\o#1{\mathbin{\mathsf{#1}}} \def\a#1#2{\ang{#1,#2}} \def\ab{\a ab} \def\cd{\a cd} \begin{array}{rcl} % \ab â \cd &:=& aâcâbâd \\ \ab â \cd &:=& aâcâbâd \\[5pt] % \ab \o{above} \cd &:=& aâcâbâd \\ \ab \o{below} \cd &:=& aâcâbâd \\ \ab \o{leftof} \cd &:=& aâcâbâd \\ \ab \o{rightof} \cd &:=& aâcâbâd \\[5pt] % \o{valid}(\ab) &:=& \abâΩ \\ \o{ne}(\ab) &:=& \o{if} \o{valid}(\a a{b+1}) \o{then} \o{ne}(\a a{b+1}) \o{else} \ab \; \o{end} \\ \o{nw}(\ab) &:=& \o{if} \o{valid}(\a {a+1}b) \o{then} \o{nw}(\a {a+1}b) \o{else} \ab \; \o{end} \\[5pt] % \ab â \cd &:=& \a{\o{min}(a,c)}{\o{min}(b,d)} \\ \ab â \cd &:=& \a{\o{max}(a,c)}{\o{max}(b,d)} \\[5pt] % \ab \to \cd &:=& \begin{array}[t]{llll} \o{if} & \ab \o{below} \cd & \o{then} & â \\ \o{elseif} & \ab \o{leftof} \cd & \o{then} & \o{ne}(\abâ\cd) \\ \o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\abâ\cd) \\ \o{elseif} & \ab \o{above} \cd & \o{then} & \cd \\ \o{end} \end{array} \\[5pt] % â &:=& \o{sup}(Ω) \\ â &:=& \a00 \\ Â\ab &:=& \abââ \\ \abâ\cd &:=& (\abâ\cd)â (\cdâ\ab)\\ \end{array}$$
%
% We will sometimes call them $â_D,â_D,â_D,â_D,â_D,â_D,Â_D$ to
% distinguish them from other ones.

% --- let's say with the default logic'', for shortness ---

Let $Ω$ be the ZHA at the top left in the figure below. Then, with the
default meanings for the connectives neither $ÂÂPâP$ nor
$Â(PâQ)â(ÂPâÂQ)$ are tautologies, as there are valuations that make
them yield results different than $â=32$:
%
%R local znotnotP =
%R 1/ T   \
%R  |  .  |
%R  | . c |
%R  |b . a|
%R  | P . |
%R  \  F  /
%R local T = {F="â", T="â", a="P'", b="P''", c="â"}
%R
%R local zdemorgan =
%R 1/ T   \
%R  |  o  |
%R  | . . |
%R  |q . p|
%R  | P Q |
%R  \  a  /
%R local T = {F="â", T="â", p="P'", q="Q'", a="â", o="â"}
%R
%
%L -- ÂÂPâP
%L ubs [[
%L Â Â  P 10 u  Pre 02 u Pre 20 u ()  â P 10 u Bin 12 u
%L   notnotP def   output
%L ]]
%L
%L -- Â(PâQ)â(ÂPâÂQ)
%L ubs [[
%L   Â P 10 u â Q 01 u Bin 00 u () Pre 32 u
%L   â   Â P 10 u Pre 02 u   â   Â Q 01 u Pre 20 u   Bin 22 u ()   Bin 22 u
%L   demorgan def   output
%L ]]
%L
%
$$\pu \begin{array}{ccccl} \ohouse && \znotnotP && \mat{\notnotP} \\ \\ && \zdemorgan && \mat{\demorgan} \\ \end{array}$$

So: {\sl some} classical tautologies are not tautologies in this ZHA.

The somewhat arbitrary-looking definition of $â$' will be explained
at the end of the next section.

%  _   _    _
% | | | |  / \   ___
% | |_| | / _ \ / __|
% |  _  |/ ___ \\__ \
% |_| |_/_/   \_\___/
%
% Â«HAsÂ» (to ".HAs")
% (phap 7)

\section{Heyting Algebras}

A {\sl Heyting Algebra} is a PC-structure
%
$$H = (Ω,â_H,â_H,â_H,â_H,â_H,â_H,â_H,Â_H),$$
%
in which:

1) $(Ω,â_H)$ is a partial order

2) $â_H$ is the top element of the partial order

3) $â_H$ is the bottom element of the partial order

4) $P â_H Q$ is the same as $(P â_H Q)â_H(Q â_H P)$

5) $Â_H P$ is the same as $P â_H â_H$

6) $âP,Q,RâΩ.\;\; (P â_H (Q â_H R)) â ((P â_H Q) â (P â_H R))$

7) $âP,Q,RâΩ.\;\; ((P â_H Q) â_H R) â ((P â_H R) â (Q â_H R))$

8) $âP,Q,RâΩ.\;\; (P â_H (Q â_H R)) â ((P â_H R) â_H R)$

6') $âQ,RâΩ.\, â!YâΩ.\, âPâΩ.\;\; (P â_H Y) â ((P â_H Q) â (P â_H R))$

7') $âP,QâΩ.\, â!XâΩ.\, âRâΩ.\;\; (X â_H R) â ((P â_H R) â (Q â_H R))$

8') $âQ,RâΩ.\, â!YâΩ.\, âPâΩ.\;\; (P â_H Y) â ((P â_H R) â_H R)$

\msk

The conditions 6', 7', 8' say that there are unique elements in $Ω$
that behave as'' $Q â_H R$, $P â_H Q$ and $Q â_H R$ for given $P$,
$Q$, $R$; the conditions 6,7,8 say that $Q â_H R$, $P â_H Q$ and $Q â_H R$ are exactly the elements with this behavior.

\msk

The positional notation on ZHAs is very helpful for visualizing what
the conditions 6',7',8',6,7,8 mean. Let $Ω$ be the ZDAG on the left
below:
%
$$%R local QoRai, PoQai, PnnP = %R 1/ T \, 1/ T \, 1/ T \ %R | . . | | . . | | . | %R | . . . | | . . . | | . . | %R | . . . i | | . o . . | |d . n| %R |. Q . . .| |. P . . .| | P . | %R | . . R . | | . . Q . | \ F / %R | . a . | | . . . | %R | . . | | . . | %R \ F / \ F / %R local T = {a="(â)", o="(â)", i="(\\!â\\!)", n="(Â)", d="(\\!\\!ÂÂ\\!)", %R T="Â", F="Â", T="â", F="â", } %R PoQai:tozmp({def="PoQai", scale="10pt", meta=nil}):addcells(T):addcontour():output() %R QoRai:tozmp({def="QoRai", scale="10pt", meta=nil}):addcells(T):addcontour():output() %R PnnP :tozmp({def="PnnP" , scale="10pt", meta=nil}):addcells(T):addcontour():output() %R %R PoQai:tozmp({def="lozfive", scale="10pt", meta=nil}):addlrs():addcontour():output() \pu \lozfive \qquad \QoRai \qquad \PoQai$$
%
we will see that

a) if $Q=31$ and $R=12$ then $Q â_H R = 11$,

b) if $P=31$ and $Q=12$ then $P â_H Q = 32$,

c) if $Q=31$ and $R=12$ then  $Q â_H R = 14$.

\msk

Let's see each case separately --- but, before we start, note that in
6, 7, 8, 6', 7', 8' we work part with truth values in $Ω$ and part
with standard truth values. For example, in 6, with $P=20$, we have:
%
$$\und{(\und{\und{P}{20} â_H (\und{\und{Q}{31} â_H \und{R}{12}}{11})}{0}) â (\und{(\und{\und{P}{20} â_H \und{Q}{31}}{1}) â (\und{\und{P}{20} â_H \und{R}{12}}{0}) }{0}) }{1}$$

\bsk

a) Let $Q=31$ and $R=12$. We want to see that $Q â_H R = 11$, i.e.,
that
%
$$âPâΩ.\;\; (P â_H Y) â ((P â_H Q) â (P â_H R))$$
%
holds for $Y=11$ and for no other $YâΩ$. We can visualize the behavior
of $P â_H Q$ for all $P$'s by drawing $»P{:}Ω.(P â_H Q)$ in the
positional notation; then we do the same for $»P{:}Ω.(P â_H R)$ and
for $»P{:}Ω.((P â_H Q) â (P â_H R))$. Suppose that the full
expression, $âP{:}Ω.\,\_\_\_$', is true; then the behavior of the
left side of the $â$', $»P{:}Ω.(P â_H Y)$, has to be    a copy of the
behavior of the right side, and that lets us find the only adequate
value for $Y$.

The order in which we calculate and draw things is below, followed by
the results themselves:
%
$$(\und{P â_H \und{Y}{(7)}}{(6)}) â (\und{(\und{P â_H \und{Q}{(1)}}{(3)}) â (\und{P â_H \und{R}{(2)}}{(4)}) }{(5)} )$$
%
$$%R local z = ZHA.fromspec("123454321") %R local mpQ = mpnew({def="fooQ", scale="5pt", meta="s"}, "123454321") %R local mpR = mpnew({def="fooR", scale="5pt", meta="s"}, "123454321") %R local mpA = mpnew({def="fooA", scale="5pt", meta="s"}, "123454321") %R mpQ:zhalrf0("P -> P:below(v'31') and 1 or 0"):output() %R mpR:zhalrf0("P -> P:below(v'12') and 1 or 0"):output() %R mpA:zhalrf0("P -> P:below(v'11') and 1 or 0"):output() \pu (\und{P â_H \und{Y}{11}}{\fooA}) â (\und{(\und{P â_H \und{Q}{31}}{\fooQ}) â (\und{P â_H \und{R}{12}}{\fooR}) }{\fooA} )$$

\msk

b) Let $P=31$ and $Q=12$. We want to see that $P â_H Q = 32$, i.e.,
that
%
$$âR{:}Ω.\;\; (X â_H R) â ((P â_H R) â (Q â_H R))$$
%
holds for $X=32$ and for no other $XâΩ$. We do essentially the same as
we did in (a), but now we calculate $»R{:}Ω.(P â_H R)$, $»R{:}Ω.(Q â_H R)$, and $»R{:}Ω.((P â_H R) â (Q â_H R))$. The order in which we
calculate and draw things is below, followed by the results
themselves:
%
$$(\und{\und{X}{(7)} â_H R}{(6)}) â (\und{(\und{\und{P}{(1)} â_H R}{(3)}) â (\und{\und{Q}{(2)} â_H R}{(4)}) }{(5)} )$$
%
$$%R local z = ZHA.fromspec("123454321") %R local mpQ = mpnew({def="fooP", scale="5pt", meta="s"}, "123454321") %R local mpR = mpnew({def="fooQ", scale="5pt", meta="s"}, "123454321") %R local mpA = mpnew({def="fooA", scale="5pt", meta="s"}, "123454321") %R mpQ:zhalrf0("P -> P:above(v'31') and 1 or 0"):output() %R mpR:zhalrf0("P -> P:above(v'12') and 1 or 0"):output() %R mpA:zhalrf0("P -> P:above(v'32') and 1 or 0"):output() \pu (\und{\und{X}{32} â_H R}{\fooA}) â (\und{(\und{\und{P}{31} â_H R}{\fooP}) â (\und{\und{Q}{12} â_H R}{\fooQ}) }{\fooA} )$$

\msk

c) Let $Q=31$ and $R=12$. We want to see that $Q â_H R = 14$, i.e.,
that
%
$$âP{:}Ω.\;\; (P â_H Y) â ((P â_H Q) â_H R)$$
%
holds for $Y=14$ and for no other $YâΩ$. Here the strategy is slightly
different. We start by visualizing $»P{:}Ω.(P â_H Q)$, which is a
function from $Ω$ to $Ω$, not a function from $Ω$ to $\{0,1\}$ like
the ones we were using before. The order in which we calculate and
draw things is below, followed by the results:
%
$$(\und{P â_H \und{Y}{(6)}}{(5)}) â (\und{(\und{P â_H \und{Q}{(1)}}{(3)}) â_H \und{R}{(2)} }{(4)} )$$
%
$$%R local z = ZHA.fromspec("123454321") %R local mpQ = mpnew({def="fooQ", scale="6pt", meta="s"}, "123454321") %R local mpR = mpnew({def="fooR", scale="5pt", meta="s"}, "123454321") %R local mpA = mpnew({def="fooA", scale="5pt", meta="s"}, "123454321") %R mpQ:zhalrf ("P -> P:And (v'31') "):output() %R mpR:zhalrf0("P -> P:below(v'14') and 1 or 0"):output() %R mpA:zhalrf0("P -> P:below(v'11') and 1 or 0"):output() \pu (\und{P â_H \und{Y}{14}}{\fooR}) â (\und{(\und{P â_H \und{Q}{31}}{\fooQ}) â_H \und{R}{12} }{\fooR} )$$

%  _                _        _         _   _    _
% | |    ___   __ _(_) ___  (_)_ __   | | | |  / \   ___
% | |   / _ \ / _ | |/ __| | | '_ \  | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__  | | | | | |  _  |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/   \_\___/
%             |___/
%
% Â«logic-in-HAsÂ» (to ".logic-in-HAs")
% (phap 10)

\section{Logic in a Heyting Algebra}
\label  {logic-in-HAs}

In the previous sextion we saw a set of conditions --- called 1 to 8'
--- that characterize the Heyting-Algebra-ness'' of a PC-structure.
It is easy to see that Heyting-Algebra-ness, or HA-ness'', is
equivalent to this set of conditions:
%
$$\begin{array}{|r|lrcccc|l|l|}\hline 1 & âP. & (PâP) & & & & & \id \\ & âP,Q,R. & (PâR) & â & (PâQ) &â& (QâR) & \comp \\ \hline 2 & âP. & (Pââ) & & & & & â_1 \\ 3 & âQ. & (ââQ) & & & & & â_1 \\ \hline \hline 6 & âP,Q,R. & (PâQâR) &â& (PâQ) & & & â_1 \\ & âP,Q,R. & (PâQâR) &â& & & (PâR) & â_2 \\ & âP,Q,R. & (PâQâR) &â& (PâQ) & â & (PâR) & â_3 \\ \hline 7 & âP,Q,R. & (PâQâR) &â& (PâR) & & & â_1 \\ & âP,Q,R. & (PâQâR) &â& & & (QâR) & â_2 \\ & âP,Q,R. & (PâQâR) &â& (PâR) & â & (QâR) & â_3 \\ \hline 8 & âP,Q,R. & (PâQ{â}R) &â& \multicolumn{3}{c|}{(PâQâR)} & â_1 \\ & âP,Q,R. & (PâQ{â}R) &â& \multicolumn{3}{c|}{(PâQâR)} & â_2 \\ \hline \end{array}$$
%
We omitted the conditions 4 and 5, that defined $â$' and $Â$' in
terms of the other operators. The last column gives a name to each of
these new conditions.

These new conditions let us put (some) proofs about HAs in tree form,
as we shall see soon.

\def\t{\text}

\msk

Let us introduce two new notations. The first one,
$$(\t{expr})\subst{v_1 := \t{repl}_1 \\ v_2 := \t{repl}_2}$$ indicates
simultaneous substitution of all (free) occurrences of the variables
$v_1$ and $v_2$ in expr by $\t{repl}_1$ and $\t{repl}_2$. For example,
%
$$((x+y)Âz) \subst{ x:=a+y \\ y:=b+z \\ z:=c+x \\ } \;\;=\;\; ((a+y)+(b+z))Â(c+x).$$

The second is a way to write $â$'s as horizontal bars. In
%:
%:                                           L   M
%:                                    -\ee   -----\zeta
%:  A  B  C     E  F     H            K        N         O
%:  -------\aa  ----\bb  -\gg  -\dd   --------------------\eta
%:     D         G       I     J               P
%:
%:     ^t1       ^t2     ^t3   ^t4             ^t5
%:
$$\pu \ded{t1} \qquad \ded{t2} \qquad \ded{t3} \qquad \ded{t4} \qquad \ded{t5}$$
%
the trees mean:
%
\begin{itemize}
\item if $A$, $B$, $C$ are true then $D$ is true (by $\aa$),

\item if $E$, $F$, are true then $G$ is true (by $\bb$),

\item if $H$ is true then $I$ is true (by $\gg$),

\item $J$ is true (by $\dd$, with no hypotheses),

\item $K$ is true (by $\ee$); if $L$ and $M$ then $N$ (by $\zeta$);
if $K$, $N$, $O$, then $P$ (by $\eta$); combining all this we get a
way to prove that if $L$, $M$, $O$, then $P$,
\end{itemize}
%
where $\aa, \bb, \gg, \dd, \ee, \zeta, \eta$ are usually names
of rules.

\msk

The implications in the table in the beginning of this section can be
rewritten as tree rules'' as:
%:
%:             PâQ  QâR
%:   ----\id   ---------\comp    -----â_1    -----â_1
%:   PâP         PâR            Pââ        ââQ
%:
%:    ^id         ^comp           ^T1       ^B1
%:
%:   PâQâR      PâQâR      PâQ  PâR
%:   ------â_1  ------â_2  -----------â_3
%:    PâQ        PâR         PâQâR
%:
%:    ^and1      ^and2        ^and3
%:
%:   PâQâR      PâQâR      PâR  QâR
%:   ------â_1  ------â_2  -----------â_3
%:    PâR        QâR         PâQâR
%:
%:    ^or1       ^or2         ^or3
%:
%:
%:    PâQ{â}R         PâQâR
%:    ---------â_1   ---------â_2
%:    PâQâR          PâQ{â}R
%:
%:     ^imp1           ^imp2
%:
{
\pu
$$\ded{id} \qquad \ded{comp} \qquad \ded{T1} \qquad \ded{B1}$$

$$\ded{and1} \qquad \ded{and2} \qquad \ded{and3}$$

$$\ded{or1} \qquad \ded{or2} \qquad \ded{or3}$$

$$\ded{imp1} \qquad \ded{imp2}$$

}

\msk

Note that the $âP,Q,RâΩ$'s are left implicit in the tree rules, which
means that {\sl every substitution instance of the tree rules hold};
sometimes --- but rarely --- we will indicate the substitution
explicitly, like this,
%:
%:    PâQ{â}R         PâQâR
%:    ---------â_1   ---------â_2
%:    PâQâR          PâQ{â}R
%:
%:     ^imp1           ^imp2
%:
%:    Pâ(P{â}â)ââ
%:   ------------------â_2\su
%:   Pâ((P{â}â){â}â)
%:
%:     ^foo
%:
$$\pu \def\su{\bsm{Q:=P{â}â \\ R:=â}} % \begin{array}{rcl} \left(\cded{imp2}\right) \su &\squigto& {\def\su{} \cded{foo}} \\\\ (â_2)\su &\squigto& \cded{foo} \\ \end{array}$$
%
Usually we will only say $â_2$' instead of $â_2\bsm{Q:=P{â}â \\ R:=â}$' at the right of a bar, and the task of discovering which
substitution has been used is left to the reader.

\msk

The tree rules can be composed in a nice visual way. For example,
this,
%:
%:  ---------\id               ---------\id
%:  PâQâPâQ                    PâQâPâQ
%:  ---------â_1               ---------â_2
%:   PâQâP       PâR            PâQâQ       QâS
%:   ------------------\comp    ------------------\comp
%:      PâQâR                        PâQâS
%:      ------------------------------------â_3
%:                    PâQâRâS
%:
%:                     ^foo
%:
$$\pu \ded{foo}$$
%
is'' a proof for:
%
%$$âP,Q,R,SâΩ.\; (P â_H R)â(Q â_H S) â ((P â_H Q) â_H (R â_H S)).$$
%
$$âP,Q,R,SâΩ.\; (P â R)â(Q â S) â ((P â Q) â (R â S)).$$

%  ____            _               _              _
% |  _ \  ___ _ __(_)_   _____  __| |  _ __ _   _| | ___  ___
% | | | |/ _ \ '__| \ \ / / _ \/ _ | | '__| | | | |/ _ \/ __|
% | |_| |  __/ |  | |\ V /  __/ (_| | | |  | |_| | |  __/\__ \
% |____/ \___|_|  |_| \_/ \___|\__,_| |_|   \__,_|_|\___||___/
%
% Â«derived-rulesÂ» (to ".derived-rules")
% (phap 12)
\subsection{Derived rules}
\label     {derived-rules}

\def\HAness{\mathsf{HA-ness}}
\def\HAness{\textsf{HA-ness}}

{\sl Note:} in this section we will ignore the operators $â$' and
$Â$' in PC-structures; we will think that every $PâQ$' is as
abbreviation for $(P{â}Q)â(Q{â}P)$' and every $ÂP$' is an
abbreviation for $P{â}â$'.

We'll write $[â_1], \ldots, [â_2]$ for the linear'' versions of the
rules in last section --- for example, $[â_2]$ is $(âP,Q,RâΩ.\; (PâQâR) â (PâQ{â}R))$ --- and if $S=(r_1,\ldots,r_n)$ is a set of
rules, each in tree form, then $[S]=[r_1]â\ldotsâ[r_n]$, and an
$S$-tree'' is a proof in tree form that only uses rules that are in
the set $S$.

\msk

Let $\HAness_1$, $\HAness_2$, $\HAness_3$, be these sets, with the
rules from sec.\ref{logic-in-HAs}:
%
%$$\HAness_1 = \{\id,\comp,â_1,â_1,â_1,â_2,â_3,â_1,â_2,â_3,â_1,â_2\},$$
$$\begin{array}{rcl} \HAness_1 &=& \{\id,\comp,â_1,â_1, â_3, â_3, â_2\}, \\ \HAness_2 &=& \{ â_1,â_2, â_1,â_2, â_1 \}, \\ \HAness_3 &=& \HAness_1 âª \HAness_2 \\ \end{array}$$
%
and let $\HAness_4$, $\HAness_5$ and $\HAness_7$ be these ones, where the new rules
are the ones at the left column of fig.\ref{derived-rules-1}:
%
$$\begin{array}{rcl} \HAness_4 &=& \{â_4,â_5,â_4,â_5,\MP_0,\MP\} \\ \HAness_5 &=& \HAness_1 âª \HAness_4 \\ \HAness_7 &=& \HAness_1 âª \HAness_2 âª \HAness_4 \\ \end{array}$$

% (laop 8)
% (find-LATEX "2016-2-LA-logic.tex" "derived-rules")

%:
%:                   ---------\id\subst{P:=QâR}
%:                   QâRâQâR
%:   ------â_4  :=  ---------â_1\subst{P:=QâR}
%:   QâRâQ          QâRâQ
%:
%:   ^and4a           ^and4b
%:
%:
%:                   ---------\id\subst{P:=QâR}
%:                   QâRâQâR
%:   ------â_5  :=  ---------â_2\subst{P:=QâR}
%:   QâRâR          QâRâR
%:
%:   ^and5a           ^and5b
%:
%:                   ---------\id\subst{P:=PâQ}
%:                   PâQâPâQ
%:   ------â_4  :=  ---------â_1\subst{R:=PâQ}
%:   PâPâQ           PâPâQ
%:
%:   ^or4a            ^or4b
%:
%:                   ---------\id\subst{P:=PâQ}
%:                   PâQâPâQ
%:   ------â_5  :=  ---------â_2\subst{R:=PâQ}
%:   QâPâQ           QâPâQ
%:
%:   ^or5a            ^or5b
%:
%:                                                ---------\id
%:                                                Q{â}RâQ{â}R
%:                       ------------------\id    --------------â_1
%:                       Qâ(Q{â}R)â(Q{â}R)âQ     (Q{â}R)âQâR
%:  -----------\MP_0 :=  ---------------------------------------\comp   (wrong)
%:  Qâ(Q{â}R)âR                   Qâ(Q{â}R)âR
%:
%:    ^MP0L                         ^MP0R
%:
%:
%:
%:                        ---------\id
%:                        Q{â}RâQ{â}R
%:  -----------\MP_0 :=   --------------â_1
%:  Qâ(Q{â}R)âR         (Q{â}R)âQâR
%:
%:    ^MP0L                  ^MP0R
%:
%:                          PâQ  PâQ{â}R
%:                          ------------    ----------\MP_0
%:  PâQ  PâQ{â}R          PâQâ(Q{â}R)      Qâ(Q{â}R)âR
%:  ------------\MP  :=     --------------------------\comp
%:      PâR                         PâR
%:
%:      ^MPL                         ^MPR
%:
\begin{figure}[htbp]
\pu
$$\fbox{ \begin{array}{rcl} \ded{and4a} &:=& \ded{and4b} \\\\ \ded{and5a} &:=& \ded{and5b} \\\\ \ded{or4a} &:=& \ded{or4b} \\\\ \ded{or5a} &:=& \ded{or5b} \\\\ \ded{MP0L} &:=& \ded{MP0R} \\\\ \ded{MPL} &:=& \ded{MPR} \\\\ \end{array} }$$
\caption{Derived rules}
\label{derived-rules-1}
\end{figure}

%:
%:
%:
%:                              ------â_4
%:   PâQâR            PâQâR   QâRâQ
%:   ------â_1   :=   ----------------\comp
%:    PâQ                  PâQ
%:
%:    ^and1a                ^and1b
%:
%:                               ------â_5
%:   PâQâR             PâQâR   QâRâR
%:   ------â_2   :=    ----------------\comp
%:    PâR                   PâR
%:
%:    ^and2a                 ^and2b
%:
%:
%:
%:                     ------â_4
%:   PâQâR            PâPâQ     PâQâR
%:   ------â_1  :=    ------------------\comp
%:    PâR                   PâR
%:
%:    ^or1a                  ^or1b
%:
%:                     ------â_5
%:   PâQâR            QâPâQ     PâQâR
%:   ------â_2  :=    ------------------\comp
%:    QâR                   QâR
%:
%:    ^or2a                  ^or2b
%:
%:
%:                                 ------â_4
%:                                 PâQâP     PâQ{â}R
%:                    ------â_5    ------------------\comp
%:                    PâQâQ         PâQâQ{â}R
%:                    --------------------------â_3    -------------\MP_0
%:  PâQ{â}R              PâQâQâ(Q{â}R)              Qâ(Q{â}R)âR
%:  ---------â_1  :=  ----------------------------------------------\comp
%:  PâQâR                    PâQâR
%:
%:  ^imp2a                    ^imp2b
%:
\begin{figure}[htbp]
\pu
$$\fbox{ \begin{array}{rcl} \\ \ded{and1a} &:=& \ded{and1b} \\\\ \ded{and2a} &:=& \ded{and2b} \\\\ \ded{or1a} &:=& \ded{or1b} \\\\ \ded{or2a} &:=& \ded{or2b} \\\\ %\ded{imp2a} &:=& \ded{imp2b} \\\\ \ded{imp2a} &:=& \\\\ \multicolumn{3}{c}{\phantom{mm}\ded{imp2b}} \\\\ \end{array} }$$
\caption{Derived rules (2)}
\label{derived-rules-2}
\end{figure}

% (find-xpdfpage "~/LATEX/2010unilog-current.pdf" 52)

Note that the trees in the right of fig.\ref{derived-rules-1} are
$\HAness_3$-trees.

Fig.\ref{derived-rules-1} can be interpreted in two ways. The first
one is that it shows that
%
$$\begin{array}{rcl} [\HAness_3] &â& [â_4], \\ \relax [\HAness_3] &â& [â_5], \\ \relax [\HAness_3] &â& [â_4], \\ \relax [\HAness_3] &â& [â_5], \\ \relax [\HAness_3] &â& [\MP_0], \\ \relax [\HAness_3] &â& [\MP], \\ \relax [\HAness_3] &â& [\HAness_4], \\ \relax [\HAness_3] &â& [\HAness_7]; \\ \end{array}$$
%
the second one is that it shows a way to replace occurrences of $â_4$,
$â_5$, $â_4$, $â_5$, $\MP_0$, $\MP$. Take an $\HAness_7$-tree, $T$.
Call it hypotheses $H_1, \ldots, H_n$, and its conclusion $C$, Replace
each occurrence of $â_4$, $â_5$, $â_4$, $â_5$, $\MP_0$, $\MP$ in $T$
by the corresponding tree in the right side of
fig.\ref{derived-rules-1}. The result is a new tree, $T'$, which is
equivalent'' to $T$ in the sense of having the same hypotheses and
conclusion as $T$. So,
%
\begin{itemize}

\item every $\HAness_3$-tree is an $\HAness_7$-tree,

\item every $\HAness_7$-tree is equivalent'' to an $\HAness_3$-tree.

\end{itemize}

We call this trick derived rules'' --- the rules in $\HAness_4$ are
derived'' from $\HAness_3$, and $\HAness_3$ and $\HAness_7$ are
equivalent'' in the sense that they prove the same things''.

Now look at fig.\ref{derived-rules-2}. It has the rules in $\HAness_2$
at the left, and $\HAness_5$-trees at the right; it shows that
%
$$\begin{array}{rcl} [\HAness_5] &â& [â_1], \\ \relax [\HAness_5] &â& [â_2], \\ \relax [\HAness_5] &â& [â_1], \\ \relax [\HAness_5] &â& [â_2], \\ \relax [\HAness_5] &â& [â_2], \\ \relax [\HAness_5] &â& [\HAness_2], \\ \relax [\HAness_5] &â& [\HAness_7], \\ \end{array}$$
%
and it also shows how to take an $\HAness_7$-tree $T$ and replace
every occurrence of an $\HAness_4$-rule in it by an $\HAness_3$-tree,
producing an $\HAness_3$-tree $T'$ which is equivalent'' to $T$.
This means that:
%
\begin{itemize}

\item every $\HAness_5$-tree is an $\HAness_7$-tree,

\item every $\HAness_7$-tree is equivalent'' to an $\HAness_5$-tree,

\end{itemize}
%
and that $\HAness_3$, $\HAness_7$ and $\HAness_5$ are all equivalent''.

% \bsk
%
% \def\ab{\ang{a,b}}
% \def\cd{\ang{c,d}}
% \def\ef{\ang{e,f}}
%
% Let's establish a partial order on $\LR$: we say that $\ab â \cd$ iff
% $aâc$ and $bâd$.
%
% We define intervals'' in $\LR$ as:
% %
% $$[\ab,\ef] := \setofst {\cd â \LR} {\ab â \cd â \ef}$$
% %
% If $\abâ\ef$ then $[\ab,\ef]$ is a lozenge with $\ab$ at the bottom
% and $\ef$ at the top; if $\ab \notâ \ef$ then $[\ab,\ef]$ is empty.
%
% We say thay a subset $S \subset \LR$ is {\sl convex} when $\ab,\efâS$
% implies $[\ab,\ef]\subset S$.
%
% \msk

% __        ___                         _         ______   _    _       ___
% \ \      / / |__   ___ _ __ ___    __| | ___   |__  / | | |  / \   __|__ \
%  \ \ /\ / /| '_ \ / _ \ '__/ _ \  / _ |/ _ \    / /| |_| | / _ \ / __|/ /
%   \ V  V / | | | |  __/ | |  __/ | (_| | (_) |  / /_|  _  |/ ___ \\__ \_|
%    \_/\_/  |_| |_|\___|_|  \___|  \__,_|\___/  /____|_| |_/_/   \_\___(_)
%
% Â«where-do-ZHAs-come-fromÂ» (to ".where-do-ZHAs-come-from")
% (phap 11)

% \section{Where do ZHAs come from?}
% \label  {where-do-ZHAs-come-from}
%
% In almost any Topos Theory book we find the following facts:
% %
% % \begin{itemize}
% % \item The logic of a Heyting Algebras is intuitionistic'', i.e.:
% % \item HAs are the models for Intuitionistic Proposition Logic,
% % \item Topologies are HAs,
% % \item HAs are Cartesian Closed Categories (CCCs''),
% % \item For any small category $\catC$ the functor category $\catC^\catTwo$ is a HA.
% % \end{itemize}
% % %
% % These other facts are less well-known:
% % %
% % \begin{itemize}
% % \item Finite topologies are Alexandroff,
% % \item Finite topologies are order topologies on finite DAGs.
% % \end{itemize}
%
% 1) The logic of a Heyting Algebras is intuitionistic'', i.e.:
%
% 2) HAs are the models for Intuitionistic Proposition Logic,
%
% 3) Topologies are HAs,
%
% 4) HAs are Cartesian Closed Categories (CCCs''),
%
% 5) For any small category $\catC$ the functor category $\catC^\catTwo$ is a HA.
%
% \ssk
%
% \noindent These other facts are less well-known:
%
% 6) Finite topologies are Alexandroff,
%
% 7) Finite topologies are order topologies on finite DAGs.
%
% \ssk
%
% In this section we will see how ZHAs appear as topologies on thin''
% finite DAGs. I've tried to structure the explanation to make it
% accessible to people who don't know the concepts above, and to make it
% an introduction to some of those concepts.

%  _____                 _             _
% |_   _|__  _ __   ___ | | ___   __ _(_) ___  ___
%   | |/ _ \| '_ \ / _ \| |/ _ \ / _ | |/ _ \/ __|
%   | | (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
%   |_|\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%           |_|                  |___/
%
% Â«topologiesÂ» (to ".topologies")
\section{Topologies}
\label  {topologies}

The best way to connect ZHAs to several standard concepts is by seeing
that ZHAs are topologies on certain finite sets --- actually on
2-column acyclical graphs. This will be done here and in the next few
sections.

\msk

\noindent
A {\sl topology} on a set $X$ is a subset $\calS$ of $\Pts(X)$ such
that:

1) $\calS$ contains $X$ and $\void$,

2) if $P,Qâ\calS$ then $\calS$ contains $PâQ$ and $PâªQ$,

3) if $\calS' â \calS$ then $\calS$ contains $\bigcup \calS'$.

A {\sl topological space} is a pair $(X,\calS)$ where $X$ is a set and
$\calS$ is a topology on $X$.

When $(X,\calS)$ is a topological space and $Uâ\calS$ we say that $U$
is {\sl open} in $(X,\calS)$.

\ssk

% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L X = "1.2|.3.|4.5"
%L mp = MixedPicture.new({def="dagX", meta="s", scale="4.5pt"}, z):zfunction(X):output()
\pu

For example, let $X$ be the ZSet $\dagXâââââ$, and let's use the
characteristic function notation from sec.\ref{positional} to denote
its subsets --- we write $X=\dagX11111$ and $\void=\dagX00000$ instead
of $X=\dagXâââââ$ and $\void=\dagXÂÂÂÂÂ$.

If $\calS = \left\{\dagX10000, \, \dagX01000, \, \dagX00100, \, \dagX00010, \, \dagX00001 \right\}$ then $\calSâ\Pts(X)$ but $\calS$
fails all the conditions in 1, 2, 3 above:

1) $X=\dagX11111 \notâ \calS$ and $\void=\dagX00000 \notâ \calS$

2) Let $P=\dagX10000â\calS$ and $Q=\dagX01000â\calS$. Then
$PâQ=\dagX00000 \notâ \calS$ and $PâªQ=\dagX11000 \notâ \calS$.

3) Let $\calS' = \left\{\dagX01000, \, \dagX00100, \, \dagX00010 \right\} â \calS$. Then $\bigcup\calS' = \dagX01000 âª \dagX00100 âª \dagX00010 = \dagX01110 \notâ \calS$.

\msk

Now let $K=\dagKiteâââââ$ and $\calS = \left\{ \dagKite00000, \, \dagKite00001, \, \dagKite00011, \, \dagKite00111, \, \dagKite01011, \, \dagKite01111, \, \dagKite11111 \right\}$. In this case $(K,\calS)$ is a topological space.

\bsk

Some sets have default'' topologies on them, denoted with
$\Opens$'. For example, $\R$ is often used to mean the topological
space $(\R, \Opens(\R))$, where:
%
$$\Opens(\R) = \setofst {Uâ\R} {U \text{ is a union of open intervals}}.$$
%
We say that a subset $Uâ\R$ is open in $\R$'' (in the default
sense''; note that now we are saying just open in $\R$'', not open
in $(\R, \Opens(\R))$'') when $U$ is a union of open intervals, i.e.,
when $Uâ\Opens(\R)$; but note that $\Pts(\R)$ and $\{\void,\R\}$ are
also topologies on $\R$, and:
%
$$\begin{array}{lclll} \{2,3,4\} â\Pts(\R), &\text{so}& \{2,3,4\} \text{ is open in } (\R,\Pts(\R)), \\ \{2,3,4\}\notâ\Opens(\R), &\text{so}& \{2,3,4\} \text{ is not open in } (\R,\Opens(\R)), \\ \{2,3,4\}\notâ\{\void,\R\}, &\text{so}& \{2,3,4\} \text{ is not open in } (\R,\{\void,\R\}); \\ \end{array}$$
%
when we say just $U$ is open in $X$'', this means that:

1) $\Opens(X)$ is clear from the context, and

2) $Uâ\Opens(X)$.

%  _____                               _________       _
% |_   _|__  _ __  ___    ___  _ __   |__  / ___|  ___| |_ ___
%   | |/ _ \| '_ \/ __|  / _ \| '_ \    / /\___ \ / _ \ __/ __|
%   | | (_) | |_) \__ \ | (_) | | | |  / /_ ___) |  __/ |_\__ \
%   |_|\___/| .__/|___/  \___/|_| |_| /____|____/ \___|\__|___/
%           |_|
%
% Â«topologies-on-ZSetsÂ» (to ".topologies-on-ZSets")
\section{The default topology on a ZSet}
\label  {topologies-on-ZSets}

Let's define a default topology $\Opens(D)$ for each ZSet $D$.

\msk

For each ZSet $D$ we define $\Opens(D)$ as:
%
$$\label{O(D)} \Opens(D) := \setofst {UâD} {â((x,y),(x',y')){â}\BPM(D). \; ((x,y){â}U â (x',y'){â}U)}$$
%
whose visual meaning is this. Turn $D$ into a ZDAG by adding arrows
for the black pawns moves (sec.\ref{ZDAGs}), and regard each subset
$UâD$ as a board configuration in which the black pieces may move down
to empty positions through the arrows. A subset $U$ is stable'' when
no moves are possible because all points of $U$ ahead'' of a black
piece are already occupied by black pieces; a subset $U$ is
non-stable'' when there is at least one arrow
$((x,y),(x',y'))â\BPM(D)$ in which $(x,y)$ had a black piece and
$(x',y')$ is an empty position.

In our two notations for subsets (sec.\ref{positional}) a subset $UâD$
is unstable when it has an arrow like $ââÂ$' or $1â0$'; remember
that black pawn moves arrows go down. A subset $UâD$ is stable when
none of its $â$'s or $1$'s can move down to empty positions.

% A subset $UâD$ is open iff it is stable.

Open'' is the same as stable''. $\Opens(D)$ is the set of stable
subsets of $D$.

\msk

Some examples:

$\dagKite00100$ is not open because it has a 1 above a 0,

$\Opens(\dagKiteâââââ) = \left\{ \dagKite00000, \, \dagKite00001, \, \dagKite00011, \, \dagKite00111, \, \dagKite01011, \, \dagKite01111, \, \dagKite11111 \right\}$,

$\Opens(\dagHouseâââââ) = \left\{ \dagHouse00000, \, \dagHouse00001, \, \dagHouse00010, \, \dagHouse00011, \, \dagHouse00101, \, \dagHouse00111, \, \dagHouse01010, \, \dagHouse01011, \, \dagHouse01111, \, \dagHouse11111 \right\}$.

\msk

The definition of $\Opens(D)$ above can be generalized to any directed
graph. If $(A,R)$ is a directed graph, then $(A,\Opens_R(A))$ is a
topological space if we define:
%
$$\Opens_R(A) := \setofst{UâA}{â(a,b)âR.\;(aâUâbâU)}$$
%
The two definitions are related as this: $\Opens(D) = \Opens_{\BPM(D)}(D)$.

Note that we can see the arrows in $\BPM(D)$ or in $R$ as {\sl
obligations} that open sets must obey; each arrow $aâb$ says that
every open set that contains $a$ is forced to contain $b$ too.

%  _____                                           _
% |_   _|__  _ __  ___    __ _ ___    ___  _ __ __| | ___ _ __ ___
%   | |/ _ \| '_ \/ __|  / _ / __|  / _ \| '__/ _ |/ _ \ '__/ __|
%   | | (_) | |_) \__ \ | (_| \__ \ | (_) | | | (_| |  __/ |  \__ \
%   |_|\___/| .__/|___/  \__,_|___/  \___/|_|  \__,_|\___|_|  |___/
%           |_|
%
% Â«topologies-as-partial-ordersÂ» (to ".topologies-as-partial-orders")
\section{Topologies as partial orders}
\label  {topologies-as-partial-orders}

For any topological space $(X,\Opens(X))$ we can regard $\Opens(X)$ as
a partial order, ordered by inclusion, with $\void$ as its minimal
element and $X$ as its maximal element; we denote that partial order
by $(\Opens(X),â)$.

Take any ZSet $D$. The partial order $(\Opens(D),â)$ will {\sl
sometimes} be a ZHA when we draw it with $\void$ at the bottom, $D$
at the top, and inclusions pointing up, as can be seen in the three
figures below; when $D=\dagHouseâââââ$ or $D=\dagGuillââââââ$ the
result is a ZHA, but when $D=\dagWâââââ$ it not.

Let's write $Vâ_1U$'' for $VâU$ and $V$ and $U$ differ in exactly
one point''. When $D$ is a ZSet the relation $â$ on $\Opens(D)$ is the
transitive-reflexive closure of $â_1$, and $(\Opens(D),â_1)$ is easier
to draw than $(\Opens(D),â)$.

% (find-angg ".emacs" "find-planarhas")
% (find-planarhas       "background-story")
% (find-planarhaspage 8 "Background story")
% (find-planarhastext 8 "Background story")
% (find-planarhas       "background-story-2")
% (find-planarhaspage 9 "Background story, 2")
% (find-planarhastext 9 "Background story, 2")

%R local house, ohouse = 2/  #1  \, 7/       !h11111                     \
%R                        |#2  #3|   |              !h01111              |
%R                        \#4  #5/   |       !h01011       !h00111       |
%R                                   |!h01010       !h00011       !h00101|
%R                                   |       !h00010       !h00001       |
%R                                   \              !h00000              /

%R local guill, oguill = 2/  #1  #2\, 8/                !g111111                \
%R                        |#3  #4  |   |        !g101111        !g011111        |
%R                        \  #5  #6/   |                !g001111        !g010111|
%R                                     |        !g001011        !g000111        |
%R                                     |!g001010        !g000011                |
%R                                     |        !g000010        !g000001        |
%R                                     \                !g000000                /
%R
{\pu
$$\def\h{\zfHouse} (H,\BPM(H)) = \zdagHouse \qquad (\Opens(H), â_1) = \zdagOHouse$$

$$\def\g{\zfGuill} (G,\BPM(G)) = \zdagGuill \qquad (\Opens(G), â_1) = \zdagOGuill$$
}
%
%R local w, womit, W =
%R 2/#1  #2  #3\, 2/    a     \, 7/              !w11111              \
%R  \  #4  #5  /   |  b c d   |   |       !w11011!w10111!w01111       |
%R                 |  e f g   |   |       !w10011!w01011!w00111       |
%R                 |h   i   j |   |!w10010       !w00011       !w00101|
%R                 |  k   l   |   |       !w00010       !w00001       |
%R                 \    m     /   \              !w00000              /
%
$$\pu \def\w{\zfW} (W,\BPM(W)) = \zdagW \qquad (\Opens(W), â_1) = \zdagOW$$

We can formalize a way to draw $\Opens(D)$ as a ZHA'' (or ...as a
ZDAG'') as a bijective function $f$ from a ZHA (or from a ZSet) $S$ to
$\Opens(D)$ that creates a perfect correspondence between the white
moves in $S$ and the $Vâ_1U$-arrows''; more precisely, an $f$ such
that this holds: if $a,bâS$ then $(a,b)â\WPM(S)$ iff $f(a)â_1f(b)$.

Note that the {\sl number of elements} in an open set corresponds to
the {\sl height} where it is drawn; if $f:Sâ\Opens(D)$ is a way to
draw $\Opens(D)$ as a ZHA or a ZDAG then $f$ takes points of the form
$(\_\_,y)$ to open sets with $y$ elements, and if $f:Sâ\Opens(D)$ is a
way to draw $\Opens(D)$ as a ZHA (not a ZDAG!) then we also have that
$f((0,0)) = \void â \Opens(D)$.

\msk

The diagram for $(\Opens(H), â_1)$ above is a way to draw $\Opens(H)$
as a ZHA.

The diagram for $(\Opens(G), â_1)$ above is a way to draw $\Opens(H)$
as a ZHA.

The diagram for $(\Opens(W), â_1)$ above is {\sl not} a way to draw
$\Opens(W)$ as a ZSet. Look at $\dagW01011$ and $\dagW10111$ in the
middle of the cube formed by all open sets of the form $\dagW abc11$.
We don't have $\dagW01011 â_1 \dagW10111$, but we do have a white pawn
move (not draw in the diagram!) from $fÂ(\dagW01011)$ to
$fÂ(\dagW10111)$. We say that a ZSet is {\sl thin} when it doesn't
have three independent points.

\msk

Every time that a ZSet $D$ has three independent points, as in $W$, we
will have a situation like in $(\Opens(W), â_1)$; for example, if
$B=\dagHexâââââââ$ then the open sets of $B$ of the form
$\dagHex00abc11$ form a cube.

% \bsk
% \bsk
% \bsk
%
%
% The definition for $\Opens(D)$ in page \pageref{O(D)} can be generalized
% to any directed graph. If $(A,R)$ is a directed graph, then
% %
% $$\Opens(A,R) := \setofst {UâA} {â(a,b){â}R.\; (a{âU}âb{âU})},$$
% %
% is the {\sl set of down-sets} on $A$ (see DaveyPriestley, pp.20-21).
% There are some directed graphs,

%  ____   ____ ____
% |___ \ / ___/ ___|___
%   __) | |  | |  _/ __|
%  / __/| |__| |_| \__ \
% |_____|\____\____|___/
%
% Â«2CGsÂ» (to ".2CGs")
\section{2-Column Graphs}
\label  {2CGs}

\def\LC {\mathsf{LC}}
\def\RC {\mathsf{RC}}
\def\TCG{\mathsf{2CG}}
\def\pile{\mathsf{pile}}
\def\l#1{#1\_}
\def\r#1{\_#1}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\ltol#1#2{#1\_{\to}#2\_}
\def\rtor#1#2{\_#1{\to}\_#2}

Note: in this section we will manipulate objects with names like $1\_, 2\_, 3\_, \ldots,$ $\_1, \_2, \_3, \ldots$; here are two good ways to
formalize them:
%
$$\begin{array}{cc} \vdots & \vdots \\ 4\_=(0,4) & \_4=(1,4) \\ 3\_=(0,3) & \_3=(1,3) \\ 2\_=(0,2) & \_2=(1,2) \\ 1\_=(0,1) & \_1=(1,1) \\ \end{array} \quad \text{or} \quad \begin{array}{cc} \vdots & \vdots \\ 4\_=\verb|"4_"| & \_4=\verb|"_4"| \\ 3\_=\verb|"3_"| & \_3=\verb|"_3"| \\ 2\_=\verb|"2_"| & \_2=\verb|"_2"| \\ 1\_=\verb|"1_"| & \_1=\verb|"_1"| \\ \end{array},$$
%
where \verb|"1_"|, \verb|"_2"|, \verb|""|, \verb|"Hello!"|, etc are
strings.

\msk

We define:
%
$$\begin{array}{ccc} LC(l) &:=& \{1\_, 2\_, \ldots, l\_\} \\ RC(l) &:=& \{\_1, \_2, \ldots, \_r\}, \\ \end{array}$$
%
which generate a left column'' of height $l$ and a right column''
of height $r$.

A {\sl description for a 2-column graph} (a D2CG'') is a 4-tuple
$(l,r,R,L)$, where $l,râ\N$, $Râ\LC(l)Ã\RC(r)$, $Lâ\RC(r)Ã\LC(l)$; $l$
is the height of the left column, $r$ is the height of the right
column, and $R$ and $L$ are set of intercolumn arrows (going right and
left respectively).

The operation $\TCG$ (in a sans-serif font) generates a directed graph
from a D2CG:

$$\begin{array}{rcl} \TCG(l,r,R,L) &:=& \left(\LC(l)âª\RC(r), \csm{\{\ltol{l}{(l-1)}, \;\ldots, \;\ltol21\}âª \\ \{\rtor{r}{(r-1)}, \;\ldots, \;\rtor21\}âª \\ RâªL } \right) \end{array}$$

For example,
%
$$\begin{array}{rcl} \TCG(3,4,\csm{\ltor34, \\ \ltor23}, \csm{\lotr22, \\ \lotr12}) &:=& \left(\csm{\phantom{\l4,}\; \l3, \; \l2, \; \l1, \\ \r4, \; \r3, \; \r2, \; \r1 \\ }, \csm{\phantom{\rtor43,\;}\ltol32,\; \ltol21, \\ \rtor43 ,\; \rtor32,\; \rtor21, \\ \ltor34,\;\ltor23, \\ \lotr22,\;\lotr12 \\ } \right) \end{array}$$
%
which is:
%
%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
%L
%L tcg = TCG.new(tcg_big,    "foo", 3, 4, "34 23", "22 12"):lrs():vs():hs():output()
$$\pu \foo$$
%
we will usually draw that more compactly, by omitting the intracolumn
(i.e., vertical) arrows:
%
%L tcg_spec = "3, 4; 34 23, 22 12"
%L tcgmed("foo"):lrs():hs():output()
%L tcgmed("bar"):bus():hs():output()
$$\pu \foo \quad \text{or} \quad \bar.$$

A {\sl 2-column graph} (a 2CG'') is a directed graph that is of the
form $\TCG(l,r,R,L)$. We will often say $(P,A) = \TCG(l,r,R,L)$, where
the $P$ stand for points'' and $A$ for arrows''.

A {\sl 2-column acyclical graph} (a 2CAG'') is a 2CG that doesn't
have cycles. If $L$ has an arrow that is the opposite of an arrow in
$R$, this generates a cycle of length 2; if $R$ has an arrow
$\ltor{l}{r'}$ and $L$ has an arrow $\lotr{l'}{r}$, where $lâl'$ and
$râr'$, this generates a cycle that can have a more complex shape ---
a triangle or a bowtie. For example,

%L tcg_spec = "4, 3; 32, 32"
%L tcgbig("foo"):lrs():vs():hs():output()
%L tcg_spec = "3, 4; 14, 32"
%L tcgbig("bar"):lrs():vs():hs():output()
$$\pu \foo \quad \text{and} \quad \bar.$$

%  _____                               ____   ____ ____
% |_   _|__  _ __  ___    ___  _ __   |___ \ / ___/ ___|___
%   | |/ _ \| '_ \/ __|  / _ \| '_ \    __) | |  | |  _/ __|
%   | | (_) | |_) \__ \ | (_) | | | |  / __/| |__| |_| \__ \
%   |_|\___/| .__/|___/  \___/|_| |_| |_____|\____\____|___/
%           |_|
%
% Â«topologies-on-2CGsÂ» (to ".topologies-on-2CGs")
\section{Topologies on 2CGs}
\label  {topologies-on-2CGs}

\catcodeâ=13 \defâ{\dnto}
\catcodeâ=13 \defâ{{\dnto}}

In this section we will see that ZHAs are topologies on 2CAGs.

\msk

\noindent
Let $(P,A) = \TCG(l,r,R,L)$ be a 2-column graph.

\noindent
What happens if we look at the open sets of $(P,A)$, i.e., at
$\Opens_A(P)$? Two things:

1) every open set $Uâ\Opens_A(P)$ is of the form $\LC(a)âª\LC(b)$,

2) arrows in $R$ and $L$ forbids some $\LC(a)âª\LC(b)$'s from being
open sets.

\noindent
In order to understand that we need to introduce some notations for
piles''.

\msk

The function
%
$$\pile(\ang{a,b}) := \LC(a)âª\LC(b)$$
%
converts an element $\ang{a,b}â\LR$ into a pile of elements in the
left column of height $a$ and a pile of elements in the right column
of height $b$. We will write subsets of the points of a 2CG using a
positional notation with arrows. So, for example, if $(P,A) = \TCG(3,4,\{\ltor23\}, \{\lotr22\})$ then
%
%L tcg_spec = "3, 4; 23, 22"
%L tcgmed("foo"):lrs():hs():output()
%L tcgmed("bar"):cs("110", "1000"):hs():output()
$$\pu (P,A)=\foo \qquad \text{and} \qquad \pile(21) = \bar \;\; \text{(as a subset of P)}.$$

Note that $\pile(21)$ is not open in $(P,\Opens_A(P))$, as it has an
arrow $1â0$'. In fact, the presence of the arrow $\{\ltor23\}$ in $A$
means that all piles of the form
%
%L tcgmed("bar"):cs("11?", "??00"):hs():output()
$$\pu \bar$$
%
are not open, the presence of the arrow $\{\lotr22\}$ means that the
piles of the form
%
%L tcgmed("bar"):cs("?00", "11??"):hs():output()
$$\pu \bar$$
%
are not open sets.

The effect of these prohibitions can be expressed nicely with
implications. If
%
$$(P,A) = \TCG(l,r,\csm{\ltor cd, \\ \ltor ef}, \csm{\lotr gh, \\ \lotr ij})$$
%
then
%
$$\Opens_A(P) = \setofst {\pile(ab)} {aâ\{0,\ldots,l\}, bâ\{0,\ldots,r\}, \psm {aâc â bâd \; â \\ aâe â bâf \; â \\ aâg â bâh \; â \\ aâi â bâj \;\;\; \\ } }$$

Let's use a shorter notation for comparing 2CGs and their topologies:
%
%L tcg_spec = "4, 5; 32, 14 25"
%L tcgbig("foo"):lrs():hs():vs():output()
%L z = LR.fromtwocolgraph(4, 5, "32", "14 25"):zha()
$$\pu \Opens \foo \quad = \quad \bar % \bigthinge$$
%
the arrows in $R$ and $L$ and the values of $l$ and $r$ are easy to
read from the 2CG at the left, and we omit the $\pile$'s at the
right.

\msk

In a situation like the above we say that the 2CG in the
$\Opens(\ldots)$' {\sl generates} the ZHA at the right. There is an
easy way to draw the ZHA generated by a 2CG, and a simple way to find
the 2CG that generates a given ZHA. To describe them we need two new
concepts.

If $(A,R)$ is a directed graph and $SâA$ then $âS$ is the smallest
open set in $\Opens_R(A)$ that contains $S$. If $(A,R)$ is a ZDAG with
black pawns moves as its arrows, think that the 1's in $S$ are
painted with a black paint that is very wet, and that that paint flows
into the 0's below; the result of $âS$ is what we get when all the
0's below 1's get painted black. For example: $â\dagGuill010000 = \dagGuill010111$. When $(P,A)$ is a 2CG and $SâP$, we have to think
that the paint flows along the arrows, even if some of the intercolumn
arrows point upward. For example:
%
%L tcg_spec = "3, 4; 23, 22"
%L tcgmed("foo"):cs("100", "0100"):hs():output()
%L tcgmed("bar"):cs("110", "1110"):hs():output()
%
$$\pu â\foo = \bar$$
%
and if $S$ consists of a single point, $S=\{s\}$, then we may write
$âs$ instead of $â\{s\} = âS$. In the 2CG above, we have (omitting the
$\pile$'s):
%
%L tcgmed("foo"):cs("000", "0100"):hs():output()
%L tcgmed("bar"):cs("110", "1110"):hs():output()
%
$$\pu â\r2 \;=\; â\{\r2\} =\; â\foo = \bar = \;23, \quad \text{and} \quad \sm{ && â\r4=24, \\ â\l3=33, && â\r3=23, \\ â\l2=23, && â\r2=23, \\ â\l1=10, && â\r1=01, \\ }$$

The second concept is this: the generators'' of a ZDAG $D$ with
white pawns moves as its arrows --- or of a ZHA $D$ --- are the points
of $D$ that have exactly one white pawn move pointing {\sl to} them
(not {\sl going out of} them).

\msk

If $(P,A)$ is a 2CAG, then $\Opens_A(P)$ is a ZHA, and $â$' is a
bijection from $P$ to the generators of $\Opens_A(P)$; for example:
%L tcg_spec = "4, 5; 32, 14 25"
%L tcgbig("foo"):lrs():hs():vs():output()
%L z = LR.fromtwocolgraph(4, 5, "32", "14 25"):zha()
$$\pu \Opens \foo \quad = \quad \bar \qquad \qquad \poo % \bigthinge$$
%
but if $(P,A)$ is a 2CG with cycles, then $\Opens_A(P)$ is not a ZHA
because each cycle generates a gap'' that disconnects the points of
$\Opens_A(P)$. We just saw an example of a 2CG with a cycle in which
$â\l2 = 23 = â\r3 = â\r2$; look at its topology:
%
%R tcg_spec = "3, 4; 23, 22"
%R tcgbig("foo"):lrs():vs():hs():output()
%R local top =
%R 2/    34  \
%R  |  33  24|
%R  |    23  |
%R  |        |
%R  |        |
%R  |  11    |
%R  |10  01  |
%R  \  00    /
%
$$\pu \Opens\foo \quad = \quad \bar$$

%  ______   _    _            __   __     ____   ____    _    ____
% |__  / | | |  / \   ___    / /   \ \   |___ \ / ___|  / \  / ___|___
%   / /| |_| | / _ \ / __|  / /_____\ \    __) | |     / _ \| |  _/ __|
%  / /_|  _  |/ ___ \\__ \  \ \_____/ /   / __/| |___ / ___ \ |_| \__ \
% /____|_| |_/_/   \_\___/   \_\   /_/   |_____|\____/_/   \_\____|___/
%
% Â«converting-ZHAs-2CAGsÂ» (to ".converting-ZHAs-2CAGs")
\section{Converting bewteen ZHAs and 2CAGs}
\label  {converting-ZHAs-2CAGs}

Let's now see how to start from a 2CAG and produce its topology (a
ZHA) quickly, and how to find quickly the 2CAG that generates a given
ZHA.

\msk

{\sl From 2CAGs to ZHAs.} Let $(P,A) = \TCG(l,r,R,L)$ be a 2CAG, and
call the ZHA generated by it $H$. Then the top point of $H$ is $lr$,
its bottom point is 00. Let $C := \{00, â\l1, â\l2, \ldots, â\l l, lr\}$; then $C$ has some of the points of the left wall
(sec.\ref{ZHAs}) of $H$, but usually not all. To complete'' $C$,
apply this operation repeatedly: if $abâC$ and $abâlr$, then test if
either $(a+1)b$ or $a(b+1)$ are in $C$; if none of them are, add
$a(b+1)$, which is northeast of $ab$. When there is nothing else to
add, then $C$ is the whole of the left wall of $H$. For the right
wall, start with $D := \{00, â\r1, â\r2, \ldots, â\r r, lr\}$, and for
each $abâC$ with $abâlr$, test if either $(a+1)b$ or $a(b+1)$ are in
$D$; if none of them are, add $(a+1)b$, which is northwest of $ab$.
When there is nothing else to add, then $D$ is the whole of the right
wall of $H$.

In the acyclic example of the last section this yields:
%
$$\begin{array}{rcl} C &=& \{00, â\l1, â\l2, â\l3, â\l4, lr\} \\ &=& \{00, 10, 20, 32, 42, 45\} \\ &\squigto& \{00, 10, 20, 21, 22, 32, 42, 43, 44, 45\}, \\ D &=& \{00, â\r1, â\r2, â\r3, â\r4, â\r5, lr\} \\ &=& \{00, 01, 02, 03, 14, 25, 45\} \\ &\squigto& \{00, 01, 02, 03, 13, 14, 24, 25, 35, 45\}. \\ \end{array}$$
%
and the ZHA is everything between the left wall'' $C$ and the
right wall'' $D$.

\msk

{\sl From ZHAs to 2CAGs.} Let $H$ be a ZHA and let $lr$ be its top
point. Form the sequence of its left wall generators (the generators
of $H$ in which the arrow pointing to them points northwest) and the
sequence of its right wall generators (the generators of $H$ in which
the arrow pointing to them points northeast). Look at where there are
gaps'' in these sequences; each gap in the left wall generators
becomes an intercolumn arrow going right, and each gap in the right
wall generators becomes an intercolun arrow going left. In the acyclic
example of the last section, this yields:
%
$$\def\gap#1{\!\!\!\!\!\text{(gap, arrow #1)}} \def\gap#1{\!\!\!\!\!\text{(gap becomes #1)}} \def\nogap{\!\!\!\!\!\text{(no gap)}} % \begin{array}{lllllll} & && \r5 = 25 & \\ & && & \gap{\lotr25} \\ \l4 = 42 & && \r4 = 14 & \\ &\nogap && & \gap{\lotr14} \\ \l3 = 32 & && \r3 = 03 & \\ &\gap{\ltor32} && & \nogap \\ \l2 = 20 & && \r2 = 02 & \\ &\nogap && & \nogap \\ \l1 = 10 & && \r1 = 01 & \\ \end{array}$$
%
We know $l$ and $r$ from the top point of the ZHA, and from the gaps
we get $R$ and $L$; the 2CAG that generates this ZHA is:
%
$$(4,5,\cmat{\ltor32},\cmat{\lotr25, \\ \lotr14}).$$

% (phap 15)
% (find-planarhas        "2-column-graphs")
% (find-planarhaspage 10 "2-Column graphs")
% (find-planarhastext 10 "2-Column graphs")

\newpage

%  ____  _
% |  _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% |  __/| | (_| (__\__ \
% |_|   |_|\___\___|___/
%
% Â«piccs-and-slashingsÂ» (to ".piccs-and-slashings")
\section{Piccs and slashings}
\label  {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}

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,cd] := [\ang{a,b},\ang{c,d}] := \setofst {\ang{l,r}â\LR} {aâlâc \& bârâd},$$
%
Note that it can be adapted to define intervals'' in a ZHAs $H$:
%
$$\begin{array}{rcl} [ab,cd]âH & := & \setofst {\ang{l,r}â\LR} {aâlâc \& bârâd}âH \\ & = & \setofst {\ang{l,r}âH} {aâlâc \& bârâd}. \\ \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\bsl45\bsl6)$
is a slashing on $[00,46]$. We write the bars in $L$ as $/$'s and the
bars in $R$ as $\bsl$' as a reminder that they are to be interpreted
as northeast and northwest cuts'' respectively; $S=(4321/0,\, 0123\bsl45\bsl6)$ 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 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-regs}) 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}

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\bsl#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\bsl45\bsl6) \end{array}$$

%  ____  _           _
% / ___|| | __ _ ___| |__        _ __ ___   __ ___  __
% \___ \| |/ _ / __| '_ \ _____| '_  _ \ / _ \ \/ /
%  ___) | | (_| \__ \ | | |_____| | | | | | (_| |>  <
% |____/|_|\__,_|___/_| |_|     |_| |_| |_|\__,_/_/\_\
%
% Â«slash-maxÂ» (to ".slash-max")
\section{Slash-regions have maximal elements}
\label  {slash-max}
% (phap 27)

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

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}
% (phap 29)

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}
% (phap 30)

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

\newpage

%      _
%     | |       ___  _ __  ___
%  _  | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
%  \___/       \___/| .__/|___/
%                   |_|
%
% Â«J-ops-and-regionsÂ» (to ".J-ops-and-regions")
% J-regions and J-operators
\section{J-operators and J-regions}
\label  {J-ops-and-regs}

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{J-regs-and-slashings}. 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}.

%      _                   _
%     | |   __ _ _ __   __| |   ___ ___  _ __  _ __  ___
%  _  | |  / _ | '_ \ / _ |  / __/ _ \| '_ \| '_ \/ __|
% | |_| | | (_| | | | | (_| | | (_| (_) | | | | | | \__ \
%  \___/   \__,_|_| |_|\__,_|  \___\___/|_| |_|_| |_|___/
%
% Â«J-ops-and-connectivesÂ» (to ".J-ops-and-connectives")
\section{How J-operators interact with connectives}
\label  {J-ops-and-connectives}

% (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")

%      _                                        _       _           _
%     | |  _ __ ___  __ _ ___    __ _ _ __   __| |  ___| | __ _ ___| |__  ___
%  _  | | | '__/ _ \/ _ / __|  / _ | '_ \ / _ | / __| |/ _ / __| '_ \/ __|
% | |_| | | | |  __/ (_| \__ \ | (_| | | | | (_| | \__ \ | (_| \__ \ | | \__ \
%  \___/  |_|  \___|\__, |___/  \__,_|_| |_|\__,_| |___/_|\__,_|___/_| |_|___/
%                   |___/
%
% Â«J-regs-and-slashingsÂ» (to ".J-regs-and-slashings")
\section{J-regions come from slashings}
\label  {J-regs-and-slashings}

% (find-LATEX "2015planar-has.tex" "there-are-no-YL-cuts")
% (find-planarhaspage 20 "There are no Y-cuts")
% (find-planarhastext 20 "There are no Y-cuts")

\newpage

%   ____ _     _ _     _
%  / ___| |__ (_) | __| |_ __ ___ _ __
% | |   | '_ \| | |/ _ | '__/ _ \ '_ \
% | |___| | | | | | (_| | | |  __/ | | |
%  \____|_| |_|_|_|\__,_|_|  \___|_| |_|
%
% Â«childrenÂ» (to ".children")
\section{Appendix: on children''}
\label{children}

% (find-LATEXfile "" "istanbul1.tex")
% (find-LATEXfile "istanbul1.org")
% (find-LATEXfile "istanbul1.org" "Why study CT")
% (find-xpdfpage "~/LATEX/istanbul1.pdf")
% (find-xpdfpage "~/LATEX/istanbul1.pdf" 3)

...from the slides of my minicourse in the UniLog 2016 (Istanbul):

\begin{itemize}
\item Why study Category Theory {\sl now}?

Public education in Brazil is being dismantled --- maybe we should
be doing better things than studying very technical \& inaccessible
subjects with no research grants ---

{\sl (Here I showed a photo called The New Girl From Ipanema'' ---
a girl walking on the Ipanema beach at night with a gas mask, with
a huge cloud of tear gas behind her)}

\item Category theory should be more accessible

Most texts about CT are for specialists in research universities...
{\sl Category theory should be more accessible.}.

To whom?...

\begin{itemize}
\item Non-specialists (in research universities)
\item Grad students (in research universities)
\item Non-specialists (in conferences - where we have to be quick)
\item Undergrads (e.g., in CompSci - in teaching colleges) - (Children'')
\end{itemize}

\item What do we mean by "accessible"?

\begin{itemize}
\item Done on very firm grounds: mathematical objects made from
numbers, sets and tuples; FINITE, SMALL mathematical objects
whenever possible. Avoid references to non-mathematical things like
windows, cars and pizzas (like the object-orientation people do);
avoid reference to Physics; avoid Quantum Mecanics at all costs;
time is difficult to draw, prefer {\sl static} rather than {\sl
changing}

\item People have very short attention spans nowadays

\item Self-contained, but not {\sl isolated} or {\sl isolating}; our
material should make the literature more accessible

\item We learn better by doing. Our material should have lots of space
for exercises.

\item Most people with whom I interact are not from Maths/CS/etc

\item {\sl Proving} general cases is relatively hard. {\sl Checking}
and {\sl calculating} is much easier. People can believe that
something can be generalized after seeing a convincing particular
case. (Sometimes leave them to look for the right generalization by
themselves)
\end{itemize}
\end{itemize}

% \msk

% Most books on advanced mathematics mention, in their introductions,
% how much mathematical maturity'' a reader needs to have in order
% to understand their contents... the term mathematical maturity''
% means, among other things, the ability to {\sl work on very abstract
% settings}, to {\sl generalize}, to {\sl particularize}, and to {\sl
% use infinite objects}, besides familiarity with the notation,
% methods, and main concepts in mathematics. A nice term for people
% with very little mathematical maturity is children''.

% I've tried to write this paper in a way as to makes it as accessible
% as possible to children'' like humanities students, philosophers
% with little mathematical background, and freshmen Computer Science
% students. Most of the sections were written after I presented the
% material corresponding to them in a {\sl very} basic introductory
% course on lambda-calculus and logic that I gave in the second half
% of 2016, whose audience was a group of six CompSci students; the
% exercises that they solved in class are not included here.

% I've had a handful of opportunities to present parts of this
% exercises on expressions, quantifiers, evaluation, functions, sets,
% and lambda-notation, that are not included here.

I've been using for children'' in titles for a while. This is a bit
of a marketing strategy, of course, but the term children'' here has
a precise, though unusual, meaning: it means people with very little
mathematical maturity'', where I am taking these as the main aspects
of mathematical maturity'': the ability to {\sl work on very
abstract settings}, to {\sl generalize}, to {\sl particularize}, and
to {\sl use infinite objects}.

Writing things for children'' in this sense results in material that
[is accessible] [exercises, not included here] [visual, easy to check]
[who I've tested this with]

\msk

{\sl A note for adults''.} In [Ochs2013] I sketched a method for
working in a general case and in a particular case (an archetypal
case'') in parallel, and also a way to prove things in the archetypal
case and then lift'' the proofs to the general case. This paper is
an offspring of that one; I believe that planar Heyting Algebras
presented here (ZHAs, sec.\ref{ZHAs}) are archetypal Heyting Algebras,
and when we add closure operators'' to ZHAs (as in the seminar notes
\url{http://angg.twu.net/math-b.html\#zhas-for-children}, pp.13--30;
they are called J-operators'' there) we get something that is
archetypal for studying toposes and sheaves; that will be the subject
of a sequel of this paper.

[Topos theory books are too hard for me] [a bridge between
philosophers and toposophers]

% besides familiarity with the notation, methods, and main concepts in
% mathematics.

%   ____                               _                    _
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __
% | |   / _ \| '_  _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | |
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
%                      |_|
%
% Â«comprehensionÂ» (to ".comprehension")
\section{Appendix: notations for set comprehension}

% (find-angg "LATEX/2016-2-LA-zhas.tex")
% (lazp 1)

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}} \def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}} \def\ue#1{\und{#1}{expr}}
\def\uv#1{\und{#1}{var}}

\def\tbl#1#2{\fbox{$\begin{array}{#1}#2\end{array}$}}
\def\tbl#1#2{\fbox{$\sm{#2}$}}
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
% "Stop":
\def\S{\omit\vrule\phantom{$\scriptstyle($}\hss}   % stop
% strut:
\def\s{\mathstrut}
\def\s{\phantom{$|$}}
\def\s{\phantom{|}}
\def\s{}

This is section is just to clarify the exact meaning of the
$\setofst{\ldots}{\ldots}$-expressions'' in the previous sections.

% The definition of $\LR$ in the previous sections deserves more
% explanations.

We'll use three notations for set comprehensions: a low-level'' one,
with generators and filters separated by commas, then a semicolon and
then the result expression, and two higher-level notations using a
$|$', that are closer to the standard ones.

Here are some examples of the low-level notation,
%
$$\begin{array}{lll} \{\ug{aâ\{1,2,3,4\}}; \ue{10a}\} &=& \{10,20,30,40\} \\ \{\ug{aâ\{1,2,3,4\}}; \ue{a}\} &=& \{1,2,3,4\} \\ \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{a}\} &=& \{3,4\} \\ \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{10a}\} &=& \{30,40\} \\ \{\ug{aâ\{10,20\}}, \ug{bâ\{3,4\}}; \ue{a+b}\} &=& \{13,14,23,24\} \\ \{\ug{aâ\{1,2\}}, \ug{bâ\{3,4\}}; \ue{(a,b)}\} &=& \{(1,3),(1,4),(2,3),(2,4)\} \\ \end{array}$$

Here is how to calculate the results of some low-level comprehensions
using tables; note that when a filter yields false'' we stop ---
this is indicated by a vertical bar --- and we don't calculate the
rest of the line. The result of the comprehension is the set of the
results in the lines where all filters yielded true''.
%
$$\begin{array}{l} \{\ug{xâ\{1,2,3\}}, \ug{yâ\{3,4\}}, \uf{x+y<6}; \ue{(x,y)}\} = \{(1,3),(1,4),(2,3)\} \\ \tbl{ccc}{ \s x & y & x+y<6 & (x,y) \\\hline \s 1 & 3 & \V & (1,3) \\ \s 1 & 4 & \V & (1,4) \\ \s 2 & 3 & \V & (2,3) \\ \s 2 & 4 & \F & \S \\ \s 3 & 3 & \F & \S \\ \s 3 & 4 & \F & \S \\ } \end{array}$$

$$\begin{array}{l} \{\ug{(x,y)â\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\} = \{(2,1), (3,1), (3,2)\} \\ \tbl{ccc}{ \s (x,y) & x & y & x>y & (x,y) \\\hline \s (1,1) & 1 & 1 & \F & \S \\ \s (1,2) & 1 & 2 & \F & \S \\ \s (1,3) & 1 & 3 & \F & \S \\ \s (2,1) & 2 & 1 & \V & (2,1) \\ \s (2,2) & 2 & 2 & \F & \S \\ \s (2,3) & 2 & 3 & \F & \S \\ \s (3,1) & 3 & 1 & \V & (3,1) \\ \s (3,2) & 3 & 2 & \V & (3,2) \\ \s (3,3) & 3 & 3 & \F & \S \\ } \end{array}$$

\bsk

Here are some examples of the higher-level, standard-ish notations for
set comprehensions, and how they can be translated into the low-level notation:
%
$$\begin{array}{llll} & \text{(standard)} & & \text{(low-level)} \\[5pt] % & \setofst{\ue{10a}}{\ug{aâ\{1,2,3,4\}}} &=& \{\ug{aâ\{1,2,3,4\}}; \ue{10a}\} \\ & \setofst{\ue{a}}{\ug{aâ\{1,2,3,4\}}} &=& \{\ug{aâ\{1,2,3,4\}}; \ue{a}\} \\ & \setofst{\ue{10a}}{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}} &=& \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{10a}\} \\ & \setofst{\ue{a}}{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}} &=& \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{a}\} \\ & \setofst{\ug{aâ\{1,2,3,4\}}}{\uf{aâ3}} &=& \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{a}\} \\ % & \{\ug{aâ\{10,20\}}, \ug{bâ\{3,4\}}; \ue{a+b}\} \\ % & \{\ug{aâ\{1,2\}}, \ug{bâ\{3,4\}}; \ue{(a,b)}\} \\ \end{array}$$

The first four are of the form
$\setofst{\text{expr}}{\text{generators and filters}}$''
(e$|$gf''), and the last one is of the form
$\setofst{\text{generator}}{\text{filters}}$'' (g$|$f''). In
g$|$f'' comprehensions the final expr' is the variable of the
generator:
%
% (find-angg "LATEX/2016-2-LA-zhas.tex" "comprehension-2")
% (lazp 2)
%
$$\begin{array}{llll} % & \text{(standard)} & & \text{(explicit)} \\[5pt] & \setofst{\ug{\uv{a}â\{1,2,3,4\}}}{\uf{aâ3}} &=& \{\ug{aâ\{1,2,3,4\}}, \uf{aâ3}; \ue{a}\} \\ % & \setofst {\ug{\uv{(x,y)}â\{1,2,3\}^2}} {\uf{x>y}} &=& % \{\ug{(x,y)â\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\} \\ \end{array}$$

\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "Â«%sÂ»"
% End:

`