|
Warning: this is an htmlized version!
The original is here, 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"))
% (defun u () (interactive) (find-latex-upload-links "2016planar-has"))
% (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[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb} % (find-es "tex" "colorweb")
\usepackage{tikz}
\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 edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.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 K:tomp({def="Kmini", scale="4pt", meta="s"}):addbullets() :output()
%R K:tomp({def="Kb", scale="8pt", meta=nil}):addbullets() :output()
%R K:tomp({def="KB", scale="20pt", meta=nil}):addbullets():addarrows(nil):output()
%R K:tomp({def="Kn", scale="20pt", meta=nil}):addxys ():addarrows(nil):output()
%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="↗"}
%R B:tozmp({def="Bmne", scale="9pt", meta=nil}):addcells(T):output()
%R W:tozmp({def="Wmne", scale="9pt", meta=nil}):addcells(T):output()
$$\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)
% (find-dn6file "zhas.lua" "addxys =")
%
%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 mp = zhav:tozmp({def="zhav", scale="20pt", meta=nil}):addxys():addarrows("w")
%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
when we start with a ZHA, erase the axes, and then add the axes back
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 mpB:addbullets():output()
%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")
%L mpB:addbullets():output()
%L mp :addlrs() :output()
$$
\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()
% %R zhav:tozmp({def="za", 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 znotnotP:tozmp({def="znotnotP", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%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 zdemorgan:tozmp({def="zdemorgan", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse", scale="10pt", meta=nil}):addlrs():output()
%
%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 house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R house:tomp({def="zdagHouse", scale="15pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse", scale="12pt", meta="s"}):addlrs():addarrows("w"):output()
%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 guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R guill:tomp({def="zdagGuill", scale="7pt", meta="t"}):addbullets():addarrows():output()
%R guill:tomp({def="zdagGuill", scale="13pt", meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill", scale="12pt", meta="s"}):addlrs():addarrows():output()
%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 /
%R w:tomp({def="zfW#1#2#3#4#5", scale="3.5pt", meta="s"}):addcells():output()
%R w:tomp({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW", scale="13pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({def="zdagOW", scale="25pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%
$$
\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()
%L MixedPicture.new({def="bar", scale="10pt", meta=nil}, z):addlrs():output()
$$
\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()
%L MixedPicture.new({def="bar", scale="10pt", meta=nil}, z):addlrs():output()
%L MixedPicture.new({def="poo", scale="10pt", meta=nil}, z):addgens():output()
$$
\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 /
%R top:tomp({def="bar", scale="10pt"}):addcells():output()
%
$$\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 = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
% / \
% 46
% / \ \
% 45 36
% \ \ \
% 35 26
% / \ /
% 34 25
% \ /
% 24
% / \ \
% 23 14
% / \ / \
% 22 13 04
% \ / \ /
% 12 03
% / / /
% 11 02
% \ / /
% 01
% / /
% 00
% 4321/0 \ / 0123\45\6
%
$$\pu
\foo
\qquad
\ZQuot
\qquad
\ZQuotients
$$
A slashing $S=(L,R)$ on a ZHA $H$ with top element $ab$ induces an
equivalence relation `$\eqS$' on $H$ that works like this: $\ang{c,d}
\eqS \ang{e,f}$ iff $c \eqL e$ and $d \eqR f$. We write
%
$$\begin{array}{rcl}
[c]_L &:=& \setofst {e∈\{0,\ldots,a\}} {c \eqL a} \\ \relax
[d]_R &:=& \setofst {f∈\{0,\ldots,b\}} {d \eqL f} \\ \relax
[cd]_S &:=& \setofst {ef∈H} {cd \eqS ef} \\
\end{array}
$$
%
for the equivalence classes, and note that
%
% (find-planarhas "zquotients")
% (find-planarhaspage 26 "ZQuotients")
% (find-planarhastext 26 "ZQuotients")
%
$$\begin{array}{lrcl}
\text{if} & [c]_L &=& \{c',\ldots,c''\} \\
\text{and} & [d]_L &=& \{d',\ldots,d''\} \\
\text{then} & [cd]_S &=& [c'd',c''d'']∩H; \\
\end{array}
$$
%
for example, in the ZHA at the right at the example above we have:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
[12]_S &=& [10,43]∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
We say that a slashing $S$ on a ZHA $H$ partitions $H$ into {\sl
slash-regions}; later (sec.\ref{J-ops-and-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()
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
H = \;\;\foo
\quad
\begin{array}[t]{r}
LW_H = \{00,01,11,12,22,23,24,34,35,45,46\} \\
RW_H = \{00,01,02,03,04,14,24,25,26,36,46\} \\
\end{array}
$$
To recover the picc $L$ --- which is a picc on $\{0,1,2,3,4\}$ --- we
need to find where we change from an $L$-equivalence class to another
when we go from one digit to the next; and to recover the picc $R$ ---
which is a picc on $\{0,1,2,3,4,5,6\}$ --- we need to find where we
change from an $R$-equivalence class to another when we go from one
digit to the next.
We can recover $L$ and $R$ by walking $LW_H$ (or $RW_H$) from bottom
to top in a series of white pawns moves, and checking when we change
from one $S$-equivalence class to another. Northwest moves give
information about $L$, and northeast moves give information about $R$.
Look at the example below, in which we walk on $RW_H$:
%
\def\nem#1#2{\psm{ &\!#2\\ #1& \\}}
\def\nwm#1#2{\psm{ #2& \\ &\!#1\\}}
\def\nem#1#2{\sm{ &&\!#2\\ &\!\nearrow&\\ #1& \\}}
\def\nwm#1#2{\sm{ #2&\\&\!\nwarrow&\\ &&\!#1\\}}
\def\neyes#1#2#3#4{\nem{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #2 { \eqR} #4 \;⇒\; #2 #4 }
\def\neno #1#2#3#4{\nem{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #2 {\not\eqR} #4 \;⇒\; #2\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 }
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="LWH"}, "1RLRLRRLRLR"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="RWH"}, "1RRRRLLRRLL"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
\begin{array}{c}
H = \;\;\foo
\qquad
LW_H = \;\;\LWH
\quad
RW_H = \!\!\!\!\!\!\!\!\RWH
%
\\ \\
%
\begin{array}{ll}
& \neno 25 26 \\
& \neyes 24 25 \\
\nwyes 36 46 & \neno 03 04 \\
\nwyes 26 36 & \neyes 02 03 \\
\nwyes 14 24 & \neyes 01 02 \\
\nwno 04 14 & \neyes 00 01 \\
\end{array}
%
\\ \\
%
% ⇒ \quad
(L,R) \;=\; (4321/0, 0123\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")
%L -- mp:addlrs():addcuts("c 01|23 10w-11n 32w-33n"):output()
%L mp:addlrs():addcuts("c 01|23 20w-21n 32w-33n"):output()
$$\pu
\foo
$$
Here is an easy way to prove formally that the partition above does
not come from a slashing $S=(L,R)$. We will adapt the idea from
sec.\ref{slash-partitions}, where we recovered $L$ and $R$ from
northwest and northeast steps.
%
\def\undtrue #1{\und{#1}{\text{true}}}
\def\undfalse#1{\und{#1}{\text{false}}}
\def\undfrown#1{\und{#1}{=(}}
\def\iff{\;\;↔\;\;}
\def\notiff{\;\not↔\;}
%
$$\begin{array}{rcl}
\undfalse{21 \eqP 31} \;\;↔\;\; \undfrown{2 \eqL 3} \;\;↔\;\; \undtrue {22 \eqP 32} \\
\undtrue {31 \eqP 41} \;\;↔\;\; \undfrown{3 \eqL 4} \;\;↔\;\; \undfalse{32 \eqP 42} \\
\end{array}
$$
The problem is that the figure above has ``cuts stopping midway''...
if its cuts all crossed the ZHA all the way through, we would have
this for $L$ and northeast cuts,
%
$$\begin{array}{c}
0\eqL1 \iff 00\eqP10 \iff 01\eqP11 \iff 02\eqP12 \iff 03\eqP13 \\
1\eqL2 \iff 10\eqP20 \iff 11\eqP21 \iff 12\eqP22 \iff 13\eqP23 \\
2\eqL3 \iff 20\eqP30 \iff 21\eqP31 \iff 22\eqP32 \iff 23\eqP33 \\
3\eqL4 \iff 30\eqP40 \iff 31\eqP41 \iff 32\eqP42 \iff 33\eqP43 \\
4\eqL5 \iff 40\eqP50 \iff 41\eqP51 \iff 42\eqP52 \iff 43\eqP53 \\
5\eqL6 \iff 50\eqP60 \iff 51\eqP61 \iff 52\eqP62 \iff 53\eqP63 \\
\end{array}
$$
%
and something similar for $R$ and northwest cuts.
\msk
Formally, a partition $P$ on $H$ has an ``L-cut between $c$ and $c^+$
stopping midway'' if $cd \eqP c^+d \notiff cd \eqP c^+d$ for some $d$,
and it has an ``R-cut between $d$ and $d^+$ stopping midway'' if $cd
\eqP cd^+ \notiff c^+d \eqP c^+d^+$ for some $c$; here we are writing
$x^+$ for $x+1$.
\msk
{\sl Theorem: a partition of $H$ into closed intervals is a
slash-partition if and only if it doesn't have any cuts stopping
midway.} Proof: use the ideas above to recover $L$ and $R$ from
$\eqP$, and then check that $S=(L,R)$ induces an equivalence relation
$\eqS$ that coincides with $\eqP$.
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
% «slash-ops» (to ".slash-ops")
\section{Slash-operators}
\label {slash-ops}
% (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"):addlrs():output()
%L mp = mpnew({def="andCube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3")
%L mp:put(v"30", "P"):put(v"31", "P'", "P'"):put(v"32", "P*", "P^S")
%L mp:put(v"03", "Q"):put(v"13", "Q'", "Q'"):put(v"23", "Q*", "Q^S")
%L mp:output()
%
$$\pu
\begin{array}{c}
\andcube
\qquad
\andCube
\\ \\
\und{( \und{ \und{P}{30} ∧ \und{Q}{03} }{00} )^S}{22} =
\und{( \und{ \und{\und{P }{30}{}^S}{32} ∧ \und{\und{Q }{03}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{\und{P'}{31}{}^S}{32} ∧ \und{\und{Q'}{13}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{P'}{31} ∧ \und{Q'}{13} }{11} )^S}{22}
\\
\end{array}
$$
%
Note that all subexpressions belong to three $S$-regions: a region
with $P$, $P'$, $P^S=P'{}^S$, another with $Q$, $Q'$, $Q^S=Q'{}^S$,
and one with all the `$∧$'s. If we had cuts stopping midway then some
of the `$∧$'s could be in different regions.
I think that the clearest way to show (1) is by putting its proof in
tree form:
%
%L addabbrevs("(~S)", "\\eqS ", "(~L)", "\\eqL ", "(~R)", "\\eqR ")
%:
%: cd(~S)c'd' ef(~S)e'f' cd(~S)c'd' ef(~S)e'f'
%: ---------- ---------- ---------- ----------
%: c(~L)c' e(~L)e' d(~R)d' f(~R)f'
%: ------------------------ ------------------------
%: \min(c,e)(~L)\min(c',e') \min(d,f)(~L)\min(d',f')
%: ----------------------------------------------------
%: \min(c,e)\min(d,f)(~S)\min(c',e')\min(d',f')
%: --------------------------------------------
%: cd∧ef(~S)c'd'∧e'f'
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
\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")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
\foo
$$
%
It is easy to see that `$·^*$' obeys $\J1$ and $\J2$; however, it does
{\sl not} obey $\J3$ --- we will prove that in
sec.\ref{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)
% https://mail.google.com/mail/ca/u/0/#search/arndt/153e28089870b2ba
...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 Undergrads (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
% material to humanities students --- with them I had to start with
% 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: