|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This file: (find-LATEX "2021planar-HAs-2.tex")
% Supersedes: (find-LATEX "2020J-ops-new.tex")
% (find-LATEX "2019J-ops.tex")
% (find-LATEX "2019J-ops-arxiv.tex")
% (find-LATEX "2017planar-has-2.tex")
% See: (find-TH "math-b" "zhas-for-children-2")
%
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021planar-HAs-2.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2021planar-HAs-2.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021planar-HAs-2.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021planar-HAs-2.pdf"))
% (defun e () (interactive) (find-LATEX "2021planar-HAs-2.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021planar-HAs-2"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2021planar-HAs-2.pdf"))
% (code-eec-LATEX "2021planar-HAs-2")
% (find-pdf-page "~/LATEX/2021planar-HAs-2.pdf")
% (find-sh0 "cp -v ~/LATEX/2021planar-HAs-2.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021planar-HAs-2.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021planar-HAs-2.pdf
% file:///tmp/2021planar-HAs-2.pdf
% file:///tmp/pen/2021planar-HAs-2.pdf
% http://angg.twu.net/LATEX/2021planar-HAs-2.pdf
% (find-LATEX "2019.mk")
% «.parts» (to "parts")
% «.0._front-matter» (to "0._front-matter")
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.toc» (to "toc")
% «.status» (to "status")
% «.background» (to "background")
% «.1._slashings» (to "1._slashings")
% «.basic-definitions» (to "basic-definitions")
% «.qms-and-slashings» (to "qms-and-slashings")
% «.piccs-and-slashings» (to "piccs-and-slashings")
% «.slash-ops» (to "slash-ops")
% «.converting» (to "converting")
% «.2._J-operators» (to "2._J-operators")
% «.J-operators» (to "J-operators")
% «.3._midway» (to "3._midway")
% «.cuts-stopping-midway» (to "cuts-stopping-midway")
% «.no-Y-cuts-no-L-cuts» (to "no-Y-cuts-no-L-cuts")
% «.4._cubes» (to "4._cubes")
% «.cubes» (to "cubes")
% «.5._valuations» (to "5._valuations")
% «.valuations» (to "valuations")
% «.6._algebra» (to "6._algebra")
% «.polynomial-J-ops» (to "polynomial-J-ops")
% «.algebra-of-piccs» (to "algebra-of-piccs")
% «.algebra-of-J-ops» (to "algebra-of-J-ops")
% «.slashings-are-poly» (to "slashings-are-poly")
% «.7._toposes» (to "7._toposes")
% «.some-bijections» (to "some-bijections")
% «.a-particular-case» (to "a-particular-case")
% «.ArtDecoN» (to "ArtDecoN")
% «.ArtDecoN-shortdefs» (to "ArtDecoN-shortdefs")
% «.ArtDecoN-bijdefs» (to "ArtDecoN-bijdefs")
% «.visual-intuition» (to "visual-intuition")
% «.arxiv» (to "arxiv")
% «.make» (to "make")
%\documentclass[oneside,12pt]{article}
\documentclass[oneside,11pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{tocloft} % (find-es "tex" "tocloft")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (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
%
% (find-dednat6file "demo-write-dnt.tex")
\usepackage{ifluatex}
\ifluatex
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\else
\usepackage[utf8]{inputenc}
\input edrx21chars-d.tex % (find-LATEX "edrx21chars-d.tex")
\fi
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
\def\superscriptOne {^{*}}
\def\superscriptTwo {^{**}}
\def\superscriptThree{^{***}}
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\ifluatex
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}
\else
\input\jobname.dnt % (find-LATEXfile "2021lindenhovius-j-to-X.dnt")
\def\pu{}
\fi
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
%L forths["<-->"] = function () pusharrow("<-->") end
\pu
\input 2019J-ops-defs.tex % (find-LATEX "2019J-ops-defs.tex")
\def\nuc{(·)^*}
\def\clop{\ovl{(·)}}
\def\calY{{\mathcal{Y}}}
\def\Cst{\mathsf{CST}}
\def\Can{\mathsf{Can}}
\def\can{\mathsf{can}}
\def\Incs {\mathsf{Incs}}
\def\inc {\mathsf{inc}}
\def\CanSub {\mathsf{CanSub}}
\def\SubPoints{\mathsf{SubPoints}}
\def\Subsets {\mathsf{Subsets}}
\def\GrTops {\mathsf{GrTops}}
\def\pmt #1{\pmat{\text{#1}}}
\def\pmtt #1#2{\pmat{\text{#1} \\ \text{#2}}}
\def\pmttt #1#2#3{\pmat{\text{#1} \\ \text{#2} \\ \text{#3}}}
\def\pmtttt#1#2#3#4{\pmat{\text{#1} \\ \text{#2} \\ \text{#3} \\ \text{#4}}}
\def\smt #1{\sm{\text{#1}}}
\def\smtt #1#2{\sm{\text{#1} \\ \text{#2}}}
\def\smttt #1#2#3{\sm{\text{#1} \\ \text{#2} \\ \text{#3}}}
\def\smtttt#1#2#3#4{\sm{\text{#1} \\ \text{#2} \\ \text{#3} \\ \text{#4}}}
% ____ _
% | _ \ __ _ _ __| |_ ___
% | |_) / _` | '__| __/ __|
% | __/ (_| | | | |_\__ \
% |_| \__,_|_| \__|___/
%
% «parts» (to ".parts")
% (p2ap 1 "parts")
% (p2aa "parts")
% (jopp 1 "parts")
% (jopa "parts")
% ___ _____ _ __ __ _ _
% / _ \ | ___| __ ___ _ __ | |_ | \/ | __ _| |_| |_ ___ _ __
% | | | | | |_ | '__/ _ \| '_ \| __| | |\/| |/ _` | __| __/ _ \ '__|
% | |_| | | _|| | | (_) | | | | |_ | | | | (_| | |_| || __/ |
% \___(_) |_| |_| \___/|_| |_|\__| |_| |_|\__,_|\__|\__\___|_|
%
% «0._front-matter» (to ".0._front-matter")
% (p2ap 1 "0._front-matter")
% (p2aa "0._front-matter")
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (p2ap 1 "title")
% (p2aa "title")
%\title{A Way to Visualize Nuclei on
% % Certain
% \\ Planar Heyting Algebras}
\title{Planar Heyting Algebras for Children 2:
J-Operators, Slashings, and Nuclei}
\author{Eduardo Ochs}
\maketitle
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% (p2ap 1 "abstract")
% (p2aa "abstract")
\begin{abstract}
Every topos admits several ``notions of sheafness'' on it; for
example, one is associated to booleanizing its logic, and for any
propositions $P$ and $Q$ on it there is one associated to ``forcing
$P→Q$ to be true''. How can we visualize them? Or, better: how can we
visualize them when we know very little Topos Theory?
Let $𝐃$ be a finite 2-column graph. Let $𝐄$ be the topos $\Set^𝐃$, and
let $H$ be its Heyting Algebra of truth-values: $H=\Sub(1_𝐄)$. Then
$H$ is a finite Planar Heyting Algebra (a ``ZHA''), and \cite{PH1}
shows how to use these ZHAs to visualize how Intuitionistic
Propositional Logic works. A {\sl nucleus} on a Heyting Algebra $H$ is
an operation $·^*:H→H$ that obeys $P≤P^*=P^{**}$ and
$(P∧Q)^*=P^*∧Q^*$; we will show to visualize these nuclei on Heyting
Algebras that are ZHAs, and how to use that as a first step towards
understanding the bijection between nuclei and notions of sheafness.
We will use the term {\sl J-operator} for a nucleus that acts on a
ZHA, and the first sections of this paper will be dedicated to: seeing
in elementary terms how these J-operators work, proving that each
J-operator on a ZHA $H$ corresponds to a way to slash $H$ by diagonal
cuts that do not stop midway, and seeing how to visualize some famous
J-operators, like booleanization and forcing.
In the last two sections we will see how to start from this knowledge
of J-operators to learn some Topos Theory. If the reader is willing to
believe a small list of (provable) statements then he will be able to
convert any J-operator $\nuc$ to the a Lawvere-Tierney topology $j$
and a sheafification functor on our topos $𝐄=\Set^𝐃$, and to visualize
in particular cases what many theorems in, say, \cite{BellLST},
``mean'' --- and to understand the theory by working on a particular
case and on the general case in parallel, using the techniques for
doing ``categories for children'' explained in \cite{FavC}.
\end{abstract}
\newpage
% _____ ___ ____
% |_ _/ _ \ / ___|
% | || | | | |
% | || |_| | |___
% |_| \___/ \____|
%
% «toc» (to ".toc")
% (p2ap 1 "toc")
% (p2aa "toc")
% (jonp 2 "toc")
% (jona "toc")
% (find-es "tex" "tocloft")
\renewcommand{\cfttoctitlefont}{\bfseries}
\setlength{\cftbeforesecskip}{2.5pt}
\tableofcontents
\vspace*{2.0cm}
% «status» (to ".status")
{\sl Status of these notes:} this is my $n$-th attempt to rewrite
these notes to make them publishable as a journal article, or at least
publishable on Arxiv. The sections
\ref{background}--\ref{slashings-are-poly} are practically in final
form; most of them are stable since 2019, but I rewrote the sections
\ref{background}--\ref{converting} and \ref{no-Y-cuts-no-L-cuts} in
August 2021 and I need to revise them. Everything from the section
\ref{toposes} onwards will be totally rewritten to make this paper
work a complement to \cite{ClopsAndTops} and \cite{FavC} and as a
preparation and motivation to them for people who know very little
Category Theory.
For the most recent version see:
\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}
\newpage
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «background» (to ".background")
% (p2ap 3 "background")
% (p2aa "background")
\setcounter{section}{-1}
\section{Background}
\label{background}
One of the main constructions of \cite{PH1} is a bijection between
(proper) 2-column graphs and Planar Heyting Algebras. For example, in
%
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=40, v=25, crv=7} -- with v arrows
%L tspec_PA = TCGSpec.new("35; 22, 24")
%L tspec_PA :mp ({zdef="O_A(P) 35"}) :addlrs():print() :output()
%L tspec_PA :tcgq({tdef="(P,A) 35", meta="1pt p"}, "lr q h v ap") :output()
%L
\pu
%
$$(P,A) = \tcg{(P,A) 35}
\qquad
H = \Opens_A(P) = \;\;\;\; \zha{O_A(P) 35}
$$
%
the 2-column graph $(P,A)$ has left height 3 and right height 5; its
set of points is
%
$$P \;\; = \;\; \pileelements{3}{5}
$$
%
and its set of arrows $A$ is made of all the vertical, or
intra-column, arrows going one step down plus two intercolumn arrows:
$2▁←▁4$ and $2▁→▁2$. We will use the 2-column graph $(P,A)$ above in all
examples in this section.
A {\sl pile} is a subset of $P$ of the form:
%
$$\pile(ab) \;\; = \;\; \pileelements{a}{b}
$$
%
We say that a subset $U⊆P$ {\sl obeys} an arrow $v→w$ when it obeys
$v∈U→w∈U$; for example, $\pile(14)$ obeys $2▁→▁2$ but {\sl violates}
$2▁←▁4$. The subsets of $P$ that obey all the vertical arrows are
exactly the piles.
The {\sl order topology} $\Opens_A(P)$ is the set:
%
$$\begin{array}{rcl}
\Opens_A(P) &=& \setofst{U⊆P}{∀(v→w)∈A.\; U \text{ obeys } v→w} \\
&=& \setofst{U⊆P}{U \text{ obeys all arrows in } A} \\
\end{array}
$$
In contexts in which a 2CG $(P,A)$ is defined the letter $H$ will
always denote the order topology $\Opens_A(P)$ regarded as a Heyting
Algebra.
\msk
Section 3 of \cite{PH1} defines a way to interpret each $ab≡\pile(ab)$
as a point of $\Z^2$, by:
%
$$ab \;\; ≡ \;\; (0,0) + a\VEC{-1,1} + b\VEC{1,1}
$$
%
i.e.: start at $(0,0)$, then walk $a$ steps northwest and $b$ steps
northeast. The `$≡$' here is pronounced ``can be interpreted as''.
It is easy to see that $22∈\Opens_A(P)$ but $21 \not∈ \Opens_A(P)$;
the arrow $2▁→▁2$ forbids 21, and all the piles that can be obtained
by walking southwest and northwest from 21 --- let's denote the set of
those piles by $\mathsf{swnw}(21)$ --- are also forbidden. Similarly,
24 is open but 14 is not, and $2▁←▁4$ forbids all piles in the set
$\mathsf{sene}(14)$. If we draw all piles and then erase the ones
forbidden by $2▁→▁2$ and $2▁←▁4$ we get exactly all the piles in the
$\Opens_A(P)$ of the example above, and this holds in general.
\msk
We say that two piles $ab$ and $cd$ in $\Opens_A(P)$ are {\sl
neighbors} --- notation: $ab \eqN cd$ --- when they differ by
exactly one element; for example, $24 \eqN 25$ but $34 \not\eqN 25$
and $25 \not\eqN 25$. Let $∼_1^*$ be the transitive-reflexive closure
of $∼_1$, and let's say that $\Opens_A(P)$ is {\sl $∼_1^*$-connected}
if all piles of $\Opens_A(P)$ are $∼_1^*$-equivalent. Section 15 of
\cite{PH1} shows an $\Opens_A(P)$ is $∼_1^*$-connected iff $(P,A)$ is
acyclic.
We will say that a 2-column graph $(P,A)$ is {\sl proper} iff it is
finite and acyclic. A {\sl Planar Heyting Algebra} (or: a ``ZHA'') is
a finite subset of $\Z^2$ that ``is'' the order topology for a proper
2CG. From here onwards all our 2CGs will be implicitly proper.
Here are some examples of ZHAs (drawn with bullets insted of with
2-digit numbers):
%
%L drawzhawithbullets = function (zdef, spec)
%L -- mpnew({zdef=zdef, scale="6pt", meta="s"}, spec):addbullets():output()
%L mpnew({zdef=zdef, scale="4pt", meta="s"}, spec):addbullets():output()
%L end
%L drawzhawithbullets("dots1", "1")
%L drawzhawithbullets("dots4", "1LLL")
%L drawzhawithbullets("dots3", "1RR")
%L drawzhawithbullets("dots43", "123L21")
%L drawzhawithbullets("dotsbottle", "12321L")
%L drawzhawithbullets("dotsa", "12RRLLRR1")
%L drawzhawithbullets("dotsb", "1R2R3212RL1")
%L drawzhawithbullets("dotsc", "12345RR4321")
\pu
$$\zha{dots1}
\qquad
\zha{dots4}
\qquad
\zha{dots3}
\qquad
\zha{dots43}
\qquad
\zha{dotsbottle}
\qquad
\zha{dotsa}
\qquad
\zha{dotsb}
\qquad
\zha{dotsc}
$$
\def\IPLstar{\ensuremath{\text{IPL}^*}}
The two {\sl basic} themes in \cite{PH1} are that we can interpret
Intuitionistic Propositional Logic on ZHAs and that we can use ZHAs to
develop {\sl visual intuition} about IPL. Here we will take that one
step ahead. Take IPL and add a modal operator $·^*$ to it, with axioms
that assert that $P≤P^*≤P²$ and $(P∧Q)^*=P^*∧Q^*$. Call this new logic
\IPLstar. Here we will see how to use ZHAs with slashings to develop
visual intuition about \IPLstar, and in the last sections we will see
how to {\sl use} this visual intuition to learn some ideas about
toposes and sheaves, and we will see how to {\sl formalize} what this
``visual intuition'' works.
% (ph9p)
% (ph9t 2 "The objective of the series")
% _ ____ _ _ _
% / | / ___|| | __ _ ___| |__ (_)_ __ __ _ ___
% | | \___ \| |/ _` / __| '_ \| | '_ \ / _` / __|
% | |_ ___) | | (_| \__ \ | | | | | | | (_| \__ \
% |_(_) |____/|_|\__,_|___/_| |_|_|_| |_|\__, |___/
% |___/
%
% «1._slashings» (to ".1._slashings")
% (p2ap 1 "1._slashings")
% (p2aa "1._slashings")
% (jonp 3 "basic-definitions")
% (josa "basic-definitions")
% ____ _ _ __
% | __ ) __ _ ___(_) ___ __| | ___ / _|___
% | _ \ / _` / __| |/ __| / _` |/ _ \ |_/ __|
% | |_) | (_| \__ \ | (__ | (_| | __/ _\__ \
% |____/ \__,_|___/_|\___| \__,_|\___|_| |___/
%
% «basic-definitions» (to ".basic-definitions")
% (p2ap 3 "basic-definitions")
% (p2aa "basic-definitions")
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7} -- with v arrows
%L tspec_PA = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L tspec_PA :mp ({zdef="O_A(P)"}) :addlrs():print() :output()
%L tspec_PAQ:mp ({zdef="O_A(P),J"}):addlrs():print() :output()
%L tspec_PA :tcgq({tdef="(P,A)", meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L tspec_PAC = TCGSpec.new("46; 11 22 34 45, 25", "?...", "???...")
%L tspec_PAC:mp ({zdef="closed-op"}) :addlrs():print() :output()
%L tspec_PAC:tcgq({tdef="closed-op", meta="1pt p"}, "lr q h v ap") :output()
\pu
% ___ _ _
% / _ \ _ __ ___ ___ __ _ _ __ __| | ___| |___
% | | | | '_ ` _ \/ __| / _` | '_ \ / _` | / __| / __|
% | |_| | | | | | \__ \ | (_| | | | | (_| | \__ \ \__ \
% \__\_\_| |_| |_|___/ \__,_|_| |_|\__,_| |___/_|___/
%
% «qms-and-slashings» (to ".qms-and-slashings")
% (jonp 3 "qms-and-slashings")
% (jos "qms-and-slashings")
\section{Question marks and slashings}
\label {qms-and-slashings}
A {\sl set of question marks} on a 2CG $(P,A)$ is a subset $Q⊆P$. We
write a 2CG with question marks as $((P,A),Q)$, and we represent this
$Q$ graphically by writing a `?' close to each element of $P$ that
belongs to $Q$, as in the figure below. The intended meaning of these
question marks is that we want to forget the information on them and
then see which elements of $\Opens_A(P)$ become indistinguishable
after this forgetting: two elements $ab,cd∈H$ are {\sl
$Q$-equivalent}, written as $ab \eqQ cd$, iff $\pile(ab)∖Q =
\pile(cd)∖Q$. In the $((P,A),Q)$ of the figure below we have $23 \eqQ
13 \not\eqQ 14$.
A {\sl slashing} $S$ on a ZHA $H$ is a set of diagonal cuts on $H$
``that do not stop midway''. These cuts are interpreted as fences that
divide $H$ in separate regions, and two elements $ab,cd∈H$ are {\sl
$S$-equivalent}, written as $ab \eqS cd$, if they belong to the same
region. In the slashing at the right in the figure below we have $11
\eqS 23 \not\eqS 14$.
%
$$\tcg{(P,A),Q} \;\; \squigbij \;\;\; \zha{O_A(P),J}$$
In \cite{PH1} we used the notation $(P,A) \; \squigbijbody \; H$
to say that $H$ is the ZHA associated to the 2CG $(P,A)$; this ``is
associated to'' was interpreted formally as $\Opens_A(P) = H$. We are
now extending this to $((P,A),Q) \; \squigbijbody \; (H,S)$ --- a 2CG
with question marks $((P,A),Q)$ is associated to the ZHA with slashing
$(H,S)$ when we have $\Opens_A(P) = H$ and the equivalence relations
$\eqQ,\eqS⊆H×H$ coincide. Note that the two `$\squigbijbody$'s are
both pronounced as ``is associated to'', but they have different
formal meanings.
% ____ _ _ _ _
% | _ \(_) ___ ___ ___ __ _ _ __ __| | ___| |___| |__ ___
% | |_) | |/ __/ __/ __| / _` | '_ \ / _` | / __| / __| '_ \/ __|
% | __/| | (_| (__\__ \ | (_| | | | | (_| | \__ \ \__ \ | | \__ \
% |_| |_|\___\___|___/ \__,_|_| |_|\__,_| |___/_|___/_| |_|___/
%
% «piccs-and-slashings» (to ".piccs-and-slashings")
% (jonp 4 "piccs-and-slashings")
% (jos "piccs-and-slashings")
% (ph2p 4 "piccs-and-slashings")
% (ph2 "piccs-and-slashings")
\subsection{Piccs and slashings}
\label {piccs-and-slashings}
A picc (``partition into contiguous classes'') of a ``discrete
interval'' $I=\{0,\ldots,n\}$ is a partition $P$ of $I$ that obeys
this condition (``picc-ness''):
%
$$∀a,b,c∈\{0,\ldots,n\}.\; (a<b<c ∧ a \eqP c) → (a \eqP b ∧ b \eqP c).$$
%
So $P = \{\{0\},\{1,2,3\},\{4,5\}\}$ is a picc of $\{0,\ldots,5\}$,
and
%
$$P' = \{\{0\},\{1,2,4,5\},\{3\}\}$$
%
is a partition of $\{0,\ldots,5\}$ that is not a picc.
A short notation for piccs is this:
%
$$0|123|45 \equiv \{\{0\},\{1,2,3\},\{4,5\}\}$$
%
we list all digits in the (discrete) interval in order, and we put
bars to indicate where we change from one equivalence class to
another.
\msk
We will represent a slashing $S$ formally as pairs of piccs, one for
the left digit and one for the right digit. Our notation for slashings
as pairs will be based on this figure:
%
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="VCuts"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
$$\pu
\VCuts
\qquad
% \ZQuot
% \qquad
\ZQuotients
$$
The slashing $S$ that we are using in our examples will be represented
as:
%
$$\begin{array}{rcl}
S &=& (L,R) \\
&=& (\{\{0\},\{1,2,3,4\}\}, \, \{\{0,1,2,3\},\{4,5\},\{6\}\}) \\
&=& (0|1234, 0123|45|6) \\
&=& (4321/0,\, 0123∖45∖6) \\
\end{array}
$$
%
We use `$/$'s and `$∖$'s instead of `$|$'s to remind us of the
direction of the cuts: the `$/$'s correspond to cuts that go northeast
and the `$∖$'s to cuts that go northwest.
We can now define the equivalence relation $\eqS$ formally: if
$S=(L,R)$ then $ab \eqS cd$ iff $a \eqL c$ and $c \eqR d$.
\msk
The expression ``$S=(L,R)$ is a slashing on $H$'' will mean: $H$ is a
ZHA, $L$ is a picc on $\{0,\ldots,l\}$, and $R$ a picc on
$\{0,\ldots,r\}$, where $lr$ is the top element of $H$. The domain of
the equivalence relation $\eqS$ will be considered to be $H$, not
$\{0,\ldots,l\} × \{0,\ldots,r\}$.
% Note that $\eqS$ is an equivalence relation on $H$, not on
% $\{0,\ldots,a\} × \{0,\ldots,b\}$.
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
%
% «slash-ops» (to ".slash-ops")
% (jonp 5 "slash-ops")
% (jos "slash-ops")
\subsection{Slash-operators}
\label {slash-ops}
When $S=(L,R)$ is a slashing on $H$ we will use the notations $[·]^L$,
$[·]^R$, $[·]^S$ for the equivalence classes of $L$, $R$, $S$ and the
notations $·^L$, $·^R$, $·^S$ for the highest element in those
equivalence classes. In our example we have $[2]^L = \{1,2,3,4\}$,
$[2]^R = \{0,1,2,3\}$, $[22]^S = \{11,12,13,22,23\}$, $2^L = 4$, $2^R
= 4$, $2^S = 23$. Note that $[a]^L×[b]^R$, that we define as
%
$$\begin{array}{rcl}
[a]^L×[b]^R &=& \setofst{cd}{c∈[a]^L, d∈[b]^R}
\end{array}
$$
%
is a rectangle (tilted $45^\circ$) that may contain piles that are not
open; for example, $04∈[2]^L×[2]^R$, and $[22]^S \subsetneq
[2]^L×[2]^R$.
A {\sl slash-operator} on a ZHA $H$ is a function $·^F:H→H$ that is
equal to some $·^S$. Let's do that more explicitly. A function
$·F:H→H$ if a slash-operator iff there exists a slashing $S$ on the
ZHA $H$ such that $·^F=·^S$.
\msk
\def\eqLone{∼_{L1}}
\def\eqRone{∼_{L1}}
Supppose that we have a ZHA $H$ and an arbitrary function $·^F:H→H$ on
it. Suppose that the top element of $H$ is $lr$. We can define $\eqL$,
$\eqR$, $L$, $R$ from that $·^F$ in the following way.
First we define a relation $L_F⊂\{1,\ldots,l\}^2$ in which $a \, L_F
\, c$ is true if and only if there are $ab,cd∈H$ with $ab^F=cd$. We
then define $\eqL$ as the transitive-reflexive closure of $L_F$, and
we define the partition $L$ of $\{1,\ldots,l\}$ as the set of
equivalence classes of $\eqL$. We do the same to define
$R_F⊂\{1,\ldots,r\}^2$, $\eqR$, and $R$. If this $L$ is not a picc on
$\{1,\ldots,l\}$, or if this $R$ is not a picc on $\{1,\ldots,r\}$, we
stop: our original $·^F$ is not a slash-operator. If both $L$ and $R$
are piccs, we define $·^L$, $·^R$, and $·^S$ as in the beginning of
the section, and we test if this $·^S$ if equal to our original $·^F$.
If they are equal then our $·^F$ is a slash-operator; if $·^S ≠ ·^F$
then our $·^F$ is not a slash-operator.
% ____ _ _
% / ___|___ _ ____ _____ _ __| |_(_)_ __ __ _
% | | / _ \| '_ \ \ / / _ \ '__| __| | '_ \ / _` |
% | |__| (_) | | | \ V / __/ | | |_| | | | | (_| |
% \____\___/|_| |_|\_/ \___|_| \__|_|_| |_|\__, |
% |___/
%
% «converting» (to ".converting")
% (jonp 6 "converting")
% (jos "converting")
\subsection{From slashings to question marks and vice-versa}
\label{converting}
\def\symdiff{\mathbin{\triangle}}
Let's write $A \symdiff B$ for the symmetric difference between two
sets, and $H^2_u$ for the subset of $H^2$ formed by the pairs of
neighboring points of $H$ whose difference is exactly $u$:
%
$$H^2_u = \setofst{(ab,cd)∈H^2}{ab \symdiff cd = \{u\}}$$
There are several ways to convert a slashing to question marks and
vice-versa. They are all based on this idea: if one pair
$(ab,cd)∈H^2_u$ is $S$-equivalent, then all the other pairs will also
be, and this means that all these pairs have to be $Q$-equivalent ---
which means $u∈Q$. So:
%
$$\begin{array}{rcl}
Q &=& \setofst{u∈P}{∃(ab,cd)∈H^2_u. \; ab \eqS cd} \\
&=& \setofst{u∈P}{∀(ab,cd)∈H^2_u. \; ab \eqS cd} \\
\end{array}
$$
Here is a simple way to do that conversion visually. Choose any path
from the bottom element of the ZHA to its top element that is made of
one unit steps northwest or northeast --- for example, this one:
%
$$(a_0b_0, a_1b_1, \ldots a_{10}b_{10}) = (00, 01, 02, 03, 04, 14, 24, 34, 35, 36, 46)$$
If we are converting from a slashing to question marks, then for each
step from one element of the ZHA to the next one, say, from $ab$ to
$cd$, check if we have crossed one of the cuts of the slashing; if we
haven't then we've moved between two $S$-equivalent points, and as
they should also be $Q$-equivalent we add their difference $ab
\symdiff cd$ to $Q$. If we are converting from question marks to
slashings then every time that we move from a point $ab$ to a point
$cd$ and their difference $ab \symdiff cd$ is not a question mark
point then we draw a cut separating $ab$ and $cd$.
In a diagram:
\msk
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L local mp = tspec_PAQ:mp ({zdef="path"})
%L for _,ab in ipairs(split("00 01 02 03 04 14 24 34 35 36 46")) do
%L mp:put(v(ab), ab)
%L end
%L mp:print():output()
\pu
%
$$\begin{array}{c}
\tcg{(P,A),Q} \;\; \squigbij \;\;\; \zha{path}
\\
\end{array}
$$
\msk
To convert from slashings to question marks:
We have $00 \eqS 01 \eqS 02 \eqS 03$, so $▁1, ▁2, ▁3∈Q$.
We have $14 \eqS 24 \eqS 34$ and $34 \eqS 35$, so $2▁, 3▁ ∈Q$ and $▁5∈Q$.
We have $36 \eqS 46$, so $▁4∈Q$.
\msk
To convert from question marks to slashings:
We have $03 \not\eqQ 04$, so we draw a cut between 03 and 04 ($3∖4$).
We have $04 \not\eqQ 14$, so we draw a cut between 04 and 14 ($1/0$).
We have $35 \not\eqQ 36$, so we draw a cut between 35 and 36 ($5∖6$).
Our slashing is $4321/0$ $0123∖45∖6$.
\newpage
% _
% | | ___ _ __ ___
% _ | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
% \___/ \___/| .__/|___/
% |_|
%
% «2._J-operators» (to ".2._J-operators")
% (p2ap 10 "2._J-operators")
% (p2aa "2._J-operators")
% (jonp 8 "J-operators")
% (jol "J-operators")
% «J-operators» (to ".J-operators")
% (jonp 8 "J-operators")
% (jol "J-operators")
% J-regions and J-operators
% (p2lp 1 "J-operators")
% (p2l "J-operators")
\section{J-operators}
\label {J-operators}
% Good (ph2p 9 "J-ops-and-regions")
% (fooi "Ω" "H")
A {\sl J-operator} on a Heyting Algebra $H ≡ (H,≤,⊤,⊥,∧,∨,→,↔,¬)$ is a
function $J:H→H$ that obeys the axioms $\J1$, $\J2$, $\J3$ below; we
usually write $J$ as $·^*:H→H$, and write the axioms as rules.
%
%L addabbrevs(".\\eqJ.", " \\eqJ ")
%L addabbrevs("&", "\\&", "vv", "∨", "->", "→")
%L -- addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%:
%: -----\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 non-decreasing.
\par $\J2$ says that the operation $·^*$ is idempotent.
\par $\J3$ is a bit mysterious but will have interesting consequences.
\msk
% Note that when $H$ is a ZHA then any slash-operator on $H$ is a
% J-operator on it; see secs.\ref{slash-ops} and
% \ref{slash-ops-property}.
%
% \msk
A J-operator induces an equivalence relation and equivalence classes
on $H$, like slashings do:
%
$$\begin{array}{rcl}
P \eqJ Q &\text{iff}& P^*=Q^* \\[5pt] \relax
[P]^J &:=& \setofst{Q∈H}{P^*=Q^*} \\
\end{array}
$$
%
The equivalence classes of a J-operator $J$ are called {\sl
$J$-regions}.
\msk
The axioms $\J1$, $\J2$, $\J3$ have many consequences. The first ones
are listed in Figure \ref{fig:J-ops-basic-derived-rules} as derived
rules, whose names mean:
$\Mop$ (monotonicity for products): a lemma used to prove $\Mo$,
$\Mo$ (monotonicity): $P≤Q$ implies $P^*≤Q^*$,
$\Sand$ (sandwiching): all truth values between $P$ and $P^*$ are equivalent,
$\ECa$: equivalence classes are closed by `$\&$',
$\ECv$: equivalence classes are closed by `$∨$',
$\ECS$: equivalence classes are closed by sandwiching,
% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%:
%: ------------\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≤P∨Q P∨Q≤P¹
%: ----------------
%: P≤P∨Q≤P¹
%: -----------\Sand
%: P¹=Q¹ P¹=Q¹\bk P¹=(P∨Q)¹
%: ------------\ECv := ------------------
%: P¹=Q¹=(P∨Q)¹ P¹=Q¹=(P∨Q)¹
%:
%: ^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
%:
\begin{figure}
\pu
\resizebox{\textwidth}{!}{%
\fbox{$
\def\bk{HELLO}
\def\bk{\hspace{-1cm}}
\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}
$}
}
\caption{J-operators: basic derived rules}
\label{fig:J-ops-basic-derived-rules}
\end{figure}
\bsk
Take a J-equivalence class, $[P]^J$, and list its elements: $[P]^J =
\{P_1, \ldots, P_n\}$. Let $P_∧ := ((P_1∧P_2)∧\ldots)∧P_n$ and $P_∨ :=
((P_1∨P_2)∨\ldots)∨P_n$. Clearly $P_∧ ≤ P_i ≤ P_∨$ for each $i$, so
$[P]^J ⊆ [P_∧,P_∨]$. We will use the interval notation $[P,R]$ to mean
the set of all elements of $H$ obeying $P≤Q≤R$:
%
$$[P,R] \;\; = \;\; \setofst{Q∈H}{P≤Q≤R}.$$
Using $\ECa$ and $\ECv$ several times we see that:
%
$$\begin{array}{rrr}
P_1∧P_2 \eqJ P && P_1∨P_2 \eqJ P \\
(P_1∧P_2)∧P_3 \eqJ P && (P_1∨P_2)∨P_3 \eqJ P \\
\vdots\phantom{mmmm} && \vdots\phantom{mmmm} \\
((P_1∧P_2)∧\ldots)∧P_n \eqJ P && ((P_1∨P_2)∨\ldots)∨P_n \eqJ P \\
P_∧ \eqJ P && P_∨ \eqJ P \\[5pt]
P_∧ ∈ [P]^J && P_∨ ∈ [P]^J \\
\end{array}
$$
%
and using $\ECS$ we can see that all elements between $P_∧$ and $P_∨$
are $J$-equivalent to $P$:
%:
%: P_∧.\eqJ.P P_∨.\eqJ.P
%: ---------- ----------
%: {P_∧}^*=P^* {P_∨}^*=P^*
%: ----------------------
%: P_∧≤Q≤P_∨ {P_∧}^*={P_∨}^*
%: --------------------------------\ECS
%: {P_∧}^*=Q^*={P_∨}^* {P_∨}^*=P^*
%: -------------------------------------------
%: Q^*=P^*
%: ---------
%: Q.\eqJ.P
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
%
so $[P_∧,P_∨] ⊆ [P]^J$. This means that {\sl J-regions are intervals}.
% _____ __ __ _ _
% |___ / | \/ (_) __| |_ ____ _ _ _
% |_ \ | |\/| | |/ _` \ \ /\ / / _` | | | |
% ___) | | | | | | (_| |\ V V / (_| | |_| |
% |____(_) |_| |_|_|\__,_| \_/\_/ \__,_|\__, |
% |___/
%
% «3._midway» (to ".3._midway")
% (p2ap 11 "3._midway")
% (p2aa "3._midway")
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
% (jonp 11 "cuts-stopping-midway")
% (jom "cuts-stopping-midway")
% (p2lp 3 "cuts-stopping-midway")
% (p2l "cuts-stopping-midway")
\section{Cuts stopping midway}
\label{cuts-stopping-midway}
Look at the figure at the left below, that shows a partition of a ZHA
$A=[00,66]$ into five regions, each region being an interval; this
partition does not come from a slashing, as it has (four) cuts that
stop midway. They are detailed at the right; the ones in which the
cuts look like a `Y' will be called Y-cuts, and the ones that look
like `$λ$'s will be called $λ$-cuts. Define an operation `$·^*$' on
$A$, that works by taking each truth-value $P$ in it to the top
element of its region; for example, $30^*=61$.
%
%L mp = mpnew({zdef="4-cuts-stopping-midway", meta="10pt"}, "1234567654321")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
%L
%R local Y22, Y52, La25, La55 =
%R 2/ 22 \, 2/ 52 \, 2/ 25 \, 2/ 55 \
%R |21 12| |51 42| |24 15| |54 45|
%R \ 11 / \ 41 / \ 14 / \ 44 /
%R
%R La55:tozmp({zdef="La55", scale="11pt"}):addcells():addcuts("00w-11e 00e-00n"):output()
%R La25:tozmp({zdef="La25", scale="11pt"}):addcells():addcuts("00w-00n 00e-10n"):output()
%R Y52 :tozmp({zdef="Y52", scale="11pt"}):addcells():addcuts("00e-11w 11e-11s"):output()
%R Y22 :tozmp({zdef="Y22", scale="11pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
%
$$\pu
\zha{4-cuts-stopping-midway}
\quad
\begin{array}{ccc}
\text{$λ$-cuts:} & \zha{La55} & \zha{La25} \\[15pt]
\text{Y-cuts:} & \zha{Y52} & \zha{Y22} \\
\end{array}
$$
%
It is easy to see that `$·^*$' obeys $\J1$ and $\J2$; however, it does
{\sl not} obey $\J3$ --- we will prove that in
sec.\ref{no-Y-cuts-no-L-cuts}. As we will see, {\sl the partitions of
a ZHA into intervals that obey $\J1$, $\J2$, $\J3$ ae exactly the
slashings;} or, in other words, {\sl every J-operator comes from a
slashing}.
% _ _ __ __ _
% | \ | | ___ \ \ / / ___ _ _| |_ ___
% | \| |/ _ \ \ V / / __| | | | __/ __|
% | |\ | (_) | | | | (__| |_| | |_\__ \
% |_| \_|\___/ |_| \___|\__,_|\__|___/
%
% «no-Y-cuts-no-L-cuts» (to ".no-Y-cuts-no-L-cuts")
% (jonp 11 "no-Y-cuts-no-L-cuts")
% (jom "no-Y-cuts-no-L-cuts")
% (p2lp 4 "no-Y-cuts-no-L-cuts")
% (p2l "no-Y-cuts-no-L-cuts")
\subsection{The are no Y-cuts and no $\lambda$-cuts}
\label {no-Y-cuts-no-L-cuts}
% Good (ph2p 12 "no-Y-cuts-no-L-cuts")
Let's start with these particular cases of a $λ$-cut and a Y-cut:
%
%R local YPQ, LaPQ =
%R 4/ !PoQ \, 4/ !PoQ \
%R |!Ps !Qs| |!Ps !Qs|
%R \ !PaQ / \ !PaQ /
%R
%R YPQ :tozmp({zdef="YPQ", scale="20pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
%R LaPQ:tozmp({zdef="LaPQ", scale="20pt"}):addcells():addcuts("00w-11e 00e-00n"):output()
%
$$\pu
\def\PoQ{P{∨}Q}
\def\PaQ{P{∧}Q}
\def\Ps{P \;\;\;\; }
\def\Qs{ \;\;\;\; Q}
\text{$λ$-cut:} \;\;\;\;\; \zha{LaPQ}
\qquad
\quad
\text{Y-cut:} \;\;\;\;\; \zha{YPQ}
$$
One way to prove that $λ$-cuts can't happen when $\J1$, $\J2$, and
$\J3$ all hold is to show a proof of $(P \eqJ P{∨}Q) → (P{∧}Q \eqJ Q)$
that uses only $\J1$, $\J2$, $\J3$ and the axioms of Heyting Algebras;
and similarly, we can prove that $Y$-cuts can't happen by showing a
proof of $(P \eqJ P{∨}Q) ← (P{∧}Q \eqJ Q)$. Here are the proofs, with
the proof of ``$λ$-cuts can't happen'' first:
%:
%: P¹=(P∨Q)¹
%: ---------------
%: P¹∧Q¹=(P∨Q)¹∧Q¹
%: =================\J3 =========
%: (P∧Q)¹=((P∨Q)∧Q)¹ (P∨Q)∧Q=Q
%: -------------------------------
%: (P∧Q)¹=Q¹
%:
%: ^no-L-cuts-2021
%:
%: (P∧Q)¹=Q¹
%: -------------
%: P∨(P∧Q)¹=P∨Q¹
%: -------------------
%: (P∨(P∧Q)¹)¹=(P∨Q¹)¹
%: ========= ===================\oor_6=\oor_4
%: P=P∨(P∧Q) (P∨(P∧Q))¹=(P∨Q)¹
%: -----------------
%: P¹=(P∨Q)¹
%:
%: ^no-Y-cuts-2021
%:
\pu
$$\ded{no-L-cuts-2021}$$
$$\ded{no-Y-cuts-2021}$$
The expansion of the double bar labeled `$\oor_6=\oor_4$' uses (twice)
a derived rule with that name, that can be obtained from the
`$\oor$-cubes' of sec.\ref{cubes}.
% \standout{Old:}
%
% % (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
% %
% %: Q¹=R¹
% %: ---------
% %: P∨Q¹=P∨R¹
% %: ---------------
% %: Q¹=R¹ (P∨Q¹)¹=(P∨R¹)¹
% %: ---------------\NoYcuts := ===============\ostarcube
% %: (P∨Q)¹=(P∨R)¹ (P∨Q)¹=(P∨R)¹
% %:
% %: ^NoYcuts1- ^NoYcuts2-
% %:
% %: P¹=Q¹
% %: ---------
% %: P¹∨R=Q¹∨R
% %: ---------------
% %: P¹=Q¹ (P¹∨R)¹=(Q¹∨R)¹
% %: ---------------\NoYcuts := ================\oor_5=\oor_4
% %: (P∨R)¹=(Q∨R)¹ (P∨R)¹=(Q∨R)¹
% %:
% %: ^NoYcuts1 ^NoYcuts2
% %:
% %:
% %: Q¹=R¹
% %: ----------
% %: Q¹=R¹ P¹∧Q¹=P¹∧R¹
% %: ---------------\NoLcuts := ------------\J3
% %: (P∧Q)¹=(P∧R)¹ (P∧Q)¹=(P∧R)¹
% %:
% %: ^NoLcuts1- ^NoLcuts2-
% %:
% %: P¹=Q¹
% %: ----------
% %: P¹=Q¹ P¹∧R¹=Q¹∧R¹
% %: ---------------\NoLcuts := ------------\J3
% %: (P∧R)¹=(Q∧R)¹ (P∧R)¹=(Q∧R)¹
% %:
% %: ^NoLcuts1 ^NoLcuts2
% %:
% \pu
% $$\begin{array}{rcl}
% \ded{NoYcuts1} &:=& \ded{NoYcuts2} \\ \\
% \end{array}
% $$
% $$\begin{array}{rcl}
% \ded{NoLcuts1} &:=& \ded{NoLcuts2} \\ \\
% \end{array}
% $$
%
% The expansion of double bar labeled `$\oor_6=\oor_4$' in the top
% derivation uses twice the derived rule $\oor_6=\oor_4$, that is easy
% to prove using the cubes of sec.\ref{cubes}.
%
% We want to see that if a partition of a ZHA $H$ into intervals has
% ``Y-cuts'' or ``$λ$-cuts'', like these parts of the last diagram in
% sec.\ref{cuts-stopping-midway},
% %
% %R local Y, La =
% %R 2/ 22 \, 2/ 25 \
% %R |21 12| |24 15|
% %R \ 11 / \ 14 /
% %R
% %R Y :tozmp({def="Ycut", scale="10pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
% %R La:tozmp({def="Lcut", scale="10pt"}):addcells():addcuts("00w-00n 00e-10n"):output()
% $$\pu
% \begin{array}{rcl}
% \Ycut &\Leftarrow& \text{this is a Y-cut} \\\\
% \Lcut &\Leftarrow& \text{this is a $λ$-cut}\\
% \end{array}
% $$
% %
% then the operation $J$ that takes each element to the top of its
% equivalence class cannot obey $\J1$, $\J2$ and $\J3$ at the same time.
% We will prove that by deriving rules that say that if $11 \eqJ 12$
% then $21 \eqJ 22$, and that if $15 \eqJ 25$ then $14 \eqJ 24$;
% actually, our rules will say that if $11^* = 12^*$ then $(11∨21)^* =
% (12∨21)^*$, and that if $15^*=25^*$ then $(15∧24)^*=(25∧24)^*$. The
% rules are:
\newpage
% _ _ ____ _
% | || | / ___| _| |__ ___ ___
% | || |_ | | | | | | '_ \ / _ \/ __|
% |__ _| | |__| |_| | |_) | __/\__ \
% |_|(_) \____\__,_|_.__/ \___||___/
%
% «4._cubes» (to ".4._cubes")
% (p2ap 11 "4._cubes")
% (p2aa "4._cubes")
% «cubes» (to ".cubes")
% (jonp 13 "cubes")
% (joc "cubes")
\section{How J-operators interact with connectives}
\label {cubes}
% (find-LATEX "2015planar-has.tex" "J-connectives")
% (find-planarhaspage 16 "How J-operators interact with the connectives")
% (find-planarhastext 16 "How J-operators interact with the connectives")
The axiom $\J3$ says that $(P∧Q)¹=P¹∧Q¹$ --- it says something about
how `$·^*$' interacts with `$∧$'. Let's introduce a shorter notation.
There are eight ways to replace each of the `?'s in $(P^? ∧ Q^?)^?$ by
either nothing or a star. We establish that the three `?'s in $(P^? ∧
Q^?)^?$ are ``worth'' 1, 2 and 4 respectively, and we use $P \oand_n
Q$ to denote $(P^? ∧ Q^?)^?$ with the bits ``that belong to $n$''
replaced by stars. So:
%
$$\begin{array}{rcrcrcr}
\oand_0 &=& P∧Q, && \oand_4 &=& (P∧Q)^*, \\
\oand_1 &=& P^*∧Q, && \oand_5 &=& (P^*∧Q)^*, \\
\oand_2 &=& P∧Q^*, && \oand_6 &=& (P∧Q^*)^*, \\
\oand_3 &=& P^*∧Q^*, && \oand_7 &=& (P^*∧Q^*)^*. \\
\end{array}
$$
We omit the arguments of $\oand_n$ when they are $P$ and $Q$ --- so we
can rewrite $(P∧Q)¹=P¹∧Q¹$ as $\oand_4=\oand_3$. These conventions
also hold for $\oor$ and $\oimp$.
%D diagram cube-and*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-and*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-or*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
\pu
%$$
% \begin{array}{rcl}
% \diag{cube-and*-obvious} && \diag{cube-and*-full} \\ \\
% \diag{cube-or*-obvious} && \diag{cube-or*-full} \\ \\
% \diag{cube-imp*-obvious} && \diag{cube-imp*-full} \\
% \end{array}
%$$
It is easy to prove each one of the arrows in the cubes below ($A
\diagxyto/->/ B$ means $A≤B$):
%
$$\myresizebox{$
\pu
\diag{cube-and*-obvious}
\quad
\diag{cube-or*-obvious}
\quad
\diag{cube-imp*-obvious}
$}
$$
\bsk
Let's write their sets of elements as $\oand_\zs := \{\oand_0, \ldots,
\oand_7\}$, $\oor_\zs := \{\oor_0, \ldots, \oor_7\}$, and $\oimp_\zs
:= \{\oimp_0, \ldots, \oimp_7\}$. The cubes above --- we will call
them the ``obvious and-cube'', the ``obvious or-cube'', and the
``obvious implication-cube'' --- can be interpreted as directed graphs
$(\oand_\zs, \OCube_\land)$, $(\oor_\zs, \OCube_\lor)$, $(\oimp_\zs,
\OCube_\to)$.
The ``extended cubes'' will be the directed graphs with the arrows
above plus the ones coming from these derived rules:
%:
%:
%: =====================\oand_7=\oand_3=\oand_4
%: (P¹∧Q¹)¹=P¹∧Q¹=(P∧Q)¹
%:
%: ^and*-extra-arrow
%:
%: ===============\oor_7≤\oor_3
%: (P¹∨Q¹)¹≤(P∨Q)¹
%:
%: ^or*-extra-arrow
%:
%: =============\oimp_6≤\oimp_3
%: (P→Q¹)¹≤P¹→Q¹
%:
%: ^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≤P∨Q Q≤P∨Q (P→Q¹)∧P≤Q¹
%: ---------\Mo ----------\Mo ---------------\Mo
%: P¹≤(P∨Q)¹ Q¹≤(P∨Q)¹ ((P→Q¹)∧P)¹≤Q²
%: ----------------------- ---------------\J2
%: P¹∨Q¹≤(P∨Q)¹ ((P→Q¹)∧P)¹≤Q¹
%: ---------------\Mo ---------------\J3
%: (P¹∨Q¹)¹≤(P∨Q)² (P→Q¹)¹∧P¹≤Q¹
%: ----------------\J2 --------------
%: (P¹∨Q¹)¹≤(P∨Q)¹ (P→Q¹)¹≤P¹→Q¹
%:
%: ^or*-extra-arrow-proof ^imp*-extra-arrow-proof
%:
%:
$$
\myresizebox{$\pu
\def\bk{HELLO}
\def\bk{\hspace{-0.5cm}}
\begin{array}{rcl}
\multicolumn{3}{l}{\ded{and*-extra-arrow} \quad :=} \\ \\
\multicolumn{3}{r}{\ded{and*-extra-arrow-proof}} \\ \\
\ded{or*-extra-arrow} &:=& \bk \ded{or*-extra-arrow-proof} \\\\
\ded{imp*-extra-arrow} &:=& \ded{imp*-extra-arrow-proof} \\
\end{array}
$}
$$
%
where $\oand_7=\oand_3=\oand_4$ will be interpreted as these arrows:
%
$$(P^*∧Q^*)^* \two/<-`->/<200> P^*∧Q^* \two/<-`->/<200> (P∧Q)^*$$
The directed graphs of these ``extended cubes'' will be called
$(\oand_\zs, \ECube_\land)$, $(\oor_\zs, \ECube_\lor)$, $(\oimp_\zs,
\ECube_\to)$. We are interested in the (non-strict) partial orders
that they generate, and we want an easy way to remember these partial
orders. The figure below shows these extended cubes at the left, and
at the right the ``simplified cubes'', $\SCube_∧$, $\SCube_∨$, and
$\SCube_→$, that generate the same partial orders that the extended
cubes.
%D diagram extended-and-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oand_7
%D ren A5 A3 A6 ==> \oand_5 \oand_3 \oand_6
%D ren A1 A4 A2 ==> \oand_1 \oand_4 \oand_2
%D ren A0 ==> \oand_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 -> sl^ A3 A7 <- sl_
%D A3 A4 -> sl^ A3 A4 <- sl_
%D ))
%D enddiagram
%
%D diagram extended-and-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oand_7
%D ren A5 A3 A6 ==> \oand_5 \oand_3 \oand_6
%D ren A1 A4 A2 ==> \oand_1 \oand_4 \oand_2
%D ren A0 ==> \oand_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram extended-or-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oor_7
%D ren A5 A3 A6 ==> \oor_5 \oor_3 \oor_6
%D ren A1 A4 A2 ==> \oor_1 \oor_4 \oor_2
%D ren A0 ==> \oor_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D A7 A4 -> .slide= 8pt
%D ))
%D enddiagram
%
%D diagram extended-or-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oor_7
%D ren A5 A3 A6 ==> \oor_5 \oor_3 \oor_6
%D ren A1 A4 A2 ==> \oor_1 \oor_4 \oor_2
%D ren A0 ==> \oor_0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram extended-imp-cube-with-arrows
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oimp_7
%D ren A5 A3 A6 ==> \oimp_5 \oimp_3 \oimp_6
%D ren A1 A4 A2 ==> \oimp_1 \oimp_4 \oimp_2
%D ren A0 ==> \oimp_0
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D A6 A3 ->
%D ))
%D enddiagram
%
%D diagram extended-imp-cube-with-equals
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> \oimp_7
%D ren A5 A3 A6 ==> \oimp_5 \oimp_3 \oimp_6
%D ren A1 A4 A2 ==> \oimp_1 \oimp_4 \oimp_2
%D ren A0 ==> \oimp_0
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
%\begin{figure}
\pu
$$\resizebox{!}{180pt}{%
$
\begin{array}{rcl}
\left( \diag{extended-and-cube-with-arrows} \right)^* &=&
\left( \diag{extended-and-cube-with-equals} \right)^* \\ \\
\left( \diag{extended-or-cube-with-arrows} \right)^* &=&
\left( \diag{extended-or-cube-with-equals} \right)^* \\ \\
\left( \diag{extended-imp-cube-with-arrows} \right)^* &=&
\left( \diag{extended-imp-cube-with-equals} \right)^* \\ \\
\end{array}
$
}
$$
%$}
% \caption{The extended cubes and the simplified cubes.}
% \label{fig:extended-and-simplified-cubes}
%\end{figure}
From these cubes it is easy to see, for example, that we can prove
$\oor_5 = \oor_6$ (as a derived rule).
\newpage
% ____ __ __ _ _ _
% | ___| \ \ / /_ _| |_ _ __ _| |_(_) ___ _ __ ___
% |___ \ \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __|
% ___) | \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \
% |____(_) \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/
%
% «5._valuations» (to ".5._valuations")
% (p2ap 14 "5._valuations")
% (p2aa "5._valuations")
% «valuations» (to ".valuations")
% (jonp 16 "valuations")
% (jov "valuations")
\section{Valuations}
\label {valuations}
Let $H_\odot$ and $J_\odot$ be a ZHA and a J-operator on it, and let
$v_\odot$ be a function from the set $\{P,Q\}$ to $H$. By an abuse of
language $v_\odot$ will also denote the triple $(H_\odot, J_\odot,
v_\odot)$ --- and by a second abuse of language $v_\odot$ will also
denote the obvious extension of $v_\odot: \{P,Q\}→H$ to the set of all
valid expressions formed from $P$, $Q$, $·^*$, $⊤$, $⊥$, and the
connectives.
Let $i,j∈\{0,\ldots,7\}$. Then $(\oand_i,\oand_j)∈\SCube^*_\land$
means that $\oand_i ≤ \oand_j$ is a theorem, and so $v_\odot(\oand_i)
≤ v_\odot(\oand_j)$ holds; i.e.,
%
$$\SCube^*_\land
⊆ \setofst {(\oand_i,\oand_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oand_i) ≤ v_\odot(\oand_j)}
$$
%
and the same for:
%
$$\begin{array}{c}
\SCube^*_\lor
⊆ \setofst {(\oor_i,\oor_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oor_i) ≤ v_\odot(\oor_j)}
\\
\SCube^*_\to
⊆ \setofst {(\oimp_i,\oimp_j)}
{i,j∈\{0,\ldots,7\}, \; v_\odot(\oimp_i) ≤ v_\odot(\oimp_j)}
\\
\end{array}
$$
Some valuations that turn these `$⊆$'s into `$=$'. Let
%
%L mp = mpnew({def="orCube", scale="11pt"}, "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^*")
%L mp:output()
%
%L mp = mpnew({def="andCube", scale="11pt"}, "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^*")
%L mp:output()
%
%L mp = mpnew({def="impCube", scale="11pt"}, "12R1L"):addcuts("c 2/10 01|2")
%L mp:put(v"10", "P") -- :put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q") -- :put(v"02", "Q*", "Q^*")
%L mp:output()
%
\pu
%
$$\begin{array}{c}
(H_∧, J_∧, v_∧) = \andCube
\qquad
(H_∨, J_∨, v_∨) = \orCube \\
(H_→, J_→, v_→) = \impCube \\
\end{array}
$$
%
then
%
$$\begin{array}{c}
\SCube^*_\land
= \setofst {(\oand_i,\oand_j)}
{i,j∈\{0,\ldots,7\}, \; v_∧(\oand_i) ≤ v_∧(\oand_j)}
\\
\SCube^*_\lor
= \setofst {(\oor_i,\oor_j)}
{i,j∈\{0,\ldots,7\}, \; v_∨(\oor_i) ≤ v_∨(\oor_j)}
\\
\SCube^*_\to
= \setofst {(\oimp_i,\oimp_j)}
{i,j∈\{0,\ldots,7\}, \; v_→(\oimp_i) ≤ v_→(\oimp_j)}
\\
\end{array}
$$
%
or, in more elementary terms:
\newpage
{\sl A very important fact.}
For any $i$ and $j$,
%
$$\pu
\begin{array}{rcl}
\oand_i≤\oand_j & \text{ is a theorem iff it is true in } & \andCube \;\; , \\
\\
\oor_i≤\oor_j & \text{ is a theorem iff it is true in } & \orCube \;\; , \\
\\
\oimp_i≤\oimp_j & \text{ is a theorem iff it is true in } & \impCube \;\; . \\
\end{array}
$$
The very important fact, and the valuations $v_∧$, $v_∨$, $v_→$, give
us:
\begin{itemize}
\item a way to {\sl remember} which sentences of the forms
$\oand_i≤\oand_j$, $\oor_i≤\oor_j$, $\oimp_i≤\oimp_j$ are theorems;
\item countermodels for all the sentences of these forms not in
$\SCube_∧$, $\SCube_∨$, $\SCube_→$. For example, $\oor_7≤\oor_4$ is
not in $\SCube_∨$; and $v_∨(\oor_7)≤v_∨(\oor_4)$, which shows that
$\oor_7≤\oor_4$ can't be a theorem.
\end{itemize}
% (find-books "__cats/__cats.el" "bell")
% (find-books "__cats/__cats.el" "bell" "163")
{\sl An observation.} I arrived at the cubes $\ECube_∧^*$,
$\ECube_∨^*$, $\ECube_→^*$ by taking the material in the corollary 5.3
of chapter 5 in \cite{BellLST} and trying to make it fit into less
mental space (as discussed in \cite{IDARCT}); after that I wanted
to be sure that each arrow that is not in the extended cubes has a
countermodel, and I found the countermodels one by one; then I
wondered if I could find a single countermodel for all non-theorems in
$\ECube_∧^*$ (and the same for $\ECube_∨^*$ and $\ECube_→^*$), and I
tried to start with a valuation that distinguished {\sl some}
equivalence classes in $\ECube_∧^*$, and change it bit by bit, getting
valuations that distinguished more equivalence classes at every step.
Eventually I arrived at $v_∧$, $v_∨$ and at $v_→$, and at the ---
surprisingly nice --- ``very important fact'' above.
% (ph2p 20 "ZHA-vals-good")
% (ph2 "ZHA-vals-good")
Note that this valuation
%
%L mp = mpnew({def="orand", scale="11pt"}, "1234321L"):addcuts("c 432/10 01|23")
%L mp:put(v"20", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"13", "Q*", "Q^*")
%L mp:output()
%
$$(H_{∧∨},J_{∧∨},v_{∧∨}) \;\; = \;\; \pu\orand$$
%
distinguishes all equivalence classes in $\ECube^*_∧$ and in
$\ECube^*_∨$, but not in $\ECube^*_→$... it ``thinks'' that $P→Q$ and
$P^*→Q$ are equal.
\newpage
% __ _ _ _
% / /_ / \ | | __ _ ___| |__ _ __ __ _
% | '_ \ / _ \ | |/ _` |/ _ \ '_ \| '__/ _` |
% | (_) | / ___ \| | (_| | __/ |_) | | | (_| |
% \___(_) /_/ \_\_|\__, |\___|_.__/|_| \__,_|
% |___/
%
% «6._algebra» (to ".6._algebra")
% (p2ap 17 "6._algebra")
% (p2aa "6._algebra")
% ____ _ _
% | _ \ ___ | |_ _ | | ___ _ __ ___
% | |_) / _ \| | | | | _ | |_____ / _ \| '_ \/ __|
% | __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_| \___/|_|\__, | \___/ \___/| .__/|___/
% |___/ |_|
%
% «polynomial-J-ops» (to ".polynomial-J-ops")
% (p2ap 17 "polynomial-J-ops")
% (p2aa "polynomial-J-ops")
% (jonp 19 "polynomial-J-ops")
% (joa "polynomial-J-ops")
\section{Polynomial J-operators}
\label {polynomial-J-ops}
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 331) "polynomial")
\def\Jnotnot{{(¬¬)}}
\def\JiiR {{({→→}R)}}
\def\JoQ {{(∨Q)}}
\def\JiR {{({→}R)}}
\def\JfoQR {{(∨Q∧{→}R)}}
\def\JmiQ {({→→}Q∧{→}Q)}
{
It is not hard to check that for any Heyting Algebra $H$ and any
$Q,R∈H$ the operations $\Jnotnot$, $\ldots$, $\JfoQR$ below are
J-operators:
%
%$$\begin{array}{rclcrcl}
% (¬¬) &:=& λP{:}H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% \JiiR &:=& λP{:}H.((P{→}R){→}R) && \JiiR(P) &=& (P{→}R){→}R \\
% \JoQ &:=& λP{:}H.(P{∨}Q) && \JoQ(P) &=& P∨Q \\
% \JiR &:=& λP{:}H.(P{→}R) && \JiR(P) &=& P{→}R\\
% \JfoQR &:=& λP{:}H.((P{∨}Q) ∧ (P{→}R)) && \JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
%$$
%
$$\begin{array}{rclcrcl}
(¬¬)(P) &=& ¬¬P \\
\JiiR(P) &=& (P{→}R){→}R \\
\JoQ(P) &=& P∨Q \\
\JiR(P) &=& P{→}R\\
\JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
\end{array}
$$
Checking that they are J-operators means checking that each of them
obeys $\J1$, $\J2$, $\J3$. Let's define formally what are $\J1$, $\J2$
and $\J3$ ``for a given $F:H→H$'':
%
$$\begin{array}{rcc}
\J1_F &:=& (P ≤ F(P)) \\
\J2_F &:=& (F(P) = F(F(P)) \\
\J3_F &:=& (F(P∧P') = F(P)∧F(P')) \\
\end{array}
$$
%
and:
%
$$\J123_F \quad := \quad \J1_F ∧ \J2_F ∧ \J3_F.$$
% (ph1p 18 "logic-in-HAs")
% (ph1 "logic-in-HAs")
Checking that $\Jnotnot$ obeys $\J1$, $\J2$, $\J3$ means proving
$\J123_\Jnotnot$ using only the rules from intuitionist logic from
section 10 of \cite{PH1}; we will leave the proof of this, of and
$\J123_\JiiR$, $\J123_\JoQ$, and so on, to the reader.
\msk
The J-operator $\JfoQR$ is a particular case of building more complex
J-operators from simpler ones. If $J,K: H→H$, we define:
%
$$(J∧K) := λP{:}H.(J(P){∧}K(P))$$
%
it not hard to prove $\J123_{(J∧K)}$ from $\J123_J$ and $\J123_K$
using only the rules from intuitionistic logic.
\msk
The J-operators above are the first examples of J-operators in Fourman
and Scott's ``Sheaves and Logic'' (\cite{Fourman}); they appear in
pages 329--331, but with these names (our notation for them is at the
right):
(i) {\sl The closed quotient,}
$$J_a p = a ∨ p \qquad J_Q = \JoQ.$$
(ii) {\sl The open quotient,}
$$J^a p = a→p \qquad J^R = \JiR.$$
(iii) {\sl The Boolean quotient}.
$$B_a p = (p→a)→a \qquad B_R = \JiiR.$$
(iv) {\sl The forcing quotient}.
$$(J_a∧J^b)p = (a∨p)∧(b→p) \qquad (J_Q∧J^R) = \JfoQR.$$
(vi) {\sl A mixed quotient.}
$$(B_a∧J^a)p = (p→a)→p \qquad (B_Q∧J^Q) = \JmiQ.$$
\msk
The last one is tricky. From the definition of $B_a$ and $J^a$ what we
have is
%
$$(B_a∧J^a)p = ((p→a)→a)∧(a→p),$$
%
but it is possible to prove
%
$$((p→a)→a)∧(a→p) \;\;↔\;\; ((p→a)→p)$$
%
intuitionistically.
The operators above are ``polynomials on $P,Q,R,→,∧,∨,⊥$'' in the
terminology of Fourman/Scott: ``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'' (p.331).
\msk
When I started studying sheaves I spent several years without any
visual intuition about the J-operators above. I was saved by ZHAs and
brute force --- and the brute force method also helps in testing if a
polynomial (in the sense above) is a J-operator in a particular case.
For example, take the operators $λP{:}H.(P∧22)$ and $({∨}22)$ on
$H=[00,44]$:
%
% (phop 23)
% (pho "J-ops-diagrams")
% (pho "J-ops-diagrams" "jout")
% (find-dn6 "zhas.lua" "shortoperators-tests")
% (find-dn6file "zhas.lua" "mpnewJ =")
%
%L shortoperators()
%L mpnewF = function (opts, spec, J)
%L return mpnew(opts, spec, J):setz():zhaJ()
%L end
%L
%L mpnewF({def="fooa"}, "123454321", function (P) return And(v"22", P) end):output()
%L mpnewF({def="fooo"}, "123454321", Cloq(v"22")):output()
%L mpnewJ({def="fooO"}, "123454321", Cloq(v"22")):zhaPs("22"):output()
%
$$\pu
\begin{array}{rcccl}
λP{:}H.(P∧22) &=& \fooa \\ \\
({∨}22) &=& \fooo &=& \fooO \\
\end{array}
$$
The first one, $λP{:}H.(P∧22)$, is not a J-operator; one easy way to
see that is to look at the region in which the result is 22 --- its
top element is 44, and this violates the conditions on slash-operators
in sec.\ref{slash-ops}. The second operator, $({∨}22)$, is a slash
operator and a J-operator; at the right we introduce a convenient
notation for visualizing the action of a polynomial slash-operator, in
which we draw only the contours of the equivalence classes and the
constants that appear in the polynomial.
Using this new notation, we have:
%
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123R2L1", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123R2L1", Booq(v"11")):zhaPs("11"):output()
%L
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123454321", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123454321", Booq(v"22")):zhaPs("22"):output()
%L mpnewJ({def="foobor", scale="7pt", meta="s"}, "1234567654321", Cloq(v"42")):zhaPs("42"):output()
%L mpnewJ({def="foobim", scale="7pt", meta="s"}, "1234567654321", Opnq(v"24")):zhaPs("24"):output()
%L mpnewJ({def="foofor", scale="7pt", meta="s"}, "1234567654321", Forq(v"42", v"24")):zhaPs("42 24"):output()
%L mpnewJ({def="foomix", scale="7pt", meta="s"}, "12345654321", Mixq(v"22")):zhaPs("22"):output()
%
\pu
$$
\begin{array}{c}
(¬¬) \;\;=\;\;
({→→}00) \;\;=\;\; \fooboo \qquad \qquad
({→→}22) \;\;=\;\; \foobii \\
\\
({∨}42) \;\;=\;\; \foobor \qquad
({→}24) \;\;=\;\; \foobim \\[-20pt]
\\
({∨}42∧{→}24) \;\;=\;\; \foofor \\
\qquad \qquad
\qquad \qquad
\qquad \qquad
({→→}22∧{→}22) \;\;=\;\; \foomix \\
\end{array}
$$
Note that the slashing for $({∨}42∧{→}24)$ has all the cuts for
$({∨}42)$ plus all the cuts for $({→}24)$, and $({∨}42∧{→}24)$
``forces $42≤24$'' in the following sense: if $P^* = ({∨}42∧{→}24)(P)$
then $42^*≤24^*$.
}
% _ _ _
% _ __ (_) ___ ___ ___ __ _| | __ _ ___| |__ _ __ __ _
% | '_ \| |/ __/ __/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_) | | (_| (__\__ \ | (_| | | (_| | __/ |_) | | | (_| |
% | .__/|_|\___\___|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-piccs» (to ".algebra-of-piccs")
% (p2ap 20 "algebra-of-piccs")
% (p2aa "algebra-of-piccs")
% (jonp 21 "algebra-of-piccs")
% (joa "algebra-of-piccs")
\subsection{An algebra of piccs}
\label {algebra-of-piccs}
We saw in the last section a case in which $(J∧K)$ has all the cuts
from $J$ plus all the cuts from $K$; this suggests that we {\sl may}
have an operation dual to that, that behaves as this: $(J∨K)$ has
exactly the cuts that are both in $J$ and in $K$:
%
$$\begin{array}{rcl}
\Cuts(J∧K) &=& \Cuts(J)∪\Cuts(K) \\
\Cuts(J∨K) &=& \Cuts(J)∩\Cuts(K) \\
\end{array}
$$
And it $J_1, \ldots, J_n$ are all the slash-operators on a given ZHA,
then
%
$$\begin{array}{rclcl}
\Cuts(J_1∧\ldots∧J_n) &=& \Cuts(J_1)∪\ldots∪\Cuts(J_k) &=& \text{(all cuts)} \\
\Cuts(J_1∨\ldots∨J_n) &=& \Cuts(J_1)∩\ldots∩\Cuts(J_k) &=& \text{(no cuts)} \\
\end{array}
$$
%
yield the minimal element and the maximal element, respectively, of an
algebra of slash-operators; note that the slash-operator with ``all
cuts'' is the identity map $λP{:}H.P$, and the slash-operator with
``no cuts'' is the one that takes all elements to $⊤$: $λP{:}H.⊤$.
This yields a lattice of slash-operators, in which the partial order
is $J≤K$ iff $\Cuts(J) ⊇ \Cuts(K)$. This is somewhat counterintuitive
if we think in terms of cuts --- the order seems to be reversed ---
but it makes a lot of sense if we think in terms of piccs
(sec.\ref{piccs-and-slashings}) instead.
\msk
Each picc $P$ on $\{0,\ldots,n\}$ has an associated function $·^P$
that takes each element to the top element of its equivalence class.
If we define $P≤P'$ to mean $∀a∈\{0,\ldots,n\}.\,a^P≤a^{P'}$, then we
have this:
%
% (pho "algebra-of-piccs")
% (phop 25 "algebra-of-piccs")
%
%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|2|\ldots|n$, and the top element is $012\ldots
n$, that takes all elements to $n$.
The piccs on $\{0,\ldots,n\}$ form a Heyting Algebra, where
$⊥=0|1|\ldots|n$,
$⊤=01\ldots n$,
and `$∧$' and `$∨$' are the
operations that we have discussed above; it is possible to define a
`$→$' there, but this `$→$' is not going to be useful for us and we
are mentioning it just as a curiosity. We have, for example:
%
%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}$$
% _ _ _
% | | ___ _ __ ___ __ _| | __ _ ___| |__ _ __ __ _
% _ | |_____ / _ \| '_ \/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | __/ |_) | | | (_| |
% \___/ \___/| .__/|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-J-ops» (to ".algebra-of-J-ops")
% (jonp 22 "algebra-of-J-ops")
% (joa "algebra-of-J-ops")
\subsection{An algebra of J-operators}
\label {algebra-of-J-ops}
% Bad (ph2p 50 "algebra-of-J-ops")
% (find-books "__cats/__cats.el" "fourman")
Fourman and Scott define the operations $∧$ and $∨$ on J-operators in
pages 325 and 329 (\cite{Fourman}), and in page 331 they list ten
properties of the algebra of J-operators:
%
$$
\def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
\def\li#1 #2 #3 #4 {\text{#1}& }
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} && (∨21)∨(∨12)=(∨22) \\
\li (ii) J^a∨J^b = J^{a∧b} && ({→}32)∨({→}23)=({→}22) \\
\li (iii) J_a∧J_b = J_{a∧b} && (∨21)∧(∨12)=(∨11) \\
\li (iv) J^a∧J^b = J^{a∨b} && ({→}32)∧({→}23)=({→}33) \\
\li (v) J_a∧J^a = ⊥ && (∨22)∧({→}22)=(⊥) \\
\li (vi) J_a∨J^a = ⊤ && (∨22)∨({→}22)=(⊤) \\
\li (vii) J_a∨K = K∘J_a \\
\li (viii) J^a∨K = J^a∘K \\
\li (ix) J_a∨B_a = B_a \\
\li (x) J^a∨B_b = B_{a→b} \\
\end{array}
$$
% (pho "J-ops-algebra-2")
% (phop 28 "J-ops-algebra-2")
The first six are easy to visualize; we won't treat the four last
ones. In the right column of the table above we've put a particular
case of (i), $\ldots$, (vi) in our notation, and the figures below put
all together.
In Fourman and Scott's notation,
%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}
$$
%
in our notation,
%
%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}
$$
%
and drawing the polynomial J-operators as in
sec.\ref{polynomial-J-ops}:
%
%L deforp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Cloq(v(P))):zhaPs(draw):print():output()
%L end
%L defimp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Opnq(v(P))):zhaPs(draw):print():output()
%L end
%L deforp("21", "21", "ora")
%L deforp("22", "22", "orb")
%L deforp("11", "11", "orc")
%L deforp("12", "12", "ord")
%L deforp("00", "", "orB")
%L defimp("32", "32", "ima")
%L defimp("22", "22", "imb")
%L defimp("33", "33", "imc")
%L defimp("34", "34", "imd")
%L defimp("00", "", "imB")
%
%R local algebra =
%R 4/ !imB \
%R | |
%R | !orb !imb |
%R |!ora !ord !ima !imd|
%R | !orc !imc |
%R | |
%R \ !orB /
%R
%R algebra:tomp({def="foo", scale="30pt"}):addcells():output()
$$\pu
% \bhbox{$
\begin{array}{c}
\\
\foo \\
\\
\end{array}
% $}
$$
% $$
% \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}
% $$
%
% $$\begin{array}{rclcrcl}
% (¬¬) &:=& λP:H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% (→→R) &:=& λP:H.((P{→}R){→}R) && (→→R)(P) &=& (P{→}R){→}R \\
% (∨Q) &:=& λP:H.(P{∨}Q) && (∨Q)(P) &=& P∨Q \\
% (→R) &:=& λP:H.(P{→}R) && (→R)(P) &=& P{→}R\\
% (∨Q∧→R) &:=& λP:H.((P{∨}Q) ∧ (P{→}R)) && (∨Q∧→R)(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
% $$
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ ___ | |_ _
% \___ \| |/ _` / __| '_ \ | '_ \ / _ \| | | | |
% ___) | | (_| \__ \ | | | | |_) | (_) | | |_| |
% |____/|_|\__,_|___/_| |_| | .__/ \___/|_|\__, |
% |_| |___/
% «slashings-are-poly» (to ".slashings-are-poly")
% (p2ap 25 "slashings-are-poly")
% (p2aa "slashings-are-poly")
% (jonp 24 "slashings-are-poly")
% (joa "slashings-are-poly")
\subsection{All slash-operators are polynomial}
\label {slashings-are-poly}
% (ph2p 51 "slashings-are-poly")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 30)
% (find-LATEX "2015planar-has.tex" "zquotients-poly")
{
%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="slaT", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):addlrs() :output():print()
%L mpnewJ({def="slaA", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):addlrs() :output():print()
%L mpnewJ({def="slaB", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):addlrs() :output():print()
%L mpnewJ({def="slaC", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):addlrs() :output():print()
%L mpnewJ({def="fooa", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):zhaPs("04") :output():print()
%L mpnewJ({def="foob", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):zhaPs("23") :output():print()
%L mpnewJ({def="fooc", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):zhaPs("45") :output():print()
%L mpnewJ({def="food", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):zhaPs("04 23 45"):output():print()
%L mpnew ({def="fooe", scale="7pt", meta="s"}, "1R2R3212RL1" ):addlrs():output()
%L mpnewJ({def="foof", scale="7pt", meta="s"}, "1R2R3212RL1", babc):zhaJ() :output()
\pu
Here is an easy way to see that all slashings --- i.e., J-operators on
ZHAs --- are polynomial. Every slashing $J$ has only a finite number of
cuts; call them $J_1, \ldots, J_n$. For example:
%
$$J=\slaT \qquad J_1=\slaA \quad J_2=\slaB \quad J_3=\slaC$$
Each cut $J_i$ divides the ZHA into an upper region and a lower
region, and $J_i(00)$ yields the top element of the lower region.
Also, $({→→}J_i(00))$ is a polynomial way of expressing that cut:
%
$$\def\foo#1#2{
\begin{array}{rr}
J_#1= \\
% ({→→}J_#1(00))= \\
(→→#2)= \\
\end{array}}
\foo1{04} \fooa \quad
\foo2{23} \foob \quad
\foo3{45} \fooc
$$
The conjunction of these `$({→→}J_i(00))$'s yields the original
slashing:
%
% $$
% \begin{array}{c}
% \fooa ∧ \foob ∧ \fooc = \food
% \end{array}
% $$
%
$$(→→04)∧(→→23)∧(→→45) = \food = J$$
}
% \newpage
% \input 2019J-ops-categories.tex % (find-LATEX "2019J-ops-categories.tex")
% \newpage
% \input 2019J-ops-classifier.tex % (find-LATEX "2019J-ops-classifier.tex")
% \newpage
% \input 2019J-ops-kan.tex % (find-LATEX "2019J-ops-kan.tex")
\newpage
% _____
% |_ _|__ _ __ ___ ___ ___ ___
% | |/ _ \| '_ \ / _ \/ __|/ _ \/ __|
% | | (_) | |_) | (_) \__ \ __/\__ \
% |_|\___/| .__/ \___/|___/\___||___/
% |_|
%
% «7._toposes» (to ".7._toposes")
% (p2ap 27 "7._toposes")
% (p2aa "7._toposes")
\section{Toposes}
\label{toposes}
\standout{Everything from here onwards will be rewritten!}
% (cltp 4 "inclusions")
% (clta "inclusions")
% (cltp 22 "SetCs-and-SetDs")
% (clta "SetCs-and-SetDs")
% ____ _ _ _
% / ___| ___ _ __ ___ ___ | |__ (_)(_)___
% \___ \ / _ \| '_ ` _ \ / _ \ | '_ \| || / __|
% ___) | (_) | | | | | | __/ | |_) | || \__ \
% |____/ \___/|_| |_| |_|\___| |_.__/|_|/ |___/
% |__/
%
% «some-bijections» (to ".some-bijections")
% (p2ap 25 "some-bijections")
% (p2aa "some-bijections")
\subsection{Some bijections}
% _ _ _ _
% / \ _ __ __ _ _ __| |_(_) ___ _ _| | __ _ _ __ ___ __ _ ___ ___
% / _ \ | '_ \ / _` | '__| __| |/ __| | | | |/ _` | '__| / __/ _` / __|/ _ \
% / ___ \ | |_) | (_| | | | |_| | (__| |_| | | (_| | | | (_| (_| \__ \ __/
% /_/ \_\ | .__/ \__,_|_| \__|_|\___|\__,_|_|\__,_|_| \___\__,_|___/\___|
% |_|
%
% «a-particular-case» (to ".a-particular-case")
% (p2ap 27 "a-particular-case")
% (p2aa "a-particular-case")
\subsection{A particular case}
[TODO: rewrite everything from this point onwards]
Fix a 2-column graph $(P,A)$, and let $\catD$ be the DAG $(P,A)$
regarded as a posetal category. Let $\catE$ be the topos $\Set^\catD$,
and let $H$ be the (planar) Heyting Algebra of truth-values of
$\catE$: $H=\CanSub(1_\catE)$. From here on $\catD$, $\catE$, and $H$
will be our default 2CG, our default topos, and our default ZHA. Let's
take this idea of ``defaults'' a bit further.
%D diagram bijections-with-names
%D 2Dx 100 +50 +70
%D 2D 100 \aqmarks \asubset \anucleus
%D 2D
%D 2D +40 \aclop
%D 2D
%D 2D +45 \agrtop \alttop
%D 2D
%D # ren ==>
%D
%D (( \aqmarks \asubset <-->
%D \asubset \anucleus <-> .plabel= b \LindC
%D \agrtop \alttop <-> .plabel= b \MM
%D \alttop \aclop <-> .plabel= r \CLT
%D \asubset \agrtop <-> .plabel= l \LindC
%D \anucleus \aclop <-->
%D \aqmarks \anucleus <-> .slide= 20pt .plabel= a \PHdois
%D ))
%D enddiagram
%D
$$\pu
\def\asubset {\pmtt{a subset}{$\calY⊆\catD_0$}}
\def\anucleus{\pmtt{a nucleus}{$(·)^*:H→H$}}
\def\agrtop {\pmttt{a Grothendieck}{topology}{$J⊂Ω$}}
\def\alttop {\pmtttt{a Lawvere-}{Tierney}{topology}{$j:Ω→Ω$}}
\def\aclop {\pmttt{a closure operator:}{for every $E∈\catE$ a}{$\clop_E:\Incs(E)→\Incs(E)$}}
\def\aqmarks {\pmtttt{a set of}{question}{marks}{$Q⊆\catD_0$}}
% (lindp 74 "C.4")
% (linda "C.4")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-books "__cats/__cats.el" "mclarty")
\def\MM {\smtttt{\cite{MacLaneMoerdijk}}{Sec V.4}{Thm 1}{p.233}}
\def\LindC {\smttt{\cite{Lindenhovius}}{Thm C4,}{p.74}}
\def\CLT {\smtt{\cite[sec.21]{McLarty},}{\cite[sec.2.6]{ClopsAndTops}}}
\def\PHdois {\smt{\cite{PH2}}}
\diag{bijections-with-names}
$$
In sections \ref{J-operators}--\ref{cubes} we saw a bijection that
converts each set of question marks $Q$ to a $J$-operator $(·)^*$ and
vice-versa. The theorem C4 of \cite{Lindenhovius} defines a bijection
that converts every J-operator $(·)^*$ to a subset $\calY⊂\calD_0$ and
vice-versa, and another bijection that converts each $\calY⊂\calD_0$
to a Grothendieck topology $J$ in $\Set^\catD$. Section V.4 of
\cite{MacLaneMoerdijk} how to convert each $J$ to a Lawvere-Tierney
topology $j$ and vice-versa, and \cite{McLarty} and
\cite{ClopsAndTops} show how to convert each $j$ to a closure operator
$\clop$ and vice-versa. Let's refer to the operations that perform the
conversions as $(Q \mapsto (·)^*)$, $((·)^* \mapsto Q)$, and so on;
for example,
$$\begin{array}{rcl}
(\calY \mapsto J) &=& λ\calY⊂\catD_0. \;
λu∈\catD_0. \;
\setofst{\calS∈Ω(u)}{\calY∩{↓}u⊂\calS}\\
(J \mapsto \calY) &=& λJ∈\GrTops(\catE). \;
\setofst{u∈\catD_0}{J(u)=\{{↓}u\}} \\
\end{array}
$$
This means that once we've chosen a value for $Q$, or for $\nuc$,
$\calY$, $J$, $j$, or $\clop$ the default values for the other ones
become automatically determined. Here is an example. If we choose $Q$
as in the top left below we get this:
%
% «ArtDecoN» (to ".ArtDecoN")
%
%L ArtDecoN_ts = TCGSpec.new("33; 32,"):LRcolstrs("!ga{L1} !ga{L2} !ga{L3}",
%L "!ga{R1} !ga{R2} !ga{R3}")
%L ArtDecoN_td_0 = TCGDims {h=15, v=8, q=15, crh=3.5, crv=7, qrh=5}
%L ArtDecoN_td_1 = TCGDims {h=25, v=22, q=15, crh=7.5, crv=7, qrh=5}
%L ArtDecoN_td_2 = TCGDims {h=65, v=50, q=15, crh=20, crv=15, qrh=5}
%L ArtDecoN_td_3 = TCGDims {h=85, v=70, q=15, crh=30, crv=30, qrh=5}
%L ArtDecoN_td_4 = TCGDims {h=85, v=80, q=15, crh=35, crv=35, qrh=5}
%L ArtDecoN_tq = TCGQ.newdsoa(ArtDecoN_td_0, ArtDecoN_ts,
%L {tdef="ArtDecoNSmall", meta="1pt s"},
%L "h ap LR o")
%L ArtDecoN_tq = TCGQ.newdsoa(ArtDecoN_td_1, ArtDecoN_ts,
%L {tdef="ArtDecoNMed", meta="1pt s"},
%L "h v ap LR o")
%L ArtDecoN_tq = TCGQ.newdsoa(ArtDecoN_td_2, ArtDecoN_ts,
%L {tdef="ArtDecoNBig", meta="1pt"},
%L "h v ap LR o")
%L ArtDecoN_tq = TCGQ.newdsoa(ArtDecoN_td_3, ArtDecoN_ts,
%L {tdef="ArtDecoNBigg", meta="1pt"},
%L "h v ap LR o")
%L ArtDecoN_tq = TCGQ.newdsoa(ArtDecoN_td_4, ArtDecoN_ts,
%L {tdef="ArtDecoNBigg", meta="1pt"},
%L "h v ap LR o")
\pu
%
\def\ArtDecoNSetargs#1#2#3#4#5#6{
\sa{L3}{#1}\sa{R3}{#2}%
\sa{L2}{#3}\sa{R2}{#4}%
\sa{L1}{#5}\sa{R1}{#6}%
}
%
% «ArtDecoN-shortdefs» (to ".ArtDecoN-shortdefs")
%
\def\adnsetargs#1{\ArtDecoNSetargs#1}
\def\adn #1{{\adnsetargs#1 \tcg{ArtDecoNSmall} }}
\def\padn #1{{\adnsetargs#1 \left( \tcg{ArtDecoNSmall} \right) }}
\def\badn #1{{\adnsetargs#1 \left[ \tcg{ArtDecoNSmall} \right] }}
\def\padnmed #1{{\adnsetargs#1 \left( \tcg{ArtDecoNMed} \right) }}
\def\padnbig #1{{\adnsetargs#1 \left( \tcg{ArtDecoNBig} \right) }}
\def\padnbigg #1{{\adnsetargs#1 \left( \tcg{ArtDecoNBigg} \right) }}
\def\padnbiggg #1{{\adnsetargs#1 \left( \tcg{ArtDecoNBigg} \right) }}
%
% «ArtDecoN-bijdefs» (to ".ArtDecoN-bijdefs")
% (find-es "dednat" "lawvere-tierney-mpunder")
%
%L -- Our spec:
%L ArtDecoNQ_ts = TCGSpec.new("33; 32, ", "..?",".?.")
%L
%L -- Question marks:
%L ArtDecoNQ_td_1 = TCGDims {h=35, v=25, q=15, crh=12, crv=8, qrh=5}
%L ArtDecoNQ_tq = TCGQ.newdsoa(ArtDecoNQ_td_1, ArtDecoNQ_ts,
%L {tdef="ArtDecoN-qmarks", meta="1pt p"},
%L "h v q ap"):lrs():output()
%L
%L -- Nucleus/J-operator:
%L ArtDecoNQ_ts:mp({zdef="ArtDecoN-nucleus", scale="12pt", meta=""}):addlrs():output()
%L
%L -- Components of the Lawvere-Tierney topology:
%L mp = ArtDecoNQ_ts:mpunder("32", {zdef="OADN:j:3_", scale="8pt", meta="s"}):output()
%L mp = ArtDecoNQ_ts:mpunder("20", {zdef="OADN:j:2_", scale="8pt", meta="s"}):output()
%L mp = ArtDecoNQ_ts:mpunder("10", {zdef="OADN:j:1_", scale="8pt", meta="s"}):output()
%L mp = ArtDecoNQ_ts:mpunder("03", {zdef="OADN:j:_3", scale="8pt", meta="s"}):output()
%L mp = ArtDecoNQ_ts:mpunder("02", {zdef="OADN:j:_2", scale="8pt", meta="s"}):output()
%L mp = ArtDecoNQ_ts:mpunder("01", {zdef="OADN:j:_1", scale="8pt", meta="s"}):output()
\pu
%
\def\QMarks {\tcg{ArtDecoN-qmarks}}
\def\RelevantPoints{
\cmat{ & ▁3, \\
2▁, & \\
1▁, & ▁1 \\
}}
\def\Nucleus{\zha{ArtDecoN-nucleus}}
%
\def\GrTopology{
\padnbig{
{{\badn{?·1?11}}} {\badn{·1·?·1}}
{\badn{··1·1·}} {\badn{···?·1}}
{\badn{····1·}} {\badn{·····1}}
}}
\def\LTTopology{
\padnbiggg{
{{\zha{OADN:j:3_}}} {\zha{OADN:j:_3}}
{\zha{OADN:j:2_}} {\zha{OADN:j:_2}}
{\zha{OADN:j:1_}} {\zha{OADN:j:_1}}
}}
%
%D diagram bijections-particular-case
%D 2Dx 100 +75 +115
%D 2D 100 \QMarks \RelevantPoints \Nucleus
%D 2D
%D 2D +120 \GrTopology \LTTopology
%D 2D
%D # ren ==>
%D
%D (( \QMarks \RelevantPoints <-->
%D \RelevantPoints \Nucleus <->
%D \GrTopology \LTTopology <->
%D \RelevantPoints \GrTopology <->
%D \Nucleus \LTTopology <-->
%D \QMarks \Nucleus <-> .slide= 35pt
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{bijections-particular-case}
$}
$$
Note that I have dropped the $\clop$ from the diagram. This is because
I don't have (yet) a good way to draw closure operators.
This diagram --- of a particular case! --- suggests that the points in
$\calY$ are exactly the points of $Q$ without question marks, and that
each $j(u):Ω(u)→Ω(u)$ is the slashing $\nuc$ restricted to ${↓}u$, or,
more precisely, that $j(u)(v) = v^*∧u$. If we remake that diagram for
the other 63 `$Q$'s, we see that this still holds. If we do the same
for some other 2CGs and for all `$Q$'s in them, we will see that the
same patterns still hold --- but there infinitely many 2CGs. We {\sl
can} obtain direct proofs that the `$\calY$'s are always the points
of $\catD_0$ without question marks, and that the `$\nuc$'s are
exactly the slashings and that the `$j$'s are obtained by restricting
the `$\nuc$'s, but some calculations may be hairy.
Remember that we are looking for ``visual intuition'' on what are the
`$\nuc$'s and their associates $j$'s and $J$. Are these fully
formalized proofs really necessary? Answer: not if we formalize
``visual intuition'' in the way that we do in the next section.
\def\smuv{\psm{u\\↓\\v\\}}
$$\begin{array}{rcl}
\nuc &:=& λ𝓢∈H. \; \bigcup\setofst{𝓡∈H}{𝓡∩𝓨=𝓢∩𝓨} \\
𝓨 &:=& \setofst{u∈\catD_0}{{↓}^-u∈H^*} \\
&=& \setofst{u∈\catD_0}{({↓}^-u)^* = {↓}^-u} \\
&=& \setofst{u∈\catD_0}{({↓}u∖\{u\})^* = ({↓}u∖\{u\})} \\
[5pt]
J &:=& λu∈\catD_0. \; \setofst{𝓢∈Ω(u)}{(𝓨∩{↓}u)⊆𝓢} \\
𝓨 &:=& \setofst{u∈\catD_0}{J(u)=\{{↓}u\}} \\
[5pt]
J &:=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ {↓}u = 𝓢^*∩{↓}u} \\
&=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ {↓}u ⊂ 𝓢^*} \\
&=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ u ∈ 𝓢^*} \\
\nuc &:=& λ𝓢∈H. \; \setofst{u\in \catD_0}{𝓢\cap{↓}u \in J(u)} \\
[5pt]
j &:=& λu∈\catD_0. \; λ𝓢∈Ω(u). \Cst(\setofst{v∈{↓}u}{Ω\smuv(𝓢)∈J(v)}) \\
&=& λu∈\catD_0. \; λ𝓢∈Ω(u). \Cst(\setofst{v∈{↓}u}{𝓢∩{{↓}v}∈J(v)}) \\
J &:=& λu∈\catD_0. \; \setofst{𝓢∈Ω(u)}{j(u)(𝓢) = ⊤(u)(*)} \\
&=& λu∈\catD_0. \; \setofst{𝓢∈Ω(u)}{j(u)(𝓢) = {↓}u} \\
\end{array}
$$
Hypotheses:
$$\begin{array}{rcl}
J(u) &:=& \setofst{𝓢∈Ω(u)}{𝓢^*∩{↓}u={↓}u} \\
j(u)(𝓢) &:=& 𝓢^*∩{↓}u \\
u∈Q &:=& ? \\
\\
J_j(p) & = & \{S\in D({↓} p):p\in j(S)\} \\
J_j(u) & = & \{S\in Ω(u) : u \in j(S)\} \\
J(u) & = & \{𝓢\in Ω(u) : u \in 𝓢^*\} \\
& = & \{𝓢\in Ω(u) : {↓}u ⊂ 𝓢^*\} \\
& = & \{𝓢\in Ω(u) : {↓}u = 𝓢^*∩{↓}u\} \\
J &:=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ {↓}u = 𝓢^*∩{↓}u} \\
&=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ {↓}u ⊂ 𝓢^*} \\
&=& λu∈\catD_0. \; \setofst{𝓢\in Ω(u) }{ u ∈ 𝓢^*} \\
\\
j_J(A) & = & \{p\in P:A\cap↓ p\in J(p)\} \\
𝓢^* & = & \setofst{u\in \catD_0}{𝓢\cap{↓}u \in J(u)} \\
\nuc & = & λ𝓢∈H. \; \setofst{u\in \catD_0}{𝓢\cap{↓}u \in J(u)} \\
\end{array}
$$
% (lindp 64 "B.25")
% (linda "B.25")
% __ ___ _ _ _ _ _ _
% \ \ / (_)___ _ _ __ _| | (_)_ __ | |_ _ _(_) |_(_) ___ _ __
% \ \ / /| / __| | | |/ _` | | | | '_ \| __| | | | | __| |/ _ \| '_ \
% \ V / | \__ \ |_| | (_| | | | | | | | |_| |_| | | |_| | (_) | | | |
% \_/ |_|___/\__,_|\__,_|_| |_|_| |_|\__|\__,_|_|\__|_|\___/|_| |_|
%
% «visual-intuition» (to ".visual-intuition")
% (p2ap 30 "visual-intuition")
% (p2aa "visual-intuition")
\section{Visual intuition}
\label {visual-intuition}
% (grcp 41 "meaning-from-pictures")
% (grca "meaning-from-pictures")
This is an excerpt from a long blog post by Kevin Buzzard
(\cite{Buzzard2021}):
%
% https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/
%
\begin{quote}
{\bf Mathematicians think in pictures}
I have a picture of the real numbers in my head. It's a straight
line. This picture provides a great intuition as to how the real
numbers work. I also have a picture of what the graph of a
differentiable function looks like. It's a wobbly line with no kinks
in. This is by no means a perfect picture, but it will do in many
cases. For example: If someone asked me to prove or disprove the
existence of a strictly increasing infinitely differentiable
function $f:\R→\R$ such that $f'(37)=0$ and $f''(37)<0$ then I would
start by considering a picture of a graph of a strictly increasing
function (monotonically increasing as we move from left to right),
and a second picture of a function whose derivative at $x=37$ is
zero and whose second derivative is negative (a function with a
local maximum). I then note that there are features in these
pictures which make them incompatible with each other. Working with
these pictures in mind, I can now follow my intuition and write down
on paper a picture-free proof that such a function cannot exist, and
this proof would be acceptable as a model solution to an exam
question. My perception is that other working mathematicians have
the same pictures in their head when presented with the same
problem, and would go through roughly the same process if they were
asked to write down a sketch proof of this theorem.
\end{quote}
Fulano talks of starting from visual intuition, and from that
producing conjectures and formal proofs; in sections 1 to 6 we
developed visual intuition for a well-known part of basic Topos
Theory. How can we put these two things in the same framework.
%D diagram bijections-letters-1
%D 2Dx 100 +30 +30
%D 2D 100 Q \calY \nuc
%D 2D ^
%D 2D +20 | \clop
%D 2D v |
%D 2D +20 J <---> j
%D 2D
%D # ren \nuc ==> (·)^*
%D
%D (( Q \nuc <-> .slide= +10pt
%D \calY \nuc <->
%D \calY J <->
%D J j <->
%D j \clop <->
%D ))
%D enddiagram
%D
$$\pu
\diag{bijections-letters-1}
$$
\newpage
%L write_dnt_file()
\pu
\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% _ _
% / \ _ ____ _(_)_ __
% / _ \ | '__\ \/ / \ \ / /
% / ___ \| | > <| |\ V /
% /_/ \_\_| /_/\_\_| \_/
%
% «arxiv» (to ".arxiv")
% (find-build-for-arxiv-links "2021planar-HAs-2")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
export PATH=/usr/local/texlive/2019/bin/x86_64-linux:$PATH
which biber
biber --version
make -f 2019.mk STEM=2021planar-HAs-2 veryclean
lualatex 2021planar-HAs-2.tex
biber 2021planar-HAs-2
pdflatex -record 2021planar-HAs-2.tex
# (find-LATEXfile "2021planar-HAs-2.fls" "biblatex/")
cd ~/LATEX/
flsfiles-zip 2021planar-HAs-2.fls 2021planar-HAs-2.zip
rm -rfv /tmp/2021planar-HAs-2.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/2021planar-HAs-2.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2021planar-HAs-2.zip
cd /tmp/edrx-latex/
pdflatex 2021planar-HAs-2.tex
pdflatex 2021planar-HAs-2.tex
cp -v 2021planar-HAs-2.pdf /tmp/
# (find-fline "/tmp/edrx-latex/")
# (find-fline "/tmp/edrx-latex/2021planar-HAs-2.bbl" "bbl format version")
# (find-pdf-page "/tmp/edrx-latex/2021planar-HAs-2.pdf")
# (find-pdf-text "/tmp/edrx-latex/2021planar-HAs-2.pdf")
# (find-fline "/tmp/2021planar-HAs-2.zip")
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021planar-HAs-2 veryclean
make -f 2019.mk STEM=2021planar-HAs-2 pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "p2a"
% End: