|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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}& &\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}
$$
\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: