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