|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% To compile this with texmaker you need to tell texmaker to run
% lualatex, biber, and then lualatex again. To do this, select:
%
% Options -> Configure TeXmaker -> Quick build -> User
%
% and put this in the text box below the option "User":
%
% lualatex -interaction=nonstopmode %.tex|biber %|lualatex -interaction=nonstopmode %.tex
%
% Then <F1> ("Quick build") should do the right thing.
% Use <F7> ("View Pdf") to view the resulting PDF.
% (find-angg "LATEX/2017planar-has-1.tex")
% (find-angg "LATEX/2017planar-has-defs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has-1.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2017planar-has-1.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2017planar-has-1.pdf"))
% (defun b () (interactive) (find-sh "biber 2017planar-has-1"))
% (defun e () (interactive) (find-LATEX "2017planar-has-1.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017planar-has-1"))
% (find-pdf-page "~/LATEX/2017planar-has-1.pdf")
% (find-pdftools-page "~/LATEX/2017planar-has-1.pdf")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-1.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-1.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017planar-has-1.pdf
% file:///tmp/2017planar-has-1.pdf
% file:///tmp/pen/2017planar-has-1.pdf
% http://angg.twu.net/LATEX/2017planar-has-1.pdf
%
% (find-es "tex" "biber")
% (find-LATEX "2017planar-has-1.mk")
% (find-sh "make -f 2017planar-has-1.mk veryclean")
% (find-sh "make -f 2017planar-has-1.mk")
%
% (find-anggfile "LATEX/" "2017planar-has-1.tex")
% (find-twusfile "LATEX/" "2017planar-has-1")
% (find-twupfile "LATEX/" "2017planar-has-1")
% (find-twusfile "LATEX/" "2017planar-has-1-v1")
% (find-twupfile "LATEX/" "2017planar-has-1-v1")
% (find-TH "math-b" "zhas-for-children-2")
% http://angg.twu.net/math-b.html#zhas-for-children-2
%
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.introduction» (to "introduction")
% «.internal-external» (to "internal-external")
%
% «.positional» (to "positional")
% «.ZDAGs» (to "ZDAGs")
% «.LR-coords» (to "LR-coords")
% «.ZHAs» (to "ZHAs")
% «.two-conventions» (to "two-conventions")
% «.prop-calc» (to "prop-calc")
% «.prop-calc-ZHA» (to "prop-calc-ZHA")
% «.HAs» (to "HAs")
% «.calculating-and» (to "calculating-and")
% «.calculating-or» (to "calculating-or")
% «.calculating-imp» (to "calculating-imp")
% «.implication-new» (to "implication-new")
% «.logic-in-HAs» (to "logic-in-HAs")
% «.derived-rules» (to "derived-rules")
% «.natural-deduction» (to "natural-deduction")
% «.topologies» (to "topologies")
% «.topologies-on-ZSets» (to "topologies-on-ZSets")
% «.topologies-as-partial-orders» (to "topologies-as-partial-orders")
% «.2CGs» (to "2CGs")
% «.topologies-on-2CGs» (to "topologies-on-2CGs")
% «.topologies-as-HAs» (to "topologies-as-HAs")
% «.converting-ZHAs-2CAGs» (to "converting-ZHAs-2CAGs")
% «.ZHAL-is-between» (to "ZHAL-is-between")
%
% «.bibliography» (to "bibliography")
%
% «.clean-up-names» (to "clean-up-names")
% «.write-ph1-body» (to "write-ph1-body")
%
%\documentclass[pdftex]{sajl}
\documentclass[lualatex]{sajl}
\volume{X}
\issue{X}
\year{20XX}
\setcounter{page}{1}
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib} % (find-LATEX "catsem-u.bib")
\usepackage{latexsym,amssymb,amsfonts,amsmath}
\usepackage{graphicx}
\usepackage{array} % (find-es "tex" "array")
%\usepackage{hyperref} % (find-es "tex" "hyperref")
%\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%%\usepackage[latin1]{inputenc}
%\usepackage{amsmath}
%\usepackage{amsfonts}
%\usepackage{amssymb}
\usepackage{pict2e}
%\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
\usepackage{proof} % (find-dn6 "preamble6.lua" "preamble0")
\input diagxy % (find-dn6 "preamble6.lua" "preamble0")
%%
%\usepackage{edrx17} % (find-angg "LATEX/edrx17.sty")
\input edrxaccents.tex % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrx17defs.tex % (find-LATEX "edrx17defs.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
%\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
% (find-es "tex" "newtheorem")
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{remark}[definition]{Remark}
\newtheorem{remarks}[definition]{Remarks}
\newtheorem{example}[definition]{Example}
\newtheorem{examples}[definition]{Examples}
\newtheorem{corollary}[definition]{Corollary}
\newtheorem{myfigure}[definition]{Figure} % Edrx
\newcommand{\negr}[1]{\boldsymbol{#1}}
\newenvironment{proof}{\noindent\bf Proof. \rm}{\hfill $\negr{\blacksquare}$ \\}
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
\catcode`→=13 \def→{\rightarrow}
% FROM HERE
\def\Opens{\mathcal{O}}
\def\resizediag#1#2#3{\resizebox{#1}{#2}{$\diag{#3}$}}
\def\squigbijy{-2.8} % (find-LATEX "2017planar-has-defs.tex" "squigbijtest")
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
% (ph1p 1 "title")
% (ph1a "title")
\setlength{\extrarowheight}{1pt}
\title{Planar HAs for Children}{Planar Heyting Algebras for Children}
\author{E. Ochs}{Eduardo Ochs}
\maketitle
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% (ph1p 1 "abstract")
% (ph1a "abstract")
\begin{abstract}
This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} using finite Planar Heyting Algebras (``ZHAs''),
that are certain subsets of $\Z^2$. We also show the connection
between ZHAs and the familiar semantics for IPL where the truth-values
are open sets: the points of a ZHA $H$ correspond to the open sets of
a finite topological space $(P,\Opens_A(P))$, where the topology
$\Opens_A(P)$ is the order topology on a 2-column graph $(P,A)$. The
logic of ZHAs is between classical and intuitionistic but different
from both; there are some sentences that are intuitionistically false
but that can't have countermodels in ZHAs --- their countermodels
would need three ``columns'' or more.
In a wider context these ZHAs are interesting because toposes of the
form $\Set^{(P,A)}$ are one of the basic tools for doing ``Topos
Theory for Children'', in the following sense. We can {\sl define}
``children'' as people who think mathematically in a certain way ---
as {\sl people who prefer to start from particular cases and finite
examples that can be drawn explicitly, and only then generalize} ---
and we can define a method for working on a particular case (less
abstract, ``for children'') and on a general case (``for adults'') in
parallel, using parallel diagrams with similar shapes; we have some
ways of transfering knowledge from the general case to the particular
case, {\sl and back}. This method is sketched in the introduction.
Except for the introduction this paper is self-contained, and its
title ``Planar Heyting Algebras for Children'' also has a second
sense, different from the above: it can be read by students who have
just taken a basic course on Discrete Mathematics --- who are
``children'' in the sense that they don't have much mathematical
maturity --- and it prepares these students to read standard books on
Logic that they would otherwise find a bit too abstract.
This paper is the first in a series of three. Categories and toposes
only appear explicitly in the third one, that is about visualizing
geometric morphisms, and at this moment the method of parallel
diagrams has only been fully formalized for categorical diagrams.
Behind the choices of finite examples and particular cases in this
paper there is an {\sl attempt} to adapt that method to areas outside
Category Theory, but the precise details of how this is done are left
for a future work.
% Except for the introduction this paper is self-contained and can be
% read by students who have had a basic course on Discrete Mathematics
% This method of parallel diagram works much more naturally in
% Category Theory than in other areas of Mathematics, though --- and
% this is the first in a series of three papers, and categories and
% toposes only appear {\sl explicitly} in the third one
% --- and in the introduction we sketch some techniques for working
% on a particular case (``for children'') and on a general case (``for
% adults'') in parallel, using parallel diagrams with similar shapes.
% This paper is the first in a series of three, and categories,
% toposes, and the technique of parallel diagrams only appear, and are
% only used {\sl explicitly}, in the third paper. Except for the
% introduction and the last section this paper is self-contained, and
% its title ``Planar Heyting Algebras for Children'' also has a second
% sense, different from the above: it can be read by students who have
% just finished a course on Discrete Mathematics --- they are
% ``children'' in the sense that they don't have much mathematical
% maturity --- and it prepares them to read standard books on Logic
% that they would otherwise find a bit too abstract.
% When a mathematical text says ``for children'' this means either
% that it is written for people without lots of mathematical {\sl
% knowledge} or that it doesn't require mathematical {\sl maturity};
% we follow the second, stronger, meaning of the term. ``Children''
% for us means people who are not able to understand structures that
% are too abstract straight away, they need particular cases first ---
% and they also have trouble with infinite objects, and with theorems
% about things that they can't calculate: {\sl calculating} is much
% more basic for them than {\sl proving}. Writing ``for children''
% makes us enforce a style where everything is constructive and finite
% and all the main examples are objects that are easy to draw
% explicitly.
% When a mathematical paper is written ``for children'' this means
% either that it is written for people without lots of mathematical {\sl
% knowledge} or that it doesn't require mathematical {\sl maturity};
% we follow the second, stronger, meaning of the term. ``Children'' for
% us means people who are not able to understand structures that are too
% abstract straight away, they need particular cases first --- and they
% also have trouble with infinite objects, and with theorems about
% things that they can't calculate: {\sl calculating} is much more basic
% for them than {\sl proving}. Writing ``for children'' makes us enforce
% a style where everything is constructive and finite and all the main
% examples are objects that are easy to draw explicitly.
% Closure operators on Heyting Algebras are very important on Topos
% Theory: they generate geometric morphisms and sheaves. This paper
% introduces several tools that can be used to explain some parts of
% Topos Theory to ``children'', but here we stop just before
% categories and toposes --- when we move to categories and
% (pre)sheaves we have to replace most of the `0's and `1's in our
% diagrams by sets.
\end{abstract}
\keywords{Heyting Algebras, Intuitionistic Logic, diagrammatic
reasoning.}
\bsk
\bsk
% (find-kopkadaly4page (+ 12 58) "3.4 Table of contents")
%\tableofcontents
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (ph1p 2 "introduction")
% (ph1a "introduction")
This paper is the first in a series of three. Let's refer to them as
PH1 (this one), PH2 and PH3, and to the whole series as PH123. A
nearly complete working draft of PH2 is available at \cite{OchsPH2},
and the extended abstract \cite{OchsACT2019} shows the core results
that will be in PH3.
The objective of the series can be explained in two ways. In the first
one --- shallow, and purely mathematical,
\begin{itemize}
\item PH1 shows how to interpret IPL in Planar Heyting Algebras
(``ZHAs'', sec.\ref{ZHAs}) and shows that ZHAs are order topologies
on two-column graphs (``2CGs'', sec.\ref{2CGs}); this is used to
show how one can develop visual intuition about IPL. The trickiest
part is the implication; the method that allows one to calculate
$P→Q$ by sight in ZHAs has four subcases, and is discussed in
sections \ref{prop-calc-ZHA}, \ref{HAs}, and \ref{implication-new}.
It would probably be obvious to anyone who has worked enough with
lattices, but I believe that it deserves to be more widely known.
\item The paper PH2 extends the correspondence $(P,A)
\;\squigbijbody\; H$ between 2CGs and ZHAs of PH1 to a
correspondence $((P,A),Q) \;\squigbijbody\; (H,J)$ between 2CGs
``with question marks'' and ZHAs with a J-operator --- that, more
visually, are ZHAs ``with slashings''.
\item PH3 transports this to Topos Theory: if we regard a 2CG $(P,A)$
as a category, then $\Set^{(P,A)}$ is a topos whose objects are easy
to draw, and the logic of $\Set^{(P,A)}$ is exactly the ZHA
associated to $(P,A)$; also, a set of question marks $Q⊆P$ induces
an operation on $\Set^{(P,A)}$ that erases the information on $Q$
and reconstructs it in a natural way, and this
erasing-plus-reconstruction yields a sheafification functor --- that
is exactly the one associated to the local operator $j$ associated
to the J-operator $J$. This gives us a way to visualize (certain)
toposes, sheaves, geometric morphisms, and two factorizations of
geometric morphisms.
\end{itemize}
The second way to explain the goals of PH123 is by taking {\sl
Diagrammatic Reasoning} as the main theme. Let me start with an
anecdote (90\% true). Many, many years ago, when I tried to learn
Topos Theory for the first time, mainly from \cite{Johnstone} and
\cite{Goldblatt}, everything felt far too abstract: most of the
diagrams were omitted, and the motivating examples were mentioned very
briefly, if at all. The intended audience for those books surely knew
how to supply by themselves the missing diagrams, examples,
calculations, and details --- but I didn't. My slogan became: ``I need
a version for children of this!''.
At first this expression, ``for children'', was informal, and I used
it as a half-joke. Very gradually it started to acquire a precise
sense: clearly, CT done in a purely algebraic way is ``for adults'',
and diagrams, particular cases, and finite examples are ``for
children''. Writing ``for adults'' only and keeping the mentions to
the ``for children'' part very brief is considered good style because
``adults'' have the technical machinery for producing more or less
automatically the ``for children'' part when they need it, and people
who are not yet ``adults'' can become ``adults'' by struggling with
the texts ``for adults'' long enough and learning by themselves how to
handle the new level of abstraction.
A clear frontier between ``for adults'' and ``for children'' appears
when we realize that we can draw a diagram for the general case (``for
adults'') of a categorical concept and the diagram for a particular
case of it (``for children'') side by side. The two diagrams will have
roughly the same shape, and we can transport knowledge between them in
both ways: from the general to the particular, {\sl and back}. Look at
Figure \ref{fig:internal-external}; let's name its subdiagrams as $A$,
$B$, and $C$, like this: $\sm{A \; B \\ C}$. Each one of $A$, $B$, $C$
has an {\sl internal view} above and an {\sl external view} below.
% (oxap 4 "fig:internal-1")
% (oxa "fig:internal-1")
% «internal-external» (to ".internal-external")
% (ph1p 4 "internal-external")
% (ph1a "internal-external")
\def\ooo (#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx 100 +20 +20
%D 2D 100 a-1 |--> b-1
%D 2D +08 a0 |--> b0
%D 2D +08 a1 |--> b1
%D 2D +08 a2 |--> b2
%D 2D +08 a3 |--> b3
%D 2D +08 a4 |--> b4
%D 2D +14 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D (( a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D b-1 place
%D a0 b0 |->
%D a1 b1 |->
%D a2 b2 |->
%D a3 b3 |->
%D a4 b4 |->
%D a5 b5 |->
%D \N \R -> .plabel= a \sqrt{\phantom{a}}
%D a-1 relplace -7 -7 \phantom{foo}
%D b5 relplace 7 7 \phantom{bar}
%D ))
%D enddiagram
%D
%D diagram generic-adjunction
%D 2Dx 100 +30 +35 +25
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +30 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +30 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +30 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> LA' A'
%D ren LB B ==> LA A
%D ren C RC ==> B RB
%D ren D RD ==> B' RB'
%D ren E F ==> \catB \catA
%D ren G H ==> LRB B
%D ren I J ==> A RLA
%D
%D (( LA A <-| .plabel= a L_0
%D LB B <-| .plabel= a L_0
%D C RC |-> .plabel= b R_0
%D D RD |-> .plabel= b R_0
%D
%D LA B harrownodes nil 20 nil <-| sl^ .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> sl^ .plabel= b R_1
%D
%D LA LB -> .plabel= l Lα
%D A B -> .plabel= r α
%D LB C -> .plabel= l \sm{g^♭\\f}
%D B RC -> .plabel= r \sm{g\\f^♯}
%D C D -> .plabel= l β
%D RC RD -> .plabel= r Rβ
%D E F <- sl^ .plabel= a L
%D E F -> sl_ .plabel= b R
%D G H -> .plabel= l εB
%D I J -> .plabel= r ηA
%D ))
%D enddiagram
%D
%D diagram (xB)-|(B->)
%D 2Dx 100 +45 +35 +40
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +30 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +30 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +30 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> A{×}C A
%D ren LB B ==> B{×}C B
%D ren C RC ==> D (C{→}D)
%D ren D RD ==> E (C{→}E)
%D ren E F ==> \Set \Set
%D ren G H ==> (C{→}D){×C} D
%D ren I J ==> B (C→B{×}C)
%D ren I J ==> B (C{→}(B{×}C))
%D
%D (( LA A <-| # .plabel= a ({×}B)_0
%D LB B <-| # .plabel= a ({×}B)_0
%D C RC |-> # .plabel= b (B{→})_0
%D D RD |-> # .plabel= b (B{→})_0
%D
%D LA B harrownodes nil 20 nil <-| sl^ # .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> sl^ # .plabel= b R_1
%D
%D LA LB -> .plabel= l λp.(f(πp),π'p)
%D A B -> .plabel= r f
%D LB C -> .plabel= l \sm{λp.g(πp)(π'p)\\\phantom{mmmmmm}h}
%D B RC -> .plabel= r \sm{g\phantom{mmmmm}\\λb.λc.h(b,c)}
%D C D -> .plabel= l k
%D RC RD -> .plabel= r λf.λc.k(fc)
%D E F <- sl^ .plabel= a ({×}C)
%D E F -> sl_ .plabel= b (C{→})
%D G H -> .plabel= l λp.(πp)(π'p)
%D I J -> .plabel= r λb.λc.(b,c)
%D ))
%D enddiagram
%D
\begin{figure}[!htbp]
\pu
\centering
$\begin{array}{c}
\resizediag{!}{!}{second-blob-function}
\qquad
\resizediag{!}{!}{generic-adjunction}
\\
\\
\resizediag{!}{!}{(xB)-|(B->)}
\end{array}
$
\caption{Three cases of internal views and external views.}
\label{fig:internal-external}
\end{figure}
Diagram $A$ shows, below, the external view of the function $\N
\ton{\sqrt{\phantom{a}}} \R$, and above that its internal view --- in
which one of the arrows, $n \mapsto \sqrt{n}$, shows the action of
$\sqrt{\phantom{a}}$ on a generic element, and the other `$\mto$'
arrows, like $3 \mapsto \sqrt{3}$ and $4 \mapsto 2$, show substitution
instances of $n \mapsto \sqrt{n}$, maybe after some term reductions.
Diagram $B$ shows the external view of a (generic) adjunction $L⊣R$,
and above it its internal view. The nodes and arrows above $\catB$ are
objects and morphisms in $\catB$, and similarly for the nodes and
arrows above $\catA$. The `$\mto$' arrows of the internal view are now
of three kinds: actions of functors on objects, actions of functors on
morphisms, and ``transpositions'' coming from the natural isomorphism
$\Hom(L-,-) ↔ \Hom(-,R-)$. Diagram $C$ is essentially the same as $B$,
but for a particular adjunction: $({×}B)⊣(B{→})$. Note how the
diagrams $B$ and $C$ have exactly the same shape --- but our diagrams
for internal views are much bigger than the corresponding external
views.
For a case in which the interplay between external and internal views
is examined in full detail, see \cite{OchsNotesOnYoneda}; it shows how
each node and arrow in the diagrams can be can interpreted as a term
in a type system, and this {\sl may} be a basis for analyzing
precisely which kinds of knowledge, and which kinds of intuitions ---
as in \cite{Kromer}, especially sec.1.3.2, and in \cite{Corfield} ---
we are transporting from the less abstract diagrams to the more
abstract ones, and vice-versa. Note that having a clearly-defined
method for lifting information --- in the sense of \cite{OchsIDARCT}
--- from a case ``for children'' to a case ``for adults'' would allow
people to publish much more material ``for children'' than they do
now, without this being regarded as bad style. For a non-trivial
example of lifting information from a particular case to a general
case, see \cite{OchsACT2019}.
\msk
This paper can be seen as part of bigger projects in at least the two
ways described above, but it was also written to be as readable and as
self-contained as possible. In 2016 and 2017 I had the opportunity to
test some of the ideas here on ``real children'', in the sense of
``people with little mathematical {\sl knowledge} and little
mathetical {\sl maturity}''. I gave a seminar course about Logic and
$λ$-calculus that had no prerequisites, and that was mostly based on
exercises that the students would try to solve together by discussing
on the whiteboard; it was mostly attended by Computer Science students
who had just finished a course on Discrete Mathematics, but there were
also some Psychology and Art students --- that unfortunately left
after the first weeks of each semester. All these students, including
the CompSci ones, had in common that definitions only made sense to
them after they had played with a few concrete examples; at some parts
of the course I would ask them to read some sections of this paper,
then work on some extra exercises that I had prepared, and then read
excerpts of books like \cite{VanDalen} or \cite{Awodey}. Most sections
of this paper had been tested ``on real children'' in this way, and
were rewritten several times after their feedback and reactions. I owe
them many thanks --- I'm glad that they had fun in the process -- and
I hope that I'll be able in the future to transform what I learned
with them into precise techniques for writing ``for children''.
% (find-LATEX "catsem-u.bib" "bib-VanDalen")
% So: how much Topos Theory can one learn by using toposes of the form
% $\Set^\PAS$ as the archetypal examples of toposes, and where is this
% person's intuition going to fail when he or she passes to arbitrary
% toposes? This first paper does not discuss toposes, or even
% categories, but it has a small example of intuition failing: a
% person with very good visual thinking may be led to believe
% (wrongly) that the sentence $S$ of sec.\ref{ZHAL-is-between} is an
% intuitionistic theorem because it is true in all ZHAs.
\bsk
% The upper right part and the lower part --- ``generic case'' and
% ``particular case'' --- have the same {\sl shape}, so its easy to
% transfer knowledge from the generic case to the particular case,
% {\sl and back}; and as these diagrams can be formalized in Type
% Systems and proof assistants (see \cite{OchsNotesOnYoneda}) we can
% be precise about which kinds of knowledge we are transfering back
% and forth, and map this onto the kinds of {\sl mathematical
% intuitions} discussed in, say, \cite{Corfield} and \cite{Kromer}.
% Once we develop and formalize a set of precise techniques for
% ``lifting'' (in the sense of \cite{OchsIDARCT}) ideas from
% particular cases to general cases we become allowed to use
% particular cases in our papers, and analyse them at length without
% this being considered bad mathematical style.
%
% Once we develop and formalize a set of precise techniques for
% ``lifting'' (in the sense of \cite{OchsIDARCT}) ideas from
% particular cases to general cases we become allowed to use
% particular cases in our papers, and analyse them at length without
% this being considered bad mathematical style.
%
% These techniques for transfering knowledge between ``general'' and
% ``particular'' --- that were somewhat inspired by Non-Standard
% Analysis, with its transfer theorems between a universe with
% infinitesimals and one without --- are easy to formalize for
% Category Theory, that only appears in PH3. PH1 and PH2 use
% particular cases a lot, in a style that is an attempt --- still
% informal --- to adapt these techniques to mathematics outside CT.
% \printbibliography
% \end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The ``for children'' of the title uses the term ``children'' in a
% unusual way. When we explain a theorem to children --- in the strict
% sense of the term --- we focus on concrete examples, and we avoid
% generalizations, abstract structures and infinite objects; when we
% present something to ``children'', now in the wider sense of the term
% that means ``people without mathematical maturity'', or even ``people
% without expertise in a certain area'', we usually do something
% similar: we start from a few motivating examples, and only then we
% generalize. This is in stark contrast with how things are done for
% example in most books on Category Theory, where concepts are usually
% presented first in the most general way possible, and then the
% motivating cases are mentioned very briefly --- let's call that style
% ``mathematics for adults''. Here we try to do things in particular
% cases first, but in a way that our proofs can be ``lifted'' to general
% proofs with ease, with only trivial changes.
%
% Except for the last section, this paper has been written to be
% self-contained and readable by students with just a basic knowledge of
% discrete mathematics and $λ$-notation.
%
% \msk
%
% Two sequels to this paper are in preparation: one that shows how to
% visualize ``closure operators'' on ZHAs, and another one that uses
% that to show how to visualize several theorems about geometric
% morphism on toposes (from section A4 of \cite{Elephant1}). It may be
% possible, in the future, to find meta-theorems about how to do
% ``mathematics for adults'' via ``mathematics for children'', or to
% find criteria that say which examples ``for children'' are good enough
% for lifting; but at this moment we are simply beginning to build a
% corpus of examples and techniques --- an approach was inspired by
% sections 22 and 23 of \cite{OchsIDARCT}.
%
% Take a set $S=\{S_1, \ldots, S_n\}$ of freshmen students. Tell them
% ``Let $B$ be the set of all birds'', and ask them to take a piece of
% paper each and write down elements of $B$; let's call their lists
% $L_1, \ldots, L_n$. After some time we ask them to read their lists
% aloud, as we write the elements on the blackboard in an attempt to
% create a list $L=L_1∪\ldots∪L_n$. What usually happens\footnote{At
% least with me; I've done this experiment several times} is that
% disagreements will start to appear: $S_1$ has put Tweety but $S_2$
% complains that Tweety can't on the list because it's a {\sl fictional}
% bird; they can't agree if $S_3$'s pet parrot is the same bird as
% $S_4$'s parrot or not; ``hen'' may be the same of ``chick'', only
% older; they may not be sure if penguin, ostrich and archeopteryx are
% valid elements; and does that set $B$ change when a bird dies, or
% becomes extinct, of when a new species of feathered dinosuar is
% discovered?
%
% The use of ``real-world sets'' like $B$ often makes Maths confusing.
% Similar things also happen in other areas: for example, the standard
% way of teaching Object-Oriented Programming starts by saying that
% ``objects'' are things like shapes, windows, cars, and pizzas, and
% this idea baffles and paralyzes people who can't imagine ways to
% represent these objects in a computer...
%
% \begin{itemize}
% \item Category theory should be more accessible
%
% Most texts about CT are for specialists in research universities...
% {\sl Category theory should be more accessible.}.
%
% To whom?...
%
% \begin{itemize}
% \item Non-specialists (in research universities)
% \item Grad students (in research universities)
% \item Undergrads (in research universities)
% \item Non-specialists (in conferences - where we have to be quick)
% \item Undergrads (e.g., in CompSci - in teaching colleges) - (``Children'')
% \end{itemize}
%
% \item What do we mean by "accessible"?
%
% \begin{itemize}
% \item Done on very firm grounds: mathematical objects made from
% numbers, sets and tuples; FINITE, SMALL mathematical objects
% whenever possible. Avoid references to non-mathematical things like
% windows, cars and pizzas (like the object-orientation people do);
% avoid reference to Physics; avoid Quantum Mecanics at all costs;
% time is difficult to draw, prefer {\sl static} rather than {\sl
% changing}
%
% \item People have very short attention spans nowadays
%
% \item Self-contained, but not {\sl isolated} or {\sl isolating}; our
% material should make the literature more accessible
%
% \item We learn better by doing. Our material should have lots of space
% for exercises.
%
% \item Most people with whom I interact are not from Maths/CS/etc
%
% \item {\sl Proving} general cases is relatively hard. {\sl Checking}
% and {\sl calculating} is much easier. People can believe that
% something can be generalized after seeing a convincing particular
% case. (Sometimes leave them to look for the right generalization by
% themselves)
% \end{itemize}
% \end{itemize}
%
%
%
% Except for two last sections all the rest of this paper has been
% written to be readable by ``children'' in the sense above, and huge
% parts of it have been tested on ``real children'' of mainly two kinds:
% a group of ``older children'', who are Computer Science students who
% had already completed a course on Discrete Mathematics, and some
% ``little children'', who are friends of mine who are students of
% Psychology or Social Sciences. The text has benefited enormously from
% they feedback --- especially their puzzled looks at some points, that
% made me modify my presentation and the exercises I was giving to them.
% Those exercises are not included here, though, and neither the
% rationale behind most style decisions.
% \section*{New introduction}
%
% \def\PAS{{{(P,A^*)}}}
%
% This paper is the first in a series of three, and one way to explain
% the goal of the whole series is this. Toposes of the form
% $\Set^\PAS$, where $\PAS$ is the preorder category associated to a
% 2-column graph $(P,A)$, are interesting to students of Topos Theory
% because their objects are easy to draw explicitly, and because by
% working on them one can develop a lot of visual intuition about what
% certain categorical constructions ``mean''; in particular, the
% ``logic'' of a $\Set^\PAS$, i.e., its $\Sub(1)$, is a Planar Heyting
% Algebra, and some ways to visualize sheaves on a $\Set^\PAS$ are
% presented in the second paper in this series.
% A better way to explain the goal of this series of papers needs the
% term ``children''. Many years ago, when I started learning Category
% Theory and Topos Theory from \cite{CWM} and \cite{Johnstone}, I felt
% that I was taking far more time than reasonable to supply the diagrams
% that were ``omitted'' from the text, and treatd as they were trivial
% exercises (see \cite{Kromer}, p.(?)); I kept saying to my colleagues
% ``I need a version `for children' of this!'' --- but at that time this
% was a half-joke and it didn't have a precise meaning. Years later it
% became clear that once we have a precise meaning for ``children'' ---
% as people with certain style of thinking; compare with ``people who
% think algebraically'' and ``people who think geometrically'' --- this
% yields {\sl guidelines} on how to {\sl complement} a standard
% categorical text, and produce auxiliary material that makes the
% original presaentation --- abstract, ``for adults'' --- more
% accessible.
% It turned out that the following {\sl definition} of ``children'' is
% especially fruitful. ``Children'':
%
% 1) have trouble with very abstract definitions,
%
% 2) prefer to start from particular cases (and only then generalize),
%
% 3) handle diagrams better than algebraic notations,
%
% 4) like finite objects that can be drawn explicitly, and that are
% built just from numbers by forming lists and sets,
%
% 5) develop intuition about mathematical objects mostly by ``playing''
% with them, and by learning how to do calculations quickly; {\sl
% calculating} for them is much more basic than {\sl proving
% theorems},
%
% 6) tend to remember categorical definitions and proofs
% ``positionally'' by diagrams that are always drawn in a certain way.
%
% Item 6 has an important consequence. Once we establish that, for
% example, our geometric morphisms will be drawn like this,
% %
% $$(diagram)$$
% %
% then all our particular cases of geometric morphisms became diagrams
% with the same shape of that one --- [slides] and [PH3] have a
% medium-sized example --- and we can {\sl transfer knowledge} from one
% side to the other and vice-versa; it is easy to transfer a
% construction done on the diagram for the general case (``for adults'')
% to the particular case (``for children''), and sometimes it is also
% possible to start
% ____ _ _ _ _
% | _ \ ___ ___(_) |_(_) ___ _ __ __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _` | |
% | __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_| \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% «positional» (to ".positional")
\section{Positional notations}
\label {positional}
% (ph1p 5 "positional")
% (ph1a "positional")
% (laq 2)
% (laq 3)
% (gaap 5)
% (to "picturedots")
\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}
Definition: a {\sl ZSet} is a finite, non-empty subset of $\N^2$ that
touches both axes, i.e., that has a point of the form $(0,\_)$ and a
point of the form $(\_,0)$. We will often represent ZSets using a
bullet notation, with or without the axes and ticks. For example:
%
$$K =
\csm{ & (1,3), & \\
(0,2), & & (2,2), \\
& (1,1), & \\
& (1,0) & \\
}
= \;\picturedotsadef{k0a}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
= \;\picturedotsdef {k0}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
$$
We will use the ZSet above a lot in examples, so let's give it a short
name: $K$ (``kite'').
The condition of touching both axes is what lets us represent ZSets
unambiguously using just the bullets:
%
% $$ \;\picturedotsa(0,0)(4,4){ 3,4 2,3 4,3 3,2 3,1 }\;
% \sa \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
% \sa \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
% \quad =\!(
% \qquad
% \qquad
% \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
% \sa \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
% \sa \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
% \quad =)
% $$
%
$$\begin{array}{r}
\;\picturedotsadef{k1}(0,0)(4,4){ 3,4 2,3 4,3 3,2 3,1 }\;
\sa \;\picturedotsdef {k2}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
\sa \;\picturedotsadef{k3}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
\quad =\!(
\\
\\
\;\picturedotsadef{k4}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
\sa \;\picturedotsdef {k5}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
\sa \;\picturedotsadef{k6}(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
\quad =)
\\
\end{array}
$$
We can use a positional notation to represent functions {\sl from} a
ZSet. For example, if
%
$$\begin{array}{ccrcl}
f &:& K &→& \N \\
& & (x,y) &↦& x \\
\end{array}
$$
%
then
%
$$f =
\csm{ & ((1,3),1), & \\
((0,2),0), & & ((2,2),2), \\
& ((1,1),1), & \\
& ((1,0),1) & \\
}
=
\sm{ & 1 & \\
0 & & 2 \\
& 1 & \\
& 1 & \\
}
$$
We will sometimes use $λ$-notation to represent functions compactly.
For example:
%
$$λ(x,y){:}K.x =
\csm{ & ((1,3),1), & \\
((0,2),0), & & ((2,2),2), \\
& ((1,1),1), & \\
& ((1,0),1) & \\
}
=
\sm{ & 1 & \\
0 & & 2 \\
& 1 & \\
& 1 & \\
}
$$
%
$$λ(x,y){:}K.y =
\csm{ & ((1,3),3), & \\
((0,2),2), & & ((2,2),2), \\
& ((1,1),1), & \\
& ((1,0),0) & \\
}
=
\sm{ & 3 & \\
2 & & 2 \\
& 1 & \\
& 0 & \\
}
$$
The ``reading order'' on the points of a ZSet $S$ ``lists'' the points
of $S$ starting from the top and going from left to right in each
line. More precisely, if $S$ has $n$ points then
$r_S:S→\{1,\ldots,n\}$ is a bijection, and for example:
%
$$r_K = \sm{ & 1 & \\
2 & & 3 \\
& 4 & \\
& 5 & \\
}
$$
Subsets of a ZSet are represented with a notation with `$\bullet$'s
and `$\cdot$', and partial functions from a ZSet are represented with
`$\cdot$'s where they are not defined. For example:
%
$$\sm{ & • & \\
· & & • \\
& • & \\
& · & \\
}
\qquad
\sm{ & 1 & \\
· & & 3 \\
& 4 & \\
& · & \\
}
$$
%L kite = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite", meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW", meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex", meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu
The {\sl characteristic function} of a subset $S'$ of a ZSet $S$ is
the function $\chi_{S'}:S→\{0,1\}$ that returns 1 exactly on the
points of $S'$; for example, $\dagKite10110$ is the characteristic
function of $\dagKite{•}{·}{•}{•}{·} ⊂ \dagKite{•}{•}{•}{•}{•}$. We
will sometimes denote subsets by their characteristic functions
because this makes them easier to ``pronounce'' by reading aloud their
digits in the reading order --- for example, $\dagKite10110$ is
``one-zero-one-one-zero'' (see sec.\ref{topologies-on-ZSets}).
% _________ _ ____
% |__ / _ \ / \ / ___|___
% / /| | | |/ _ \| | _/ __|
% / /_| |_| / ___ \ |_| \__ \
% /____|____/_/ \_\____|___/
%
% «ZDAGs» (to ".ZDAGs")
% (ph1p 6 "ZDAGs")
% (ph1a "ZDAGs")
\section{ZDAGs}
\label {ZDAGs}
We will sometimes use the bullet notation for a ZSet $S$ as a {\sl
shorthand} for one of the two DAGs induced by $S$: one with its
arrows going up, the other one with them going down. For example:
sometimes
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
%
%R local K =
%R 1/ o \
%R |o o|
%R | o |
%R \ o /
%R K:tomp({def="Kmini", scale="4pt", meta="s"}):addbullets() :output()
%R K:tomp({def="Kb", scale="8pt", meta=nil}):addbullets() :output()
%R K:tomp({def="KB", scale="24pt", meta=nil}):addbullets():addarrows(nil):output()
%R K:tomp({def="Kn", scale="24pt", meta=nil}):addxys ():addarrows(nil):output()
%R -- mp:output()
%
\pu
$$%\pu
\Kb \;\;\;\;\text{will stand for:}\;\;
\KB =
\Kn =
$$
$$
\qquad
\qquad
\qquad
\qquad
\pmat{
% \cmat{ & (1,3), & \\
% (0,2), & & (2,2), \\
% & (1,1), & \\
% & (0,0) & \\
% },
\csm{ (1,3), \\
(0,2), \phantom{(1,2),} (2,2), \\
(1,1), \\
(0,0) \\
},
\csm{ ((1,3),(0,2)), ((1,3),(2,2)), \\
((0,2),(1,1)), ((2,2),(1,1)), \\
((1,1),(0,0)) \\
}
}
$$
\msk
Let's formalize this.
Consider a game in which black and white pawns are placed on points of
$\Z^2$, and they can move like this:
%
%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="10pt", meta=nil}):addcells(T):output()
%R W:tozmp({def="Wmne", scale="10pt", meta=nil}):addcells(T):output()
$$\pu \Bmne \qquad \Wmne
$$
Black pawns can move from $(x,y)$ to $(x+k,y-1)$ and white pawns from
$(x,y)$ to $(x+k,y+1)$, where $k∈\{-1,0,1\}$. The mnemonic is that
black pawns are ``solid'', and thus ``heavy'', and they ``sink'', so
they move down; white pawns are ``hollow'', and thus ``light'', and
they ``float'', so they move up.
Let's now restrict the board positions to a ZSet $S$. Black pawns can
move from $(x,y)$ to $(x+k,y-1)$ and white pawns from $(x,y)$ to
$(x+k,y+1)$, where $k∈\{-1,0,1\}$, but only when the starting and
ending positions both belong to $S$. The sets of possible black pawn
moves and white pawn moves on $S$ can be defined formally as:
%
$$\mat{
\BPM(S) = \setofst {((x,y),(x',y'))∈S^2} {x-x'∈\{-1,0,1\}, y'=y-1} \\
\WPM(S) = \setofst {((x,y),(x',y'))∈S^2} {x-x'∈\{-1,0,1\}, y'=y+1} \\
}
$$
%
...and now please forget everything else you expect from a game ---
like starting position, capturing, objective, winning... the idea of a
``game'' was just a tool to let us explain $\BPM(S)$ and $\WPM(S)$
quickly.
\msk
A {\sl ZDAG} is a DAG of the form $(S,\BPM(S))$ or $(S,\WPM(S))$,
where $S$ is a ZSet.
A {\sl ZPO} is partial order of the form $(S,\BPM(S)^*)$ or
$(S,\WPM(S)^*)$, where $S$ is a ZSet and the `${}^*$' denotes the
transitive-reflexive closure of the relation.
\msk
Sometimes, when this is clear from the context, a bullet diagram like
$\Kmini$ will stand for either the ZDAGs $(\Kmini,\BPM(\Kmini))$ or
$(\Kmini,\WPM(\Kmini))$, or for the ZPOs $(\Kmini,\BPM(\Kmini)^*)$ or
$(\Kmini,\WPM(\Kmini)^*)$ (sec.\ref{ZHAs}).
% or even for the ZPOs seen as categories (section $\_\_\_$).
% _ ____ _ _ _
% | | | _ \ ___ ___ ___ _ __ __| (_)_ __ __ _| |_ ___ ___
% | | | |_) | / __/ _ \ / _ \| '__/ _` | | '_ \ / _` | __/ _ \/ __|
% | |___| _ < | (_| (_) | (_) | | | (_| | | | | | (_| | || __/\__ \
% |_____|_| \_\ \___\___/ \___/|_| \__,_|_|_| |_|\__,_|\__\___||___/
%
% «LR-coords» (to ".LR-coords")
\section{LR-coordinates}
\label {LR-coords}
% (ph1p 7 "LR-coords")
\def\LR{\mathbb{LR}}
The {\sl lr-coordinates} are useful for working on quarter-plane of
$\Z^2$ that looks like $\N^2$ turned $45°$ to the left. Let $\ang{l,r}
:= (-l+r,l+r)$; then (the bottom part of)
$\setofst{\ang{l,r}}{l,r∈\N}$ is:
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
% (find-dn6file "zhas.lua" "addxys =")
%
%R local zhav =
%R 1/o o o o o\
%R | o o o o |
%R | o o o |
%R | o o |
%R \ o /
%R mplr = zhav:tomp({def="mplra", scale="14pt", meta="s"})
%R mpxy = zhav:tomp({def="mpxya", scale="14pt", meta="s"})
%R mplr = zhav:tomp({def="mplra", scale="21pt", meta=nil})
%R mpxy = zhav:tomp({def="mpxya", scale="21pt", meta=nil})
%R f = function (p) local l,r = p:to_l_r(); return "\\ang{"..l..","..r.."}" end
%R for p,str in mplr:points() do mplr:put(p, f(p-v(4,0))) end
%R for p,str in mpxy:points() do mpxy:put(p, (p-v(4,0)):xy()) end
%R mplr:output()
%R mpxy:output()
%
$$\pu
\mplra
\quad =
\quad
\mpxya
$$
Sometimes we will write $lr$ instead of $\ang{l,r}$. So:
%
%R local zhav =
%R 1/o o o o o\
%R | o o o o |
%R | o o o |
%R | o o |
%R \ o /
%R mplr = zhav:tomp({def="mplr", scale="13.5pt", meta="s"})
%R mpxy = zhav:tomp({def="mpxy", scale="14pt", meta="s"})
%R mplr = zhav:tomp({def="mplr", scale="19pt", meta=nil})
%R mpxy = zhav:tomp({def="mpxy", scale="20pt", meta=nil})
%R f = function (p) local l,r = p:to_l_r(); return l..r end
%R for p,str in mplr:points() do mplr:put(p, f(p-v(4,0))) end
%R for p,str in mpxy:points() do mpxy:put(p, (p-v(4,0)):xy()) end
%R mplr:output()
%R mpxy:output()
%
$$\pu
\mplr
\quad =
\quad
\mpxy
$$
Let $\LR = \setofst{\ang{l,r}}{l,r∈\N}$.
% ______ _ _
% |__ / | | | / \ ___
% / /| |_| | / _ \ / __|
% / /_| _ |/ ___ \\__ \
% /____|_| |_/_/ \_\___/
%
% «ZHAs» (to ".ZHAs")
% (ph1p 8 "ZHAs")
% (ph1a "ZHAs")
\section{ZHAs}
\label {ZHAs}
A {\sl ZHA} is a subset of $\LR$ ``between a left and a right wall'',
as we will see.
\msk
A triple $(h,L,R)$ is a ``height-left-right-wall'' when:
1) $h∈\N$
2) $L:\{0,\ldots,h\}→\Z$ and $R:\{0,\ldots,h\}→\Z$
3) $L(h)=R(h)$ (the top points of the walls are the same)
4) $L(0)=R(0)=0$ (the bottom points of the walls are the same, $0$)
5) $∀y∈\{0,\ldots,h\}.\,L(y)≤R(y)$ (``left'' is left of ``right'')
6) $∀y∈\{1,\ldots,h\}.\,L(y)-L(y-1)=\pm1$ (the left wall makes no jumps)
7) $∀y∈\{1,\ldots,h\}.\,R(y)-R(y-1)=\pm1$ (the right wall makes no jumps)
\msk
The {\sl ZHA generated by} a height-left-right-wall $(h,L,R)$ is the
set of all points of $\LR$ with valid height and between the left and
the right walls. Formally:
$$\ZHAG(h,L,R) = \setofst {(x,y)∈\LR} {y≤h, L(y)≤x≤R(y)}.$$
A {\sl ZHA} is a set of the form $\ZHAG(h,L,R)$, where the triple
$(h,L,R)$ is a height-left-right-wall.
Here is an example of a ZHA (with the white pawn moves on it):
%
% (find-LATEX "2015planar-has.tex" "zhas-visually")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 7)
%
%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:tozmp({def="zhav", scale="23pt", meta=nil}):addxys():addarrows("w")
%R local L = {[0]=0,-1,-2,-3,-2,-1,-2,-3,-4,-3}
%R local R = {[0]=0, 1, 0, 1, 0,-1,-2,-3,-2,-3}
%R local x = {L=8, R=10.5, a=13.5, b=16.5}
%R local x = {L=4, R=7, a=10, b=12.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), "=", "h=9")
%R mp:put(v(x.a, 9), "=", "L(9)=R(9)")
%R mp:put(v(x.a, 0), "=", "\\;\\;\\;\\;L(0)=R(0)=0")
%R mp:output()
%
$$\pu
\zhav
$$
We will see later (in section \ref{prop-calc-ZHA}) that ZHAs (with
white pawn moves) are Heyting Algebras.
% _____ _ _
% |_ _|_ _____ ___ ___ _ ____ _____ _ __ | |_(_) ___ _ __ ___
% | | \ \ /\ / / _ \ / __/ _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | | \ V V / (_) | | (_| (_) | | | \ V / __/ | | | |_| | (_) | | | \__ \
% |_| \_/\_/ \___/ \___\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «two-conventions» (to ".two-conventions")
% (ph1p 9 "two-conventions")
% (ph1a "two-conventions")
\section{Conventions on diagrams without axes}
\label {two-conventions}
We can use a bullet notation to denote ZHAs, but look at what happens
when we start with a ZHA, erase the axes, and then add the axes back
using the convention from sec.\ref{positional}:
%
$$ \quad\picturedotsadef{b1}(-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad
\sa \quad\picturedotsdef {b2}(-2,0)(2,5){ 0,0 1,1 2,2 -1,1 0,2 1,3 -2,2 -1,3 0,4 -1,5 }\quad
\sa \quad\picturedotsadef{b3} (0,0)(4,5){ 2,0 3,1 4,2 1,1 2,2 3,3 0,2 1,3 2,4 1,5 }\quad
$$
%
The new, restored axes are in a different position --- the bottom
point of the original ZHA at the left was $(0,0)$, but in the ZSet at
the right the bottom point is $(2,0)$.
{\sl The convention from sec.\ref{positional} is not adequate for ZHAs.}
Let's modify it!
{\sl From this point on,} the convention on where to
draw the axes will be this one: {\sl when it is clear from the context
that a bullet diagram represents a ZHA,} then its (unique) bottom
point has coordinate $(0,0)$, and we use that to draw the axes;
otherwise we apply the old convention, that chooses $(0,0)$ as the
point that makes the diagram fit in $\N^2$ and touch both axes.
The new convention with two cases also applies to functions from ZHAs,
and to partial functions and subsets. For example:
%
%L local mpB = mpnew({zdef="bottledots", scale="6pt", meta="s"}, "12321L")
%L local mpx = mpnew({zdef="bottlex", scale="6pt", meta="s"}, "12321L")
%L local mpl = mpnew({zdef="bottlel", scale="6pt", meta="s"}, "12321L")
%L local mpr = mpnew({zdef="bottler", scale="6pt", meta="s"}, "12321L")
%L f = function (n) return "\\text{"..n.."}" end
%L mpB:addbullets():output()
%L mpx:zhalrf0("P -> f(P[1])"):output()
%L mpl:zhalrf0("P -> P:xytolr()[1]"):output()
%L mpr:zhalrf0("P -> P:xytolr()[2]"):output()
%L
%L -- local mpB = mpnew({def="fooB", scale="5pt", meta="s"}, "12321L")
%L local mp = mpnew({zdef="bottlelr", scale="7pt", meta="s"}, "12321L")
%L mpB:addbullets():output()
%L mp :addlrs() :output()
\pu
$$
\begin{array}{lll}
B = \zha{bottledots} \quad \text{(a ZHA)}
& \phantom{m} &
λ(x,y){:}B.x = \zha{bottlex} \\ \\
λ\ang{l,r}{:}B.l = \zha{bottlel} & &
λ\ang{l,r}{:}B.r = \zha{bottler} \\
\end{array}
$$
\bsk
We will often denote ZHAs by the identity function on them:
%
$$
\pu
λ\ang{l,r}{:}B.\ang{l,r}
\;=\; λlr{:}B.lr
\;=\; \zha{bottlelr}
\qquad
\quad
B \;=\; \zha{bottlelr}
$$
%
Note that we are using the compact notation from the end of section
\ref{LR-coords}: `$lr$' instead of `$\ang{l,r}$'.
% to denote ZHAs and
% functions from ZHAs compactly, but we have to modify the convention
% for adding the axes back.
%
% %R local zhav =
% %R 1/ o \
% %R | o |
% %R | o o |
% %R |o o o|
% %R | o o |
% %R \ o /
% %R zhav:tomp ({def="zb", scale="15pt", meta=nil}):addxys():output()
% %R zhav:tozmp({def="za", scale="15pt", meta=nil}):addxys():output()
% %
% $$\pu
% \za \qquad \sa \qquad \zb
% $$
% ____ _
% | _ \ _ __ ___ _ __ ___ __ _| | ___
% | |_) | '__/ _ \| '_ \ / __/ _` | |/ __|
% | __/| | | (_) | |_) | | (_| (_| | | (__
% |_| |_| \___/| .__/ \___\__,_|_|\___|
% |_|
%
% «prop-calc» (to ".prop-calc")
% (ph1p 10 "prop-calc")
% (ph1a "prop-calc")
\section{Propositional calculus}
\label {prop-calc}
A {\sl PC-structure} is a tuple
%
$$L = (Ω,≤,⊤,⊥,∧,∨,→,↔,¬),$$
%
where:
$Ω$ is the ``set of truth values'',
$≤$ is a relation on $Ω$,
$⊤$ and $⊥$ are two elements of $Ω$,
$∧$, $∨$, $→$, $↔$ are functions from $Ω×Ω$ to $Ω$,
$¬$ is a function from $Ω$ to $Ω$.
\msk
Classical Logic ``is'' a PC-structure, with $Ω=\{0,1\}$, $⊤=1$, $⊥=0$,
$≤=\{(0,0),(0,1), \linebreak[0] (1,0)\}$, $∧=\csm{((0,0),0),
((0,1),0), \\ ((1,0),0), ((1,1),1)}$, etc.
PC-structures let us interpret expressions from Propositional Calculus
(``PC-expressions''), and let us define a notion of {\sl tautology}.
For example, in Classical Logic,
%
\begin{itemize}
\item $¬¬P↔P$ is a tautology because it is valid (i.e., it yields $⊤$)
for all values of $P$ in $Ω$,
\item $¬(P∧Q)→(¬P∨¬Q)$ is a tautology because it is valid for all
values of $P$ and $Q$ in $Ω$,
\item but $P∨Q→P∧Q$ is {\sl not} a tautology, because when $P=0$ and
$Q=1$ the result is not $⊤$:
%
$$\und{\und{\und{P}0 ∨ \und{Q}1}{1} → \und{\und{P}0 ∧\und{Q}1}{0}}{0}$$
\end{itemize}
% ____ _ ______ _ _
% | _ \ _ __ ___ _ __ ___ __ _| | ___ |__ / | | | / \
% | |_) | '__/ _ \| '_ \ / __/ _` | |/ __| / /| |_| | / _ \
% | __/| | | (_) | |_) | | (_| (_| | | (__ / /_| _ |/ ___ \
% |_| |_| \___/| .__/ \___\__,_|_|\___| /____|_| |_/_/ \_\
% |_|
%
% «prop-calc-ZHA» (to ".prop-calc-ZHA")
% (ph1p 11 "prop-calc-ZHA")
% (ph1a "prop-calc-ZHA")
\section{Propositional calculus in a ZHA}
\label {prop-calc-ZHA}
Let $Ω$ be the set of points of a ZHA and $≤$ the default partial
order on it. The {\sl default meanings for $⊤,⊥,∧,∨,→,↔,¬$} are these
ones:
%
$$\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\def\a#1#2{\ang{#1,#2}}
\def\ab{\a ab}
\def\cd{\a cd}
\begin{array}{rcl}
%
\ab ≤ \cd &:=& a≤c∧b≤d \\
\ab ≥ \cd &:=& a≥c∧b≥d \\[5pt]
%
\ab \o{above} \cd &:=& a≥c∧b≥d \\
\ab \o{below} \cd &:=& a≤c∧b≤d \\
\ab \o{leftof} \cd &:=& a≥c∧b≤d \\
\ab \o{rightof} \cd &:=& a≤c∧b≥d \\[5pt]
%
\o{valid}(\ab) &:=& \ab∈Ω \\
\o{ne}(\ab) &:=& \o{if} \o{valid}(\a a{b+1})
\o{then} \o{ne}(\a a{b+1})
\o{else} \ab \;
\o{end} \\
\o{nw}(\ab) &:=& \o{if} \o{valid}(\a {a+1}b)
\o{then} \o{nw}(\a {a+1}b)
\o{else} \ab \;
\o{end} \\[5pt]
%
\ab ∧ \cd &:=& \a{\o{min}(a,c)}{\o{min}(b,d)} \\
\ab ∨ \cd &:=& \a{\o{max}(a,c)}{\o{max}(b,d)} \\[5pt]
%
\ab \to \cd &:=& \begin{array}[t]{llll}
\o{if} & \ab \o{below} \cd & \o{then} & ⊤ \\
\o{elseif} & \ab \o{leftof} \cd & \o{then} & \o{ne}(\cd) \\
\o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\cd) \\
\o{elseif} & \ab \o{above} \cd & \o{then} & \cd \\
\o{end}
\end{array} \\[5pt]
%
⊤ &:=& \o{sup}(Ω) \\
⊥ &:=& \a00 \\
¬\ab &:=& \ab→⊥ \\
\ab↔\cd &:=& (\ab→\cd)∧ (\cd→\ab)\\
\end{array}
$$
%
% We will sometimes call them $⊤_D,⊥_D,∧_D,∨_D,→_D,↔_D,¬_D$ to
% distinguish them from other ones.
% --- let's say ``with the default logic'', for shortness ---
Let $Ω$ be the ZHA at the top left in the figure below. Then, with the
default meanings for the connectives neither $¬¬P→P$ nor
$¬(P∧Q)→(¬P∨¬Q)$ are tautologies, as there are valuations that make
them yield results different than $⊤=32$:
%
%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="12pt", 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="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse", scale="12pt", meta=nil}):addlrs():output()
%
%UB (¬ ¬ P) → P
%UB -- --
%UB 10 10
%UB ---
%UB 02
%UB -----
%UB 20
%UB -----------
%UB 12
%L
%L defub "notnotP"
%
%UB ¬(P ∧ Q) → (¬ P ∨ ¬ Q)
%UB -- -- -- --
%UB 10 01 10 01
%UB ----- --- ---
%UB 00 02 20
%UB ------- ---------
%UB 32 22
%UB ----------------------
%UB 22
%L
%L defub "demorgan"
%
$$\pu
\begin{array}{ccccl}
\ohouse && \znotnotP && \mat{\ub{notnotP}} \\ \\
&& \zdemorgan && \mat{\ub{demorgan}} \\
\end{array}
$$
So: {\sl some} classical tautologies are not tautologies in this ZHA.
The somewhat arbitrary-looking definition of `$→$' will be explained
at the end of the next section.
% _ _ _
% | | | | / \ ___
% | |_| | / _ \ / __|
% | _ |/ ___ \\__ \
% |_| |_/_/ \_\___/
%
% «HAs» (to ".HAs")
% (ph1p 12 "HAs")
% (ph1a "HAs")
\section{Heyting Algebras}
\label{HAs}
A {\sl Heyting Algebra} is a PC-structure
%
$$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H,↔_H,¬_H),$$
%
in which:
1) $(Ω,≤_H)$ is a partial order
2) $⊤_H$ is the top element of the partial order
3) $⊥_H$ is the bottom element of the partial order
4) $P ↔_H Q$ is the same as $(P →_H Q)∧_H(Q →_H P)$
5) $¬_H P$ is the same as $P →_H ⊥_H$
6) $∀P,Q,R∈Ω.\;\; (P ≤_H (Q ∧_H R)) ↔ ((P ≤_H Q) ∧ (P ≤_H R))$
7) $∀P,Q,R∈Ω.\;\; ((P ∨_H Q) ≤_H R) ↔ ((P ≤_H R) ∧ (Q ≤_H R))$
8) $∀P,Q,R∈Ω.\;\; (P ≤_H (Q →_H R)) ↔ ((P ∧_H Q) ≤_H R)$
6') $∀Q,R∈Ω.\, ∃!Y∈Ω.\, ∀P∈Ω.\;\; (P ≤_H Y) ↔ ((P ≤_H Q) ∧ (P ≤_H R))$
7') $∀P,Q∈Ω.\, ∃!X∈Ω.\, ∀R∈Ω.\;\; (X ≤_H R) ↔ ((P ≤_H R) ∧ (Q ≤_H R))$
8') $∀Q,R∈Ω.\, ∃!Y∈Ω.\, ∀P∈Ω.\;\; (P ≤_H Y) ↔ ((P ∧_H R) ≤_H R)$
\msk
The conditions 6', 7', 8' say that there are unique elements in $Ω$
that ``behave as'' $Q ∧_H R$, $P ∨_H Q$ and $Q →_H R$ for given $P$,
$Q$, $R$; the conditions 6,7,8 say that $Q ∧_H R$, $P ∨_H Q$ and $Q
→_H R$ are exactly the elements with this behavior.
\msk
% There is a very visual way to calculate these $Q ∧_H R$, $P ∨_H Q$
% and $Q →_H R$ on a ZHA.
The positional notation on ZHAs is very helpful for visualizing what
the conditions 6',7',8',6,7,8 ``mean''. More precisely: once we fix a
ZHA $Ω$ and truth-values $P,Q,R∈Ω$ we have a way to draw and to
visualize the ``behavior'' of each subexpression of the conditions 6,
7, 8 using the positional notations of sec.\ref{positional}, and we
can use that to obtain the only possible values for $Q ∧_H R$, $P ∨_H
Q$ and $Q →_H R$.
We will examine three particular cases: with $Ω$ being the ZDAG on the
left below,
%
%R local QoRai, PoQai, PnnP =
%R 1/ T \, 1/ T \, 1/ T \
%R | . . | | . . | | . |
%R | . . . | | . . . | | . . |
%R | . . . i | | . o . . | |d . n|
%R |. Q . . .| |. P . . .| | P . |
%R | . . R . | | . . Q . | \ F /
%R | . a . | | . . . |
%R | . . | | . . |
%R \ F / \ F /
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R T="·", F="·", T="⊤", F="⊥", }
%R PoQai:tozmp({def="PoQai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
$$
\pu
\lozfive \qquad \QoRai \qquad \PoQai
$$
a) if $Q=31$ and $R=12$ then $Q ∧_H R = 11$,
b) if $P=31$ and $Q=12$ then $P ∨_H Q = 32$,
c) if $Q=31$ and $R=12$ then $Q →_H R = 14$.
\msk
% Let's see each case separately --- but,
Before we start, note that in 6, 7, 8, 6', 7', 8' some subexpressions
yield truth values in $Ω$ and other subexpressions yield standard
truth values. For example, in 6, with $P=20$, we have:
%
%UB ( P ≤_H ( Q ∧_H R )) ↔ (( P ≤_H Q ) ∧ ( P ≤_H R ))
%UB -- -- -- -- -- -- --
%UB 20 31 12 20 31 20 12
%UB --------- --------- ---------
%UB 11 1 0
%UB -------------------- ----------------------------
%UB 0 0
%UB ---------------------------------------------------------
%UB 1
%L
%L defub "P<=(QaR) <-> (P<=Q a P<=R)"
$$\pu \ub{P<=(QaR) <-> (P<=Q a P<=R)}$$
\bsk
% «calculating-and» (to ".calculating-and")
% (ph1p 13 "calculating-and")
% (ph1a "calculating-and")
%
Case (a). Let $Q=31$ and $R=12$. We want to see that $Q ∧_H R = 11$,
i.e., that
%
$$∀P∈Ω.\;\; (P ≤_H Y) ↔ ((P ≤_H Q) ∧ (P ≤_H R))$$
%
holds for $Y=11$ and for no other $Y∈Ω$. We can visualize the behavior
of $P ≤_H Q$ for all `$P$'s by drawing $λP{:}Ω.(P ≤_H Q)$ in the
positional notation; then we do the same for $λP{:}Ω.(P ≤_H R)$ and
for $λP{:}Ω.((P ≤_H Q) ∧ (P ≤_H R))$. Suppose that the full
expression, `$∀P{:}Ω.\,\_\_\_$', is true; then the behavior of the
left side of the `$↔$', $λP{:}Ω.(P ≤_H Y)$, has to be a copy of the
behavior of the right side, and that lets us find the only adequate
value for $Y$.
The order in which we calculate and draw things is below, followed by
the results themselves:
%
%UB ( P ≤_H Y) ↔ (( P ≤_H Q) ∧ ( P ≤_H R))
%UB --- --- ---
%UB (7) (1) (2)
%UB ---------- ---------- ----------
%UB (6) (3) (4)
%UB ---------------------------
%UB (5)
%L
%L defub "P<=Y <-> (P<=Q a P<=R)"
%
%L local spec = "123454321"
%L local mpuQ = mpnew({zdef="uQ", scale="5pt", meta="s"}, spec)
%L local mpuR = mpnew({zdef="uR", scale="5pt", meta="s"}, spec)
%L local mpuQaR = mpnew({zdef="uQaR", scale="5pt", meta="s"}, spec)
%L mpuQ :zhalrf0("P -> P:below(v'31') and 1 or 0"):output()
%L mpuR :zhalrf0("P -> P:below(v'12') and 1 or 0"):output()
%L mpuQaR:zhalrf0("P -> P:below(v'11') and 1 or 0"):output()
%L
%UB ( P ≤_H Y) ↔ (( P ≤_H Q) ∧ ( P ≤_H R))
%UB -- -- --
%UB 11 31 12
%UB ---------- ---------- ----------
%UB \zha{uQaR} \zha{uQ} \zha{uR}
%UB ---------------------------
%UB \zha{uQaR}
%L
%L defub "P<=Y <-> (P<=Q a P<=R) : zhas"
%L
$$\pu
\begin{array}{cc}
\ub{P<=Y <-> (P<=Q a P<=R)} \\ \\
\ub{P<=Y <-> (P<=Q a P<=R) : zhas}
\end{array}
$$
\msk
% «calculating-or» (to ".calculating-or")
% (ph1p 14 "calculating-or")
% (ph1a "calculating-or")
%
Case (b). Let $P=31$ and $Q=12$. We want to see that $P ∨_H Q = 32$,
i.e., that
%
$$∀R{:}Ω.\;\; (X ≤_H R) ↔ ((P ≤_H R) ∧ (Q ≤_H R))$$
%
holds for $X=32$ and for no other $X∈Ω$. We do essentially the same as
we did in (a), but now we calculate $λR{:}Ω.(P ≤_H R)$, $λR{:}Ω.(Q ≤_H
R)$, and $λR{:}Ω.((P ≤_H R) ∧ (Q ≤_H R))$. The order in which we
calculate and draw things is below, followed by the results
themselves:
%
%UB ( X ≤_H R) ↔ (( P ≤_H R) ∧ ( Q ≤_H R))
%UB --- --- ---
%UB (7) (1) (2)
%UB ---------- ---------- ----------
%UB (6) (3) (4)
%UB ---------------------------
%UB (5)
%L
%L defub "X<=R <-> (P<=R a Q<=R)"
$$\pu \ub{X<=R <-> (P<=R a Q<=R)}$$
%
%L local spec = "123454321"
%L local mpoP = mpnew({zdef="oP", scale="5pt", meta="s"}, spec)
%L local mpoQ = mpnew({zdef="oQ", scale="5pt", meta="s"}, spec)
%L local mpoPvQ = mpnew({zdef="oPvQ", scale="5pt", meta="s"}, spec)
%L mpoP :zhalrf0("P -> P:above(v'31') and 1 or 0"):output()
%L mpoQ :zhalrf0("P -> P:above(v'12') and 1 or 0"):output()
%L mpoPvQ:zhalrf0("P -> P:above(v'32') and 1 or 0"):output()
%L
%UB ( X ≤_H R) ↔ (( P ≤_H R) ∧ ( Q ≤_H R))
%UB -- -- --
%UB 32 31 12
%UB ---------- ---------- ----------
%UB \zha{oPvQ} \zha{oP} \zha{oQ}
%UB ---------------------------
%UB \zha{oPvQ}
%L
%L defub "X<=R <-> (P<=R a Q<=R) : zhas"
$$\pu \ub{X<=R <-> (P<=R a Q<=R) : zhas}$$
\msk
% «calculating-imp» (to ".calculating-imp")
% (ph1p 14 "calculating-imp")
% (ph1a "calculating-imp")
%
Case (c). Let $Q=31$ and $R=12$. We want to see that $Q →_H R = 14$,
i.e., that
%
$$∀P{:}Ω.\;\; (P ≤_H Y) ↔ ((P ∧_H Q) ≤_H R)$$
%
holds for $Y=14$ and for no other $Y∈Ω$. Here we have to do something
slightly different. We start by visualizing $λP{:}Ω.(P ∧_H Q)$, which
is a function from $Ω$ to $Ω$, not a function from $Ω$ to $\{0,1\}$
like the ones we were using before. The order in which we calculate
and draw things is below, followed by the results:
%
%UB ( P ≤_H Y) ↔ (( P ∧_H Q) ≤_H R))
%UB --- --- ---
%UB (6) (1) (2)
%UB ---------- ----------
%UB (5) (3)
%UB -------------------
%UB (4)
%L
%L defub "P<=Y <-> (PaQ <= R)"
$$\pu \ub{P<=Y <-> (PaQ <= R)}$$
%
%L local spec = "123454321"
%L local mpaQ = mpnew({zdef="aQ", scale="6pt", meta="s"}, spec)
%L local mpaQuR = mpnew({zdef="aQuR", scale="5pt", meta="s"}, spec)
%L mpaQ :zhalrf ("P -> P:And (v'31') "):output()
%L -- mpaQuR:zhalrf0("P -> P:below(v'12') and 1 or 0"):output() -- TYPO, fixed in 2019sep10
%L mpaQuR:zhalrf0("P -> P:below(v'14') and 1 or 0"):output()
%L
%UB ( P ≤_H Y) ↔ (( P ∧_H Q) ≤_H R))
%UB --- --- ---
%UB 14 31 12
%UB ---------- ----------
%UB \zha{aQuR} \zha{aQ}
%UB -------------------
%UB \zha{aQuR}
%L
%L defub "P<=Y <-> (PaQ <= R) : zhas"
$$\pu \ub{P<=Y <-> (PaQ <= R) : zhas}$$
% __
% \ \ _ __ _____ __
% _____\ \ | '_ \ / _ \ \ /\ / /
% |_____/ / | | | | __/\ V V /
% /_( ) |_| |_|\___| \_/\_/
% |/
%
% «implication-new» (to ".implication-new")
% (ph1p 15 "implication-new")
% (ph1a "implication-new")
\section{The two implications are equivalent}
\label{implication-new}
{
\def\toC {\ton{\text{C}}}
\def\toHA{\ton{\text{HA}}}
\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\def\a#1#2{\ang{#1,#2}}
\def\ab{\a ab}
\def\cd{\a cd}
\def\ef{\a ef}
\def\ab{ab}
\def\cd{cd}
\def\ef{ef}
\def\wh{\widehat}
In sec.\ref{prop-calc-ZHA} we gave a definition of `$→$' that is easy
to calculate, and in sec.\ref{HAs} we saw a way to find by brute
force\footnote{``When in doubt use brute force'' --- Ken Thompson} a
value for $Q→R$ that obeys
%
%$$(P≤(Q→R))↔(P≤Q∧R)$$ % TYPO, fixed in 2019sep10
$$ (P≤(Q→R))↔(P∧Q≤R)$$
%
for all $P$. In this section we will see a proof that these two
operations --- called `$\toC$' and `$\toHA$' from here on --- always
give the same results.
\begin{theorem}
We have $(Q \toC R) = (Q \toHA R)$, for any ZHA $H$ and $Q,R∈H$.
\end{theorem}
The proof will take the rest of this section, and our approach will be
to check that for any ZHA $H$ and $Q,R∈H$ this holds, for all $P∈H$:
%
%$$(P≤(Q \toC R))↔(P≤Q∧R).$$ % TYPO, fixed in 2019sep10
$$ (P≤(Q \toC R))↔(P∧Q≤R).$$
\msk
In `$\toC$' the order of the cases is very important. For example, if
$cd=21$ and $ef=23$ then both ``$\cd \o{below} \ef$'' and ``$\cd
\o{leftof} \ef$'' are true, but ``$\cd \o{below} \ef$'' takes
precedence and so $\cd \toC \ef = ⊤$. We can fix this by creating
variants of $\o{below}$, $\o{leftof}$, $\o{righof}$ and $\o{above}$,
called $\o{below}'$, $\o{leftof}'$, $\o{righof}'$ and $\o{above}'$,
that make the four cases disjoint. Abbreviating $\o{below}$,
$\o{leftof}$, $\o{righof}$ and $\o{above}$ as $\o{b}$, $\o{l}$,
$\o{r}$ and $\o{a}$, we have:
%
$$\def\foo#1#2#3{\cd\,\o{#1}\,\ef\;:=\; c#2e ∧ d#3f}
\begin{array}{rrr}
\foo{b}{≤}{≤} && \foo{b'}{≤}{≤} \\
\foo{l}{≤}{≥} && \foo{l'}{≤}{>} \\
\foo{r}{≥}{≤} && \foo{r'}{>}{≤} \\
\foo{a}{>}{>} && \foo{a'}{>}{>} \\
\end{array}
$$
%
visually the regions are these, for $R$ fixed:
%
%L mp = mpnew({def="blraprime", scale="8pt", meta="s"}, "12345654321"):addcuts("c 543/210 012|345")
%L mp:put(v"22", "R")
%L mp:put(v"44", "Q\\o{a}'R")
%L mp:put(v"11", "Q\\o{b}'R")
%L mp:put(v"41", "Q\\o{l}'R")
%L mp:put(v"14", "Q\\o{r}'R")
%L mp:output()
%
$$\pu
\blraprime
$$
%
Note that $R$ belongs to the lower region --- i.e., $R \o{b}'R$.
\msk
Now we clearly have:
%
$$Q \toC R
%
\;=\;
%
\left(
\!
\begin{array}{lccl}
\o{if} & Q\o{b}R & \o{then} & ⊤ \\
\o{elseif} & Q\o{l}R & \o{then} & \o{ne}(R) \\
\o{elseif} & Q\o{r}R & \o{then} & \o{nw}(R) \\
\o{elseif} & Q\o{a}R & \o{then} & R \\
\o{end}
\end{array}
\!\!\!
\right)
%
\;=\;
%
\left(
\!
\begin{array}{lccl}
\o{if} & Q\o{b'}R & \o{then} & ⊤ \\
\o{elseif} & Q\o{l'}R & \o{then} & \o{ne}(R) \\
\o{elseif} & Q\o{r'}R & \o{then} & \o{nw}(R) \\
\o{elseif} & Q\o{a'}R & \o{then} & R \\
\o{end}
\end{array}
\!\!\!
\right)
$$
%
and $P ≤ (Q \toC R)$ can be expressed as a conjunction of the four
cases:
%
$$\def\foo#1{((P ≤ #1) ↔ (P∧Q≤R))}
\def\fooc {((P ≤ Q \toC R) ↔ (P∧Q≤R))}
\def\cond#1{Q\o{#1}R}
%
\begin{array}{l}
\fooc \\[5pt]
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \fooc & ∧ \\
\cond{l'} → \fooc & ∧ \\
\cond{r'} → \fooc & ∧ \\
\cond{a'} → \fooc & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \foo{⊤} & ∧ \\
\cond{l'} → \foo{\o{ne}(R)} & ∧ \\
\cond{r'} → \foo{\o{nw}(R)} & ∧ \\
\cond{a'} → \foo{R} & \\
\end{array}
\right) \\
\end{array}
$$
Let's introduce a notation: a ``$\widehat{a}$'' means ``make this
digit as big possible without leaving the ZHA''. So,
%
%L mpnew({zdef="fat-zha-for-ne-nw", scale="11pt"}, "123RL232L1"):addlrs():output()
$$\pu
\text{in} \qquad \zha{fat-zha-for-ne-nw} \qquad \text{we have} \qquad
\begin{array}{rclcl}
\wh1\wh2 &=& 54 &=& ⊤, \\
1\wh2 &=& 13 &=& \o{ne}(12), \\
\wh12 &=& 42 &=& \o{nw}(12); \\
\end{array}
% \quad ;
$$
\def\EF{\wh e \wh f}
\def\Ef{\wh e f}
\def\eF{ e \wh f}
\def\ef{ e f}
This lets us rewrite $⊤$ as $\wh e \wh f$, $\o{ne}(ef)$ as $e \wh f$,
and $\o{nw}(ef)$ as $\wh e f$.
Making $P=ab$, $Q=cd$, $R=ef$, we have:
$$\def\fooc {((ab ≤ cd \toC ef) ↔ (ab∧cd≤ef))}
\def\foo #1 {((ab ≤ #1) ↔ (ab∧cd≤ef))}
\def\foor#1#2{((ab ≤ #1) ↔ (ab∧cd≤#2))}
\def\fooR#1#2{((ab ≤ #1) ↔ #2)}
\def\cond#1 {cd\o{#1}ef}
\def\Cond#1#2{c#1e ∧ d#2f}
%
\begin{array}{l}
\fooc \\[5pt]
\quad ↔ \quad
\left(
\begin{array}{ll}
\cond{b'} → \foo{\EF} & ∧ \\
\cond{l'} → \foo{\eF} & ∧ \\
\cond{r'} → \foo{\Ef} & ∧ \\
\cond{a'} → \foo{\ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond{≤}{≤} → \foo{\EF} & ∧ \\
\Cond{>}{≤} → \foo{\eF} & ∧ \\
\Cond{≤}{>} → \foo{\Ef} & ∧ \\
\Cond{>}{>} → \foo{\ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond{≤}{≤} → \foor{\EF}{cd} & ∧ \\
\Cond{>}{≤} → \foor{\eF}{ed} & ∧ \\
\Cond{≤}{>} → \foor{\Ef}{cf} & ∧ \\
\Cond{>}{>} → \foor{\ef}{ef} & \\
\end{array}
\right) \\ \\
\quad ↔ \quad
\left(
\begin{array}{ll}
\Cond{≤}{≤} → \fooR{\EF}{⊤} & ∧ \\
\Cond{>}{≤} → \fooR{\eF}{a≤e} & ∧ \\
\Cond{≤}{>} → \fooR{\Ef}{b≤f} & ∧ \\
\Cond{>}{>} → \fooR{\ef}{(a≤e∧b≤f)} & \\
\end{array}
\right) \\
\end{array}
$$
In the last conjunction the four cases are trivial to check.
}
% _ _ _ _ _ _
% | | ___ __ _(_) ___ (_)_ __ | | | | / \ ___
% | | / _ \ / _` | |/ __| | | '_ \ | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__ | | | | | | _ |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/ \_\___/
% |___/
%
% «logic-in-HAs» (to ".logic-in-HAs")
% (ph1p 18 "logic-in-HAs")
% (ph1a "logic-in-HAs")
\section{Logic in a Heyting Algebra}
\label {logic-in-HAs}
In sec.\ref{HAs} we saw a set of conditions --- called 1 to 8' ---
that characterize the ``Heyting-Algebra-ness'' of a PC-structure. It
is easy to see that Heyting-Algebra-ness, or ``HA-ness'', is
equivalent to this set of conditions:
%
$$
\fbox{$
\begin{array}{ll%
rrcccc%
cc}
1) && ∀P. & (P≤P) & & & & && (\id) \\
&& ∀P,Q,R. & (P≤R) &←& (P≤Q) &∧& (Q≤R) && (\comp) \\[5pt]
2) && ∀P. & (P≤⊤) & & & & && (⊤_1) \\
3) && ∀Q. & (⊥≤Q) & & & & && (⊥_1) \\[10pt]
6) && ∀P,Q,R. & (P≤Q∧R) &→& (P≤Q) & & && (∧_1) \\
&& ∀P,Q,R. & (P≤Q∧R) &→& & & (P≤R) && (∧_2) \\
&& ∀P,Q,R. & (P≤Q∧R) &←& (P≤Q) &∧& (P≤R) && (∧_3) \\[5pt]
7) && ∀P,Q,R. & (P∨Q≤R) &→& (P≤R) & & && (∨_1) \\
&& ∀P,Q,R. & (P∨Q≤R) &→& & & (Q≤R) && (∨_2) \\
&& ∀P,Q,R. & (P∨Q≤R) &←& (P≤R) &∧& (Q≤R) && (∨_3) \\[5pt]
8) && ∀P,Q,R. & (P≤Q{→}R) &→& \multicolumn{3}{l}{(P∧Q≤R)} && (→_1) \\
&& ∀P,Q,R. & (P≤Q{→}R) &←& \multicolumn{3}{l}{(P∧Q≤R)} && (→_2) \\
\end{array}
$}
$$
%
We omitted the conditions 4 and 5, that defined `$↔$' and `$¬$' in
terms of the other operators. The last column of the table gives a
name to each of these new conditions.
These new conditions let us put (some) proofs about HAs in tree form,
as we shall see soon.
% {\sl Note: this section, and its two subsections, are just very quick
% introductions to the most basic ideas of Sequent Calculus and
% Natural Deduction ...}
\def\t{\text}
\msk
Let us introduce two new notations. The first one,
$$(\t{expr})\subst{v_1 := \t{repl}_1 \\ v_2 := \t{repl}_2}$$ indicates
simultaneous substitution of all (free) occurrences of the variables
$v_1$ and $v_2$ in expr by the replacements $\t{repl}_1$ and
$\t{repl}_2$. For example,
%
$$((x+y)·z) \subst{
x:=a+y \\
y:=b+z \\
z:=c+x \\
}
\;\;=\;\;
((a+y)+(b+z))·(c+x).
$$
The second is a way to write `$→$'s as horizontal bars. In
%:
%: L M
%: -\ee -----\zeta
%: A B C E F H K N O
%: -------\aa ----\bb -\gg -\dd --------------------\eta
%: D G I J P
%:
%: ^t1 ^t2 ^t3 ^t4 ^t5
%:
$$\pu
\ded{t1} \qquad \ded{t2} \qquad \ded{t3} \qquad \ded{t4} \qquad \ded{t5}
$$
%
the trees mean:
%
\begin{itemize}
\item if $A$, $B$, $C$ are true then $D$ is true (by $\aa$),
\item if $E$, $F$, are true then $G$ is true (by $\bb$),
\item if $H$ is true then $I$ is true (by $\gg$),
\item $J$ is true (by $\dd$, with no hypotheses),
\item $K$ is true (by $\ee$); if $L$ and $M$ then $N$ (by $\zeta$);
if $K$, $N$, $O$, then $P$ (by $\eta$); combining all this we get a
way to prove that if $L$, $M$, $O$, then $P$,
\end{itemize}
%
where $\aa, \bb, \gg, \dd, \ee, \zeta, \eta$ are usually names
of rules.
\msk
The implications in the table in the beginning of this section can be
rewritten as ``tree rules'' as:
%:
%: P≤Q Q≤R
%: ----\id ---------\comp -----⊤_1 -----⊥_1
%: P≤P P≤R P≤⊤ ⊥≤Q
%:
%: ^id ^comp ^T1 ^B1
%:
%: P≤Q∧R P≤Q∧R P≤Q P≤R
%: ------∧_1 ------∧_2 -----------∧_3
%: P≤Q P≤R P≤Q∧R
%:
%: ^and1 ^and2 ^and3
%:
%: P∨Q≤R P∨Q≤R P≤R Q≤R
%: ------∨_1 ------∨_2 -----------∨_3
%: P≤R Q≤R P∨Q≤R
%:
%: ^or1 ^or2 ^or3
%:
%:
%: P≤Q{→}R P∧Q≤R
%: ---------→_1 ---------→_2
%: P∧Q≤R P≤Q{→}R
%:
%: ^imp1 ^imp2
%:
{
\pu
$$\ded{id} \qquad \ded{comp} \qquad \ded{T1} \qquad \ded{B1}$$
$$\ded{and1} \qquad \ded{and2} \qquad \ded{and3}$$
$$\ded{or1} \qquad \ded{or2} \qquad \ded{or3}$$
$$\ded{imp1} \qquad \ded{imp2}$$
}
\msk
Note that the `$∀P,Q,R∈Ω$'s are left implicit in the tree rules, which
means that {\sl every substitution instance of the tree rules hold};
sometimes --- but rarely --- we will indicate the substitution
explicitly, like this,
%:
%: P≤Q{→}R P∧Q≤R
%: ---------→_1 ---------→_2
%: P∧Q≤R P≤Q{→}R
%:
%: ^imp1 ^imp2
%:
%: P∧(P{→}⊥)≤⊥
%: ------------------→_2\su
%: P≤((P{→}⊥){→}⊥)
%:
%: ^imp2-su
%:
$$\pu
\def\su{\bsm{Q:=P{→}⊥ \\ R:=⊥}}
%
\begin{array}{rcl}
\left(\cded{imp2}\right) \su &\squigto& {\def\su{} \cded{imp2-su}} \\\\
(→_2)\su &\squigto& \cded{imp2-su} \\
\end{array}
$$
%
Usually we will only say `$→_2$' instead of `$→_2\bsm{Q:=P{→}⊥
\\ R:=⊥}$' at the right of a bar, and the task of discovering which
substitution has been used is left to the reader.
\msk
The tree rules can be composed in a nice visual way. For example,
this tree --- let's call it $({∧}{∧})$,
%:
%: ---------\id ---------\id
%: P∧Q≤P∧Q P∧Q≤P∧Q
%: ---------∧_1 ---------∧_2
%: P∧Q≤P P≤R P∧Q≤Q Q≤S
%: ------------------\comp ------------------\comp
%: P∧Q≤R P∧Q≤S
%: ------------------------------------∧_3
%: P∧Q≤R∧S
%:
%: ^(andand)
%:
$$\pu
\ded{(andand)}
$$
%
``is'' a proof for:
%
%$$∀P,Q,R,S∈Ω.\; (P ≤_H R)∧(Q ≤_H S) → ((P ∧_H Q) ≤_H (R ∧_H S)).$$
%
$$∀P,Q,R,S∈Ω.\; (P ≤ R)∧(Q ≤ S) → ((P ∧ Q) ≤ (R ∧ S)).$$
We can perform substitutions on trees, and the notation will be the
same as for tree rules: for example, $({∧}{∧}) \subst{S:=P∧Q}$.
% ____ _ _ _
% | _ \ ___ _ __(_)_ _____ __| | _ __ _ _| | ___ ___
% | | | |/ _ \ '__| \ \ / / _ \/ _` | | '__| | | | |/ _ \/ __|
% | |_| | __/ | | |\ V / __/ (_| | | | | |_| | | __/\__ \
% |____/ \___|_| |_| \_/ \___|\__,_| |_| \__,_|_|\___||___/
%
% «derived-rules» (to ".derived-rules")
% (ph1p 20 "derived-rules")
% (ph1a "derived-rules")
\subsection{Derived rules}
\def\Hs{\{H_1, \ldots, H_n\}}
Let be $𝐬{HAT}$ the set of ``Heyting Algebra rules in tree form'' from
the last section:
%
$$𝐬{HAT} = \{(\id), \ldots, (→_2)\}.$$
Let's see a way to treat $𝐬{HAT}$ as a deductive system.
If $𝐬S$ is a set of tree rules, we will write:
\begin{itemize}
\item $𝐬{Trees}(𝐬S)$ for the set of all trees whose bars are all
substituion instances of rules in $𝐬S$,
\item $𝐬{Trees}(𝐬S, \Hs)$ for the set of all trees in $𝐬{Trees}(𝐬S)$
whose hypotheses are contained in the set $\{H_1, \ldots, H_n\}$,
and
\item $𝐬{Trees}(𝐬S, \Hs, C)$ for the set of trees in $𝐬{Trees}(𝐬S,
\Hs)$ having $C$ as their conclusion.
\end{itemize}
When the set $𝐬S$ is clear from the context, we write
%:
%: H_1 \ldots H_n
%: ================
%: C
%:
%: ^H1...Hn-to-C
%:
$$\pu
\ded{H1...Hn-to-C}
$$
%
to mean: {\sl we know} a tree in $𝐬{Trees}(𝐬S, \Hs, C)$, and this is
an abbreviation for it. I like to think of the double bar as the
bellows of a closed accordion: when the accordion is closed we can
still see the keyboards at both sides, but not the drawings painted on
the folded part of the pleated cloth.
The notation that defines a {\sl derived rule} is ``\textsl{newrule
$:=$ expansion}'', where \textsl{expansion} is a tree in
$𝐬{Trees}(𝐬S, \Hs, C)$ and \textsl{newrule} is a bar with hypotheses
$H_1, \ldots, H_n$ and conclusion $C$, written with a single bar with
a (new) rule name, instead of with a double bar. For example, this is
a version of Modus Ponens for Heyting Algebras:
%:
%: ---------\id
%: P≤Q{→}R P≤Q Q{→}R≤Q{→}R
%: ------------∧_3 ----------→_1
%: P≤Q P≤Q{→}R P≤(Q{→}R){∧}Q (Q{→}R){∧}Q≤R
%: ------------\MP := --------------------------\comp
%: P≤R P≤R
%:
%: ^MPL ^MPR
%:
\pu
$$\ded{MPL} \quad := \quad \ded{MPR}$$
After the definition of a derived rule --- say, ``$D_1 := E_1$'' ---
the set of allowed tree rules that is implicit from the context is
increased, with $D_1$ being added to it; when we define another
derived rule, $D_2 := E_2$, its expansion $E_2$ can have bars that are
substitution instances of $D_1$. After adding more derived rules, $D_3
:= E_3$, $\ldots$, $D_n := E_n$, we can use all the new rules $D_1,
\ldots, D_n$ in our trees --- and we have a way to remove all the
derived rules from our trees! Take a tree $T∈𝐬{Trees}(𝐬S∪\{D_1,
\ldots, D_n\})$; replace each substitution instance of $D_n$ in it by
its expansion, then replace every substitution instance of $D_{n-1}$
in the new tree by its expansion, and so on; after replacing all
substitution instances of $D_1$ we get a tree in $𝐬{Trees}(𝐬S)$, with
the same hypotheses and the same conclusion as the original $T$.
We want to add these other derived rules:
%:
%: -------\id
%: Q∧R≤Q∧R
%: ------∧E_1 := -------∧_1
%: Q∧R≤Q Q∧R≤Q
%:
%: ^and4a ^and4b
%:
%:
%: ---------\id
%: Q∧R≤Q∧R
%: ------∧E_2 := ---------∧_2
%: Q∧R≤R Q∧R≤R
%:
%: ^and5a ^and5b
%:
%: ---------\id
%: P∨Q≤P∨Q
%: ------∨I_1 := ---------∨_1
%: P≤P∨Q P≤P∨Q
%:
%: ^or4a ^or4b
%:
%: ---------\id
%: P∨Q≤P∨Q
%: ------∨I_2 := ---------∨_2
%: Q≤P∨Q Q≤P∨Q
%:
%: ^or5a ^or5b
%:
%:
%: P∧R≤S Q∧R≤S
%: -----→_2 -----→_2
%: P≤R→S Q≤R→S
%: ---------------∨_3
%: P∧R≤S Q∧R≤S P∨Q≤R→S
%: ------------∨E := ---------→_1
%: (P∨Q)∧R≤R (P∨Q)∧R≤R
%:
%: ^orE1 ^orE2
%:
\pu
$$\begin{array}{rcl}
\ded{and4a} &:=& \ded{and4b} \\\\
\ded{and5a} &:=& \ded{and5b} \\\\
\ded{or4a} &:=& \ded{or4b} \\\\
\ded{or5a} &:=& \ded{or5b} \\\\
\ded{orE1} &:=& \ded{orE2} \\\\
\end{array}
$$
% _ _ _ _ _ _
% | \ | | __ _| |_ _ _ _ __ __ _| | __| | ___ __| |
% | \| |/ _` | __| | | | '__/ _` | | / _` |/ _ \/ _` |
% | |\ | (_| | |_| |_| | | | (_| | | | (_| | __/ (_| |
% |_| \_|\__,_|\__|\__,_|_| \__,_|_| \__,_|\___|\__,_|
%
% «natural-deduction» (to ".natural-deduction")
% (ph1p 22 "natural-deduction")
% (ph1a "natural-deduction")
\subsection{Natural deduction}
The system $𝐬{HAT}$ with all the derived rules of the last section
added to it will be called $𝐬{HAND}$:
%
$$𝐬{HAND} = \{(\id), \ldots, (→_2), (\MP), \ldots, (∨E))\}$$
Trees in Natural Deduction for IPL can be translated into $𝐬{HAND}$ by
a method that we will sketch below. Note that this section is not
self-contained --- it should be regarded as an introduction to
\cite{NegriVonPlato}. Note that {\sl all our trees can be intepreted
as proofs about Heyting Algebras.}
% (find-books "__logic/__logic.el" "negri-vonplato")
\msk
This is an example of a tree in Natural Deduction:
%
% (ntyp 46 "ND-3")
% (nty "ND-3")
%
%: [P]^1 P{→}Q [P]^1 P{→}R
%: ------------(→E) ------------(→E)
%: Q R
%: -------------------(∧I)
%: Q{∧}R
%: -----------(→I);1
%: P{→}(Q{∧}R)
%:
%: ^ND-1
%:
\pu
$$\ded{ND-1}$$
%
The ``;1'' in its last bar means: below this point the hypotheses
marked with `$[\,·\,]^1$' are ``discharged'' from the list of
hypotheses. Each subtree of a ND tree with undischarged hypotheses
$H_1, \ldots, H_n$ and conclusion $C$ will be interpreted as {\sl
some} tree in $𝐬{HAND}$ with no hypotheses and conclusion
$H_1∧\ldots∧H_n≤C$ --- there are usually several possible choices. So:
%:
%: P P{→}Q
%: -------- ==> -----------\MP
%: Q P∧(P{→}Q)≤Q
%:
%: ^a1 ^a2
%:
%: P P{→}R
%: -------- ==> -----------\MP
%: R P∧(P{→}R)≤R
%:
%: ^b1 ^b2
%:
%: Q R
%: ----- ==> -----------\id
%: Q{∧}R Q{∧}R≤Q{∧}R
%:
%: ^c1 ^c2
%:
%: P P{→}Q P P{→}R
%: -------- --------
%: Q R
%: ---------------- ==> =========================
%: Q{∧}R ((P{→}R)∧(P{→}Q))∧P≤Q{∧}R
%:
%: ^d1 ^d2
%:
%: [P]^1 P{→}Q [P]^1 P{→}R
%: ------------ ------------
%: Q R
%: ------------------- =========================
%: Q{∧}R ((P{→}R)∧(P{→}Q))∧P≤Q{∧}R
%: -----------(→I);1 ==> -------------------------→_2
%: P{→}(Q{∧}R) (P{→}R)∧(P{→}Q)≤P{→}Q{∧}R
%:
%: ^e1 ^e2
%:
\pu
$$\def\becomes{\Longrightarrow}
\begin{array}{rcl}
\ded{a1} &\becomes& \ded{a2} \\ \\
\ded{b1} &\becomes& \ded{b2} \\ \\
\ded{c1} &\becomes& \ded{c2} \\ \\
\ded{d1} &\becomes& \ded{d2} \\ \\
\ded{e1} &\becomes& \ded{e2} \\
\end{array}
$$
The ND rules that are difficult to understand and difficult to
translate are the ones that involve discharges: `$(→I)$', that appears
above, and `$(∨E)$':
%:
%: [P]^1 R [Q]^1 R
%: ::::::::T_1 ::::::::T_2 =====T_1 =====T_2
%: P∨Q S S P∧R≤S Q∧R≤S
%: ----------------------(∨E) ---------------∨E
%: S (P∨Q)∧R≤S
%:
%: ^oE1 ^oE2
%:
\pu
$$\def\becomes{\Longrightarrow}
\begin{array}{rcl}
\ded{oE1} &\becomes& \ded{oE2} \\
\end{array}
$$
%
Note that the derived rule $∨E$ is used to combine the translations of
the subtrees $T_1$ and $T_2$ into a translation of the whole ND tree.
My suggestion for the readers that are seeing this for the first time
is: start by translating the ND tree below
%
% (find-books "__logic/__logic.el" "negri-vonplato")
% (find-books "__logic/__logic.el" "van_dalen")
% (find-xpdfpage "~/LATEX/2017distributivity.pdf")
% (find-LATEXfile "2017distributivity.tex" "fails in some way")
%:
%: (P∨Q)∧R (P∨Q)∧R
%: -------(∧E_2) -------(∧E_2)
%: [P]^1 R [Q]^1 R
%: ----------(∧I) -----------(∧I)
%: (P∨Q)∧R P∧R Q∧R
%: -------(∧E_1) ------------(∨I_1) -----------(∨I_2)
%: P∨Q (P∧R)∨(Q∧R) (P∧R)∨(Q∧R)
%: ----------------------------------------------(∨E);1
%: (P∧R)∨(Q∧R)
%:
%: ^distr-weird-1
%:
$$\pu
\ded{distr-weird-1}
$$
%
to a tree in $𝐬{HAND}$, and then to a tree in $𝐬{HAT}$; then read the
relevant parts of \cite{NegriVonPlato} to see how they would do that
translation.
% _____ _ _
% |_ _|__ _ __ ___ | | ___ __ _(_) ___ ___
% | |/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | | (_) | |_) | (_) | | (_) | (_| | | __/\__ \
% |_|\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
% |_| |___/
%
% «topologies» (to ".topologies")
% (ph1p 24 "topologies")
% (ph1a "topologies")
\section{Topologies}
\label {topologies}
The best way to connect ZHAs to several standard concepts is by seeing
that ZHAs are topologies on certain finite sets --- actually on
2-column acyclical graphs (sec.\ref{2CGs}). This will be done here and
in the next few sections.
\msk
\noindent
A {\sl topology} on a set $X$ is a subset $\calU$ of $\Pts(X)$ that
contains the ``everything'' and the ``nothing'' and is closed by
binary unions and intersections and by arbitrary unions. Formally:
1) $\calU$ contains $X$ and $\void$,
2) if $P,Q∈\calU$ then $\calU$ contains $P∪Q$ and $P∩Q$,
3) if $\calV ⊂ \calU$ then $\calU$ contains $\bigcup \calV$.
A {\sl topological space} is a pair $(X,\calU)$ where $X$ is a set and
$\calU$ is a topology on $X$.
When $(X,\calU)$ is a topological space and $U∈\calU$ we say that $U$
is {\sl open} in $(X,\calU)$.
\ssk
% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L X = "1.2|.3.|4.5"
%L kite = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L mp = MixedPicture.new({def="dagX", meta="s", scale="5pt"}, z):zfunction(X):output()
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="6pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagKite", meta="t", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):output()
\pu
For example, let $X$ be the ZSet $\dagX{•}{•}{•}{•}{•}$, and let's use
the characteristic function notation from sec.\ref{positional} to
denote its subsets --- we write $X=\dagX11111$ and $\void=\dagX00000$
instead of $X=\dagX{•}{•}{•}{•}{•}$ and $\void=\dagX{·}{·}{·}{·}{·}$.
If $\calU = \left\{\dagX10000, \, \dagX01000, \, \dagX00100, \,
\dagX00010, \, \dagX00001 \right\}$ then $\calU⊂\Pts(X)$ but $\calU$
fails all the conditions in 1, 2, 3 above:
1) $X=\dagX11111 \not∈ \calU$ and $\void=\dagX00000 \not∈ \calU$
2) Let $P=\dagX10000∈\calU$ and $Q=\dagX01000∈\calU$. Then
$P∩Q=\dagX00000 \not∈ \calU$ and $P∪Q=\dagX11000 \not∈ \calU$.
3) Let $\calV = \left\{\dagX01000, \, \dagX00100, \, \dagX00010
\right\} ⊂ \calU$. Then $\bigcup\calV = \dagX01000 ∪ \dagX00100 ∪
\dagX00010 = \dagX01110 \not∈ \calU$.
\msk
Now let $K=\dagKite{•}{•}{•}{•}{•}$ and $\calU = \left\{
\dagKite00000, \,
\dagKite00001, \,
\dagKite00011, \,
\dagKite00111, \,
\dagKite01011, \,
\dagKite01111, \,
\dagKite11111
\right\}$. In this case $(K,\calU)$ is a topological space.
\bsk
Some sets have ``default'' topologies on them, denoted with
`$\Opens$'. For example, $\R$ is often used to mean the topological
space $(\R, \Opens(\R))$, where:
%
$$\Opens(\R) = \setofst {U⊂\R} {U \text{ is a union of open
intervals}}.
$$
%
We say that a subset $U⊂\R$ is ``open in $\R$'' (``in the default
sense''; note that now we are saying just ``open in $\R$'', not ``open
in $(\R, \Opens(\R))$'') when $U$ is a union of open intervals, i.e.,
when $U∈\Opens(\R)$; but note that $\Pts(\R)$ and $\{\void,\R\}$ are
also topologies on $\R$, and:
%
$$\begin{array}{lclll}
\{2,3,4\} ∈\Pts(\R), &\text{so}& \{2,3,4\} \text{ is open in } (\R,\Pts(\R)), \\
\{2,3,4\}\not∈\Opens(\R), &\text{so}& \{2,3,4\} \text{ is not open in } (\R,\Opens(\R)), \\
\{2,3,4\}\not∈\{\void,\R\}, &\text{so}& \{2,3,4\} \text{ is not open in } (\R,\{\void,\R\}); \\
\end{array}
$$
%
when we say just ``$U$ is open in $X$'', this means that:
1) $\Opens(X)$ is clear from the context, and
2) $U∈\Opens(X)$.
% _____ _________ _
% |_ _|__ _ __ ___ ___ _ __ |__ / ___| ___| |_ ___
% | |/ _ \| '_ \/ __| / _ \| '_ \ / /\___ \ / _ \ __/ __|
% | | (_) | |_) \__ \ | (_) | | | | / /_ ___) | __/ |_\__ \
% |_|\___/| .__/|___/ \___/|_| |_| /____|____/ \___|\__|___/
% |_|
%
% «topologies-on-ZSets» (to ".topologies-on-ZSets")
% (ph1p 25 "topologies-on-ZSets")
% (ph1a "topologies-on-ZSets")
\section{The default topology on a ZSet}
\label {topologies-on-ZSets}
Let's define a default topology $\Opens(D)$ for each ZSet $D$.
\msk
For each ZSet $D$ we define $\Opens(D)$ as:
%
%$$\label{O(D)}
% \Opens(D) := \setofst {U⊂D} {∀((x,y),(x',y')){∈}\BPM(D). \; ((x,y){∈}U → (x',y'){∈}U)}
%$$
%
$$\label{O(D)}
\begin{array}{rcr}
\Opens(D) &:=& \{\, U⊂D \;|\; ∀((x,y),(x',y'))∈\BPM(D). \qquad\quad \\
&& (x,y)∈U → (x',y')∈U \,\} \\
\end{array}
$$
%
whose visual meaning is this. Turn $D$ into a ZDAG by adding arrows
for the black pawns moves (sec.\ref{ZDAGs}), and regard each subset
$U⊂D$ as a board configuration in which the black pieces may move down
to empty positions through the arrows. A subset $U$ is ``stable'' when
no moves are possible because all points of $U$ ``ahead'' of a black
piece are already occupied by black pieces; a subset $U$ is
``non-stable'' when there is at least one arrow
$((x,y),(x',y'))∈\BPM(D)$ in which $(x,y)$ had a black piece and
$(x',y')$ is an empty position.
In our two notations for subsets (sec.\ref{positional}) a subset $U⊂D$
is unstable when it has an arrow like `$•→·$' or `$1→0$'; remember
that black pawn moves arrows go down. A subset $U⊂D$ is stable when
none of its `$•$'s or `$1$'s can move down to empty positions.
% A subset $U⊂D$ is open iff it is stable.
``Open'' is the same as ``stable''. $\Opens(D)$ is the set of stable
subsets of $D$.
\msk
Some examples:
$\dagKite00100$ is not open because it has a 1 above a 0,
$\Opens(\dagKite{•}{•}{•}{•}{•}) = \left\{
\dagKite00000, \,
\dagKite00001, \,
\dagKite00011, \,
\dagKite00111, \,
\dagKite01011, \,
\dagKite01111, \,
\dagKite11111
\right\}$,
$\Opens(\dagHouse{•}{•}{•}{•}{•}) = \left\{
\dagHouse00000, \,
\dagHouse00001, \,
\dagHouse00010, \,
\dagHouse00011, \,
\dagHouse00101, \,
\dagHouse00111, \,
\dagHouse01010, \,
\dagHouse01011, \,
\dagHouse01111, \,
\dagHouse11111
\right\}$.
\msk
The definition of $\Opens(D)$ above can be generalized to any directed
graph. If $(A,R)$ is a directed graph, then $(A,\Opens_R(A))$ is a
topological space if we define:
%
$$\Opens_R(A) := \setofst{U⊆A}{∀(a,b)∈R.\;(a∈U→b∈U)}$$
%
The two definitions are related as this: $\Opens(D) =
\Opens_{\BPM(D)}(D)$.
Note that we can see the arrows in $\BPM(D)$ or in $R$ as {\sl
obligations} that open sets must obey; each arrow $a→b$ says that
every open set that contains $a$ is forced to contain $b$ too.
% _____ _
% |_ _|__ _ __ ___ __ _ ___ ___ _ __ __| | ___ _ __ ___
% | |/ _ \| '_ \/ __| / _` / __| / _ \| '__/ _` |/ _ \ '__/ __|
% | | (_) | |_) \__ \ | (_| \__ \ | (_) | | | (_| | __/ | \__ \
% |_|\___/| .__/|___/ \__,_|___/ \___/|_| \__,_|\___|_| |___/
% |_|
%
% «topologies-as-partial-orders» (to ".topologies-as-partial-orders")
% (ph1p 26 "topologies-as-partial-orders")
% (ph1a "topologies-as-partial-orders")
\section{Topologies as partial orders}
\label {topologies-as-partial-orders}
For any topological space $(X,\Opens(X))$ we can regard $\Opens(X)$ as
a partial order, ordered by inclusion, with $\void$ as its minimal
element and $X$ as its maximal element; we denote that partial order
by $(\Opens(X),⊆)$.
Take any ZSet $D$. The partial order $(\Opens(D),⊆)$ will {\sl
sometimes} be a ZHA when we draw it with $\void$ at the bottom, $D$
at the top, and inclusions pointing up, as can be seen in the three
figures below; when $D=\dagHouse{•}{•}{•}{•}{•}$ or
$D=\dagGuill{•}{•}{•}{•}{•}{•}$ the result is a ZHA, but when
$D=\dagW{•}{•}{•}{•}{•}$ it is not.
Let's write ``$V⊂_1U$'' for ``$V⊆U$ and $V$ and $U$ differ in exactly
one point''. When $D$ is a ZSet the relation $⊆$ on $\Opens(D)$ is the
transitive-reflexive closure of $⊂_1$, and $(\Opens(D),⊂_1)$ is easier
to draw than $(\Opens(D),⊆)$.
% (find-angg ".emacs" "find-planarhas")
% (find-planarhas "background-story")
% (find-planarhaspage 8 "Background story")
% (find-planarhastext 8 "Background story")
% (find-planarhas "background-story-2")
% (find-planarhaspage 9 "Background story, 2")
% (find-planarhastext 9 "Background story, 2")
% New diagram:
%
% Notes on the names:
% We deal with the ZDAGs "H" ("House"), "G" ("Guill") and "W".
%
% \zfHouse01010 draws a characteristic function of a subset of the ZSet H
% \zha{House} draws the "house" ZDAG with arrows (black pawn's moves)
% \zha{OHouse} draws ZDAG (H,O(H)) - a Heyting Algebra - with white pawn's moves
%
% Note that \zha{House} is not a ZHA - it is only a ZDAG, but we use
% the library for ZHAs to draw it - and \zha{OW} is a non-planar
% Heyting Algebra containing a cube!
%
%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
%R house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({zdef="House" , scale="20pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({zdef="OHouse", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R
%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
%R guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R guill:tomp({zdef="Guill", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({zdef="OGuill", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R
%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({zdef="W", scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({zdef="OW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%
$$\pu
\begin{array}{ccl}
(H,\BPM(H)) = \zha{House}
& \qquad
& (\Opens(H), ⊂_1) = \def\h{\zfHouse}\zha{OHouse} \\
\\
(G,\BPM(G)) = \zha{Guill}
& \qquad
& (\Opens(G), ⊂_1) = \def\g{\zfGuill}\zha{OGuill} \\
\\
(W,\BPM(W)) = \zha{W}
& \qquad
& (\Opens(W), ⊂_1) = \def\w{\zfW}\zha{OW} \\
\end{array}
$$
% Old diagram:
% %
% %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="20pt", meta=nil}):addbullets():addarrows():output()
% %R ohouse:tomp({def="zdagOHouse", scale="28pt", 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="20pt", meta=nil}):addbullets():addarrows():output()
% %R oguill:tomp({def="zdagOGuill", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
% %R oguill:tozmp({def="zdagoguill", scale="12pt", meta="s"}):addlrs():addarrows():output()
% %
% %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="20pt", meta=nil}):addbullets():addarrows() :output()
% %R W:tomp({def="zdagOW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
% %
% $$\pu
% \begin{array}{ccl}
% (H,\BPM(H)) = \zdagHouse
% & \qquad
% & (\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse \\
% \\
% (G,\BPM(G)) = \zdagGuill
% & \qquad
% & (\Opens(G), ⊂_1) = \def\g{\zfGuill}\zdagOGuill \\
% \\
% (W,\BPM(W)) = \zdagW
% & \qquad
% & (\Opens(W), ⊂_1) = \def\w{\zfW}\zdagOW \\
% \end{array}
% $$
We can formalize a ``way to draw $\Opens(D)$ as a ZHA'' (or ``...as a
ZDAG'') as a bijective function $f$ from a ZHA (or from a ZSet) $S$ to
$\Opens(D)$ that creates a perfect correspondence between the white
moves in $S$ and the ``$V⊂_1U$-arrows''; more precisely, an $f$ such
that this holds: if $a,b∈S$ then $(a,b)∈\WPM(S)$ iff $f(a)⊂_1f(b)$.
Note that the {\sl number of elements} in an open set corresponds to
the {\sl height} where it is drawn; if $f:S→\Opens(D)$ is a way to
draw $\Opens(D)$ as a ZHA or a ZDAG then $f$ takes points of the form
$(\_\_,y)$ to open sets with $y$ elements, and if $f:S→\Opens(D)$ is a
way to draw $\Opens(D)$ as a ZHA (not a ZDAG!) then we also have that
$f((0,0)) = \void ∈ \Opens(D)$.
\msk
The diagram for $(\Opens(H), ⊂_1)$ above is a way to draw $\Opens(H)$
as a ZHA.
The diagram for $(\Opens(G), ⊂_1)$ above is a way to draw $\Opens(G)$
as a ZHA.
The diagram for $(\Opens(W), ⊂_1)$ above is {\sl not} a way to draw
$\Opens(W)$ as a ZSet. Look at $\dagW01011$ and $\dagW10111$ in the
middle of the cube formed by all open sets of the form $\dagW abc11$.
We don't have $\dagW01011 ⊂_1 \dagW10111$, but we do have a white pawn
move (not draw in the diagram!) from $f¹(\dagW01011)$ to
$f¹(\dagW10111)$. We say that a ZSet is {\sl thin} when it doesn't
have three independent points.
\msk
Every time that a ZSet $D$ has three independent points, as in $W$, we
will have a situation like in $(\Opens(W), ⊂_1)$; for example, if
$B=\dagHex{•}{•}{•}{•}{•}{•}{•}$ then the open sets of $B$ of the form
$\dagHex00abc11$ form a cube.
% \bsk
% \bsk
% \bsk
%
%
% The definition for $\Opens(D)$ in page \pageref{O(D)} can be generalized
% to any directed graph. If $(A,R)$ is a directed graph, then
% %
% $$\Opens(A,R) := \setofst {U⊆A} {∀(a,b){∈}R.\; (a{∈U}→b{∈U})},$$
% %
% is the {\sl set of down-sets} on $A$ (see DaveyPriestley, pp.20-21).
% There are some directed graphs,
% ____ ____ ____
% |___ \ / ___/ ___|___
% __) | | | | _/ __|
% / __/| |__| |_| \__ \
% |_____|\____\____|___/
%
% «2CGs» (to ".2CGs")
% (ph1p 28 "2CGs")
% (ph1a "2CGs")
\section{2-Column Graphs}
\label {2CGs}
\def\l#1{#1\_}
\def\r#1{\_#1}
Note: in this section we will manipulate objects with names like $1\_,
2\_, 3\_, \ldots,$ $\_1, \linebreak[0] \_2, \linebreak[0] \_3,
\ldots$; here are two good ways to formalize them:
%
$$\begin{array}{cc}
\vdots & \vdots \\
4\_=(0,4) & \_4=(1,4) \\
3\_=(0,3) & \_3=(1,3) \\
2\_=(0,2) & \_2=(1,2) \\
1\_=(0,1) & \_1=(1,1) \\
\end{array}
\quad
\text{or}
\quad
\begin{array}{cc}
\vdots & \vdots \\
4\_=\verb|"4_"| & \_4=\verb|"_4"| \\
3\_=\verb|"3_"| & \_3=\verb|"_3"| \\
2\_=\verb|"2_"| & \_2=\verb|"_2"| \\
1\_=\verb|"1_"| & \_1=\verb|"_1"| \\
\end{array},
$$
%
where \verb|"1_"|, \verb|"_2"|, \verb|""|, \verb|"Hello!"|, etc are
strings.
\msk
We define:
%
$$\begin{array}{ccc}
\LC(l) &:=& \{1\_, 2\_, \ldots, l\_\} \\
\RC(r) &:=& \{\_1, \_2, \ldots, \_r\}, \\
\end{array}
$$
%
which generate a ``left column'' of height $l$ and a ``right column''
of height $r$.
A {\sl description for a 2-column graph} (a ``D2CG'') is a 4-tuple
$(l,r,R,L)$, where $l,r∈\N$, $R⊂\LC(l)×\RC(r)$, $L⊂\RC(r)×\LC(l)$; $l$
is the height of the left column, $r$ is the height of the right
column, and $R$ and $L$ are set of intercolumn arrows (going right and
left respectively).
The operation $\TCG$ (in a sans-serif font) generates a directed graph
from a D2CG:
$$\begin{array}{rcl}
\TCG(l,r,R,L) &:=& \left(\LC(l)∪\RC(r),
\csm{\{\ltol{l}{(l-1)}, \;\ldots, \;\ltol21\}∪ \\
\{\rtor{r}{(r-1)}, \;\ldots, \;\rtor21\}∪ \\
R∪L
}
\right)
\end{array}
$$
For example,
%
$$\begin{array}{rcl}
\TCG(3,4,\csm{\ltor34, \\ \ltor23},
\csm{\lotr22, \\ \lotr12})
&:=& \left(\csm{\phantom{\l4,}\; \l3, \; \l2, \; \l1, \\
\r4, \; \r3, \; \r2, \; \r1 \\
},
\csm{\phantom{\rtor43,\;}\ltol32,\; \ltol21, \\
\rtor43 ,\; \rtor32,\; \rtor21, \\
\ltor34,\;\ltor23, \\
\lotr22,\;\lotr12 \\
}
\right)
\end{array}
$$
%
which is:
%
%L tcg_big = {scale="14pt", meta="p", dv=2, dh=2.75, ev=0.32, eh=0.275}
%L tcg_Big = {scale="14pt", meta="p", dv=2, dh=3.5, ev=0.32, eh=0.200}
%L tcg_medium = {scale= "9pt", meta="p s", dv=1, dh=2.2, ev=0.32, eh=0.275}
%L tcgnew = function (opts, def, str)
%L return TCG.new(opts, def, unpack(split(str, "[ %d]+")))
%L end
%L tcgbig = function (def, spec) return tcgnew(tcg_big, def, spec or tcg_spec) end
%L tcgBig = function (def, spec) return tcgnew(tcg_Big, def, spec or tcg_spec) end
%L tcgmed = function (def, spec) return tcgnew(tcg_medium, def, spec or tcg_spec) end
%L
%L tcg = TCG.new(tcg_big, "tcgbiga", 3, 4, "34 23", "22 12"):lrs():vs():hs():output()
$$\pu
\tcgbiga
$$
%
we will usually draw that more compactly, by omitting the intracolumn
(i.e., vertical) arrows:
%
%L tcg_spec = "3, 4; 34 23, 22 12"
%L tcgmed("tcgmedlrs"):lrs():hs():output()
%L tcgmed("tcgmedbus"):bus():hs():output()
$$\pu
\tcgmedlrs
\quad
\text{or}
\quad
\tcgmedbus.
$$
A {\sl 2-column graph} (a ``2CG'') is a directed graph that is of the
form $\TCG(l,r,R,L)$. We will often say $(P,A) = \TCG(l,r,R,L)$, where
the $P$ stand for ``points'' and $A$ for ``arrows''.
A {\sl 2-column acyclical graph} (a ``2CAG'') is a 2CG that doesn't
have cycles. If $L$ has an arrow that is the opposite of an arrow in
$R$, this generates a cycle of length 2; if $R$ has an arrow
$\ltor{l}{r'}$ and $L$ has an arrow $\lotr{l'}{r}$, where $l≤l'$ and
$r≤r'$, this generates a cycle that can have a more complex shape ---
a triangle or a bowtie. For example,
%L tcg_spec = "4, 3; 32, 32"
%L tcgbig("tcgbigwithbig") :lrs():vs():hs():output()
%L tcg_spec = "3, 4; 14, 32"
%L tcgbig("tcgbigwithbowtie"):lrs():vs():hs():output()
$$\pu
\tcgbigwithbig
\quad
\text{and}
\quad
\tcgbigwithbowtie.
$$
% _____ ____ ____ ____
% |_ _|__ _ __ ___ ___ _ __ |___ \ / ___/ ___|___
% | |/ _ \| '_ \/ __| / _ \| '_ \ __) | | | | _/ __|
% | | (_) | |_) \__ \ | (_) | | | | / __/| |__| |_| \__ \
% |_|\___/| .__/|___/ \___/|_| |_| |_____|\____\____|___/
% |_|
%
% «topologies-on-2CGs» (to ".topologies-on-2CGs")
% (ph1p 29 "topologies-on-2CGs")
% (ph1a "topologies-on-2CGs")
\section{Topologies on 2CGs}
\label {topologies-on-2CGs}
%\catcode`↓=13 \def↓{\dnto}
%\catcode`↓=13 \def↓{{\dnto}}
\def\dnto{\downarrow}
\def\dnto{{\downarrow}}
In this section we will see that ZHAs are topologies on 2CAGs.
\msk
\noindent
Let $(P,A) = \TCG(l,r,R,L)$ be a 2-column graph.
\noindent
What happens if we look at the open sets of $(P,A)$, i.e., at
$\Opens_A(P)$? Two things:
1) every open set $U∈\Opens_A(P)$ is of the form $\LC(a)∪\RC(b)$,
2) arrows in $R$ and $L$ forbids some `$\LC(a)∪\RC(b)$'s from being
open sets.
\noindent
In order to understand that we need to introduce some notations for
``piles''.
\msk
The function
%
$$\pile(\ang{a,b}) := \LC(a)∪\RC(b)$$
%
converts an element $\ang{a,b}∈\LR$ into a pile of elements in the
left column of height $a$ and a pile of elements in the right column
of height $b$. We will write subsets of the points of a 2CG using a
positional notation with arrows. So, for example, if $(P,A) =
\TCG(3,4,\{\ltor23\}, \{\lotr22\})$ then
%
%L tcg_spec = "3, 4; 23, 22"
%L tcgmed("tcgmedConvLR") :lrs() :hs():output()
%L tcgmed("tcgmedConvBool"):cs("110", "1000"):hs():output()
$$\pu
(P,A)=\tcgmedConvLR
\qquad
\text{and}
\qquad
\pile(21) = \tcgmedConvBool \;\; \text{(as a subset of $P$)}.
$$
Note that $\pile(21)$ is not open in $(P,\Opens_A(P))$, as it has an
arrow `$1→0$'. In fact, the presence of the arrow $\{\ltor23\}$ in $A$
means that all piles of the form
%
%L tcgmed("tcgmedConvQA"):cs("11?", "??00"):hs():output()
$$\pu
\tcgmedConvQA
$$
%
are not open, the presence of the arrow $\{\lotr22\}$ means that the
piles of the form
%
%L tcgmed("tcgmedConvQB"):cs("?00", "11??"):hs():output()
$$\pu
\tcgmedConvQB
$$
%
are not open sets.
The effect of these prohibitions can be expressed nicely with
implications. If
%
$$(P,A) = \TCG(l,r,\csm{\ltor cd, \\ \ltor ef}, \csm{\lotr gh, \\ \lotr ij})$$
%
then
%
$$\Opens_A(P) = \setofst {\pile(ab)}
{a∈\{0,\ldots,l\},
b∈\{0,\ldots,r\},
\psm {a≥c \,→\, b≥d \; ∧ \\
a≥e \,→\, b≥f \; ∧ \\
a≥g \,←\, b≥h \; ∧ \\
a≥i \,←\, b≥j \;\;\; \\
}
}
$$
Let's use a shorter notation for comparing 2CGs and their topologies:
%
%L tcg_spec = "4, 5; 32, 14 25"
%L tcgBig("tcgbigConvShorter"):lrs():hs():vs():output()
%L z = LR.fromtwocolgraph(4, 5, "32", "14 25"):zha()
%L MixedPicture.new({def="zhaConvShorter", scale="12pt", meta=nil}, z):addlrs():output()
$$
\pu
\Opens \tcgbigConvShorter \quad = \quad \zhaConvShorter
% \bigthinge
$$
%
the arrows in $R$ and $L$ and the values of $l$ and $r$ are easy to
read from the 2CG at the left, and we omit the `$\pile$'s at the
right.
\msk
In a situation like the above we say that the 2CG in the
`$\Opens(\ldots)$' {\sl generates} the ZHA at the right. There is an
easy way to draw the ZHA generated by a 2CG, and a simple way to find
the 2CG that generates a given ZHA. To describe them we need two new
concepts.
If $(A,R)$ is a directed graph and $S⊂A$ then $↓S$ is the smallest
open set in $\Opens_R(A)$ that contains $S$. If $(A,R)$ is a ZDAG with
black pawns moves as its arrows, think that the `1's in $S$ are
painted with a black paint that is very wet, and that that paint flows
into the `0's below; the result of $↓S$ is what we get when all the
`0's below `1's get painted black. For example: $↓\dagGuill010000 =
\dagGuill010111$. When $(P,A)$ is a 2CG and $S⊆P$, we have to think
that the paint flows along the arrows, even if some of the intercolumn
arrows point upward. For example:
%
%L tcg_spec = "3, 4; 23, 22"
%L tcgmed("tcgpaintA"):cs("100", "0100"):hs():output()
%L tcgmed("tcgpaintB"):cs("110", "1110"):hs():output()
%
$$\pu
↓\tcgpaintA = \tcgpaintB
$$
%
and if $S$ consists of a single point, $S=\{s\}$, then we may write
$↓s$ instead of $↓\{s\} = ↓S$. In the 2CG above, we have (omitting the
`$\pile$'s):
%
%L tcgmed("tcgpaintC"):cs("000", "0100"):hs():output()
%L tcgmed("tcgpaintD"):cs("110", "1110"):hs():output()
%
$$\pu
↓\r2 \;=\; ↓\{\r2\} =\;
↓\tcgpaintC = \tcgpaintD = \;23,
\quad
\text{and}
\quad
\sm{ && ↓\r4=24, \\
↓\l3=33, && ↓\r3=23, \\
↓\l2=23, && ↓\r2=23, \\
↓\l1=10, && ↓\r1=01, \\
}
$$
The second concept is this: the ``generators'' of a ZDAG $D$ with
white pawns moves as its arrows --- or of a ZHA $D$ --- are the points
of $D$ that have exactly one white pawn move pointing {\sl to} them
(not {\sl going out of} them).
\msk
If $(P,A)$ is a 2CAG, then $\Opens_A(P)$ is a ZHA, and `$↓$' is a
bijection from $P$ to the generators of $\Opens_A(P)$; for example:
%L tcg_spec = "4, 5; 32, 14 25"
%L tcgBig("tcgGens"):lrs():hs():vs():output()
%L z = LR.fromtwocolgraph(4, 5, "32", "14 25"):zha()
%L MixedPicture.new({def="zhaGens", scale="12pt", meta=nil}, z):addlrs():output()
%L MixedPicture.new({def="zhaGensGens", scale="12pt", meta=nil}, z):addgens():output()
$$
\pu
\Opens \tcgGens \quad = \quad \zhaGens
\qquad
\qquad
\zhaGensGens
% \bigthinge
$$
%
but if $(P,A)$ is a 2CG with cycles, then $\Opens_A(P)$ is not a ZHA
because each cycle generates a ``gap'' that disconnects the points of
$\Opens_A(P)$. We just saw an example of a 2CG with a cycle in which
$↓\l2 = 23 = ↓\r3 = ↓\r2$; look at its topology:
%
%R tcg_spec = "3, 4; 23, 22"
%R tcgbig("tcgLoop"):lrs():vs():hs():output()
%R local top =
%R 2/ 34 \
%R | 33 24|
%R | 23 |
%R | |
%R | |
%R | 11 |
%R |10 01 |
%R \ 00 /
%R top:tomp({def="zhaLoop", scale="12pt"}):addcells():output()
%
$$\pu
\Opens\tcgLoop \quad = \quad \zhaLoop
$$
% _____ _ _ _
% |_ _|__ _ __ ___ __ _ ___ | | | | / \ ___
% | |/ _ \| '_ \/ __| / _` / __| | |_| | / _ \ / __|
% | | (_) | |_) \__ \ | (_| \__ \ | _ |/ ___ \\__ \
% |_|\___/| .__/|___/ \__,_|___/ |_| |_/_/ \_\___/
% |_|
%
% «topologies-as-HAs» (to ".topologies-as-HAs")
% (ph1p 32 "topologies-as-HAs")
% (ph1a "topologies-as-HAs")
\section{Topologies as Heyting Algebras}
\label {topologies-as-HAs}
\def\toM{\ton{\text{M}}}
The {\sl open-set semantics} for Intuitionistic Propositional Logic is
based on this idea: choose any topological space $(X,\Opens(X))$; the
opens sets of $\Opens(X)$ will play the role of truth-values, and we
define the components of a Heyting Algebra (sec.\ref{HAs}) as this:
%
$$\begin{array}{rclcl}
Ω &:=& \Opens(X) \\
P ≤ Q &:=& P⊆Q \\
⊤ &:=& \setofst{x∈X}{⊤} &=& X \\
⊥ &:=& \setofst{x∈X}{⊥} &=& ∅ \\
P ∧ Q &:=& \setofst{x∈X}{x∈P∧x∈Q} &=& P∩Q \\
P ∨ Q &:=& \setofst{x∈X}{x∈P∨x∈Q} &=& P∪Q \\[5pt]
P \toM Q &:=& \setofst{x∈X}{x∈P→x∈Q} \\
&=& \setofst{x∈X}{x\not∈P∨x∈Q} &=& (X∖P)∪Q \\
\end{array}
$$
%
However, this `$\toM$' {\sl may} return a non-open result even when
given open inputs,
%
$$\dagHouse 01010 \toM \dagHouse 00011 \;=\; \dagHouse 10111$$
%
so our definition is broken; we can fix it by taking the interior:
%
% (see sec.\ref{propagation}):
%
$$\begin{array}{rclcl}
P \to Q &:=& \Int(P \toM Q) % \\
% &=& \Int(\setofst{x∈X}{x∈P→x∈Q}) \\
&=& \Int((X∖P)∪Q) \\
\end{array}
$$
\begin{theorem}
For any topological space $(X,\Opens(X))$ the structure
$(Ω,≤,⊤,⊥,∧,∨,→)$ defined as above is a Heyting Algebra. In
particular, this holds for any $P,Q,R∈Ω$: $P≤(Q→R)$ iff $(P∧Q)≤R$.
\label{topologies-as-HAs-thm}
\end{theorem}
\begin{proof}
Standard; see for example \cite{Awodey} (section 6.3).
\end{proof}
Note that Theorem \ref{topologies-as-HAs-thm} gives us another way to
calculate the connectives in 2CGs. In sec.\ref{prop-calc-ZHA} we saw
how to calculate $¬¬P→P$ in a certain ZHA when $P=10$; compare it with
the ``topological'' way, in which the truth-values are subsets of
$\dagHouse{•}{•}{•}{•}{•}$:
%
% Old diagrams:
%
% $$\und{\und{¬\und{¬ \und{P}{10}}{02}}{20} → \und{P}{10}}{12}
% \qquad
% \qquad
% \und{\und{¬\und{¬ \und{P}{\dagHouse 00010}}{\dagHouse 00101}}{\dagHouse 01010}
% → \und{P}{\dagHouse 00010}}{\dagHouse 00111}
% $$
%
% New diagrams:
%
%UB (¬ ¬ P) → P
%UB -- --
%UB 10 10
%UB ---
%UB 02
%UB -----
%UB 20
%UB -----------
%UB 12
%L
%L defub "ntntP -> P"
%
%UB (¬ ¬ P ) → P
%UB ------- -------
%UB \h00010 \h00010
%UB --------
%UB \h00101
%UB ---------
%UB \h01010
%UB ----------------------
%UB \h00111
%L
%L defub "ntntP -> P : houses"
%L
$$\pu
\ub{ntntP -> P}
\qquad
\qquad
\def\h{\dagHouse}
\ub{ntntP -> P : houses}
$$
% ______ _ _ __ __ ____ ____ _ ____
% |__ / | | | / \ ___ / / \ \ |___ \ / ___| / \ / ___|___
% / /| |_| | / _ \ / __| / /_____\ \ __) | | / _ \| | _/ __|
% / /_| _ |/ ___ \\__ \ \ \_____/ / / __/| |___ / ___ \ |_| \__ \
% /____|_| |_/_/ \_\___/ \_\ /_/ |_____|\____/_/ \_\____|___/
%
% «converting-ZHAs-2CAGs» (to ".converting-ZHAs-2CAGs")
% (ph1p 33 "converting-ZHAs-2CAGs")
% (ph1a "converting-ZHAs-2CAGs")
\section{Converting between ZHAs and 2CAGs}
\label {converting-ZHAs-2CAGs}
Let's now see how to start from a 2CAG and produce its topology (a
ZHA) quickly, and how to find quickly the 2CAG that generates a given
ZHA.
\msk
{\sl From 2CAGs to ZHAs.} Let $(P,A) = \TCG(l,r,R,L)$ be a 2CAG, and
call the ZHA generated by it $H$. Then the top point of $H$ is $lr$,
and its bottom point is 00. Let $C := \{00, ↓\l1, ↓\l2, \ldots, ↓\l l,
lr\}$, i.e., the left generators (see the end of
sec.\ref{topologies-on-2CGs}) plus $⊥$ and $⊤$; then $C$ has some of
the points of the left wall (sec.\ref{ZHAs}) of $H$, but usually not
all. To ``complete'' $C$, apply this operation repeatedly: if $ab∈C$
and $ab≠lr$, then test if either $(a+1)b$ or $a(b+1)$ are in $C$; if
none of them are, add $a(b+1)$, which is northeast of $ab$. When there
is nothing else to add, then $C$ is the whole of the left wall of $H$.
For the right wall, start with $D := \{00, ↓\r1, ↓\r2, \ldots, ↓\r r,
lr\}$, and for each $ab∈C$ with $ab≠lr$, test if either $(a+1)b$ or
$a(b+1)$ are in $D$; if none of them are, add $(a+1)b$, which is
northwest of $ab$. When there is nothing else to add, then $D$ is the
whole of the right wall of $H$.
In the acyclic example of the last section this yields:
%
$$\begin{array}{rcl}
C &=& \{00, ↓\l1, ↓\l2, ↓\l3, ↓\l4, lr\} \\
&=& \{00, 10, 20, 32, 42, 45\} \\
&\squigto& \{00, 10, 20, 21, 22, 32, 42, 43, 44, 45\}, \\
D &=& \{00, ↓\r1, ↓\r2, ↓\r3, ↓\r4, ↓\r5, lr\} \\
&=& \{00, 01, 02, 03, 14, 25, 45\} \\
&\squigto& \{00, 01, 02, 03, 13, 14, 24, 25, 35, 45\}. \\
\end{array}
$$
%
and the ZHA is everything between the ``left wall'' $C$ and the
``right wall'' $D$.
\msk
{\sl From ZHAs to 2CAGs.} Let $H$ be a ZHA and let $lr$ be its top
point. Form the sequence of its left wall generators (the generators
of $H$ in which the arrow pointing to them points northwest) and the
sequence of its right wall generators (the generators of $H$ in which
the arrow pointing to them points northeast). Look at where there are
``gaps'' in these sequences; each gap in the left wall generators
becomes an intercolumn arrow going right, and each gap in the right
wall generators becomes an intercolun arrow going left. In the acyclic
example of the last section, this yields:
%
$$\def\gap#1{\!\!\!\!\!\text{(gap, arrow $#1$)}}
\def\gap#1{\!\!\!\!\!\text{(gap becomes $#1$)}}
\def\nogap{\!\!\!\!\!\text{(no gap)}}
%
\begin{array}{lllllll}
& && \r5 = 25 & \\
& && & \gap{\lotr25} \\
\l4 = 42 & && \r4 = 14 & \\
&\nogap && & \gap{\lotr14} \\
\l3 = 32 & && \r3 = 03 & \\
&\gap{\ltor32} && & \nogap \\
\l2 = 20 & && \r2 = 02 & \\
&\nogap && & \nogap \\
\l1 = 10 & && \r1 = 01 & \\
\end{array}
$$
%
We know $l$ and $r$ from the top point of the ZHA, and from the gaps
we get $R$ and $L$; the 2CAG that generates this ZHA is:
%
$$(4,5,\cmat{\ltor32},\cmat{\lotr25, \\ \lotr14}).$$
% (find-planarhas "2-column-graphs")
% (find-planarhaspage 10 "2-Column graphs")
% (find-planarhastext 10 "2-Column graphs")
\msk
\begin{theorem}
The two operations above are inverse to one another in the following
sense. If we start with a ZHA $H$, produce its 2CAG, and produce a ZHA
$H'$ from that, we get the same ZHA: $H'=H$. In the other direction,
if we start with a 2CAG $(P,A) = \TCG(l,r,R,L)$, produce its ZHA, $H$,
and then obtain a 2CAG $(P',A') = \TCG(l',r',R',L')$ from $H$, we get
back the original 2CAG {\sl if and only if it didn't have any
superfluous arrows}; if the original 2CAG had superflous arrows then
then new 2CAG will have $l'=l$, $r'=r$, and $R'$ and $L'$ will be $R$
and $L$ minus these ``superfluous arrows'', that are the ones that can
be deleted without changing which 2-piles are forbidden. For example:
%
%L tcg_spec = "4, 4; 44 43 32 22, "
%L tcgbig("tcgRedundant"):lrs():vs():hs():output()
%L tcg_spec = "4, 4; 44 22, "
%L tcgbig("tcgRedundantClean"):lrs():vs():hs():output()
%L mpnew({def="zhaRedundant", scale="12pt"}, "12RR3L21L"):addlrs():output()
%
$$\pu
\begin{array}{rcccl}
\tcgRedundant &\sa& \zhaRedundant &\sa& \tcgRedundantClean \\
% R =\cmat{\ltor44, \\ \ltor43, \\ \ltor32, \\ \ltor22} &&&&
% R'=\cmat{\ltor44, \\ \ltor22} \\
\end{array}
$$
%
In this case we have $R =\csm{\ltor44, \\ \ltor43, \\ \ltor32,
\\ \ltor22}$ and $R'=\csm{\ltor44, \\ \ltor22}$.
\end{theorem}
%
% \begin{proof}
% Proof of your theorem.
% \end{proof}
%
% {\sl Theorem.} The two operations above are inverse to one another in
% the following sense. If we start with a ZHA $H$, produce its 2CAG, and
% produce a ZHA $H'$ from that, we get the same ZHA: $H'=H$. In the
% other direction, if we start with a 2CAG $(P,A) = \TCG(l,r,R,L)$,
% produce its ZHA, $H$, and then obtain a 2CAG $(P',A') =
% \TCG(l',r',R',L')$ from $H$, we get back the original 2CAG {\sl if and
% only if it didn't have any superfluous arrows}; if the original 2CAG
% had superflous arrows then then new 2CAG will have $l'=l$, $r'=r$, and
% $R'$ and $L'$ will be $R$ and $L$ minus these ``superfluous arrows'',
% that are the ones that can be deleted without changing which 2-piles
% are forbidden. For example:
%
% ___ ____ _ __ ______ _ _ _ __ ____ ____ _
% |_ _| _ \| | / / |__ / | | | / \ | | / / / ___| _ \| |
% | || |_) | | / / / /| |_| | / _ \ | | / / | | | |_) | |
% | || __/| |___ \ \ / /_| _ |/ ___ \| |___ \ \ | |___| __/| |___
% |___|_| |_____| \_\ /____|_| |_/_/ \_\_____| \_\ \____|_| |_____|
%
% «ZHAL-is-between» (to ".ZHAL-is-between")
% (ph1p 34 "ZHAL-is-between")
% (ph1a "ZHAL-is-between")
\section{ZHA Logic is between IPL and CPL}
\label{ZHAL-is-between}
% (find-books "__logic/__logic.el" "chagrov")
% (find-chagrovzmlpage (+ 15 112) "BW_n")
In standard terminology, this is: ZHA Logic is a superintuitionistic
logic (\cite{ChagrovZakharyaschev}, p.109) of ``bounded width 2'',
i.e., where the axiom $𝐛{BW}_2$ of \cite{ChagrovZakharyaschev}, p.112,
holds. But let's see this in elementary terms.
\def\IPL {\mathsf{IPL}}
\def\ZHAL{\mathsf{ZHAL}}
\def\CPL {\mathsf{CPL}}
\def\Taut{\mathsf{Taut}}
\def\Vars{\mathsf{Vars}}
\def\bfV {\mathbf{V}}
% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L local Pyr = ".1.|234"
%L mp = MixedPicture.new({def="dagPyr", meta="s", scale="5pt"}, z):zfunction(Pyr):output()
\pu
Let $S$ be this sentence:
%
$$\begin{array}{rcl}
S_P &:=& P→(Q∨R) \\
S_Q &:=& Q→(R∨P) \\
S_R &:=& R→(P∨Q) \\
S &:=& S_P ∨ S_Q ∨ S_R \\
\end{array}
$$
$S$ can't be an intuitionistic theorem because in this Heyting
Algebra, with these values for $P$, $Q$, $R$,
%
%R local w, womit, W =
%R 2/ #1 \, 2/ T \, 6/ !w1111 \
%R \#2#3#4/ | a | | !w0111 |
%R |b c d | |!w0110!w0101!w0011|
%R |e f g | |!w0100!w0010!w0001|
%R \ h / \ !w0000 /
%R w:tomp({def="zfPyr#1#2#3#4", scale="5pt", meta="s"}):addcells():output()
%R w:tomp({def="zfPyrmed#1#2#3#4", scale="24pt", meta=nil}):addcells():addarrows():output()
%R w:tomp({def="zfPyrbig#1#2#3#4", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagPyr", scale="13pt", meta=nil}):addbullets():addarrows():output()
%R W:tomp({def="zdagOPyr", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(1,2)0"):output()
%
$$
\pu
\def\w{\zfPyr}
(W,A) = \zfPyrmed1234 %\zdagPyr
\qquad
(\Opens_A(W), ⊂_1) = \zdagOPyr
\qquad
\begin{array}{rcl}
P &=& \dagPyr0100 \\
Q &=& \dagPyr0010 \\
R &=& \dagPyr0001 \\
\end{array}
$$
%
we have $S=\dagPyr0111≠⊤=\dagPyr1111$.
One way to define a {\sl valuation} for a sentence $S$ with variables
$\Vars(S)$ --- in our example we have $\Vars(S)=\{P,Q,R\}$) --- is as
a pair made of a Heyting Algebra $H$ and a function $v:\Vars(S)→H$. A
looser definition is that a valuation for $S$ is a pair made of 1)
something that generates a Heyting Algebra in a known, canonical way,
and 2) a function from $\Vars(S)$ to the elements of that HA. So:
\msk
A {\sl classical valuation} for $S$ is a valuation of the form
$(\{0,1\},v)$.
A {\sl ZHA-valuation} for $S$ is a valuation of the form $(H,v)$,
where $H$ is a ZHA.
A {\sl finite DAG-valuation} for $S$ is a valuation of the form
$((W,A),v)$, where $W$ is a finite set and $A⊆W×W$ is a set of arrows
on $W$; the Heyting Algebra on $(W,\Opens_A(W))$ is built as in
sec.\ref{topologies-as-HAs}.
A {\sl 2CG-valuation} for $S$ is a finite DAG-valuation for $S$ of the
form $((P,A),v)$, where $(P,A)$ is a 2-column graph; each
2CG-valuation is naturally equivalent to a ZHA-valuation, and
vice-versa.
\msk
A {\sl classical countermodel} for $S$ is classical valuation for $S$
in which the value of $S$ is not $⊤$; a {\sl ZHA-countermodel} for $S$
is a ZHA-valuation for $S$ in which the value of $S$ is not $⊤$; an
{\sl intuitionistic countermodel} for $S$ is a finite DAG-valuation for $S$
in which the value of $S$ is not $⊤$.
\msk
A sentence $S$ is a {\sl classical tautology} (notation:
$S∈\Taut(\CPL)$) if $S$ has no classical countermodels; a sentence $S$
is a {\sl ZHA-tautology} (notation: $S∈\Taut(\ZHAL)$); and a sentence
$S$ is an {\sl intuitionistic tautology} (notation: $S∈\Taut(\IPL)$)
of $S$ has no finite-DAG countermodels.
\msk
It is a standard result that the intuitionistic {\sl theorems} are
exactly the finite-DAG {\sl tautologies}; this can be seen using Gödel
translation (see \cite{Goedel1933f} and \cite{Goedel1933fintro}) to
translate $S$ to S4, and then using modal tableaux for S4
(\cite{Fitting72}) to look for a countermodel; in standard
terminology, $W$ is a set of ``worlds'', $A$ is an ``accessibility
relation'' or a notion of which worlds are ``ahead'' of which other
ones, and $(W,A^*)$ is a Kripke frame for S4.
The sentence $S=S_P ∨ S_Q ∨ S_R$ of the beginning of the section is a
good example for introducting tableau methods for modal logics to
``children'', as the tableau that it generates doesn't have branches.
We can present the method directly and in elementary terms, as we will
do now.
\msk
Fix a set $W$ and a relation $A⊆W×W$. We will say that $β$ is
``ahead'' of $α$ when $(α,β)∈A^*$, i.e., when there is a path
$α→\ldots→β$ using only arrows in $A$. Let $P$ and $Q$ be open sets in
$\Opens_A(W)$. The only way to have $P∨Q$ false in a world $α$
(notation: $(P∨Q)_α=0$) is to have $P_α=0$ and $Q_α=0$. The only way
to have $P→Q$ false in a world $α$, i.e., $(P→Q)_α=0$ is to have
$P_β=1$ and $Q_β=0$ in {\sl some} world $β$, with $β$ ahead of $α$.
Let $((W,A),v)$ be a finite DAG-countermodel for $S=S_P ∨ S_Q ∨ S_R$.
Then $v(P), \linebreak[0] v(Q), \linebreak[0] v(R)∈\Opens_A(W)$; we
will omit the `$v$'s. If $((W,A),v)$ is a countermodel this means that
$S≠⊤$, and there is some world $α$ in $W$ in which $S_α=0$. Fix this
$α$. $S_α=0$ means $(S_P ∨ S_Q ∨ S_R)_α=0$, which means that
$(S_P)_α=0$, $(S_Q)_α=0$, and $(S_R)_α=0$. $(S_P)_α=0$ means
$(P→(Q∨R))_α=0$, which means that there is a world $β$ ahead of $α$ in
which $P_β=1$ and $(Q∨R)_β=0$, and $(Q∨R)_β=0$ means $Q_β=0$ and
$R_β=0$; similarly, $(S_Q)_α=0$ means that there is a world $γ$ ahead
of $α$ in which $Q_γ=1$, $R_γ=0$, $P_γ=0$, and $(S_R)_α=0$ means that
there is a world $δ$ ahead of $α$ in which $R_δ=1$, $P_δ=0$, $Q_δ=0$.
In diagrams:
%
%D diagram smallpyr
%D 2Dx 100 +20 +20
%D 2D 100 α
%D 2D
%D 2D +20 β γ δ
%D 2D
%D (( α β ->
%D α γ ->
%D α δ ->
%D ))
%D enddiagram
%D
%D diagram bigpyr
%D 2Dx 100 +50 +50
%D 2D 100 \mata
%D 2D
%D 2D +50 \matb \matc \matd
%D 2D
%D (( \mata \matb ->
%D \mata \matc ->
%D \mata \matd ->
%D ))
%D enddiagram
%D
$$\def\mata{\begin{array}{c}
S_α=0 \\
(S_P)_α = (P→(Q∨R))_α = 0 \\
(S_Q)_α = (Q→(R∨P))_α = 0 \\
(S_R)_α = (R→(P∨Q))_α = 0 \\
\end{array}
}
\def\matb{\begin{array}{c}
P_β=1 \\
(Q∨R)_β=0 \\
Q_β=0 \\
R_β=0 \\
\end{array}
}
\def\matc{\begin{array}{c}
Q_γ=1 \\
(R∨P)_γ=0 \\
R_γ=0 \\
P_γ=0 \\
\end{array}
}
\def\matd{\begin{array}{c}
R_δ=1 \\
(P∨Q)_δ=0 \\
P_δ=0 \\
Q_δ=0 \\
\end{array}
}
\pu
\diag{smallpyr}
\qquad
\diag{bigpyr}
$$
Note that $β$ and $γ$ are ``independent'' in the sense that in $A^*$
we can't have an arrow $β→γ$ and neither an arrow $γ→β$; we can't have
$β→γ$ because $P_β=1$ but $P_γ=0$, and we can't have $γ→β$ because
$Q_γ=1$ but $Q_β=0$. We can use a similar argument to show that $γ$
and $δ$ are independent, and to show also that $δ$ and $β$ are
independent.
{\sl We can't have three independent points in a 2-column graph,} so
we have finite DAG-countermodels for $S$ but no 2CG-countermodels for
$S$, and so no ZHA-countermodels for $S$. This means that $S$ is not
an intuitionistic tautology, but it is a ZHA-tautology. It is easy to
see that $\Taut(\IPL)⊂\Taut(\ZHAL)⊂\Taut(\CPL)$, and we saw that $S
\not∈ \Taut(\IPL)$, $S∈\Taut(\ZHAL)$, $(¬¬P→P) \not∈ \Taut(\ZHAL)$,
$(¬¬P→P) ∈ \Taut(\IPL)$, which means that:
%
$$\Taut(\IPL) \subsetneq \Taut(\ZHAL) \subsetneq \Taut(\CPL)$$
%
and so ``ZHA Logic'', {\sl which we have not defined via a deduction
system,} only by the notions of ``ZHA countermodels'' and ``ZHA
tautologies'', is strictly between Intuitionistic Logic and Classical
Logic, and is different from both.
% It may be possible to axiomatize our ``ZHA Logic'' as a ``logic of
% width 2'' using the ideas from \cite{ModalHandbook}, pp.449--450,
% but I have not attempted to do that yet.
% (find-books "__modal/__modal.el" "fitting")
% (ph1a "topologies")
% (ph1p 22 "topologies")
% We saw in sec.\ref{prop-calc} a figure that shows that $P∨Q→P∧Q$ is
% not a tautology in Classical Logic, and in sec.\ref{prop-calc-ZHA} we
% saw a figure that shows that $¬(P∧Q)→(¬P∨¬Q)$ is not a tautology in a
% certain ZHA; it reappered in sec.\ref{topologies-as-HAs}, translated
% to a topological setting. We saw very little about deductive systems
% --- only a bit in sec.\ref{logic-in-HAs}.
%
% There is an easy argument that shows that ``ZHA Logic'' lies between
% Classical Propositional Logical and Intuitionistic Propositional
% Logic, and is distinct from both. We will work on the sets of
% tautologies. Let:
% %
% %
% We will try to find a countermodel for $S$, and in the process we will
% discover that $\Taut(\IPL) \subsetneq \Taut(\ZHAL) \subsetneq
% \Taut(\CPL)$.
%
% If $E$ is a PC-expression (sec.\ref{prop-calc}) on a set $\bfV$ of
% variables --- say, $\bfV = \{P,Q,R\}$ --- then a {\sl valuation} for
% $E$ if a triple $(W,A,v)$, where $W$ is a finite set of ``worlds'',
% $A⊆W×W$ is an ``accessibility relation'' on $W$, and
% $v:\bfV→\Opens_A(W)$ is a function that assigns an open set to each
% variable in $\bfV$. Our examples will only need cases where $W$ is a
% ZSet and $A = \BPM(W)$, and this lets us use a very compact notation
% for a triple $(W,A,v)$ in which only $v$ is shown and $W$ and $A$ are
% left implicit.
% «bibliography» (to ".bibliography")
% (ph1p 36 "bibliography")
% (ph1a "bibliography")
% (find-anggfile "LATEX/" "2017planar-has-1.tex")
% (find-LATEXfile "sajl/template-sajl.tex" "\\begin{thebibliography}{10}")
% (ph1a "bibliography")
% (ph1p 36 "bibliography")
% (pha "bibliography")
% (phap 63 "bibliography")
% (find-kopkadaly4page (+ 12 310) "With \\nocite{*}, every entry")
% (find-kopkadaly4text (+ 12 310) "With \\nocite{*}, every entry")
% (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4page (+ 12 316) "14.2.3 Cross-referencing")
% (find-kopkadaly4text (+ 12 316) "14.2.3 Cross-referencing")
% % (find-kopkadaly4page (+ 12 309) "\\bibliography{database1,")
% % (find-kopkadaly4text (+ 12 309) "\\bibliography{database1,")
% \bibliography{catsem}
% %\bibliographystyle{plain}
%
% % (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% % (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")
% \bibliographystyle{alpha}
\printbibliography
\authorname{Eduardo Ochs}
\address{Departmento de Ciências da Natureza\\
Universidade Federal Fluminense (UFF)\\
Rua Recife, Lotes 1-7, Jardim Bela Vista, Rio das Ostras, RJ, CEP 28895-532, Brazil}
\email{eduardoochs@gmail.com}
% TO HERE
%L write_dnt_file()
\pu
\end{document}
% «clean-up-names» (to ".clean-up-names")
% Clean up repeated names in the .dnt:
% (find-LATEX "2017planar-has-1-body.tex")
% (find-LATEX "2017planar-has-1.dnt")
% (find-LATEXfile "2017planar-has-1.tex" 384)
% (find-LATEXfile "2017planar-has-1.dnt" "\\begin{picture}")
% (find-LATEXfile "2017planar-has-1.dnt" "mpxy")
% (find-LATEXsh "cat 2017planar-has-1.dnt | egrep '^.def' | sort")
% (find-LATEXsh "cat 2017planar-has-1.dnt | egrep '^.def' | sort | grep cell")
% (find-LATEXsh "cat 2017planar-has-1.dnt | egrep '^.def' | sort | grep -v cell")
% (find-LATEXsh "cat 2017planar-has-1.dnt | egrep '^.def' | sort | grep -v cell | grep -i house")
% (find-LATEXsh "cat 2017planar-has-1.dnt | egrep '^.def' | sort | grep -v cell | grep -i kite")
% «write-ph1-body» (to ".write-ph1-body")
% (find-LATEX "2019ilha-grande-poster-a4.tex" "write-poster-body")
% (find-LATEX "2017planar-has-1-body.tex")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
fname1 = "2017planar-has-1.tex" -- input
fname2 = "2017planar-has-1-body.tex" -- output
bigstr = ee_readfile(fname1)
smallerstr = bigstr:match("%% FROM HERE.-%% TO HERE\n")
head = "\\directlua{tf_push(\""..fname2.."\")}\n"
tail = "\\directlua{tf_pop()}\n"
= head
= tail
newbody = head..smallerstr..tail
ee_writefile(fname2, newbody)
-- (find-LATEX "2017planar-has-1-body.tex")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# laf 2017planar-has*
laf --sort=time 2017planar-has-1*
# (find-man "ls")
% Local Variables:
% coding: utf-8-unix
% ee-tla: "ph1"
% End: