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