Warning: this is an htmlized version! The original is across this link, and the conversion rules are here.
% (find-angg "LATEX/2017planar-has-1.tex")
% (find-angg "LATEX/2017planar-has-defs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has-1.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017planar-has-1.pdf"))
% (defun b () (interactive) (find-zsh "biber 2017planar-has-1"))
% (defun e () (interactive) (find-LATEX "2017planar-has-1.tex"))
% (find-xpdfpage "~/LATEX/2017planar-has-1.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017planar-has-1.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017planar-has-1.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017planar-has-1.pdf
%               file:///tmp/2017planar-has-1.pdf
%           file:///tmp/pen/2017planar-has-1.pdf
% http://angg.twu.net/LATEX/2017planar-has-1.pdf
%
% (find-anggfile "LATEX/" "2017planar-has-1.tex")
%
% Â«.titleÂ»				(to "title")
% Â«.abstractÂ»				(to "abstract")
% Â«.dednat6Â»				(to "dednat6")
%
% Â«.introductionÂ»			(to "introduction")
% Â«.childrenÂ»				(to "children")
% Â«.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")
% Â«.logic-in-HAsÂ»			(to "logic-in-HAs")
% Â«.derived-rulesÂ»			(to "derived-rules")
% Â«.derived-rules-fig1Â»			(to "derived-rules-fig1")
% Â«.derived-rules-fig2Â»			(to "derived-rules-fig2")
% Â«.topologiesÂ»				(to "topologies")
% Â«.topologies-on-ZSetsÂ»		(to "topologies-on-ZSets")
% Â«.topologies-as-partial-ordersÂ»	(to "topologies-as-partial-orders")
% Â«.2CGsÂ»				(to "2CGs")
% Â«.topologies-on-2CGsÂ»			(to "topologies-on-2CGs")
% Â«.topologies-as-HAsÂ»			(to "topologies-as-HAs")
% Â«.converting-ZHAs-2CAGsÂ»		(to "converting-ZHAs-2CAGs")
% Â«.ZHAL-is-betweenÂ»			(to "ZHAL-is-between")
%
% Â«.bibliographyÂ»			(to "bibliography")
%
%\documentclass[pdftex]{sajl}
\documentclass[lualatex]{sajl}
\volume{X}
\issue{X}
\year{20XX}
\setcounter{page}{1}

\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")

\usepackage{latexsym,amssymb,amsfonts,amsmath}
\usepackage{graphicx}
\usepackage{array}    % (find-es "tex" "array")
%\usepackage{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{edrx17}               % (find-angg "LATEX/edrx17.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrx17defs.tex             % (find-LATEX "edrx17defs.tex")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%\input edrxgac2.tex              % (find-LATEX "edrxgac2.tex")

\def\Opens{\mathcal{O}}
\catcodeâ=13 \defâ{\rightarrow}

% (find-es "tex" "newtheorem")
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{remark}[definition]{Remark}
\newtheorem{remarks}[definition]{Remarks}
\newtheorem{example}[definition]{Example}
\newtheorem{examples}[definition]{Examples}
\newtheorem{corollary}[definition]{Corollary}
\newtheorem{myfigure}[definition]{Figure}       % Edrx

\newcommand{\negr}[1]{\boldsymbol{#1}}
\newenvironment{proof}{\noindent\bf Proof. \rm}{\hfill $\negr{\blacksquare}$ \\}

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

\title{Planar HAs for Children}{Planar Heyting Algebras for Children}

\author{E. Ochs}{Eduardo Ochs}

\begin{document}

\setlength{\extrarowheight}{1pt}

\maketitle

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

\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$. We also show the connection
between ZHAs and the familiar semantics for IPL where the truth-values
are open sets: the points of a ZHA $H$ correspond to the open sets of
a finite topological space $(P,\Opens(P))$, where this $(P,\Opens(P))$
is an order topology on a 2-column graph''. The logic of ZHAs is
between classical and intuitionistic but different from both; there
are some sentences that are intuitionistically false but that can't
have countermodels in ZHAs --- their countermodels would need three
columns'' or more.

When a mathematical text says for children'' this means either that
it is written for people without lots of mathematical {\sl knowledge}
or that it doesn't require mathematical {\sl maturity}; we follow the
second, stronger, meaning of the term. Children'' for us means
people who are not able to understand structures that are too abstract
straight away, they need particular cases first --- and they also have
trouble with infinite objects, and with theorems about things that
they can't calculate: {\sl calculating} is much more basic for them
than {\sl proving}. Writing for children'' makes us enforce a style
where everything is constructive and finite and all the main examples
are objects that are easy to draw explicitly.

% It turns out that ZHA logic'' is between intuitionistic and
% classical proprositional logics and is different from both. Let
% $S=S_{PQR}âS_{QRP}âS_{RPQ}$, where $S_{ABC}=Aâ(BâC)$; then
% $\Taut(\IPL) \subsetneq \Taut(\ZHAL) \subsetneq \Taut(\CPL)$

% ; ZHAs are essentially planar,
% finite distributive lattices.

% In the second part of the paper 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 then
% be recovered from the inclusion $f:SâP$ as a restriction map $f^*: % \Opens(P)â\Opens(S)$ followed by a map $f_*: \Opens(S)â\Opens(P)$
% that reconstructs the missing information in the biggest way
% possible''.

% When a mathematical paper is written for children'' this means
% either that it is written for people without lots of mathematical {\sl
%   knowledge} or that it doesn't require mathematical {\sl maturity};
% we follow the second, stronger, meaning of the term. Children'' for
% us means people who are not able to understand structures that are too
% abstract straight away, they need particular cases first --- and they
% also have trouble with infinite objects, and with theorems about
% things that they can't calculate: {\sl calculating} is much more basic
% for them than {\sl proving}. Writing for children'' makes us enforce
% a style where everything is constructive and finite and all the main
% examples are objects that are easy to draw explicitly.

% Closure operators on Heyting Algebras are very important on Topos
% Theory: they generate geometric morphisms and sheaves. This paper
% introduces several tools that can be used to explain some parts of
% Topos Theory to children'', but here we stop just before
% categories and toposes --- when we move to categories and
% (pre)sheaves we have to replace most of the 0's and 1's in our
% diagrams by sets.

\end{abstract}

\keywords{Heyting Algebras, Intuitionistic Logic, diagrammatic
reasoning.}

%      _          _             _    __
%   __| | ___  __| |_ __   __ _| |_ / /_
%  / _ |/ _ \/ _ | '_ \ / _ | __| '_ \
% | (_| |  __/ (_| | | | | (_| | |_| (_) |
%  \__,_|\___|\__,_|_| |_|\__,_|\__|\___/
%
% Â«dednat6Â» (to ".dednat6")
% See: (find-LATEX "edrx17defs.tex" "dednat6")
\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

% (find-es "lua5" "luarepl-2017-latex")
% \def\repl{\eval{sync:run()}}
\def\repl{\eval{if os.getenv("REPL")=="1" then sync:run() end}}
\repl

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

\section*{Introduction}

This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} using finite Planar Heyting Algebras, that are
certain subsets of $\Z^2$. We call these subsets of $\Z^2$ ZHAs''
(sec.\ref{ZHAs}), and the interpretation of the connectives is
described in sec.\ref{prop-calc-ZHA}. In the second half of the paper
--- sec.\ref{topologies} onwards --- we show the relation between ZHAs
and topologies on certain finite sets; it turns out that ZHAs are
exactly the topologies on 2-column graphs'' (sections \ref{2CGs},
\ref{topologies-on-2CGs}, \ref{converting-ZHAs-2CAGs}).

The for children'' of the title uses the term children'' in a
unusual way. When we explain a theorem to children --- in the strict
sense of the term --- we focus on concrete examples, and we avoid
generalizations, abstract structures and infinite objects; when we
present something to children'', now in the wider sense of the term
that means people without mathematical maturity'', or even people
without expertise in a certain area'', we usually do something
similar: we start from a few motivating examples, and only then we
generalize. This is in stark contrast with how things are done for
example in most books on Category Theory, where concepts are usually
presented first in the most general way possible, and then the
motivating cases are mentioned very briefly --- let's call that style
mathematics for adults''. Here we try to do things in particular
cases first, but in a way that our proofs can be lifted'' to general
proofs with ease, with only trivial changes.

Except for the last section, this paper has been written to be
self-contained and readable by students with just a basic knowledge of
discrete mathematics and $»$-notation.

\msk

Two sequels to this paper are in preparation: one that shows how to
visualize closure operators'' on ZHAs, and another one that uses
that to show how to visualize several theorems about geometric
morphism on toposes (from section A4 of \cite{Elephant1}). It may be
possible, in the future, to find meta-theorems about how to do
mathematics for adults'' via mathematics for children'', or to
find criteria that say which examples for children'' are good enough
for lifting; but at this moment we are simply beginning to build a
corpus of examples and techniques --- an approach was inspired by
sections 22 and 23 of \cite{OchsIDARCT}.

% Two sequels to this

% \bsk
%
% 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

% %   ____ _     _ _     _
% %  / ___| |__ (_) | __| |_ __ ___ _ __
% % | |   | '_ \| | |/ _ | '__/ _ \ '_ \
% % | |___| | | | | | (_| | | |  __/ | | |
% %  \____|_| |_|_|_|\__,_|_|  \___|_| |_|
% %
% % Â«childrenÂ» (to ".children")
% \section{On Children''}
% \label  {children}
% % (ph1p 2 "children")
%
% Take a set $S=\{S_1, \ldots, S_n\}$ of freshmen students. Tell them
% Let $B$ be the set of all birds'', and ask them to take a piece of
% paper each and write down elements of $B$; let's call their lists
% $L_1, \ldots, L_n$. After some time we ask them to read their lists
% aloud, as we write the elements on the blackboard in an attempt to
% create a list $L=L_1âª\ldotsâªL_n$. What usually happens\footnote{At
%   least with me; I've done this experiment several times} is that
% disagreements will start to appear: $S_1$ has put Tweety but $S_2$
% complains that Tweety can't on the list because it's a {\sl fictional}
% bird; they can't agree if $S_3$'s pet parrot is the same bird as
% $S_4$'s parrot or not; hen'' may be the same of chick'', only
% older; they may not be sure if penguin, ostrich and archeopteryx are
% valid elements; and does that set $B$ change when a bird dies, or
% becomes extinct, of when a new species of feathered dinosuar is
% discovered?
%
% The use of real-world sets'' like $B$ often makes Maths confusing.
% Similar things also happen in other areas: for example, the standard
% way of teaching Object-Oriented Programming starts by saying that
% objects'' are things like shapes, windows, cars, and pizzas, and
% this idea baffles and paralyzes people who can't imagine ways to
% represent these objects in a computer...
%
% Something similar happens in other areas too
%
%
% \begin{itemize}
% \item Category theory should be more accessible
%
%   Most texts about CT are for specialists in research universities...
%   {\sl Category theory should be more accessible.}.
%
%   To whom?...
%
% \begin{itemize}
% \item Non-specialists (in research universities)
% \item Grad students (in research universities)
% \item Undergrads (in research universities)
% \item Non-specialists (in conferences - where we have to be quick)
% \item Undergrads (e.g., in CompSci - in teaching colleges) - (Children'')
% \end{itemize}
%
% \item What do we mean by "accessible"?
%
% \begin{itemize}
% \item Done on very firm grounds: mathematical objects made from
%   numbers, sets and tuples; FINITE, SMALL mathematical objects
%   whenever possible. Avoid references to non-mathematical things like
%   windows, cars and pizzas (like the object-orientation people do);
%   avoid reference to Physics; avoid Quantum Mecanics at all costs;
%   time is difficult to draw, prefer {\sl static} rather than {\sl
%     changing}
%
% \item People have very short attention spans nowadays
%
% \item Self-contained, but not {\sl isolated} or {\sl isolating}; our
%   material should make the literature more accessible
%
% \item We learn better by doing. Our material should have lots of space
%   for exercises.
%
% \item Most people with whom I interact are not from Maths/CS/etc
%
% \item {\sl Proving} general cases is relatively hard. {\sl Checking}
%   and {\sl calculating} is much easier. People can believe that
%   something can be generalized after seeing a convincing particular
%   case. (Sometimes leave them to look for the right generalization by
%   themselves)
% \end{itemize}
% \end{itemize}
%
%
%
% % when we tell them to take a piece of paper each, list
% % elements of the set of all birds, and then make a big list together,
% % is that we will stumble on several problems like these
%
%
% 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
% 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.

%  ____           _ _   _                   _
% |  _ \ ___  ___(_) |_(_) ___  _ __   __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _ | |
% |  __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_|   \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% Â«positionalÂ» (to ".positional")
\section{Positional notations}
\label  {positional}
% (ph1p  2 "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 =) %$$
%
$$\begin{array}{r} \;\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 =\!( \\ \\ \;\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 =) \\ \end{array}$$

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}
% (ph1p  4 "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 -- mp:output()
%
\pu
$$%\pu \Kb \;\;\;\;\text{will stand for:}\;\; \KB = \Kn =$$
$$\qquad \qquad \qquad \qquad \pmat{ % \cmat{ & (1,3), & \\ % (0,2), & & (2,2), \\ % & (1,1), & \\ % & (0,0) & \\ % }, \csm{ (1,3), \\ (0,2), \phantom{(1,2),} (2,2), \\ (1,1), \\ (0,0) \\ }, \csm{ ((1,3),(0,2)), ((1,3),(2,2)), \\ ((0,2),(1,1)), ((2,2),(1,1)), \\ ((1,1),(0,0)) \\ } }$$

\msk

Let's formalize this.

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

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

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

\msk

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

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

\msk

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

%  or even for the ZPOs seen as categories (section $\_\_\_$).

%  _     ____                            _ _             _
% | |   |  _ \    ___ ___   ___  _ __ __| (_)_ __   __ _| |_ ___  ___
% | |   | |_) |  / __/ _ \ / _ \| '__/ _ | | '_ \ / _ | __/ _ \/ __|
% | |___|  _ <  | (_| (_) | (_) | | | (_| | | | | | (_| | ||  __/\__ \
% |_____|_| \_\  \___\___/ \___/|_|  \__,_|_|_| |_|\__,_|\__\___||___/
%
% Â«LR-coordsÂ» (to ".LR-coords")
\section{LR-coordinates}
\label  {LR-coords}
% (ph1p  5 "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)
%
%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 mplr = zhav:tomp({def="mplr", scale="21pt", meta=nil})
%R mpxy = zhav:tomp({def="mpxy", scale="21pt", meta=nil})
%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 mplr = zhav:tomp({def="mplr", scale="19pt", meta=nil})
%R mpxy = zhav:tomp({def="mpxy", scale="20pt", meta=nil})
%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}
% (ph1p  7 "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 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 (in 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}
% (ph1p  6 "two-conventions")

We can use a bullet notation to denote ZHAs, but look at what happens
using the convention from sec.\ref{positional}:
%
$$\quad\picturedotsa(-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad \sa \quad\picturedots (-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad \sa \quad\picturedotsa (0,0)(4,5){ 2,0 3,1 4,2 1,1 2,2 3,3 0,2 1,3 2,4 1,5 }\quad$$
%
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="6pt", meta="s"}, "12321L")
%L local mpx = mpnew({def="foox", scale="6pt", meta="s"}, "12321L")
%L local mpl = mpnew({def="fool", scale="6pt", meta="s"}, "12321L")
%L local mpr = mpnew({def="foor", scale="6pt", meta="s"}, "12321L")
%L f = function (n) return "\\text{"..n.."}" end
%L mpx:zhalrf0("P -> f(P[1])"):output()
%L mpl:zhalrf0("P -> P:xytolr()[1]"):output()
%L mpr:zhalrf0("P -> P:xytolr()[2]"):output()
$$\pu \begin{array}{lll} B = \fooB \quad \text{(a ZHA)} & \phantom{m} & »(x,y){:}B.x = \foox \\ \\ »\ang{l,r}{:}B.l = \fool & & »\ang{l,r}{:}B.r = \foor \\ \end{array}$$

\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")
$$\pu »\ang{l,r}{:}B.\ang{l,r} \;=\; »lr{:}B.lr \;=\; \foo \qquad \quad B \;=\; \foo$$
%
Note that we are using the compact notation from the end of section
\ref{LR-coords}: $lr$' instead of $\ang{l,r}$'.

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

%  ____                              _
% |  _ \ _ __ ___  _ __     ___ __ _| | ___
% | |_) | '__/ _ \| '_ \   / __/ _ | |/ __|
% |  __/| | | (_) | |_) | | (_| (_| | | (__
% |_|   |_|  \___/| .__/   \___\__,_|_|\___|
%                 |_|
%
% Â«prop-calcÂ» (to ".prop-calc")
\section{Propositional calculus}
\label  {prop-calc}
% (ph1p  7 "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), \linebreak[0] (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
(PC-expressions''), 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}
% (ph1p  9 "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
%R local zdemorgan =
%R 1/ T   \
%R  |  o  |
%R  | . . |
%R  |q . p|
%R  | P Q |
%R  \  a  /
%R local T = {F="â", T="â", p="P'", q="Q'", a="â", o="â"}
%R
%
%L -- ÂÂPâP
%L ubs [[
%L Â Â  P 10 u  Pre 02 u Pre 20 u ()  â P 10 u Bin 12 u
%L   notnotP def   output
%L ]]
%L
%L -- Â(PâQ)â(ÂPâÂQ)
%L ubs [[
%L   Â P 10 u â Q 01 u Bin 00 u () Pre 32 u
%L   â   Â P 10 u Pre 02 u   â   Â Q 01 u Pre 20 u   Bin 22 u ()   Bin 22 u
%L   demorgan def   output
%L ]]
%L
%
$$\pu \begin{array}{ccccl} \ohouse && \znotnotP && \mat{\notnotP} \\ \\ && \zdemorgan && \mat{\demorgan} \\ \end{array}$$

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

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

%  _   _    _
% | | | |  / \   ___
% | |_| | / _ \ / __|
% |  _  |/ ___ \\__ \
% |_| |_/_/   \_\___/
%
% Â«HAsÂ» (to ".HAs")
% (ph1p  9 "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="12pt", meta=nil}):addcells(T):addcontour():output() %R QoRai:tozmp({def="QoRai", scale="12pt", meta=nil}):addcells(T):addcontour():output() %R PnnP :tozmp({def="PnnP" , scale="12pt", meta=nil}):addcells(T):addcontour():output() %R %R PoQai:tozmp({def="lozfive", scale="12pt", 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")
% Good (ph1p 12 "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.

\begin{theorem}
We have $(Q \toC R) = (Q \toHA R)$, for any ZHA $H$ and $Q,RâH$.
\end{theorem}

The proof will take the rest of this section, and our approach will be
to check that for any ZHA $H$ and $Q,RâH$ this holds, for all $PâH$:
%
$$(Pâ(Q \toC R))â(PâQâR).$$

\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="8pt", 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,
%
$$\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.

}

%  _                _        _         _   _    _
% | |    ___   __ _(_) ___  (_)_ __   | | | |  / \   ___
% | |   / _ \ / _ | |/ __| | | '_ \  | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__  | | | | | |  _  |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/   \_\___/
%             |___/
%
% Â«logic-in-HAsÂ» (to ".logic-in-HAs")
% (ph1p 14 "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")
% (ph1p 17 "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 Figure
\ref{derived-rules-fig1}:
%
$$\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
%:
% Â«derived-rules-fig1Â» (to ".derived-rules-fig1")
% (ph1p 19 "derived-rules-fig1")
% (find-es "tex" "figure-and-caption")
%
\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{\label{derived-rules-fig1}Derived rules}
%\begin{myfigure}Derived rules\end{myfigure}
\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
%:
% Â«derived-rules-fig2Â» (to ".derived-rules-fig2")
% (ph1p 20 "derived-rules-fig2")
%
\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{\label{derived-rules-fig2}Derived rules (2)}
\end{figure}

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

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

Figure \ref{derived-rules-fig1} 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 Figure
\ref{derived-rules-fig1}. 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 Figure \ref{derived-rules-fig2}. 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

%  _____                 _             _
% |_   _|__  _ __   ___ | | ___   __ _(_) ___  ___
%   | |/ _ \| '_ \ / _ \| |/ _ \ / _ | |/ _ \/ __|
%   | | (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
%   |_|\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%           |_|                  |___/
%
% Â«topologiesÂ» (to ".topologies")
\section{Topologies}
\label  {topologies}
% (ph1p 22 "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 kite  = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L mp = MixedPicture.new({def="dagX", meta="s", scale="5pt"}, z):zfunction(X):output()
%L mp = MixedPicture.new({def="dagKite",  meta="s", scale="6pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagKite",  meta="t", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):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}
% (ph1p 21 "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}
% (ph1p 24 "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 is not.

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

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

%R local house, ohouse = 2/  #1  \, 7/       !h11111                     \
%R                        |#2  #3|   |              !h01111              |
%R                        \#4  #5/   |       !h01011       !h00111       |
%R                                   |!h01010       !h00011       !h00101|
%R                                   |       !h00010       !h00001       |
%R                                   \              !h00000              /
%
%R local guill, oguill = 2/  #1  #2\, 8/                !g111111                \
%R                        |#3  #4  |   |        !g101111        !g011111        |
%R                        \  #5  #6/   |                !g001111        !g010111|
%R                                     |        !g001011        !g000111        |
%R                                     |!g001010        !g000011                |
%R                                     |        !g000010        !g000001        |
%R                                     \                !g000000                /
%
%R local w, womit, W =
%R 2/#1  #2  #3\, 2/    a     \, 7/              !w11111              \
%R  \  #4  #5  /   |  b c d   |   |       !w11011!w10111!w01111       |
%R                 |  e f g   |   |       !w10011!w01011!w00111       |
%R                 |h   i   j |   |!w10010       !w00011       !w00101|
%R                 |  k   l   |   |       !w00010       !w00001       |
%R                 \    m     /   \              !w00000              /
%
$$\pu \begin{array}{ccl} (H,\BPM(H)) = \zdagHouse & \qquad & (\Opens(H), â_1) = \def\h{\zfHouse}\zdagOHouse \\ \\ (G,\BPM(G)) = \zdagGuill & \qquad & (\Opens(G), â_1) = \def\g{\zfGuill}\zdagOGuill \\ \\ (W,\BPM(W)) = \zdagW & \qquad & (\Opens(W), â_1) = \def\w{\zfW}\zdagOW \\ \end{array}$$

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}
% (ph1p 24 "2CGs")

\def\l#1{#1\_}
\def\r#1{\_#1}

Note: in this section we will manipulate objects with names like $1\_, 2\_, 3\_, \ldots,$ $\_1, \linebreak[0] \_2, \linebreak[0] \_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="14pt", meta="p",   dv=2, dh=2.75, ev=0.32, eh=0.275}
%L tcg_Big    = {scale="14pt", meta="p",   dv=2, dh=3.5,  ev=0.32, eh=0.200}
%L tcg_medium = {scale= "9pt", meta="p s", dv=1, dh=2.2,  ev=0.32, eh=0.275}
%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 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}
% (ph1p 27 "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)âª\RC(b)$,

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

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

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

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

\msk

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

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

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

\msk

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

%  _____                             _   _    _
% |_   _|__  _ __  ___    __ _ ___  | | | |  / \   ___
%   | |/ _ \| '_ \/ __|  / _ / __| | |_| | / _ \ / __|
%   | | (_) | |_) \__ \ | (_| \__ \ |  _  |/ ___ \\__ \
%   |_|\___/| .__/|___/  \__,_|___/ |_| |_/_/   \_\___/
%           |_|
%
% Â«topologies-as-HAsÂ» (to ".topologies-as-HAs")
\section{Topologies as Heyting Algebras}
\label  {topologies-as-HAs}
% (ph1p 29 "topologies-as-HAs")

\def\toM{\ton{\text{M}}}

The {\sl open-set semantics} for Intuitionistic Propositional Logic is
based on this idea: choose any topological space $(X,\Opens(X))$; the
opens sets of $\Opens(X)$ will play the role of truth-values, and we
define the components of a Heyting Algebra (sec.\ref{HAs}) as this:
%
$$\begin{array}{rclcl} Ω &:=& \Opens(X) \\ P â Q &:=& PâQ \\ â &:=& \setofst{xâX}{â} &=& X \\ â &:=& \setofst{xâX}{â} &=& â \\ P â Q &:=& \setofst{xâX}{xâPâxâQ} &=& PâQ \\ P â Q &:=& \setofst{xâX}{xâPâxâQ} &=& PâªQ \\[5pt] P \toM Q &:=& \setofst{xâX}{xâPâxâQ} \\ &=& \setofst{xâX}{x\notâPâxâQ} &=& (XâP)âªQ \\ \end{array}$$
%
However, this $\toM$' {\sl may} return a non-open result even when
given open inputs,
%
$$\dagHouse 01010 \toM \dagHouse 00011 \;=\; \dagHouse 10111$$
%
so our definition is broken; we can fix it by taking the interior:
%
% (see sec.\ref{propagation}):
%
$$\begin{array}{rclcl} P \to Q &:=& \Int(P \toM Q) % \\ % &=& \Int(\setofst{xâX}{xâPâxâQ}) \\ &=& \Int((XâP)âªQ) \\ \end{array}$$

\begin{theorem}
For any topological space $(X,\Opens(X))$ the structure
$(Ω,â,â,â,â,â,â)$ defined as above is a Heyting Algebra. In
particular, this holds for any $P,Q,RâΩ$: $Pâ(QâR)$ iff $(PâQ)âR$.
\label{topologies-as-HAs-thm}
\end{theorem}

\begin{proof}
Standard; see for example \cite{Awodey} (section 6.3).
\end{proof}

Note that Theorem \ref{topologies-as-HAs-thm} gives us another way to
calculate the connectives in 2CGs. In sec.\ref{prop-calc-ZHA} we saw
how to calculate $ÂÂPâP$ in a certain ZHA when $P=10$; compare it with
the topological'' way, in which the truth-values are subsets of
$\dagHouseâââââ$:
%
$$\und{\und{Â\und{Â \und{P}{10}}{02}}{20} â \und{P}{10}}{12} \qquad \qquad \und{\und{Â\und{Â \und{P}{\dagHouse 00010}}{\dagHouse 00101}}{\dagHouse 01010} â \und{P}{\dagHouse 00010}}{\dagHouse 00111}$$

%  ______   _    _            __   __     ____   ____    _    ____
% |__  / | | |  / \   ___    / /   \ \   |___ \ / ___|  / \  / ___|___
%   / /| |_| | / _ \ / __|  / /_____\ \    __) | |     / _ \| |  _/ __|
%  / /_|  _  |/ ___ \\__ \  \ \_____/ /   / __/| |___ / ___ \ |_| \__ \
% /____|_| |_/_/   \_\___/   \_\   /_/   |_____|\____/_/   \_\____|___/
%
% Â«converting-ZHAs-2CAGsÂ» (to ".converting-ZHAs-2CAGs")
\section{Converting between ZHAs and 2CAGs}
\label  {converting-ZHAs-2CAGs}
% (ph1p 29 "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$,
and its bottom point is 00. Let $C := \{00, â\l1, â\l2, \ldots, â\l l, lr\}$, i.e., the left generators (see the end of
sec.\ref{topologies-on-2CGs}) plus $â$ and $â$; 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

\begin{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()
%
$$\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}$.
\end{theorem}

%
% \begin{proof}
% \end{proof}
%
% {\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:
%

%  ___ ____  _        __  ______   _    _    _        __   ____ ____  _
% |_ _|  _ \| |      / / |__  / | | |  / \  | |      / /  / ___|  _ \| |
%  | || |_) | |     / /    / /| |_| | / _ \ | |     / /  | |   | |_) | |
%  | ||  __/| |___  \ \   / /_|  _  |/ ___ \| |___  \ \  | |___|  __/| |___
% |___|_|   |_____|  \_\ /____|_| |_/_/   \_\_____|  \_\  \____|_|   |_____|
%
% Â«ZHAL-is-betweenÂ» (to ".ZHAL-is-between")
\section{ZHA Logic is between IPL and CPL}
\label{ZHAL-is-between}
% (ph1p 31 "ZHAL-is-between")

\def\IPL {\mathsf{IPL}}
\def\ZHAL{\mathsf{ZHAL}}
\def\CPL {\mathsf{CPL}}
\def\Taut{\mathsf{Taut}}
\def\Vars{\mathsf{Vars}}
\def\bfV {\mathbf{V}}

% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L local Pyr = ".1.|234"
%L mp = MixedPicture.new({def="dagPyr", meta="s", scale="5pt"}, z):zfunction(Pyr):output()
\pu

Let $S$ be this sentence:
%
$$\begin{array}{rcl} S_P &:=& Pâ(QâR) \\ S_Q &:=& Qâ(RâP) \\ S_R &:=& Râ(PâQ) \\ S &:=& S_P â S_Q â S_R \\ \end{array}$$

$S$ can't be an intuitionistic theorem because in this Heyting
Algebra, with these values for $P$, $Q$, $R$,
%
%R local w, womit, W =
%R 2/  #1  \, 2/  T   \, 6/      !w1111      \
%R  \#2#3#4/   |  a   |   |      !w0111      |
%R             |b c d |   |!w0110!w0101!w0011|
%R             |e f g |   |!w0100!w0010!w0001|
%R             \  h   /   \      !w0000      /
%
$$\pu \def\w{\zfPyr} (W,A) = \zfPyrmed1234 %\zdagPyr \qquad (\Opens_A(W), â_1) = \zdagOPyr \qquad \begin{array}{rcl} P &=& \dagPyr0100 \\ Q &=& \dagPyr0010 \\ R &=& \dagPyr0001 \\ \end{array}$$
%
we have $S=\dagPyr0111ââ=\dagPyr1111$.

One way to define a {\sl valuation} for a sentence $S$ with variables
$\Vars(S)$ --- in our example we have $\Vars(S)=\{P,Q,R\}$) --- is as
a pair made of a Heyting Algebra $H$ and a function $v:\Vars(S)âH$. A
looser definition is that a valuation for $S$ is a pair made of 1)
something that generates a Heyting Algebra in a known, canonical way,
and 2) a function from $\Vars(S)$ to the elements of that HA. So:

\msk

A {\sl classical valuation} for $S$ is a valuation of the form
$(\{0,1\},v)$.

A {\sl ZHA-valuation} for $S$ is a valuation of the form $(H,v)$,
where $H$ is a ZHA.

A {\sl finite DAG-valuation} for $S$ is a valuation of the form
$((W,A),v)$, where $W$ is a finite set and $AâWÃW$ is a set of arrows
on $W$; the Heyting Algebra on $(W,\Opens_A(W))$ is built as in
sec.\ref{topologies-as-HAs}.

A {\sl 2CG-valuation} for $S$ is a finite DAG-valuation for $S$ of the
form $((P,A),v)$, where $(P,A)$ is a 2-column graph; each
2CG-valuation is naturally equivalent to a ZHA-valuation, and
vice-versa.

\msk

A {\sl classical countermodel} for $S$ is classical valuation for $S$
in which the value of $S$ is not $â$; a {\sl ZHA-countermodel} for $S$
is a ZHA-valuation for $S$ in which the value of $S$ is not $â$; an
{\sl intuitionistic countermodel} for $S$ is a finite DAG-valuation for $S$
in which the value of $S$ is not $â$.

\msk

A sentence $S$ is a {\sl classical tautology} (notation:
$Sâ\Taut(\CPL)$) if $S$ has no classical countermodels; a sentence $S$
is a {\sl ZHA-tautology} (notation: $Sâ\Taut(\ZHAL)$); and a sentence
$S$ is an {\sl intuitionistic tautology} (notation: $Sâ\Taut(\IPL)$)
of $S$ has no finite-DAG countermodels.

\msk

It is a standard result that the intuitionistic {\sl theorems} are
exactly the finite-DAG {\sl tautologies}; this can be seen using GÃ⊃del
translation (see \cite{Goedel1933f} and \cite{Goedel1933fintro}) to
translate $S$ to S4, and then using modal tableaux for S4
(\cite{Fitting72}) to look for a countermodel; in standard
terminology, $W$ is a set of worlds'', $A$ is an accessibility
relation'' or a notion of which worlds are ahead'' of which other
ones, and $(W,A^*)$ is a Kripke frame for S4.

The sentence $S=S_P â S_Q â S_R$ of the beginning of the section is a
good example for introducting tableau methods for modal logics to
children'', as the tableau that it generates doesn't have branches.
We can present the method directly and in elementary terms, as we will
do now.

\msk

Fix a set $W$ and a relation $AâWÃW$. We will say that $β$ is
ahead'' of $α$ when $(α,β)âA^*$, i.e., when there is a path
$αâ\ldotsâβ$ using only arrows in $A$. Let $P$ and $Q$ be open sets in
$\Opens_A(W)$. The only way to have $PâQ$ false in a world $α$
(notation: $(PâQ)_α=0$) is to have $P_α=0$ and $Q_α=0$. The only way
to have $PâQ$ false in a world $α$, i.e., $(PâQ)_α=0$ is to have
$P_β=1$ and $Q_β=0$ in {\sl some} world $β$, with $β$ ahead of $α$.

Let $((W,A),v)$ be a finite DAG-countermodel for $S=S_P â S_Q â S_R$.
Then $v(P), \linebreak[0] v(Q), \linebreak[0] v(R)â\Opens_A(W)$; we
will omit the $v$'s. If $((W,A),v)$ is a countermodel this means that
$Sââ$, and there is some world $α$ in $W$ in which $S_α=0$. Fix this
$α$. $S_α=0$ means $(S_P â S_Q â S_R)_α=0$, which means that
$(S_P)_α=0$, $(S_Q)_α=0$, and $(S_R)_α=0$. $(S_P)_α=0$ means
$(Pâ(QâR))_α=0$, which means that there is a world $β$ ahead of $α$ in
which $P_β=1$ and $(QâR)_β=0$, and $(QâR)_β=0$ means $Q_β=0$ and
$R_β=0$; similarly, $(S_Q)_α=0$ means that there is a world $γ$ ahead
of $α$ in which $Q_γ=1$, $R_γ=0$, $P_γ=0$, and $(S_R)_α=0$ means that
there is a world $∧$ ahead of $α$ in which $R_∧=1$, $P_∧=0$, $Q_∧=0$.
In diagrams:
%
%D diagram smallpyr
%D 2Dx     100 +20 +20
%D 2D  100     α
%D 2D
%D 2D  +20 β   γ   ∧
%D 2D
%D (( α β ->
%D    α γ ->
%D    α ∧ ->
%D ))
%D enddiagram
%D
%D diagram bigpyr
%D 2Dx     100   +50   +50
%D 2D  100       \mata
%D 2D
%D 2D  +50 \matb \matc \matd
%D 2D
%D (( \mata \matb ->
%D    \mata \matc ->
%D    \mata \matd ->
%D ))
%D enddiagram
%D
$$\def\mata{\begin{array}{c} S_α=0 \\ (S_P)_α = (Pâ(QâR))_α = 0 \\ (S_Q)_α = (Qâ(RâP))_α = 0 \\ (S_R)_α = (Râ(PâQ))_α = 0 \\ \end{array} } \def\matb{\begin{array}{c} P_β=1 \\ (QâR)_β=0 \\ Q_β=0 \\ R_β=0 \\ \end{array} } \def\matc{\begin{array}{c} Q_γ=1 \\ (RâP)_γ=0 \\ R_γ=0 \\ P_γ=0 \\ \end{array} } \def\matd{\begin{array}{c} R_∧=1 \\ (PâQ)_∧=0 \\ P_∧=0 \\ Q_∧=0 \\ \end{array} } \pu \diag{smallpyr} \qquad \diag{bigpyr}$$

Note that $β$ and $γ$ are independent'' in the sense that in $A^*$
we can't have an arrow $βâγ$ and neither an arrow $γâβ$; we can't have
$βâγ$ because $P_β=1$ but $P_γ=0$, and we can't have $γâβ$ because
$Q_γ=1$ but $Q_β=0$. We can use a similar argument to show that $γ$
and $∧$ are independent, and to show also that $∧$ and $β$ are
independent.

{\sl We can't have three independent points in a 2-column graph,} so
we have finite DAG-countermodels for $S$ but no 2CG-countermodels for
$S$, and so no ZHA-countermodels for $S$. This means that $S$ is not
an intuitionistic tautology, but it is a ZHA-tautology. It is easy to
see that $\Taut(\IPL)â\Taut(\ZHAL)â\Taut(\CPL)$, and we saw that $S \notâ \Taut(\IPL)$, $Sâ\Taut(\ZHAL)$, $(ÂÂPâP) \notâ \Taut(\ZHAL)$,
$(ÂÂPâP) â \Taut(\IPL)$, which means that:
%
$$\Taut(\IPL) \subsetneq \Taut(\ZHAL) \subsetneq \Taut(\CPL)$$
%
and so ZHA Logic'', {\sl which we have not defined via a deduction
system,} only by the notions of ZHA countermodels'' and ZHA
tautologies'', is strictly between Intuitionistic Logic and Classical
Logic, and is different from both.

It may be possible to axiomatize our ZHA Logic'' as a logic of
width 2'' using the ideas from \cite{ModalHandbook}, pp.449--450, but
I have not attempted to do that yet.

% (find-books "__modal/__modal.el" "fitting")

% (ph1     "topologies")
% (ph1p 22 "topologies")

% We saw in sec.\ref{prop-calc} a figure that shows that $PâQâPâQ$ is
% not a tautology in Classical Logic, and in sec.\ref{prop-calc-ZHA} we
% saw a figure that shows that $Â(PâQ)â(ÂPâÂQ)$ is not a tautology in a
% certain ZHA; it reappered in sec.\ref{topologies-as-HAs}, translated
% to a topological setting. We saw very little about deductive systems
% --- only a bit in sec.\ref{logic-in-HAs}.
%
% There is an easy argument that shows that ZHA Logic'' lies between
% Classical Propositional Logical and Intuitionistic Propositional
% Logic, and is distinct from both. We will work on the sets of
% tautologies. Let:
% %
% %
% We will try to find a countermodel for $S$, and in the process we will
% discover that $\Taut(\IPL) \subsetneq \Taut(\ZHAL) \subsetneq % \Taut(\CPL)$.
%
% If $E$ is a PC-expression (sec.\ref{prop-calc}) on a set $\bfV$ of
% variables --- say, $\bfV = \{P,Q,R\}$ --- then a {\sl valuation} for
% $E$ if a triple $(W,A,v)$, where $W$ is a finite set of worlds'',
% $AâWÃW$ is an accessibility relation'' on $W$, and
% $v:\bfVâ\Opens_A(W)$ is a function that assigns an open set to each
% variable in $\bfV$. Our examples will only need cases where $W$ is a
% ZSet and $A = \BPM(W)$, and this lets us use a very compact notation
% for a triple $(W,A,v)$ in which only $v$ is shown and $W$ and $A$ are
% left implicit.

% Â«bibliographyÂ» (to ".bibliography")
% (find-anggfile "LATEX/" "2017planar-has-1.tex")
% (find-LATEXfile "sajl/template-sajl.tex" "\\begin{thebibliography}{10}")
% (ph1     "bibliography")
% (ph1p 36 "bibliography")
% (pha     "bibliography")
% (phap 63 "bibliography")

% (find-kopkadaly4page (+ 12 310) "With \\nocite{*}, every entry")
% (find-kopkadaly4text (+ 12 310) "With \\nocite{*}, every entry")
% (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4page (+ 12 316) "14.2.3 Cross-referencing")
% (find-kopkadaly4text (+ 12 316) "14.2.3 Cross-referencing")

% % (find-kopkadaly4page (+ 12 309) "\\bibliography{database1,")
% % (find-kopkadaly4text (+ 12 309) "\\bibliography{database1,")
% \bibliography{catsem}
% %\bibliographystyle{plain}
%
% % (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% % (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")
% \bibliographystyle{alpha}

\printbibliography

\authorname{Eduardo Ochs}
Rua Recife, s.n., CEP ?????-???,  Rio das Ostras,  Brazil}
\email{eduardoochs@gmail.com}

\end{document}

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