% (find-angg "LATEX/2015planar-has.tex")
% (find-angg ".emacs" "find-planarhas")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2015planar-has.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2015planar-has.pdf"))
% (defun e () (interactive) (find-LATEX "2015planar-has.tex"))
% (defun u () (interactive) (find-latex-upload-links "2015planar-has"))
% (find-xpdfpage "~/LATEX/2015planar-has.pdf")
% (find-sh0 "cp -v  ~/LATEX/2015planar-has.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2015planar-has.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2015planar-has.pdf
%               file:///tmp/2015planar-has.pdf
%           file:///tmp/pen/2015planar-has.pdf
% http://angg.twu.net/LATEX/2015planar-has.pdf
%
% This is practically a copy of:
%   (find-dn6 "tests/4.tex")
% slightly modified to use my macros in a more standard way.

\documentclass[oneside]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{indentfirst}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-angg "LATEX/edrxchars.tex")
%\input edrxheadfoot.tex          % (find-dn4ex "edrxheadfoot.tex")
%
% See: (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams

\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\pu{\directlua{pu()}}
\pu

% «.title-page»			(to "title-page")
% «.one-page-intro»		(to "one-page-intro")
% «.connectives»		(to "connectives")
% «.connectives-2»		(to "connectives-2")
% «.non-tautologies»		(to "non-tautologies")
% «.basic-definitions»		(to "basic-definitions")
% «.zhas-visually»		(to "zhas-visually")
% «.background-story»		(to "background-story")
% «.background-story-2»		(to "background-story-2")
% «.2-column-graphs»		(to "2-column-graphs")
% «.missing-digits»		(to "missing-digits")
% «.zhas-to-2col-graphs»	(to "zhas-to-2col-graphs")

% «.J-operators»		(to "J-operators")
% «.J-derived-rules»		(to "J-derived-rules")
% «.J-connectives»		(to "J-connectives")
% «.J-connectives-proofs»	(to "J-connectives-proofs")
% «.J-completeness»		(to "J-completeness")
% «.J-figure»			(to "J-figure")
% «.there-are-no-YL-cuts»	(to "there-are-no-YL-cuts")
% «.J-examples»			(to "J-examples")
% «.J-ops-diagrams»		(to "J-ops-diagrams")
% «.piccs»			(to "piccs")
% «.algebra-of-piccs»		(to "algebra-of-piccs")
% «.zquotients»			(to "zquotients")
% «.J-ops-algebra»		(to "J-ops-algebra")
% «.J-ops-algebra-2»		(to "J-ops-algebra-2")
% «.J-ops-algebra-3»		(to "J-ops-algebra-3")
% «.zquotients-poly»		(to "zquotients-poly")
% «.flipping»			(to "flipping")
% «.zquots-on-2colgs»		(to "zquots-on-2colgs")
% «.zquots-on-2colgs-2»		(to "zquots-on-2colgs-2")
% «.zquots-on-2colgs-3»		(to "zquots-on-2colgs-3")

% «.zsets-handouts»		(to "zsets-handouts")
% «.order-topologies»		(to "order-topologies")
% «.characteristic-functions»	(to "characteristic-functions")
% «.2-column-graphs»		(to "2-column-graphs")


% From: (find-LATEX "istanbuldefs.tex")
\catcode`¬=13 \def¬{\neg}
\catcode`±=13 \def±{\pm}
\catcode`·=13 \def·{\cdot}
\catcode`×=13 \def×{\times}
\catcode`λ=13 \defλ{\lambda}
\catcode`•=13 \def•{\bullet}
\catcode`↑=13 \def↑{\uparrow}
\catcode`→=13 \def→{\to}
\catcode`↓=13 \def↓{\downarrow}
\catcode`←=13 \def←{\leftarrow}
\catcode`↔=13 \def↔{\bij}
\catcode`↕=13 \def↕{\updownarrow}
\catcode`↖=13 \def↖{\nwarrow}
\catcode`↗=13 \def↗{\nearrow}
\catcode`↘=13 \def↘{\searrow}
\catcode`↙=13 \def↙{\swarrow}
\catcode`∀=13 \def∀{\forall}
\catcode`∃=13 \def∃{\exists}
\catcode`∈=13 \def∈{\in}
\catcode`∘=13 \def∘{\circ}
\catcode`∧=13 \def∧{\land}
\catcode`∨=13 \def∨{\lor}
\catcode`∩=13 \def∩{\cap}
\catcode`∪=13 \def∪{\cup}
\catcode`∼=13 \def∼{\sim}
\catcode`≡=13 \def≡{\equiv}
\catcode`≤=13 \def≤{\le}
\catcode`≥=13 \def≥{\ge}
\catcode`⊆=13 \def⊆{\subseteq}
\catcode`⊇=13 \def⊇{\supseteq}
\catcode`⊤=13 \def⊤{\top}
\catcode`⊥=13 \def⊥{\bot}
\catcode`⋄=13 \def⋄{\lozenge}
\catcode`⊣=13 \def⊣{\dashv}


% From: (find-LATEX "edrx15defs.tex")
\def\Set{\mathbf{Set}}
\def\Sets{\mathbf{Sets}}
\def\N{\mathbb{N}}
\def\R{\mathbb{R}}
\def\Z{\mathbb{Z}}
\def\BM{\mathsf{BM}}
\def\WM{\mathsf{WM}}
\def\LW{\mathsf{LW}}
\def\RW{\mathsf{RW}}
\def\ZS{\mathsf{ZS}}
\def\ZHA{\mathsf{ZHA}}
\def\St{\mathsf{St}}
\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\op{{\operatorname{op}}}
\def\bsl{\backslash}

% From: (find-LATEX "edrx15.sty")
\def\Opens{\mathcal{O}}
\def\ot{\leftarrow}
\def\bij{\leftrightarrow}

% From: (find-dn6file "tests/3.tex" "shorthand for matrices")
\def\mat #1{\begin       {matrix}#1\end{matrix}}
\def\pmat#1{\left (\begin{matrix}#1\end{matrix}\right)}
\def\bmat#1{\left [\begin{matrix}#1\end{matrix}\right]}
\def\cmat#1{\left\{\begin{matrix}#1\end{matrix}\right\}}
\def\sm #1{\begin       {smallmatrix}#1\end{smallmatrix}}
\def\psm#1{\left (\begin{smallmatrix}#1\end{smallmatrix}\right )}
\def\bsm#1{\left [\begin{smallmatrix}#1\end{smallmatrix}\right ]}
\def\csm#1{\left\{\begin{smallmatrix}#1\end{smallmatrix}\right\}}

\def\o#1{\mathop{\mathsf{#1}}}
\def\maxy{\o{maxy}}
\def\J   {\mathsf{J}}
\def\Mo  {\mathsf{Mo}}
\def\Mop {\mathsf{Mop}}
\def\Sand{\mathsf{Sand}}
\def\ECa {\mathsf{EC}{\&}}
\def\ECv {\mathsf{EC}{∨}}
\def\ECS {\mathsf{ECS}}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\Int{{\operatorname{int}}}

\def\NoLcuts{\mathsf{No}λ\mathsf{cuts}}
\def\NoYcuts{\mathsf{NoYcuts}}
\def\astarcube{{\&}^*\mathsf{Cube}}
\def\ostarcube{{∨}^*\mathsf{Cube}}
\def\istarcube{{→}^*\mathsf{Cube}}

\catcode`∧=13 \def∧{\mathop{\&}}


% (find-es "tex" "MaxMatrixCols")
\setcounter{MaxMatrixCols}{15}

\def\Set{\mathbf{Set}}
\def\Lan{\mathsf{Lan}}
\def\Ran{\mathsf{Ran}}

\def\scrC{\mathcal{C}}
\def\scrD{\mathcal{D}}
\def\E{\mathcal{E}}
\def\BF#1{\noindent{\bf#1}\quad}
\def\ton#1{\overset{#1}{\to}}

\def\co{\mathsf{co}}






%  _____ _ _   _
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/
%
% «title-page» (to ".title-page")

{\bf Intuitionistic Logic for Children, or:

Planar Heyting Algebras for Children}

\bigskip

Eduardo Ochs, 2015

eduardoochs@gmail.com

Version: 2015oct19a

\url{http://angg.twu.net/math-b.html\#zhas-for-children}

\url{http://angg.twu.net/LATEX/2015planar-has.pdf}

\bigskip

This is a work in progress...

It has a funny formatting because it is:

part seminar notes (for humanities people),

part handouts,

part a demo of dednat6,

part a draft for something more serious.

\bigskip

Also, the ``seminar notes'' format allowed me

to focus on examples and figures instead of

on formal definitions.

For more on archetypal examples, see:

\url{http://angg.twu.net/math-b.html#idarct}

\url{http://angg.twu.net/LATEX/idarct-preprint.pdf}

{\sl Feedback very welcome!}

\newpage





%   ___                                            _       _
%  / _ \ _ __   ___       _ __   __ _  __ _  ___  (_)_ __ | |_ _ __ ___
% | | | | '_ \ / _ \_____| '_ \ / _` |/ _` |/ _ \ | | '_ \| __| '__/ _ \
% | |_| | | | |  __/_____| |_) | (_| | (_| |  __/ | | | | | |_| | | (_) |
%  \___/|_| |_|\___|     | .__/ \__,_|\__, |\___| |_|_| |_|\__|_|  \___/
%                        |_|          |___/
%
% «one-page-intro» (to ".one-page-intro")

{\bf One page intro (to the main theorem)}

{

%R f = function (spec, def)
%R     local opts = {def=def, scale="12pt", meta="s"}
%R     local mp = mpnew(opts, spec):addlrs():addarrows("w"):output()
%R   end
%R f("1",             "zhaone")
%R f("1R",            "zhatwo")
%R f("1RL",           "zhatree")
%R f("12321L",        "zhaohouse")
%R f("12LRLRLR1",     "zhasquig")
%R f("123LLRR21",     "zhabigguill")
%R f("1234567654321", "zharect")
%R f("123RRR45R4321", "zharectcut")
%R f("123RRR43212R1", "zharectcutcut")
\pu

Each one of the posets below is a Heyting Algebra:
%
$$\zhaone
  \quad \zhatwo
  \quad \zhatree
  \quad \zhaohouse
  \quad \zhasquig
  \quad \zhabigguill
$$
%
$$\zharect
  \zharectcut
  \zharectcutcut
$$

}

The connectives `$\&$', `$∨$', `$→$' can be {\sl defined} by:

$$\def\o#1{\mathop{\mathsf{#1}}}
  \begin{array}{rcl}
  ab \;\&\; cd &:=& \o{min}(a,c)\o{min}(b,d) \\
  ab ∨ cd     &:=& \o{max}(a,c)\o{max}(b,d) \\
  P \to Q &:=& \begin{array}[t]{lll}
               \o{if}     & (P \o{below} Q)   & \o{then} ⊤           \\
               \o{elseif} & (P \o{leftof} Q)  & \o{then} \o{ne}(P\&Q) \\
               \o{elseif} & (P \o{rightof} Q) & \o{then} \o{nw}(P\&Q) \\
               \o{elseif} & (P \o{above} Q)   & \o{then} Q            \\
               \o{end}
               \end{array} \\
  \end{array}
$$

which are easy to interpret graphically - for example:
%
%R local PoQai, PnnP, QoRai =
%R     1/    T    \, 1/ T   \, 1/    T    \
%R      |   . .   |   |  .  |   |   . .   |
%R      |  . . .  |   | . . |   |  . . .  |
%R      | . o . i |   |d . n|   | . o . i |
%R      |. P . . .|   | P . |   |. Q . . .|
%R      | . . Q . |   \  F  /   | . . R . |
%R      |  . a .  |             |  . a .  |
%R      |   . .   |             |   . .   |
%R      \    F    /             \    F    /
%R local T = {a="(\\&)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R            T="·", F="·", T="⊤", F="⊥", }
%R PoQai:tozmp({def="PoQai", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="10pt", meta=nil}):addlrs():addcontour():output()
%
\pu
$$\PoQai \qquad \PnnP
  \qquad
  \begin{array}{rcl}
  (\&) &:=& P\&Q \\
  (∨) &:=& P∨Q \\
  (→) &:=& P→Q \\
  (¬) &:=& ¬P \\
  (¬¬) &:=& ¬¬P \\
  \end{array}
$$


\newpage

%   ____                            _   _
%  / ___|___  _ __  _ __   ___  ___| |_(_)_   _____  ___
% | |   / _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|
% | |__| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \
%  \____\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/
%
% «connectives» (to ".connectives")

{\bf Connectives (via brute force)}

The best way to see that the definitions

$$\def\o#1{\mathop{\mathsf{#1}}}
  \begin{array}{rcl}
  ab \;\&\; cd &:=& \o{min}(a,c)\o{min}(b,d) \\
  ab ∨ cd     &:=& \o{max}(a,c)\o{max}(b,d) \\
  P \to Q &:=& \begin{array}[t]{lll}
               \o{if}     & (P \o{below} Q)   & \o{then} ⊤           \\
               \o{elseif} & (P \o{leftof} Q)  & \o{then} \o{ne}(P\&Q) \\
               \o{elseif} & (P \o{rightof} Q) & \o{then} \o{nw}(P\&Q) \\
               \o{elseif} & (P \o{above} Q)   & \o{then} Q            \\
               \o{end}
               \end{array} \\
  \end{array}
$$

obey the expected properties, which are

$$
\begin{array}{rrcl}
∀P. & (P≤Q\&R) & ↔ & (P≤Q)\&(P≤R) \\
∀R. & (P{∨}Q≤R) & ↔ & (P≤R)\&(Q≤R) \\
∀P. & (P≤Q{→}R) & ↔ & (P\&Q≤R) \\
\end{array}
$$

is by brute force.

% (find-ist "-july.tex" "brute-force")

For example, in this case,
%
$$\lozfive \qquad \PoQai $$

we can do:

%R local pler, qler, poqler =
%R 1/    1    \, 1/    1    \, 1/    1    \
%R  |   1 1   |   |   1 1   |   |   1 1   |
%R  |  1 1 0  |   |  1 1 1  |   |  1 1 0  |
%R  | 1 1 0 0 |   | 0 1 1 1 |   | 0 1 0 0 |
%R  |0 1 0 0 0|   |0 0 1 1 0|   |0 0 0 0 0|
%R  | 0 0 0 0 |   | 0 0 1 0 |   | 0 0 0 0 |
%R  |  0 0 0  |   |  0 0 0  |   |  0 0 0  |
%R  |   0 0   |   |   0 0   |   |   0 0   |
%R  \    0    /   \    0    /   \    0    /
%R   pler:tozmp({def="pler",   scale="5pt", meta="s"}):addcells():output()
%R   qler:tozmp({def="qler",   scale="5pt", meta="s"}):addcells():output()
%R poqler:tozmp({def="poqler", scale="5pt", meta="s"}):addcells():output()
%L -- ∀R.  (P{∨}Q≤R) ↔ (P≤R)&(Q≤R)
%L ubs [[
%L   ∀R.\;   P 31 u ∨ Q 12 u Bin ? u ≤ R Bin \Poqler u ()
%L       ↔   P 31 u ≤ R Bin \Pler u ()   ∧  Q 21 u ≤ R Bin \Qler u () Bin   \Pleroqler u
%L       Bin Pre
%L   bruteforceor def   output
%L ]]
$$\pu
  \def\Pler{\sm{λR.(31≤R)       = \\ \pler}}
  \def\Qler{\sm{λR.(12≤R)       = \\ \qler}}
  \def\Pleroqler{\sm{λR.((31≤R)∧(12≤R)) = \\ \poqler}}
  \def\Poqler{\sm{
  % λR.(31{∨}12≤R) = \\
    λR.(?≤R) = \\
    λR.((31≤R)∧(12≤R)) = \\
    \poqler}}
  \bruteforceor
$$

we get $(31∨12)=$`?'$=32$.




\newpage

%   ____                            _   _                  ____
%  / ___|___  _ __  _ __   ___  ___| |_(_)_   _____  ___  |___ \
% | |   / _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|   __) |
% | |__| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \  / __/
%  \____\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/ |_____|
%
% «connectives-2» (to ".connectives-2")

{\bf Connectives (via brute force, 2)}

$$
\begin{array}{rrcl}
∀P. & (P≤Q\&R) & ↔ & (P≤Q)\&(P≤R) \\
% ∀R. & (P{∨}Q≤R) & ↔ & (P≤R)\&(Q≤R) \\
∀P. & (P≤Q{→}R) & ↔ & (P\&Q≤R) \\
\end{array}
$$

$$\lozfive \qquad \QoRai
$$

Here's how to calculate $31∧12$:
%
%R local pleq, pler, pleqar =
%R 1/    0    \, 1/    0    \, 1/    0    \
%R  |   0 0   |   |   0 0   |   |   0 0   |
%R  |  0 0 0  |   |  0 0 0  |   |  0 0 0  |
%R  | 0 0 0 0 |   | 0 0 0 0 |   | 0 0 0 0 |
%R  |0 1 0 0 0|   |0 0 0 0 0|   |0 0 0 0 0|
%R  | 1 1 0 0 |   | 0 0 1 0 |   | 0 0 0 0 |
%R  |  1 1 0  |   |  0 1 1  |   |  0 1 0  |
%R  |   1 1   |   |   1 1   |   |   1 1   |
%R  \    1    /   \    1    /   \    1    /
%R   pleq:tozmp({def="pleq",   scale="5pt", meta="s"}):addcells():output()
%R   pler:tozmp({def="pler",   scale="5pt", meta="s"}):addcells():output()
%R pleqar:tozmp({def="pleqar", scale="5pt", meta="s"}):addcells():output()
%L -- ∀P.  (P ≤ Q&R) ↔ (P≤Q) & (P≤R)
%L ubs [[
%L   ∀P.\;\; P ≤ Q 31 u ∧ R 12 u Bin ? u    Bin \Paqler u ()
%L       ↔   P ≤ Q 31 u Bin () \Pleq u   ∧
%L            P ≤ R 12  u Bin () \Pler u
%L            Bin \Pleqapler u
%L       Bin Pre
%L   bruteforceand def   output
%L ]]
$$\pu
  \def\Pleq{\sm{λP.(P≤31)       = \\ \pleq}}
  \def\Pler{\sm{λP.(P≤12)       = \\ \pler}}
  \def\Pleqapler{\sm{λP.((P≤31)∧(P≤12)) = \\ \pleqar}}
  \def\Paqler{\sm{
  % λR.(31{∨}12≤R) = \\
    λP.(P≤?) = \\
    λP.((P≤31)∧(P≤12)) = \\
    \pleqar}}
  \bruteforceand
$$

We get $(31∧12)=$`?'$=11$.

\medskip

Once we learn how to calculate `$∧$'s quickly,

we can calculate `$→$'s - they need $λP.(P∧Q)$:
%
%R local paq, paqler =
%R 2/        31        \, 1/    0    \
%R  |      31  31      |   |   0 0   |
%R  |    31  31  21    |   |  0 0 0  |
%R  |  31  31  21  11  |   | 0 0 0 1 |
%R  |30  31  21  11  01|   |0 0 0 1 1|
%R  |  30  21  11  01  |   | 0 0 1 1 |
%R  |    20  11  01    |   |  0 1 1  |
%R  |      10  01      |   |   1 1   |
%R  \        00        /   \    1    /
%R    paq:tozmp({def="paq",    scale="6pt", meta="s"}):addcells():output()
%R paqler:tozmp({def="paqler", scale="5pt", meta="s"}):addcells():output()
%L -- ∀P.  (P≤ Q→R) ↔ (P∧Q ≤ R)
%L ubs [[
%L   ∀P.\;\; P ≤ Q 31 u → R 12 u Bin ? u     Bin \Pleqir u ()
%L       ↔   P ∧ Q 31 u Bin \Paq u ≤ R 12 u  Bin \Paqler u ()
%L       Bin Pre
%L   bruteforceimp def   output
%L ]]
$$\pu
  \def\Paq   {\sm{λP.(P∧31)       = \\ \paq}}
  \def\Paqler{\sm{λP.((P∧31)≤12) = \\ \paqler}}
  \def\Pleqir{\sm{
  % λR.(31{∨}12≤R) = \\
    λP.(P≤?) = \\
    λP.((P∧31)≤12) = \\
    \paqler}}
  \bruteforceimp
$$


\newpage

%  _   _                   _              _        _             _           
% | \ | | ___  _ __       | |_ __ _ _   _| |_ ___ | | ___   __ _(_) ___  ___ 
% |  \| |/ _ \| '_ \ _____| __/ _` | | | | __/ _ \| |/ _ \ / _` | |/ _ \/ __|
% | |\  | (_) | | | |_____| || (_| | |_| | || (_) | | (_) | (_| | |  __/\__ \
% |_| \_|\___/|_| |_|      \__\__,_|\__,_|\__\___/|_|\___/ \__, |_|\___||___/
%                                                          |___/             
% «non-tautologies» (to ".non-tautologies")

{\bf Some non-tautologies}

Some propositions that are always true classically,

$$\mat{
P & ¬P & ¬¬P & (¬¬P)→P \\ \hline
0 &  1 &  0  &     1    \\
1 &  0 &  1  &     1    \\
}
$$
%
$$\mat{
P  & Q  & P∧Q  & ¬(P∧Q)  & ¬P & ¬Q  & ¬P∨¬Q  & ¬(P∧Q)→(¬P∨¬Q) \\ \hline
0  & 0  &  0   &     1    &  1 &  1  &   1    &        1         \\
0  & 1  &  0   &     1    &  1 &  0  &   1    &        1         \\
1  & 0  &  0   &     1    &  0 &  1  &   1    &        1         \\
1  & 1  &  1   &     0    &  0 &  0  &   0    &        1         \\
}
$$

\medskip

are not always true intuitionistically,

and we can use ZHAs to exhibit cases where they are not $⊤$:

%R local znotnotP =
%R 1/ T   \
%R  |  .  |
%R  | . c |
%R  |b . a|
%R  | P . |
%R  \  F  /
%R local T = {F="⊥", T="⊤", a="P'", b="P''", c="→"}
%R znotnotP:tozmp({def="znotnotP", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R local zdemorgan =
%R 1/ T   \
%R  |  o  |
%R  | . . |
%R  |q . p|
%R  | P Q |
%R  \  a  /
%R local T = {F="⊥", T="⊤", p="P'", q="Q'", a="∧", o="∨"}
%R zdemorgan:tozmp({def="zdemorgan", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse",    scale="10pt", meta=nil}):addlrs():output()

%L -- ¬¬P→P
%L ubs [[
%L ¬ ¬  P 10 u  Pre 02 u Pre 20 u ()  → P 10 u Bin 12 u
%L   notnotP def   output
%L ]]
%L
%L -- ¬(P∧Q)→(¬P∨¬Q)
%L ubs [[
%L   ¬ P 10 u ∧ Q 01 u Bin 00 u () Pre 32 u
%L   →   ¬ P 10 u Pre 02 u   ∨   ¬ Q 01 u Pre 20 u   Bin 22 u ()   Bin 22 u
%L   demorgan def   output
%L ]]
%L

$$\pu
  \begin{array}{ccccl}
  \ohouse && \znotnotP  && \mat{\notnotP} \\ \\
          && \zdemorgan && \mat{\demorgan} \\
  \end{array}
$$

\bigskip

I have {\sl some} material that helps in telling the full story -

classical and intuitionistic theorems and tautologies, for children -

and I will try to put it in the last section of these notes

as I typeset it for the seminars.



\newpage

%  ____            _            _       __
% | __ )  __ _ ___(_) ___    __| | ___ / _|___
% |  _ \ / _` / __| |/ __|  / _` |/ _ \ |_/ __|
% | |_) | (_| \__ \ | (__  | (_| |  __/  _\__ \
% |____/ \__,_|___/_|\___|  \__,_|\___|_| |___/
%
% «basic-definitions» (to ".basic-definitions")

{\bf Basic definitions.}

A {\sl ZSet} is a finite nonempty subset of $\N^2$ that touches boths axes.

The {\sl black moves} and the {\sl white moves} on a ZSet $A$ are defined as:
%
$$\begin{array}{rcl}
  \o{BM}(A) &:=& \setofst{((x,y),(x+dx,y-1))∈A^2}{dx∈\{-1,0,1\}} \\
  \o{WM}(A) &:=& \setofst{((x,y),(x+dx,y+1))∈A^2}{dx∈\{-1,0,1\}}
  \end{array}
$$

Mnemonic:
\par a black piece, `$\bullet$', is solid/heavy/wants to sink and move down;
\par a white piece, `$\circ$', is hollow/light/wants to float and move up.

Figure:

%R local B, W = 2/    bp    \, 2/wp  wp  wp\
%R               |  swsose  |   |  nwnone  |
%R               \bp  bp  bp/   \    wp    /
%R
%R local T = {bp="\\bullet", wp="\\circ",
%R            sw="↙", so="↓", se="↘",
%R            nw="↖", no="↑", ne="↗"}
%R B:tozmp({def="Bmne", scale="9pt", meta=nil}):addcells(T):output()
%R W:tozmp({def="Wmne", scale="9pt", meta=nil}):addcells(T):output()
$$\pu \Bmne \Wmne
$$

A {\sl ZDAG} is a graph of the form $(A, \BM(A))$ or $(A, \WM(A))$, and
\par A {\sl ZPoset} is a graph of the form $(A, \BM(A)^*)$ or $(A, \WM(A)^*)$,
\par where A is a ZSet, and $(A, R^*)$ is transitive-reflexive closure of $(A, R)$.

\medskip

We say that triple $(\o{maxy}, L, R)$ {\sl generates a ZHA} when:
\par 1) $\o{maxy}∈\N$, and $L$ and $R$ are functions from $\{0, 1, ..., \o{maxy}\}$ to $\N$,
\par 2) $L(y) ≤ R(y)$ always holds,
\par 3) $L(y+1) = L(1)\pm1$ and $R(y+1) = R(1)\pm1$ always hold,
\par 4) $L(0)=R(0)$ and $L(\o{maxy})=R(\o{maxy})$,
\par 5) $L(y)=0$ for some $y$.

\smallskip

The {\sl parity} of $(x,y)∈\N^2$ is the parity of $x+y$.

The {\sl left wall} and the {\sl right wall} of a ZHA are the sets
%
$$\begin{array}{rcl}
  \LW(\maxy,L,R) &:=& \setofst{(x,y)∈\N^2}{x=L(y)}, \\
  \RW(\maxy,L,R) &:=& \setofst{(x,y)∈\N^2}{x=R(y)}.
  \end{array}
$$

The {\sl ZSet generated by} $(\maxy,L,R)$, $\ZS(\maxy,L,R)$, is the set of all points
\par between $\LW(\maxy,L,R)$ and $\RW(\maxy,L,R)$ with the same parity as $(L(0),0)$.

The {\sl ZHA generated by} $(\maxy,L,R)$ is this ZPoset:
%
$$\ZHA(\maxy,L,R) \;:=\; (\ZS(\maxy,L,R), \WM(\ZS(\maxy,L,R))^*)$$

\medskip

We use the {\sl lr-coordinates} to refer to points of a ZHA.
\par The point $(L(0),0)$ is denoted by ``00''.
\par The $l$-coordinate increases when we walk northwest.
\par The $r$-coordinate increases when we walk northeast.


%$$\begin{array}{rcl}
  % \ZDAG(\maxy,L,R) &:=& (\ZS(\maxy,L,R), \WM(\ZS(\maxy,L,R)))
%   \ZHA(\maxy,L,R) &:=& (\ZS(\maxy,L,R), \WM(\ZS(\maxy,L,R))^*)
%  \end{array}
%$$


\newpage

%  ______   _    _                _                 _ _
% |__  / | | |  / \   ___  __   _(_)___ _   _  __ _| | |_   _
%   / /| |_| | / _ \ / __| \ \ / / / __| | | |/ _` | | | | | |
%  / /_|  _  |/ ___ \\__ \  \ V /| \__ \ |_| | (_| | | | |_| |
% /____|_| |_/_/   \_\___/   \_/ |_|___/\__,_|\__,_|_|_|\__, |
%                                                       |___/
% «zhas-visually» (to ".zhas-visually")
% (find-istfile "1.org" "ZHAs (formally) (2)")

{\bf ZHAs, visually}

%R local zhav =
%R 1/ o    \  -- L(9)=1 R(9)=1   maxy=9  L(maxy)=R(maxy)
%R  |o o   |
%R  | o    |
%R  |  o   |
%R  |   o  |
%R  |  o o |
%R  | o o o|
%R  |  o o |
%R  |   o o|  -- L(1)=3 R(1)=5
%R  \    o /  -- L(0)=4 R(0)=4   L(0)=R(0)=x_0=4
%R mp = zhav:tomp({def="zhav", scale="20pt", meta=nil}):addxys():addarrows("w")
%R mp:put(v(8,0), "L0", "L(0)=4")
%R local L = {[0]=4, 3, 2, 1, 2, 3, 2, 1, 0, 1}
%R local R = {[0]=4, 5, 4, 5, 4, 3, 2, 1, 0, 1}
%R local x = {L=8, R=10.5, a=13.5, b=16.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), "=", "\\maxy=9")
%R mp:put(v(x.a, 9), "=", "L(9)=R(9)")
%R mp:put(v(x.a, 0), "=", "L(0)=R(0)")
%R mp:output()

$$\pu
  \zhav
$$

\medskip

We say that triple $(\o{maxy}, L, R)$ {\sl generates a ZHA} when:
\par 1) $\o{maxy}∈\N$, and $L$ and $R$ are functions from $\{0, 1, ..., \o{maxy}\}$ to $\N$,
\par 2) $L(y) ≤ R(y)$ always holds,
\par 3) $L(y+1) = L(1)\pm1$ and $R(y+1) = R(1)\pm1$ always hold,
\par 4) $L(0)=R(0)$ and $L(\o{maxy})=R(\o{maxy})$,
\par 5) $L(y)=0$ for some $y$.

\smallskip

The {\sl parity} of $(x,y)∈\N^2$ is the parity of $x+y$.

The {\sl left wall} and the {\sl right wall} of a ZHA are the sets
%
$$\begin{array}{rcl}
  \LW(\maxy,L,R) &:=& \setofst{(x,y)∈\N^2}{x=L(y)}, \\
  \RW(\maxy,L,R) &:=& \setofst{(x,y)∈\N^2}{x=R(y)}.
  \end{array}
$$

The {\sl ZSet generated by} $(\maxy,L,R)$, $\ZS(\maxy,L,R)$, is the set of all points
\par between $\LW(\maxy,L,R)$ and $\RW(\maxy,L,R)$ with the same parity as $(L(0),0)$.

The {\sl ZHA generated by} $(\maxy,L,R)$ is this ZPoset:
%
$$\ZHA(\maxy,L,R) \;:=\; (\ZS(\maxy,L,R), \WM(\ZS(\maxy,L,R))^*)$$

\newpage



%  ____             _                                   _
% | __ )  __ _  ___| | ____ _ _ __ ___  _   _ _ __   __| |
% |  _ \ / _` |/ __| |/ / _` | '__/ _ \| | | | '_ \ / _` |
% | |_) | (_| | (__|   < (_| | | | (_) | |_| | | | | (_| |
% |____/ \__,_|\___|_|\_\__, |_|  \___/ \__,_|_| |_|\__,_|
%                       |___/
%
% «background-story» (to ".background-story")

{\bf Background story.}

Several years ago I was looking for finite, easy-to-draw Heyting Algebras,
\par because I was trying to understand sheaves, and I had no intuition at all
\par about what those ``closure operators'' were doing...
\par When I tried to generate Heyting Algebras from order topologies -
\par if $D=(A,R)$ is a DAG, then $D':=(\Opens(A), ⊆)$ is a Heyting Algebra -
\par the results had very regular shapes, and were often planar.

For example:

%R local house, ohouse = 2/  #1  \, 7/       !h11111                     \
%R                        |#2  #3|   |              !h01111              |
%R                        \#4  #5/   |       !h01011       !h00111       |
%R                                   |!h01010       !h00011       !h00101|
%R                                   |       !h00010       !h00001       |
%R                                   \              !h00000              /
%R  house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt",   meta="s"}):addcells():output()
%R  house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R  house:tomp({def="zdagHouse",      scale="15pt",  meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse",     scale="25pt",  meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse",    scale="12pt",  meta="s"}):addlrs():addarrows("w"):output()

%R local guill, oguill = 2/  #1  #2\, 8/                !g111111                \
%R                        |#3  #4  |   |        !g101111        !g011111        |
%R                        \  #5  #6/   |                !g001111        !g010111|
%R                                     |        !g001011        !g000111        |
%R                                     |!g001010        !g000011                |
%R                                     |        !g000010        !g000001        |
%R                                     \                !g000000                /
%R  guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R  guill:tomp({def="zdagGuill",    scale="7pt", meta="t"}):addbullets():addarrows():output()
%R  guill:tomp({def="zdagGuill",    scale="13pt",  meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill",   scale="25pt",  meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill",  scale="12pt",  meta="s"}):addlrs():addarrows():output()
%R
{\pu
$$
  \def\h{\zfHouse}
  H = \zdagHouse
  \qquad
  H' (\Opens(H), ⊆) = \zdagOHouse
$$

$$
  \def\g{\zfGuill}
  G = \zdagGuill
  \qquad
  G' (\Opens(G), ⊆) = \zdagOGuill
$$
}

\newpage

%  ____             _                                   _   ____
% | __ )  __ _  ___| | ____ _ _ __ ___  _   _ _ __   __| | |___ \
% |  _ \ / _` |/ __| |/ / _` | '__/ _ \| | | | '_ \ / _` |   __) |
% | |_) | (_| | (__|   < (_| | | | (_) | |_| | | | | (_| |  / __/
% |____/ \__,_|\___|_|\_\__, |_|  \___/ \__,_|_| |_|\__,_| |_____|
%                       |___/
%
% «background-story-2» (to ".background-story-2")

{\bf Background story, 2: planarity, `$↓$'}

%R local w, womit, W =
%R 2/#1  #2  #3\, 2/    a     \, 7/              !w11111              \
%R  \  #4  #5  /   |  b c d   |   |       !w11011!w10111!w01111       |
%R                 |  e f g   |   |       !w10011!w01011!w00111       |
%R                 |h   i   j |   |!w10010       !w00011       !w00101|
%R                 |  k   l   |   |       !w00010       !w00001       |
%R                 \    m     /   \              !w00000              /
%R w:tomp({def="zfW#1#2#3#4#5", scale="3.5pt", meta="s"}):addcells():output()
%R w:tomp({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW",  scale="13pt", meta=nil}):addbullets():addarrows() :output()
%R -- W:tomp({def="zdagOW", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R -- local omit = function (_, _, vdx) return vdx=="(2,4)0" end
%R -- W:tomp({def="zdagOW", scale="25pt", meta=nil}):addcells():addarrowsexcept("w", omit):output()
%R W:tomp({def="zdagOW", scale="25pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()



\pu

Everytime that I started with a DAG $D$ with three independent points

then $D'$ would contain a cube, and would be non-planar. For example:
%
$$
  \def\w{\zfW}
  W = \zdagW
  \qquad
  W' = (\Opens(W), ⊆) = \zdagOW
$$

Everytime that I started with a ``thin'' DAG $D$ - ``thin'' meaning

``does not have three independent points'' - then $D'$ would be planar.

\bigskip

It turns out that we can always recover $D$ from $D'$.

For $C⊆D$ let $↓C$ be the smallest down-set of $D$ containing $C$.

For $d⊆D$ let $↓d$ be the smallest down-set of $D$ containing $\{d\}$.

The map
%
$$\begin{array}{rrcl}
  ↓: & D &    \to& D' \\
      & d &\mapsto& ↓d \\
  \end{array}
$$

is always a (contra-variant) embedding of $D$ into $D'$, and its image

is exactly the set of points of $D'$ with exactly one arrow coming in:
%
$$
  \def\w{\zfW}
  \zdagW
  \qquad
  \diagxyto/-->/<250>
  \qquad
  \zfWbig {\w10010} {\w01011} {\w00101}
                {\w00010} {\w00001}
$$

% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ 10 118) "5.12 Birkhoff's representation theorem.")
% (find-daveypriestleytext (+ 10 118) "5.12 Birkhoff's representation theorem.")

The isomorphism between $↓D⊆D'$ and $D^\op$ is (part of)

{\sl Birkhoff's representation theorem for finite distributive lattices} -

See Davey \& Priestley's ``Introduction to Lattices and Order (2nd ed)'',

pages 116-118, for its properties.





\newpage

%  ____                 _                         _
% |___ \       ___ ___ | |   __ _ _ __ __ _ _ __ | |__  ___
%   __) |____ / __/ _ \| |  / _` | '__/ _` | '_ \| '_ \/ __|
%  / __/_____| (_| (_) | | | (_| | | | (_| | |_) | | | \__ \
% |_____|     \___\___/|_|  \__, |_|  \__,_| .__/|_| |_|___/
%                           |___/          |_|
%
% «2-column-graphs» (to ".2-column-graphs")

{\bf 2-Column graphs}

%D diagram piles0
%L drawtwocolgraph(30, -15, 4, 6, "13 42", "45")
%D enddiagram

This is a {\sl 2-column graph},
and our short notation for it:

$$\pu \left(\diag{piles0}\right)
  ≡
  \left(
  4, 6, \cmat{\ltor42, \\ \ltor13}, \cmat{\lotr45}
  \right)
$$

\bigskip

%R local threefour = 2/    #4\
%R                    |#1  #5|
%R                    |#2  #6|
%R                    \#3  #7/
%R threefour:tomp({def="zfthreefour#1#2#3#4#5#6#7", scale="5pt", meta="s p"}):addcells():output()

\pu

This is a {\sl 2-pile}, and our short notation for it:
%
% (find-istfile "-july.tex" "ThreeFour")
%
$$\zfthreefour0010111 ≡ 13$$

Note that the `1' and `3' tell only the number of `1's

in each column; the total heights are omitted.

%D diagram bigthingc
%L -- drawtwocolgraph(30, -15, 4, 6, "13 42", "45")
%L -- drawtwocolgraph(30, -15, 4, 6, "32", "15 26")
%L drawtwocolgraph(30, -15, 4, 5, "32", "14 25")
%D enddiagram

%L z = LR.fromtwocolgraph(4, 6, "13 42", "45"):zha()
%L z = LR.fromtwocolgraph(4, 6, "32", "15 26"):zha()
%L z = LR.fromtwocolgraph(4, 5, "32", "14 25"):zha()
%L MixedPicture.new({def="bigthingc", scale="25pt", meta=nil}, z):addgens():addarrows("w")
%L MixedPicture.new({def="bigthingc", scale="20pt", meta=nil}, z):addgens():addarrows("w"):output()
%L MixedPicture.new({def="bigthingd", scale="12pt", meta="s"}, z):addgens():addarrows("w"):output()
%L MixedPicture.new({def="bigthinge", scale="10pt", meta=nil}, z):addlrs():output()

\pu

$$D ≡ \left(\diag{bigthingc}\right)
  \qquad
  (\Opens(D), ⊆) ≡ \bigthingc
$$


\newpage


%  __  __ _         _                   _ _       _ _
% |  \/  (_)___ ___(_)_ __   __ _    __| (_) __ _(_) |_ ___
% | |\/| | / __/ __| | '_ \ / _` |  / _` | |/ _` | | __/ __|
% | |  | | \__ \__ \ | | | | (_| | | (_| | | (_| | | |_\__ \
% |_|  |_|_|___/___/_|_| |_|\__, |  \__,_|_|\__, |_|\__|___/
%                           |___/           |___/
%
% «missing-digits» (to ".missing-digits")

{\bf Missing digits}

The {\sl generators} of a ZHA are the points with exactly one arrow coming in.

%R local leftgen, rightgen = 2/wp  \, 2/  wp\
%R                            \  nw/   \ne  /
%R local T = {bp="\\bullet", wp="\\circ",
%R            sw="↙", so="↓", se="↘",
%R            nw="↖", no="↑", ne="↗"}
%R leftgen :tozmp({def="leftgen",  scale="5pt", meta="s"}):addcells(T):output()
%R rightgen:tozmp({def="rightgen", scale="5pt", meta="s"}):addcells(T):output()
\pu

The {\sl left generators} are the ones of the form `$\leftgen$'.

The {\sl right generators} are the ones of the form `$\rightgen$'.

\medskip

%R local fourfive = 2/    #5\
%R                   |#1  #6|
%R                   |#2  #7|
%R                   |#3  #8|
%R                   \#4  #9/
%R fourfive:tomp({def="fourfive#1#2#3#4#5#6#7#8#9", scale="5pt", meta="s p"}):addcells():output()
\pu

Let $C$ be a 2-column graph, and $C' := (\Opens(C), ⊆)$ (a ZHA).

The inclusion $↓:C→C'$ takes the

left column of $C$ to the left generators of $C'$, and the

right column of $C$ to the right generators of $C'$, and the

Example:
%
$$D ≡ \left(\diag{bigthingc}\right)
  \qquad
  (\Opens(D), ⊆) ≡ \bigthingd
$$

To obtain the ``missing digits'' in $1\_, 2\_, \ldots, \_1, \_2, \ldots$ we can do:
%
$$
  \def\ff{\fourfive}
  \begin{array}{cc}
                                              & ↓\_5 = ↓\ff0000 11111 = \ff0011 11111 = 25 \\[10pt]
  ↓4\_ = ↓\ff1111 00000 = \ff1111 00011 = 42 & ↓\_4 = ↓\ff0000 01111 = \ff0001 01111 = 14 \\[10pt]
  ↓3\_ = ↓\ff0111 00000 = \ff0111 00011 = 32 & ↓\_3 = ↓\ff0000 00111 = \ff0000 00111 = 03 \\[10pt]
  ↓2\_ = ↓\ff0011 00000 = \ff0011 00000 = 20 & ↓\_2 = ↓\ff0000 00011 = \ff0000 00011 = 02 \\[10pt]
  ↓1\_ = ↓\ff0001 00000 = \ff0001 00000 = 10 & ↓\_1 = ↓\ff0000 00001 = \ff0000 00001 = 01 \\
  \end{array}
$$

Once we draw $1\_≡10$, $2\_≡10$, $3\_≡32$, $\ldots$ in the $lr$-plane,

drawing the rest of the ZHA is automatic.

$$\bigthinge$$


\newpage

%  ______   _    _          _          ____                 _
% |__  / | | |  / \   ___  | |_ ___   |___ \       ___ ___ | |
%   / /| |_| | / _ \ / __| | __/ _ \    __) |____ / __/ _ \| |
%  / /_|  _  |/ ___ \\__ \ | || (_) |  / __/_____| (_| (_) | |
% /____|_| |_/_/   \_\___/  \__\___/  |_____|     \___\___/|_|
%
% «zhas-to-2col-graphs» (to ".zhas-to-2col-graphs")

{\bf From ZHAs to 2-column graphs}

Here's how to go in the opposite direction.

Starting from a ZHA $H$, write its generators in two columns.

The leftmost and righmost digits increase in unit steps always,

but the middle digits correspond to the ``missing digits'' we discussed before.

Starting from the bottom of each of the two columns,

look at when the ``missing''/``middle'' digit changes.

Each one of these ``generators after change'' becomes an arrow

in the 2-column graph C.


%D diagram zha-to-2col-graph
%D 2Dx     100 +55 +45 +60
%D 2D  100 \aa \bb \cc \dd
%D 2D
%D 2D  +45             \ee
%D 2D
%D (( \aa \bb --> \bb \cc --> \cc \dd --> \dd \ee -->
%D
%D ))
%D enddiagram
%D
\pu
$$\def\aa{\bigthinge}
  \def\bb{\begin{array}{rcl}
         & 25 \\
      42 & 14 \\
      32 & 03 \\
      30 & 02 \\
      10 & 01 \\
    \end{array}}
  \def\cc{\begin{array}{rcl}
         & 25 \\
      32 & 14 \\
    \end{array}}
  \def\dd{\begin{array}{rcl}
              & \lotr25 \\
      \ltor32 & \lotr14 \\
    \end{array}}
  \def\ee{\left(4, 5, \cmat{\ltor32}, \cmat{\lotr25, \\ \lotr14}\right)}
  %
  \diag{zha-to-2col-graph}
$$






\newpage

{\bf Part 2:

J-operators and ZQuotients}

(For older children)

\medskip

J-operators are a basic tool for constructing

{\sl sheaves} and for moving back and forth

between different logics...

But we will not see the categorical part here.


\newpage




%      _                                  _
%     | |       ___  _ __   ___ _ __ __ _| |_ ___  _ __ ___
%  _  | |_____ / _ \| '_ \ / _ \ '__/ _` | __/ _ \| '__/ __|
% | |_| |_____| (_) | |_) |  __/ | | (_| | || (_) | |  \__ \
%  \___/       \___/| .__/ \___|_|  \__,_|\__\___/|_|  |___/
%                   |_|
%
% «J-operators» (to ".J-operators")

% (find-istfile "1.org" "What is axiom M3? Monotonicity (2)")
% (find-istfile "1.org" "** DONE The sandwich lemma")
% (find-angg "LATEX/istanbulquotes.tex")
% (find-angg "LATEX/istanbulquotes.tex" "fourman")

{\bf J-operators}

\catcode`∧=13 \def∧{\mathop{\&}}

A {\sl J-operator} on a Heyting Algebra $H$ is a function $J:H→H$,
\par that obeys the three axioms below.
\par We usually write $J$ as $·^*:H→H$, and write the axioms as rules.
%
%L addabbrevs("&", "\\&", "vv", "∨", "->", "→")
%L addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
%:
%:    -----\J1    ------\J2    ------------\J3
%:    P<=P!       P!=P!!       (P&Q)!=P!&Q!
%:
%:    ^J1         ^J2          ^J3
%:
\pu
$$\ded{J1} \qquad \ded{J2} \qquad \ded{J3}$$
\par $\J1$ says that the operation $·^*$ is increasing.
\par $\J2$ says that the operation $·^*$ is idempotent.
\par $\J3$ is something mysterious (for now).

\medskip

A J-operator induces an equivalence relation and equivalence classes:
%
$$\begin{array}{rcl}
  P∼Q  &\text{iff}& P^*=Q^* \\ \relax
  [P]^* &:=&         \setofst{Q∈H}{P^*=Q^*} \\
  \end{array}
$$

We will use the interval notation,
%
$$[P,R] := \setofst{Q∈H}{P≤Q≤R}$$

to denote all truth-values between P and R (inclusive).

\medskip

The proofs in the next pages will show that every
\par equivalence class is closed by `$\&$', `$∨$', and ``sandwiching''.
\par For example, if 42, 33, and 14 belong to
\par the same equivalence class, $E$, then:
%
$$
  \begin{array}{c}
  44 = 42∨33∨14 ∈ E  \\
  12 = 42∧33∧14 ∈ E  \\ \relax
  [12, 44] = [42∧33∧14, 42∨33∨14] ⊆ E
  \end{array}
$$
%
%R local ra =
%R 2/          ..        \
%R  |        ..  ..      |
%R  |      ..  ..  ..    |
%R  |    ..  ..  ..  ..  |
%R  |      ..  ..  ..  ..|
%R  |        ..  ..  ..  |
%R  |      ..  44  ..  ..|
%R  |    ..  **  **  ..  |
%R  |  ..  42  33  **    |
%R  |..  ..  **  **  14  |
%R  |  ..  ..  **  **  ..|
%R  |    ..  ..  12  ..  |
%R  |      ..  ..  ..    |
%R  |        ..  ..      |
%R  \          ..        /
%R ra:tozmp({def="ra"}):addcells():addcontour():output()
$$\pu \ra$$

Moreover, if $E=\{Q_1, \ldots, Q_n\}$
\par then $Q_1∧\ldots∧Q_n∈E$ and $Q_1∨\ldots∨Q_n∈E$,
\par and $E=[Q_1∧\ldots∧Q_n, Q_1∨\ldots∨Q_n]$.

\newpage

%      _       _           _               _              _
%     | |   __| | ___ _ __(_)_   _____  __| |  _ __ _   _| | ___  ___
%  _  | |  / _` |/ _ \ '__| \ \ / / _ \/ _` | | '__| | | | |/ _ \/ __|
% | |_| | | (_| |  __/ |  | |\ V /  __/ (_| | | |  | |_| | |  __/\__ \
%  \___/   \__,_|\___|_|  |_| \_/ \___|\__,_| |_|   \__,_|_|\___||___/
%
% «J-derived-rules» (to ".J-derived-rules")

{\bf Derived rules}

All the rules below,

\smallskip

{\sl Monotonicity}: $P≤Q$ implies $P^*≤Q^*$,

{\sl Sandwich lemma}: all truth values between $P$ and $P^*$ are equivalent,

$\ECa$, $\ECv$, $\ECS$: equivalence classes are closed by `$\&$', `$∨$', and sandwiching,

\smallskip

are consequences of just the Heyting Algebra rules plus $\J1$, $\J2$, $\J3$.
%:
%:                         ------------\J3   ---------
%:                         (P&Q)!=P!&Q!      P!&Q!<=Q!
%:   ----------\Mop  :=    ---------------------------
%:   (P&Q)!<=Q!            (P&Q)!<=Q!
%:
%:   ^Mop1                 ^Mop2
%:
%:                  P<=Q
%:                  =====
%:                  P=P&Q
%:                  ---------  ----------\Mop
%:   P<=Q           P!=(P&Q)!  (P&Q)!<=Q!
%:   ------\Mo  :=  ---------------------
%:   P!<=Q!                 P!<=Q!
%:
%:   ^Mo1                   ^Mo2
%:
%:                                  Q<=P!
%:                                  -------\Mo  ------\J2
%:                        P<=Q      Q!<=P!!     P!!=P!
%:                       ------Mo   ------------------
%:   P<=Q<=P!            P!<=Q!            Q!<=P!
%:   --------\Sand  :=   ------------------------
%:     P!=Q!                   P!=Q!
%:
%:     ^Sand1                  ^Sand2
%:
%:
%:                          P!=Q!
%:                          ===========   ------------\J3
%:   P!=Q!                  P!=Q!=P!&Q!   P!&Q!=(P&Q)!
%:   ------------\ECa  :=   --------------------------
%:   P!=Q!=(P&Q)!                 P!=Q!=(P&Q)!
%:
%:   ^ECa1                        ^ECa2
%:                                                            P!=Q!
%:                                                  -----\J1  -----
%:                                                  Q<=Q!     Q!=P!
%:                                        -----\J1  ---------------
%:                                        P<=P!         Q<=P!
%:                               -------  -------------------
%:                               P<=PvvQ     PvvQ<=P!
%:                               --------------------
%:                                  P<=PvvQ<=P!
%:                                  -----------\Sand
%:   P!=Q!                  P!=Q!   P!=(PvvQ)!
%:   ------------\ECv  :=   ------------------
%:   P!=Q!=(PvvQ)!            P!=Q!=(PvvQ)!
%:
%:   ^ECv1                       ^ECv2
%:
%:                                       P!=R!
%:                            -----\J1   -----
%:                   P<=Q<=R  R<=R!      R!=P!
%:                   -------------------------
%:                           P<=Q<=P!
%:                           --------\Sand
%:   P<=Q<=R  P!=R!           P!=Q!         P!=R!
%:   --------------\ECS  :=   -------------------
%:     P!=Q!=R!                 P!=Q!=R!
%:
%:     ^ECS1                    ^ECS2
%:
\pu
$$\begin{array}{rcl}
  \ded{Mop1}  &:=& \ded{Mop2}  \\ \\
  \ded{Mo1}   &:=& \ded{Mo2}   \\ \\
  \ded{Sand1} &:=& \ded{Sand2} \\ \\
  \ded{ECa1}  &:=& \ded{ECa2}  \\
  \ded{ECv1}  &:=& \ded{ECv2}  \\ \\
  \ded{ECS1}  &:=& \ded{ECS2}  \\
  \end{array}
$$


(Todo: use these rules to prove the figure in the previous page.)

\newpage

%      _                                   _   _
%     | |   ___ ___  _ __  _ __   ___  ___| |_(_)_   _____  ___
%  _  | |  / __/ _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|
% | |_| | | (_| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \
%  \___/   \___\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/
%
% «J-connectives» (to ".J-connectives")

{\bf How J-operators interact with the connectives}

{
\def∧{{\&}}
\def∨{{\lor}}
\def→{{\to}}

For the next result about how J-operators divide a ZHA

into equivalence classes we need one of the facts that

will be proved below - one arrow of the cubes.

\medskip

The implications in the cubes below
%
%D diagram cube-and*-0
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P^*∧Q^*)^*
%D ren  A2 A3 A4   ==>  (P∧Q^*)^* P^*∧Q^*  (P^*∧Q)^*
%D ren  A5 A6 A7   ==>   P∧Q^*     (P∧Q)^*  P^*∧Q
%D ren     A8      ==>              P∧Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-or*-0
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P^*∨Q^*)^*
%D ren  A2 A3 A4   ==>  (P∨Q^*)^* P^*∨Q^*  (P^*∨Q)^*
%D ren  A5 A6 A7   ==>   P∨Q^*     (P∨Q)^*  P^*∨Q
%D ren     A8      ==>              P∨Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-imp*-0
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P→Q^*)^*
%D ren  A2 A3 A4   ==>  (P^*→Q^*)^*   P→Q^*  (P→Q)^*
%D ren  A5 A6 A7   ==>   P^*→Q^*   (P^*→Q)^*  P→Q
%D ren     A8      ==>              P^*→Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
\pu
$$
  \diag{cube-and*-0}
  \quad
  \diag{cube-or*-0}
  \quad
  \diag{cube-imp*-0}
$$

can be proved easily using just $\Mo$ plus the derived HA rules

that say that `$∧$', `$∨$', `$→$' are functorial.

\medskip

If we add the arrows corresponding to the proofs below

(that are done explicitly in the next page),
%:
%:   =====================   ==================   ====================
%:   (P!&Q!)!=P!&Q!=(P&Q)!   (P!vvQ!)!<=(PvvQ)!   (P->Q^*)^*<=P^*->Q^*
%:
%:   ^and*-extra-arrow       ^or*-extra-arrow     ^imp*-extra-arrow
%:
%:
%:      ------\J2   ------\J2
%:      P!!=P!      Q!!=Q!
%:   =============================\J3
%:   (P!&Q!)!=P!!&Q!!=P!&Q!=(P&Q)!
%:   -----------------------------
%:      (P!&Q!)!=P!&Q!=(P&Q)!
%:
%:      ^and*-extra-arrow-proof
%:
%:                                     -------------
%:                                     P->Q^*<=P->Q^*
%:      ------            -------      ---------------
%:      P<=PvvQ           Q<=PvvQ      (P->Q^*)&P<=Q^*
%:   ------------\Mo -----------\Mo    -------------------\Mo
%:   P!<=(PvvQ)!     Q!<=(PvvQ)!       ((P->Q^*)&P)^*<=Q!!
%:   ---------------------------       -------------------\J2
%:        P!vvQ!<=(PvvQ)!              ((P->Q^*)&P)^*<=Q^*
%:     -------------------\Mo          -------------------\J3
%:     (P!vvQ!)!<=(PvvQ)!!             (P->Q^*)^*&P^*<=Q^*
%:     -------------------\J2          -------------------
%:      (P!vvQ!)!<=(PvvQ)!             (P->Q^*)^*<=P^*->Q^*
%:
%:      ^or*-extra-arrow-proof         ^imp*-extra-arrow-proof
%:
%:
\pu

$$\ded{and*-extra-arrow}$$

$$\ded{or*-extra-arrow} \qquad \ded{imp*-extra-arrow}$$

the partial orders on the cubes becomes

(equivalent to the one generated by) this:
%
%D diagram cube-and*-2
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P^*∧Q^*)^*
%D ren  A2 A3 A4   ==>  (P∧Q^*)^* P^*∧Q^*  (P^*∧Q)^*
%D ren  A5 A6 A7   ==>   P∧Q^*     (P∧Q)^*  P^*∧Q
%D ren     A8      ==>              P∧Q
%D
%D (( A1 A2  = A1 A3  = A1 A4  =
%D    A2 A5 <- A2 A6  = A3 A5 <- A3 A7 <- A4 A6  = A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-or*-1
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P^*∨Q^*)^*
%D ren  A2 A3 A4   ==>  (P∨Q^*)^* P^*∨Q^*  (P^*∨Q)^*
%D ren  A5 A6 A7   ==>   P∨Q^*     (P∨Q)^*  P^*∨Q
%D ren     A8      ==>              P∨Q
%D
%D (( A1 A2  = A1 A3 <- A1 A4  =
%D    A2 A5 <- A2 A6  = A3 A5 <- A3 A7 <- A4 A6  = A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-imp*-1
%D 2Dx     100 +30 +30
%D 2D  100     A1
%D 2D  +25 A2  A3  A4
%D 2D  +25 A5  A6  A7
%D 2D  +25     A8
%D 2D
%D ren     A1      ==>            (P→Q^*)^*
%D ren  A2 A3 A4   ==>  (P^*→Q^*)^*   P→Q^*  (P→Q)^*
%D ren  A5 A6 A7   ==>   P^*→Q^*   (P^*→Q)^*  P→Q
%D ren     A8      ==>              P^*→Q
%D
%D (( A1 A2  = A1 A3  = A1 A4 <-
%D    A2 A5  = A2 A6 <- A3 A5  = A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
\pu
$$
  \diag{cube-and*-2}
  \quad
  \diag{cube-or*-1}
  \quad
  \diag{cube-imp*-1}
$$

We will call the cubes above, and the rules coming from them,

the $\astarcube$, $\ostarcube$, and $\istarcube$,

\newpage

%      _                                   _   _                  ____
%     | |   ___ ___  _ __  _ __   ___  ___| |_(_)_   _____  ___  |___ \
%  _  | |  / __/ _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|   __) |
% | |_| | | (_| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \  / __/
%  \___/   \___\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/ |_____|
%
% «J-connectives-proofs» (to ".J-connectives-proofs")

{\bf How J-operators interact with the connectives: proofs}

$$
  \diag{cube-and*-0}
  \quad
  \diag{cube-or*-0}
  \quad
  \diag{cube-imp*-0}
$$

plus:

$$\ded{and*-extra-arrow-proof}$$
$$\ded{or*-extra-arrow-proof} \qquad \ded{imp*-extra-arrow-proof}$$

yields:

$$
  \diag{cube-and*-2}
  \quad
  \diag{cube-or*-1}
  \quad
  \diag{cube-imp*-1}
$$

\newpage

%      _                             _      _
%     | |   ___ ___  _ __ ___  _ __ | | ___| |_ ___ _ __   ___  ___ ___
%  _  | |  / __/ _ \| '_ ` _ \| '_ \| |/ _ \ __/ _ \ '_ \ / _ \/ __/ __|
% | |_| | | (_| (_) | | | | | | |_) | |  __/ ||  __/ | | |  __/\__ \__ \
%  \___/   \___\___/|_| |_| |_| .__/|_|\___|\__\___|_| |_|\___||___/___/
%                             |_|
%
% «J-completeness» (to ".J-completeness")

{\bf How J-operators interact with the connectives: completeness}

Take a 4-uple $(H,J,P,Q)$ made of a Heyting Algebra,
\par a J-operator on it, and two truth-values $P, Q ∈ H$.
\par The arrows in $\astarcube$, $\ostarcube$, $\istarcube$ are {\sl theorems},
\par so they are true on all `$(H,J,P,Q)$'s.
\par Take an arrow that is not in the cubes -- for example, $P^*∨Q^*≤(P∨Q)^*$.
\par Maybe it is true in all `$(H,J,P,Q)$'s.
\par Maybe it is a theorem, that we forgot to prove.
\par Maybe our cubes are {\sl incomplete}.

\medskip

They {\sl are} complete, though.

\medskip

Here is a way to:
\par 1) prove that the arrows in the cubes are the only theorems,
\par 2) exhibit countermodels for all arrows not in the cubes,
\par 3) remember which arrows are and are not in the cubes.
\par We just need one model for each of the cubes/connectives.

\medskip

It is in the next page.

\newpage

%      _    __ _
%     | |  / _(_) __ _ _   _ _ __ ___
%  _  | | | |_| |/ _` | | | | '__/ _ \
% | |_| | |  _| | (_| | |_| | | |  __/
%  \___/  |_| |_|\__, |\__,_|_|  \___|
%                |___/
%
% «J-figure» (to ".J-figure")

{\bf How J-operators interact with the connectives: figure}

%L -- The (v*) cube
%L mp = mpnew({def="orStarCubeArchetypal"}, "12321L"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*"):output()
%L
%L -- The (&*) cube
%L mp = mpnew({def="andStarCubeArchetypal"}, "12321"):addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*"):output()
%L
%L -- The (->*) cube
%L mp = mpnew({def="impStarCubeArchetypal"}, "12321"):addcuts("c 2/10 01|2")
%L mp:put(v"10", "P")
%L mp:put(v"00", "Q"):output()
\pu

$$\begin{array}{ccl}
  \diag{cube-and*-2} & \andStarCubeArchetypal \\ \\
  \diag{cube-or*-1}  & \orStarCubeArchetypal \\ \\
  \diag{cube-imp*-1} & \impStarCubeArchetypal \\
  \end{array}
$$


}


\newpage

%  _   _        __   __             _
% | \ | | ___   \ \ / /   ___ _   _| |_ ___
% |  \| |/ _ \   \ V /   / __| | | | __/ __|
% | |\  | (_) |   | |   | (__| |_| | |_\__ \
% |_| \_|\___/    |_|    \___|\__,_|\__|___/
%
% «there-are-no-YL-cuts» (to ".there-are-no-YL-cuts")
{\bf There are Y-cuts or $λ$-cuts}

We saw that the equivalence classes of a J-operator are {\sl intervals} -

i.e., lozenges, except maybe for dents coming from irregular

contours of ZHAs, like:
%
%R -- (find-ist "-july.tex" "zquotients")
%R local zquo =
%R 2/    46    \
%R  |  45  46  |
%R  |    45  46|
%R  |  45  45  |
%R  |    45    |
%R  |  23  45  |
%R  |23  23  04|
%R  |  23  03  |
%R  |23  03    |
%R  |  03      |
%R  \00        /
%R zquo:tozmp({def="zquoa"}):addlrs():output()
%R zquo:tozmp({def="zquob"}):addcells():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
  \zquoa
  \qquad \diagxyto/-->/<250> \qquad
  \zquob
$$

From what we know now this may be a J-operator:
%
%R local badJ =
%R 2/            66            \
%R  |          66  66          |
%R  |        66  66  46        |
%R  |      66  66  46  46      |
%R  |    66  66  44  46  46    |
%R  |  61  66  44  44  46  46  |
%R  |61  61  44  44  44  46  46|
%R  |  61  61  44  44  14  46  |
%R  |    61  61  44  14  14    |
%R  |      61  61  14  14      |
%R  |        61  14  14        |
%R  |          14  14          |
%R  \            14            /
%R badJ:tozmp({def="badJa"}):addlrs():output()
%R badJ:tozmp({def="badJb"}):addcells():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
  \badJa
  \qquad \diagxyto/-->/<250> \qquad
  \badJb
$$

%R local sml = 2/  #1  \
%R              |#2  #3|
%R              \  #4  /
%R sml:tomp({def="sml#1#2#3#4", scale="6pt", meta="s p"}):addcells():output()
\pu

It has some cuts stopping midway

instead of going NW-SE or SW-NE as far as possible...

To show that this can't happen we will show that a J-operator

cannot have four neighboring points, like $\sml{22}{21}{12}{11}$ or $\sml{25}{24}{15}{14}$,

in three different equivalence classes.

%R local ya, yb, la, lb =
%R 2/  22  \, 2/  44  \, 2/  25  \, 2/  46  \
%R  |21  12|   |61  14|   |24  15|   |44  46|
%R  \  11  /   \  14  /   \  14  /   \  14  /
%R ya:tozmp({def="ya"}):addcells():output()
%R yb:tozmp({def="yb"}):addcells():addcuts("c 00w-01n 10e-10n"):output()
%R la:tozmp({def="la"}):addcells():output()
%R lb:tozmp({def="lb"}):addcells():addcuts("c 01s-11w 00w-00n"):output()
$$\pu
  \begin{array}{rcll}
  \ya & \diagxyto/-->/<250> & \yb & \Leftarrow \text{this a Y-cut} \\ \\
  \la & \diagxyto/-->/<250> & \lb & \Leftarrow \text{this a $λ$-cut} \\ \\
  \end{array}
$$



\newpage

%  _   _        __   __             _
% | \ | | ___   \ \ / /   ___ _   _| |_ ___
% |  \| |/ _ \   \ V /   / __| | | | __/ __|
% | |\  | (_) |   | |   | (__| |_| | |_\__ \
% |_| \_|\___/    |_|    \___|\__,_|\__|___/
%
% «there-are-no-YL-cuts» (to ".there-are-no-YL-cuts")
{\bf There are Y-cuts or $λ$-cuts: proofs}

We need these two derived rules:
%:                                  Q!=R!
%:                               ----------
%:      Q!=R!                    P!&Q!=P!&R!
%:  ---------------\NoLcuts  :=  ------------\J3
%:  (P&Q)!=(P&R)!                (P&Q)!=(P&R)!
%:
%:  ^NoLcuts1                     ^NoLcuts2
%:
%:                                     Q!=R!
%:                                  -----------
%:                                  PvvQ!=PvvR!
%:                               -----------------
%:      Q!=R!                    (PvvQ!)!=(PvvR!)!
%:  ---------------\NoYcuts  :=  -----------------\ostarcube
%:  (PvvQ)!=(PvvR)!               (PvvQ)!=(PvvR)!
%:
%:  ^NoYcuts1                      ^NoYcuts2
%:
$$\pu
  \begin{array}{rcl}
  \ded{NoYcuts1} &:=& \ded{NoYcuts2} \\ \\
  \ded{NoLcuts1} &:=& \ded{NoLcuts2} \\ \\
  \end{array}
$$

Now let's use them to prove the the Y-cut and the $λ$-cut

of the example in the previous page are inadmissible

in a J-operator.

%R local ya, yb, la, lb =
%R 2/  22  \, 2/  44  \, 2/  25  \, 2/  46  \
%R  |21  12|   |61  14|   |24  15|   |44  46|
%R  \  11  /   \  14  /   \  14  /   \  14  /
%R ya:tozmp({def="ya"}):addcells():output()
%R yb:tozmp({def="yb"}):addcells():addcuts("c 00w-01n 10e-10n"):output()
%R la:tozmp({def="la"}):addcells():output()
%R lb:tozmp({def="lb"}):addcells():addcuts("c 01s-11w 00w-00n"):output()
$$\pu
  \begin{array}{rcll}
  \ya & \diagxyto/-->/<250> & \yb & \Leftarrow \text{this a Y-cut} \\ \\
  \la & \diagxyto/-->/<250> & \lb & \Leftarrow \text{this a $λ$-cut} \\ \\
  \end{array}
$$

Look:
%
%:       11!=12!                     25!=15!
%:  ------------------\NoYcuts    -----------------\NoLcuts
%:  (21vv11)!=(21vv12)!           (24&25)!=(24&15)!
%:  -------------------           -----------------
%:        21!=22!                     24!=14!
%:       --------                     -------
%:        61=14                       44=14
%:
%:        ^noYcut-counterex           ^noLcut-counterex
%:
$$\pu
  \ded{noYcut-counterex}
  \qquad
  \ded{noLcut-counterex}
$$













\newpage

%      _                                  _
%     | |   _____  ____ _ _ __ ___  _ __ | | ___  ___
%  _  | |  / _ \ \/ / _` | '_ ` _ \| '_ \| |/ _ \/ __|
% | |_| | |  __/>  < (_| | | | | | | |_) | |  __/\__ \
%  \___/   \___/_/\_\__,_|_| |_| |_| .__/|_|\___||___/
%                                  |_|
%
% «J-examples» (to ".J-examples")
% (find-ist "-july.tex" "J-examples")

{\bf Examples of J-operators: Fourman and Scott}

%L zhafromspec = function (spec) mpnew({}, spec):addlrs():output() end
\def\zhafromspec#1{\directlua{zhafromspec("#1")}}
\pu

%L showzha = function (spec)        return mpnewJ("", spec)   :zhalr()  :output() end
%L showJ   = function (spec, J)     return mpnewJ("", spec, J):zhalr()  :output() end
%L showJPs = function (spec, J, Ps) return mpnewJ("", spec, J):zhaPs(Ps):output() end
\def\showJ    #1#2{\directlua{showJ("#1", '#2')}}
\def\showJPs#1#2#3{\directlua{showJPs("#1", '#2', "#3")}}
\pu

(i) {\sl The closed quotient.}
$$J_a p = a ∨ p.$$

(ii) {\sl The open quotient.}
$$J^a p = a→p.$$

(iii) {\sl The Boolean quotient}.
$$B_a p = (p→a)→a.$$

(iv) {\sl The forcing quotient}.
$$(J_a∧J^b)p = (a∨p)∧(b→p).$$

(vi) {\sl A mixed quotient.}
$$(B_a∧J^a)p = (p→a)→p.$$


$$
\def\li#1 #2 #3 #4    #5 #6 #7 #8 {\text{#1}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\}
\begin{array}{rlclcrlclc}
\li   (i) J_a∨J_b = J_{a∨b}    (ii)   J^a∨J^b = J^{a∧b}
\li (iii) J_a∧J_b = J_{a∧b}    (iv)   J^a∧J^b = J^{a∨b}
\li   (v) J_a∧J^a = ⊥          (vi)   J_a∨J^a = ⊤
\li (vii) J_a∨K   = K∘J_a      (viii) J^a∨K   = J^a∘K
\li  (ix) J_a∨B_a = B_a        (x)    J^a∨B_b = B_{a→b}
\end{array}
$$


\bigskip

This above is from M.P. Fourman and D.S. Scott's

``Sheaves and Logic'' (1979), that was published in SLNM0753

(``Applications of Sheaves: Proceedings of the Research Symposium

on Applications of Sheaf Theory to Logic, Algebra and Analysis -

Durham, july 9-21, 1977''). Relevant pages: 329-331.

\medskip

How do we visualize the J-operators $J_a$, $J^a$, $B_a$, etc?

And what are the `$∧$' and `$∨$' in the algebra of J-operators?

How do we visualize these `$∧$' and `$∨$'?









\newpage

%      _                             _ _
%     | |       ___  _ __  ___    __| (_) __ _  __ _ _ __ __ _ _ __ ___  ___
%  _  | |_____ / _ \| '_ \/ __|  / _` | |/ _` |/ _` | '__/ _` | '_ ` _ \/ __|
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | (_| | | | (_| | | | | | \__ \
%  \___/       \___/| .__/|___/  \__,_|_|\__,_|\__, |_|  \__,_|_| |_| |_|___/
%                   |_|                        |___/
%
% «J-ops-diagrams» (to ".J-ops-diagrams")

{\bf Examples of J-operators: diagrams}

% (find-dn6 "newrect.lua" "shortoperators-tests")

%L shortoperators()
%L spec = "1234567654321"
%L jout = function (J, marks, altspec) mpnewJ({}, altspec or spec, J):zhaPs(marks):output() end
\def\jout#1{\directlua{jout(#1)}}
\pu
%L spec = "123454321"
\pu
$$
\begin{array}{ccc}
\mat{J_a p := a∨p \\ \text{(closed quotient)}}  &&  J_{22} = \jout{Cloq(v"22"), "22"} \\ \\
\mat{J^a p := a→p \\ \text{(open quotient)}}    &&  J^{22} = \jout{Opnq(v"22"), "22"} \\ \\
\mat{B_a p := (p→a)→a \\ \text{(Boolean quotient)}}  &&  B_{12} = \jout{Booq(v"12"), "12"} \\ \\
\mat{(J_a∧J^b)p := (a∨p)∧(b→p) \\ \text{(forcing quotient)}}
  && (J_{42}∧J^{24})p = \jout{Forq(v"42", v"24"), "42 24", "1234567654321"} \\ \\
% \mat{(B_a∧J^a)p := (p→a)→p \\ \text{(mixed quotient)}}
%   && (B_{22}∧J^{22}))p = \jout{Mixq(v"22"), "22", "12345654321"} \\ \\
\end{array}
$$

\newpage

%  ____  _
% |  _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% |  __/| | (_| (__\__ \
% |_|   |_|\___\___|___/
%
% «piccs» (to ".piccs")
% (find-ist "-july.tex" "piccs")

{\bf Partitions into contiguous classes (``piccs'')}

A good way to understand the algebra of J-operators

is to start by the one-dimensional case.

(ZHAs are two-dimensional things.)

\medskip

A partition of $\{0, \ldots, n\}$ into contiguous classes (a ``picc'')

is one in which this holds: if $a,b,c∈\{0, \ldots, n\}$, $a<b<c$ and $a∼c$,

then $a∼b∼c$.

So, for example, $\{\{0,1\},\{2\},\{3,4,5\}\}$ is a picc,

but $\{\{0,2\},\{1\}\}$ is not.

\medskip

A partition of $\{0, \ldots, n\}$ into contiguous classes induces:

1) an equivalence relation $· ∼_P ·$,

2) a function $[·]_P$ that returns the equivalence class of an element,

3) a function
%
$$\begin{array}{rrcl}
  ·^P:& \{0, \ldots, n\} &→& \{0, \ldots, n\} \\
      &                a &↦& \max \; [a]_P \\
  \end{array}
$$

that takes each element to the top element in its class,

4) a set $\St_P := \setofst{a∈\{0, \ldots, n\}}{a^P=a}$ of the "stable"

elements of $\{0,...,n\}$, and

5) a graphical representation with a bar between $a$ and $a+1$

when they are in different classes:
%
$$ 01|2|345 \quad ≡ \quad \{\{0,1\},\{2\},\{3,4,5\}\},$$

which will be our favourite notation for piccs from now on.


\newpage

%     _    _            _                        __         _
%    / \  | | __ _  ___| |__  _ __ __ _    ___  / _|  _ __ (_) ___ ___ ___
%   / _ \ | |/ _` |/ _ \ '_ \| '__/ _` |  / _ \| |_  | '_ \| |/ __/ __/ __|
%  / ___ \| | (_| |  __/ |_) | | | (_| | | (_) |  _| | |_) | | (_| (__\__ \
% /_/   \_\_|\__, |\___|_.__/|_|  \__,_|  \___/|_|   | .__/|_|\___\___|___/
%            |___/                                   |_|
%
% «algebra-of-piccs» (to ".algebra-of-piccs")
% (find-ist "-july.tex" "alg-of-piccs")
% (phop 25)

{\bf The algebra of piccs}

When $P$ and $P'$ are two piccs on $\{0, \ldots, n\}$ we say

that $P≤P'$ when $∀a∈\{0, \ldots, n\}.a^P≤a^{P'}$.

The intuition is that $P≤P'$ means that the graph

of the function $·^P$ is under the graph of $·^{P'}$:
%
%L partitiongraph = function (opts, spec, ylabel)
%L     local mp = MixedPicture.new(opts)
%L     for y=0,5 do mp:put(v(-1, y), y.."") end
%L     for x=0,5 do mp:put(v(x, -1), x.."") end
%L     for a=0,5 do local aP = spec:sub(a+1, a+1)+0; mp:put(v(a, aP), "*") end
%L     mp.lp:addlineorvector(v(0, 0), v(6, 0), "vector")
%L     mp.lp:addlineorvector(v(0, 0), v(0, 6.5), "vector")
%L     mp:put(v(7, 0), "a")
%L     mp:put(v(0, 7), "aP", ylabel)
%L     return mp
%L   end
%L pg = function (def, spec, ylabel)
%L     return partitiongraph({def=def, scale="5pt", meta="s"}, spec, ylabel)
%L   end
%L
%L pg("grapha", "012345", "a^P"     ):output()
%L pg("graphb", "113355", "a^{P'}"  ):output()
%L pg("graphc", "115555", "a^{P''}" ):output()
%L pg("graphd", "555555", "a^{P'''}"):output()
%L
%
%  a^P                  a^P                  a^P                  a^P
%    ^                    ^                    ^                    ^
%  5 |         *        5 |       * *        5 |   * * * *        5 * * * * * *
%  4 |       *          4 |                  4 |                  4 |
%  3 |     *        <=  3 |   * *        <=  3 |              <=  3 |
%  2 |   *              2 |                  2 |                  2 |
%  1 | *                1 * *                1 * *                1 |
%  0 *----------> a     0 +----------> a     0 +----------> a     0 +----------> a
%    0 1 2 3 4 5          0 1 2 3 4 5          0 1 2 3 4 5          0 1 2 3 4 5
%
%     0|1|2|3|4|5   <=      01|23|45     <=       01|2345            012345
%
$$\pu
  \begin{array}{ccccccc}
  \grapha     &≤& \graphb  &≤& \graphc &≤& \graphd \\ \\
  0|1|2|3|4|5 &≤& 01|23|45 &≤& 01|2345 &≤& 012345  \\
  P           &≤& P'       &≤& P''     &≤& P'''    \\
  \end{array}
$$

This yields a partial order on piccs, whose bottom element is the

identity function $0|1|\ldots|n$, and the top element is $01\ldots n$,

that takes all elements to $n$.

\medskip

It turns out that the piccs form a (Heyting!) algebra, in which we can

define $⊤$, $⊥$, $∧$, $∨$, and even $→$.

%D diagram algebra-of-piccs
%D 2Dx     100    +20   +20     +30 +20 +20
%D 2D  100       01234              T
%D 2D              ^                ^
%D 2D              |                |
%D 2D  +20      01|234             PvQ
%D 2D           ^    ^            ^   ^
%D 2D          /      \          /     \
%D 2D  +20 0|1|234  01|2|34     P       Q
%D 2D          ^      ^          ^     ^
%D 2D           \    /            \   /
%D 2D  +20     0|1|2|34            P&Q
%D 2D              ^                ^
%D 2D              |                |
%D 2D  +20     0|1|2|3|4           bot
%D 2D
%D (( T .tex= ⊤  PvQ .tex= P∨Q  P&Q .tex= P∧Q  bot .tex= ⊥
%D    01234 01|234 <-                             T PvQ <-
%D    01|234 0|1|234 <- 01|234 01|2|34 <-         PvQ P <- PvQ Q <-
%D    0|1|234 0|1|2|34 <- 01|2|34 0|1|2|34 <-     P P&Q <- Q P&Q <-
%D    0|1|2|34 0|1|2|3|4 <-                       P&Q bot <-
%D
%D ))
%D enddiagram
%D
$$\pu \diag{algebra-of-piccs}$$




\newpage

%  ________              _   _            _
% |__  / _ \ _   _  ___ | |_(_) ___ _ __ | |_ ___
%   / / | | | | | |/ _ \| __| |/ _ \ '_ \| __/ __|
%  / /| |_| | |_| | (_) | |_| |  __/ | | | |_\__ \
% /____\__\_\\__,_|\___/ \__|_|\___|_| |_|\__|___/
%
% «zquotients» (to ".zquotients")
% (phop 26)

{\bf ZQuotients}

A {\it ZQuotient} for a ZHA with top element 46 is:

a picc on $\{0, \ldots ,4\}$ (a ``partition of the left wall''), plus

a picc on $\{0, \ldots ,6\}$ (a ``partition of the right wall'').

\medskip

Our favourite short notation for ZQuotients is with ``$/$''s and ``$\bsl$''s,

like this, ``$4321/0\; 0123\bsl45\bsl6$'', because we regard the cuts

in a ZQuotient as diagonal cuts on the ZHA.

%L mpnew({def="ZQ", scale="2pt", meta="t"}, "1R2R3212RL1"):addbullets():output()
%
The graphical notation is this (for $4321/0\; 0123\bsl45\bsl6$ on $\pu \ZQ$):
%
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
%                /  \
%                 46
%             /  \     \
%              45    36
%             \     \     \
%                 35    26
%             /        \  /
%              34    25
%             \        /
%                 24
%             /  \     \
%              23    14
%          /        \  /  \
%           22    13    04
%          \        /  \  /
%              12    03
%          /     /     /
%           11    02
%          \  /     /
%              01
%          /     /
%           00
% 4321/0   \  /           0123\45\6
%
$$\pu
  \ZQuotients
$$

which makes clear how we can adapt the definitions of

$·∼_P·$, $[·]_P$, $·^P$, $\St_P$, which were on (one-dimensional!) piccs,

to their two-dimensional counterparts on ZQuotients.

If $P$ is the ZQuotient of the figure above, then:
%
$$\begin{array}{rcl}
   34 ∼_P 25 &\text{is}& \text{true}, \\
   23 ∼_P 24 &\text{is}& \text{false}, \\
   {}[12]_P   &=&         \{11, 12, 13, 22, 23\}, \\
   22^P       &=&          23, \\
   \St_P      &=&         \{03, 04, 23, 45, 46\}. \\
  \end{array}
$$


\newpage

%      _                           _            _
%     | |   ___  _ __  ___    __ _| | __ _  ___| |__  _ __ __ _
%  _  | |  / _ \| '_ \/ __|  / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| | | (_) | |_) \__ \ | (_| | | (_| |  __/ |_) | | | (_| |
%  \___/   \___/| .__/|___/  \__,_|_|\__, |\___|_.__/|_|  \__,_|
%               |_|                  |___/
%
% «J-ops-algebra» (to ".J-ops-algebra")
% (phop 27)

{\bf The algebra of J-operators}

$$\begin{array}{rlcl}
  (i)   & J_a∨J_b = J_{a∨b}   & & J_{21}∨J_{12} = J_{21∨12} \\
  (ii)  & J^a∨J^b = J^{a{∧}b} & & J^{32}∨J^{23} = J^{32{∧}23} \\
  (iii) & J_a∧J_b = J_{a{∧}b} & & J_{32}∧J_{23} = J_{32{∧}23} \\
  (iv)  & J^a∧J^b = J^{a∨b}   & & J^{32}∧J^{23} = J^{32∨23} \\ \\
        &                      & & \text{($↑$ used in the examples below)} \\
  \end{array}
$$

%L spec = "123454321"
\pu
$$
\begin{array}{rccc}
(i)   & \jout{Cloq(v"21"), "21"} ∨
        \jout{Cloq(v"12"), "12"} =
        \jout{Cloq(v"22"), "12 21 22"} \\ \\
(ii)  & \jout{Opnq(v"32"), "32"} ∨
        \jout{Opnq(v"23"), "23"} =
        \jout{Opnq(v"22"), "32 23 22"} \\ \\
(iii) & \jout{Cloq(v"32"), "32"} ∧
        \jout{Cloq(v"23"), "23"} =
        \jout{Cloq(v"22"), "32 23 22"} \\ \\
(iv)  & \jout{Opnq(v"32"), "32"} ∧
        \jout{Opnq(v"23"), "23"} =
        \jout{Opnq(v"33"), "32 23 33"} \\ \\
\end{array}
$$

\newpage

%      _                           _            _                 ____
%     | |   ___  _ __  ___    __ _| | __ _  ___| |__  _ __ __ _  |___ \
%  _  | |  / _ \| '_ \/ __|  / _` | |/ _` |/ _ \ '_ \| '__/ _` |   __) |
% | |_| | | (_) | |_) \__ \ | (_| | | (_| |  __/ |_) | | | (_| |  / __/
%  \___/   \___/| .__/|___/  \__,_|_|\__, |\___|_.__/|_|  \__,_| |_____|
%               |_|                  |___/
%
% «J-ops-algebra-2» (to ".J-ops-algebra-2")
% (phop 28)

{\bf The algebra of J-operators, 2}

We can depict the four equations of the previous page as:

%D diagram J-alg-1
%D 2Dx     100 +20 +20 +10 +10 +20 +20
%D 2D  100             T
%D 2D  +30     A               E
%D 2D  +20 B       C       F       G
%D 2D  +20     D               H
%D 2D  +30            bot
%D 2D
%D ren      T     ==>           J_⊤=⊤=J^⊥
%D ren    A   E   ==>     J_{22}          J^{22}
%D ren   B C F G  ==> J_{21} J_{12}   J^{32} J^{23}
%D ren    D   H   ==>     J_{11}          J^{11}
%D ren     bot    ==>           J_⊥=⊥=J^⊤
%D
%D (( A T -> E T ->
%D    B A -> C A -> F E -> G E ->
%D    D B -> D C -> H F -> H G ->
%D    bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{J-alg-1}
$$

using Fourman and Scott's notation, or as

%D diagram J-alg-2
%D 2Dx     100 +20 +20 +10 +10 +20 +20
%D 2D  100             T
%D 2D  +30     A               E
%D 2D  +20 B       C       F       G
%D 2D  +20     D               H
%D 2D  +30            bot
%D 2D
%D 2Dx     100 +20 +20 +15 +15 +20 +20
%D 2D  100             T
%D 2D  +35     A               E
%D 2D  +20 B       C       F       G
%D 2D  +20     D               H
%D 2D  +35            bot
%D 2D
%D ren      T     ==>      (⊤∨)=(λp.⊤)=(⊥{→})
%D ren    A   E   ==>     (22∨)          (22{→})
%D ren   B C F G  ==> (21∨) (12∨)   (32{→}) (23{→})
%D ren    D   H   ==>     (11∨)          (33{→})
%D ren     bot    ==>      (⊥∨)=(λp.p)=(⊤{→})
%D
%D (( A T -> E T ->
%D    B A -> C A -> F E -> G E ->
%D    D B -> D C -> H F -> H G ->
%D    bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{J-alg-2}
$$

using a notation that I think is obvious.

\newpage

%      _                           _            _                 _____
%     | |   ___  _ __  ___    __ _| | __ _  ___| |__  _ __ __ _  |___ /
%  _  | |  / _ \| '_ \/ __|  / _` | |/ _` |/ _ \ '_ \| '__/ _` |   |_ \
% | |_| | | (_) | |_) \__ \ | (_| | | (_| |  __/ |_) | | | (_| |  ___) |
%  \___/   \___/| .__/|___/  \__,_|_|\__, |\___|_.__/|_|  \__,_| |____/
%               |_|                  |___/
%
% «J-ops-algebra-3» (to ".J-ops-algebra-3")
% (phop 29)

{\bf The algebra of J-operators, 3}

$$\begin{array}{rlcl}
  (v)   & J_a∧J^a = ⊥         & & J_{21}∧J^{21} = ⊥      \\
  (vi)  & J_a∨J^a = ⊤         & & J_{21}∨J^{21} = ⊤      \\
  (ix)  & J_a∨B_a = B_a        & & J_{21}∨B_{21} = B_{21}  \\
  (x)   & J^a∨B_b = B_{a→b}   & & J^{21}∨B_{12} = B_{21{→}12}  \\
        &                      & & \text{($↑$ used in the examples below)} \\
  \end{array}
$$

%L spec = "123454321"
\pu
$$
\begin{array}{rccc}
(v)  & \jout{Cloq(v"21"), "21"} ∧
       \jout{Opnq(v"21"), "21"} =
       \jout{Falq(), ""}          \\ \\
(vi) & \jout{Cloq(v"21"), "21"} ∨
       \jout{Opnq(v"21"), "21"} =
       \jout{Truq(), ""}          \\ \\
(ix) & \jout{Cloq(v"21"), "21"} ∨
       \jout{Booq(v"21"), "21"} =
       \jout{Booq(v"21"), "21"}   \\ \\
(x)  & \jout{Opnq(v"21"), "21"} ∨
       \jout{Booq(v"12"), "12"} =
       \jout{Booq(v"14"), "21 12 14"} \\
\end{array}
$$





\newpage

%  ________              _   _            _                     _
% |__  / _ \ _   _  ___ | |_(_) ___ _ __ | |_ ___   _ __   ___ | |_   _
%   / / | | | | | |/ _ \| __| |/ _ \ '_ \| __/ __| | '_ \ / _ \| | | | |
%  / /| |_| | |_| | (_) | |_| |  __/ | | | |_\__ \ | |_) | (_) | | |_| |
% /____\__\_\\__,_|\___/ \__|_|\___|_| |_|\__|___/ | .__/ \___/|_|\__, |
%                                                  |_|            |___/
% «zquotients-poly» (to ".zquotients-poly")

{\bf ZQuotients as polynomials}

% (find-books "__cats/__cats.el" "slnm0753")
% (find-slnm0753page (+ 14 331)   "polynomial")

Fourman and Scott, p.331:

{\sl If we take a polynomial in $→$, $∧$, $∨$, $⊥$, say $f(p,a,b,\ldots)$, it is a

decidable question whether for all $a,b,\ldots$ it defines a J-operator.}

\medskip

All ZQuotients are polynomials in that sense.

Moreover, they can be built from elementary J-operators

using just $B_P$ and $∧$.

Example:

{

%L local ba, bb, bc = Booq(v"04"), Booq(v"23"), Booq(v"45")
%L local babc = Jand(ba, Jand(bb, bc))
%L mpnewJ({def="fooa"}, "1R2R3212RL1", Booq(v"04")):zhaPs("04")      :output():print()
%L mpnewJ({def="foob"}, "1R2R3212RL1", Booq(v"23")):zhaPs("23")      :output():print()
%L mpnewJ({def="fooc"}, "1R2R3212RL1", Booq(v"45")):zhaPs("45")      :output():print()
%L mpnewJ({def="food"}, "1R2R3212RL1", babc       ):zhaPs("04 23 45"):output():print()
%L mpnew ({def="fooe"}, "1R2R3212RL1"      ):addlrs():output()
%L mpnewJ({def="foof"}, "1R2R3212RL1", babc):zhaJ()  :output()
\pu
$$
  \begin{array}{c}
  \fooa ∧ \foob ∧ \fooc = \food
  \end{array}
$$

\medskip

It is easy to check by hand (test it for a few `$P$'s!) that
%
$$
  \def→{{\to}}
  \def\foo#1{((P→#1)→#1)}
  \begin{array}{rcl}
    B_{04}∧B_{23}∧B_{45} &=& λP.((B_{04}∧B_{23}∧B_{45})(P))      \\
                          &=& λP.((B_{04}(P)∧B_{23}(P)∧B_{45}(P)) \\
                          &=& λP.(\foo{04}∧\foo{23}∧\foo{45})     \\
  \end{array}
$$

acts as:

$$
\fooe
\quad
% \diagxyto/-->/<750>^{B_{04}∧B_{23}∧B_{45}}
\diagxyto/-->/<250>
\quad
\foof
$$

}

\bigskip
\bigskip

Now we know that on ZHAs

1) J-operators are ZQuotients,

2) ZQuotients are (polynomial!) J-operators.

\newpage

%  _____ _ _             _             
% |  ___| (_)_ __  _ __ (_)_ __   __ _ 
% | |_  | | | '_ \| '_ \| | '_ \ / _` |
% |  _| | | | |_) | |_) | | | | | (_| |
% |_|   |_|_| .__/| .__/|_|_| |_|\__, |
%           |_|   |_|            |___/ 
%
% «flipping» (to ".flipping")

{\bf Bottlenecks and flipping}

A {\sl bottleneck} in a ZHA is a point where $L(y)=R(y)$.

We can flip everything in a ZHA between two consecutive bottlenecks

and obtain a ZHA that is isomorphic to the previous one.

%R local flipa, flipb, flipc, flipd =
%R 1/    o \, 1/  o \, 1/    o  \, 1/  o  \
%R  |   o g|   | o g|   |   h o |   | h o |
%R  |  e f |   |e f |   |    o k|   |  o k|
%R  |   *  |   | *  |   |   o j |   | o j |
%R  |  *   |   |  * |   |  g i  |   |g i  |
%R  | o d  |   | o d|   |   *   |   | *   |
%R  |b o   |   |b o |   |  * f  |   |f *  |
%R  | a c  |   | a c|   | d e   |   | e d |
%R  \  o   /   \  o /   |  *    |   |  *  |
%R                      | o c   |   | o c |
%R                      |a b    |   |a b  |
%R                      \ o     /   \ o   /
%R flipa:tozmp({def="flipa"}):addcells():addcontour():output()
%R flipb:tozmp({def="flipb"}):addcells():addcontour():output()
%R flipc:tozmp({def="flipc"}):addcells():addcontour():output()
%R flipd:tozmp({def="flipd"}):addcells():addcontour():output()

$$\pu
  \flipa \diagxyto/-->/<250> \quad \flipb
  \qquad
  \flipc \diagxyto/-->/<250> \quad \flipd
$$

Their 2-column graphs will be isomorphic, too,

but that may not be evident when we look at them.

%D diagram flipa
%L drawtwocolgraph(30, -15, 3, 5, "33", "12 23", "a b e", "c d • f g")
%D enddiagram

%D diagram flipb
%L drawtwocolgraph(30, -15, 4, 4, "32", "12 33", "a b • e", "c d f g")
%D enddiagram

%D diagram flipc
%L drawtwocolgraph(30, -15, 4, 7, "22 34 46", "13 25", "a d g h", "b c e f i j k")
%D enddiagram

%D diagram flipd
%L drawtwocolgraph(30, -15, 5, 6, "22 43 55", "13 34", "a e f g h", "b c d i j k")
%D enddiagram

$$\pu
  \left(\diag{flipa}\right)
  \quad \diagxyto/-->/<250> \quad
  \left(\diag{flipb}\right)
  \qquad
  \left(\diag{flipc}\right)
  \quad \diagxyto/-->/<250> \quad
  \left(\diag{flipd}\right)
$$




\newpage

%  ________              _                       ____           _           
% |__  / _ \ _   _  ___ | |_ ___    ___  _ __   |___ \ ___ ___ | | __ _ ___ 
%   / / | | | | | |/ _ \| __/ __|  / _ \| '_ \    __) / __/ _ \| |/ _` / __|
%  / /| |_| | |_| | (_) | |_\__ \ | (_) | | | |  / __/ (_| (_) | | (_| \__ \
% /____\__\_\\__,_|\___/ \__|___/  \___/|_| |_| |_____\___\___/|_|\__, |___/
%                                                                 |___/     
% «zquots-on-2colgs» (to ".zquots-on-2colgs")

{\bf How ZQuotients act on 2-column graphs}

Here is one way to understand how a ZQuotient acts on a 2-column graph.

It will take several slides.

\medskip

Let $C:=\left( 5, 6,
               \csm{\ltor45 \\ \ltor34 \\ \ltor22 \\ \ltor11},
               \cmat{\lotr 25}
        \right)$.

Let $C^⋄:=\left( 5, 6, \{\}, \{\} \right)$.

Let $H$ be the ZHA for $C$.

Let $H^⋄$ be the ZHA for $C^⋄$ (a lozenge).

Let $J:H→H$ be a J-operator on $H$.

We can describe $J$ by its cuts.

Draw the same cuts on $H^⋄$.

This induces a J-operator $J^⋄:H^⋄→H^⋄$ on $H^⋄$.

For example, if the cuts are
%
$$5 / 4321 / 0 \; 0123 \bsl 45 \bsl 6,$$

then $(H,J)$ and $(H^⋄,J^⋄)$ are:
%
%L mpnew({def="quoa"}, "1R2R3212RLL1"):addlrs():addcuts("c 5/4321/0 0123|45|6"):output()
%L mpnew({def="quob"}, "123456R54321"):addlrs():addcuts("c 5/4321/0 0123|45|6"):output()
%
$$
  \pu
  \quoa
  \qquad
  \qquad
  \quob
$$

The operation `${·}^*$' takes each element in $H$

to the top element in its equivalence class.

Let's create a dual operation, `${·}^{\co*}$', that takes

each element in $H$ to the {\sl bottom} element in its equivalence class.

The corresponding operations on $H^⋄$

will be denoted by `${·}^⋄$' and `${·}^{\co⋄}$'.

For example:
%
$$\begin{array}{rrr}
       12^*=23 &&     12^⋄=43  \\
  12^{\co*}=11 && 12^{\co⋄}=10 \\
  \end{array}
$$

Now look at the cuts, and at the left and right piccs...
%
$$\begin{array}{rclrclrcl}
       [1]^L &=& \{1,2,3,4\}  &&&&     [2]^R &=& \{0,1,2,3\} \\
         1^L &=& 4            &&&&       2^R &=& 3 \\
   1^{\co L} &=& 1            &&&& 2^{\co R} &=& 0 \\
  \end{array}
$$

We have:
%
$$\begin{array}{rclccrcccl}
  ab^⋄      &=& a^Lb^R             &&&      12^⋄ &=& 1^L2^R &=& 43 \\
  ab^{\co⋄} &=& a^{\co L}b^{\co R} &&& 12^{\co⋄} &=& 1^{\co L}2^{\co R} &=& 10 \\
  \end{array}
$$


\newpage

%  ________              _                       ____                 ____  
% |__  / _ \ _   _  ___ | |_ ___    ___  _ __   |___ \ ___ __ _ ___  |___ \ 
%   / / | | | | | |/ _ \| __/ __|  / _ \| '_ \    __) / __/ _` / __|   __) |
%  / /| |_| | |_| | (_) | |_\__ \ | (_) | | | |  / __/ (_| (_| \__ \  / __/ 
% /____\__\_\\__,_|\___/ \__|___/  \___/|_| |_| |_____\___\__, |___/ |_____|
%                                                         |___/             
% «zquots-on-2colgs-2» (to ".zquots-on-2colgs-2")

{\bf How ZQuotients act on 2-column graphs, 2}

Let $C:=\left( 5, 6,
               \csm{\ltor45 \\ \ltor34 \\ \ltor22 \\ \ltor11},
               \cmat{\lotr 25}
        \right)$.

Let $C^⋄:=\left( 5, 6, \{\}, \{\} \right)$.

Let $H$ be the ZHA for $C$.

Let $H^⋄$ be the ZHA for $C^⋄$ (a lozenge).

Let $J:H→H$ be a J-operator on $H$,

and $J^⋄:H^⋄→H^⋄$ be a J-operator on $H^⋄$,

both with these cuts:
%
$$5 / 4321 / 0 \; 0123 \bsl 45 \bsl 6.$$

Then $(H^⋄,J^⋄)$ and $(H,J)$ and are:
%
%L mpnew({def="quoa"}, "123456R54321"):addlrs():addcuts("c 5/4321/0 0123|45|6"):output()
%L mpnew({def="quob"}, "1R2R3212RLL1"):addlrs():addcuts("c 5/4321/0 0123|45|6"):output()
%
$$
  \pu
  \quoa
  \qquad
  \qquad
  \quob
$$

The equivalence classes for 12 in $(H^⋄,J^⋄)$ and $(H,J)$ are

$[12]^⋄ = [12^{\co⋄},12^⋄] = [10,43]⊆H^⋄$ and

$[12]^* = [12^{\co*},12^*] = [11,23]⊆H$.

The elements of $[12]^⋄$ and $[12]^*$

are simply the open sets of these forms:

%D diagram zquoa
%L drawtwocolgraph(30, -15, 5, 6, "",            "",   "1 ? ? ? 0", "? ? ? 0 0 0")
%D enddiagram
%
%D diagram zquob
%L drawtwocolgraph(30, -15, 5, 6, "11 22 34 45", "25", "1 ? ? ? 0", "? ? ? 0 0 0")
%D enddiagram
%
%D diagram zquoc
%L drawtwocolgraph(30, -15, 5, 6, "11 22 34 45", "25", "1 ? 0 0 0", "1 ? ? 0 0 0")
%D enddiagram
%
$$\pu
  \def\L#1#2{#2}
  \def\R#1#2{#2}
  \left(\diag{zquoa}\right)
  \qquad
  % \diagxyto/-->/<250>
  \qquad
  \left(\diag{zquob}\right)
  % \quad
  \diagxyto/-->/<250>
  % \quad
  \left(\diag{zquoc}\right)
$$


\newpage

%  ________              _                       ____                 _____ 
% |__  / _ \ _   _  ___ | |_ ___    ___  _ __   |___ \ ___ __ _ ___  |___ / 
%   / / | | | | | |/ _ \| __/ __|  / _ \| '_ \    __) / __/ _` / __|   |_ \ 
%  / /| |_| | |_| | (_) | |_\__ \ | (_) | | | |  / __/ (_| (_| \__ \  ___) |
% /____\__\_\\__,_|\___/ \__|___/  \___/|_| |_| |_____\___\__, |___/ |____/ 
%                                                         |___/             
% «zquots-on-2colgs-3» (to ".zquots-on-2colgs-3")

{\bf How ZQuotients act on 2-column graphs, 3}

The best way to see the action of a J-operator

on a 2-column graph $C$ is this.

An open set on $C$ is a map $C→\{0,1\}$.

We erase some of its information, replacing it by `$?$'s,

then we try to reconstruct it.

There are two natural ways.

One, depicted below, that yields `$·^*$', takes the {\sl biggest}

open set with `0' and `1's in the specified places.

%D diagram zquoa
%L drawtwocolgraph(20, -15, 5, 6, "11 22 34 45", "25", "1 0 0 0 0", "1 1 0 0 0 0")
%D enddiagram
%
%D diagram zquob
%L drawtwocolgraph(20, -15, 5, 6, "11 22 34 45", "25", "1 ? ? ? 0", "? ? ? 0 ? 0")
%D enddiagram
%
%D diagram zquoc
%L drawtwocolgraph(20, -15, 5, 6, "11 22 34 45", "25", "1 1 0 0 0", "1 1 1 0 0 0")
%D enddiagram
%
$$\pu
  12
  \;\; ≡ \;\;
  \left(\diag{zquoa}\right)
  \diagxyto/-->/<250>^{\text{erase}}
  \left(\diag{zquob}\right)
  \diagxyto/-->/<250>^{\text{biggest}}
  \left(\diag{zquoc}\right)
  \;\; ≡ \;\;
  23
  \; = \;
  12^*
$$

The other way, that takes the {\sl smallest} open set with `0' and `1's

in the specified places, yields `$·^{\co*}$'.

\bigskip

Here is the {\sl right} way (for adults!!!) to see that.

Choose a subset $D$ of the points of $C$.

Endow $D$ with the topology inherited from $C$.

(In our case, $D$ has to inherit the {\sl order}).

%D diagram cquoC
%L drawtwocolgraph(30, -15, 5, 6, "11 22 34 45", "25")
%D enddiagram
%
%D diagram cquoD
%D ((
%D node: 100,100 L1 .tex= 1\_
%D node: 100,85  L2 .tex= 2\_
%D node: 100,70  L3 .tex= 3\_
%D node: 100,55  L4 .tex= 4\_
%D node: 100,40  L5 .tex= 5\_
%D node: 130,100 R1 .tex= \_1
%D node: 130,85  R2 .tex= \_2
%D node: 130,70  R3 .tex= \_3
%D node: 130,55  R4 .tex= \_4
%D node: 130,40  R5 .tex= \_5
%D node: 130,25  R6 .tex= \_6
%D L5 L1 ->    R6 R4 ->
%D L5 R4 ->    R6 L1 ->
%D ))
%D enddiagram
%D 
$$\pu
  D
  \;\; ≡ \;\;
  \left(\diag{cquoD}\right)
  \quad
  \diagxyto/->/<250>^{i}
  \quad
  \left(\diag{cquoC}\right)
  \;\; ≡ \;\;
  C
$$

The inclusion map $i:D→C$ induces a map $i^*:\Opens(D) ← \Opens(C)$,

that can be extended to a functor $i^*: \Set^D ← \Set^C$

having both adjoints --- $i_! ⊣ i^* ⊣ i_*$.

This $i_! ⊣ i^* ⊣ i_*$ is an {\sl essential geometric morphism}

that is an {\sl inclusion}.


\newpage



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

{\bf Part 3:

Seminar handouts}

(For younger children -

including some who have

never seen a theorem)

\medskip

This part is {\sl very} incomplete

at this moment!

\newpage




%  _________       _           _________    _    ____
% |__  / ___|  ___| |_ ___    |__  /  _ \  / \  / ___|___
%   / /\___ \ / _ \ __/ __|     / /| | | |/ _ \| |  _/ __|
%  / /_ ___) |  __/ |_\__ \_   / /_| |_| / ___ \ |_| \__ \_
% /____|____/ \___|\__|___( ) /____|____/_/   \_\____|___( )
%                         |/                             |/
%  _________        _              _
% |__  / ___| _   _| |__  ___  ___| |_ ___
%   / /\___ \| | | | '_ \/ __|/ _ \ __/ __|
%  / /_ ___) | |_| | |_) \__ \  __/ |_\__ \
% /____|____/ \__,_|_.__/|___/\___|\__|___/
%
% «zsets-handouts» (to ".zsets-handouts")

{\bf Handouts: ZSets and ZDAGs for children}

%R local kite = 2/  #1  \
%R               |#2  #3|
%R               |  #4  |
%R               \  #5  /
%R kite:tomp({def=  "zsetKiteMicro",      scale="2.8pt", meta="t"}):addbullets():output()
%R kite:tomp({def=  "zsetKite",           scale="4.5pt", meta=nil}):addbullets():output()
%R kite:tomp({def=    "zfKite#1#2#3#4#5", scale="5pt",   meta="s"}):addcells():output()
%R kite:tomp({def=  "zdagKite#1#2#3#4#5", scale="20pt",  meta=nil}):addcells():addarrows():output()
%R kite:tomp({def="zdagKiteWM#1#2#3#4#5", scale="20pt",  meta=nil}):addcells():addarrows():output()
%R kite:tomp({def= "zfKiteBig#1#2#3#4#5", scale="15pt",  meta=nil}):addcells():output()
\pu

As a subset of $\Z^2$, $K = \zsetKite$ (``kite'') is:

$$\left\{ \; \zfKiteBig {(1,3),} {(0,2),} {(2,2),} {(1,1),} {(1,0)} \; \right\}.$$

The {\it reading order} on $K$, $\mathsf{read}_K: K \to \N$, is $\zfKite12345$.

The two natural DAGs on $K$ are:

$$(K, \BM(K))
  =
  \zdagKite  {(1,3)} {(0,2)} {(2,2)} {(1,1)} {(1,0)}
  =
  (
  \cmat{ (1,3), \\ (0,2),\,(2,2), \\ (1,1), \\ (1,0) }
  , \;
  \cmat{ ((1,3),(0,2)),\,((1,3),(2,2)) \\ ((0,2),(1,1)),\,((2,2),(1,1)), \\ ((1,1),(1,0)) }
  )
$$

$$(K, \WM(K))
  =
  \zdagKiteWM {(1,3)} {(0,2)} {(2,2)} {(1,1)} {(1,0)}
  =
  (
  \cmat{ (1,3), \\ (0,2),\,(2,2), \\ (1,1), \\ (1,0) }
  , \;
  \cmat{ ((0,2),(1,3)),\,((2,2),(1,3)) \\ ((1,1),(0,2)),\,((1,1),(2,2)), \\ ((1,0),(1,1)) }
  )
$$

which are isomorphic to:

$$\zdagKite 12345
  =
  (
  \cmat{ 1 \\ 2,\;\;3, \\ 4, \\ 5, }
  , \;
  \cmat{ (1,2),\,(1,3) \\ (2,4),\,(3,4), \\ (4,5) }
  )
$$

$$\zdagKiteWM 12345
  =
  (
  \cmat{ 1 \\ 2,\;\;3, \\ 4, \\ 5, }
  , \;
  \cmat{ (2,1),\,(3,1) \\ (4,2),\,(4,3), \\ (5,4) }
  )
$$

\newpage

%   ____ _                   __                  _   _
%  / ___| |__   __ _ _ __   / _|_   _ _ __   ___| |_(_) ___  _ __  ___
% | |   | '_ \ / _` | '__| | |_| | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% | |___| | | | (_| | |    |  _| |_| | | | | (__| |_| | (_) | | | \__ \
%  \____|_| |_|\__,_|_|    |_|  \__,_|_| |_|\___|\__|_|\___/|_| |_|___/
%
% «characteristic-functions» (to ".characteristic-functions")

{\bf Handouts: Notation for characteristic functions.}

By default $\zfKite01001$ would be the function $\zfKite01001:
\zfKite••••• \to \{0,1\}$,

but when we say $\zfKite01001 ⊆ \zfKite•••••$ we mean:

$\cmat{ · \\ (0,2),\;\;\;· \\ · \\ (1,0) }
 ⊆
 \cmat{ (1,3), \\ (0,2),\,(2,2), \\ (1,1), \\ (1,0) }
$,
or
$\cmat{ · \\ 2,\;\;\;· \\ · \\ 5 }
 ⊆
 \cmat{ 1 \\ 2,\;\;3, \\ 4, \\ 5 }
$.

\bigskip
\bigskip
\bigskip


%   ___          _             _                    _             _
%  / _ \ _ __ __| | ___ _ __  | |_ ___  _ __   ___ | | ___   __ _(_) ___  ___
% | | | | '__/ _` |/ _ \ '__| | __/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | |_| | | | (_| |  __/ |    | || (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
%  \___/|_|  \__,_|\___|_|     \__\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%                                      |_|                  |___/
% «order-topologies» (to ".order-topologies")

{\bf Handouts: Order topologies.}

{
\def\k{\zfKite}

Example:
$(\zsetKiteMicro, \Opens(\zsetKiteMicro))$
is
$\left(\k•••••,
       \left\{ \k00000, \k00001, \k00011, \k00111, \k01011, \k01111, \k11111 \right\}
 \right)$.


Note that $\k01001$ is {\sl not open} - because when we draw it like this,

$$\zdagKite01001$$

there is an arrow `$1 \to 0$' in it.

Order topologies can be defined formally interpreting each arrow as a condition.
For example, on this DAG,
%
$$\zdagKite 12345$$
%
the set of open sets is:
%
$$\def\cond#1#2{#1{∈}A \to #2{∈}A}
  %
  \left\{\,
  A ⊆ \{1,2,3,4,5\}
  \,\middle|\,
  \pmat{\cond12 \;\;\&\;\; \cond13 \;\;\& \\ \cond24 \;\;\&\;\; \cond34 \;\;\& \\ \cond45}
  \,\right\}
$$

}

\end{document}

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