|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% 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}& &\text{#5}& \\}
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} (ii) J^a∨J^b = J^{a∧b}
\li (iii) J_a∧J_b = J_{a∧b} (iv) J^a∧J^b = J^{a∨b}
\li (v) J_a∧J^a = ⊥ (vi) J_a∨J^a = ⊤
\li (vii) J_a∨K = K∘J_a (viii) J^a∨K = J^a∘K
\li (ix) J_a∨B_a = B_a (x) J^a∨B_b = B_{a→b}
\end{array}
$$
% (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: