|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2026planar-has-1.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2026planar-has-1.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2026planar-has-1.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2026planar-has-1.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2026planar-has-1.pdf"))
% (defun e () (interactive) (find-LATEX "2026planar-has-1.tex"))
% (defun o () (interactive) (find-LATEX "2019planar-has-1-main.tex"))
% (defun oo () (interactive) (find-LATEX "2017planar-has-1-body.tex"))
% (defun u () (interactive) (find-latex-upload-links "2026planar-has-1"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2026planar-has-1.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (defun ooe () (interactive) (find-2a '(oo) '(e)))
% (code-eec-LATEX "2026planar-has-1")
% (find-pdf-page "~/LATEX/2026planar-has-1.pdf")
% (find-sh0 "cp -v ~/LATEX/2026planar-has-1.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2026planar-has-1.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2026planar-has-1.pdf")
% file:///home/edrx/LATEX/2026planar-has-1.pdf
% file:///tmp/2026planar-has-1.pdf
% file:///tmp/pen/2026planar-has-1.pdf
% http://anggtwu.net/LATEX/2026planar-has-1.pdf
% https://anggtwu.net/LATEX/2026planar-has-1.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2 ZHA4")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2026planar-has-1" "3" "ph12026" "ph1")
% «.geometry» (to "geometry")
% «.edrx26a» (to "edrx26a")
% «.biber» (to "biber")
% «.edrx26b» (to "edrx26b")
% «.edrx26c» (to "edrx26c")
% «.2026planar-has-defs» (to "2026planar-has-defs")
% «.defs» (to "defs")
% «.footer» (to "footer")
%
% «.title» (to "title")
% «.positional» (to "positional")
%
% «.writetoc» (to "writetoc")
% «.references» (to "references")
% ;-- defs
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{amsthm} % (find-es "tex" "colorweb")
\newtheorem{theorem}{Theorem}
\newtheorem{proof}{Proof}
%\usepackage{tikz}
%
% (find-LATEX "dednat7-test1.tex")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
% «geometry» (to ".geometry")
% (find-es "tex" "geometry")
%\usepackage[a6paper, landscape,
% top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
% ]{geometry}
%
% «edrx26a» (to ".edrx26a")
\usepackage{edrx26a} % (find-LATEX "edrx26a.sty")
%
% «biber» (to ".biber")
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-ab.bib} % (find-LATEX "catsem-ab.bib")
%\addbibresource{education.bib} % (find-LATEX "education.bib")
%
\begin{document}
% «edrx26b» (to ".edrx26b")
\input edrx26b.tex % (find-LATEX "edrx26b.tex")
% «edrx26c» (to ".edrx26c")
% (find-LATEX "edrx26c.tex")
%L processsubfile "edrx26c.tex" -- runs the "%L"s
\input edrx26c % loads the defs
% «2026planar-has-defs» (to ".2026planar-has-defs")
% (find-processsubfile-links "2026planar-has-defs")
% (find-LATEX "2026planar-has-defs.tex")
%L processsubfile "2026planar-has-defs.tex" -- runs the "%L"s
\input 2026planar-has-defs % loads the defs
\pu
%L require "ZHA4" -- (find-angg "LUA/ZHA4.lua")
%L require "underbrace2d" -- (find-dn6 "underbrace2d.lua")
%L require "luarects" -- (find-dn6 "luarects.lua")
\pu
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
\def\comp {\operatorname{comp}}
% «footer» (to ".footer")
% (find-LATEX "edrxheadfoot.tex")
\def\drafturl{http://anggtwu.net/LATEX/2026-1-C3.pdf}
\def\drafturl{http://anggtwu.net/2026.1-C3.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}
\def\catX{{\mathbf{X}}}
\def\catY{{\mathbf{Y}}}
\def\resizediag#1#2#3{\resizebox{#1}{#2}{$\diag{#3}$}}
\def\eqQ{\sim_Q}
% ;-- title
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (ph12026p 1 "title")
% (ph12026a "title")
% «positional» (to ".positional")
% (ph12026a "positional")
% (find-LATEX "2017planar-has-1-body.tex" "positional" "dagKite")
% Done:
% (find-LATEX "2017planar-has-1-body.tex" "positional")
% (find-LATEX "2017planar-has-1-body.tex" "positional" "adef")
% (find-LATEX "edrx26c.tex" "picturedots" "adef")
\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}
$$\picturedots (0,0)(2,3){ 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 }
$$
% Not yet:
% (find-LATEX "2017planar-has-1-body.tex" "positional" "dagKite")
%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
% (find-fline "~/LATEX/2017planar-has-1.dnt")
% (find-fline "~/LATEX/2017planar-has-1.dnt" "\\def\\dagKite")
% (find-LATEX "2017planar-has-defs.tex" "picturedotsdef")
% (find-LATEX "2026defs-comprehensions.tex" "picturedots")
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")
\section{ZDAGs}
\label {ZDAGs}
% (ph1p 6 "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")
% (ph1 "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} -- old
%R local x = {L=4, R=7, a=10, b=12} -- new
%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")
% (ph1 "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")
\section{Propositional calculus}
\label {prop-calc}
% (ph1p 10 "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")
\section{Propositional calculus in a ZHA}
\label {prop-calc-ZHA}
% (ph1p 11 "prop-calc-ZHA")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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")
\section{Topologies}
\label {topologies}
% (ph1p 23 "topologies")
% (ph1 "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")
% (ph1 "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 25 "topologies-as-partial-orders")
% (ph1 "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 27 "2CGs")
% (ph1 "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")
% (ph1 "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 31 "topologies-as-HAs")
% (ph1 "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 32 "converting-ZHAs-2CAGs")
% (ph1 "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")
% (ph1 "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")
% (ph1 "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.
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2026planar-has-1")
% (find-build-for-arxiv-links "2026planar-has-1")
% Local Variables:
% coding: utf-8-unix
% outline-regexp: "% +;--"
% ee-tla: "ph1"
% ee-tla: "ph12026"
% End: