|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017planar-has.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017planar-has.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2017planar-has; makeindex 2017planar-has"))
% (defun e () (interactive) (find-LATEX "2017planar-has.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017planar-has"))
% (find-xpdfpage "~/LATEX/2017planar-has.pdf")
% (find-sh0 "cp -v ~/LATEX/2017planar-has.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017planar-has.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017planar-has.pdf
% file:///tmp/2017planar-has.pdf
% file:///tmp/pen/2017planar-has.pdf
% http://angg.twu.net/LATEX/2017planar-has.pdf
% An improvised index with links to pages:
% (find-LATEXsh "grep phap 2017planar-has.tex")
% (phai)
% (defun geta (str) (string-match "«\\(.*\\)»" str) (match-string 1 str))
% (defun getb () (geta (ee-no-properties (buffer-substring (ee-bol) (ee-eol)))))
% (defun getc () (format "\n%% (phap 0 \"%s\")" (getb)))
% (defun getd () (interactive) (insert (getc)))
% (setq last-kbd-macro (kbd "C-e <<getd>>"))
% (find-LATEXfile "2017ebl-slides.tex" "defun geta ")
% «.picturedots» (to "picturedots")
% «.title» (to "title")
% «.introduction» (to "introduction")
%
% «.positional» (to "positional")
% «.ZDAGs» (to "ZDAGs")
% «.LR-coords» (to "LR-coords")
% «.ZHAs» (to "ZHAs")
% «.two-conventions» (to "two-conventions")
% «.prop-calc» (to "prop-calc")
% «.prop-calc-ZHA» (to "prop-calc-ZHA")
% «.HAs» (to "HAs")
% «.implication-new» (to "implication-new")
% «.implication-formally» (to "implication-formally")
% «.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")
% «.no-Y-cuts-no-L-cuts» (to "no-Y-cuts-no-L-cuts")
% «.J-ops-and-connectives» (to "J-ops-and-connectives")
% «.J-cubes-as-partial-orders» (to "J-cubes-as-partial-orders")
% «.valuations-induce-POs» (to "valuations-induce-POs")
% «.comparing-partial-orders» (to "comparing-partial-orders")
% «.lindenbaum-fragments» (to "lindenbaum-fragments")
% «.polynomial-J-ops» (to "polynomial-J-ops")
% «.algebra-of-piccs» (to "algebra-of-piccs")
% «.algebra-of-J-ops» (to "algebra-of-J-ops")
% «.slashings-are-poly» (to "slashings-are-poly")
%
% «.question-marks» (to "question-marks")
% «.propagation» (to "propagation")
% «.relevant-points» (to "relevant-points")
% «.rectangular-versions» (to "rectangular-versions")
% «.extremities» (to "extremities")
% «.J-and-coJ-in-three-steps» (to "J-and-coJ-in-three-steps")
% «.sub-2CGs» (to "sub-2CGs")
% «.J-ops-as-adjunctions» (to "J-ops-as-adjunctions")
%
% «.bibliography» (to "bibliography")
%
% «.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")
\input diagxy % (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\calI{\mathcal{I}}
\def\calK{\mathcal{K}}
\def\calV{\mathcal{V}}
\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\Int{{\operatorname{\mathsf{int}}}}
\def\coInt{{\operatorname{\mathsf{coint}}}}
%\def\Opens{{\mathcal{O}}}
%
\def\NoLcuts{\mathsf{No}λ\mathsf{cuts}}
\def\NoYcuts{\mathsf{NoYcuts}}
\def\astarcube{{\&}^*\mathsf{Cube}}
\def\ostarcube{{∨}^*\mathsf{Cube}}
\def\istarcube{{→}^*\mathsf{Cube}}
\def\acz{{\&}^*\mathsf{C}_0}
\def\ocz{{∨}^*\mathsf{C}_0}
\def\icz{{→}^*\mathsf{C}_0}
%
\def\astarcuben{{\&}^*\mathsf{Cube}_\mathsf{n}}
\def\ostarcuben{{∨}^*\mathsf{Cube}_\mathsf{n}}
\def\istarcuben{{→}^*\mathsf{Cube}_\mathsf{n}}
\def\astarcubev{{\&}^*\mathsf{Cube}_\mathsf{v}}
\def\ostarcubev{{∨}^*\mathsf{Cube}_\mathsf{v}}
\def\istarcubev{{→}^*\mathsf{Cube}_\mathsf{v}}
%
%\catcode`∧=13 \def∧{\mathop{\&}}
\def\biggest {\mathsf{biggest}}
\def\smallest{\mathsf{smallest}}
\def\Cuts {\mathsf{Cuts}}
\def\myresizebox#1{%
\noindent\hbox to \textwidth{\hss
\resizebox{1.0\textwidth}{!}{#1}%
\hss}
}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
\title{Planar Heyting Algebras for Children}
\author{Eduardo Ochs}
\begin{abstract}
This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} using finite Planar Heyting Algebras (``ZHAs''),
that are certain subsets of $\Z^2$. The ``for children'' of the title
means ``for people without mathematical maturity'', i.e., for people
who are not able to understand structures that are too abstract
straight away, they need particular cases first; everything in the
paper is constructive and easy to visualize using finite diagrams.
We also show the connection between ZHAs and the familiar semantics
for IPL where the truth-values are open sets in a finite topological
space $(P,\Opens(P))$, and we show how each closure operator $J:H→H$
on a ZHA $H⊆\Z^2$ corresponds to a) a way to ``slash'' $H$ using
diagonal cuts, and b) a choice of a subset $S⊆P$; $J$ can be recovered
from $S$ as a restriction map $\Opens(P)→\Opens(S)$ followed by a map
$\Opens(S)→\Opens(P)$ that reconstructs the missing information ``in
the biggest way possible''.
\end{abstract}
\maketitle
% ___ _ _ _ _
% |_ _|_ __ | |_ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | || (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__\___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (phap 1 "introduction")
This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} (sec.\ref{prop-calc-ZHA}) using finite Planar
Heyting Algebras (``ZHAs'', sec.\ref{ZHAs}), that are certain subsets
of $\Z^2$. The ``for children'' of the title means ``for people
without mathematical maturity'' (sec.\ref{children}).
In sections \ref{topologies}--\ref{converting-ZHAs-2CAGs} we show the
connection between ZHAs and the familiar semantics for IPL where the
truth-values are open sets in a topological space $(P,\Opens(P))$, and
in sections \ref{piccs-and-slashings}--\ref{slashings-are-poly} we
discuss how each closure operator on a ZHA $H⊆\Z^2$ corresponds to a
way to ``slash'' $H$ using diagonal cuts; in sections
\ref{question-marks}--\ref{J-ops-as-adjunctions} we show how each
closure operator correspond to a subset $S⊆P$, or rather to a
restriction map $\Opens(P)→\Opens(S)$ followed by a map
$\Opens(S)→\Opens(P)$ that reconstructs the missing information ``in
the biggest way possible''.
% The ``for children'' in the title has a precise, but somewhat
% unusual, meaning, that is explained in sec.\ref{children}.
% \bsk
% ____ _ _ _ _
% / ___| |__ (_) | __| |_ __ ___ _ __
% | | | '_ \| | |/ _` | '__/ _ \ '_ \
% | |___| | | | | | (_| | | | __/ | | |
% \____|_| |_|_|_|\__,_|_| \___|_| |_|
%
% (phap 2 "children")
\section{Children}
\label {children}
The ``children'' in the title of this paper means: ``people without
mathematical maturity''. ``Children'' in this sense are not able to
understand structures that are too abstract straight away, they need
particular cases first; and they also don't deal well with infinite
objects or with expressions like ``for every proposition $P(x)$'', or
even with {\sl theorems}...
{
In my experience what works best with ``children'' is to teach them
first that ``basic mathematical objects'' are things built from
numbers, sets, and lists --- like this (our first logic!):
%
\def\p#1{\phantom{#1}}
\def\CL{\mathsf{CL}}
\def\fo #1 #2 #3 {((#1,#2),#3)}
\def\ba #1 #2 #3 #4 {
\foo 0 0 #1 , \\
\foo 0 1 #2 , \\
\foo 1 0 #3 , \\
\foo 1 1 #4 \p, \\
}
\def\foc#1 #2 {(#1,#2)}
\def\co #1 #2 {
\fooc 0 #1 ,\\
\fooc 1 #2 \p,\\
}
\def\com {0,\\ 1\p,\\}
\def\cand{\ba 0 0 0 1 }
\def\cor {\ba 0 1 1 1 }
\def\cimp{\ba 1 1 0 1 }
\def\ciff{\ba 1 0 0 1 }
\def\cnot{\co 1 0 }
%
\def\foo#1 #2 #3 {((#1,#2),#3)}
\def\fooc #1 #2 {(#1,#2)}
%
$$\begin{array}{l}
\CL = (Ω, ⊤, ⊥, ∧, ∨, →, ↔, ¬) = \\
\psm{\csm{\com}, 1, 0, \csm{\cand}, \csm{\cor}, \csm{\cimp}, \csm{\ciff}, \csm{\cnot}} \\
\end{array}\;,
$$
%
and then teach them how to calculate with functions, set
comprehension, quantification and $λ$-nota\-tion when the domains are
all finite; only after they acquire some practice, speed and intuition
about {\sl calculations} we can state some theorems as {\sl
propositions} whose results can be calculated by brute force, and
then discuss why some of these propositions-theorems always yield
``true''.
}
\msk
Except for two last sections all the rest of this paper has been
written to be readable by ``children'' in the sense above, and huge
parts of it have been tested on ``real children'' of mainly two kinds:
a group of ``older children'', who are Computer Science students who
had already completed a course on Discrete Mathematics, and some
``little children'', who are friends of mine who are students of
Psychology or Social Sciences. The text has benefited enormously from
they feedback --- especially their puzzled looks at some points, that
made me modify my presentation and the exercises I was giving to them.
Those exercises are not included here, though, and neither the
rationale behind most style decisions.
% \end{document}
% ____ _ _ _ _
% | _ \ ___ ___(_) |_(_) ___ _ __ __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _` | |
% | __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_| \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% «positional» (to ".positional")
\section{Positional notations}
\label {positional}
% Good (phap 1 "positional")
% (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{topologies-on-ZSets}).
% _________ _ ____
% |__ / _ \ / \ / ___|___
% / /| | | |/ _ \| | _/ __|
% / /_| |_| / ___ \ |_| \__ \
% /____|____/_/ \_\____|___/
%
% «ZDAGs» (to ".ZDAGs")
\section{ZDAGs}
\label {ZDAGs}
% Good (phap 2 "ZDAGs")
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}
% Good (phap 3 "LR-coords")
\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}
% Good (phap 4 "ZHAs")
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.
% _____ _ _
% |_ _|_ _____ ___ ___ _ ____ _____ _ __ | |_(_) ___ _ __ ___
% | | \ \ /\ / / _ \ / __/ _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | | \ V V / (_) | | (_| (_) | | | \ V / __/ | | | |_| | (_) | | | \__ \
% |_| \_/\_/ \___/ \___\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «two-conventions» (to ".two-conventions")
\section{Conventions on diagrams without axes}
\label {two-conventions}
% Good (phap 5 "two-conventions")
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
$$
%
The new, restored axes are in a different position --- the bottom
point of the original ZHA at the left was $(0,0)$, but in the ZSet at
the right the bottom point is $(2,0)$.
{\sl The convention from sec.\ref{positional} is not adequate for ZHAs.}
Let's modify it!
{\sl From this point on,} the convention on where to
draw the axes will be this one: {\sl when it is clear from the context
that a bullet diagram represents a ZHA,} then its (unique) bottom
point has coordinate $(0,0)$, and we use that to draw the axes;
otherwise we apply the old convention, that chooses $(0,0)$ as the
point that makes the diagram fit in $\N^2$ and touch both axes.
The new convention with two cases also applies to functions from ZHAs,
and to 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}
$$
\bsk
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}
% Good (phap 5 "prop-calc")
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}
% Good (phap 6 "prop-calc-ZHA")
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}(\cd) \\
\o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\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")
% Good (phap 7 "HAs")
\section{Heyting Algebras}
\label{HAs}
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 Q) ≤_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}
)
$$
% __
% \ \ _ __ _____ __
% _____\ \ | '_ \ / _ \ \ /\ / /
% |_____/ / | | | | __/\ V V /
% /_( ) |_| |_|\___| \_/\_/
% |/
%
% «implication-new» (to ".implication-new")
% Ongoing (phap 10 "implication-new")
\section{The two implications are equivalent}
{
\def\toC {\ton{\text{C}}}
\def\toHA{\ton{\text{HA}}}
\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}
\def\ef{\a ef}
\def\ab{ab}
\def\cd{cd}
\def\ef{ef}
\def\wh{\widehat}
In sec.\ref{prop-calc-ZHA} we gave a definition of `$→$' that is easy
to calculate, and in sec.\ref{HAs} we saw a way to find by brute
force\footnote{``When in doubt use brute force'' --- Ken Thompson} a
value for $Q→R$ that obeys
%
$$(P≤(Q→R))↔(P≤Q∧R)$$
%
for all $P$. In this section we will see that these two operations ---
called `$\toC$' and `$\toHA$' from here on --- always give the same
results. We will do that by checking that for any ZHA $H$ and $Q,R∈H$
this holds
%
$$(P≤(Q \toC R))↔(P≤Q∧R)$$
%
for all $P∈H$.
\msk
In `$\toC$' the order of the cases is very important. For example, if
$cd=21$ and $ef=23$ then both ``$\cd \o{below} \ef$'' and ``$\cd
\o{leftof} \ef$'' are true, but ``$\cd \o{below} \ef$'' takes
precedence and so $\cd \toC \ef = ⊤$. We can fix this by creating
variants of $\o{below}$, $\o{leftof}$, $\o{righof}$ and $\o{above}$
that make the four cases disjoint. Abbreviating $\o{below}$,
$\o{leftof}$, $\o{righof}$ and $\o{above}$ as $\o{b}$, $\o{l}$,
$\o{r}$ and $\o{a}$, we have:
%
$$\def\foo#1#2#3{\cd\,\o{#1}\,\ef\;:=\; c#2e ∧ d#3f}
\begin{array}{rrr}
\foo{b}≤≤ && \foo{b'}≤≤ \\
\foo{l}≤≥ && \foo{l'}≤> \\
\foo{r}≥≤ && \foo{r'}>≤ \\
\foo{a}>> && \foo{a'}>> \\
\end{array}
$$
%
visually the regions are these, for $R$ fixed:
%
%L mp = mpnew({def="blraprime", scale="7pt", meta="s"}, "12345654321"):addcuts("c 543/210 012|345")
%L mp:put(v"22", "R")
%L mp:put(v"44", "Q\\o{a}'R")
%L mp:put(v"11", "Q\\o{b}'R")
%L mp:put(v"41", "Q\\o{l}'R")
%L mp:put(v"14", "Q\\o{r}'R")
%L mp:output()
%
$$\pu
\blraprime
$$
We clearly have:
%
$$Q \toC R
%
\;=\;
%
\left(
\!
\begin{array}{lccl}
\o{if} & Q\o{b}R & \o{then} & ⊤ \\
\o{elseif} & Q\o{l}R & \o{then} & \o{ne}(R) \\
\o{elseif} & Q\o{r}R & \o{then} & \o{nw}(R) \\
\o{elseif} & Q\o{a}R & \o{then} & R \\
\o{end}
\end{array}
\!\!\!
\right)
%
\;=\;
%
\left(
\!
\begin{array}{lccl}
\o{if} & Q\o{b'}R & \o{then} & ⊤ \\
\o{elseif} & Q\o{l'}R & \o{then} & \o{ne}(R) \\
\o{elseif} & Q\o{r'}R & \o{then} & \o{nw}(R) \\
\o{elseif} & Q\o{a'}R & \o{then} & R \\
\o{end}
\end{array}
\!\!\!
\right)
$$
%
and $P ≤ Q \toC R$ can be expressed as a conjunction of the four
cases:
%
$$\def\foo#1{((P ≤ #1) ↔ (P∧Q≤R))}
\def\fooc {((P ≤ Q \toC R) ↔ (P∧Q≤R))}
\def\cond#1{Q\o{#1}R}
%
\begin{array}{l}
\fooc \\[5pt]
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \fooc & ∧ \\
\cond{l'} → \fooc & ∧ \\
\cond{r'} → \fooc & ∧ \\
\cond{a'} → \fooc & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \foo{⊤} & ∧ \\
\cond{l'} → \foo{\o{ne}(R)} & ∧ \\
\cond{r'} → \foo{\o{nw}(R)} & ∧ \\
\cond{a'} → \foo{R} & \\
\end{array}
\right) \\
\end{array}
$$
Let's introduce a notation: a ``$\widehat{a}$'' means ``make this
digit as big possible without leaving the ZHA''. So,
%
%L mpnew({def="foo"}, "123RL232L1"):addlrs():output()
$$\pu
\text{in} \qquad \foo \qquad \text{we have} \qquad
\begin{array}{rclcl}
\wh1\wh2 &=& 54 &=& ⊤, \\
1\wh2 &=& 13 &=& \o{ne}(12), \\
\wh12 &=& 42 &=& \o{nw}(12); \\
\end{array}
% \quad ;
$$
\def\EF{\wh e \wh f}
\def\Ef{\wh e f}
\def\eF{ e \wh f}
\def\ef{ e f}
This lets us rewrite $⊤$ as $\wh e \wh f$, $\o{ne}(ef)$ as $e \wh f$,
and $\o{nw}(ef)$ as $\wh e f$.
Making $P=ab$, $Q=cd$, $R=ef$, we have:
$$\def\fooc {((ab ≤ cd \toC ef) ↔ (ab∧cd≤ef))}
\def\foo #1 {((ab ≤ #1) ↔ (ab∧cd≤ef))}
\def\foor#1#2{((ab ≤ #1) ↔ (ab∧cd≤#2))}
\def\fooR#1#2{((ab ≤ #1) ↔ #2)}
\def\cond#1 {cd\o{#1}ef}
\def\Cond#1#2{c#1e ∧ d#2f}
%
\begin{array}{l}
\fooc \\[5pt]
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \foo{\EF} & ∧ \\
\cond{l'} → \foo{\eF} & ∧ \\
\cond{r'} → \foo{\Ef} & ∧ \\
\cond{a'} → \foo{\ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond≤≤ → \foo{\EF} & ∧ \\
\Cond>≤ → \foo{\eF} & ∧ \\
\Cond≤> → \foo{\Ef} & ∧ \\
\Cond>> → \foo{\ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond≤≤ → \foor{\EF}{cd} & ∧ \\
\Cond>≤ → \foor{\eF}{ed} & ∧ \\
\Cond≤> → \foor{\Ef}{cf} & ∧ \\
\Cond>> → \foor{\ef}{ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond≤≤ → \fooR{\EF}{⊤} & ∧ \\
\Cond>≤ → \fooR{\eF}{a≤e} & ∧ \\
\Cond≤> → \fooR{\Ef}{b≤f} & ∧ \\
\Cond>> → \fooR{\ef}{(a≤e∧b≤f)} & \\
\end{array}
\right) \\
\end{array}
$$
In the last conjunction the four cases are trivial to check.
}
% __ __ _ _
% \ \ / _| ___ _ __ _ __ ___ __ _| | |_ _
% _____\ \ | |_ / _ \| '__| '_ ` _ \ / _` | | | | | |
% |_____/ / | _| (_) | | | | | | | | (_| | | | |_| |
% /_( ) |_| \___/|_| |_| |_| |_|\__,_|_|_|\__, |
% |/ |___/
%
% «implication-formally» (to ".implication-formally")
% Bad (phap 10 "implication-formally")
%\section{Implication, formally}
%\label {implication-formally}
% _ _ _ _ _ _
% | | ___ __ _(_) ___ (_)_ __ | | | | / \ ___
% | | / _ \ / _` | |/ __| | | '_ \ | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__ | | | | | | _ |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/ \_\___/
% |___/
%
% «logic-in-HAs» (to ".logic-in-HAs")
% Good (phap 12 "logic-in-HAs")
\section{Logic in a Heyting Algebra}
\label {logic-in-HAs}
In sec.\ref{HAs} 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")
% Bad (phap 14 "derived-rules")
\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")
% Deleted (phap 11 "where-do-ZHAs-come-from")
% \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}
% Good (phap 18 "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 (sec.\ref{2CGs}). This will be done here and
in the next few sections.
\msk
\noindent
A {\sl topology} on a set $X$ is a subset $\calU$ of $\Pts(X)$ that
contains the ``everything'' and the ``nothing'' and is closed by
binary unions and intersections and by arbitrary unions. Formally:
1) $\calU$ contains $X$ and $\void$,
2) if $P,Q∈\calU$ then $\calU$ contains $P∪Q$ and $P∩Q$,
3) if $\calV ⊂ \calU$ then $\calU$ contains $\bigcup \calV$.
A {\sl topological space} is a pair $(X,\calU)$ where $X$ is a set and
$\calU$ is a topology on $X$.
When $(X,\calU)$ is a topological space and $U∈\calU$ we say that $U$
is {\sl open} in $(X,\calU)$.
\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 $\calU = \left\{\dagX10000, \, \dagX01000, \, \dagX00100, \,
\dagX00010, \, \dagX00001 \right\}$ then $\calU⊂\Pts(X)$ but $\calU$
fails all the conditions in 1, 2, 3 above:
1) $X=\dagX11111 \not∈ \calU$ and $\void=\dagX00000 \not∈ \calU$
2) Let $P=\dagX10000∈\calU$ and $Q=\dagX01000∈\calU$. Then
$P∩Q=\dagX00000 \not∈ \calU$ and $P∪Q=\dagX11000 \not∈ \calU$.
3) Let $\calV = \left\{\dagX01000, \, \dagX00100, \, \dagX00010
\right\} ⊂ \calU$. Then $\bigcup\calV = \dagX01000 ∪ \dagX00100 ∪
\dagX00010 = \dagX01110 \not∈ \calU$.
\msk
Now let $K=\dagKite•••••$ and $\calU = \left\{
\dagKite00000, \,
\dagKite00001, \,
\dagKite00011, \,
\dagKite00111, \,
\dagKite01011, \,
\dagKite01111, \,
\dagKite11111
\right\}$. In this case $(K,\calU)$ 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}
% Good (phap 19 "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)}
%$$
%
$$\label{O(D)}
\begin{array}{rcr}
\Opens(D) &:=& \{\, U⊂D \;|\; ∀((x,y),(x',y'))∈\BPM(D). \qquad\quad \\
&& (x,y)∈U → (x',y')∈U \,\} \\
\end{array}
$$
%
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}
% Good (phap 19 "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(G)$
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}
% Good (phap 21 "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(r) &:=& \{\_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}
% Good (phap 22 "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 between ZHAs and 2CAGs}
\label {converting-ZHAs-2CAGs}
% Good (phap 25 "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}).$$
% (find-planarhas "2-column-graphs")
% (find-planarhaspage 10 "2-Column graphs")
% (find-planarhastext 10 "2-Column graphs")
\msk
{\sl Theorem.} The two operations above are inverse to one another in
the following sense. If we start with a ZHA $H$, produce its 2CAG, and
produce a ZHA $H'$ from that, we get the same ZHA: $H'=H$. In the
other direction, if we start with a 2CAG $(P,A) = \TCG(l,r,R,L)$,
produce its ZHA, $H$, and then obtain a 2CAG $(P',A') =
\TCG(l',r',R',L')$ from $H$, we get back the original 2CAG {\sl if and
only if it didn't have any superfluous arrows}; if the original 2CAG
had superflous arrows then then new 2CAG will have $l'=l$, $r'=r$, and
$R'$ and $L'$ will be $R$ and $L$ minus these ``superfluous arrows'',
that are the ones that can be deleted without changing which 2-piles
are forbidden. For example:
%
%L tcg_spec = "4, 4; 44 43 32 22, "
%L tcgbig("fooa"):lrs():vs():hs():output()
%L tcg_spec = "4, 4; 44 22, "
%L tcgbig("foob"):lrs():vs():hs():output()
%L mpnew({def="foo", meta="10pt"}, "12RR3L21L"):addlrs():output()
%
$$\pu
% \fooa \quad\sa\quad \foo \quad\sa\quad \foob
\begin{array}{rcccl}
\fooa &\sa& \foo &\sa& \foob \\
% R =\cmat{\ltor44, \\ \ltor43, \\ \ltor32, \\ \ltor22} &&&&
% R'=\cmat{\ltor44, \\ \ltor22} \\
\end{array}
$$
%
In this case we have $R =\csm{\ltor44, \\ \ltor43, \\ \ltor32,
\\ \ltor22}$ and $R'=\csm{\ltor44, \\ \ltor22}$.
\newpage
% ____ _
% | _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% | __/| | (_| (__\__ \
% |_| |_|\___\___|___/
%
% «piccs-and-slashings» (to ".piccs-and-slashings")
\section{Piccs and slashings}
\label {piccs-and-slashings}
% Good (phap 28 "piccs-and-slashings")
\def\eqP{\underset{P}{\sim}}
\def\eqJ{\underset{J}{\sim}}
\def\eqP{\underset{\scriptscriptstyle P}{\sim}}
\def\eqJ{\underset{\scriptscriptstyle J}{\sim}}
\def\eqP{\sim_P}
\def\eqJ{\sim_J}
\def\eqL{\sim_L}
\def\eqR{\sim_R}
\def\eqS{\sim_S}
\def\eqF{\sim_F}
\def\eqQ{\sim_Q}
A picc (``partition into contiguous classes'') of an interval
$I=\{0,\ldots,n\}$ is a partition $P$ of $I$ that obeys this
condition (``picc-ness''):
%
$$∀a,b,c∈\{0,\ldots,n\}.\; (a<b<c \;\;\&\;\; a \eqP c) → (a \eqP b \eqP c).$$
%
So $P = \{\{0\},\{1,2,3\},\{4,5\}\}$ is a picc of $\{0,\ldots,5\}$,
and $P' = \{\{0\},\{1,2,4,5\},\{3\}\}$ is a partition of
$\{0,\ldots,5\}$ that is not a picc.
A short notation for piccs is this:
%
$$0|123|45 \equiv \{\{0\},\{1,2,3\},\{4,5\}\}$$
%
we list all digits in the ``interval'' in order, and we put bars to
indicate where we change from one equivalence class to another.
\msk
Let's define a notation for ``intervals'' in $\LR$,
%
$$[ab,ef]
:=
[\ang{a,b},\ang{e,f}]
:=
\setofst {\ang{c,d}∈\LR} {a≤c≤e \;\;\&\;\; b≤d≤f},
$$
%
Note that it can be adapted to define ``intervals'' in a ZHAs $H$:
%
$$\begin{array}{rcl}
[ab,ef]∩H & := & \setofst {\ang{c,d}∈\LR} {a≤c≤e \;\;\&\;\; b≤d≤f}∩H \\
& = & \setofst {\ang{c,d}∈H} {a≤c≤e \;\;\&\;\; b≤d≤f}. \\
\end{array}
$$
A {\sl slashing} $S$ on a ZHA $H$ with top element $ab$ is a pair of
piccs, $S=(L,R)$, where $L$ is a picc on $\{0,\ldots,a\}$ and $R$ is a
picc on $\{0,\ldots,b\}$; for example, $S=(4321/0,\, 0123∖45∖6)$
is a slashing on $[00,46]$. We write the bars in $L$ as `$/$'s and the
bars in $R$ as `$∖$' as a reminder that they are to be interpreted
as northeast and northwest ``cuts'' respectively; $S=(4321/0,\,
0123∖45∖6)$ is interpreted as the diagram at the left below, and
it ``slashes'' $[00,46]$ and the ZHA at the right below as:
%
%L -- local putl, putr, cutl, cutr
%L -- mp = MixedPicture.new {scale="7pt", def="foo"}
%L -- putl = function (n) mp:put(v((n+1).."0"), n.."", n.."") end
%L -- putr = function (n) mp:put(v("0"..(n+1)), n.."", n.."") end
%L -- cutl = function (n) mp:addcuts(format("%d0w-%d0n", n+1, n+1)) end
%L -- cutr = function (n) mp:addcuts(format("0%dn-0%de", n+1, n+1)) end
%L -- putl(0); putl(1); putl(2); putl(3); putl(4)
%L -- putr(0); putr(1); putr(2); putr(3); putr(4); putr(5); putr(6)
%L -- cutl(0)
%L -- cutr(3); cutr(5)
%L -- mp:print():output()
%L
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="foo"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
% / \
% 46
% / \ \
% 45 36
% \ \ \
% 35 26
% / \ /
% 34 25
% \ /
% 24
% / \ \
% 23 14
% / \ / \
% 22 13 04
% \ / \ /
% 12 03
% / / /
% 11 02
% \ / /
% 01
% / /
% 00
% 4321/0 \ / 0123\45\6
%
$$\pu
\foo
\qquad
\ZQuot
\qquad
\ZQuotients
$$
A slashing $S=(L,R)$ on a ZHA $H$ with top element $ab$ induces an
equivalence relation `$\eqS$' on $H$ that works like this: $\ang{c,d}
\eqS \ang{e,f}$ iff $c \eqL e$ and $d \eqR f$. We write
%
$$\begin{array}{rcl}
[c]_L &:=& \setofst {e∈\{0,\ldots,a\}} {c \eqL a} \\ \relax
[d]_R &:=& \setofst {f∈\{0,\ldots,b\}} {d \eqL f} \\ \relax
[cd]_S &:=& \setofst {ef∈H} {cd \eqS ef} \\
\end{array}
$$
%
for the equivalence classes, and note that
%
% (find-planarhas "zquotients")
% (find-planarhaspage 26 "ZQuotients")
% (find-planarhastext 26 "ZQuotients")
%
$$\begin{array}{lrcl}
\text{if} & [c]_L &=& \{c',\ldots,c''\} \\
\text{and} & [d]_L &=& \{d',\ldots,d''\} \\
\text{then} & [cd]_S &=& [c'd',c''d'']∩H; \\
\end{array}
$$
%
for example, in the ZHA at the right at the example above we have:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
[12]_S &=& [10,43]∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
We say that a slashing $S$ on a ZHA $H$ partitions $H$ into {\sl
slash-regions}; later (sec.\ref{J-ops-and-regions}) we will see that
a J-operator $J$ also partitions $H$, and we will refer to its
equivalence classes as {\sl J-regions}.
Slash-regions are intervals, but note that neither 10 or 43 belong to
the slash-region $[12]_S = [10,43]∩H$ above.
\msk
A {\sl slash-partition} is a partition on a ZHA induced by a slashing,
and a {\sl slash-equivalence} is an equivalence relation on a ZHA
induced by a slashing. Formally, a slash-partition on $H$ is a set of
subsets of $H$, and a slash-equivalence is subset of $H×H$, but it is
so easy to convert between partitions and equivalence relations that
we will often use both terms interchangeably. Our visual
representation for slash-partitions and slash-equivalences on a ZHA
$H$ will be the same: $H$ slashed by diagonal cuts.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ __ _ _ __| |_
% \___ \| |/ _` / __| '_ \ _____| '_ \ / _` | '__| __|
% ___) | | (_| \__ \ | | |_____| |_) | (_| | | | |_
% |____/|_|\__,_|___/_| |_| | .__/ \__,_|_| \__|
% |_|
% «slash-partitions» (to ".slash-partitions")
\section{From slash-partitions back to slashings}
\label {slash-partitions}
% Good (phap 29 "slash-partitions")
We saw how to go from a slashing $S=(L,R)$ on $H$ to an equivalence
relation $\eqS$ on $H$; let's see now how to recover $L$ and $R$ from
$\eqS$.
% Let's see a way to recover the piccs $L$ and $R$ from an equivalence
% relation $\eqS$ on a ZHA $H$.
Let $LW_H$ be the left wall of $H$, and $RW_H$ the right wall of $H$.
For example,
%
%L -- mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():output()
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
H = \;\;\foo
\quad
\begin{array}[t]{r}
LW_H = \{00,01,11,12,22,23,24,34,35,45,46\} \\
RW_H = \{00,01,02,03,04,14,24,25,26,36,46\} \\
\end{array}
$$
To recover the picc $L$ --- which is a picc on $\{0,1,2,3,4\}$ --- we
need to find where we change from an $L$-equivalence class to another
when we go from one digit to the next; and to recover the picc $R$ ---
which is a picc on $\{0,1,2,3,4,5,6\}$ --- we need to find where we
change from an $R$-equivalence class to another when we go from one
digit to the next.
We can recover $L$ and $R$ by walking $LW_H$ (or $RW_H$) from bottom
to top in a series of white pawns moves, and checking when we change
from one $S$-equivalence class to another. Northwest moves give
information about $L$, and northeast moves give information about $R$.
Look at the example below, in which we walk on $RW_H$:
%
\def\nem#1#2{\psm{ &\!#2\\ #1& \\}}
\def\nwm#1#2{\psm{ #2& \\ &\!#1\\}}
\def\nem#1#2{\sm{ &&\!#2\\ &\!\nearrow&\\ #1& \\}}
\def\nwm#1#2{\sm{ #2&\\&\!\nwarrow&\\ &&\!#1\\}}
\def\neyes#1#2#3#4{\nem{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #2 { \eqR} #4 \;⇒\; #2 #4 }
\def\neno #1#2#3#4{\nem{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #2 {\not\eqR} #4 \;⇒\; #2∖#4 }
\def\nwyes#1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #1 { \eqL} #3 \;⇒\; #3 #1 }
\def\nwno #1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #1 {\not\eqL} #3 \;⇒\; #3/#1 }
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="LWH"}, "1RLRLRRLRLR"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="RWH"}, "1RRRRLLRRLL"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
\begin{array}{c}
H = \;\;\foo
\qquad
LW_H = \;\;\LWH
\quad
RW_H = \!\!\!\!\!\!\!\!\RWH
%
\\ \\
%
\begin{array}{ll}
& \neno 25 26 \\
& \neyes 24 25 \\
\nwyes 36 46 & \neno 03 04 \\
\nwyes 26 36 & \neyes 02 03 \\
\nwyes 14 24 & \neyes 01 02 \\
\nwno 04 14 & \neyes 00 01 \\
\end{array}
%
\\ \\
%
% ⇒ \quad
(L,R) \;=\; (4321/0, 0123∖45∖6)
\end{array}
$$
% ____ _ _
% / ___|| | __ _ ___| |__ _ __ ___ __ ___ __
% \___ \| |/ _` / __| '_ \ _____| '_ ` _ \ / _` \ \/ /
% ___) | | (_| \__ \ | | |_____| | | | | | (_| |> <
% |____/|_|\__,_|___/_| |_| |_| |_| |_|\__,_/_/\_\
%
% «slash-max» (to ".slash-max")
\section{Slash-regions have maximal elements}
\label {slash-max}
% Good (phap 29 "slash-max")
...here is how our argument will work, in a particular case:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
I &=& [10,43], \\ \relax
[12]_S &=& I∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
$$\def\uoo#1#2{ \und{#1}{oo:#2} }
\def\uo #1#2{(\und{#1}{oo:#2})}
%
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈I}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
\qquad
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈H}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
$$
$$\bigvee [12]_S
= \bigvee \{11,12,13,22,23\}
= 11∨12∨13∨22∨23
∈ I∩H
$$
$$11 ≤ \bigvee [12]_S, \;
12 ≤ \bigvee [12]_S, \;
\ldots, \;
23 ≤ \bigvee [12]_S
$$
We have $[12]_S = I∩H$, and $\bigvee [12]_S$ belongs to $I∩H$ and is
greter-or-equal than all elements of $I∩H$, so $\bigvee [12]_S$ is the
maximal element of $[12]_S$.
\bsk
Here is how we can do that in the general case. Let $S=(L,R)$ be a
slashing on a ZHA $H$. Let $P$ be a point of $H$. The equivalence
class $[P]_S$ is a finite set $\{P_1, \ldots, P_n\}$, and we know that
$[P]_S=H∩I$ for some interval $I$. Look at the elements $P_1$,
$P_1∨P_2$, $(P_1∨P_2)∨P_3$, $\ldots$, $((P_1∨P_2)∨\ldots)∨P_n$ We can
see that all of them belong to both $H$ and $I$, so we conclude that
$\bigvee [P]_S = ((P_1∨P_2)∨\ldots)∨P_n$ belongs to $H∩I$, and it is
easy to see that it is greater-or-equal that all elements in $H∩I$, so
it is the maximal element of $H∩I$.
A similar argument shows that $\bigwedge [P]_S =
((P_1∧P_2)∧\ldots)∧P_n$ is the smallest element of $[P]_S$.
\msk
The same argument shows that if $C$ is any non-empty set of the form
$I∩H$, where $I$ is an interval, then $\bigvee C ∈ C$, $\bigwedge C ∈
C$, $[\bigwedge C, \bigvee C]∩H = C$.
Remember that an {\sl interval} in a ZHA $H$ is any set of the form
$[P,Q]∩H$. Let's introduce a new definition: a {\sl closed interval}
in a ZHA $H$ is a non-empty set $C⊂H$, with $⋁C∈C$, $⋀C∈C$, $[⋀C,
⋁C]∩H = C$; informally, a closed interval in a ZHA has a lowest and
highest element, and it ``is'' everything between them.
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
\section{Cuts stopping midway}
\label {cuts-stopping-midway}
% Good (phap 31 "cuts-stopping-midway")
We saw in the last section that every slash-region is a closed
interval. A {\sl partition into closed intervals} of a ZHA $H$ is, as
its name says, a partition of $H$ whose equivalence classes are all
closed intervals in $H$.
Some partitions into closed intervals of a ZHA are not slashings ---
for example, take the partition $P$ with these equivalence classes:
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234LL321")
%L -- mp:addlrs():addcuts("c 01|23 10w-11n 32w-33n"):output()
%L mp:addlrs():addcuts("c 01|23 20w-21n 32w-33n"):output()
$$\pu
\foo
$$
Here is an easy way to prove formally that the partition above does
not come from a slashing $S=(L,R)$. We will adapt the idea from
sec.\ref{slash-partitions}, where we recovered $L$ and $R$ from
northwest and northeast steps.
%
\def\undtrue #1{\und{#1}{\text{true}}}
\def\undfalse#1{\und{#1}{\text{false}}}
\def\undfrown#1{\und{#1}{=(}}
\def\iff{\;\;↔\;\;}
\def\notiff{\;\not↔\;}
%
$$\begin{array}{rcl}
\undfalse{21 \eqP 31} \;\;↔\;\; \undfrown{2 \eqL 3} \;\;↔\;\; \undtrue {22 \eqP 32} \\
\undtrue {31 \eqP 41} \;\;↔\;\; \undfrown{3 \eqL 4} \;\;↔\;\; \undfalse{32 \eqP 42} \\
\end{array}
$$
The problem is that the figure above has ``cuts stopping midway''...
if its cuts all crossed the ZHA all the way through, we would have
this for $L$ and northeast cuts,
%
$$\begin{array}{c}
0\eqL1 \iff 00\eqP10 \iff 01\eqP11 \iff 02\eqP12 \iff 03\eqP13 \\
1\eqL2 \iff 10\eqP20 \iff 11\eqP21 \iff 12\eqP22 \iff 13\eqP23 \\
2\eqL3 \iff 20\eqP30 \iff 21\eqP31 \iff 22\eqP32 \iff 23\eqP33 \\
3\eqL4 \iff 30\eqP40 \iff 31\eqP41 \iff 32\eqP42 \iff 33\eqP43 \\
4\eqL5 \iff 40\eqP50 \iff 41\eqP51 \iff 42\eqP52 \iff 43\eqP53 \\
5\eqL6 \iff 50\eqP60 \iff 51\eqP61 \iff 52\eqP62 \iff 53\eqP63 \\
\end{array}
$$
%
and something similar for $R$ and northwest cuts.
\msk
Formally, a partition $P$ on $H$ has an ``L-cut between $c$ and $c^+$
stopping midway'' if $cd \eqP c^+d \notiff cd \eqP c^+d$ for some $d$,
and it has an ``R-cut between $d$ and $d^+$ stopping midway'' if $cd
\eqP cd^+ \notiff c^+d \eqP c^+d^+$ for some $c$; here we are writing
$x^+$ for $x+1$.
\msk
{\sl Theorem: a partition of $H$ into closed intervals is a
slash-partition if and only if it doesn't have any cuts stopping
midway.} Proof: use the ideas above to recover $L$ and $R$ from
$\eqP$, and then check that $S=(L,R)$ induces an equivalence relation
$\eqS$ that coincides with $\eqP$.
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
% «slash-ops» (to ".slash-ops")
\section{Slash-operators}
\label {slash-ops}
% Good (phap 32 "slash-ops")
We can define operations that take each each $P∈H$ to the maximal and
to the minimal element of its $S$-equivalent class, now that we know
that these maximal and minimal elements exist:
%
$$\begin{array}{rclll}
P^S &:=& \bigvee [P]_S && \text{(maximal element),} \\
P^{\co S} &:=& \bigwedge [P]_S && \text{(minimal element).}
\end{array}
$$
Note that $[P]_S = [P^{\co S}, P^S]∩H$.
We will use the operation $·^S$ a lot and $·^{\co S}$ very little. The
`$\co$' in `$\co S$' means that $·^{\co S}$ is dual to $·^S$, in a
sense that will be made precise later.
\msk
A {\sl slash-operator} on a ZHA $H$ is a function $·^S:H→H$ induced by
a slashing $S=(L,R)$ on $H$. It is easy to see that $P ≤ P^S$
(``\,$·^S$ is non-decreasing'') and that $P^S = (P^S)^S$ (``\,$·^S$ is
idempotent'').
\msk
Any idempotent function $·^F:H→H$ induces an equivalence relation on
$H$: $P \eqF Q$ iff $P^F = Q^F$. We can use that to test if a given
$·^F:H→H$ is a slash-operator: $·^F$ is a slash-operator iff it obeys
all this:
1) $·^F$ is idempotent,
2) $·^F$ is non-decreasing,
3) $\eqF$ partitions $H$ into closed intervals,
4) $\eqF$ doesn't have cuts stopping midway.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ _ __ ___ _ __ ___ _ __| |_ _ _
% \___ \| |/ _` / __| '_ \ | '_ \| '__/ _ \| '_ \ / _ \ '__| __| | | |
% ___) | | (_| \__ \ | | | | |_) | | | (_) | |_) | __/ | | |_| |_| |
% |____/|_|\__,_|___/_| |_| | .__/|_| \___/| .__/ \___|_| \__|\__, |
% |_| |_| |___/
%
% «slash-ops-property» (to ".slash-ops-property")
\section{Slash-operators: a property}
\label {slash-ops-property}
% Good (phap 33 "slash-ops-property")
Slash-operators obey a certain property that will be very important
later. Let's state that property in five equivalent ways:
1) If $cd \eqS c'd'$ and $ef \eqS e'f'$ then $cd∧ef \eqS c'd'∧e'f'$.
2) If $P \eqS P'$ and $Q \eqS Q'$ then $P∧Q \eqS P'∧Q'$.
3) If $P \eqS P'$ and $Q \eqS Q'$ then $(P∧Q)^S = (P'∧Q')^S$.
4) If $P \eqS P'$ and $Q \eqS Q'$ then
%
$$\begin{array}{rclll}
(P∧Q)^S &=& (P^S∧Q^S)^S && \text{(a)} \\
&=& ((P')^S∧(Q')^S)^S && \text{(b)} \\
&=& (P'∧Q')^S && \text{(c)} \\
\end{array}
$$
5) $(P∧Q)^S = (P^S∧Q^S)^S$.
\msk
\noindent Here's a proof of $1↔2↔3↔4↔5$.
$1↔2$: we just changed notation,
$2↔3$: because $A \eqS B$ iff $A^S = B^S$,
$3→5$: make the substitution $\subst{P':=P^S \\ Q':=Q^S}$ in 3,
$5→4$: 4a is just a copy of 5, and 4c is a copy of 5 with
$\subst{P:=P' \\ Q:=Q'}$. For 4b, note that $P \eqP P'$ implies $P^S =
(P')^S$ and $Q \eqP Q'$ implies $Q^S = (Q')^S$,
$4→3$: 4 is an equality between more expressions than 3,
\msk
\noindent ...and here is a way to visualize what is going on:
%
% (find-planarhas "J-figure")
% (find-planarhaspage 19 "How J-operators interact with the connectives: figure")
% (find-planarhastext 19 "How J-operators interact with the connectives: figure")
%
%L -- The (&*) cube
%L mp = mpnew({def="andcube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3"):addlrs():output()
%L mp = mpnew({def="andCube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3")
%L mp:put(v"30", "P"):put(v"31", "P'", "P'"):put(v"32", "P*", "P^S")
%L mp:put(v"03", "Q"):put(v"13", "Q'", "Q'"):put(v"23", "Q*", "Q^S")
%L mp:output()
%
$$\pu
\begin{array}{c}
\andcube
\qquad
\andCube
\\ \\
\und{( \und{ \und{P}{30} ∧ \und{Q}{03} }{00} )^S}{22} =
\und{( \und{ \und{\und{P }{30}{}^S}{32} ∧ \und{\und{Q }{03}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{\und{P'}{31}{}^S}{32} ∧ \und{\und{Q'}{13}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{P'}{31} ∧ \und{Q'}{13} }{11} )^S}{22}
\\
\end{array}
$$
%
Note that all subexpressions belong to three $S$-regions: a region
with $P$, $P'$, $P^S=P'{}^S$, another with $Q$, $Q'$, $Q^S=Q'{}^S$,
and one with all the `$∧$'s. If we had cuts stopping midway then some
of the `$∧$'s could be in different regions.
I think that the clearest way to show (1) is by putting its proof in
tree form:
%
%L addabbrevs("(~S)", "\\eqS ", "(~L)", "\\eqL ", "(~R)", "\\eqR ")
%:
%: cd(~S)c'd' ef(~S)e'f' cd(~S)c'd' ef(~S)e'f'
%: ---------- ---------- ---------- ----------
%: c(~L)c' e(~L)e' d(~R)d' f(~R)f'
%: ------------------------ ------------------------
%: \min(c,e)(~L)\min(c',e') \min(d,f)(~L)\min(d',f')
%: ----------------------------------------------------
%: \min(c,e)\min(d,f)(~S)\min(c',e')\min(d',f')
%: --------------------------------------------
%: cd∧ef(~S)c'd'∧e'f'
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
% _
% | | ___ _ __ ___
% _ | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
% \___/ \___/| .__/|___/
% |_|
%
% «J-ops-and-regions» (to ".J-ops-and-regions")
% J-regions and J-operators
\section{J-operators and J-regions}
\label {J-ops-and-regions}
% Good (phap 35 "J-ops-and-regions")
A {\sl J-operator} on a Heyting Algebra $H = (Ω,≤,⊤,⊥,∧,∨,→,↔,¬)$ is a
function $J:Ω→Ω$ that obeys the axioms $\J1$, $\J2$, $\J3$ below; we
usually write $J$ as $·^*:Ω→Ω$, and write the axioms as rules.
%
%L addabbrevs("&", "\\&", "vv", "∨", "->", "→")
%L addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
%:
%: -----\J1 ------\J2 ------------\J3
%: P<=P! P!=P!! (P&Q)!=P!&Q!
%:
%: ^J1 ^J2 ^J3
%:
\pu
$$\ded{J1} \qquad \ded{J2} \qquad \ded{J3}$$
\par $\J1$ says that the operation $·^*$ is non-decreasing.
\par $\J2$ says that the operation $·^*$ is idempotent.
\par $\J3$ is a bit mysterious but will have interesting consequences.
\msk
Note that when $H$ is a ZHA then any slash-operator on $H$ is a
J-operator on it; see secs.\ref{slash-ops} and
\ref{slash-ops-property}.
\msk
A J-operator induces an equivalence relation and equivalence classes
on $Ω$, like slashings do:
%
$$\begin{array}{rcl}
P \eqJ Q &\text{iff}& P^*=Q^* \\[5pt] \relax
[P]^J &:=& \setofst{Q∈Ω}{P^*=Q^*} \\
\end{array}
$$
The axioms $\J1$, $\J2$, $\J3$ have many consequences. The first ones
are listed in Figure \ref{J-ops-basic-derived-rules} as derived rules,
whose names mean:
$\Mop$ (monotonicity for products): a lemma used to prove $\Mo$,
$\Mo$ (monotonicity): $P≤Q$ implies $P^*≤Q^*$,
$\Sand$ (sandwiching): all truth values between $P$ and $P^*$ are equivalent,
$\ECa$: equivalence classes are closed by `$\&$',
$\ECv$: equivalence classes are closed by `$∨$',
$\ECS$: equivalence classes are closed by sandwiching,
%:
%: ------------\J3 ---------
%: (P&Q)!=P!&Q! P!&Q!<=Q!
%: ----------\Mop := ---------------------------
%: (P&Q)!<=Q! (P&Q)!<=Q!
%:
%: ^Mop1 ^Mop2
%:
%: P<=Q
%: =====
%: P=P&Q
%: --------- ----------\Mop
%: P<=Q P!=(P&Q)! (P&Q)!<=Q!
%: ------\Mo := ---------------------
%: P!<=Q! P!<=Q!
%:
%: ^Mo1 ^Mo2
%:
%: Q<=P!
%: -------\Mo ------\J2
%: P<=Q Q!<=P!! P!!=P!
%: ------Mo ------------------
%: P<=Q<=P! P!<=Q! Q!<=P!
%: --------\Sand := ------------------------
%: P!=Q! P!=Q!
%:
%: ^Sand1 ^Sand2
%:
%:
%: P!=Q!
%: =========== ------------\J3
%: P!=Q! P!=Q!=P!&Q! P!&Q!=(P&Q)!
%: ------------\ECa := --------------------------
%: P!=Q!=(P&Q)! P!=Q!=(P&Q)!
%:
%: ^ECa1 ^ECa2
%: P!=Q!
%: -----\J1 -----
%: Q<=Q! Q!=P!
%: -----\J1 ---------------
%: P<=P! Q<=P!
%: ------- -------------------
%: P<=PvvQ PvvQ<=P!
%: --------------------
%: P<=PvvQ<=P!
%: -----------\Sand
%: P!=Q! P!=Q! P!=(PvvQ)!
%: ------------\ECv := ------------------
%: P!=Q!=(PvvQ)! P!=Q!=(PvvQ)!
%:
%: ^ECv1 ^ECv2
%:
%: P!=R!
%: -----\J1 -----
%: P<=Q<=R R<=R! R!=P!
%: -------------------------
%: P<=Q<=P!
%: --------\Sand
%: P<=Q<=R P!=R! P!=Q! P!=R!
%: --------------\ECS := -------------------
%: P!=Q!=R! P!=Q!=R!
%:
%: ^ECS1 ^ECS2
%:
\begin{figure}
\pu
\fbox{$
\begin{array}{rcl} \\
\ded{Mop1} &:=& \ded{Mop2} \\ \\
\ded{Mo1} &:=& \ded{Mo2} \\ \\
\ded{Sand1} &:=& \ded{Sand2} \\ \\
\ded{ECa1} &:=& \ded{ECa2} \\
\ded{ECv1} &:=& \ded{ECv2} \\ \\
\ded{ECS1} &:=& \ded{ECS2} \\ \\
\end{array}
$}
\caption{J-operators: basic derived rules}
\label{J-ops-basic-derived-rules}
\end{figure}
\bsk
Take a J-equivalence class, $[P]^J$, and list its elements: $[P]^J =
\{P_1, \ldots, P_n\}$. Let $P_∧ := ((P_1∧P_2)∧\ldots)∧P_n$ and Let
$P_∨ := ((P_1∨P_2)∨\ldots)∨P_n$. It turns out that $[P]^J =
[P_∧,P_∨]∩Ω$; let's prove that by doing `$⊆$' first, then `$⊇$'.
Using $\ECa$ and $\ECv$ several times we see that
%
$$\begin{array}{rrr}
P_1∧P_2 \eqJ P && P_1∨P_2 \eqJ P \\
(P_1∧P_2)∧P_3 \eqJ P && (P_1∨P_2)∨P_3 \eqJ P \\
\vdots\phantom{mmmm} && \vdots\phantom{mmmm} \\
((P_1∧P_2)∧\ldots)∧P_n \eqJ P && ((P_1∨P_2)∨\ldots)∨P_n \eqJ P \\
\end{array}
$$
%
so $P_∧ \eqJ P_∨ \eqJ P$, and by the sandwich lemma $([P_∧,P_∨]∩Ω) ⊆
[P]^J$.
For any $P_i∈[P]^J$ we have $P_∧≤P_i≤P_∨$, which means that:
%
$$\begin{array}{rcl}
[P]^J &=& \{P_1, \ldots, P_n\} \\
&⊆& \setofst{Q∈Ω}{P_∧≤Q≤P_∨} \\
&=& [P_∧,P_∨]∩Ω, \\
\end{array}
$$
%
so $[P]^J ⊆ [P_∧,P_∨]∩Ω$.
\msk
As the operation `$·^*$' is increasing and idempotent, each
equivalence class $[P]^J$ has exactly one maximal element, which is
$P^*$; but $P_∨$ is also the maximal element of $[P]^J$, so $P_∨ =
P^*$, and we can interpret the operation `$·*$' as ``take each $P$ to
the top element in its equivalence class'', which is similar to how we
defined an(other) operation `$·^*$' on slashings in the previous
section.
The operation ``take each $P$ to the bottom element in its equivalence
class'' will be useful in a few occasions; we will call it
`$·^{\co*}$' to indicate that it is dual to `$·^*$' in some sense.
Note that $P^{\co*} = P_∧$.
% (find-LATEX "2015planar-has.tex" "J-operators")
% (find-planarhaspage 13 "Part 2:" "J-operators and ZQuotients")
% (find-planarhastext 13 "Part 2:" "J-operators and ZQuotients")
% (find-LATEX "2015planar-has.tex" "J-derived-rules")
% (find-planarhaspage 15 "Derived rules")
% (find-planarhastext 15 "Derived rules")
\bsk
Look at the figure below, that shows a partition of a ZHA $A=[00,66]$
into five regions, each region being an interval; this partition does
not come from a slashing, as it has cuts that stop midway. Define an
operation `$·^*$' on $A$, that works by taking each truth-value $P$ in
it to the top element of its region; for example, $30^*=61$.
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234567654321")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
\foo
$$
%
It is easy to see that `$·^*$' obeys $\J1$ and $\J2$; however, it does
{\sl not} obey $\J3$ --- we will prove that in
sec.\ref{no-Y-cuts-no-L-cuts}. As we will see, {\sl the partitons of a
ZHA into intervals that obey $\J1$, $\J2$, $\J3$ ae exactly the
slashings;} or, in other words, {\sl every J-operator comes from a
slashing}.
% _ _ __ __ _
% | \ | | ___ \ \ / / ___ _ _| |_ ___
% | \| |/ _ \ \ V / / __| | | | __/ __|
% | |\ | (_) | | | | (__| |_| | |_\__ \
% |_| \_|\___/ |_| \___|\__,_|\__|___/
%
% «no-Y-cuts-no-L-cuts» (to ".no-Y-cuts-no-L-cuts")
\section{The are no Y-cuts and no $\lambda$-cuts}
\label {no-Y-cuts-no-L-cuts}
% Good (phap 37 "no-Y-cuts-no-L-cuts")
We want to see that if a partition of a ZHA $H$ into intervals has
``Y-cuts'' or ``$λ$-cuts'' like these parts of the last diagram in the
last section,
%
%R local Y, La =
%R 2/ 22 \, 2/ 25 \
%R |21 12| |24 15|
%R \ 11 / \ 14 /
%R
%R Y :tozmp({def="Ycut", scale="10pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
%R La:tozmp({def="Lcut", scale="10pt"}):addcells():addcuts("00w-00n 00e-10n"):output()
$$\pu
\begin{array}{rcl}
\Ycut &\Leftarrow& \text{this is a Y-cut} \\\\
\Lcut &\Leftarrow& \text{this is a $λ$-cut}\\
\end{array}
$$
%
then it operation $J$ that takes each element to the top of its
equivalence class cannot obey $\J1$, $\J2$ and $\J3$ at the same time.
We will prove that by deriving rules that say that if $11 \eqJ 12$
then $21 \eqJ 22$, and that if $15 \eqJ 25$ then $14 \eqJ 24$;
actually, our rules will say that if $11^* = 12^*$ then $(11∨21)^* =
(12∨21)^*$, and that if $15^*=25^*$ then $(15∧24)^*=(25∧24)^*$. The
rules are:
%: Q!=R!
%: -----------
%: PvvQ!=PvvR!
%: -----------------
%: Q!=R! (PvvQ!)!=(PvvR!)!
%: ---------------\NoYcuts := =================\ostarcube
%: (PvvQ)!=(PvvR)! (PvvQ)!=(PvvR)!
%:
%: ^NoYcuts1- ^NoYcuts2-
%:
%: P!=Q!
%: -----------
%: PvvR!=QvvR!
%: -----------------
%: P!=Q! (PvvR!)!=(QvvR!)!
%: ---------------\NoYcuts := =================\ostarcube
%: (PvvR)!=(QvvR)! (PvvR)!=(QvvR)!
%:
%: ^NoYcuts1 ^NoYcuts2
%:
%:
%: Q!=R!
%: ----------
%: Q!=R! P!&Q!=P!&R!
%: ---------------\NoLcuts := ------------\J3
%: (P&Q)!=(P&R)! (P&Q)!=(P&R)!
%:
%: ^NoLcuts1- ^NoLcuts2-
%:
%: P!=Q!
%: ----------
%: P!=Q! P!&R!=Q!&R!
%: ---------------\NoLcuts := ------------\J3
%: (P&R)!=(Q&R)! (P&R)!=(Q&R)!
%:
%: ^NoLcuts1 ^NoLcuts2
%:
$$\pu
\begin{array}{rcl}
\ded{NoYcuts1} &:=& \ded{NoYcuts2} \\ \\
\ded{NoLcuts1} &:=& \ded{NoLcuts2} \\ \\
\end{array}
$$
The top derivation mentions a rule called `$\ostarcube$', which will
be proved in the next section.
% _ _
% | | __ _ _ __ __| | ___ ___ _ __ _ __ ___
% _ | | / _` | '_ \ / _` | / __/ _ \| '_ \| '_ \/ __|
% | |_| | | (_| | | | | (_| | | (_| (_) | | | | | | \__ \
% \___/ \__,_|_| |_|\__,_| \___\___/|_| |_|_| |_|___/
%
% «J-ops-and-connectives» (to ".J-ops-and-connectives")
% (phap 39 "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")
Let's start by proving another three derived rules:
%:
%:
%: =====================\acz ==================\ocz ====================\icz
%: (P!&Q!)!=P!&Q!=(P&Q)! (P!vvQ!)!<=(PvvQ)! (P->Q^*)^*<=P^*->Q^*
%:
%: ^and*-extra-arrow ^or*-extra-arrow ^imp*-extra-arrow
%:
%:
%: ------\J2 ------\J2
%: P!!=P! Q!!=Q!
%: =============================\J3
%: (P!&Q!)!=P!!&Q!!=P!&Q!=(P&Q)!
%: -----------------------------
%: (P!&Q!)!=P!&Q!=(P&Q)!
%:
%: ^and*-extra-arrow-proof
%:
%: -------------
%: P->Q^*<=P->Q^*
%: ------ ------- ---------------
%: P<=PvvQ Q<=PvvQ (P->Q^*)&P<=Q^*
%: ------------\Mo -----------\Mo -------------------\Mo
%: P!<=(PvvQ)! Q!<=(PvvQ)! ((P->Q^*)&P)^*<=Q!!
%: --------------------------- -------------------\J2
%: P!vvQ!<=(PvvQ)! ((P->Q^*)&P)^*<=Q^*
%: -------------------\Mo -------------------\J3
%: (P!vvQ!)!<=(PvvQ)!! (P->Q^*)^*&P^*<=Q^*
%: -------------------\J2 -------------------
%: (P!vvQ!)!<=(PvvQ)! (P->Q^*)^*<=P^*->Q^*
%:
%: ^or*-extra-arrow-proof ^imp*-extra-arrow-proof
%:
%:
$$
\myresizebox{$\pu
\begin{array}{rcl}
\ded{and*-extra-arrow} &:=& \ded{and*-extra-arrow-proof} \\\\
\ded{or*-extra-arrow} &:=& \ded{or*-extra-arrow-proof} \\\\
\ded{imp*-extra-arrow} &:=& \ded{imp*-extra-arrow-proof} \\
\end{array}
$}
$$
%D diagram cube-and*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-and*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-or*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
\pu
%$$
% \begin{array}{rcl}
% \diag{cube-and*-obvious} && \diag{cube-and*-full} \\ \\
% \diag{cube-or*-obvious} && \diag{cube-or*-full} \\ \\
% \diag{cube-imp*-obvious} && \diag{cube-imp*-full} \\
% \end{array}
%$$
It is easy to prove each one of the arrows below ($A \diagxyto/->/ B$
means $A≤B$):
%
$$\myresizebox{$
\pu
\def∧{{\&}}
\def∨{{\lor}}
\def→{{\to}}
%
% \text{(omitted to make compilation faster)}
\diag{cube-and*-obvious}
\quad
\diag{cube-or*-obvious}
\quad
\diag{cube-imp*-obvious}
$}
$$
\bsk
The cubes above will be called the ``obvious and-cube'', the ``obvious
or-cube'', and the ``obvious implication-cube'', and they show partial
orders between expressions of the form $(P^? \odot Q^?)^?$, where the
`$\odot$' stands for one of the connectives `$∧$', `$∨$' or `$→$', and
each `?' marks a place where we can put either a `${}^*$' or nothing.
The rules $\acz$, $\ocz$ and $\icz$ that we proved in the beginning of
the section can be used to add more information to the partial orders
given by the three ``obvious'' cubes above; adding them yields the
cubes below, that will be called the ``full and-cube'', the ``full
or-cube'', and the ``full implication-cube''.
\bsk
%
\myresizebox{$
\pu
\def∧{{\&}}
\def∨{{\lor}}
\def→{{\to}}
%
% \text{(omitted to make compilation faster)}
\diag{cube-and*-full}
\quad
\diag{cube-or*-full}
\quad
\diag{cube-imp*-full}
$}
\bsk
We say that $\text{expr}_1 ≤ \text{expr}_2$ is true ``by the full
and-cube'' when $\text{expr}_1 ≤ \text{expr}_2$ can be read from the
(non-strict!) partial order in the the full and-cube; for example,
$P∧Q^* ≤ (P^*∧Q)^*$ is true ``by the full and-cube'', and similary
$P^*∨Q^* ≤ (P∨Q)^*$ is true by the full or-cube and $(P→Q)^* ≤ P→Q^*$
is true by the full implication-cube.
We write
%:
%:
%: ----------------------------\astarcube
%: \text{expr}_1≤\text{expr}_2
%:
%: ^astar
%:
%:
%: ----------------------------\ostarcube
%: \text{expr}_1≤\text{expr}_2
%:
%: ^ostar
%:
%:
%: ----------------------------\istarcube
%: \text{expr}_1≤\text{expr}_2
%:
%: ^istar
%:
$$\pu
\ded{astar}
\qquad
\ded{ostar}
\qquad
\ded{istar}
$$
%
to indicate that the expression below the bar is a consequence (a
substitution instance) of the partial order in the full and-cubes, the
full or-cube, or the full implication-cube.
\msk
The six cubes will be discussed in more detail in the section
\ref{comparing-partial-orders}.
% https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders
\newpage
% _ _ ____ ___
% | | ___ _ _| |__ ___ ___ __ _ ___ | _ \ / _ \ ___
% _ | |_____ / __| | | | '_ \ / _ \/ __| / _` / __| | |_) | | | / __|
% | |_| |_____| (__| |_| | |_) | __/\__ \ | (_| \__ \ | __/| |_| \__ \
% \___/ \___|\__,_|_.__/ \___||___/ \__,_|___/ |_| \___/|___/
%
% «J-cubes-as-partial-orders» (to ".J-cubes-as-partial-orders")
\section{J-cubes as partial orders}
\label {J-cubes-as-partial-orders}
% Good (phap 40 "J-cubes-as-partial-orders")
{
If we number the vertices of the cubes of
sec.\ref{J-ops-and-connectives} like ths,
%
$$\mat{ & 7 & \\
5 & 3 & 6 \\
1 & 4 & 2 \\
& 0 & \\
}
$$
%
then we can refer to their nodes as $(∧)_0, \ldots, (∧)_7$, $(∨)_0,
\ldots, (∨)_7$, $(→)_0, \ldots,$ $(→)_7$; note that
%
$$\begin{array}{rclcrcl}
(∧)_0 &=& P∧Q, && (∧)_4 &=& (P∧Q)^*, \\
(∧)_1 &=& P^*∧Q, && (∧)_{1+4} &=& (P^*∧Q)^*, \\
(∧)_2 &=& P∧Q^*, && (∧)_{2+4} &=& (P∧Q^*)^*, \\
(∧)_{1+2} &=& P^*∧Q^*, && (∧)_{1+2+4} &=& (P^*∧Q^*)^*, \\
\end{array}
$$
%
and the same for $(∨)_k$ and $(→)_k$.
With this convention we can interpret s set of arrows in a cube as a
subset of $\{0,\ldots,7\}^2$, and use the positional notation for
subsets from sec.\ref{positional} to represent that as a grid of `0's
and `1's:
%
%D diagram cube-and*-0
%D 2Dx 100 +20 +20
%D 2D 100 A1
%D 2D +15 A2 A3 A4
%D 2D +15 A5 A6 A7
%D 2D +15 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D ren A1 ==> 7
%D ren A2 A3 A4 ==> 5 3 6
%D ren A5 A6 A7 ==> 1 4 2
%D ren A8 ==> 0
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%R local foo, foos =
%R 2/0 0 0 1 0 1 1 0 \, 2/1 1 1 1 1 1 1 1 \
%R |0 0 1 0 1 0 0 0 | |1 0 1 0 1 0 1 0 |
%R |0 1 0 0 1 0 0 0 | |1 0 0 0 1 1 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 1 0 0 1 0 0 0 |
%R |0 1 1 0 0 0 0 0 | |1 1 1 1 0 0 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 0 1 0 0 0 0 0 |
%R |1 0 0 0 0 0 0 0 | |1 1 0 0 0 0 0 0 |
%R \0 0 0 0 0 0 0 0 / \1 0 0 0 0 0 0 0 /
%R
%R foo :tomp({def="foo", scale="7pt", meta="s"}):addcells():output()
%R foos:tomp({def="foos", scale="7pt", meta="s"}):addcells():output()
%
\pu
$$
\diag{cube-and*-0}
\quad
=
\quad
\cmat{(0,1),(2,3),(4,5),(6,7),\\
(0,2),(1,3),(4,6),(5,7),\\
(0,4),(1,5),(2,6),(3,7)\\
}
\quad
=
\quad
\foo
$$
This gives us a way to represent explictly the transitive-reflexive
closure of a set of arrows:
%
$$\left(\diag{cube-and*-0}\right)^*
\quad
=
\quad
\foos
$$
The derived rule $\acz$ from sec.\ref{J-ops-and-connectives} proves
%
$$(P^*∧Q^*)^*=P^*∧Q^*=(P∧Q)^*,
$$
%
that corresponds to arrows $7 \two/->`<-/<150> 3 \two/->`<-/<150> 4$;
if we add these arrows to the cube above we get this,
%
%D diagram cube-and*-0b
%D 2Dx 100 +20 +20
%D 2D 100 A1
%D 2D +15 A2 A3 A4
%D 2D +15 A5 A6 A7
%D 2D +15 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D ren A1 ==> 7
%D ren A2 A3 A4 ==> 5 3 6
%D ren A5 A6 A7 ==> 1 4 2
%D ren A8 ==> 0
%D
%D (( A1 A2 <- A1 A3 = A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D A3 A6 =
%D ))
%D enddiagram
%
%D diagram cube-and*-0c
%D 2Dx 100 +20 +20
%D 2D 100 A1
%D 2D +15 A2 A3 A4
%D 2D +15 A5 A6 A7
%D 2D +15 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D ren A1 ==> 7
%D ren A2 A3 A4 ==> 5 3 6
%D ren A5 A6 A7 ==> 1 4 2
%D ren A8 ==> 0
%D
%D (( A1 A2 = A1 A3 = A1 A4 =
%D A2 A5 <- A2 A6 = A3 A5 <- A3 A7 <- A4 A6 = A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%R local fooand =
%R 2/1 1 1 1 1 1 1 1 \
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 0 1 0 0 0 0 0 |
%R |1 1 0 0 0 0 0 0 |
%R \1 0 0 0 0 0 0 0 /
%R
%R fooand:tomp({def="fooand", scale="7pt", meta="s"}):addcells():output()
\pu
$$\diag{cube-and*-0b} \quad ;
$$
We have
%
$$\diag{cube-and*-0b}
\quad \neq \quad
\diag{cube-and*-0c}
$$
%
but:
%
$$\left(\diag{cube-and*-0b}\right)^*
\quad = \quad
\left(\diag{cube-and*-0c}\right)^*
\quad = \quad
\fooand
$$
Let's give a name to this (non-strict) partial order:
``$\astarcuben$'', the ``numerical version'' of the full and-cube. Now
we can see more clearly the extent of the rule $\astarcube$ defined in
the end of sec.\ref{J-ops-and-connectives}: we have
%:
%:
%: -------------\astarcube
%: (∧)_i≤(∧)_j
%:
%: ^acuberule
%:
$$\pu
\ded{acuberule}
$$
%
whenever $(i,j)∈\astarcuben$.
We have something similar for the or-cube and the implication-cube:
%
%D diagram cube-or*-0c
%D 2Dx 100 +20 +20
%D 2D 100 A1
%D 2D +15 A2 A3 A4
%D 2D +15 A5 A6 A7
%D 2D +15 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D ren A1 ==> 7
%D ren A2 A3 A4 ==> 5 3 6
%D ren A5 A6 A7 ==> 1 4 2
%D ren A8 ==> 0
%D
%D (( A1 A2 = A1 A3 <- A1 A4 =
%D A2 A5 <- A2 A6 = A3 A5 <- A3 A7 <- A4 A6 = A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%R local fooor =
%R 2/1 1 1 1 1 1 1 1 \
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 0 0 0 0 |
%R |1 0 1 0 0 0 0 0 |
%R |1 1 0 0 0 0 0 0 |
%R \1 0 0 0 0 0 0 0 /
%R
%R fooor:tomp({def="fooor", scale="7pt", meta="s"}):addcells():output()
\pu
$$\ostarcuben
\quad = \quad
\left(\diag{cube-or*-0c}\right)^*
\quad = \quad
\fooor
$$
%D diagram cube-imp*-0c
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> (P^*→Q^*)^*
%D ren A5 A3 A6 ==> (P→Q^*)^* P^*→Q^* (P^*→Q)^*
%D ren A1 A4 A2 ==> P→Q^* (P→Q)^* P^*→Q
%D ren A0 ==> P→Q
%D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 <- A1 A3 = A4 A6 <- A5 A7 =
%D A0 A4 -> A1 A5 = A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%R local fooimp =
%R 2/1 1 1 1 1 1 1 1 \
%R |0 0 1 0 0 0 1 0 |
%R |1 1 1 1 1 1 1 1 |
%R |0 0 1 0 1 0 1 0 |
%R |1 1 1 1 1 1 1 1 |
%R |0 0 1 0 0 0 0 0 |
%R |1 1 1 1 1 1 1 1 |
%R \1 0 1 0 0 0 0 0 /
%R
%R fooimp:tomp({def="fooimp", scale="7pt", meta="s"}):addcells():output()
\pu
$$\istarcuben
\quad = \quad
\left(\diag{cube-imp*-0c}\right)^*
\quad = \quad
\fooimp
$$
Note that the arrows $2→0$ and $6→4$ in the version for the
implication-cube above are not mistakes --- they correspond to
$P^*{→}Q ≤ P{→}Q$ and $(P^*{→}Q)^* ≤ (P{→}Q)^*$.
}
% __ __ _ _ _ __ ____ ___
% \ \ / /_ _| |_ _ __ _| |_(_) ___ _ __ ___ \ \ | _ \ / _ \ ___
% \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __| _____\ \ | |_) | | | / __|
% \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \ |_____/ / | __/| |_| \__ \
% \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/ /_/ |_| \___/|___/
%
% «valuations-induce-POs» (to ".valuations-induce-POs")
\section{Valuations induce partial orders}
\label {valuations-induce-partial-orders}
% Good (phap 42 "valuations-induce-POs")
Let $H$ be a ZHA, $J$ be a J-operator on $H$, and $v$ be a
``valuation'' that assigns to the variables $P$ and $Q$ values in $H$;
$v$ is a function from $\{P,Q\}$ to $H$, where $P$ and $Q$ are seen as
names. Once we have $(H,J,v)$ we have a natural way to extend $v$ to
make it assign values in $H$ for $P^*$, $Q^*$, and for the expressions
in the nodes of the and-cube, the or-cube and the implication-cube.
We will represent a triple $(H,J,v)$ graphically by something like
this,
%
%L mp = mpnew({def="andCube", scale="11pt"}, "12321"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
\pu
$$\andCube
$$
%
that shows the ZHA $H$, the slashing on $H$ corresponding to $J$, and
{\sl at least} $v(P)$ and $v(Q)$; sometimes the diagram will show also
$v(P^*)$ and $v(Q^*)$, for convenience. With this information is it
easy to calculate $v(\text{expr})$ for all `expr's of the form $(P^?
\odot Q^?)^?$, i.e., all the expressions in the nodes of the and-cube,
the or-cube and the implication-cube.
Let's restrict our attention to `$∨$' at this moment. We have:
%
\def\V#1{v(#1)}
\def\VV#1{v((∨)_#1)}
$$\andCube
\qquad
\begin{array}{rclcrclcl}
&&&& \V{P∨Q} &=& 11 &=& \VV0 \\
&&&& \V{P^*∨Q} &=& 21 &=& \VV1 \\
\V{P} &=& 10 && \V{P∨Q^*} &=& 12 &=& \VV2 \\
\V{Q} &=& 01 && \V{P^*∨Q^*} &=& 22 &=& \VV3 \\
\V{P^*} &=& 20 && \V{(P∨Q)^*} &=& 22 &=& \VV4 \\
\V{Q^*} &=& 02 && \V{(P^*∨Q)^*} &=& 22 &=& \VV5 \\
&&&& \V{(P∨Q^*)^*} &=& 22 &=& \VV6 \\
&&&& \V{(P^*∨Q^*)^*} &=& 22 &=& \VV7 \\
\end{array}
$$
This induces a partial order $\ostarcubev(v) ⊆ \{0,\ldots,7\}^2$ in
the following way: $i ≤_v j$ iff $\VV{i} ≤_H \VV{j}$. One easy way to
calculate this `$≤_v$' is to replace each number from 0 to 7 in the
cube by $\VV{i}$, and then draw arrows on that to represent the
partial order in $H$, and then bring these arrows ``back'':
%
%D diagram cube-or*-0v
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> (P^*∨Q^*)^*
%D ren A5 A3 A6 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A1 A4 A2 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A0 ==> P∨Q
%D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> 22
%D ren A5 A3 A6 ==> 22 22 22
%D ren A1 A4 A2 ==> 21 22 12
%D ren A0 ==> 11
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-0vn
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> (P^*∨Q^*)^*
%D ren A5 A3 A6 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A1 A4 A2 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A0 ==> P∨Q
%D
%D ren A7 ==> 22
%D ren A5 A3 A6 ==> 22 22 22
%D ren A1 A4 A2 ==> 21 22 12
%D ren A0 ==> 11
%D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%R local fooor =
%R 2/1 1 1 1 1 1 1 1 \
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 0 0 0 0 |
%R |1 0 1 0 0 0 0 0 |
%R |1 1 0 0 0 0 0 0 |
%R \1 0 0 0 0 0 0 0 /
%R
%R fooor:tomp({def="fooor", scale="7pt", meta="s"}):addcells():output()
\pu
$$\mat{ & 7 & \\
5 & 3 & 6 \\
1 & 4 & 2 \\
& 0 & \\
}
\quad\squigto\quad
\mat{ & 22 & \\
22 & 22 & 22 \\
21 & 22 & 12 \\
& 11 & \\
}
\;\;\squigto\;
\left(\diag{cube-or*-0v}\right)^*
\squigto\;
\left(\diag{cube-or*-0vn}\right)^*
$$
We can do this more compactly, as:
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%D diagram cube-or*-a
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-b
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P{∨}Q^*)^* P^*{∨}Q^* (P^*{∨}Q)^*
%D ren A1 A4 A2 ==> P{∨}Q^* (P{∨}Q)^* P^*{∨}Q
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
$$\pu
\begin{array}{rcl}
\ostarcubev\left(\orCube\right) &=& \left(\diag{cube-or*-a}\right)^* \\ \\
&=& \left(\diag{cube-or*-b}\right)^* \\
\end{array}
$$
%
which shows that {\sl in this valuation} we have, for example, $\VV3 =
\VV7$, i.e., $P^*{∨}Q^* = (P^*{∨}Q^*)^*$. The important information
that a valuation gives, though, is in its `$\not≤$'s. For example,
here we have
%
$$\begin{array}{rclcrcl}
\VV1 &<& \VV5 && P{∨}Q^* &<& (P{∨}Q^*)^* \\
\VV5 &>& \VV1 && (P{∨}Q^*)^* &>& P{∨}Q^* \\
\VV5 &\not≤& \VV1 && (P{∨}Q^*)^* &\not≤& P{∨}Q^* \\
\end{array}
$$
%
If it were possible to prove --- as in sec.\ref{J-ops-and-connectives}
--- that $(P{∨}Q^*)^* ≤ P{∨}Q^*$, then that would be true in all
valuations; by showing a valuation where $(P{∨}Q^*)^* \not≤ P{∨}Q^*$
we show that $(P{∨}Q^*)^* ≤ P{∨}Q^*$ cannot be a theorem, and that all
attempts to find a tree-like proof for $(P{∨}Q^*)^* ≤ P{∨}Q^*$ are
doomed to fail.
\msk
Note that
%
%L mp = mpnew({def="orCubeTen", scale="11pt"}, "12321L"):addcuts("c 321/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%D diagram cube-or*-c
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P{∨}Q^*)^* P^*{∨}Q^* (P^*{∨}Q)^*
%D ren A1 A4 A2 ==> P{∨}Q^* (P{∨}Q)^* P^*{∨}Q
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
$$\pu
\begin{array}{rcl}
\ostarcubev\left(\orCubeTen\right) &=& \left(\diag{cube-or*-c}\right)^* \\
\end{array}
$$
%
This new valuation tells us something that the previous one didn't:
that $P^*{∨}Q^* < (P^*{∨}Q^*)^*$ in some valuation, and so
$(P^*{∨}Q^*)^* ≤ P^*{∨}Q^*$ cannot be a theorem.
% ____ _ ____ ___
% / ___|___ _ __ ___ _ __ __ _ _ __(_)_ __ __ _ | _ \ / _ \ ___
% | | / _ \| '_ ` _ \| '_ \ / _` | '__| | '_ \ / _` | | |_) | | | / __|
% | |__| (_) | | | | | | |_) | (_| | | | | | | | (_| | | __/| |_| \__ \
% \____\___/|_| |_| |_| .__/ \__,_|_| |_|_| |_|\__, | |_| \___/|___/
% |_| |___/
%
% «comparing-partial-orders» (to ".comparing-partial-orders")
\section{Comparing partial orders}
\label {comparing-partial-orders}
% Rewrite (phap 44 "comparing-partial-orders")
If we represent the partial orders of the examples of the last section
as subsets of $\{0,\ldots,7\}^2$ we get:
%
%D diagram cube-or*-obv
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-or*-a
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-c
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="orCubeTen", scale="11pt"}, "12321L"):addcuts("c 321/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%R local fooobvious, foofull, foonine =
%R 2/1 1 1 1 1 1 1 1 \, 2/1 1 1 1 1 1 1 1 \, 2/1 1 1 1 1 1 1 1 \
%R |1 0 1 0 1 0 1 0 | |1 1 1 1 1 1 1 1 | |1 1 1 1 1 1 1 1 |
%R |1 1 0 0 1 1 0 0 | |1 1 1 1 1 1 1 1 | |1 1 1 1 1 1 1 1 |
%R |1 0 0 0 1 0 0 0 | |1 1 1 1 1 1 1 1 | |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 0 0 0 0 | |1 1 1 1 0 0 0 0 | |1 1 1 1 1 1 1 1 |
%R |1 0 1 0 0 0 0 0 | |1 0 1 0 0 0 0 0 | |1 0 1 0 0 0 0 0 |
%R |1 1 0 0 0 0 0 0 | |1 1 0 0 0 0 0 0 | |1 1 0 0 0 0 0 0 |
%R \1 0 0 0 0 0 0 0 / \1 0 0 0 0 0 0 0 / \1 0 0 0 0 0 0 0 /
%R
%R local footen = foofull
%R fooobvious:tomp({def="fooobvious", scale="7pt", meta="s"}):addcells():output()
%R foofull :tomp({def="foofull", scale="7pt", meta="s"}):addcells():output()
%R foonine :tomp({def="foonine", scale="7pt", meta="s"}):addcells():output()
%R footen :tomp({def="footen", scale="7pt", meta="s"}):addcells():output()
%
\pu
$$
\begin{array}{rclcl}
\ostarcubev\left(\orCube \right) &=& \left(\diag{cube-or*-a}\right)^* &=& \foonine \\ \\
\ostarcubev\left(\orCubeTen\right) &=& \left(\diag{cube-or*-c}\right)^* &=& \footen \\
\end{array}
$$
\def\ptab#1{\left(\begin{tabular}{c}#1\end{tabular}\right)}
If we represent the transitive-reflexive closures of the obvious
or-cube and the full or-cube of sec.\ref{J-cubes-as-partial-orders} as
subsets of $\{0,\ldots,7\}^2$, we get:
%
$$
\begin{array}{rclcl}
\ptab{obvious \\ or-cube \\}^* &=& \left(\diag{cube-or*-obv}\right)^* &=& \fooobvious \\ \\
\ptab{full \\ or-cube \\}^* &=& \left(\diag{cube-or*-c} \right)^* &=& \foofull \\
\end{array}
$$
If we compare these four partial orders we get:
%
%$$\ptab{obvious \\ or-cube \\}^*
% \subsetneq\;
% \ptab{full \\ or-cube \\}^*
% =\;
% \ostarcubev\left(\orCubeTen\right)^*
% \subsetneq\;
% \ostarcubev\left(\orCube \right)^*
%$$
%
$$\begin{array}{llllllll}
\ptab{obvious \\ or-cube \\}^*
& \!\! \subsetneq \!\!
& \ptab{full \\ or-cube \\}^* \\
& \!\! = \!\!
& \ostarcubev\left(\orCubeTen\right) % ^*
& \!\!\! \subsetneq \!\!\!\!
& \ostarcubev\left(\orCube \right) % ^*
\end{array}
$$
Note that each `1' in the grid of the obvious or-cube tells us
something that we know how to prove; the same for the full or-cube,
and the full or-cube has more `1's in its grid, so it has ``more
information'' --- about the existence of tree-like theorems --- than
the obvious or-cube. For example, the obvious or-cube tells us that we
know how prove $(P{∨}Q)^* ≤ (P^*{∨}Q^*)^*$, and the full or-cube tells
us that we know how to prove $(P{∨}Q)^* = (P^*{∨}Q^*)^*$.
\msk
Each '0' in the grid of a valuation-cube tells us about something that
cannot be be proved as a theorem, because that valuation is a
``countermodel'' for it. The first valuation in the beginning of this
section is on a ZHA with 9 elements, and the second one is on a ZHA
with 10 elements; let's refer to them as $(H_9,J_9,v_9)$ and $(H_{10},
J_{10}, v_{10})$, or just as $v_9$ and $v_{10}$. Note that the grid
for $v_{10}$ has more `0's; and $\ostarcubev(v_{10}) \subsetneq
\ostarcubev(v_9)$; for example, we have $(7,3)∈\ostarcubev(v_9)$ but
%
$$\begin{array}{llllll}
(7,3)\not∈\ostarcubev(v_{10}) &⇒& v_{10}(\VV7) \not≤_{H_{10}} v_{10}(\VV3) \\
&⇒& v_{10}((P^*{∨}Q^*)^*) \not≤_{H_{10}} v_{10}(P^*{∨}Q^*) \\
&⇒& v_{10} \text{ is a countermodel for }
(P^*{∨}Q^*)^* ≤ P^*{∨}Q^* \\
&⇒& v_{10} \text{ shows that } (P^*{∨}Q^*)^* ≤ P^*{∨}Q^* \\
&& \text{cannot be a theorem},
\end{array}
$$
%
so $v_{10}$ has ``more information'' --- now about the {\sl
non-existence} of tree-like theorems --- than $v_9$.
\msk
The full or-cube is ``better'' than the obvious or-cube, and the
$v_{10}$-cube is ``better'' than the $v_9$-cube. Moreover, the full
or-cube and the $v_{10}$-cube coincide, and this means that the status
of every statement of the form $\VV i ≤ \VV j$ can be determined in
the following way: if $\VV i ≤ \VV j$ is true in this partial order
%
$$\diag{cube-or*-c}
$$
%
then $\VV i ≤ \VV j$ is a consequence of the obvious or-cube plus
$\ocz$ (sec.\ref{J-ops-and-connectives}); if $\VV i ≤ \VV j$ is not
true in the partial order, then it cannot be proved as a theorem, and
the valuation $v_{10}$ is a countermodel for it.
We can do even better, and extract all information from well-chosen
valuations.
\msk
{\sl Theorem.} Take any statement of the form $\VV i ≤ \VV j$. If it
is true in the valuation below,
%
$$v_{(∨)} \quad = \quad v_{10} \quad = \quad \orCubeTen$$
%
then it is a theorem and can be proved using the obvious or-cube and
$\ocz$; if the statement is false in the valuation $v_{(∨)}$, then it
cannot be a theorem and $v_{(∨)}$ is a countermodel that shows that.
\msk
%L mp = mpnew({def="andCube", scale="11pt"}, "12321"):addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="impCube", scale="11pt"}, "12R1L"):addcuts("c 2/10 01|2")
%L mp:put(v"10", "P") -- :put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q") -- :put(v"02", "Q*", "Q^*")
%L mp:output()
%
\pu
We also have:
{\sl Theorem.} Take any statement of the form $(P^?{∧}Q^?)^? ≤
(P^?{∧}Q^?)^?$. If it is true in the valuation below,
%
$$v_{(∧)} \quad = \quad \andCube$$
%
then it is a theorem and can be proved using the obvious and-cube and
$\acz$; if the statement is false in the valuation $v_{(∧)}$, then it
cannot be a theorem and $v_{(∧)}$ is a countermodel that shows that.
{\sl Theorem.} Take any statement of the form $(P^?{→}Q^?)^? ≤
(P^?{→}Q^?)^?$. If it is true in the valuation below,
%
$$v_{(→)} \quad = \quad \impCube$$
%
then it is a theorem and can be proved using the obvious
implication-cube and $\icz$; if the statement is false in the
valuation $v_{(→)}$, then it cannot be a theorem and $v_{(→)}$ is a
countermodel that shows that.
% _ _ _ _
% | | (_)_ __ __| | ___ _ __ | |__ __ _ _ _ _ __ ___
% | | | | '_ \ / _` |/ _ \ '_ \| '_ \ / _` | | | | '_ ` _ \
% | |___| | | | | (_| | __/ | | | |_) | (_| | |_| | | | | | |
% |_____|_|_| |_|\__,_|\___|_| |_|_.__/ \__,_|\__,_|_| |_| |_|
%
% «lindenbaum-fragments» (to ".lindenbaum-fragments")
\section{Fragments of Lindenbaum Algebras}
\label {lindenbaum-fragments}
% Bad (phap 47 "lindenbaum-fragments")
% ____ _ _
% | _ \ ___ | |_ _ | | ___ _ __ ___
% | |_) / _ \| | | | | _ | |_____ / _ \| '_ \/ __|
% | __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_| \___/|_|\__, | \___/ \___/| .__/|___/
% |___/ |_|
%
% «polynomial-J-ops» (to ".polynomial-J-ops")
\section{Polynomial J-operators}
\label {polynomial-J-ops}
% Bad (phap 47 "polynomial-J-ops")
% (phop 22)
% (pho "J-examples")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 331) "polynomial")
\def\Jnotnot{{(¬¬)}}
\def\JiiR {{({→→}R)}}
\def\JoQ {{(∨Q)}}
\def\JiR {{({→}R)}}
\def\JfoQR {{(∨Q∧{→}R)}}
\def\JmiQ {({→→}Q∧{→}Q)}
{
It is not hard to check that for any Heyting Algebra $H$ and any
$Q,R∈H$ the operations $\Jnotnot$, $\ldots$, $\JfoQR$ below are
J-operators:
%
%$$\begin{array}{rclcrcl}
% (¬¬) &:=& λP{:}H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% \JiiR &:=& λP{:}H.((P{→}R){→}R) && \JiiR(P) &=& (P{→}R){→}R \\
% \JoQ &:=& λP{:}H.(P{∨}Q) && \JoQ(P) &=& P∨Q \\
% \JiR &:=& λP{:}H.(P{→}R) && \JiR(P) &=& P{→}R\\
% \JfoQR &:=& λP{:}H.((P{∨}Q) ∧ (P{→}R)) && \JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
%$$
%
$$\begin{array}{rclcrcl}
(¬¬)(P) &=& ¬¬P \\
\JiiR(P) &=& (P{→}R){→}R \\
\JoQ(P) &=& P∨Q \\
\JiR(P) &=& P{→}R\\
\JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
\end{array}
$$
Checking that they are J-operators means checking that each of them
obeys $\J1$, $\J2$, $\J3$. Let's define formally what are $\J1$, $\J2$
and $\J3$ ``for a given $F:H→H$'':
%
$$\begin{array}{rcc}
\J1_F &:=& (P ≤ F(P)) \\
\J2_F &:=& (F(P) = F(F(P)) \\
\J3_F &:=& (F(P∧P') = F(P)∧F(P')) \\
\end{array}
$$
%
and:
%
$$\J123_F \quad := \quad \J1_F ∧ \J2_F ∧ \J3_F.$$
Checking that $\Jnotnot$ obeys $\J1$, $\J2$, $\J3$ means proving
$\J123_\Jnotnot$ using only the rules from intuitionist logic from
sec.\ref{logic-in-HAs}; we will leave the proof of this, of and
$\J123_\JiiR$, $\J123_\JoQ$, and so on, to the reader.
\msk
The J-operator $\JfoQR$ is a particular case of building more complex
J-operators from simpler ones. If $J,K: H→H$, we define:
%
$$(J∧K) := λP{:}H.(J(P){∧}K(P))$$
%
it not hard to prove $\J123_{(J∧K)}$ from $\J123_J$ and $\J123_K$
using only the rules from intuitionistic logic.
\msk
The J-operators above are the first examples of J-operators in Fourman
and Scott's ``Sheaves and Logic'' (\cite{Fourman}); they appear in
pages 329--331, but with these names (our notation for them is at the
right):
(i) {\sl The closed quotient,}
$$J_a p = a ∨ p \qquad J_Q = \JoQ.$$
(ii) {\sl The open quotient,}
$$J^a p = a→p \qquad J^R = \JiR.$$
(iii) {\sl The Boolean quotient}.
$$B_a p = (p→a)→a \qquad B_R = \JiiR.$$
(iv) {\sl The forcing quotient}.
$$(J_a∧J^b)p = (a∨p)∧(b→p) \qquad (J_Q∧J^R) = \JfoQR.$$
(vi) {\sl A mixed quotient.}
$$(B_a∧J^a)p = (p→a)→p \qquad (B_Q∧J^Q) = \JmiQ.$$
\msk
The last one is tricky. From the definition of $B_a$ and $J^a$ what we
have is
%
$$(B_a∧J^a)p = ((p→a)→a)∧(a→p),$$
%
but it is possible to prove
%
$$((p→a)→a)∧(a→p) \;\;↔\;\; ((p→a)→p)$$
%
intuitionistically.
The operators above are ``polynomials on $P,Q,R,→,∧,∨,⊥$'' in the
terminology of Fourman/Scott: ``If we take a polynomial in $→,∧,∨,⊥$,
say, $f(p,a,b,\ldots)$, it is a decidable question whether for all
$a,b,\ldots$ it defines a J-operator'' (p.331).
\msk
When I started studying sheaves I spent several years without any
visual intuition about the J-operators above. I was saved by ZHAs and
brute force --- and the brute force method also helps in testing if a
polynomial (in the sense above) is a J-operator in a particular case.
For example, take the operators $λP{:}H.(P∧22)$ and $({∨}22)$ on
$H=[00,44]$:
%
% (phop 23)
% (pho "J-ops-diagrams")
% (pho "J-ops-diagrams" "jout")
% (find-dn6 "zhas.lua" "shortoperators-tests")
% (find-dn6file "zhas.lua" "mpnewJ =")
%
%L shortoperators()
%L mpnewF = function (opts, spec, J)
%L return mpnew(opts, spec, J):setz():zhaJ()
%L end
%L
%L mpnewF({def="fooa"}, "123454321", function (P) return And(v"22", P) end):output()
%L mpnewF({def="fooo"}, "123454321", Cloq(v"22")):output()
%L mpnewJ({def="fooO"}, "123454321", Cloq(v"22")):zhaPs("22"):output()
%
$$\pu
\begin{array}{rcccl}
λP{:}H.(P∧22) &=& \fooa \\ \\
({∨}22) &=& \fooo &=& \fooO \\
\end{array}
$$
The first one, $λP{:}H.(P∧22)$, is not a J-operator; one easy way to
see that is to look at the region in which the result is 22 --- its
top element is 44, and this violates the conditions on slash-operators
in sec.\ref{slash-ops}. The second operator, $({∨}22)$, is a slash
operator and a J-operator; at the right we introduce a convenient
notation for visualizing the action of a polynomial slash-operator, in
which we draw only the contours of the equivalence classes and the
constants that appear in the polynomial.
Using this new notation, we have:
%
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123R2L1", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123R2L1", Booq(v"11")):zhaPs("11"):output()
%L
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123454321", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123454321", Booq(v"22")):zhaPs("22"):output()
%L mpnewJ({def="foobor", scale="7pt", meta="s"}, "1234567654321", Cloq(v"42")):zhaPs("42"):output()
%L mpnewJ({def="foobim", scale="7pt", meta="s"}, "1234567654321", Opnq(v"24")):zhaPs("24"):output()
%L mpnewJ({def="foofor", scale="7pt", meta="s"}, "1234567654321", Forq(v"42", v"24")):zhaPs("42 24"):output()
%L mpnewJ({def="foomix", scale="7pt", meta="s"}, "12345654321", Mixq(v"22")):zhaPs("22"):output()
%
\pu
$$
\begin{array}{c}
(¬¬) \;\;=\;\;
({→→}00) \;\;=\;\; \fooboo \qquad \qquad
({→→}22) \;\;=\;\; \foobii \\
\\
({∨}42) \;\;=\;\; \foobor \qquad
({→}24) \;\;=\;\; \foobim \\[-20pt]
\\
({∨}42∧{→}24) \;\;=\;\; \foofor \\
\qquad \qquad
\qquad \qquad
\qquad \qquad
({→→}22∧{→}22) \;\;=\;\; \foomix \\
\end{array}
$$
Note that the slashing for $({∨}42∧{→}24)$ has all the cuts for
$({∨}42)$ plus all the cuts for $({→}24)$, and $({∨}42∧{→}24)$
``forces $42≤24$'' in the following sense: if $P^* = ({∨}42∧{→}24)(P)$
then $42^*≤24^*$.
}
% _ _ _
% _ __ (_) ___ ___ ___ __ _| | __ _ ___| |__ _ __ __ _
% | '_ \| |/ __/ __/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_) | | (_| (__\__ \ | (_| | | (_| | __/ |_) | | | (_| |
% | .__/|_|\___\___|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-piccs» (to ".algebra-of-piccs")
\section{An algebra of piccs}
\label {algebra-of-piccs}
We saw in the last section a case in which $(J∧K)$ has all the cuts
from $J$ plus all the cuts from $K$; this suggests that we {\sl may}
have an operation dual to that, that behaves as this: $(J∨K)$ has
exactly the cuts that are both in $J$ and in $K$:
%
$$\begin{array}{rcl}
\Cuts(J∧K) &=& \Cuts(J)∪\Cuts(K) \\
\Cuts(J∨K) &=& \Cuts(J)∩\Cuts(K) \\
\end{array}
$$
And it $J_1, \ldots, J_n$ are all the slash-operators on a given ZHA,
then
%
$$\begin{array}{rclcl}
\Cuts(J_1∧\ldots∧J_n) &=& \Cuts(J_1)∪\ldots∪\Cuts(J_k) &=& \text{(all cuts)} \\
\Cuts(J_1∨\ldots∨J_n) &=& \Cuts(J_1)∩\ldots∩\Cuts(J_k) &=& \text{(no cuts)} \\
\end{array}
$$
%
yield the minimal element and the maximal element, respectively, of an
algebra of slash-operators; note that the slash-operator with ``all
cuts'' is the identity map $λP{:H}.P$, and the slash-operator with
``no cuts'' is the one that takes all elements to $⊤$: $λP{:H}.⊤$.
This yields a lattice of slash-operators, in which the partial order
is $J≤K$ iff $\Cuts(J) ⊇ \Cuts(K)$. This is somewhat counterintuitive
if we think in terms of cuts --- the order seems to be reversed ---
but it makes a lot of sense if we think in terms of piccs
(sec.\ref{piccs-and-slashings}) instead.
\msk
Each picc $P$ on $\{0,\ldots,n\}$ has an associated function $·^P$
that takes each element to the top element of its equivalence class.
If we define $P≤P'$ to mean $∀a∈\{0,\ldots,n\}.\,a^P≤a^{P'}$, then we
have this:
%
% (pho "algebra-of-piccs")
% (phop 25 "algebra-of-piccs")
%
%L partitiongraph = function (opts, spec, ylabel)
%L local mp = MixedPicture.new(opts)
%L for y=0,5 do mp:put(v(-1, y), y.."") end
%L for x=0,5 do mp:put(v(x, -1), x.."") end
%L for a=0,5 do local aP = spec:sub(a+1, a+1)+0; mp:put(v(a, aP), "*") end
%L mp.lp:addlineorvector(v(0, 0), v(6, 0), "vector")
%L mp.lp:addlineorvector(v(0, 0), v(0, 6.5), "vector")
%L mp:put(v(7, 0), "a")
%L mp:put(v(0, 7), "aP", ylabel)
%L return mp
%L end
%L pg = function (def, spec, ylabel)
%L return partitiongraph({def=def, scale="5pt", meta="s"}, spec, ylabel)
%L end
%L
%L pg("grapha", "012345", "a^P" ):output()
%L pg("graphb", "113355", "a^{P'}" ):output()
%L pg("graphc", "115555", "a^{P''}" ):output()
%L pg("graphd", "555555", "a^{P'''}"):output()
%L
%
% a^P a^P a^P a^P
% ^ ^ ^ ^
% 5 | * 5 | * * 5 | * * * * 5 * * * * * *
% 4 | * 4 | 4 | 4 |
% 3 | * <= 3 | * * <= 3 | <= 3 |
% 2 | * 2 | 2 | 2 |
% 1 | * 1 * * 1 * * 1 |
% 0 *----------> a 0 +----------> a 0 +----------> a 0 +----------> a
% 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5
%
% 0|1|2|3|4|5 <= 01|23|45 <= 01|2345 012345
%
$$\pu
\begin{array}{ccccccc}
\grapha &≤& \graphb &≤& \graphc &≤& \graphd \\ \\
0|1|2|3|4|5 &≤& 01|23|45 &≤& 01|2345 &≤& 012345 \\
P &≤& P' &≤& P'' &≤& P''' \\
\end{array}
$$
This yields a partial order on piccs, whose bottom element is the
identity function $0|1|2|\ldots|n$, and the top element is $012\ldots
n$, that takes all elements to $n$.
The piccs on $\{0,\ldots,n\}$ form a Heyting Algebra, where
$⊤=01\ldots n$, $⊥=0|1|\ldots|n$, and `$∧$' and `$∨$' are the
operations that we have discussed above; it is possible to define a
`$→$' there, but this `$→$' is not going to be useful for us and we
are mentioning it just as a curiosity. We have, for example:
%
%D diagram algebra-of-piccs
%D 2Dx 100 +20 +20 +30 +20 +20
%D 2D 100 01234 T
%D 2D ^ ^
%D 2D | |
%D 2D +20 01|234 PvQ
%D 2D ^ ^ ^ ^
%D 2D / \ / \
%D 2D +20 0|1|234 01|2|34 P Q
%D 2D ^ ^ ^ ^
%D 2D \ / \ /
%D 2D +20 0|1|2|34 P&Q
%D 2D ^ ^
%D 2D | |
%D 2D +20 0|1|2|3|4 bot
%D 2D
%D (( T .tex= ⊤ PvQ .tex= P∨Q P&Q .tex= P∧Q bot .tex= ⊥
%D 01234 01|234 <- T PvQ <-
%D 01|234 0|1|234 <- 01|234 01|2|34 <- PvQ P <- PvQ Q <-
%D 0|1|234 0|1|2|34 <- 01|2|34 0|1|2|34 <- P P&Q <- Q P&Q <-
%D 0|1|2|34 0|1|2|3|4 <- P&Q bot <-
%D
%D ))
%D enddiagram
%D
$$\pu \diag{algebra-of-piccs}$$
% _ _ _
% | | ___ _ __ ___ __ _| | __ _ ___| |__ _ __ __ _
% _ | |_____ / _ \| '_ \/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | __/ |_) | | | (_| |
% \___/ \___/| .__/|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-J-ops» (to ".algebra-of-J-ops")
\section{An algebra of J-operators}
\label {algebra-of-J-ops}
% Bad (phap 50 "algebra-of-J-ops")
% (find-books "__cats/__cats.el" "fourman")
Fourman and Scott define the operations $∧$ and $∨$ on J-operators in
pages 325 and 329 (\cite{Fourman}), and in page 331 they list ten
properties of the algebra of J-operators:
%
$$
\def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
\def\li#1 #2 #3 #4 {\text{#1}& }
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} && (∨21)∨(∨12)=(∨22) \\
\li (ii) J^a∨J^b = J^{a∧b} && ({→}32)∨({→}23)=({→}22) \\
\li (iii) J_a∧J_b = J_{a∧b} && (∨21)∧(∨12)=(∨11) \\
\li (iv) J^a∧J^b = J^{a∨b} && ({→}32)∧({→}23)=({→}33) \\
\li (v) J_a∧J^a = ⊥ && (∨22)∧({→}22)=(⊥) \\
\li (vi) J_a∨J^a = ⊤ && (∨22)∨({→}22)=(⊤) \\
\li (vii) J_a∨K = K∘J_a \\
\li (viii) J^a∨K = J^a∘K \\
\li (ix) J_a∨B_a = B_a \\
\li (x) J^a∨B_b = B_{a→b} \\
\end{array}
$$
% (pho "J-ops-algebra-2")
% (phop 28 "J-ops-algebra-2")
The first six are easy to visualize; we won't treat the four last
ones. In the right column of the table above we've put a particular
case of (i), $\ldots$, (vi) in our notation, and the figures below put
all together.
In Fourman and Scott's notation,
%D diagram J-alg-1
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D ren T ==> J_⊤=⊤=J^⊥
%D ren A E ==> J_{22} J^{22}
%D ren B C F G ==> J_{21} J_{12} J^{32} J^{23}
%D ren D H ==> J_{11} J^{11}
%D ren bot ==> J_⊥=⊥=J^⊤
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-1}
$$
%
in our notation,
%
%D diagram J-alg-2
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D 2Dx 100 +20 +20 +15 +15 +20 +20
%D 2D 100 T
%D 2D +35 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +35 bot
%D 2D
%D ren T ==> (⊤∨)=(λP.⊤)=(⊥{→})
%D ren A E ==> (22∨) (22{→})
%D ren B C F G ==> (21∨) (12∨) (32{→}) (23{→})
%D ren D H ==> (11∨) (33{→})
%D ren bot ==> (⊥∨)=(λP.P)=(⊤{→})
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-2}
$$
%
and drawing the polynomial J-operators as in
sec.\ref{polynomial-J-ops}:
%
%L deforp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Cloq(v(P))):zhaPs(draw):print():output()
%L end
%L defimp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Opnq(v(P))):zhaPs(draw):print():output()
%L end
%L deforp("21", "21", "ora")
%L deforp("22", "22", "orb")
%L deforp("11", "11", "orc")
%L deforp("12", "12", "ord")
%L deforp("00", "", "orB")
%L defimp("32", "32", "ima")
%L defimp("22", "22", "imb")
%L defimp("33", "33", "imc")
%L defimp("34", "34", "imd")
%L defimp("00", "", "imB")
%
%R local algebra =
%R 4/ !imB \
%R | |
%R | !orb !imb |
%R |!ora !ord !ima !imd|
%R | !orc !imc |
%R | |
%R \ !orB /
%R
%R algebra:tomp({def="foo", scale="30pt"}):addcells():output()
$$\pu
% \bhbox{$
\begin{array}{c}
\\
\foo \\
\\
\end{array}
% $}
$$
% $$
% \def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
% \begin{array}{rlclcrlclc}
% \li (i) J_a∨J_b = J_{a∨b} (ii) J^a∨J^b = J^{a∧b}
% \li (iii) J_a∧J_b = J_{a∧b} (iv) J^a∧J^b = J^{a∨b}
% \li (v) J_a∧J^a = ⊥ (vi) J_a∨J^a = ⊤
% \li (vii) J_a∨K = K∘J_a (viii) J^a∨K = J^a∘K
% \li (ix) J_a∨B_a = B_a (x) J^a∨B_b = B_{a→b}
% \end{array}
% $$
%
% $$\begin{array}{rclcrcl}
% (¬¬) &:=& λP:H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% (→→R) &:=& λP:H.((P{→}R){→}R) && (→→R)(P) &=& (P{→}R){→}R \\
% (∨Q) &:=& λP:H.(P{∨}Q) && (∨Q)(P) &=& P∨Q \\
% (→R) &:=& λP:H.(P{→}R) && (→R)(P) &=& P{→}R\\
% (∨Q∧→R) &:=& λP:H.((P{∨}Q) ∧ (P{→}R)) && (∨Q∧→R)(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
% $$
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ ___ | |_ _
% \___ \| |/ _` / __| '_ \ | '_ \ / _ \| | | | |
% ___) | | (_| \__ \ | | | | |_) | (_) | | |_| |
% |____/|_|\__,_|___/_| |_| | .__/ \___/|_|\__, |
% |_| |___/
% «slashings-are-poly» (to ".slashings-are-poly")
\section{All slash-operators are polynomial}
\label {slashings-are-poly}
% (phap 51 "slashings-are-poly")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 30)
% (find-LATEX "2015planar-has.tex" "zquotients-poly")
{
%L local ba, bb, bc = Booq(v"04"), Booq(v"23"), Booq(v"45")
%L local babc = Jand(ba, Jand(bb, bc))
%L mpnewJ({def="slaT", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):addlrs() :output():print()
%L mpnewJ({def="slaA", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):addlrs() :output():print()
%L mpnewJ({def="slaB", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):addlrs() :output():print()
%L mpnewJ({def="slaC", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):addlrs() :output():print()
%L mpnewJ({def="fooa", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):zhaPs("04") :output():print()
%L mpnewJ({def="foob", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):zhaPs("23") :output():print()
%L mpnewJ({def="fooc", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):zhaPs("45") :output():print()
%L mpnewJ({def="food", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):zhaPs("04 23 45"):output():print()
%L mpnew ({def="fooe", scale="7pt", meta="s"}, "1R2R3212RL1" ):addlrs():output()
%L mpnewJ({def="foof", scale="7pt", meta="s"}, "1R2R3212RL1", babc):zhaJ() :output()
\pu
Here is an easy way to see that all slashings --- i.e., J-operators on
ZHAs --- are polynomial. Every slashing $J$ has only a finite number of
cuts; call them $J_1, \ldots, J_n$. For example:
%
$$J=\slaT \qquad J_1=\slaA \quad J_2=\slaB \quad J_3=\slaC$$
Each cut $J_i$ divides the ZHA into an upper region and a lower
region, and $J_i(00)$ yields the top element of the lower region.
Also, $({→→}J_i(00))$ is a polynomial way of expressing that cut:
%
$$\def\foo#1#2{
\begin{array}{rr}
J_#1= \\
% ({→→}J_#1(00))= \\
(→→#2)= \\
\end{array}}
\foo1{04} \fooa \quad
\foo2{23} \foob \quad
\foo3{45} \fooc
$$
The conjunction of these `$({→→}J_i(00))$'s yields the original
slashing:
%
% $$
% \begin{array}{c}
% \fooa ∧ \foob ∧ \fooc = \food
% \end{array}
% $$
%
$$(→→04)∧(→→23)∧(→→45) = \food = J$$
}
\newpage
% ___ _ _ _
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ __ _ _ __| | _____
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \ / _` | '__| |/ / __|
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | | (_| | | | <\__ \
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|\__,_|_| |_|\_\___/
%
% «question-marks» (to ".question-marks")
% (phap 53 "question-marks")
\section{Open sets of a certain form}
\label {question-marks}
\def\OPENS{\operatorname{\mathsf{Opens}}}
\def\OPENSPABD{\OPENS(\Opens_A(P),B,D)}
\def\OPENSPABD{\OPENS((P,A),B,D)}
\def\relevant {\operatorname{\mathsf{relev}}}
\def\qmarks {\operatorname{\mathsf{qmarks}}}
\def\forget {\operatorname{\mathsf{forget}}}
\def\propagate{\operatorname{\mathsf{prpgt}}}
\def\propagate{\operatorname{\mathsf{prp}}}
\def\biggest{\mathsf{biggest}}
\def\ess{\mathsf{ess}}
A 2-column graph with question marks (a ``2CGQ'') is a triple $((P,A),
B, D)$, where $(P,A)$ is a 2CG and $B⊆D⊆P$; let $G=((P,A), B, D)$. We
represent $G$ graphically like $(P,A)$, but with `0's, `?'s and '1's
on the points of $P$, and the expression ``$C$ is of the form $G$''
means $B⊆C⊆D$. For example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgbig("tcgL"):strs("0 1", "1 0 0"):vs():hs():output()
%L tcgbig("tcgR"):strs("0 ?", "1 ? 0"):vs():hs():output()
$$\pu
\tcgL \;\; \text{is of the form} \;\; \tcgR
$$
Informally, a `0' in the graphical representation of a 2CGQ $Q$ means
``all `$C$'s of the form $G$ have a `0' here'', a `1' means ``all
`$C$'s of the form $G$ have a `1' here'', and a `?' means ``some
`$C$'s of the form $G$ have `0's there and some have `1's''. More
formally, a 2CGQ $G$ corresponds to a partition of $P$ into $P_0$,
$P_1$ and $P_?$ --- the sets of `0's, `1's and `?'s of the graphical
representation of $G$ --- and we have $P_1=B$, $P_?=D∖B$, $P_0=P∖D$,
$D=P_1∪P_?$.
Our main use for 2CGQs will be for giving us a nice notation for ``the
set of open sets of $(P,A)$ betwen $B$ and $D$'':
%
$$\OPENSPABD \;\; = \;\; \setofst{U⊆P}{B⊆U⊆D \text{ and } U∈\Opens_A(P)}$$
Note that adding intercolumn arrows reduce sets of
opens sets,
%
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcg_spec = "6, 6; 43, "
%L tcgmed("tcgB"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcg_spec = "6, 6; 43, 54"
%L tcgmed("tcgC"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%
$$\pu
\OPENS\tcgA \;⊇\;
\OPENS\tcgB \;⊇\;
\OPENS\tcgC
$$
%
because each arrow is a ``restriction'' (sec.\ref{topologies-on-2CGs})
on what is considered an open set. We can propagate `1's forward along
arrows like `$1→?$' and `0's backward along arrows like `$?→0$'
without changing the result of `$\OPENS(\ldots)$':
%
%L tcg_spec = "6, 6; 43, "
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgB"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgL" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgR" ):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$
\pu
\OPENS\tcgA = \OPENS\tcgB
\qquad
\OPENS\tcgL = \OPENS\tcgR
$$
% ____ _ _
% | _ \ _ __ ___ _ __ __ _ __ _ __ _| |_(_) ___ _ __
% | |_) | '__/ _ \| '_ \ / _` |/ _` |/ _` | __| |/ _ \| '_ \
% | __/| | | (_) | |_) | (_| | (_| | (_| | |_| | (_) | | | |
% |_| |_| \___/| .__/ \__,_|\__, |\__,_|\__|_|\___/|_| |_|
% |_| |___/
%
% «propagation» (to ".propagation")
% (phap 53 "propagation")
\section{Propagation}
\label{propagation}
Fix a 2CG $(P,A)$. There are two good, natural ways to get rid of all
arrows `$1→0$' in a subset $C⊆P$: one, called `$\propagate_{1,(P,A)}$'
or `$\propagate_{1}$', ``propagates the `1's forward'', and the other
one, called `$\propagate_{0}$' or `$\propagate_{1,(P,A)}$',
``propagates the `0's backward''. An example:
%
%L tcg_spec = "2, 3; 22, "
%L tcgmed("tcgC"):strs("0 1", "1 0 0"):hs():output()
%L tcgmed("tcgD"):strs("1 1", "1 1 0"):hs():output()
%L tcgmed("tcgB"):strs("0 0", "1 0 0"):hs():output()
%
$$\pu
\propagate_0\tcgC = \tcgB
\qquad
\propagate_1\tcgC = \tcgD
$$
It easy to see that $\propagate_1(C)$ returns the smallest open set
containing $C$, and $\propagate_0(C)$ returns the largest open set
contained in $C$,
The {\sl interior} of a set $S$ in a topology $\calU$ on $P$ is the
biggest open set in $\calU$ contained in $S$, and, dually, the {\sl
cointerior} of a set $S$ is the smallest open set in $\calU$
containing $S$. In finite topologies cointeriors always exist.
\msk
{\sl Theorem 1.} For any 2CG $(P,A)$ and $S⊆P$ we have
%
$$\Int(S) = \propagate_0(S) ⊆ S ⊆ \propagate_1(S) = \coInt(S).$$
\msk
We can define propagations for 2CGQs in a way that changes only the
`?'s. If $G=((P,A),B,D)$ is a 2CGQ, then $\propagate_1(G)$ propagates
forward only the `1's in arrows like `$1→?$', and $\propagate_0(G)$
propagates backward only the `0's in arrows like `$?→0$'.
The operations `$\propagate_1$' and `$\propagate_0$' on 2CGQs need not
commute:
%
%L tcg_spec = "2, 2; 12, "
%L tcgmed("tcgN"):strs("? 1", "0 ?"):hs():output()
%L tcgmed("tcgZ"):strs("0 1", "0 0"):hs():output()
%L tcgmed("tcgO"):strs("1 1", "0 1"):hs():output()
$$\pu
% \propagate_1\left(\propagate_0 \tcgN\right)
% = \tcgZ ≠ \tcgO =
% \propagate_0\left(\propagate_1 \tcgN\right)
\begin{array}{rcl}
\propagate_1\left(\propagate_0 \tcgN\right) &=& \tcgZ \\ \\
\propagate_0\left(\propagate_1 \tcgN\right) &=& \tcgO \\
\end{array}
$$
%
but they can only fail to commute when $\OPENS(G)=∅$. When they
commute we will write their composite as `$\propagate$'.
\msk
{\sl Theorem 2.} Let $G=((P,A),B,D)$ be a 2CGQ with $\OPENS(G)≠∅$ and
let $G' = \propagate(G) = \OPENS((P,A), B', D')$, $P'_1=B'$,
$P'_?=D'∖B'$, $P'_1=P∖D'$. Then:
% Suppose that $\OPENS(G)≠∅$ and let $G' =
% \propagate(G) = \OPENS((P,A), \linebreak[0] B', D')$. Then:
a) In $G'$ everything below a `1' is also `1',
b) In $G'$ everything above a `0' is also `0',
c) $B' = P'_1$ is an open set,
d) $D' = P'_1∪P'_? = P∖P'_0$ is an open set,
e) $B' = \propagate_1(B) = \coInt(B)$,
f) $D' = \propagate_0(D) = \Int(D)$,
g) $B' = \pile(ab)$ for some $ab$,
h) $D' = \pile(ef)$ for some $ef$,
i) $B' ∈ \OPENS(G) = \OPENS(G')$,
j) $D' ∈ \OPENS(G) = \OPENS(G')$.
\msk
An example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
%L mp = mpnew({def="foo", meta="s", scale="7pt"}, "1R2R3212RL1"):addlrs():output()
%
$$\pu
\begin{array}{c}
G = \tcgG
\qquad
G' = \propagate(G) = \tcgGGG = ((P,A), \pile(11), \pile(23))
\\
% \OPENS(G) = \OPENS(G')
% \quad
% \two/<-`->/<300>^{\pile}_{\pile^{-1}}
% \quad
% [11,23]∩\;\;\foo \\
\end{array}
$$
\msk
The next theorem translates this to ZHAs, and shows that when
$\OPENS(G)≠∅$ then it returns an interval in a ZHA (in the sense of
sec.\ref{piccs-and-slashings}),
\msk
{\sl Theorem 3.} Let $G=((P,A),B,D)$ be a 2CGQ with $\OPENS(G)≠∅$ and
let $G' = \propagate(G) = \OPENS((P,A), B', D')$, $ab=\pile^{-1}(B')$,
$ef=\pile^{-1}(D')$, $I = \pile^{-1}(\OPENS(G)) =
\pile^{-1}(\OPENS(G'))$, and let $H$ be the ZHA generated by $(P,A)$,
i.e., $H=\pile^{-1}(\Opens_A(P))$. Then:
a) $ab$ is the minimal point of $I$,
b) $ef$ is the maximal point of $I$,
c) $I⊆H$,
d) $I=[ab,ef]∩H$,
e) if $A$ has no intercolumn arrows then $I=[ab,ef]$.
\msk
With Theorem 3 we can extend the last example to:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
%L mp = mpnew({def="foo", meta="s", scale="7pt"}, "1R2R3212RL1"):addlrs():output()
%
$$\pu
\begin{array}{c}
G = \tcgG
\qquad
G' = \propagate(G) = \tcgGGG = ((P,A), \pile(11), \pile(23))
\\
\OPENS(G) = \OPENS(G') = I
\quad
\two/<-`->/<300>^{\pile}_{\pile^{-1}}
\quad
[11,23]∩\;\;\foo \\
\end{array}
$$
In the next sections we will see that in some important cases the
results of $\OPENS(\ldots)$ coincide with J-equivalence classes.
% ____ _ _ _ _
% | _ \ ___| | _____ ____ _ _ __ | |_ _ __ ___ (_)_ __ | |_ ___
% | |_) / _ \ |/ _ \ \ / / _` | '_ \| __| | '_ \ / _ \| | '_ \| __/ __|
% | _ < __/ | __/\ V / (_| | | | | |_ | |_) | (_) | | | | | |_\__ \
% |_| \_\___|_|\___| \_/ \__,_|_| |_|\__| | .__/ \___/|_|_| |_|\__|___/
% |_|
%
% «relevant-points» (to ".relevant-points")
% (phap 55 "relevant-points")
% \section{The set of relevant points of a J-operator}
\section{The set of relevant points of a slashing}
We saw in sec.\ref{piccs-and-slashings} that a slashing on a ZHA $H$
can be represented a pair $(L,R)$ of piccs, that we drew in a V-shaped
diagram; let's write $S$ for the set of numbers above the cuts in the
V-shaped diagram, converting them to the notation for elements of the
left and the right columns of 2-column graphs:
%
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="vcuts"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
$$\pu
J = \ZQuotients
\qquad
(L,R) = \vcuts
\qquad
S = \{1\_, \; \_4, \_6\}
$$
We also saw (sec.\ref{J-ops-and-regions}) that on ZHAs there is a
bijection between slashings and J-operators. Let $\relevant(J)$ be the
operation that obtains the set $S$ for a J-operator $J$: $\relevant(J)
= \{1\_, \; \_4, \_6\}$ for the $J$ above. We will call $S⊆P$ the {\sl
set of relevant points} of the J-operator $J$, and $Q = \qmarks(J)
=P∖S$ will be the {\sl set of (points that will be replaced by)
question marks} by $J$. Note that we can also go from a set $Q⊆P$ to
a slashing and a J-operator, but we will not need a notation for that.
We can define the operation that receives a $C⊆P$ and ``forgets the
information on the points of $Q$'' on $C$, returning a 2CGQ, as:
%
$$\forget_{(P,A),Q}(C) \;\; = \;\; ((P,A), C∖Q, C∪Q)$$
%
for example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
$$\pu
\forget_{(P,A),Q}(\pile(12)) = \tcgG
$$
Note that
%
%L tcg_spec = "4, 6; , "
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgGP" ):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$\pu
\begin{array}{rcl}
\propagate(\forget_{(P,A),Q}(\pile(12))) &=& \tcgGP \\
&=& ((P,A), \pile(11), \pile(23))
\end{array}
$$
%
and that:
%
$$\begin{array}{rcl}
\pile^{-1}(\OPENS(\propagate(\forget_{(P,A),Q}(\pile(12))))) &=& [11,23]∩H \\
&=& [\co J(12), J(12)]∩H \\
&=& [12]^J \\
\end{array}
$$
%
this holds in general, as we will see soon.
% and when we apply $\OPENS$ (and $\pile^{-1}$) to that we get exactly
% $[11,23]∩H$, which is the J-equivalence class of 12 --- this happens
% always, but the easiest way to understand why is to start with {\sl
% rectangular} ZHAs.
% ____ _ _
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__|
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | |
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_|
% |___/
%
% «rectangular-versions» (to ".rectangular-versions")
% (phap 56 "rectangular-versions")
\section{Rectangular versions}
\label{rectangular-versions}
The ``rectangular version'' of a 2CG, a ZHA and a J-operator are
defined as this. Let $(P,A)$ be a 2CG and $H$ its associated ZHA, and
$J:H→H$ a J-operator on $H$; then $A'$ is $A$ minus its intercolumn
arrows, $H'$ is the (rectangular) ZHA associated to $(P,A')$, and
$J':H'→H'$ is J-operator on $H'$ that has the same cuts as $J$. The
primes on $A'$, $H'$ and $J'$ will always mean from here on that we
are on the rectangular versions. Let $Q=\qmarks(J)=\qmarks(J')$.
The rectangular versions for the $(P,A)$ and the $J$ that we are using
in our examples are:
%
%L tcg_spec = "4, 6; , "
%L tcgbig("tcgRect" ):lrs():vs():hs():output()
%L mp = mpnew({def="ZRect"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
(P,A') = \tcgRect
\qquad
J' = \ZRect
\;\;.
$$
Take any $C⊆P$, The result of $\forget_{(P,A'),Q}(C)$ is always of
this form,
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGF" ):strs("a ? ? ?", "? ? ? b ? c"):hs():output()
$$\pu
% \propagate(\forget_{(P,A'),Q}(C)) = \tcgGF
\forget_{(P,A'),Q}(C) = \tcgGF
$$
%
for some $a,b,c∈\{0,1\}$; moreover, if $C$ is open then
$\forget_{(P,A'),Q}(C)$ doesn't have `1's above `0's. Take any $C⊆P$
open in $(P,A)$; $C$ will be of the form $\pile(cd)$ for some $cd∈H'$.
Let $G=\forget_{(P,A'),Q}(C)$. The action of $\propagate$ on `$G$'s of
this form is particularly simple: each column of $G$ is made of blocks
of consecutive `?'s separated by `0's or `1's, and $\propagate$ acts
homogeneously on each block, leaving `?'s in at most one block in each
column. For example, if $a=b=1$ and $c=0$ then
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGF" ):strs("1 ? ? ?", "1 1 1 1 ? 0"):hs():output()
$$\pu
\propagate(\forget_{(P,A'),Q}(C)) = \tcgGF
$$
It is easy to see that:
\msk
{\sl Theorem 1.} If $C=\pile(cd)$ then
$\pile^{-1}(\OPENS(\propagate(\forget_{(P,A'),Q}(C))))$ is a
$J'$-equivalence class.
\msk
{\sl Theorem 2.} If $C=\pile(cd)$ then
$\pile^{-1}(\OPENS(\propagate(\forget_{(P,A'),Q}(C))))$ is $[\co
J'(cd), J'(cd)]$.
\msk
{\sl Theorem 3.} Suppose that $cd∈H$ (instead of $cd∈H'$) and let:
%
$$\begin{array}{rcl}
C &=& \pile(cd) \\
G &=& \forget_{(P,A'),Q}(C) \\
G' &=& \propagate(\forget_{(P,A'),Q}(C)) \\
G'' &=& \propagate(\forget_{(P,A ),Q}(C)) \\
I' &=& \pile^{-1}(\OPENS(G')) \\
I'' &=& \pile^{-1}(\OPENS(G'')) \\
\end{array}
$$
%
then $G'$ is a ``rectangular'' (and ``propagated'') 2CGQ, and $I'=[\co
J'(cd), J'(cd)]$ is a ``rectangular interval''; $G''$ is $G'$ plus
the intercolumn arrows, and with the propagations having been done
through the intercolumn arrows too. It is not hard to see that:
a) $\OPENS(G) = \OPENS(G') ⊇ \OPENS(G'')$
b) $I'' = I'∩H$
c) $cd∈I''$
d) $I'' = [\co J(cd), J(cd)]∩H$
e) $\pile(\co J(cd)), \pile(J(cd)) ∈ I''$
f) $G'' = ((P,A), \pile(\co J(cd)), \pile(J(cd)))$
g) $G'' = ((P,A), \coInt(C∖Q), \Int(C∪Q))$, so:
h) $\pile(\co J(cd)) = \coInt(C∖Q) = \propagate_1(C∖Q)$ and
i) $\pile(J(cd)) = \Int(C∪Q) = \propagate_0(C∪Q)$,
j) $\co J(cd)) = \pile^{-1}(\coInt(C∖Q)) = \pile^{-1}(\propagate_1(C∖Q))$ and
k) $J(cd) = \pile^{-1}(\Int(C∪Q)) = \pile^{-1}(\propagate_0(C∪Q))$.
\msk
A way to visualize what Theorem 3 means is to define $B, B', B'', D,
D' D''$ like this:
%
$$\begin{array}{rcl}
(B,D) &=& (C∖Q, C∪Q) \\
G' &=& ((P,A'),B',D') \\
G'' &=& ((P,A),B'',D'') \\
\end{array}
$$
%
%L mp = mpnew({def="ZRect", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"10", "B'") :put(v"43", "D'") :output()
%L mp = mpnew({def="ZOrig", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"11", "B''"):put(v"23", "D''") :output()
%L mp = mpnew({def="ZHAJR", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%L mp = mpnew({def="ZHAJ", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%
then, in the example we are using, omitting some `$\pile$'s and
`$\pile^{-1}$'s, we have:
%
$$\pu
J=\ZHAJ
\quad
J'=\ZHAJR
\quad
\ZRect
\quad
\ZOrig
$$
%
Theorem 3 shows several ways to calculate $B', C', B'', C''$.
% _ ____ ____ ____
% ___ _ _| |__ |___ \ / ___/ ___|___
% / __| | | | '_ \ _____ __) | | | | _/ __|
% \__ \ |_| | |_) |_____/ __/| |__| |_| \__ \
% |___/\__,_|_.__/ |_____|\____\____|___/
%
% «sub-2CGs» (to ".sub-2CGs")
\section{Sub-2-column graphs}
\label{sub-2CGs}
% (phap 58 "sub-2CGs")
Another way to understand the properties of the operation
$\forget_{(P,A),Q}$ is to think that it relates two topologies,
$\Opens_A(P)$ and $\Opens_{A|_S}(S)$ (mnemonic: $S$ is a ``smaller
set'', and $S = \relevant(J) = P∖Q$). We will sometimes denote
$\Opens_A(P)$ and $\Opens_{A|_S}(S)$ as just $\Opens(P)$ and
$\Opens(S)$; $\Opens(S)$ is a restriction of $\Opens(P)$ to $S$ in the
following sense: the open sets of $\Opens(S)$ are exactly the sets of
the form $U∩S$, where $U∈\Opens_A(P)$.
The topology $\Opens(S) = \Opens_{A|_S}(S)$ comes from a
``sub-2-column graph'' $(S,A|_S)$ of $(P,A)$, where the set of arrows
$A|_S$ can be obtained from $A$ and $S$ by
%
$$A|_S \;\;:=\;\; (A^*∩(S×S))^\ess,$$
%
which means: take the transitive-reflexive closure $A^*$ of $A$, which
yields a partial order on $P$, and restrict that order to $S$ by
taking $A^*∩(S×S)$; then (note: this last step is optional!) drop the
redundant arrows in $A^*∩(S×S)$ and keep only the ``essential'' ones,
which are the ones that can't be deleted without changing the order.
For clarity, we will draw the arrows in $(S,A|_S)$ as in the original
2CG $(P,A)$, even though some arrows may look as coming from or going
to nonexistent points; a really honest drawing of $(S,A|_S)$ in the
example below would be the one at the right, that has only one
intercolumn arrow, $1\_←\_6$, and only one vertical arrow, $\_6→\_4$.
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgP") :lrs():hs():vs():output()
%L tcgbig("tcgS"):strs("1\\_ · · ·", "· · · \\_4 · \\_6"):hs():vs():output()
%L tcg_spec = "4, 6; , 16"
%L local tcg =
%L tcgbig("tcgr"):strs("1\\_ {} {} {}", "{} {} {} \\_4 {} \\_6")
%L tcg:arrow(tcg:R(6), tcg:L(1), 0.07)
%L tcg:arrow(tcg:R(6), tcg:R(4), 0.17)
%L tcg:output()
%
$$
\pu
(P,A) = \tcgP
\qquad
(S,A|_S) = \tcgS = \tcgr
$$
A {\sl sub-2-column graph} is a graph $(S,A|_S)$ generated by a 2CG
$(P,A)$ and an $S⊆P$ by the procedure above: $A|_S =
(A^*∩(S×S))^\ess$.
\msk
{\sl Theorem 1.} Fix a ZHA $H$ and a J-operator $J$ on it, and from
that produce $(P,A)$, $\calU=\Opens_A(P)$, $S$, and $Q$. We clearly
have bijections between:
$\begin{tabular}{l}
1) the set of fixed points of $J$, $\setofst{ef∈H}{J(ef)=ef}$, \\
2) the set of fixed points of $\co J$, $\setofst{ab∈H}{\co J(ab)=ab}$, \\
3) the image of $J$, $J(H) = \setofst{J(cd)}{cd∈H}$, \\
4) the image of $\co J$, $\co J(H) = \setofst{\co J(cd)}{cd∈H}$, \\
5) the set of J-equivalence classes of $H$, $H/J = \setofst{[cd]^J}{cd∈H}$, \\
6) the elements $ef∈H$ such that $\pile(ef) = \Int(\pile(ef)∪Q)$, \\
7) the elements $ab∈H$ such that $\pile(ab) = \coInt(\pile(ab)∖Q)$, \\
8) the sets $U⊆\Opens(P)$ such that $U = \Int(U∪Q)$, \\
9) the sets $W⊆\Opens(P)$ such that $W = \coInt(W∖Q)$, \\
10) the sets $U⊆P$ such that $U = \Int(U∪Q)$, \\
11) the sets $W⊆P$ such that $W = \coInt(W∖Q)$, \\
12) the opens sets in $\Opens(S)$.
\end{tabular}
$
\msk
The partial order on $\Opens(S)$ is given by inclusion; some of the
corresponding partial orders on the other sets of Theorem 1 are not so
obvious.
\msk
{\sl Theorem 2}. Let $ab,cd∈H$, $A=\pile(ab)$, $B=\pile(cd)$,
$A'=A∩S$, $B'=B∩S$. The following are all equivalent:
1) $A'⊆B'$,
2) $A∖Q⊆B∖Q$,
2') $A∪Q⊆B∪Q$,
3) $\coInt(A∖Q)⊆\coInt(B∖Q)$,
3') $\Int(A∪Q)⊆\Int(B∪Q)$,
4) $\propagate_1(A∖Q)⊆\propagate_1(B∖Q)$
4') $\propagate_0(A∪Q)⊆\propagate_0(B∪Q)$
5) $\co J(ab) ≤ \co J(cd)$,
5') $J(ab)≤J(cd)$,
6) $\inf([ab]^J) ≤ \inf([cd]^J)$,
6') $\sup([ab]^J) ≤ \sup([cd]^J)$.
\msk
Items 6 and 6' give us a way to endow $H/J$ with a partial order.
Remember that $\sup([ab]^J) = J(ab)$ and $\inf([ab]^J) = \co J(ab)$;
we say that $[ab]^J ≤ [cd]^J$ when $J(ab) ≤ J(cd)$, or, equivalently,
$\co J(ab) ≤ \co J(cd)$.
\msk
{\sl Theorem 3.} For any $ab,cd,ef∈H$ we have:
1) $[cd]^J ≤ [ef]^J$ iff $cd ≤ J(ef)$,
2) $[ab]^J ≤ [cd]^J$ iff $\co J(ab) ≤ cd$.
\msk
We can put that in a diagram,
%
%D diagram foo
%D 2Dx 100 +30
%D 2D 100 [ef]^J |--> J(ef)
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 [cd]^J <--| cd
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 [ab]^J |--> coJ(ab)
%D 2D
%D ren coJ(ab) ==> {\co}J(ab)
%D (( [ef]^J J(ef) |-> .plabel= a \sup
%D [cd]^J cd <-|
%D [ab]^J coJ(ab) |-> .plabel= b \inf
%D ))
%D (( [ef]^J J(ef) [cd]^J cd
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( [cd]^J cd [ab]^J coJ(ab)
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
%
that can be read as a categorical statement: the functor $[·]^J: H →
H/J$ has a left adjoint $\inf:H/J→H$ and a right adjoint $\sup:H/J→H$,
where $\inf$ returns the smallest element of a J-equivalence class,
and $\sup$ returns the biggest.
% Every subset $S⊆P$ induces an inclusion $f:S→P$ and a restriction map
% $f^*:\Opens(P) → \Opens(S)$ that acts as $f^*(C) = C∩Q$. We can use
% brute force --- as in sec.\ref{HAs} --- to find operations $f_*, f_!:
% \Opens(S) → \Opens(P)$ that obey, for each $V∈\Opens(S)$,
% %
% $$???$$
% %
% _ _ _
% | | ___ _ __ ___ __ _ ___ __ _ __| |(_)___
% _ | |_____ / _ \| '_ \/ __| / _` / __| / _` |/ _` || / __|
% | |_| |_____| (_) | |_) \__ \ | (_| \__ \ | (_| | (_| || \__ \
% \___/ \___/| .__/|___/ \__,_|___/ \__,_|\__,_|/ |___/
% |_| |__/
%
% «J-ops-as-adjunctions» (to ".J-ops-as-adjunctions")
\section{J-operators as adjunctions}
\label {J-ops-as-adjunctions}
% (phap 60 "J-ops-as-adjunctions")
The last diagram of the last section can be translated to topological
language:
%L delabbrev("!!")
%L delabbrev("!")
%
%D diagram foo
%D 2Dx 100 +40 +30 +45
%D 2D 100 U --> J(U)
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 O(S) :::: O(P) V^* <-- V
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W --> coJ(W)
%D 2D
%D 2D +20 S0 -----> P0 S ---> P
%D 2D
%D ren J(U) V^* coJ(W) ==> \Int(U∪Q) V∩S \coInt(U∖Q)
%D ren O(S) O(P) ==> \Opens(S) \Opens(P)
%D ren S0 P0 ==> S P
%D
%D (( O(S) O(P) -> sl^^ .plabel= a f_*
%D O(S) O(P) <- .plabel= m f^*
%D O(S) O(P) -> sl__ .plabel= b f^!
%D S0 P0 -> .plabel= a f
%D ))
%D
%D (( U J(U) |-> .plabel= a f_*
%D V^* V <-| .plabel= m f^*
%D W coJ(W) |-> .plabel= m f^!
%D S P -> .plabel= a f
%D ))
%D (( U J(U) V^* V
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( V^* V W coJ(W)
%D @ 0 @ 2 <- @ 1 @ 3 <- @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
The notation used in the diagram above is essentially the one from
figures 6 and 7 in \cite{OchsIDARCT}; the ``external view'' is at the
left,``internal view'' is at the right, the adjunction is $f^! ⊣ f^* ⊣
f_*$, and the diagram shows that $f_*(U) = \Int(U∪Q)$, $f^*(V)=V∩S$
and $f^!(W)=\coInt(U∖Q)$ (where $\Int$ and $\coInt$ use the topology
$\Opens(P)$).
The order in which things are constructed in the diagram above is
different from last section, though. Now we start with a finite set
$P$, a topology $\Opens(P)$, and a subset $S⊆P$, and we define
$\Opens(S)$ by restriction:
%
$$\Opens(S) \;\;=\;\; \setofst{V∩S}{V∈\Opens(P)}$$
%
we define $Q$ as $P∖S$, we let $f:S→P$ be the inclusion and $f^*(V)$
be $V∩S$; then {\sl it turns out} (theorem!) that the $f^!$ and $f_*$
as defined above are the left and the right adjoints of $f^*$ --- and
$J$ and $\co J$ are built from $f^!$, $f^*$ and $f_*$: the definitions
%
$$\begin{array}{rcl}
J(V) &=& f_*(f^*(V)) \\
\co J(V) &=& f^!(f^*(V)) \\
\end{array}
$$
%
yield a J-operator $J:\Opens(P)→\Opens(P)$ and its `$\co$' version,
that returns the smallest element in each equivalence class; and if
$\Opens(P) = \Opens_A(P)$ for some 2CG $(P,A)$, then we can define $J$
and $\co J$ in this other way,
%
$$\begin{array}{rcl}
J(cd) &=& \pile^{-1}(f_*(f^*(\pile(cd)))) \\
\co J(cd) &=& \pile^{-1}(f^!(f^*(\pile(cd)))) \\
\end{array}
$$
%
that yields a J-operator (and its `$\co$' version) on the ZHA $H$
generated by the 2CG $(P,A)$.
\msk
This ``topological version'' of the adjunction is a nice concrete
starting point for understanding toposes and geometric morphisms
between them --- or, actually, for introducing geometric morphisms to
``children'' who prefer to start with finite examples in which
everything can be calculated explicitly. The toposes involved are
$\Set^{\Opens(S)^\op}$ and $\Set^{\Opens(P)^\op}$, and the adjunction
$f^! ⊣ f^* ⊣ f_*$ presented above acts only on the subobjects of the
terminal of each topos --- it needs to be extended to an (essential)
geometric morphism between these toposes. This, and several concepts
from section A4 of \cite{Elephant1}, will be treated in a sequel of
this paper, in a joint work with Peter Arndt.
% ____ _ _ _ _ _
% | __ )(_) |__ | (_) ___ __ _ _ __ __ _ _ __ | |__ _ _
% | _ \| | '_ \| | |/ _ \ / _` | '__/ _` | '_ \| '_ \| | | |
% | |_) | | |_) | | | (_) | (_| | | | (_| | |_) | | | | |_| |
% |____/|_|_.__/|_|_|\___/ \__, |_| \__,_| .__/|_| |_|\__, |
% |___/ |_| |___/
%
% «bibliography» (to ".bibliography")
% (pha "bibliography")
% (phap 63 "bibliography")
%
% (find-LATEX "catsem.bib" "bib-Ochs")
% (find-LATEX "catsem.bib" "bib-Fourman")
% (find-LATEX "catsem.bib" "bib-Ochs" "OchsIDARCT")
% (find-LATEX "catsem.bib" "bib-DaveyPriestley")
% (find-LATEX "catsem.bib" "bib-Johnstone")
% (find-idarct0file "2010diags-body.tex" "defun b")
\cite{Elephant1}
\cite{DaveyPriestley}
\cite{OchsIDARCT}
\cite{Fourman}
\cite{BellLST}
\bibliography{catsem}
%\bibliographystyle{plain}
\bibliographystyle{alpha}
% ___ _ _ _
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ __ _ _ __| | _____
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \ / _` | '__| |/ / __|
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | | (_| | | | <\__ \
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|\__,_|_| |_|\_\___/
%
% «question-marks» (to ".question-marks")
%\section{Question marks}
%\label {question-marks}
% Bad (phap 53 "question-marks")
% ____ _ _ _ _
% / ___| |__ (_) | __| |_ __ ___ _ __
% | | | '_ \| | |/ _` | '__/ _ \ '_ \
% | |___| | | | | | (_| | | | __/ | | |
% \____|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «children» (to ".children")
%\section{Appendix: on ``children''}
%\label{children}
% Bad (phap 57 "children")
% ____ _ _
% / ___|___ _ __ ___ _ __ _ __ ___| |__ ___ _ __ ___(_) ___ _ __
% | | / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \
% | |__| (_) | | | | | | |_) | | | __/ | | | __/ | | \__ \ | (_) | | | |
% \____\___/|_| |_| |_| .__/|_| \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
% |_|
%
% «comprehension» (to ".comprehension")
%\section{Appendix: notations for set comprehension}
% Bad (phap 58 "comprehension")
% (phap 39)
% (phap 46)
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: