% (find-angg "LATEX/2017sajl-mini.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017sajl-mini.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017sajl-mini.pdf"))
% (defun e () (interactive) (find-LATEX "2017sajl-mini.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017sajl-mini"))
% (find-xpdfpage "~/LATEX/2017sajl-mini.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017sajl-mini.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017sajl-mini.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017sajl-mini.pdf
%               file:///tmp/2017sajl-mini.pdf
%           file:///tmp/pen/2017sajl-mini.pdf
% http://angg.twu.net/LATEX/2017sajl-mini.pdf
%
% A sort-of-minimal file that can be compiled with the SAJL class
% (for debugging).
%

%\documentclass{article}
%\usepackage{pict2e}               % (find-es "tex" "pict2e-no-suitable-driver")
%\begin{document}
%Hello
%\end{document}


%\documentclass[pdftex]{sajl}
\documentclass[lualatex]{sajl}
\volume{X}
\issue{X}
\year{20XX}
\setcounter{page}{1}
%\begin{document}
%\end{document}

\usepackage{latexsym,amssymb,amsfonts,amsmath}
\usepackage{graphicx}
\usepackage{array}    % (find-es "tex" "array")
%\usepackage{hyperref} % (find-es "tex" "hyperref")
%\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%%\usepackage[latin1]{inputenc}
%\usepackage{amsmath}
%\usepackage{amsfonts}
%\usepackage{amssymb}
\def\pdfoutput{\outputmode}
\def\pdfpagewidth{\pagewidth}
\def\pdfpageheight{\pageheight}
\usepackage{pict2e}               % (find-es "tex" "pict2e-no-suitable-driver")
%\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{edrx17}               % (find-angg "LATEX/edrx17.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrx17defs.tex             % (find-LATEX "edrx17defs.tex")
%\input edrxheadfoot.tex          % (find-dn4ex "edrxheadfoot.tex")
%\input edrxgac2.tex              % (find-LATEX "edrxgac2.tex")

\def\Opens{\mathcal{O}}
\catcode`→=13 \def→{\rightarrow}



% (find-es "tex" "newtheorem")
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{remark}[definition]{Remark}
\newtheorem{remarks}[definition]{Remarks}
\newtheorem{example}[definition]{Example}
\newtheorem{examples}[definition]{Examples}
\newtheorem{corollary}[definition]{Corollary}

\newtheorem{myfigure}[definition]{Figure}   % Edrx

\newcommand{\negr}[1]{\boldsymbol{#1}}
\newenvironment{proof}{\noindent\bf Proof. \rm}{\hfill $\negr{\blacksquare}$ \\}



%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")

\title{Planar HAs for Children}{Planar Heyting Algebras for Children}

\author{E. Ochs}{Eduardo Ochs}

\begin{document}

\setlength{\extrarowheight}{1pt}


\maketitle


%     _    _         _                  _   
%    / \  | |__  ___| |_ _ __ __ _  ___| |_ 
%   / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
%  / ___ \| |_) \__ \ |_| | | (_| | (__| |_ 
% /_/   \_\_.__/|___/\__|_|  \__,_|\___|\__|
%                                           
% «abstract» (to ".abstract")

\begin{abstract}
This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} using finite Planar Heyting Algebras (that we
call ``ZHAs''), that are certain subsets of $\Z^2$. We also show the
connection between ZHAs and the familiar semantics for IPL where the
truth-values are open sets in a finite topological space
$(P,\Opens(P))$: every ZHA is an ``order topology on a 2-column
graph''.

In the second part of the paper we show how each closure operator
$J:H→H$ on a ZHA $H⊆\Z^2$ corresponds to a) a way to ``slash'' $H$
using diagonal cuts, and b) a choice of a subset $S⊆P$; $J$ can then
be recovered from the inclusion $f:S→P$ as a restriction map $f^*:
\Opens(P)→\Opens(S)$ followed by a map $f_*: \Opens(S)→\Opens(P)$ that
reconstructs the missing information ``in the biggest way possible''.

When a mathematical paper is written ``for children'' this means
either that it is written for people without lots of mathematical {\sl
  knowledge} or that it doesn't require mathematical {\sl maturity};
we follow the second, stronger, meaning of the term. ``Children'' for
us means people who are not able to understand structures that are too
abstract straight away, they need particular cases first --- and they
also have trouble with infinite objects, and with theorems about
things that they can't calculate: {\sl calculating} is much more basic
for them than {\sl proving}. Writing ``for children'' makes us enforce
a style where everything is constructive and finite and all the main
examples are objects that are easy to draw explicitly.

Closure operators on Heyting Algebras are very important on Topos
Theory: they generate geometric morphisms and sheaves. This paper
introduces several tools that can be used to explain some parts of
Topos Theory to ``children'', but here we stop just before categories
and toposes --- when we move to categories and (pre)sheaves we have to
replace most of the `0's and `1's in our diagrams by sets.

\end{abstract}

\keywords{Heyting Algebras, Intuitionistic Logic, diagrammatic
  reasoning, geometric morphisms.}




%      _          _             _    __   
%   __| | ___  __| |_ __   __ _| |_ / /_  
%  / _` |/ _ \/ _` | '_ \ / _` | __| '_ \ 
% | (_| |  __/ (_| | | | | (_| | |_| (_) |
%  \__,_|\___|\__,_|_| |_|\__,_|\__|\___/ 
%                                         
% «dednat6» (to ".dednat6")
\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



%        _      _                      _       _       
%  _ __ (_) ___| |_ _   _ _ __ ___  __| | ___ | |_ ___ 
% | '_ \| |/ __| __| | | | '__/ _ \/ _` |/ _ \| __/ __|
% | |_) | | (__| |_| |_| | | |  __/ (_| | (_) | |_\__ \
% | .__/|_|\___|\__|\__,_|_|  \___|\__,_|\___/ \__|___/
% |_|                                                  
%
% «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}%
  }}%
}

%      _       __     
%   __| | ___ / _|___ 
%  / _` |/ _ \ |_/ __|
% | (_| |  __/  _\__ \
%  \__,_|\___|_| |___/
%                     
% «defs» (to ".defs")

\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\calI{\mathcal{I}}
\def\calK{\mathcal{K}}
\def\calV{\mathcal{V}}

\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\Int{{\operatorname{\mathsf{int}}}}
\def\coInt{{\operatorname{\mathsf{coint}}}}
%\def\Opens{{\mathcal{O}}}
%
\def\LC {\mathsf{LC}}
\def\RC {\mathsf{RC}}
\def\TCG{\mathsf{2CG}}
\def\pile{\mathsf{pile}}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\ltol#1#2{#1\_{\to}#2\_}
\def\rtor#1#2{\_#1{\to}\_#2}
%
\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\myresizebox#1{%
  \noindent\hbox to \textwidth{\hss
    \resizebox{1.0\textwidth}{!}{#1}%
    \hss}
  }






%  ___       _            _            _   _             
% |_ _|_ __ | |_ ___   __| |_   _  ___| |_(_) ___  _ __  
%  | || '_ \| __/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \ 
%  | || | | | || (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__\___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%                                                        
% «introduction» (to ".introduction")
% (phsp 1 "introduction")

\section*{Introduction}

This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} (sec.\ref{prop-calc-ZHA}) using finite Planar
Heyting Algebras (``ZHAs'', sec.\ref{ZHAs}), that are certain subsets
of $\Z^2$. The ``for children'' of the title means ``for people
without mathematical maturity'' (sec.\ref{children}). 

In sections \ref{topologies}--\ref{converting-ZHAs-2CAGs} we show the
connection between ZHAs and the familiar semantics for IPL where the
truth-values are open sets in a topological space $(P,\Opens(P))$, and
in sections \ref{piccs-and-slashings}--\ref{slashings-are-poly} we
discuss how each closure operator on a ZHA $H⊆\Z^2$ corresponds to a
way to ``slash'' $H$ using diagonal cuts; in sections
\ref{question-marks}--\ref{J-ops-as-adjunctions} we show how each
closure operator correspond to a subset $S⊆P$, or rather to a
restriction map $\Opens(P)→\Opens(S)$ followed by a map
$\Opens(S)→\Opens(P)$ that reconstructs the missing information ``in
the biggest way possible''.


% The ``for children'' in the title has a precise, but somewhat
% unusual, meaning, that is explained in sec.\ref{children}.

% \bsk

%   ____ _     _ _     _                
%  / ___| |__ (_) | __| |_ __ ___ _ __  
% | |   | '_ \| | |/ _` | '__/ _ \ '_ \ 
% | |___| | | | | | (_| | | |  __/ | | |
%  \____|_| |_|_|_|\__,_|_|  \___|_| |_|
%                                       
% «children» (to ".children")
\section{Children}
\label  {children}
% (phsp 2 "children")

The ``children'' in the title of this paper means: ``people without
mathematical maturity''. ``Children'' in this sense are not able to
understand structures that are too abstract straight away, they need
particular cases first; and they also don't deal well with infinite
objects or with expressions like ``for every proposition $P(x)$'', or
even with {\sl theorems}...

\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: