% istanbul-july.tex: a LateXed version of notes handwritten just after
% the UniLog 2015 in Istanbul.
%
% (find-angg "LATEX/istanbul-july.tex")
% (find-angg "LATEX/istanbul-july.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex istanbul-july.tex"))
% (defun c () (interactive) (find-LATEXsh "lualatex --output-format=dvi istanbul-july.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/istanbul-july.pdf"))
% (defun d () (interactive) (find-xdvipage "~/LATEX/istanbul-july.dvi"))
% (defun e () (interactive) (find-LATEX "istanbul-july.tex"))
% (defun l () (interactive) (find-LATEX "istanbul-july.lua"))
% (find-xpdfpage "~/LATEX/istanbul-july.pdf")
% (find-xdvipage "~/LATEX/istanbul-july.dvi")
% (find-pen-links "cp -v ~/LATEX/istanbul-july.pdf /tmp/pen/")

% «.children»			(to "children")
%  «.brute-force»		(to "brute-force")

% «.ZHAs-are-topologies»	(to "ZHAs-are-topologies")
%  «.2-col-graphs»		(to "2-col-graphs")
%   «.drawpile»			(to "drawpile")

% «.J-operators»		(to "J-operators")
%  «.J-examples»		(to "J-examples")
%  «.sandwich»			(to "sandwich")
%  «.J-connectives»		(to "J-connectives")
%  «.no-Y-cuts»			(to "no-Y-cuts")
%  «.piccs»			(to "piccs")
%  «.alg-of-piccs»		(to "alg-of-piccs")
%   «.partitiongraph»		(to "partitiongraph")
%  «.zquotients»		(to "zquotients")
%  «.zquotients-alg»		(to "zquotients-alg")

% «.mixedpicture-tests»		(to "mixedpicture-tests")
% «.J-and-connectives»		(to "J-and-connectives")
% «.J-proofs»			(to "J-proofs")

\documentclass[oneside]{article}
%\documentclass[oneside]{book}
% (find-angg ".emacs.papers" "latexgeom")
% \usepackage[a4paper, landscape, top=1cm, left=1cm]{geometry} 
\usepackage[a4paper, top=2cm, left=2cm]{geometry} 
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage{tikz}
\usepackage{luacode}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")

% (find-dn6file "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

\usepackage{edrx15}  % (find-LATEX "edrx15.sty")
\input istanbuldefs  % (find-ist "defs.tex")

\begin{document}

% (find-dn6 "tests/1.tex")
%
\catcode`\^^J=10                              % (find-es "luatex" "spurious-omega")
\directlua{dednat6dir = "../dednat6/"}        % (find-LATEX "" "dednat6")
\directlua{dofile(dednat6dir.."dednat6.lua")} % (find-dn6 "dednat6.lua")
\directlua{texfile(tex.jobname)}
\directlua{quiet()}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\pu{\directlua{pu()}}
\pu

\catcode`=13 \def{\ensuremath{\bullet}}
% (find-LATEX "edrx15.sty" "colors")
\edrxcolors
\def\bhbox{\bicolorhbox}

\newpage

\def\St{\mathsf{St}}
\def\Cuts{\mathsf{Cuts}}

%L forths["="] = function () pusharrow("=") end





%   ____ _     _ _     _                
%  / ___| |__ (_) | __| |_ __ ___ _ __  
% | |   | '_ \| | |/ _` | '__/ _ \ '_ \ 
% | |___| | | | | | (_| | | |  __/ | | |
%  \____|_| |_|_|_|\__,_|_|  \___|_| |_|
%                                       
% «children» (to ".children")
\section{Children}


% A good way to explain logic for children is to start by how to
% evaluate logic expressions - {\sl propositions} -, and by analyzing
% which propositions are always true - the {\sl tautologies}. We can do
% that with very little mathematical baggage, using comparison with
% evaluation in algebra, and truth tables:
% 
%    (algebra)  (proposition)
%               (truth tables)
% 
% If we write the result of each subexpression right under its central
% connective, we get a much more compact notation that lets us calculate
% all the results of a proposition easily:
% 
% 
%   P  Q
% 
%          ^
%       look here
% 
% A logic (for children) is what we need to be able to evaluate
% propositions and determine whether a given propositions is a tautology
% or not. This is just:
% 
%   Omega, operations
% 
% The part that is left out and postponed to a second moment ``because
% it is not so much for children'' will be discussed at section ... .
% 
% 
% 
% Basic mathematical objects
% ==========================
% pairs ans sets
% functions
% lambda
% 
% 
% A glimpse at a 3-valued logic
% =============================
% Now an adult comes and says: let's look at this logic -
% 
%   slash logic tables
% 
% where 01 is a truth-value that is somehow between "true" and "false".
% He says that it has fewer tautologies than ``classical logic'', which
% is the one with Omega={0,1} in section ...; we calculate the
% truth-tables for ..., ..., and ... together, and we discover that here 
% 
% 
% 
% A logic as a basic mathematical object
% ======================================
% 
% 
% 
% 
% 
% 
% ZSet, ZDAGs and ZFunctions
% ==========================
% A ZSet is a finite, non-empty subset of N^2 that touches both axes,
% i.e., has at least one point with $x=0$ and one with $y=0$. The nice
% thing about ZSets is that they can represented very compactly using a
% bullet notation; for example, housetail has these points:
% 
%   housetail points
% 
% Every finite, non-empty subset of N^2 can be translated left and down
% until it touches both axes; this yields a ZSet that has the same shape
% as the original set.
% 
% There are two natural ways of adding arrows to a ZSet $A$ to turn it
% into a directed, acyclical graph. Imagine a game, played on the points
% of $A$, in which black pieces move downwards to a neighbouring point
% in A, and white pieces move similarly, but upwards. Let BM(A) subset
% AxA denote the set of ``black moves'' on A on WM(A) subset AxA denote
% the set of ``white moves''. So, for example, these are DAGs:
% 
%   (K,BM(K)) = figure = bigpair
% 
%   (K,WM(K)) = figure = bigpair
% 
% Now forget all other expectations about the game on a ZSet, like
% initial positions, captures, and winning - mentioning a ``game'' is
% just a trick that makes people understand BM and WM quickly.
% 
% \msk
% 
% A ZDAG is a DAG of the form (A,BM(A)) or (A,WM(A)), where A is a ZSet.
% 
% If (A,R subset AxA) is a graph, we will write R^* for the
% transitive-reflexive closure of R. A ZPoset is a graph of the form
% (A,BM(A)^*) or (A,WM(A)^*) where A is a ZSet.
% 
% \msk
% 
% A ZFunction is any function f:A->B, where A is a ZSet. We will use a
% positional notation for ZFunctions - for example,
% 
%   kiteread   is   f:kite -> N
%                     ...
% 
% If A is a ZSet with n points, the _reading order_ on A is the
% bijection from A to {1,...,n} that numbers all the points in A
% starting from the top line, and going from left to right in each line.
% These are some examples of reading orders:
% 
%   ...
% 
% We can use ZFunctions to denote subsets of a ZSet. For example,
% house10101 is {(1,2), (2,1), (2,0)}. This will be useful in section
% \ref{order-topologies}, where we will generalize the
% \Omega_\dagSlash of section \ref{3-valued-logic}.
% 
% 
% 
% 
% ZHAs
% ====
% A function F:{0,...,n}->N is _a series of white moves_ when for all y
% in {0,...,n-1} the arrow (F(y),y)->(F(y+1),y+1) is a white move. A ZHA
% is a ZSet that has a bottom point, a top point, and all the
% same-parity points bewteen its ``left wall'' and its ``right wall'',
% where both the left wall and the right wall are series of white moves.
% These are some examples of ZHAs:
% 
% % (find-xdvipage "~/LATEX/istanbul1.dvi" (+ 21 12))
% 
% Formally, a ZHA is generated by a triple (maxy, L, R), where:
% 
% % (find-xdvipage "~/LATEX/istanbul1.dvi" (+ 21 14))
% 
% Given a triple (maxy, L, R) obeying the conditions above, the ZHA
% generated by it is:
% 
%   {(x,y) in N^2 | y in {0,...,maxy}, x in {L(y), L(y+2), ..., R(y)}}
% 


%  ____             _          __                    
% | __ ) _ __ _   _| |_ ___   / _| ___  _ __ ___ ___ 
% |  _ \| '__| | | | __/ _ \ | |_ / _ \| '__/ __/ _ \
% | |_) | |  | |_| | ||  __/ |  _| (_) | | | (_|  __/
% |____/|_|   \__,_|\__\___| |_|  \___/|_|  \___\___|
%                                                    
% «brute-force» (to ".brute-force")
\subsection{Brute force}
% (find-ist "-handouts.tex" "brute-force")

%L require "stacks"

%L -- (find-dn6 "picture.lua" "metaopts")
%L metaopts["z2"]  = {scale="7pt", meta="s"} 
%L metaopts["z1"]  = {scale="5pt", meta="s"} 
%L mpnew({def="Bru", scale="2pt", meta="t"}, "1234321"):zhabullets():output()

\pu
Calculating $21∧12$ by brute force (in $\Bru$):
%
%L luarecteval [[
%L ra, rb, rc =
%L 1/   0   \, 1/   0   \, 1/   0   \    
%L  |  0 0  |   |  0 0  |   |  0 0  |    
%L  | 0 0 0 |   | 0 0 0 |   | 0 0 0 |    
%L  |0 1 0 0|   |0 0 1 0|   |0 0 0 0|    
%L  | 1 1 0 |   | 0 1 1 |   | 0 1 0 |    
%L  |  1 1  |   |  1 1  |   |  1 1  |    
%L  \   1   /   \   1   /   \   1   /    
%L ra:zhatomixedpicture({def="randa", meta="z1"}):output()
%L rb:zhatomixedpicture({def="randb", meta="z1"}):output()
%L rc:zhatomixedpicture({def="randc", meta="z1"}):output()
%L ]]
%
% (P <= Q & R) <-> (P <= Q) & (P <= R)
%       21 12           21         12
%       -----       ------     ------
%         ?          \ra        \rb
%  ----------      -------------------
%    \rd                   \rc
%
%L ubs_brute_force_and
%L = ubs [[
%L   P   Q 21 u   R 12 u  \& bin ? u   \le bin \rd u ()
%L   P   Q 21 u   \le bin \ra u ()
%L   P   R 21 u   \le bin \rb u ()
%L   \& bin \rc u
%L   \bij bin
%L ]]
%
$$\pu
  \def\ra{\randa}
  \def\rb{\randb}
  \def\rc{\randc}
  \def\rd{\randc}
  \def\ra{\sm{λP.(P≤21)       = \\ \randa}}
  \def\rb{\sm{λP.(P≤12)       = \\ \randb}}
  \def\rc{\sm{λP.((P≤21)∧(P≤12)) = \\ \randc}}
  \def\rd{\sm{λP.(P≤(21∧12)) = \\ λP.(P≤?) = \\ \randc}}
  \Expr{ubs_brute_force_and}
$$
   

Calculating $21{→}12$ by brute force (in $\Bru$):
%
%L luarecteval [[
%L ra, rb =
%L 2/      21      \, 1/   0   \
%L  |    21  21    |   |  0 0  |
%L  |  21  21  11  |   | 0 0 1 |
%L  |20  21  11  01|   |0 0 1 1|
%L  |  20  11  01  |   | 0 1 1 |
%L  |    10  01    |   |  1 1  |
%L  \      00      /   \   1   /
%L ra:zhatomixedpicture({def="rimpa", meta="z2"}):output()
%L rb:zhatomixedpicture({def="rimpb", meta="z1"}):output()
%L ]]
%
%  (P <= Q -> R) <-> (P &  Q <= R )
%        21  12           21    12
%        ------       ------
%          ?           \Ra
%  -------------     --------------
%     \Rc                   \Rb
%
%L ubs_brute_force_imp
%L = ubs [[
%L   P   Q 21 u   R 12 u   \to bin ? u    \le bin \Rc u ()
%L   P   Q 21 u   \& bin \Ra u   R 12 u   \le bin \Rb u ()
%L   \bij bin
%L ]]
%
$$\pu
  \def\Ra{\sm{λP.(P∧21)       = \\ \rimpa}}
  \def\Rb{\sm{λP.((P∧21)≤12)  = \\ \rimpb}}
  \def\Rc{\sm{λP.(P≤(21→12)) = \\ λP.(P≤?) = \\ \rimpb}}
  \Expr{ubs_brute_force_imp}
$$








%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  ______   _    _                           _                            
% |__  / | | |  / \   ___    __ _ _ __ ___  | |_ ___  _ __  ___ _ __  ___ 
%   / /| |_| | / _ \ / __|  / _` | '__/ _ \ | __/ _ \| '_ \/ __| '_ \/ __|
%  / /_|  _  |/ ___ \\__ \ | (_| | | |  __/ | || (_) | |_) \__ \ |_) \__ \
% /____|_| |_/_/   \_\___/  \__,_|_|  \___|  \__\___/| .__/|___/ .__/|___/
%                                                    |_|       |_|        
% «ZHAs-are-topologies» (to ".ZHAs-are-topologies")
\section{ZHAs are topologies}

%  ____                 _                         _         
% |___ \       ___ ___ | |   __ _ _ __ __ _ _ __ | |__  ___ 
%   __) |____ / __/ _ \| |  / _` | '__/ _` | '_ \| '_ \/ __|
%  / __/_____| (_| (_) | | | (_| | | | (_| | |_) | | | \__ \
% |_____|     \___\___/|_|  \__, |_|  \__,_| .__/|_| |_|___/
%                           |___/          |_|              
%
% «2-col-graphs» (to ".2-col-graphs")
\subsection{2-Column graphs}

A 2-column graph is a graph like the one in the picture below,
composed of a {\sl left column} $4\_→3\_→2\_→1\_→0\_$, a {\sl right
  column} $6\_→5\_→4\_→3\_→2→1\_→0\_$, and some intercolumn arrows:
$4\_→\_2$, $1\_→\_3$ going from the left column to the right column,
$\_5→4\_$ going from the right column to the left column.
%
%L -- «drawpile» (to ".drawpile")
%L drawpile = function (x, y, dy, A, B, arrow)
%L     local runstr = function (str) print(str) end
%L     local runstr = function (str) dxyrun(str) end
%L     local runf = function (fmt, ...) runstr(format(fmt, ...)) end
%L     runf "(("
%L     A = split(A)
%L     B = B and split(B)
%L     for i=1,#A do
%L       runf("node: %d,%d %s", x, y+dy*(i-1), A[i])
%L       if B then runf(".tex= %s", B[i]) end
%L       if not arrow then runf("place") end
%L     end
%L     if arrow then
%L       for i=1,#A-1 do
%L         runf("%s %s %s", A[i], A[i+1], arrow)
%L       end
%L     end
%L     runf "))"
%L   end
%
%D diagram piles0
%D 2Dx     100
%D 2D  100
%D 2D
%D 2D  +20
%D 2D
%L drawpile(100, 100, -15, "L1 L2 L3 L4",       "1\\_ 2\\_ 3\\_ 4\\_", "<-")
%L drawpile(120, 100, -15, "R1 R2 R3 R4 R5 R6", "\\_1 \\_2 \\_3 \\_4 \\_5 \\_6", "<-")
%D (( L1 R3 -> L4 R2 ->
%D    L4 R5 <-
%D ))
%D enddiagram
%D
$$\pu \left(\diag{piles0}\right)$$

A compact way to specify a 2-column graph is this: (left height, right
height, left-to-right arrows, right-to-left arrows). In the graph of
the example this is $(5, 7, \{4\_→\_2, 1\_→\_3\}, \{4\_ \ot\_5\})$.

We need to attribute a precise meaning for $0\_$, $…$, $4\_$ and
$\_0$, $…$, $\_6$. For the moment let's use this one, in which they
are points in $\N^2$ with $x=0$ or $x=2$:
%
$$\def\li#1 #2 #3 #4 {#1:=#2 && #3:=#4}
  \begin{array}{ccc}
     \vdots && \vdots   \\
    \li 3\_ (0,3) \_4 (2,4) \\
    \li 2\_ (0,2) \_2 (2,2) \\
    \li 1\_ (0,1) \_1 (2,1) \\
    \li 0\_ (0,0) \_0 (2,0) \\
  \end{array}
$$

% Later we will see a different way of identifying the points of the
% columns with points of $\R^2$, that is more complex but quite
% convenient.

Let's write $(5, 7, \{…\}, \{…\})^*$ for the transitive-reflexive
closure of of the graph, and $\Opens(5, 7, \{…\}, \{…\})$ for its
order topology.

\msk

%L twopiledef = function (def, zrect)
%L     MixedPicture.new({def=def, meta="t p", scale="3.5pt"}):zfunction(zrect):output()
%L   end
%L twopiledef("ThreeFourR", "..1|2.3|4.5|6.7")

Every open set of a 2-column graph is made of a pile of $a$ elements
at the bottom of the left column and a pile of $b$ elements at the
bottom of the right column. If we write these ``2-piles'' as $ab$,
%
\pu
\def\ThreeFour#1#2#3#4#5#6#7{\ThreeFourR#4#1#5#2#6#3#7}
$$\ThreeFour 001 0111 ≡ \{1\_, \_3, \_2, \_1\} ≡ 13$$
%
the connection with ZHAs becomes clear:
%
%L mpnew({scale="23pt", def="Piles"}, "1234R321"):zhapiledefs():print():lprint():output()
\def\foo#1#2{#1\!≡\!\!\ThreeFour#2}
$$
  \pu
  \Opens(3, 4, \{\}, \{\}) \qquad = \qquad \quad
  \Piles
$$

What happens if we add a left-right arrow, for example $2\_→\_2$?

%D diagram piles1
%D 2Dx     100
%D 2D  100
%D 2D
%D 2D  +20
%D 2D
%L drawpile(100, 100, -15, "L1 L2 L3",    "1\\_ 2\\_ 3\\_",      "<-")
%L drawpile(120, 100, -15, "R1 R2 R3 R4", "\\_1 \\_2 \\_3 \\_4", "<-")
%D (( L2 R2 ->
%D
%D ))
%D enddiagram
%D
$$\pu
  (3, 4, \{2\_→\_2\}, \{\}) \qquad = \qquad \quad
    \left(\diag{piles1}\right)
$$

Its effect is to make all the 2-piles of the form $\ThreeFour ?1?
??0?$ {\sl non}-open --- more simply, the ones of the form $\ThreeFour
?11 000?$, which are $\foo{20}{011 0000}$, $\foo{21}{011 0001}$,
$\foo{30}{111 0000}$, $\foo{31}{111 0001}$. We have:
%
%L mpnew({scale="23pt", def="Piles"}, "12RR3L21"):zhapiledefs():print():lprint():output()
\def\foo#1#2{#1\!≡\!\!\ThreeFour#2}
$$
  \pu
  \Opens(3, 4, \{2\_→\_2\}, \{\}) \qquad = \qquad \quad
  \Piles
$$

Graphica

like this,

we see that a topology like $\Opens(3, 4, \{\}, \{\})$ is a ZHA:



%L luarecteval [[
%L ra, rb, rc =
%L 2/                48        \, 2/            48        \, 2/            48    \
%L  |              47  38      |   |          47  38      |   |          47  38  |
%L  |            46  37  28    |   |        46  37  28    |   |        46  37    | 
%L  |          45  36  27  18  |   |      45  36  27  18  |   |          36      |
%L  |        44  35  26  17  08|   |    44  35  26  17  08|   |        35  26    |
%L  |      43  34  25  16  07  |   |  43  34  25  16  07  |   |      34  25  16  |
%L  |    42  33  24  15  06    |   |    33  24  15  06    |   |    33  24  15  06| 
%L  |  41  32  23  14  05      |   |      23  14  05      |   |      23  14  05  |
%L  |40  31  22  13  04        |   |    22  13  04        |   |    22  13  04    |
%L  |  30  21  12  03          |   |  21  12  03          |   |  21  12  03      |
%L  |    20  11  02            |   |20  11  02            |   |20  11  02        | 
%L  |      10  01              |   |  10  01              |   |  10  01          |
%L  \        00                /   \    00                /   \    00            /
%L print(ra:spec(), rb:spec(), rc:spec())
%L --> 12345RRRR4321	123RRR45R4321	123RRR43212R1
%L ra:zhatomixedpicture({def="ra", meta="8pt"}):output()
%L rb:zhatomixedpicture({def="rb"}):output()
%L rc:zhatomixedpicture({def="rc"}):output()
%L ]]

\pu 
$$\Opens(4, 8, \{\}, \{\}) \qquad = \qquad \ra$$
$$\Opens(4, 8, \{3\_→\_3\}, \{\}) \qquad = \qquad \rb$$
$$\Opens(4, 8, \csm{4\_→\_6 \\ 3\_→\_3}, \csm{3\_←\_7}) \qquad = \qquad \rc$$











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

%      _                                  _           
%     | |   _____  ____ _ _ __ ___  _ __ | | ___  ___ 
%  _  | |  / _ \ \/ / _` | '_ ` _ \| '_ \| |/ _ \/ __|
% | |_| | |  __/>  < (_| | | | | | | |_) | |  __/\__ \
%  \___/   \___/_/\_\__,_|_| |_| |_| .__/|_|\___||___/
%                                  |_|                
% «J-examples» (to ".J-examples")
\subsection{Examples of J-operators}
\label{J-examples}

% (find-istfile "quotes.tex")
% (find-istfile "quotes.tex" "fourman")
% (find-xdvipage "~/LATEX/istanbulquotes.dvi" 3)


%L zhafromspec = function (spec)
%L     MixedPicture.new({}, ZHA.fromspec(spec)):zhalr():output()
%L   end
\pu
\def\zhafromspec#1{\directlua{zhafromspec("#1")}}

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



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


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


%L spec = "123454321"
\pu
$$
\begin{array}{rccc}
(v)  & J_a∧J^a = ⊥       &&         % J_a∧J^a = ⊥      
    \jout{Cloq(v"21"), "21"} ∧
    \jout{Opnq(v"21"), "21"} =
    \jout{Falq(), ""}          \\ \\
(vi) & J_a∨J^a = ⊤       &&         % J_a∨J^a = ⊤      
    \jout{Cloq(v"21"), "21"} ∨
    \jout{Opnq(v"21"), "21"} =
    \jout{Truq(), ""}          \\ \\
(ix) & J_a∨B_a = B_a      &&        % J_a∨B_a = B_a    
    \jout{Cloq(v"21"), "21"} ∨
    \jout{Booq(v"21"), "21"} =
    \jout{Booq(v"21"), "21"}   \\ \\
(x)  & J^a∨B_b = B_{a→b} &&        % J^a∨B_b = B_{a→b}
    \jout{Booq(v"21"), "21"} ∨
    \jout{Booq(v"12"), "12"} =
    \jout{Booq(v"14"), "21 12 14"} \\
\end{array}
$$



















$$\showJ{1234RR321}{P -> z:Imp(v"12", P)}
  \quad
  \showJ{1234RR321}{P z:Or(v"12", P)}
  \quad
  \showJPs{1234RR321}{P z:Or(v"12", P)}{12}
$$


$$\zhafromspec{1234R321}$$






%                      _          _      _     
%  ___  __ _ _ __   __| |_      _(_) ___| |__  
% / __|/ _` | '_ \ / _` \ \ /\ / / |/ __| '_ \ 
% \__ \ (_| | | | | (_| |\ V  V /| | (__| | | |
% |___/\__,_|_| |_|\__,_| \_/\_/ |_|\___|_| |_|
%                                              
% «sandwich» (to ".sandwich")
\subsection{The sandwich lemma}
\label{sandwich}

The {\sl sandwich lemma} says that if $P≤Q≤P^*$, then $P=^*Q$:
%:  
%:                                    Q≤P^*                  
%:                                 ----------Mo     ----------M2
%:                        P≤Q      Q^*≤P^{**}      P^{**}=P^*  
%:                      -------Mo  -----------M2    -------------  
%:  P≤Q  Q≤P^*          P^*≤Q^*         Q^*≤P^*              
%:  ----------Sa        -----------------------              
%:    P^*=Q^*      :=        P^*=Q^*            
%:
%:    ^sand1                 ^sand2
%:
\pu
$$\ded{sand1} \quad := \quad \ded{sand2}$$

Let's use the notation of closed interval, $[P,R]$, for the set of all
points between $P$ and $R$ (in the partial order $≤$ of the ZHA):
%
$$[P,R] := \setofst{Q∈Ω}{P≤Q≤R}$$

We saw that $Q∈[P,P^*]$ implies $P =^* Q$, which means that all points
in $[P,P^*]$ are ${}^*$-equal, and that the equivalence class $[P]^*$
contains at least the set $[P,P^*]$ -- which is never empty, because
$M1$ tells us that $P≤P^*$, so
%
$$\mat{P≤P  ≤P^* \to P  ∈[P,P^*], \\
       P≤P^*≤P^* \to P^*∈[P,P^*]. \\
}
$$

Let's call a non-empty set of the form $[P,R]$ a {\sl lozenge}, even
though it may inherit some dents from the ambient ZHA, as here:
%
$$[11,33] = (diagram)$$

If $P_1^* = P_2^*$, then the equivalence class $[P_1]^*$ ($= [P_2]^*$)
contains the union of the lozenges $[P_1, P_1^*]$ and $[P_2, P_2^*] =
[P_2, P_1^*]$. If $42^* = 33^* = 14^* = 56$, then
%
$$\mat{
  [42]^* = [33]^* = [14]^* ⊇ \\
  [42,56] ∪ [33,56] ∪ [14,56] \\
  }
$$
%
so each equivalence class $[P]^*$ is a union of lozenges or the form
$[\_, P^*]$; and if $[P_1]^* = \setof{P1, P_2, \ldots, P_n}$ then
$[P_1]^* = [P_1,P_1^*] ∪ [P_2,P_1^*] ∪ \ldots ∪ [P_n,P_1^*]$.

\msk

Let's go back to the example above, where $42^* = 33^* = 14^* = 56$.
We have
%
$$\begin{array}{rcl}
  ((42∧33)∧14)^* &=& \\
  (42∧33)^*∧14^* &=& \\
  (42^*∧33^*)∧14^* &=& \\
  (56∧56)∧56 &=& 56, \\
  \end{array}
$$
%
so $42∧33∧14$ is in the same equivalence class as 42, 33, and 14. We
have $[12, 56] ⊆ [42]^* = [33]^* = [14]^*$, which means this shape:
%
%L luarecteval [[
%L ra, rb =
%L 2/          ..        \, 2/          ..        \
%L  |        ..  ..      |   |        ..  ..      |
%L  |      ..  ..  ..    |   |      ..  ..  ..    |
%L  |    ..  65  ..  ..  |   |    ..  65  ..  ..  |
%L  |      **  **  ..  ..|   |      **  **  ..  ..|
%L  |        **  **  ..  |   |        **  **  ..  |
%L  |      **  **  **  ..|   |      **  **  **  ..|
%L  |    **  **  **  **  |   |    **  **  **  **  |
%L  |  ..  42  33  **    |   |  ..  42  33  **    |
%L  |..  ..  ..  ..  14  |   |..  ..  **  **  14  |
%L  |  ..  ..  ..  ..  ..|   |  ..  ..  **  **  ..|
%L  |    ..  ..  ..  ..  |   |    ..  ..  12  ..  |
%L  |      ..  ..  ..    |   |      ..  ..  ..    |
%L  |        ..  ..      |   |        ..  ..      |
%L  \          ..        /   \          ..        /
%L ]]
%L ra:zhatomixedpicture({def="ra"}):addcontour():output()
%L rb:zhatomixedpicture({def="rb"}):addcontour():output()
$$\pu (FIX THIS!!!) \ra \rb$$

\newpage

(...)

%:
%:
%:
%:                        P_1^*=P_2^*
%:                       ==============
%:  P_1=^*P_2            P_1^*∧P_2^*=P_1^*
%:  -----------ECC∧      =================M3
%:  P_1∧P_2=^*P_1    :=  (P_1∧P_2)^*=P_1^*
%:
%:  ^Eqcand-1             ^Eqcand-2
%:                                                    ---------M1
%:                                                    P_2≤P_2^*    P_2^*=P_1^*
%:                                       ---------M1  ------------------------
%:                                       P_1≤P_1^*       P_2≤P_1^*
%:                          -----------  -------------------------
%:  P_1=^*P_2               P_1≤P_1∨P_2  P_1∨P_2≤P_1^*
%:  -------------ECC∨       --------------------------Sa
%:  P_1=^*P_1∨P_2      :=   P_1^*=(P_1∨P_2)~*
%:
%:  ^Eqcor-1                ^Eqcor-2
%:
%:
%:                        P^*=Q^*
%:                       ==========
%:  P=^*Q                P^*∧Q^*=P*
%:  -----------ECC∧      ===========M3
%:  P∧Q=^*P          :=  (P∧Q)^*=P^*
%:
%:  ^Eqcand-1             ^Eqcand-2
%:                                    -----M1
%:                                    Q≤Q^*    Q^*=P^*
%:                           -----M1  ----------------
%:                           P≤P^*       Q≤P^*
%:                    -----  -----------------
%:  P=^*Q             P≤P∨Q  P∨Q≤P^*
%:  -------ECC∨      ----------------Sa
%:  P=^*P∨Q      :=   P^*=(P∨Q)~*
%:
%:  ^Eqcor-1          ^Eqcor-2
%:
\pu
$$\begin{array}{rcl}
  \ded{Eqcand-1} &:=& \ded{Eqcand-2} \\\\
  \ded{Eqcor-1}  &:=& \ded{Eqcor-2} \\\\
  \end{array}
$$

% $$\ded{Eqcand-1} \qquad := \qquad \ded{Eqcand-2}$$
% $$\ded{Eqcor-1}  \qquad := \qquad \ded{Eqcor-2}$$


%      _                                   _   _                
%     | |   ___ ___  _ __  _ __   ___  ___| |_(_)_   _____  ___ 
%  _  | |  / __/ _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|
% | |_| | | (_| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \
%  \___/   \___\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/
%                                                               
% «J-connectives» (to ".J-connectives")
\subsection{How J-operators interact with connectives}
\label{J-connectives}

\def\eightH#1#2#3#4#5#6#7#8#9{
  \put(0,#1){\cell{#2}}
  \put(1,#1){\cell{#3}}
  \put(2,#1){\cell{#4}}
  \put(3,#1){\cell{#5}}
  \put(4,#1){\cell{#6}}
  \put(5,#1){\cell{#7}}
  \put(6,#1){\cell{#8}}
  \put(7,#1){\cell{#9}}
}
\def\eightLines#1#2#3#4#5#6#7#8{\vcenter{\hbox{\unitlength=6pt%
\celllower=2pt%
\def\cellfont{\scriptsize}%
\begin{picture}(8,8)(-0.5,-0.5)
  \eightH 7 #1
  \eightH 6 #2
  \eightH 5 #3
  \eightH 4 #4
  \eightH 3 #5
  \eightH 2 #6
  \eightH 1 #7
  \eightH 0 #8
\end{picture}}}}

$$\eightLines{········}{·······1}{·······1}{·······1}{·····11·}{····1·1·}{····11··}{·111····}
  \quad
  \eightLines{·······1}{······11}{·····1·1}{····1··1}{···1·111}{··1·1·11}{·1··11·1}{11111111}
  \quad
  \eightLines{·111····}{····11··}{····1·1·}{·····11·}{·······1}{·······1}{·······1}{········}
  \quad
  \eightLines{11111111}{·1··11·1}{··1·1·11}{···1·111}{····1··1}{·····1·1}{······11}{·······1}
$$




%D diagram cube-with-numbers
%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      ==>     1 
%D ren  A2 A3 A4   ==>   2 3 4
%D ren  A5 A6 A7   ==>   5 6 7
%D ren     A8      ==>     8 
%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-with-numbers}$$

%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-and*-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 <-   A3 A6 =
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%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
%
$$\pu
  \diag{cube-and*-0}
  \quad
  \diag{cube-and*-1}
  \quad
  \diag{cube-and*-2}
$$





%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-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
%
$$\pu
  \def∨{{\lor}}
  \diag{cube-or*-0}
  \quad
  \diag{cube-or*-1}
$$


%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
%
%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
  \def→{{\to}}
  \diag{cube-imp*-0}
  \quad
  \diag{cube-imp*-1}
$$







%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
  \andStarCubeArchetypal
  \qquad
  \orStarCubeArchetypal
  \qquad
  \impStarCubeArchetypal
$$


$$ \begin{array}{l}
   P^*∧Q^* \overset{(M3)}{=} (P∧Q)^* \\
   (P^*∧Q^*)^* \overset{(M3)}{=} (P∧Q)^{**} \overset{(M2)}{=} (P∧Q)^* \\
   \end{array}
$$



%:
%:     ------\iota      -------\iota'
%:     P≤P∨Q           Q≤P∨Q
%:  ------------Mo  -----------Mo
%:  P^*≤(P∨Q)^*     Q^*≤(P∨Q)^*
%:  ---------------------------[,]
%:       P^*∨Q^*≤(P∨Q)^*
%:    ----------------------Mo
%:    (P^*∨Q^*)^*≤(P∨Q)^{**}  
%:    --------------------------M2
%:        (P^*∨Q^*)^*≤(P∨Q)^*
%:
%:          ^or*-extra-arrow-proof
%:
\pu
$$\ded{or*-extra-arrow-proof}
$$

% (find-dvipage "~/LATEX/2008graphs.dvi" 24)
% (find-fline "~/LATEX/2008graphs.tex")

%:
%:
%:  -------------\id
%:  P→Q^*≤P→Q^*
%:  -------------♭
%:  (P→Q^*)∧P≤Q^*
%:  ----------------------Mo
%:  ((P→Q^*)∧P)^*≤Q^{**}
%:  ----------------------M2
%:  ((P→Q^*)∧P)^*≤Q^*
%:  ----------------------M3
%:  (P→Q^*)^*∧P^*≤Q^*  
%:  -----------------♯ 
%:  (P→Q^*)^*≤P^*→Q^*
%:
%:  ^imp*-extra-arrow-proof
%:  
$$\pu
  \def→{{\to}}
  \ded{imp*-extra-arrow-proof}
$$



%  _   _        __   __             _       
% | \ | | ___   \ \ / /   ___ _   _| |_ ___ 
% |  \| |/ _ \   \ V /   / __| | | | __/ __|
% | |\  | (_) |   | |   | (__| |_| | |_\__ \
% |_| \_|\___/    |_|    \___|\__,_|\__|___/
%                                           
% «no-Y-cuts» (to ".no-Y-cuts")
\subsection{There are no Y-cuts}
\label{no-Y-cuts}

%L mp = MixedPicture.new({def="SmallLo", meta="s", scale="5pt"}):zfunction(".1.|2.3|.4."):output()
%L mp = MixedPicture.new({def="SmallLo", meta="t b", scale="4.5pt"}):zfunction(".1.|2.3|.4."):output()
\pu
$a \SmallLo{12}{34}{56}{78} b$

%L mp = MixedPicture.new({def="SmallLo", meta="t", scale="5pt"}):zfunction(".1.|2.3|.4."):output()
\def\smalo#1#2#3#4#5#6#7#8{\SmallLo{#1#2}{#3#4}{#5#6}{#7#8}}
\pu
$a \SmallLo{12}{34}{56}{78} b$

A {\sl small lozenge} in a ZHA is four points like $\{...\}$ or
$\{...\}$ in the figure below; we will write these small lozenges as
$\smalo 12 34 56 78$ and ... .

When the points in a small lozenge $L$ belong to four different
equivalence classes, like in ..., we say that $L$ is an {\sl X-cut};
when they belong to three different equivalence classes, like ... or
..., a {\sl Y-cut}; two different equivalence classes, like ... or
..., an {\sl I-cut}; one equivalence class, a {\sl no-cut}.

We saw in section \ref{sandwich} that equivalence classes are
lozenges. Let's now see that the frontiers between equivalence classes
can't be more irregular than the examples in section \ref{J-examples}.

Every way of dividing a ZHA $A$ into lozenges induces an operation
$·^*: A → A$ that takes each element to the top element of its
equivalence class; this `$·^*$' obeys axiom M1 and M2...

We need two lemmas:







%  ____  _              
% |  _ \(_) ___ ___ ___ 
% | |_) | |/ __/ __/ __|
% |  __/| | (_| (__\__ \
% |_|   |_|\___\___|___/
%                       
% «piccs» (to ".piccs")
\subsection{Partitions into contiguous classes}
\label{piccs}

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 partition into contiguous classes, but $\{\{0,2\},\{1\}\}$ is not.

A partition of $\{0, \ldots, n\}$ into contiguous classes induces an
equivalence relation $· ∼_P ·$, a function $[·]_P$ that returns the
equivalence class of an element, 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, a set $\St_P
:= \setofst{a∈\{0, \ldots, n\}}{a^P=a}$ of the "stable" elements of
$\{0,...,n\}$, and 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 partitions into contiguous
classes from now on.



%     _    _                __         _              
%    / \  | | __ _    ___  / _|  _ __ (_) ___ ___ ___ 
%   / _ \ | |/ _` |  / _ \| |_  | '_ \| |/ __/ __/ __|
%  / ___ \| | (_| | | (_) |  _| | |_) | | (_| (__\__ \
% /_/   \_\_|\__, |  \___/|_|   | .__/|_|\___\___|___/
%            |___/              |_|                   
%
% «alg-of-piccs» (to ".alg-of-piccs")
\subsection{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'}$:
%
%% «partitiongraph» (to ".partitiongraph")
%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$.

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

The operations $∧$ and $∨$ are easy to understand in terms of cuts
(the "$|$"s):
%
$$\begin{array}{rcl}
  \Cuts(P∨Q) &=& \Cuts(P)∩\Cuts(Q) \\
  \Cuts(P∧Q) &=& \Cuts(P)∪\Cuts(Q) \\
  \end{array}
$$

The stable elements of a picc on $\{0, \ldots, n\}$ are the ones at
the left of a cut plus the $n$, so we have:
%
$$\begin{array}{rcl}
  \St(P∨Q) &=& \St(P)∩\St(Q) \\
  \St(P∧Q) &=& \St(P)∪\St(Q) \\
  \end{array}
$$

Here is a case that shows how $·^{P∨Q}$ can be problematic. The result
of $a^{P∨Q}$ must be stable by both $P$ and $Q$. Let:
%
$$\begin{array}{rcl}
   E  &:=& 01|2|34|56|789 \\
   O  &:=& 01|23|45|6|789 \\
   E∨O &=& 01|23456|789 \\
   E∧O &=& 01|2|3|4|5|6|789 \\
  \end{array}
$$

We can define $a^{P∧Q} := a^P∧a^Q$, and this always works. But
$a^{P∨Q} := a^P∨a^Q$ does not, we may have to do something like
iterating the two functions many times:
%
%D diagram OvaE
%D 2Dx     100 +40 +40
%D 2D  100     OvE
%D 2D
%D 2D  +40 O       E
%D 2D
%D 2D  +40    OandE
%D 2D
%D (( OvE .tex= \OvE 
%D    O .tex= O\;=\;01|23|45|6
%D    E .tex= E\;=\;0!12|34|56
%D    OandE .tex= \OandE
%D    OvE O   <-  OvE E <-
%D    O OandE <-  E OandE <-
%D ))
%D enddiagram
%D
%             O∨E = 0123456
%         2^(O∨E) = 6
%         a^(O∨E) = (((a^O)^E)^O)^E
%              ^       ^
%             /         \
%   O=01|23|45|6       E=0!12|34|56
%             ^         ^
%              \       /
%           O∧E = 0|1|2|3|4|5|6
%       2^(O∧E) = 2^O∧2^E=3∧2=2
%       a^(O∧E) = a^O∧a^E
%
$$\pu
  \def\OvE{\begin{array}{rcl}
          O∨E &=& 0123456 \\
          2^{O∨E} &=& 6 \\
          a^{O∨E} &=& (((a^O)^E)^O)^E \\
          \end{array}}
  \def\OandE{\begin{array}{rcl}
          O∧E &=& 0|1|2|3|4|5|6 \\
          2^{O∧E} &=& 2^O∧2^E=3∧2=2 \\
          a^{O∧E} &=& a^O∧a^E \\
          \end{array}}
  \diag{OvaE}
$$

The ``$→$'' in the algebra of piccs will not be relevant to us, so we
will not discuss it.



%  ________              _   _            _       
% |__  / _ \ _   _  ___ | |_(_) ___ _ __ | |_ ___ 
%   / / | | | | | |/ _ \| __| |/ _ \ '_ \| __/ __|
%  / /| |_| | |_| | (_) | |_| |  __/ | | | |_\__ \
% /____\__\_\\__,_|\___/ \__|_|\___|_| |_|\__|___/
%                                                 
% «zquotients» (to ".zquotients")
\subsection{ZQuotients}
\label{zquotients}

% (find-kopkadaly4page (+ 12 63) "\\scriptsize")
% (find-kopkadaly4text (+ 12 63) "\\scriptsize")
%L z = ZHA.fromspec("1R2R3212RL1")
%L mp = MixedPicture.new({def="ZQ", scale="2pt", meta="t"}, z):zhabullets():output()

A {\it ZQuotient} for a ZHA with top element 46 is a partition of
$\{0, \ldots ,4\}$ into contiguous classes (a ``partition of the left
wall''), plus a partition of $\{0, \ldots ,6\}$ into contiguous
classes (a ``partition of the right wall''). 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. The graphical notation is this
(for $4321/0\; 0123\bsl45\bsl6$ on $\pu \ZQ$):
%
%L z = ZHA.fromspec("1R2R3212RL1")
%L mp = MixedPicture.new({def="ZQuotients"}, z)
%L mp:zhalr():addcuts("c 4321/0 0123|45|6"):print():output()
%
%                /  \      
%                 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 in
section \ref{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}
$$



%  ________              _   _            _               _       
% |__  / _ \ _   _  ___ | |_(_) ___ _ __ | |_ ___    __ _| | __ _ 
%   / / | | | | | |/ _ \| __| |/ _ \ '_ \| __/ __|  / _` | |/ _` |
%  / /| |_| | |_| | (_) | |_| |  __/ | | | |_\__ \ | (_| | | (_| |
% /____\__\_\\__,_|\___/ \__|_|\___|_| |_|\__|___/  \__,_|_|\__, |
%                                                           |___/ 
% «zquotients-alg» (to ".zquotients-alg")
\subsection{The algebra of ZQuotients}
\label{zquotients-alg}

The ideas of the last section apply to ZQuotients, with a few
adjustments. The

$$\St(P∧Q) = \St(P)∪\St(Q)$$

would mean, for $P = 54/32/10$ and $Q = 01/23/45$, that

$$\St(P_cuts) = St($$








\end{document}





\end{document}







% (find-LATEX "edrx15.sty" "picture-cells")
%$$
% Hello \input /tmp/o.tex % (find-fline "/tmp/o.tex")
% \hbox{\input /tmp/o.tex } % (find-fline "/tmp/o.tex")
%\bhbox{\hbox{\input /tmp/o.tex }} % (find-fline "/tmp/o.tex")
%$$

%L -- (find-dn5 "newrect.lua" "asciirectpoints-tests")
%L
%L opts = {def="dagHouse", scale="4pt", meta="p b s"}
%L mp = MixedPicture.new(opts)
%L for x,y,c in asciirectpoints(".1.|2.3|4.5") do
%L   if c:match"%d" then
%L     mp:put(v(x, y), "#"..c)
%L     mp.lp.def = mp.lp.def.."#"..c
%L   end
%L end
%L output(mp:tolatex())
%L 
%L opts = {def="PvSTbullets", meta="p b s", scale="4pt"}
%L z = ZHA.fromspec("1234R3L21L"):print()
%L mp = MixedPicture.new(opts, z)
%L for v in z:points() do mp:put(v, "**") end
%L output(mp:tolatex())

\pu
a$\dagHouse54321 b \dagHouse b \PvSTbullets$c








% «mixedpicture-tests» (to ".mixedpicture-tests")
% (find-dn5 "newrect.lua" "MixedPicture-arch-tests")

%L
%L -- (&R) is *-functorial
%L z = ZHA.fromspec("1234R321")
%L mp = MixedPicture.new({def="andRIsStarFunctorial"}, z)
%L mp:addcuts("c 32/10 01|23|4")
%L mp = mpnew({def="andRIsStarFunctorial"}, "1234R321"):addcuts("c 32/10 01|23|4")
%L mp:put(v"30", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"22", "Q"):put(v"33", "Q*", "Q^*")
%L mp:put(v"04", "R"):put(v"14", "R*", "R^*"):output()
%L -- omp()
%L 
%L -- (Pv) is *-functorial
%L z = ZHA.fromspec("1234R3L21L")
%L mp = MixedPicture.new({def="PvIsStarFunctorial"}, z)
%L mp:addcuts("c 5432/10 0|12|34")
%L mp:put(v"20", "P"):put(v"30", "P*", "P^*")
%L mp:put(v"11", "Q"):put(v"12", "Q*", "Q^*")
%L mp:put(v"03", "R"):put(v"14", "R*", "R^*"):output()
%L -- omp()
%L 

$$
\pu
\PvIsStarFunctorial
\qquad
\andRIsStarFunctorial
\qquad
\andStarCubeArchetypal
\qquad
\orStarCubeArchetypal
\qquad
\impStarCubeArchetypal
$$






\newpage


%      _ 
%     | |
%  _  | |
% | |_| |
%  \___/ 
%        
% «J-proofs» (to ".J-proofs")
% (find-istfile "1.org" "P&Q, J(P)&Q, ...")
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008graphs.tex" "LT-modalities")
% (find-853page  21 "internal-diagram")
% (find-853page  22 "and")


Extras:

%:   01=_J23    45=_J67
%:  ---------  ---------
%:  0\_=_L2\_  \_5=_R\_7
%:  --------------------
%:        05=_W27
%:  
%:        ^JLRW
%:
%:
%:  P≤^*Q                        Q≤^*R                      
%:  -------def                   -------def                 
%:  P^*≤Q^*                      Q^*≤R^*                    
%:  -----------(∧R)_1            -----------(P∨)_1          
%:  P^*∧R≤Q^*≤R                  P∨Q^*≤P∨R^*                
%:  ----------------(*)_1        -------------------(*)_1   
%:  (P^*∧R)^*≤(Q^*≤R)^*          (P∨Q^*)^*≤(P∨R^*)^*        
%:  -------------------∧-cube    -------------------∨-cube  
%:  (P∧R)^*≤(Q∧R)^*              (P∨Q)^*≤(P∨R)^*            
%:  --------------- def          ---------------def         
%:  P∧R≤^*Q∧R                    P∨Q≤^*P∨R                  
%:                                                          
%:  ^and-R-is-star-functorial    ^P-or-is-star-functorial   
%:
\pu
$$\ded{JLRW}$$
$$\ded{and-R-is-star-functorial} \qquad \ded{P-or-is-star-functorial}$$

\end{document}


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