% (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:
