|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017ebl-handouts.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017ebl-handouts.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017ebl-handouts.pdf"))
% (defun e () (interactive) (find-LATEX "2017ebl-handouts.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017ebl-handouts"))
% (find-xpdfpage "~/LATEX/2017ebl-handouts.pdf")
% (find-sh0 "cp -v ~/LATEX/2017ebl-handouts.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017ebl-handouts.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017ebl-handouts.pdf
% file:///tmp/2017ebl-handouts.pdf
% file:///tmp/pen/2017ebl-handouts.pdf
% http://angg.twu.net/LATEX/2017ebl-handouts.pdf
% «.Header» (to "Header")
%
% «.LRcoords» (to "LRcoords")
% «.Logic» (to "Logic")
% «.NonTaut» (to "NonTaut")
% «.BruteForce» (to "BruteForce")
%
% «.Body» (to "Body")
\documentclass[oneside]{book}
\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{boxedminipage} % (find-es "tex" "boxedminipage")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
%\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\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-es "tex" "geometry")
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2017ebl-slides.tex" "geometry")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
\usepackage[a4paper, landscape,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
%top=1.5cm, bottom=.5cm, left=1.5cm, right=1.5cm, includefoot
top=2cm, bottom=1.5cm, left=2cm, right=2cm, includefoot
]{geometry}
\begin{document}
\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
\def\LR{\mathbb{LR}}
\def\IPL{\text{IPL}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\setlength{\fboxsep}{5pt}
% (find-LATEX "2017planar-has.tex" "prop-calc-ZHA")
% (find-LATEX "2017planar-has.tex" "prop-calc-ZHA" "zdemorgan")
% (find-LATEX "2017planar-has.tex" "HAs")
% (phap 10 "HAs")
% _ _ _
% | | | | ___ __ _ __| | ___ _ __
% | |_| |/ _ \/ _` |/ _` |/ _ \ '__|
% | _ | __/ (_| | (_| | __/ |
% |_| |_|\___|\__,_|\__,_|\___|_|
%
% «Header» (to ".Header")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
{
\setlength{\parindent}{0pt}
\footnotesize
\par Planar Heyting Algebras for Children
\par Eduardo Ochs - EBL2017 - Pirenópolis, may 2017
\par \url{http://angg.twu.net/math-b.html\#ebl-2017}
\par \url{http://angg.twu.net/math-b.html\#zhas-for-children-2}
\par \url{http://angg.twu.net/LATEX/2017planar-has.pdf} (paper)
\par \url{http://angg.twu.net/LATEX/2017ebl-slides.pdf} (slides)
\par \url{http://angg.twu.net/LATEX/2017ebl-handouts.pdf} {\bf (these handouts)}
\par Version: \shorttoday{} \hours
}
\bsk
% _ ____ _
% | | | _ \ ___ ___ ___ _ __ __| |___
% | | | |_) / __/ _ \ / _ \| '__/ _` / __|
% | |___| _ < (_| (_) | (_) | | | (_| \__ \
% |_____|_| \_\___\___/ \___/|_| \__,_|___/
%
% «LRcoords» (to ".LRcoords")
\newsavebox{\LRcoords}
\savebox {\LRcoords}{%
\begin{boxedminipage}[t]{16.5em}
% (ebsp 4 "LR-coords")
% (ebs "LR-coords")
%
\par {\bf LR-coordinates and ZHAs:}
\msk
\par $\ang{l,r} = (0,0) + l\und{\VEC{-1,1}}{\nwarrow} + r\und{\VEC{1,1}}{\nearrow}$
\par Shorthand: $lr = \ang{l,r}$.
\par $\N^2⊂\Z^2$ is a quarter-plane.
\par $\LR⊂\Z^2$ is a ``quarter-plane
\par \quad turned $45°$ to the left'':
\par $\LR = \{\ang{l,r} \;|\; l,r∈\N \}$.
\par An LRSet is a finite, non-empty
\par subset of $\LR$ containing $(0,0)$.
\par ZHAs are LRSets obeying extra
\par conditions...
\msk
\par A ``height-left-right-wall'' $(h,L,R)$
\par generates this ZHA:
\par $\{ (x,y)∈\LR \;|\; y{≤}h, L(y){≤}x{≤}R(y) \}$
\msk
%L mpnew({def="zhab", scale="7pt", meta="s"}, "12321L"):addlrs():output()
%L mpnew({def="zhaxy", scale="11pt", meta="s"}, "12321L"):addxys():output()
\pu
Example:
\ssk
$ \pmat{9,
\csm{(5,-1), \\ (4,0), \\ (3,-1), \\ (2,-2), \\ (1,-1), \\ (0,0) },
\csm{(5,-1), \\ (4,0), \\ (3, 1), \\ (2, 2), \\ (1, 1), \\ (0,0) }
}
\squigto
$
\msk
\par
$ \squigto\;
\csm{\zhaxy}
\;\squigto\;
\zhab
$
\msk
A ZHA is made of all points in $\LR$ between a left and a right wall.
Theorem: every ZHA is a Heyting Algebra. Details: paper, secs.1--9.
\end{boxedminipage}%
}
% \usebox {\LRcoords}
% _ _ _ ______ _ _
% | | ___ __ _(_) ___ (_)_ __ __ _ |__ / | | | / \
% | | / _ \ / _` | |/ __| | | '_ \ / _` | / /| |_| | / _ \
% | |__| (_) | (_| | | (__ | | | | | | (_| | / /_| _ |/ ___ \
% |_____\___/ \__, |_|\___| |_|_| |_| \__,_| /____|_| |_/_/ \_\
% |___/
%
% «Logic» (to ".Logic")
\newsavebox{\Logic}
\savebox {\Logic}{%
\begin{boxedminipage}[t]{16.5em}
\par {\bf Logic in a ZHA}
\par Abbreviations: $\o{b}$, $\o{l}$, $\o{r}$, $\o{a}$ mean
\par $\o{below}$, $\o{leftof}$, $\o{rightof}$, $\o{above}$.
\msk
\par In a ZHA $Ω$ we have:
\msk
$\begin{array}{rcl}
⊤ &:=& \sup(Ω) \\
⊥ &:=& 00 \\
ab∧cd &:=& \min(a,c)\min(b,d) \\
ab∨cd &:=& \max(a,c)\max(b,d) \\
cd→ef &:=& \\
\multicolumn{3}{c}{
\left(\!\!
\begin{array}{lllll}
\o{if} & cd \o{b} ef & \o{then} & ⊤ \\
\o{elseif} & cd \o{l} ef & \o{then} & \o{ne}(ef) \\
\o{elseif} & cd \o{r} ef & \o{then} & \o{nw}(ef) \\
\o{elseif} & cd \o{a} ef & \o{then} & ef \\
\o{end} \\
\end{array}
\!\!\!
\right)
}
\end{array}
$
\msk
where:
\msk
$
\def\foo#1#2#3{cd\o{#1}ef &:=& c{#2}e ∧ d{#3}f}
\def\foo#1#2#3{cd\o{#1}ef &:=& c #2 e ∧ d #3 f}
\;\;\;
\begin{array}{ccl}
\foo b≤≤ \\
\foo l≥≤ \\
\foo r≤≥ \\
\foo r≤≤ \\
\end{array}
$
\msk
and $\o{ne}$ means ``go northeast as most as possible'',
and $\o{nw}$ means ``go northwest as most as possible''
\msk
Partial order:
\msk
$\;\;\;
\begin{array}{rcl}
ab≤cd &:=& a≤c∧b≤d \\
\end{array}
$
\msk
Theorem:
$P≤(Q→R)$ iff $(P∧Q)≤R$
(with the weird `$→$' above).
\end{boxedminipage}%
}
%\usebox{\Logic}
% _ _ _ _ _
% | \ | | ___ _ __ | |_ __ _ _ _| |_ ___ | | ___ __ _ _ _
% | \| |/ _ \| '_ \ _____| __/ _` | | | | __/ _ \| |/ _ \ / _` | | | |
% | |\ | (_) | | | |_____| || (_| | |_| | || (_) | | (_) | (_| | |_| |
% |_| \_|\___/|_| |_| \__\__,_|\__,_|\__\___/|_|\___/ \__, |\__, |
% |___/ |___/
% «NonTaut» (to ".NonTaut")
\newsavebox{\NonTaut}
\savebox {\NonTaut}{%
\begin{boxedminipage}[t]{25em}
{\bf Two non-tautologies}
In this ZHA, with this valuation,
%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 ]]
\pu
$H=\fooa \qquad v=\foob$
we have:
\msk
$\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
Note that $¬P = ¬10 = 10→00 = \o{ne}(00) = 02$
because $10 \o{below} 00$ is false
and $10 \o{leftof} 00$ is true.
\end{boxedminipage}%
}
%\usebox{\NonTaut}
% ____ _ __
% | __ ) _ __ _ _| |_ ___ / _| ___ _ __ ___ ___
% | _ \| '__| | | | __/ _ \ | |_ / _ \| '__/ __/ _ \
% | |_) | | | |_| | || __/ | _| (_) | | | (_| __/
% |____/|_| \__,_|\__\___| |_| \___/|_| \___\___|
%
% «BruteForce» (to ".BruteForce")
\newsavebox{\BruteForce}
\savebox {\BruteForce}{%
\begin{boxedminipage}[t]{23em}
{\bf Calculating `$→$' by brute force}
%R local z = ZHA.fromspec("123454321")
%R local mpB = mpnew({def="fooB", scale="2pt", meta="t"}, "123454321"):addbullets():output()
%R local mpQ = mpnew({def="fooQ", scale="6pt", meta="s"}, "123454321")
%R local mpR = mpnew({def="fooR", scale="5pt", meta="s"}, "123454321")
%R local mpA = mpnew({def="fooA", scale="5pt", meta="s"}, "123454321")
%R mpQ:zhalrf ("P -> P:And (v'31') "):output()
%R mpR:zhalrf0("P -> P:below(v'14') and 1 or 0"):output()
%R mpA:zhalrf0("P -> P:below(v'11') and 1 or 0"):output()
\pu
If $H=\fooB$, $Q=31$ and $R=12$, then
we can calculate $Q→R$ ($=14$) by:
\msk
$(\und{(\und{P ∧ \und{Q}{31}}
{\sm{(λP.P∧31)= \\ \fooQ}}
) ≤ \und{R}{12}
}{\sm{(λP.P∧31≤12)= \\ \fooR}}
)
\;\;=\;\;
(\und{P ≤ (\und{\und{Q}{31}→\und{R}{12}}
{\sm{?????? \\ \\
\text{must be 14,} \\
\text{look below:}}}
)
}{\sm{\text{copy the left side:} \\ \fooR}})
$
\msk
Theorem: the formula for `$→$' in terms of $\o{b}$, $\o{l}$, $\o{r}$, $\o{a}$
yields the same results as the brute force method.
\end{boxedminipage}%
}
%\usebox{\NonTaut}
% ____ _
% | __ ) ___ __| |_ _
% | _ \ / _ \ / _` | | | |
% | |_) | (_) | (_| | |_| |
% |____/ \___/ \__,_|\__, |
% |___/
%
% «Body» (to ".Body")
\noindent
\hbox to \textwidth{\hss
\resizebox{1.0\textwidth}{!}{%
\usebox{\LRcoords}
\usebox{\Logic}
\usebox{\NonTaut}
\usebox{\BruteForce}
}%
\hss}
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: