|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017ebl-slides.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017ebl-slides.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017ebl-slides.pdf"))
% (defun e () (interactive) (find-LATEX "2017ebl-slides.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017ebl-slides"))
% (find-xpdfpage "~/LATEX/2017ebl-slides.pdf")
% (find-sh0 "cp -v ~/LATEX/2017ebl-slides.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017ebl-slides.pdf /tmp/pen/")
% (find-sh0 "cp -v ~/LATEX/2017ebl-slides.pdf /tmp/pen/EBL2017-ochs.pdf")
% file:///home/edrx/LATEX/2017ebl-slides.pdf
% file:///tmp/2017ebl-slides.pdf
% file:///tmp/pen/2017ebl-slides.pdf
% http://angg.twu.net/LATEX/2017ebl-slides.pdf
% (find-fline "~/.emacs" "\"ebs\"")
% (defun geta (str) (string-match "«\\(.*\\)»" str) (match-string 1 str))
% (defun getb () (geta (ee-no-properties (buffer-substring (ee-bol) (ee-eol)))))
% (defun getc () (format "\n%% (ebsp 0 \"%s\")" (getb)))
% (defun getd () (interactive) (insert (getc)))
% (setq last-kbd-macro (kbd "C-e <<getd>>"))
% (find-LATEXsh "grep ebsp 2017ebl-slides.tex")
% «.dednat6-extensions» (to "dednat6-extensions")
% «.colors» (to "colors")
%
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.bullet-diags-as-DAGs» (to "bullet-diags-as-DAGs")
% «.BPM-and-WPM» (to "BPM-and-WPM")
% «.bullet-diags-as-sets» (to "bullet-diags-as-sets")
% «.LR-coords» (to "LR-coords")
% «.hLR» (to "hLR")
% «.hLR-2» (to "hLR-2")
% «.hLR-3» (to "hLR-3")
% «.HAs» (to "HAs")
% «.two-HAs» (to "two-HAs")
% «.non-tautologies» (to "non-tautologies")
% «.logic-in-a-ZHA» (to "logic-in-a-ZHA")
% «.logic-in-a-ZHA-2» (to "logic-in-a-ZHA-2")
% «.the-big-picture» (to "the-big-picture")
% «.J-operators» (to "J-operators")
% «.lindenbaum» (to "lindenbaum")
% «.lindenbaum-2» (to "lindenbaum-2")
% «.valuations» (to "valuations")
% «.archetypal» (to "archetypal")
% «.typical-questions» (to "typical-questions")
% «.lambda-notation» (to "lambda-notation")
% «.positional» (to "positional")
% «.ZHA-logic-quick» (to "ZHA-logic-quick")
\documentclass[oneside]{article}
\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{edrx15} % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=15cm, paperheight=12.4cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% \catcode`\^^J=10
% \directlua{dednat6dir = "dednat6/"}
% \directlua{dofile(dednat6dir.."dednat6.lua")}
% \directlua{texfile(tex.jobname)}
% \directlua{verbose()}
% \directlua{output(preamble1)}
% \def\expr#1{\directlua{output(tostring(#1))}}
% \def\eval#1{\directlua{#1}}
% \def\pu{\directlua{pu()}}
\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
% «dednat6-extensions» (to ".dednat6-extensions")
%L -- (find-dn6 "picture.lua" "V")
%L -- (find-dn6 "picture.lua" "V" " lr = ")
%L V.__index.anglr = function (v)
%L local l, r = v:to_l_r()
%L return "\\ang{"..l..","..r.."}"
%L end
%L
%L -- (find-dn6file "luarects.lua")
%L -- (find-dn6file "luarects.lua" "tozmp =")
%L AsciiRect.__index.tolrmp = function (ar, opts)
%L return MixedPicture.new(opts, nil, nil, ar:setx0())
%L end
%L
%L -- (find-dn6 "newrect.lua" "MixedPicture")
%L -- (find-dn6 "newrect.lua" "MixedPicture" "addlrs =")
%L MixedPicture.__index.addarxys = function (mp)
%L for v,str in mp.ar:points() do mp:put(v, v:xy()) end
%L return mp
%L end
%L MixedPicture.__index.addaranglrs = function (mp)
%L for v,str in mp.ar:points() do mp:put(v, v:anglr()) end
%L return mp
%L end
%L MixedPicture.__index.addarlrs = function (mp)
%L for v,str in mp.ar:points() do mp:put(v, v:lr()) end
%L return mp
%L end
%L MixedPicture.__index.addarbullets = function (mp)
%L for v,str in mp.ar:points() do mp:put(v, "\\bullet") end
%L return mp
%L end
\def\Vec#1{\overrightarrow{#1}}
\def\VEC#1{{\overrightarrow{(#1)}}}
\def\red#1{{\color{red}#1}}
\def\mysection#1{{\bf #1}\msk}
% «colors» (to ".colors")
% (find-es "tex" "colorweb")
\long\def\ColorRed #1{{\color{Red}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\setlength{\parindent}{0em}
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «picturedots» (to ".picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "comprehension-gab")
% (gaap 5)
%
\def\beginpicture(#1,#2)(#3,#4){\expr{beginpicture(v(#1,#2),v(#3,#4))}}
\def\pictaxes{\expr{pictaxes()}}
\def\pictdots#1{\expr{pictdots("#1")}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\picturedots(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
%\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\sa{\rightsquigarrow}
\def\BPM{\mathsf{BPM}}
\def\WPM{\mathsf{WPM}}
\def\ZHAG{\mathsf{ZHAG}}
\def\catTwo{\mathbf{2}}
%\def\Pts{\mathcal{P}}
\def\calS{\mathcal{S}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\subst#1{\left[\begin{array}{rcl}#1\end{array}\right]}
\def\subst{\bsm}
% (find-LATEXfile "2015planar-has.tex" "\\def\\Mop")
\def\MP{\mathsf{MP}}
\def\J {\mathsf{J}}
\def\Mo {\mathsf{Mo}}
\def\Mop {\mathsf{Mop}}
\def\Sand{\mathsf{Sand}}
\def\ECa {\mathsf{EC}{\&}}
\def\ECv {\mathsf{EC}{∨}}
\def\ECS {\mathsf{ECS}}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\Int{{\operatorname{int}}}
%
\def\NoLcuts{\mathsf{No}λ\mathsf{cuts}}
\def\NoYcuts{\mathsf{NoYcuts}}
\def\astarcube{{\&}^*\mathsf{Cube}}
\def\ostarcube{{∨}^*\mathsf{Cube}}
\def\istarcube{{→}^*\mathsf{Cube}}
\def\acz{{\&}^*\mathsf{C}_0}
\def\ocz{{∨}^*\mathsf{C}_0}
\def\icz{{→}^*\mathsf{C}_0}
%
\def\astarcuben{{\&}^*\mathsf{Cube}_\mathsf{n}}
\def\ostarcuben{{∨}^*\mathsf{Cube}_\mathsf{n}}
\def\istarcuben{{→}^*\mathsf{Cube}_\mathsf{n}}
\def\astarcubev{{\&}^*\mathsf{Cube}_\mathsf{v}}
\def\ostarcubev{{∨}^*\mathsf{Cube}_\mathsf{v}}
\def\istarcubev{{→}^*\mathsf{Cube}_\mathsf{v}}
%
%\catcode`∧=13 \def∧{\mathop{\&}}
\def\biggest {\mathsf{biggest}}
\def\smallest{\mathsf{smallest}}
\def\Cuts {\mathsf{Cuts}}
\def\LR{\mathbb{LR}}
\def\IPL{\text{IPL}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (ebsp 1 "title")
{\footnotesize Title of this talk:}
\ssk
\par {\bf Intuitionistic Propositional Logic
\par For \ColorGreen{Children} and Meta-Children, or:
\par How Archetypal Are
\par Finite Planar Heyting Algebras?}
\msk
\par EBL2017 - Pirenópolis, may 2017
\par Eduardo Ochs, UFF (Rio das Ostras, RJ)
\par \url{http://angg.twu.net/math-b.html\#ebl-2017}
\par \url{http://angg.twu.net/LATEX/2017planar-has.pdf} (paper)
\bsk
% \bsk
{\footnotesize Some quotes:}
\ssk
One great way to make the expression ``for children'' precise in
mathematical titles is to {\sl define} ``\ColorGreen{children}'' as
``people without mathematical maturity'', in the sense that they are
not able to understand structures that are too abstract straight away
--- \ColorGreen{\sl they need particular cases first.}
\msk
``Meta-children'' are people who want to study the relation between
mathematics ``for children'' and ``for adults'' and produce
(meta)mathematics for adults from that.
\msk
ZHAs [i.e., finite, planar HAs] help us visualize fragments of the
Lindenbaum Algebra of HAs.
\newpage
% «abstract» (to ".abstract")
% \mysection{...from the abstract:}
%
% {
% \setlength{\parindent}{2em}
%
% I've been using the expression ``for children'' in titles for some
% years, and with time it acquired a precise, though unusual, sense.
% ``Children'' are ``people without mathematical maturity'', where these
% are the main aspects of mathematical maturity: ableness to 1) handle
% abstract mathematical structures and 2) infinite objects; 3) work
% axiomatically, 4) generalize, and 5) particularize.
%
% % Some techniques for creating versions ``for children'' of maths
% % ``for adults'' are described in [1]; the main one is doing two
% % parallel diagrams, one for the general case and another one for a
% % particular, hopefully ``archetypal'' case.
%
% Finite, planar Heyting Algebras (``ZHA''s) are very good tools for
% teaching Intuitionistic Propositional Logic (IPL) to children: most
% non-theorems of IPL have countermodels on ZHAs that are very easy to
% understand visually, and children prefer to understand tautologies and
% non-tautologies first, and deductive systems later.
%
% ZHAs are archetypal among Heyting Algebras, but in a sense of
% ``archetypal'' that fits only the loosest definitions in (...)
%
% ``Meta-children'' are people who want to study the relation between
% mathematics ``for children'' and ``for adults'' and produce
% (meta)mathematics for adults from that. The presentation will be
% mostly about teaching ZHAs and closure operators to ``children'', with
% one result for meta-children in the end: that this new sense of
% archetypalness can be formalized using comparisons of partial orders (...)
%
% }
%
% \msk
% \msk
%
% I've tested a part of this on real ``children'': a group of 6 CS
% students that had finished a course on Discrete Mathematics, most of
% them not very brilliantly ---
%
% \newpage
% _ _ _ _ __ ____ _ ____
% | |__ _ _| | | ___| |_ ___ \ \ | _ \ / \ / ___|___
% | '_ \| | | | | |/ _ \ __/ __| _____\ \ | | | |/ _ \| | _/ __|
% | |_) | |_| | | | __/ |_\__ \ |_____/ / | |_| / ___ \ |_| \__ \
% |_.__/ \__,_|_|_|\___|\__|___/ /_/ |____/_/ \_\____|___/
%
% «bullet-diags-as-DAGs» (to ".bullet-diags-as-DAGs")
% (ebsp 2 "bullet-diags-as-DAGs")
\mysection{Bullet diagrams as directed graphs}
% (phap 2 "ZDAGs")
% (pha "ZDAGs")
Sometimes we want arrows going up,
sometimes we want arrows going down.
%R local K, H =
%R 1/ o \, 1/ o \
%R |o o| |o o|
%R | o | \o o/
%R \ o /
%R K:tomp({def="Kmini", scale="4pt", meta="s"}):addbullets() :output()
%R H:tomp({def="Hmini", scale="4pt", meta="s"}):addbullets() :output()
%R K:tomp({def="KB", scale="18pt", meta=nil}):addbullets():addarrows(nil):output()
%R H:tomp({def="HW", scale="18pt", meta=nil}):addbullets():addarrows("w"):output()
%R K:tomp({def="Kb", scale="7pt", meta=nil}):addbullets() :output()
%R H:tomp({def="Hb", scale="7pt", meta=nil}):addbullets() :output()
%R K:tomp({def="Kn", scale="20pt", meta=nil}):addxys ():addarrows(nil):output()
%
\pu
$$%\pu
K \;\; = \;\; \Kb
\quad\diagxyto/-->/<450>^{\sm{\text{add black} \\ \text{pawns moves}}}
%\;\;\;\;\text{will stand for:}\;\;
\KB = (K, \BPM(K))
% =
% \Kn =
$$
$$\qquad
\qquad
\qquad
\qquad
=
\pmat{
\csm{ & (1,3), & \\
(0,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)) \\
}
}
$$
\bsk
$$%\pu
H \;\; = \;\; \Hb
\quad\diagxyto/-->/<450>^{\sm{\text{add white} \\ \text{pawns moves}}}
%\;\;\;\;\text{will stand for:}\;\;
\HW = (H, \WPM(H))
$$
\newpage
% ____ ____ __ __ ___ __ ______ __ __
% | __ )| _ \| \/ | ( _ ) \ \ / / _ \| \/ |
% | _ \| |_) | |\/| | / _ \/\ \ \ /\ / /| |_) | |\/| |
% | |_) | __/| | | | | (_> < \ V V / | __/| | | |
% |____/|_| |_| |_| \___/\/ \_/\_/ |_| |_| |_|
%
% «BPM-and-WPM» (to ".BPM-and-WPM")
% (ebsp 3 "BPM-and-WPM")
\mysection{Black and white pawns moves}
Mnemonic:
a game with black pawns and white pawns
black pawns are solid/heavy/sink/go down
white pawns are hollow/light/float/go up
%R local G = 2/bp bp bp bp bp bp\
%R | |
%R |bp bp bp bp bp bp|
%R | swsose |
%R |. . . . . . |
%R | |
%R |. . . . . . |
%R | nwnone |
%R |wp wp wp wp wp wp|
%R | |
%R \wp wp wp wp wp wp/
%R
%R local T = {bp="\\bullet", wp="\\circ",
%R sw="↙", so="↓", se="↘",
%R nw="↖", no="↑", ne="↗"}
%R G:tozmp({def="Gmne", scale="8pt", meta=nil}):addcells(T):output()
$$\pu \Gmne
$$
\msk
$((a,b),(c,d)) ∈ \BPM(S)$ means $(a,b),(c,d)∈S$ and
$(a,b)→(c,d)$ is a black pawn move
\msk
$((a,b),(c,d)) ∈ \WPM(S)$ means $(a,b),(c,d)∈S$ and
$(a,b)→(c,d)$ is a white pawn move
\newpage
% _ ____ _
% | | | _ \ ___ ___ ___ _ __ __| |___
% | | | |_) | / __/ _ \ / _ \| '__/ _` / __|
% | |___| _ < | (_| (_) | (_) | | | (_| \__ \
% |_____|_| \_\ \___\___/ \___/|_| \__,_|___/
%
% «LR-coords» (to ".LR-coords")
% (ebsp 4 "LR-coords")
\mysection{LR-coordinates}
\par $\N^2⊂\Z^2$ is a quarter-plane.
\par $\LR⊂\Z^2$ is a ``quarter-plane turned $45°$ to the left''.
\par $\LR = \setofst{\ang{l,r}}{l,r∈\N}$
\msk
\par LR-coordinates:
\par $lr = \ang{l,r} = (0,0) + l\und{\VEC{-1,1}}{\nwarrow} + r\und{\VEC{1,1}}{\nearrow}$
\bsk
\par The lower part of $\LR$,
\par in LR-coordinates and xy-coordinates:
%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 zhav:tolrmp({def="zxy", scale="13pt", meta="s"}):addarxys():output()
%R zhav:tolrmp({def="zlr", scale="13pt", meta="s"}):addarlrs():output()
$$\pu
\zlr
\quad =
\quad
\zxy
$$
% (phap 3 "LR-coords")
% (pha "LR-coords")
\newpage
% _ _ _ _ __ _
% | |__ _ _| | | ___| |_ ___ \ \ ___ ___| |_ ___
% | '_ \| | | | | |/ _ \ __/ __| _____\ \ / __|/ _ \ __/ __|
% | |_) | |_| | | | __/ |_\__ \ |_____/ / \__ \ __/ |_\__ \
% |_.__/ \__,_|_|_|\___|\__|___/ /_/ |___/\___|\__|___/
%
% «bullet-diags-as-sets» (to ".bullet-diags-as-sets")
% (ebsp 5 "bullet-diags-as-sets")
\mysection{Bullet diagrams as subsets of $\Z^2$}
Two cases:
\par For a finite, non-empty $S∈\Z^2$,
\msk
\par $S$ is a ZSet iff $S⊂\N^2$ and
\par $S$ touches the $xy$-axes
\msk
\par $S$ is an LRSet iff $S⊂\LR$ and $S$
\par touches the $lr$-axes
\par {\sl at the point (0,0)}
%R local zset, lrset =
%R 1/ o \, 1/ o \
%R |o o| | o o |
%R | o | |o o |
%R \ o / | o o|
%R |o o o |
%R | o o |
%R \ o /
%R zset:tomp({def="zsetb", scale="6pt" }):addbullets():output()
%R zset:tomp({def="zsetxy", scale="13pt", meta="s"}):addarxys():output()
%R lrset:tolrmp({def="lrsetb", scale="4.5pt" }):addbullets():output()
%R lrset:tolrmp({def="lrsetxy", scale="12pt", meta="s"}):addarxys():output()
%R lrset:tolrmp({def="lrsetlr", scale="8pt", meta="s"}):addarlrs():output()
\pu
A ZSet: $\quad\qquad \zsetb \quad = \quad \zsetxy $
\msk
An LRSet: $\qquad \lrsetb \quad = \quad \lrsetxy \quad = \quad \lrsetlr $
\newpage
% ___ _ ______
% / / |__ | | | _ \ \
% | || '_ \ | | | |_) | |
% | || | | |_ | |___ _ | _ <| |
% | ||_| |_( ) |_____( ) |_| \_\ |
% \_\ |/ |/ /_/
%
% «hLR» (to ".hLR")
% (ebsp 6 "hLR")
\mysection{$(h,L,R)$: height, left wall, right wall}
ZHAs (planar Heyting Algebras) are LRSets obeying extra conditions...
A ZHA is ``everything between a left wall and a right wall'' ---
The left wall has one point for each $y$
The left wall is made of points of the form $(L(y),y)$ \quad (same for ``right'')
\msk
% (phap 4 "ZHAs")
% (pha "ZHAs")
% (pha "ZHAs" "zhav =")
%
% (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="20pt", meta=nil}):addxys():addarrows("w")
%R mp = zhav:tozmp({def="zhav", scale="14pt", meta="s"}):addxys()
%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=14}
%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()
%R
%R mp = zhav:tozmp({def="zhab", scale="4pt"}):addbullets():output()
%
\pu
$
\qquad
\zhab
%
\qquad\quad
\diagxyto/<-->/<350>
\qquad
\zhav
$
\msk
Top point: $(-3,9)$
Height: 9
$h=9$, \; $L:\{0,\ldots,9\}→\Z$, \; $R:\{0,\ldots,9\}→\Z$,
The ZHA is everything \ColorRed{in $\LR$} between the left and the right wall
\newpage
% ___ _ ______ ____
% / / |__ | | | _ \ \ |___ \
% | || '_ \ | | | |_) | | __) |
% | || | | |_ | |___ _ | _ <| | / __/
% | ||_| |_( ) |_____( ) |_| \_\ | |_____|
% \_\ |/ |/ /_/
%
% «hLR-2» (to ".hLR-2")
% (ebsp 7 "hLR-2")
\mysection{$(h,L,R)$: height, left wall, right wall (2)}
Numbers, sets and lists feel very concrete to ``children'', so:
\bsk
$\qquad
(h,L,R) =
\pmat{9,
\csm{(9,-3), \\ (8,-4), \\ (7,-3), \\ (6,-2), \\ (5,-1), \\ (4,-2), \\ (3,-3), \\ (2,-2), \\ (1,-1), \\ (0,0) },
\csm{(9,-3), \\ (8,-2), \\ (7,-3), \\ (6,-2), \\ (5,-1), \\ (4,0), \\ (3,1), \\ (2,0), \\ (1,1), \\ (0,0) }
}
\quad
\diagxyto/-->/<350>^{\text{generates}}
\quad
\zhab
$
\newpage
% ___ _ ______ _____
% / / |__ | | | _ \ \ |___ /
% | || '_ \ | | | |_) | | |_ \
% | || | | |_ | |___ _ | _ <| | ___) |
% | ||_| |_( ) |_____( ) |_| \_\ | |____/
% \_\ |/ |/ /_/
%
% «hLR-3» (to ".hLR-3")
% (ebsp 8 "hLR-3")
\mysection{$(h,L,R)$: height, left wall, right wall (3)}
\ssk
% (phap 4 "ZHAs")
A triple $(h,L,R)$ is a height-left-right-wall (``HLRW'') iff:
\par 1) $h∈\N$
\par 2) $L: \{0,\ldots,h\} → \Z$
\par 3) $R: \{0,\ldots,h\} → \Z$
\par 4) $L(y+1)=L(y)±1$ always
\par 5) $R(y+1)=R(y)±1$ always
\par 6) $L(0)=R(0)=0$
\par 7) $L(y)≤R(y)$ always
\par 8) $L(h)=R(h)$
\msk
The ZHA generated by $(h,L,R)$ is:
\par $\ZHAG(h,L,R) =$
\par \quad $\setofst {(x,y) \, \ColorRed{∈\LR} } {y≤h, L(y)≤x≤R(y)}$
\msk
Formal definition of a ZHA:
\ssk
\fbox{
\begin{tabular}{l}
A {\sl ZHA} is a set of the form $\ZHAG(h,L,R)$, \\
\par for some HLRW $(h,L,R)$.
\end{tabular}
}
\ssk (Theorem: every ZHA is a Heyting Algebra)
\newpage
% _ _ _
% | | | | / \ ___
% | |_| | / _ \ / __|
% | _ |/ ___ \\__ \
% |_| |_/_/ \_\___/
%
% «HAs» (to ".HAs")
% (ebsp 9 "HAs")
\mysection{Heyting Algebras}
% (phap 8 "HAs")
% (pha "HAs")
A Heyting Algebra (a ``HA'') is a structure
\msk
$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H)$
\msk
in which:
1) $Ω$ is a set (the ``set of truth values'')
2) $≤_H$ is a (strict) partial order on $Ω$
3) $⊤_H$ is the top element
4) $⊥_H$ is the bottom element
5) $(P ≤_H (Q \red{∧_H} R)) ↔ ((P ≤_H Q) ∧ (P ≤_H R))$
6) $((P \red{∨_H} Q) ≤_H R) ↔ ((P ≤_H R) ∧ (Q ≤_H R))$
7) $(P ≤_H (Q \red{→_H} R)) ↔ ((P ∧_H Q) ≤_H R)$
\msk
Sometimes we add operations `$¬$' and $↔$ to a HA $H$:
\msk
$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H,¬_H,↔_H)$
\msk
where:
8) $\;\;\;\;\;\; ¬_H P \;\; := \;\; P →_H ⊥_H$
9) $P ↔_H Q \;\; := \;\; (P →_H Q)∧_H(Q →_H P)$
\newpage
% _____ _ _ _
% |_ _|_ _____ | | | | / \ ___
% | | \ \ /\ / / _ \ | |_| | / _ \ / __|
% | | \ V V / (_) | | _ |/ ___ \\__ \
% |_| \_/\_/ \___/ |_| |_/_/ \_\___/
%
% «two-HAs» (to ".two-HAs")
% (ebsp 10 "two-HAs")
\mysection{Two Heyting Algebras}
Numbers, sets and lists feel very concrete to ``children'', so...
{
\def\p#1{\phantom{#1}}
\def\L{\mathsf{L}}
\def\CL{\mathsf{CL}}
\def\TL{\mathsf{L}_3}
\def\ul{_{\L}}
\def\ucl{_{\CL}}
\def\utl{_{\TL}}
\def\fo #1 #2 #3 {((#1,#2),#3)}
\def\ba #1 #2 #3 #4 {
\foo 0 0 #1 , \\
\foo 0 1 #2 , \\
\foo 1 0 #3 , \\
\foo 1 1 #4 \p, \\
}
\def\foc#1 #2 {(#1,#2)}
\def\co #1 #2 {
\fooc 0 #1 ,\\
\fooc 1 #2 \p,\\
}
\def\com {0,\\ 1\p,\\}
\def\cand{\ba 0 0 0 1 }
\def\cor {\ba 0 1 1 1 }
\def\cimp{\ba 1 1 0 1 }
\def\ciff{\ba 1 0 0 1 }
\def\cnot{\co 1 0 }
\def\foo#1 #2 #3 {((#1,#2),#3)}
\def\bar#1 #2 #3 #4 #5 #6 #7 #8 #9 {
\foo 00 00 #1 , \\
\foo 00 01 #2 , \\
\foo 00 11 #3 , \\
\foo 01 00 #4 , \\
\foo 01 01 #5 , \\
\foo 01 11 #6 , \\
\foo 11 00 #7 , \\
\foo 11 01 #8 , \\
\foo 11 11 #9 \p, \\
}
\def\fooc #1 #2 {(#1,#2)}
\def\col#1 #2 #3 {
\fooc 00 #1 ,\\
\fooc 01 #2 ,\\
\fooc 11 #3 \p,\\
}
\def\tom {00,\\ 01,\\ 11\p,\\}
\def\tand{\bar 00 00 00 00 01 01 00 01 11 }
\def\tor {\bar 00 01 11 01 01 11 11 11 11 }
\def\timp{\bar 11 11 11 00 11 11 00 01 11 }
\def\tiff{\bar 11 00 00 00 11 01 00 01 11 }
\def\tnot{\col 11 00 00 }
Classical logic:
\msk
$\CL = (Ω\ucl, ⊤\ucl, ⊥\ucl, ∧\ucl, ∨\ucl, →\ucl, ↔\ucl, ¬\ucl) =$
$\psm{\csm{\com}, 1, 0, \csm{\cand}, \csm{\cor}, \csm{\cimp}, \csm{\ciff}, \csm{\cnot}}$
\bsk
A 3-valued logic:
\msk
$\TL = (Ω\utl, ⊤\utl, ⊥\utl, ∧\utl, ∨\utl, →\utl, ↔\utl, ¬\utl) =$
$\psm{\csm{\tom}, 11, 00, \csm{\tand}, \csm{\tor}, \csm{\timp}, \csm{\tiff}, \csm{\tnot}}$
\bsk
Children like to calculate things, more than to prove things ---
$(¬¬P)→P$ is a tautology in $\CL$ \qquad \ColorViolet{(for $P=0$ and $P=1$ the result is $⊤$)}
$(¬¬P)→P$ is not a tautology in $\TL$ \; (for $P=01$ the result is not $⊤$)
But {\sl why}? How do we remember those tables? How do we visualize all that?
}
\newpage
% _ _ _ _ _ _
% | \ | | ___ _ __ | |_ __ _ _ _| |_ ___ | | ___ __ _(_) ___ ___
% | \| |/ _ \| '_ \ _____| __/ _` | | | | __/ _ \| |/ _ \ / _` | |/ _ \/ __|
% | |\ | (_) | | | |_____| || (_| | |_| | || (_) | | (_) | (_| | | __/\__ \
% |_| \_|\___/|_| |_| \__\__,_|\__,_|\__\___/|_|\___/ \__, |_|\___||___/
% |___/
% «non-tautologies» (to ".non-tautologies")
% (ebsp 11 "non-tautologies")
% (ebh "NonTaut")
\mysection{From the handouts: two non-tautologies \rm (for children)}
%L mpa = mpnew({def="fooa", scale="7pt", meta="s"}, "12321L")
%L mpb = mpnew({def="foob", scale="7pt", meta="s"}, "12321L"):addcuts("c")
%L mpa = mpnew({def="fooa"}, "12321L")
%L mpb = mpnew({def="foob"}, "12321L"):addcuts("c")
%L mpa:addlrs():output()
%L mpb:put(v"10", "P")
%L mpb:put(v"01", "Q")
%L mpb:output()
%R local znotnotP =
%R 1/ T \
%R | . |
%R | . c |
%R |b . a|
%R | P . |
%R \ F /
%R local T = {F="⊥", T="⊤", a="P'", b="P''", c="→"}
%R znotnotP:tozmp({def="znotnotP", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R local zdemorgan =
%R 1/ T \
%R | o |
%R | . . |
%R |q . p|
%R | P Q |
%R \ a /
%R local T = {F="⊥", T="⊤", p="P'", q="Q'", a="∧", o="∨"}
%R zdemorgan:tozmp({def="zdemorgan", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse", scale="10pt", meta=nil}):addlrs():output()
%
%L -- ¬¬P→P
%L ubs [[
%L ¬ ¬ P 10 u Pre 02 u Pre 20 u () → P 10 u Bin 12 u
%L notnotP def output
%L ]]
%L
%L -- ¬(P∧Q)→(¬P∨¬Q)
%L ubs [[
%L ¬ P 10 u ∧ Q 01 u Bin 00 u () Pre 32 u
%L → ¬ P 10 u Pre 02 u ∨ ¬ Q 01 u Pre 20 u Bin 22 u () Bin 22 u
%L demorgan def output
%L ]]
In the ZHA $H$, with the valuation $v$, we have:
\msk
\pu
$\begin{array}{c}
H=\fooa \\ \\
v=\foob \\
\end{array}
\qquad
\begin{array}{ccccl}
\znotnotP && \mat{\notnotP} \\ \\
\zdemorgan && \mat{\demorgan} \\
\end{array}
$
\msk
...these two classical tautologies are not ${=}⊤$ $({=}32)$ in $v$,
so they are not true in all Heyting Algebras,
and they can't be theorems of intuitionistic logic...
\msk
Intuitionistic logic (IPL) has fewer tautologies the classical logic (CPL).
How can we prove that something holds in all ZHAs (or in all HAs)?
{\sl This motivates rewriting the axioms of a HA into tree rules ---}
\newpage
% _ _ _ ______ _ _
% | | ___ __ _(_) ___ (_)_ __ __ _ |__ / | | | / \
% | | / _ \ / _` | |/ __| | | '_ \ / _` | / /| |_| | / _ \
% | |__| (_) | (_| | | (__ | | | | | | (_| | / /_| _ |/ ___ \
% |_____\___/ \__, |_|\___| |_|_| |_| \__,_| /____|_| |_/_/ \_\
% |___/
%
% «logic-in-a-ZHA» (to ".logic-in-a-ZHA")
% (ebsp 12 "logic-in-a-ZHA")
\mysection{Logic in a ZHA: computing $⊤,⊥,∧,∨,→$}
Every ZHA (a subset of $\Z^2$) ``is'' a HA (a 7-uple)... \qquad\qquad\qquad \ColorViolet{$←$ magic}
Trick: a ZHA can be extended {\sl canonically} to a structure
\msk
$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_C)$
\msk
where
1) $Ω$ is the set of points of the ZHA (``set of truth-values'')
2) $ab ≤_H cd$ iff $a≤c$ and $b≤d$
3) $⊤_H$ is the top element
4) $⊥_H$ is the bottom element (i.e., 00)
5) $ab ∧_H cd = \min(a,c)\min(b,d)$
6) $ab ∨_H cd = \max(a,c)\max(b,d)$
7) $→_C$ is the ``(quickly) computable implication'':
\msk
\def\s{\mathsf}
$Q→_CR
\;:=\;
\left(\!\!
\begin{array}{lcll}
\s{if} & Q \s{b} R & \s{then} & ⊤ \\
\s{elseif} & Q \s{l} R & \s{then} & \s{ne}(R) \\
\s{elseif} & Q \s{r} R & \s{then} & \s{nw}(R) \\
\s{elseif} & Q \s{a} R & \s{then} & R \\
\s{end} \\
\end{array}
\!\!\!\right)
%
\;=\;
%
\left(\!\!
\begin{array}{lcll}
\s{if} & Q \s{b}' R & \s{then} & ⊤ \\
\s{elseif} & Q \s{l}' R & \s{then} & \s{ne}(R) \\
\s{elseif} & Q \s{r}' R & \s{then} & \s{nw}(R) \\
\s{elseif} & Q \s{a}' R & \s{then} & R \\
\s{end} \\
\end{array}
\!\!\!\right)
$
\msk
where $\s{b}$, $\s{l}$, $\s{r}$, $\s{a}$ abbreviate
$\s{below}$, $\s{leftof}$, $\s{rightof}$, $\s{above}$
and $\s{b}'$, $\s{l}'$, $\s{r}'$, $\s{a}'$ are...
\newpage
% _ _ _ ______ _ _ ____
% | | ___ __ _(_) ___ (_)_ __ __ _ |__ / | | | / \ |___ \
% | | / _ \ / _` | |/ __| | | '_ \ / _` | / /| |_| | / _ \ __) |
% | |__| (_) | (_| | | (__ | | | | | | (_| | / /_| _ |/ ___ \ / __/
% |_____\___/ \__, |_|\___| |_|_| |_| \__,_| /____|_| |_/_/ \_\ |_____|
% |___/
%
% «logic-in-a-ZHA-2» (to ".logic-in-a-ZHA-2")
% (ebsp 13 "logic-in-a-ZHA-2")
\mysection{Logic in a ZHA: computing $⊤,⊥,∧,∨,→$ (2)}
...and $\s{b}'$, $\s{l}'$, $\s{r}'$, $\s{a}'$ are variants of
$\s{below}$, $\s{leftof}$, $\s{rightof}$, $\s{above}$
that divide the ZHA into four disjoint regions:
%L mp = mpnew({def="impCube", scale="7pt", meta="s"}, "12345654321"):addcuts("c 543/210 012|345")
%L mp:put(v"22", "R")
%L mp:put(v"44", "Q\\s{a}'R")
%L mp:put(v"11", "Q\\s{b}'R")
%L mp:put(v"41", "Q\\s{l}'R")
%L mp:put(v"14", "Q\\s{r}'R")
%L mp:output()
$$\pu\impCube$$
We have:
\msk
$P ≤_H
{% \tiny
\left(\!\!
\begin{array}{lcll}
\s{if} & Q \s{b}' R & \s{then} & ⊤ \\
\s{elseif} & Q \s{l}' R & \s{then} & \s{ne}(R) \\
\s{elseif} & Q \s{r}' R & \s{then} & \s{nw}(R) \\
\s{elseif} & Q \s{a}' R & \s{then} & R \\
\s{end} \\
\end{array}
\!\!\!\right)
}
\qquad
\text{iff}
\qquad
{% \tiny
\left(\!\!
\begin{array}{lcll}
Q \s{b}' R & → & P ≤_H ⊤ \\
Q \s{l}' R & → & P ≤_H \s{ne}(R) \\
Q \s{r}' R & → & P ≤_H \s{nw}(R) \\
Q \s{a}' R & → & P ≤_H R \\
\end{array}
\!\!\!\right)
}
$
\msk
The proof is tedious but easy, and it shows that $Q →_C R$ obeys:
\ssk
$(P ≤_H (Q \red{→_C} R)) ↔ ((P ∧_H Q) ≤_H R)$
\ssk
and so $(Q →_C R) = (Q →_H R)$.
\newpage
% ____ _ _ _
% | __ )(_) __ _ _ __ (_) ___| |_ _ _ _ __ ___
% | _ \| |/ _` | | '_ \| |/ __| __| | | | '__/ _ \
% | |_) | | (_| | | |_) | | (__| |_| |_| | | | __/
% |____/|_|\__, | | .__/|_|\___|\__|\__,_|_| \___|
% |___/ |_|
%
% «the-big-picture» (to ".the-big-picture")
% (ebsp 14 "the-big-picture")
\mysection{The big picture}
\vskip-10pt
%L forths["<-->"] = function () pusharrow("<-->") end
%D diagram ??
%D 2Dx 100 +35 +30 +50 +45
%D 2D 100 LU \weird
%D 2D
%D 2D +20 HAs L1U CCCUs
%D 2D
%D 2D +20 ZHAs IPL L1 CCCs
%D 2D
%D 2D +20 XOX Sets
%D 2D
%D 2D +20 XPX CPL \simple
%D 2D
%D ren LU ==> \text{U}λ
%D ren HAs L1U CCCUs ==> \text{HAs} λ1\text{U} \text{CCCUs}
%D ren ZHAs IPL L1 CCCs ==> \text{ZHAs} \text{IPL} \text{λ1} \text{CCCs}
%D ren XOX Sets ==> (X,\Opens(X)) \text{Sets}
%D ren XPX CPL ==> (X,\Pts(X)) \text{CPL}
%D
%D ren L1U ==> λ1+(U{→}U≈U)
%D
%D (( LU L1U ->
%D L1U CCCUs ->
%D HAs ZHAs <- HAs IPL <- L1U L1 <- CCCUs CCCs <-
%D ZHAs IPL <- IPL L1 -> L1 CCCs <-
%D ZHAs XOX -> ZHAs Sets -> IPL XOX -> IPL CPL -> L1 Sets -> CCCs Sets ->
%D XOX Sets ->
%D XOX XPX -> Sets XPX <-
%D XPX CPL ->
%D \weird \simple <-->
%D ))
%D enddiagram
%D
$\pu
\def\weird{\begin{tabular}{c} weirder, \\ for adults \\ \end{tabular}}
\def\simple{\begin{tabular}{c} for children \\ \end{tabular}}
\diag{??}
$
\ssk
\begin{tabular}{rl}
`$\diagxyto/->/$': & ``can be interpreted in'' \\
$λ1$: & simply-typed $λ$-calculus \\
$Uλ$: & untyped $λ$-calculus \\
$U{→}U≈U$: & we have an object $U$ such that \\
& $U{→}U$ is isomorphic to $U$ \\
CCCU: & a cartesian-closed category \\
& with an object $U{→}U≈U$ \\
\end{tabular}
\msk
IPL distinguishes $P$ and $¬¬P$; CPL does not; IPL has more models than CPL.
% https://ncatlab.org/nlab/show/lambda-calculus
% https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory
% https://ncatlab.org/nlab/show/computational+trinitarianism
\newpage
% _ _
% | | ___ _ __ ___ _ __ __ _| |_ ___ _ __ ___
% _ | | / _ \| '_ \ / _ \ '__/ _` | __/ _ \| '__/ __|
% | |_| | | (_) | |_) | __/ | | (_| | || (_) | | \__ \
% \___/ \___/| .__/ \___|_| \__,_|\__\___/|_| |___/
% |_|
%
% «J-operators» (to ".J-operators")
% (ebsp 15 "J-operators")
\mysection{J-operators}
A {\sl J-operator} is a function $·^*: H→H$ such that
$P≤P^*=P^{**}$ and $P^*∧Q^* = (P∧Q)^*$.
(They are important in topos theory: they induce sheaves.)
\msk
Examples:
%L mp = mpnew({def="zhaora", scale="10pt", meta="s"}, "12345654321"):addcuts("c 321/0 0|123")
%L mp = mpnew({def="zhaboo", scale="7pt", meta="s"}, "1234321"):addcuts("c 321/0 0|123")
%L mp:addlrs():output()
%L mp = mpnew({def="zhaor", scale="7pt", meta="s"}, "123454321"):addcuts("c 4/3/210 012|3|4")
%L mp:addlrs():output()
$$\pu
\begin{array}{rcl}
P^* & := & ¬¬P \\
20^* & = & 30 \\
31^* & = & 33 \\
\end{array}
\;\;
\zhaboo
%
\qquad
%
\begin{array}{rcl}
P^* & := & 22∨P \\
20^* & = & 22 \\
31^* & = & 32 \\
\end{array}
\;\;
\zhaor
$$
\msk
Trick (visual): $P^*$ is the top element
in the equivalence class of $P$.
\msk
The ``fences'' divide the ZHA into equivalence classes ($P∼Q$ iff $P^*=Q^*$)
Theorem: a J-operator takes each $P$ to the top element in its class.
Theorem (hard): J-operators correspond to slashings by diagonal cuts
without cuts stopping midway (see the paper, secs 17--25).
\newpage
% _ _ _ _
% | | (_)_ __ __| | ___ _ __ | |__ __ _ _ _ _ __ ___
% | | | | '_ \ / _` |/ _ \ '_ \| '_ \ / _` | | | | '_ ` _ \
% | |___| | | | | (_| | __/ | | | |_) | (_| | |_| | | | | | |
% |_____|_|_| |_|\__,_|\___|_| |_|_.__/ \__,_|\__,_|_| |_| |_|
%
% «lindenbaum» (to ".lindenbaum")
% (ebsp 16 "lindenbaum")
% https://en.wikipedia.org/wiki/Lindenbaum%E2%80%93Tarski_algebra
\mysection{Lindenbaum(-Tarski) algebras}
...are \ColorRed{non-strict partial orders}
\qquad\qquad \ColorViolet{$←$ i.e., reflexive/transitive relations}
on the set of \ColorRed{all} expressions (wffs)
\qquad \ColorViolet{$←$ what about smaller sets?}
of a logic.
\msk
$\mathsf{expr}_1 ≤_L \mathsf{expr}_2$ iff
we can prove $\mathsf{expr}_1 → \mathsf{expr}_2$ in L.
\msk
Logics: CPL, IPL, IPL${}^*$
In $\mathsf{Lind}(\text{IPL}^*(P,Q,R))$ we have:
$$\begin{array}{c}
P≤¬¬P \\
P \not≥ ¬¬P \\
P \diagxyto/->/ ¬¬P \\
\end{array}
%
\qquad
%
\begin{array}{c}
(P∨Q)^* ≤ (P^*∨Q^*)^* \\
(P∨Q)^* ≥ (P^*∨Q^*)^* \\
(P∨Q)^* \diagxyto/=/ (P^*∨Q^*)^* \\
\end{array}
$$
\msk
{
\def\logic{\text{ (logic) }}
\def\logic{\,\text{(logic)}\,}
\def\logic{\text{(logic)}}
$\mathsf{Lind}(L)$ is a p.o. on an infinite set
but we can look at ``fragments'' of it ---
p.o.s on subsets of $\mathsf{Exprs}(L)$...
}
\bsk
\ColorViolet{
Standard def: the Lindenbaum algebra is the \ColorRed{strict partial order}
on the set of equivalence classes of a logic (where $P∼Q$ iff $P↔Q$)
% Btw, a non-strict p.o. is a relation that is transitive and reflexive.
}
\newpage
% _ _ _ _ ____
% | | (_)_ __ __| | ___ _ __ | |__ __ _ _ _ _ __ ___ |___ \
% | | | | '_ \ / _` |/ _ \ '_ \| '_ \ / _` | | | | '_ ` _ \ __) |
% | |___| | | | | (_| | __/ | | | |_) | (_| | |_| | | | | | | / __/
% |_____|_|_| |_|\__,_|\___|_| |_|_.__/ \__,_|\__,_|_| |_| |_| |_____|
%
% «lindenbaum-2» (to ".lindenbaum-2")
% (ebsp 17 "lindenbaum-2")
\mysection{Lindenbaum algebras (2)}
In $\mathsf{Lind}(\text{IPL}^*(P,Q,R))$ we can prove
%D diagram cube-and*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +23 A5 A3 A6
%D 2D +23 A1 A4 A2
%D 2D +23 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +23 A5 A3 A6
%D 2D +23 A1 A4 A2
%D 2D +23 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
\pu
$$
\begin{array}{rcl}
\diag{cube-and*-full}
\quad
\text{and}
\quad
\diag{cube-or*-full}
\end{array}
$$
\msk
For any J-operator $·^*$ obeying $P≤P^*=P^{**}$ and $(P∧Q)^*=P^*∧Q^*$...
\newpage
% __ __ _ _ _
% \ \ / /_ _| |_ _ __ _| |_(_) ___ _ __ ___
% \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __|
% \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \
% \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/
%
% «valuations» (to ".valuations")
% (ebsp 18 "valuations")
\mysection{Valuations}
In this ZHA, with this J-operator, and this valuation,
%L mpa = mpnew({def="fooa", scale="7pt", meta="s"}, "12321L")
%L mpb = mpnew({def="foob", scale="7pt", meta="s"}, "12321L"):addcuts("c 321/0 0|12")
%L mpc = mpnew({def="fooc", scale="7pt", meta="s"}, "12321L"):addcuts("c 321/0 0|12")
%L mpa:addlrs():output()
%L mpb:addlrs():output()
%L mpc:put(v"10", "P")
%L mpc:put(v"01", "Q")
%L mpc:output()
$$\pu H=\fooa \qquad J=\foob \qquad v=\fooc$$
we have:
%
%L mpd = mpnew({def="food", scale="22pt", meta="s"}, "12321L"):addcuts("c 321/0 0|12")
%L mpd:put(v"10", "P")
%L mpd:put(v"01", "Q")
%L mpd:put(v"20", "P^*")
%L mpd:put(v"02", "Q^*")
%L mpd:put(v"11", "P{∨}Q")
%L mpd:put(v"21", "P^*{∨}Q")
%L mpd:put(v"12", "P{∨}Q^*")
%L mpd:put(v"22", "P^*{∨}Q^*")
%L mpd:put(v"32", "(P^?{∨}Q^?)^*")
%L mpd:output()
%
$$\pu \food
\qquad
\squigto
\qquad
\diag{cube-or*-full}
$$
\newpage
% _ _ _ _
% / \ _ __ ___| |__ ___| |_ _ _ _ __ __ _| |
% / _ \ | '__/ __| '_ \ / _ \ __| | | | '_ \ / _` | |
% / ___ \| | | (__| | | | __/ |_| |_| | |_) | (_| | |
% /_/ \_\_| \___|_| |_|\___|\__|\__, | .__/ \__,_|_|
% |___/|_|
%
% «archetypal» (to ".archetypal")
% (ebsp 19 "archetypal")
\mysection{On ``archetypalness''}
CPL does not distinguish $P$ and $¬¬P$
IPL does distinguish $P$ and $¬¬P$
% IPL has more models than CPL
{\sl How do we visualize IPL?}
\ColorGreen{ZHAs help us visualize {\sl fragments} of the
Lindenbaum Algebra of HAs.}
% (find-es "tex" "colorweb")
% (find-colorwebpage 3)
\msk
% (find-angg ".emacs" "idarct")
% (find-angg ".emacs" "unilog-current")
\par In the categorical models (``hyperdoctrines'') for first-order logic (FOL)
\par there are two different constructions for $R(x,y) \; := \; P(x)∧Q(x)$...
\par In {\sl Internal Diagrams and Archetypal Reasoning in Category Theory}
\href{http://angg.twu.net/math-b.html#idarct}{[Ochs2013]}
\par we showed a way to use the notation of FOL, and the semantics of the
\par ``archetypal model'' ($\Set$!) as tools for understanding hyperdoctrines...
\par Hyperdoctrines are too abstract and too hard when presented ``for adults'',
\par but having an ``archetypal model'' helps a lot!...
\msk
From IDARCT, sec.16:
\ColorViolet{That ``archetypical language'' does not need
to be unambiguous (...) and does not need to be convenient for
expressing all possible constructions. What is relevant is that the
archetypical language, when used side-to-side with the ``algebraic''
language, should give us a way to reason, both intuitively and
precisely, about the structure we're working on; in particular, it
should let us formulate reasonable conjectures quickly, and check
them with reasonable ease...}
\msk
{\sl That's similar to using ZHAs and valuations that ``distinguish
enough things''!}
\newpage
% _____ _ _
% |_ _| |__ __ _ _ __ | | __ _ _ ___ _ _
% | | | '_ \ / _` | '_ \| |/ / | | | |/ _ \| | | |
% | | | | | | (_| | | | | < | |_| | (_) | |_| |
% |_| |_| |_|\__,_|_| |_|_|\_\ \__, |\___/ \__,_|
% |___/
\phantom{a}
\vskip80pt
\centerline{Thank you! $=)$}
\newpage
% _____ _ _ _ _
% |_ _| _ _ __ (_) ___ __ _| | __ _ _ _ ___ ___| |_(_) ___ _ __ ___
% | || | | | '_ \| |/ __/ _` | | / _` | | | |/ _ \/ __| __| |/ _ \| '_ \/ __|
% | || |_| | |_) | | (_| (_| | | | (_| | |_| | __/\__ \ |_| | (_) | | | \__ \
% |_| \__, | .__/|_|\___\__,_|_| \__, |\__,_|\___||___/\__|_|\___/|_| |_|___/
% |___/|_| |_|
%
% «typical-questions» (to ".typical-questions")
% (ebsp 21 "typical-questions")
\mysection{Answers to typical questions}
1. ZHAs are distributive lattices
See Davey and Priestley's {\sl Introduction to Lattices and Order, 2nd ed}, chapter 4.
% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ -36 85) "4. Modular, Distributive and Boolean Lattices")
% (find-daveypriestleypage (+ -38 89) "4.10. The M3-N5 Theorem")
\msk
2. How do I find a countermodel for a sentence?
A: Use modal tableaux and the idea below
\msk
3. Can we change ``planar'' to 2D, 3D, 4D, $\ldots$?
A: Yes, ZHAs are topologies on ``2-column graphs''; change to 3 or more columns
% (phap 19 "topologies-as-partial-orders")
% (pha "topologies-as-partial-orders")
% (phap 21 "2CGs")
% (pha "2CGs")
% (phap 22 "topologies-on-2CGs")
% (pha "topologies-on-2CGs")
% (phap 25 "converting-ZHAs-2CAGs")
% (pha "converting-ZHAs-2CAGs")
%R local house, ohouse = 2/ #1 \, 7/ !h11111 \
%R |#2 #3| | !h01111 |
%R \#4 #5/ | !h01011 !h00111 |
%R |!h01010 !h00011 !h00101|
%R | !h00010 !h00001 |
%R \ !h00000 /
%R house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R house:tomp({def="zdagHouse", scale="15pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse", scale="12pt", meta="s"}):addlrs():addarrows("w"):output()
$$\pu
\def\h{\zfHouse}
(H,\BPM(H)) = \zdagHouse
\qquad
(\Opens(H), ⊂_1) = \zdagOHouse
$$
\msk
4. How do we go from finite HAs to infinite HAs?
A: A starting point: try to add a line with $r{=}2.5$ to a ZHA and see what happens $=)$
\msk
5. Are there propositions that IPL distinguish but ZHAs do not? Or:
Are there any non-theorems of IPL that don't have countermodels in ZHAs?
A: Yes. First idea: in a ZHA we may have $P$, $Q$, $R$ independent, \phantom{mm} \ColorViolet{(62, 53, 44)}
but $P∧Q$, $P∧R$, $Q∧R$ can't be all independent... \phantom{..mmmmmmmm} \ColorViolet{(52, 42, 43)}
Let $α(P,Q) := (P{→}Q)∨(Q{→}P)$,
$β(P,Q,R) := α(P,Q)∨α(P,R)∨α(Q,R)$,
$γ(P,Q,R) := β(P{∧}Q,P{∧}R,Q{∧}R)$.
Then $γ(P,Q,R)$ is a tautology in all ZHAs, but has a 3D countermodel.
Second idea: use the ``width'' of a modal logic
(See {\sl Handbook of Modal Logic}, p.454, and Davey/Priestley p.32)
% (find-books "__alg/__alg.el" "davey-priestley")
\msk
6. How do I teach these things to children:
A: I use $λ$-calculus and lots of {\sl visual} exercises
See the paper and: \url{http://angg.twu.net/LATEX/2017-1-LA-material.pdf}
\ColorViolet{``Disciplina optativa: λ-cálculo, lógicas e traduções''}
\msk
7. Future work / what are the next steps?
A: Categories, toposes and sheaves for children (ongoing work with Peter Arndt)
\newpage
8. What is the shape of a full Lindenbaum Algebra in IPL?
The free HA on one generator ($\IPL(P)$) is well-known and planar (infinite) ---
The free HA on two generators ($\IPL(P,Q)$) is uglier than the product
of two of these things...
\msk
$\IPL(P)$ is the ``Rieger-Nishimura Lattice'', that is the infinite
version of this:
%L mpa = mpnew({def="fooa"}, "12LRLRLRLRLRLR1")
%L mpa:addlrs():output()
\pu
$$\fooa$$
% %L mp:put(v"22", "R")
% %L mp:put(v"44", "Q\\s{a}'R")
% %L mp:put(v"11", "Q\\s{b}'R")
% %L mp:put(v"41", "Q\\s{l}'R")
% %L mp:put(v"14", "Q\\s{r}'R")
\end{document}
% ____ _
% / ___| __ _ _ __| |__ __ _ __ _ ___
% | | _ / _` | '__| '_ \ / _` |/ _` |/ _ \
% | |_| | (_| | | | |_) | (_| | (_| | __/
% \____|\__,_|_| |_.__/ \__,_|\__, |\___|
% |___/
\newpage
% _ _ _
% | | __ _ _ __ ___ | |__ __| | __ _
% | | / _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |__| (_| | | | | | | |_) | (_| | (_| |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%
% «lambda-notation» (to ".lambda-notation")
\mysection{$λ$-notation}
\def\fmat#1#2#3#4#5{
\begin{array}{rcrcl}
#1 &:& #2 & → & #3 \\
& & #4 & ↦ & #5 \\
\end{array}
}
\def\fmat#1#2#3#4#5{
\begin{array}{rrcl}
#1 :& #2 & → & #3 \\
& #4 & ↦ & #5 \\
\end{array}
}
$\begin{array}{rcl}
\fmat {f}{\{2,3,4\}}{\N} {a}{10a+9}
& \diagxyto/-->/<250>\quad
& f \;=\; λa{:}\{2,3,4\}.\,10a+9 \\[20pt]
\fmat {g}{\Z^2}{\Z} {(x,y)}{10x^2+y^2}
& \diagxyto/-->/<250>\quad
& g \;=\; λ(x,y){:}\Z^2.\,{10x^2+y^2} \\[20pt]
\fmat {h}{K}{\Z} {(x,y)}{x}
& \diagxyto/-->/<250>\quad &
h \;=\; λ(x,y){:}K.\,{x} \\
\end{array}
$
% ____ _ _ _ _
% | _ \ ___ ___(_) |_(_) ___ _ __ __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _` | |
% | __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_| \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% «positional» (to ".positional")
\mysection{Positional notations for functions and subsets}
% (phap 1)
% «ZHA-logic-quick» (to ".ZHA-logic-quick")
\mysection{Logic operations on a ZHA: the quick way}
% (phap 7 "prop-calc-ZHA")
\bsk
\mysection{Valuations}
\bsk
\mysection{Tautologies}
\bsk
\mysection{Proof trees}
\end{document}
% Spoiler: a Heyting Algebra in N^2
%
% ...we will see in a few slides that the subset H of Z^2,
% with the partial order given by the arrows, is a Heyting Algebra.
% I prefer to label its points using ``lr-coordinates'' (middle figure).
% We have ⊤=... and ⊥=00, and if P=... and Q=... then:
%
%
% Basic mathematical objects
Functions and $λ$-notation
% (phap 1)
Positional notations
% (phap 3)
LR coordinates
Functions as sets
Positional notations
% «hLR» (getd)
% (ebsp 0 "hLR")
foo
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% modes: (latex-mode emacs-lisp-mode)
% End: