|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2019seminario-hermann.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019seminario-hermann.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019seminario-hermann.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019seminario-hermann.pdf"))
% (defun e () (interactive) (find-LATEX "2019seminario-hermann.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019seminario-hermann"))
% (setq revert-without-query '("pdf$"))
% (find-pdf-page "~/LATEX/2019seminario-hermann.pdf")
% (find-sh0 "cp -v ~/LATEX/2019seminario-hermann.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019seminario-hermann.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019seminario-hermann.pdf
% file:///tmp/2019seminario-hermann.pdf
% file:///tmp/pen/2019seminario-hermann.pdf
% http://angg.twu.net/LATEX/2019seminario-hermann.pdf
% (find-LATEX "2019.mk")
% Based on:
% (igs)
% «.colors» (to "colors")
% «.title-page» (to "title-page")
% «.goedel-translation» (to "goedel-translation")
% «.S4-tableau-for-DeM» (to "S4-tableau-for-DeM")
% «.values-of-subexpressions-S4» (to "values-of-subexpressions-S4")
% «.values-of-subexpressions-IPL» (to "values-of-subexpressions-IPL")
% «.values-of-subexpressions-3» (to "values-of-subexpressions-3")
% «.lattice» (to "lattice")
% «.lattice-planar» (to "lattice-planar")
% «.lattice-technicalities» (to "lattice-technicalities")
% «.lattice-non-planar» (to "lattice-non-planar")
% «.2CGs-and-LR-coords» (to "2CGs-and-LR-coords")
% «.lr-coordinates» (to "lr-coordinates")
% «.2cgs» (to "2cgs")
% «.2cgs-2» (to "2cgs-2")
% «.2cgs-and-piles» (to "2cgs-and-piles")
% «.2cgs-and-piles-2» (to "2cgs-and-piles-2")
% «.HAs-elementary» (to "HAs-elementary")
% «.HAs-elementary-2» (to "HAs-elementary-2")
% «.HAs-elementary-3» (to "HAs-elementary-3")
% «.HAs-elementary-4» (to "HAs-elementary-4")
% «.2cgs-and-implication» (to "2cgs-and-implication")
% «.2cgs-and-implication-2» (to "2cgs-and-implication-2")
% «.2cgs-and-implication-3» (to "2cgs-and-implication-3")
\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
%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")
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
% «colors» (to ".colors")
% (find-LATEX "2017ebl-slides.tex" "colors")
% (find-LATEX "2017ebl-slides.tex" "colors" "\\def\\ColorGreen")
% (find-xcolorpage 39 "4.4 Colors via x11names option")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
\def\DeM{𝐬{DeM}}
\def\aheadof{𝐬{ahead\_of}}
\def\IPL{𝐬{IPL}}
\def\S{𝐬{S}}
\catcode`\^^O=13 \def*{\ensuremath{\bullet}}
% \catcode`*=13 \def*{\ensuremath{\bullet}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (sehp 1 "title-page")
% (seh "title-page")
% (igsp 1 "title-page")
% (igs "title-page")
% (lodp 1 "title-page")
% (lod "title-page")
% (find-es "tex" "huge")
\begin{center}
\Large
{\bf
Using Planar Heyting Algebras
to develop \ColorRed{visual intuition} about
Intuitionistic Propositional Logic
}
\bsk
\normalsize
Eduardo Ochs (UFF, Brazil)
\footnotesize
\url{http://angg.twu.net/math-b.html\#2019-viipl}
% (find-TH "math-b" "2019-viipl")
Seminário de Lógica do Hermann
PUC-Rio, Rio de Janeiro, 2019sep10
\end{center}
\newpage
\noedrxfooter
% ____ __ __
% | _ \ ___| \/ | ___ _ __ __ _ __ _ _ __
% | | | |/ _ \ |\/| |/ _ \| '__/ _` |/ _` | '_ \
% | |_| | __/ | | | (_) | | | (_| | (_| | | | |
% |____/ \___|_| |_|\___/|_| \__, |\__,_|_| |_|
% |___/
%
% «goedel-translation» (to ".goedel-translation")
% (sehp 2 "goedel-translation")
% (seh "goedel-translation")
{\bf The Gödel translation $T:\IPL→\S4$}
Let $\DeM = ¬( P ∧ Q) → (¬ P ∨ ¬ Q)$,
the part of the DeMorgan laws that is not
a theorem in IPL. Its Gödel translation to S4 is:
%UB ¬( P ∧ Q) → (¬ P ∨ ¬ Q)
%UB -- -- -- --
%UB ◻P ◻Q ◻P ◻Q
%UB ------- ---- ----
%UB ◻P ∧ ◻Q ◻¬◻P ◻¬◻Q
%UB ---------- ------------
%UB ◻¬(◻P∧◻Q) ◻¬◻P ∨ ◻¬◻Q
%UB ---------------------------
%UB ◻((◻¬(◻P∧◻Q))→(◻¬◻P∨◻¬◻Q))
%L
%L defub "demorgan"
%
\pu
$$\def\und#1#2{\underbrace{#1}_{#2}}
T(\ub{demorgan})
$$
\newpage
% ____ _ _ _ _ _ ____ __ __
% / ___|| || | | |_ __ _| |__ | | ___ __ _ _ _ | _ \ ___| \/ |
% \___ \| || |_ | __/ _` | '_ \| |/ _ \/ _` | | | | | | | |/ _ \ |\/| |
% ___) |__ _| | || (_| | |_) | | __/ (_| | |_| | | |_| | __/ | | |
% |____/ |_| \__\__,_|_.__/|_|\___|\__,_|\__,_| |____/ \___|_| |_|
%
% «S4-tableau-for-DeM» (to ".S4-tableau-for-DeM")
% (sehp 3 "S4-tableau-for-DeM")
% (seh "S4-tableau-for-DeM")
{\bf An S4-tableau for $\DeM$}
\msk
%UB ◻ ( ( ◻ ¬ ( ◻ P ∧ ◻ Q ) ) → ( ◻ ¬ ◻ P ∨ ◻ ¬ ◻ Q ) )
%UB --- --- --- ---
%UB ? ? ζ:1 η:1
%UB ----- ---- ---- ----
%UB ? ? δ:1 ε:1
%UB ----------- ------ ------
%UB γ:0 δ:0 ε:0
%UB --------------- -------- --------
%UB γ:1 β:0 β:0
%UB ----------------- ------------------
%UB β:1 β:0
%UB ---------------------------------------------
%UB β:0
%UB ---------------------------------------------------
%UB α:0
%L
%L defub "demorgan-cm"
%
\pu
\resizebox{0.65\textwidth}{!}{$
\ub{demorgan-cm}
$}
\quad
\scalebox{0.7}{%
\begin{tabular}[t]{l}
$∀$ $β$ ahead of $α$, \\
$∀$ $γ$ ahead of $β$, \\
$∃$ $δ$ ahead of $β$, \\
$∃$ $ε$ ahead of $β$, \\
$∀$ $ζ$ ahead of $δ$, \\
$∀$ $η$ ahead of $ε$, \\
$(◻P∧◻Q)_γ=0,$ \\
$P_ζ=1,$ \\
$Q_η=1.$ \\
\end{tabular}%
}
\msk
A solution, i.e., a countermodel for $T(\DeM)$:
%
%D diagram worlds
%D 2Dx 100 +10 +10
%D 2D 100 1
%D 2D
%D 2D +15 2 3
%D 2D
%D # ren ==>
%D (( 1 2 -> 1 3 ->
%D ))
%D enddiagram
%D
%D diagram P
%D 2Dx 100 +10 +10
%D 2D 100 1
%D 2D
%D 2D +15 2 3
%D 2D
%D ren 1 2 3 ==> 0 1 0
%D (( 1 2 -> 1 3 ->
%D ))
%D enddiagram
%D
%D diagram Q
%D 2Dx 100 +10 +10
%D 2D 100 1
%D 2D
%D 2D +15 2 3
%D 2D
%D ren 1 2 3 ==> 0 0 1
%D (( 1 2 -> 1 3 ->
%D ))
%D enddiagram
%D
$$\pu
(W,R) = \left(
\diag{worlds}
\right)^*
\quad
v(P) = \diag{P}
\quad
v(Q) = \diag{Q}
$$
\newpage
% ____ _ _ ____ __ __
% / ___|| || | / ___| \/ |
% \___ \| || |_ | | | |\/| |
% ___) |__ _| | |___| | | |
% |____/ |_| \____|_| |_|
%
%
% «values-of-subexpressions-S4» (to ".values-of-subexpressions-S4")
% (sehp 4 "values-of-subexpressions-S4")
% (seh "values-of-subexpressions-S4")
{\bf The value of the subexpressions}
% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L A = ".1.|2.3"
%L mp = MixedPicture.new({def="dagA", meta="s", scale="4pt"}):zfunction(A):output()
\pu
Once we fix $(W,R)$, $v(P)$, $v(Q)$ we can visualize the value
of each subexpression... I will drop the `$v$'s from here on.
\msk
%UB ◻ ( ( ◻ ¬ ( ◻ P ∧ ◻ Q ) ) → ( ◻ ¬ ◻ P ∨ ◻ ¬ ◻ Q ) )
%UB --- --- --- ---
%UB \P \Q \P \Q
%UB ----- ---- ---- ----
%UB *010 *001 *010 *001
%UB ----------- ------ ------
%UB *000 *101 *110
%UB --------------- -------- --------
%UB *111 *001 *010
%UB ----------------- ------------------
%UB *111 *011
%UB ---------------------------------------------
%UB *011
%UB ---------------------------------------------------
%UB *011
%L
%L defub "demorgan-cm"
%
\pu
\resizebox{0.8\textwidth}{!}{$
\def*{\dagA}
\def\P{\dagA010}
\def\Q{\dagA001}
\ub{demorgan-cm}
$}
\newpage
% ____ _
% / ___| _ _| |__ _____ ___ __ _ __ ___
% \___ \| | | | '_ \ / _ \ \/ / '_ \| '__/ __|
% ___) | |_| | |_) | __/> <| |_) | | \__ \
% |____/ \__,_|_.__/ \___/_/\_\ .__/|_| |___/
% |_|
%
% «values-of-subexpressions-IPL» (to ".values-of-subexpressions-IPL")
% (sehp 5 "values-of-subexpressions-IPL")
% (seh "values-of-subexpressions-IPL")
{\bf The value of the subexpressions (2)}
Start with any $\IPL$ expression $A$ ---
we're using $A = ¬( P ∧ Q) → (¬ P ∨ ¬ Q)$ ---
and an $\S4$ valuation $((W,R),v)$.
What happens if we calculate the values of the subexpressions
of $A$? Take any subexpression $B$ of $A$; calculate $v(T(B))$ ---
%UB ¬( P ∧ Q) → (¬ P ∨ ¬ Q)
%UB -- -- -- --
%UB ◻P ◻Q ◻P ◻Q
%UB ------- ---- ----
%UB ◻P ∧ ◻Q ◻¬◻P ◻¬◻Q
%UB ---------- ------------
%UB ◻¬(◻P∧◻Q) ◻¬◻P ∨ ◻¬◻Q
%UB ---------------------------
%UB ◻((◻¬(◻P∧◻Q))→(◻¬◻P∨◻¬◻Q))
%L
%L defub "demorgan"
%
\pu
$$\def\und#1#2{\underbrace{#1}_{#2}}
T(\ub{demorgan})
$$
\newpage
% «values-of-subexpressions-3» (to ".values-of-subexpressions-3")
% (sehp 6 "values-of-subexpressions-3")
% (seh "values-of-subexpressions-3")
{\bf The value of the subexpressions (3)}
It turns out that \ColorRed{the value of} (the translation of)
\ColorRed{each subexpression} $B$ of $A$ \ColorRed{is $◻$-stable}, in the following
sense: $◻\,v(T(B)) = v(T(B))$. Also,
the intuitionistic operations $⊤,⊥,∧,∨,→_I,¬_I,↔_I$ can
coexist with the $\S4$ operations in the same system...
%UB ¬_I( P ∧ Q) →_I (¬_I P ∨ ¬_I Q)
%UB -- -- -- --
%UB \P \Q \P \Q
%UB ------- ----- -----
%UB *000 *001 *010
%UB ------------ -------------
%UB *111 *011
%UB --------------------------------
%UB *011
%L
%L defub "demorgan"
%
\pu
$$\def\und#1#2{\underbrace{#1}_{#2}}
\def*{\dagA}
\def\P{\dagA010}
\def\Q{\dagA001}
T(\ub{demorgan})
$$
\newpage
% _ _ _ _
% | | __ _| |_| |_(_) ___ ___
% | | / _` | __| __| |/ __/ _ \
% | |__| (_| | |_| |_| | (_| __/
% |_____\__,_|\__|\__|_|\___\___|
%
% «lattice» (to ".lattice")
% (sehp 7 "lattice")
% (seh "lattice")
{\bf The lattice of $◻$-stable truth-values}
When the intuitionistic operations $⊤,⊥,∧,∨,→_I,¬_I,↔_I$
receive $◻$-stable inputs they return $◻$-stable outputs.
How do we visualize:
a) the set of $◻$-stable truth values in an $\S4$-frame $(W,R^*)$?
b) the operations $⊤,⊥,∧,∨,→_I,¬_I,↔_I$?
\msk
Tricks:
The stable truth-values are the \ColorRed{open sets} in a certain topology,
and $(W, \Opens_R(W))$ is an \ColorRed{order topology} (see [PH1], secs.11--17).
Topologies are \ColorRed{Heyting Algebras}, that are \ColorRed{lattices} with some
extra properties...
And for some `$(W,R)$'s these lattices are \ColorRed{planar}.
\newpage
% ____ _
% | _ \| | __ _ _ __ __ _ _ __
% | |_) | |/ _` | '_ \ / _` | '__|
% | __/| | (_| | | | | (_| | |
% |_| |_|\__,_|_| |_|\__,_|_|
%
% «lattice-planar» (to ".lattice-planar")
% (sehp 8 "lattice-planar")
% (seh "lattice-planar")
% (igsp 11 "stable")
% (igs "stable")
% (ph1p 25 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders" "zdef")
{\bf An example (planar)}
%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
%R ohouse:tomp({zdef="OHousebullets", scale="3.5pt", meta="s"}):addbullets():output()
%
\pu
$\resizebox{0.75\width}{!}{$
(H,\BPM(H)) = \zdagHouse
\qquad
(\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse
$}
$
Compact notation: $(\Opens(H),⊆) = \zha{OHousebullets}$
\newpage
% _____ _ _ _ _ _ _
% |_ _|__ ___| |__ _ __ (_) ___ __ _| (_) |_(_) ___ ___
% | |/ _ \/ __| '_ \| '_ \| |/ __/ _` | | | __| |/ _ \/ __|
% | | __/ (__| | | | | | | | (_| (_| | | | |_| | __/\__ \
% |_|\___|\___|_| |_|_| |_|_|\___\__,_|_|_|\__|_|\___||___/
%
% «lattice-technicalities» (to ".lattice-technicalities")
% (sehp 9 "lattice-technicalities")
% (seh "lattice-technicalities")
{\bf Some technicalities}
$\resizebox{0.60\width}{!}{$
(H,\BPM(H)) = \zdagHouse
\qquad
(\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse
$}
$
\msk
If $A⊆\Z^2$ then $\BPM(A)$ is the set of ``black pawns moves'' on $A$
([PH1], sec.2); $U⊂_1V$ means ``$U⊆V$ and they differ by exactly one
element'' ([PH1], sec.13). The transitive-reflexive closure of
$(\Opens_R(W), ⊂_1)$ is the lattice $(\Opens_R(W), ⊆)$.
\newpage
% _ _ _
% | \ | | ___ _ __ _ __ | | __ _ _ __ __ _ _ __
% | \| |/ _ \| '_ \ _____| '_ \| |/ _` | '_ \ / _` | '__|
% | |\ | (_) | | | |_____| |_) | | (_| | | | | (_| | |
% |_| \_|\___/|_| |_| | .__/|_|\__,_|_| |_|\__,_|_|
% |_|
%
% «lattice-non-planar» (to ".lattice-non-planar")
% (sehp 10 "lattice-non-planar")
% (seh "lattice-non-planar")
% (sehp 8 "lattice-planar")
% (seh "lattice-planar")
{\bf An example (non-planar)}
% (ph1p 25 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders" "zdef")
%
%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()
%R
%R womit:tomp({zdef="OWbullets", scale="4.5pt", meta="s"}):addbullets():output()
\pu
$\resizebox{0.65\width}{!}{$
(W,\BPM(W)) = \zha{W}
\qquad
(\Opens(W), ⊂_1) = \def\w{\zfW}\zha{OW} \\
$}
$
The Heyting Algebra $(\Opens(W), ⊆)$
\vskip-6pt
can't be recovered from this diagram: $\zha{OWbullets}$
\newpage
% ____ ____ ____ _ ____ _
% |___ \ / ___/ ___|___ | | | _ \ ___ ___ ___ _ __ __| |___
% __) | | | | _/ __| | | | |_) | / __/ _ \ / _ \| '__/ _` / __|
% / __/| |__| |_| \__ \_ | |___| _ < | (_| (_) | (_) | | | (_| \__ \
% |_____|\____\____|___( ) |_____|_| \_\ \___\___/ \___/|_| \__,_|___/
% |/
%
% «2CGs-and-LR-coords» (to ".2CGs-and-LR-coords")
% (sehp 11 "2CGs-and-LR-coords")
% (seh "2CGs-and-LR-coords")
{\bf 2-column graphs and LR-coordinates}
\bsk
% (oxap 7 "fig:2CGs-ZHA")
% (oxa "fig:2CGs-ZHA")
%
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7} -- with v arrows
%L tspec_PA = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L tspec_PA :mp ({zdef="O_A(P)"}) :addlrs():print() :output()
%L tspec_PAQ:mp ({zdef="O_A(P),J"}):addlrs():print() :output()
%L tspec_PA :tcgq({tdef="(P,A)", meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L tspec_PA :mp ({zdef="O_A(P) b", scale="3.5pt", meta="s"}):addbullets():output()
%L
\pu
$(\Opens\tcg{(P,A)},⊆) \;\;=\;\; \zha{O_A(P)} \;\;=\;\; \zha{O_A(P) b}$
\newpage
% _ ____ _
% | | | _ \ ___ ___ ___ _ __ __| |___
% | | | |_) | / __/ _ \ / _ \| '__/ _` / __|
% | |___| _ < | (_| (_) | (_) | | | (_| \__ \
% |_____|_| \_\ \___\___/ \___/|_| \__,_|___/
%
% «lr-coordinates» (to ".lr-coordinates")
% (sehp 12 "lr-coordinates")
% (seh "lr-coordinates")
% (lodp 30 "lr-coordinates")
% (lod "lr-coordinates")
{\bf LR-coordinates}
%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 zdemorgan:tozmp({def="ohouse", scale="10pt", meta=nil}):addlrs():addcontour():output()
%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()
\pu
$(x,y)$ means: start at $(0,0)$, walk $x$ steps E, $y$ steps N.
$〈l,r〉$ means: start at $(0,0)$, walk $l$ steps NW, $r$ steps NE.
We abbreviate $〈l,r〉$ as $lr$.
\unitlength=8pt \def\closeddot{\circle*{0.4}}
Check:
%
$$\ohouse
\qquad
\picturedotsa(-2,0)(2,5){ -1,5 0,4 -1,3 1,3 -2,2 0,2 2,2 -1,1 1,1 0,0 }
$$
$20 = 〈2,0〉 = (0,0) + 2\VEC{-1,1} + 0\VEC{1,1} = (-2,2)$
$32 = 〈2,0〉 = (0,0) + 3\VEC{-1,1} + 2\VEC{1,1} = (-1,5)$
\newpage
% ____ ____ ____
% |___ \ / ___/ ___|___
% __) | | | | _/ __|
% / __/| |__| |_| \__ \
% |_____|\____\____|___/
%
% «2cgs» (to ".2cgs")
% (sehp 13 "2cgs")
% (seh "2cgs")
% (lodp 31 "2cgs")
% (lod "2cgs")
{\bf 2-column graphs}
A 2-column graph (``2CG'') has two columns of points,
all vertical arrows pointing one step down, and
{\sl some} intercolumn arrows.
An example:
\def\l#1{#1\_}
\def\r#1{\_#1}
%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, "Foo", 3, 4, "34 23", "22 12"):lrs():vs():hs():output()
%L
%L tcg_spec = "3, 4; 34 23, 22 12"
%L tcgmed("foo"):lrs():hs():output()
%L tcgmed("bar"):bus():hs():output()
\pu
$$\Foo
\qquad
\foo
\qquad
\bar
$$
\newpage
% «2cgs-2» (to ".2cgs-2")
% (sehp 14 "2cgs-2")
% (seh "2cgs-2")
% (lodp 32 "2cgs-2")
% (lod "2cgs-2")
{\bf 2-column graphs (2)}
The operation $\TCG$ builds a 2-column graph formally from
the height of its left column,
the height of its right column,
the intercolumn arrows going right,
the intercolumn arrows going left.
\msk
$\begin{array}{l}
\TCG(3,4,\csm{\ltor34, \\ \ltor23},
\csm{\lotr22, \\ \lotr12}) \\[5pt]
=\;\;\; \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}
$
%
$$% \Foo
% \qquad
\foo
\qquad
\bar
$$
\newpage
% ____ ____ ____ _ _ _
% |___ \ / ___/ ___|___ __ _ _ __ __| | _ __ (_) | ___ ___
% __) | | | | _/ __| / _` | '_ \ / _` | | '_ \| | |/ _ \/ __|
% / __/| |__| |_| \__ \ | (_| | | | | (_| | | |_) | | | __/\__ \
% |_____|\____\____|___/ \__,_|_| |_|\__,_| | .__/|_|_|\___||___/
% |_|
%
% «2cgs-and-piles» (to ".2cgs-and-piles")
% (sehp 15 "2cgs-and-piles")
% (seh "2cgs-and-piles")
% (lodp 33 "2cgs-and-piles")
% (lod "2cgs-and-piles")
{\bf 2CGs and piles}
%L tcgmed("pia"):cs("111", "1111"):hs():output()
%L tcgmed("pib"):cs("110", "1000"):hs():output()
\pu
$\TCG(3,4,\csm{\ltor34, \\ \ltor23},
\csm{\lotr22, \\ \lotr12}) % \\[5pt]
= \left(\csm{\phantom{\l4,}\; \l3, \; \l2, \; \l1, \\
\r4, \; \r3, \; \r2, \; \r1 \\
},
\csm{\ldots
}
\right)
$
\ssk
$\pile(3,4) =
\csm{\phantom{\l4,}\; \l3, \; \l2, \; \l1, \\
\r4, \; \r3, \; \r2, \; \r1 \\
} = \pia$
\ssk
$\pile(2,1) =
\csm{\phantom{\l4, \; \l3,}\; \l2, \; \l1, \\
\phantom{\r4, \; \r3, \; \r2,}\; \r1 \\
} = \pib
$
All open sets of a 2CG are piles,
but some piles are not open sets...
for example, $\pile(2,1)$ is not open --- it has $\l2$ but not $\r3$.
\newpage
% «2cgs-and-piles-2» (to ".2cgs-and-piles-2")
% (sehp 16 "2cgs-and-piles-2")
% (seh "2cgs-and-piles-2")
% (lodp 34 "2cgs-and-piles-2")
% (lod "2cgs-and-piles-2")
{\bf 2CGs and piles (2)}
Let
%
$\begin{array}[t]{rcl}
(P,A)
&=& \TCG(3,4,\csm{\ltor34, \\ \ltor23}, \csm{\lotr22, \\ \lotr12}) \\[5pt]
&=& \foo \;\;. \\
\end{array}
$
\msk
%L z = ZHA.fromtcgspec(tcg_spec)
%L mp = MixedPicture.new({scale="10pt", def="zfoo"}, z)
%L mp:addlrs():addcontour():output()
\pu
Then $\Opens_A(P) \;\;\;=\;\;\; \zfoo$
\ssk
{\color{Violet!50!black}Can you visualize $\Opens(\R)$? I find that very hard!}
\newpage
% _ _ _ _
% | | | | / \ ___ ___| | ___ _ __ ___
% | |_| | / _ \ / __| / _ \ |/ _ \ '_ ` _ \
% | _ |/ ___ \\__ \ | __/ | __/ | | | | |
% |_| |_/_/ \_\___/ \___|_|\___|_| |_| |_|
%
% «HAs-elementary» (to ".HAs-elementary")
% (sehp 17 "HAs-elementary")
% (seh "HAs-elementary")
{\bf Heyting Algebras in elementary terms}
Here's what we did up to this point:
We saw briefly the Gödel translation and believed it,
We saw briefly that topologies are HAs and believed that,
We saw briefly how to build planar HAs from 2CGs,
We saw some very compact notations for planar HAs (``\ColorRed{ZHAs}'')...
\msk
But we don't know yet how $⊤,⊥,∧,∨,→,¬,↔$ behave
in the compact notation, and how to visualize them!
\msk
This can be done almost from scratch, using the way
to define $⊤,⊥,∧,∨,→,¬,↔$ from the partial order
of a lattice.
\newpage
% _ _ _ _ ____
% | | | | / \ ___ ___| | ___ _ __ ___ |___ \
% | |_| | / _ \ / __| / _ \ |/ _ \ '_ ` _ \ __) |
% | _ |/ ___ \\__ \ | __/ | __/ | | | | | / __/
% |_| |_/_/ \_\___/ \___|_|\___|_| |_| |_| |_____|
%
% «HAs-elementary-2» (to ".HAs-elementary-2")
% (sehp 18 "HAs-elementary-2")
% (seh "HAs-elementary-2")
{\bf Heyting Algebras in elementary terms (2)}
Left: $H$, the ZHA that we will use in the next slides.
Middle: $(∧)=(Q ∧_H R)$, \; $(→)=(Q →_H R)$.
Right: $(∨)=(P ∨_H Q)$.
\msk
%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="10pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="10pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="10pt", meta=nil}):addlrs():addcontour():output()
$
\pu
\scalebox{0.7}{$
\lozfive \quad \QoRai \quad \PoQai
$}
$
%
\msk
We will see that:
a) if $Q=31$ and $R=12$ then $Q ∧_H R = 11$,
b) if $Q=31$ and $R=12$ then $Q →_H R = 14$.
c) if $P=31$ and $Q=12$ then $P ∨_H Q = 32$,
\newpage
% «HAs-elementary-3» (to ".HAs-elementary-3")
% (sehp 19 "HAs-elementary-3")
% (seh "HAs-elementary-3")
{\bf Heyting Algebras in elementary terms (3)}
Motivation:
\def*#1{\ColorRed{#1}}
\msk
$
\begin{array}{l}
⊥→P \\
P→⊤ \\
(P→(Q∧R)) ↔ ((P→Q)∧(P→R)) \\
((P∨Q)→R) ↔ ((P→R)∧(Q→R)) \\
(P→(Q→R)) ↔ ((P∧Q)→R) \\
\end{array}
$
\bsk
$
\begin{array}{l}
*⊥≤P \\
P≤*⊤ \\
\end{array}
$
\ssk
$
\begin{array}{l}
(P≤*{(Q∧R)}) ↔ ((P≤Q)∧(P≤R)) \\
(P≤*{(Q→R)}) ↔ ((P∧Q)≤R) \\
\end{array}
$
\ssk
$
\begin{array}{l}
(*{(P∨Q)}≤R) ↔ ((P≤R)∧(Q≤R)) \\
\end{array}
$
\newpage
% «HAs-elementary-4» (to ".HAs-elementary-4")
% (sehp 20 "HAs-elementary-4")
% (seh "HAs-elementary-4")
{\bf Heyting Algebras in elementary terms (4)}
$*⊤$ and $*⊥$ are the elements of the ZHA $H$ that
obey this for all $P∈H$:
\ssk
$
\begin{array}{l}
*⊥≤P \\
P≤*⊤ \\
\end{array}
$
\msk
Fix $Q$ and $R$. $*{(Q∧R)}$ and $*{(Q→R)}$ are the
elements of $H$ that obey this for all $P$:
\ssk
$
\begin{array}{l}
(P≤*{(Q∧R)}) ↔ ((P≤Q)∧(P≤R)) \\
(P≤*{(Q→R)}) ↔ ((P∧Q)≤R) \\
\end{array}
$
\msk
Fix $P$ and $Q$. $*{(P∨Q)}$ is the element of $H$
that obeys this for all $R$:
\ssk
$
\begin{array}{l}
(*{(P∨Q)}≤R) ↔ ((P≤R)∧(Q≤R)) \\
\end{array}
$
\newpage
{\bf Guessing (wrongly) and testing}
$$
%R local QoRai, PoQai, PnnP =
%R 1/ T \, 1/ T \, 1/ T \
%R | t . | | . . | | . |
%R | . . . | | . . . | | . . |
%R | . . I i | | . o d . | |d . n|
%R |. Q . . .| |. P . . .| | P . |
%R | . . R . | | . . Q . | \ F /
%R | c a . | | . . . |
%R | b . | | . . |
%R \ F / \ F /
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R t="T'", I="I'", b="B'", c="C'", d="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
\scalebox{0.7}{$
\lozfive \quad \QoRai \quad \PoQai
$}
$$
$B'$ is a bad guess for $*⊥$: it fails when $P=01$.
$T'$ is a bad guess for $*⊤$: it fails when $P=44$.
$C'$ is a bad guess for $*{(Q∧R)}$: it fails when $P=11$.
$I'$ is a bad guess for $*{(Q→R)}$: it fails when $P=14$.
$D'$ is a bad guess for $*{(P∨Q)}$: it fails when $R=32$.
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "seh"
% End: