% (find-angg "LATEX/2019logicday.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019logicday.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2019logicday.pdf"))
% (defun e () (interactive) (find-LATEX "2019logicday.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019logicday"))
% (defun g () (interactive) (find-LATEXgrep "egrep --color -nH '^% \\(lod' 2019logicday.tex"))
% (find-xpdfpage "~/LATEX/2019logicday.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019logicday.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019logicday.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019logicday.pdf
%               file:///tmp/2019logicday.pdf
%           file:///tmp/pen/2019logicday.pdf
% http://angg.twu.net/LATEX/2019logicday.pdf
%
% «.title-page»			(to "title-page")
% «.dm-at-puro»			(to "dm-at-puro")
% «.dm-at-puro-2»		(to "dm-at-puro-2")
% «.dm-layers»			(to "dm-layers")
% «.dm-layer-1»			(to "dm-layer-1")
% «.set-comprehensions»		(to "set-comprehensions")
% «.set-comprehensions-2»	(to "set-comprehensions-2")
% «.positional»			(to "positional")
% «.propositions»		(to "propositions")
% «.propositions-2»		(to "propositions-2")
% «.propositions-3»		(to "propositions-3")
% «.context-sequents»		(to "context-sequents")
% «.context-sequents-2»		(to "context-sequents-2")
% «.part-2»			(to "part-2")
% «.lclt»			(to "lclt")
% «.evaluating-exprs»		(to "evaluating-exprs")
% «.evaluating-exprs-2»		(to "evaluating-exprs-2")
% «.evaluating-exprs-2-zoom»	(to "evaluating-exprs-2-zoom")
% «.directed-graphs»		(to "directed-graphs")
% «.wet-paint»			(to "wet-paint")
% «.stable-subsets»		(to "stable-subsets")
% «.stable-subsets-order»	(to "stable-subsets-order")
% «.stable-subsets-order-2»	(to "stable-subsets-order-2")
% «.order-topologies»		(to "order-topologies")
% «.topologies-are-has»		(to "topologies-are-has")
% «.topologies-are-has-2»	(to "topologies-are-has-2")
% «.ipl-on-a-topology»		(to "ipl-on-a-topology")
% «.ipl-on-a-topology-2»	(to "ipl-on-a-topology-2")
% «.ipl-on-a-topology-3»	(to "ipl-on-a-topology-3")
% «.visualize-imp»		(to "visualize-imp")
% «.lr-coordinates»		(to "lr-coordinates")
% «.2cgs»			(to "2cgs")
% «.2cgs-2»			(to "2cgs-2")
% «.2cgs-3»			(to "2cgs-3")
% «.2cgs-and-piles»		(to "2cgs-and-piles")
% «.2cgs-and-piles-2»		(to "2cgs-and-piles-2")
% «.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")
% «.back-to-LCLT»		(to "back-to-LCLT")
% «.five-applications»		(to "five-applications")
% «.a-nonplanar-topology»	(to "a-nonplanar-topology")

\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\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
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
%
\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")
\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                      % (find-es "luatex" "spurious-omega")
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% \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

%L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
\pu

\def\V{\mathbf{T}}
\def\F{\mathbf{F}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}

\def\picturedotsa(#1,#2)(#3,#4)#5{%
  \vcenter{\hbox{%
  \beginpicture(#1,#2)(#3,#4)%
  \pictaxes%
  \pictdots{#5}%
  \end{picture}%
  }}%
}




% «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}}

% «myoval» (to ".myoval")
% (find-LATEXfile "2018pict2e.tex" "\\def\\myoval")
\def\myvcenter#1{\ensuremath{\vcenter{\hbox{#1}}}}%
\def\myoval(#1,#2)(#3,#4)[#5]{%
  \myvcenter{%
    \begin{picture}(#1,#2)(-#3,-#4)
      \put(0,0){\oval[#5](#1,#2)}
    \end{picture}%
  }}

\catcode`•=13 \def•{\ensuremath{\bullet}}

\def\calA{\mathcal{A}}
\def\calB{\mathcal{B}}
\def\calC{\mathcal{C}}
\def\calD{\mathcal{D}}
\def\bbG{\mathbb{G}}
\def\antitabular{\hskip-5.5pt}

\setlength{\parindent}{0em}


%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page» (to ".title-page")
% (lodp 1 "title-page")
% (loda   "title-page")
% (find-es "tex" "huge")

\begin{center}

\Large 

{\bf

How to \ColorRed{almost} teach

Intuitionistic Logic to

Discrete Mathematics

Students

}

\bsk

\normalsize

Eduardo Ochs (UFF, Brazil)

\footnotesize

\url{http://angg.twu.net/math-b.html}

\scriptsize

\url{http://www.logicauniversalis.org/wld}

\url{http://www.logicauniversalis.org/wld-rio-de-janeiro}

``World Logic Day'' --- Rio de janeiro, 2019jan14

% http://www.logicauniversalis.org/wld-rio-de-janeiro


% %$$
%   \text{By:}
%   \quad
%   \begin{tabular}{c}
%     % (xz              "~/LATEX/2018vichy-video-edrx.jpg")
%     \includegraphics[height=50pt]{2018vichy-video-edrx.jpg} \\
%     Eduardo \\ Ochs \\ (UFF, Brazil)
%   \end{tabular}
%   \quad
%   \begin{tabular}{c}
%     % (xz              "~/LATEX/2018vichy-video-selana.jpg")
%     \includegraphics[height=50pt]{2018vichy-video-selana.jpg} \\
%     Selana \\ Ochs \\ \\
%   \end{tabular}
%   % \quad
%   % \begin{tabular}[b]{c}
%   %   % (xz              "~/LATEX/2018vichy-video-lucatelli.jpg")
%   %   \includegraphics[width=2cm]{2018vichy-video-lucatelli.jpg} \\
%   %   Fernando \\ Lucatelli \\
%   % \end{tabular}
% %$$

\end{center}


\newpage

\noedrxfooter



%  ____  __  __         _     ____  _   _ ____   ___  
% |  _ \|  \/  |   __ _| |_  |  _ \| | | |  _ \ / _ \ 
% | | | | |\/| |  / _` | __| | |_) | | | | |_) | | | |
% | |_| | |  | | | (_| | |_  |  __/| |_| |  _ <| |_| |
% |____/|_|  |_|  \__,_|\__| |_|    \___/|_| \_\\___/ 
%                                                     
% «dm-at-puro» (to ".dm-at-puro")
% (lodp 2 "dm-at-puro")
% (loda   "dm-at-puro")

{\bf Discrete Mathematics at PURO/UFF}

I teach in a campus that UFF has in Rio das Ostras,

in the countryside of the state of Rio de Janeiro...

The entrance of the campus looks like this:

\msk

\begin{tabular}{c}
  % http://angg.twu.net/blergh.html
  % (xz                 "~/LATEX/2019logicday-PURO.jpg")
  \includegraphics[height=120pt]{2019logicday-PURO.jpg} \\
\end{tabular}
\quad
$⇐$
\quad
\begin{tabular}[c]{l}
``PURO'': \\
Pólo Universitário \\
de Rio das Ostras \\
\end{tabular}

\newpage


% «dm-at-puro-2»  (to ".dm-at-puro-2")
% (lodp 3 "dm-at-puro-2")
% (loda   "dm-at-puro-2")

{\bf Discrete Mathematics at PURO/UFF (2)}

Discrete Mathematics is taught to first-semester

Computer Science students there.

Most of these students enter the university with

{\sl very little knowledge} of how to use variables,

and when they attempt to spell out their ideas in Portuguese,

either speaking or writing, they are \ColorRed{too imprecise}...

They ask ``can I do xxx yyy?'' and if I say ``yes'' they

write weird atrocities in the test, and when I mark them

as wrong they blame me (``you said I could do that!'');

if I say ``no, you can't do that'' then they do other

atrocites and blame me, too.

{\ColorRed{I don't have time to debug their Portuguese!}}



\newpage

%  ____  __  __   _                           
% |  _ \|  \/  | | | __ _ _   _  ___ _ __ ___ 
% | | | | |\/| | | |/ _` | | | |/ _ \ '__/ __|
% | |_| | |  | | | | (_| | |_| |  __/ |  \__ \
% |____/|_|  |_| |_|\__,_|\__, |\___|_|  |___/
%                         |___/               
%
% «dm-layers» (to ".dm-layers")
% (lodp 4 "dm-layers")
% (loda   "dm-layers")

{\bf Discrete Mathematics at PURO/UFF (3)}

...so I decided that I would stress mathetical notation ---

Almost all ideas on the blackboard (whiteboard, actually)

would have examples in mathematical notation.

\ssk

I structured the course of Discrete Mathematics

in three layers (presented more or less in parallel):

\ssk

Layer 1: \ColorRed{Calculating} things

in a system with numbers, truth-values, sets and lists

where everything can be calculated in a \ColorRed{finite} number

of steps with almost no creativity required.

\ssk

Layer 2: some infinite objects, like $\N$ and $\Z$, are allowed;

we learn how to ``calculate'', e.g., $∃k∈\Z.10k=23$

\ssk

Layer 3: we add formal proofs.

\newpage

%  _                            _ 
% | |    __ _ _   _  ___ _ __  / |
% | |   / _` | | | |/ _ \ '__| | |
% | |__| (_| | |_| |  __/ |    | |
% |_____\__,_|\__, |\___|_|    |_|
%             |___/               
%
% «dm-layer-1»  (to ".dm-layer-1")
% (lodp 5 "dm-layer-1")
% (loda   "dm-layer-1")

{\bf Layer 1: Calculating things}

...in a system with numbers, truth-values, sets and lists

where everything can be calculated in a \ColorRed{finite} number

of steps with almost no creativity required.

Example:

$\antitabular
 \begin{array}{rcl}
  (∀a∈\{2,3,5\}.a^2<10) &=& (a^2<10)[a:=2] \;∧ \\&&
                            (a^2<10)[a:=3] \;∧ \\&&
                            (a^2<10)[a:=5] \\
                        &=& (2^2<10) ∧
                            (3^2<10) ∧
                            (4^2<10) \\
                        &=& (4<10) ∧
                            (9<10) ∧
                            (16<10) \\
                        &=& \V ∧ \V ∧ \F \\
                        &=& \F \\
  \end{array}
$

Note the substituion operator:

$(a^2<10)[a:=3] = (3^2<10)$.

\newpage

%   ____                               _                    _                 
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __  ___ 
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | \__ \
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|___/
%                      |_|                                                    
%
% «set-comprehensions» (to ".set-comprehensions")
% (lodp 6 "set-comprehensions")
% (loda   "set-comprehensions")

{\bf Layer 1: Set Comprehensions}

I wrote a lengthy explanation of set comprehensions,

using ``generators'', ``filters'' and a ``result expression''.

The students started by learning how to calculate things

like these (note the `;' instead of a `$|$'; these `$\{\ldots;\ldots\}$'s

are calculated from left to right!):

\unitlength=5pt \def\closeddot{\circle*{0.4}}
\unitlength=5pt \def\closeddot{\circle*{0.2}}

$$\begin{array}{lll}
\{\ug{a∈\{1,2\}},
  \ug{b∈\{2,3\}},
  \uf{a≠b}; \ue{(a,b)}\} \\[10pt]
 = \;\; \{(1,2),(1,3),(2,3)\} \\[5pt]
 = \;\; \picturedotsa(0,0)(3,4){ 1,2 1,3 2,3 } \\
\end{array}
$$

...then $\setofst{a∈\{2,3,4\}}{a^2<10}$

and $\setofst{10a+b}{a∈\{1,2\},b∈\{3,4\}}$.


\newpage

% «set-comprehensions-2» (to ".set-comprehensions-2")
% (lodp 7 "set-comprehensions-2")
% (loda   "set-comprehensions-2")

{\bf Layer 1: Set Comprehensions (2)}

The ``lengthy explanation of set comprehensions''

using ``generators'', ``filters'' and a ``result expression'', has:

2 pages of explanations,

2 pages of exercises (5+19+16+9+16+7 exercises),

1 page of answers, all using a graphical notation ---

for example:

2)
$     A = \picturedotsa(0,0)(4,4){     1,2 2,1     }
\quad B = \picturedotsa(0,0)(4,4){     1,2 2,1 3,0 }
\quad C = \picturedotsa(0,0)(4,4){ 0,3 1,2 2,1 3,0 }
\quad D = \picturedotsa(0,0)(4,4){ 0,3 .5,2.5 1,2 1.5,1.5 2,1 2.5,.5 3,0 }
$

\msk

$
\quad E = \picturedotsa(0,0)(4,4){ 1,3 2,3 3,3   1,4 2,4 3,4 }
\quad F = \picturedotsa(0,0)(4,4){ 3,1 4,1   3,2 4,2   3,3 4,3 }
\quad G = \picturedotsa(0,0)(4,4){ 1,3 2,3 3,3   1,4 2,4 3,4 }
\quad H = \picturedotsa(0,0)(4,4){ 3,2 4,2 }
$

\msk

$
\quad I = \picturedotsa(0,0)(4,4){ 1,3 2,3       1,4         }
\quad J = \picturedotsa(0,0)(4,4){     2,3 3,3   1,4 2,4 3,4 }
\quad K = \picturedotsa(0,0)(4,4){     1,4 2,4 3,4 4,4
                                      1,3 2,3 3,3 4,3
                                      1,2 2,2 3,2 4,2
                                      1,1 2,1 3,1 4,1 }
\quad L = \picturedotsa(0,0)(4,4){ 0,4 1,4 2,4 3,4 4,4
                                  0,3 1,3 2,3 3,3 4,3
                                  0,2 1,2 2,2 3,2 4,2
                                  0,1 1,1 2,1 3,1 4,1
                                  0,0 1,0 2,0 3,0 4,0 }
$

\newpage

%  ____           _ _   _                   _ 
% |  _ \ ___  ___(_) |_(_) ___  _ __   __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _` | |
% |  __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_|   \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%                                             
% «positional» (to ".positional")
% (lodp 8 "positional")
% (loda   "positional")

{\bf Positional notations}

...then we adapt the graphical notation for subsets of $\Z^2$...

we define a convention for omitting the axes,

\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}

$$K =
  \csm{        & (1,3), &        \\
        (0,2), &        & (2,2), \\
               & (1,1), &        \\
               & (1,0)  &        \\
      }
  = \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
  = \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
$$

we define a positional notation for functions,
%
$$f =
  \csm{            & ((1,3),1), &            \\
        ((0,2),0), &            & ((2,2),2), \\
                   & ((1,1),1), &            \\
                   & ((1,0),1)  &            \\
      }
  = 
  \sm{    & 1 &   \\
        0 &   & 2 \\
          & 1 &   \\
          & 1 &   \\
      }
$$

and for subsets,
partial functions,
and characteristic functons:
%
$$% A =
  \sm{   & • &   \\
       · &   & • \\
         & • &   \\
         & · &   \\
     }
  ⊂
  \sm{   & • &   \\
       • &   & • \\
         & • &   \\
         & • &   \\
     }
  % = K
  \qquad
  % g =
  \sm{    & 1 &   \\
        · &   & 2 \\
          & 1 &   \\
          & · &   \\
      }
  % : A → \N
  \qquad
  \sm{   & 1 &   \\
       0 &   & 1 \\
         & 1 &   \\
         & 0 &   \\
     }
$$

\newpage

%  ____                            _ _   _                 
% |  _ \ _ __ ___  _ __   ___  ___(_) |_(_) ___  _ __  ___ 
% | |_) | '__/ _ \| '_ \ / _ \/ __| | __| |/ _ \| '_ \/ __|
% |  __/| | | (_) | |_) | (_) \__ \ | |_| | (_) | | | \__ \
% |_|   |_|  \___/| .__/ \___/|___/_|\__|_|\___/|_| |_|___/
%                 |_|                                      
%
% «propositions» (to ".propositions")
% (lodp 9 "propositions")
% (loda   "propositions")

{\bf Propositions}

Let $W = \{0,1,2,3\}×\{0,1,2\} =
     \picturedotsa(0,0)(3,2){ 0,2 1,2 2,2 3,2   0,1 1,1 2,1 3,1   0,0 1,0, 2,0, 3,0 }
    $ \; .

(Our ``set of worlds'').

A {\sl proposition on $A$} is a function $P:A→\{\F,\V\}$.

Let $P,Q,R$ be these propositions on $W$:

$P = \setofst{((x,y),z)}{(x,y)∈W, z=(x≤1 ∧ y≥1)}$

$Q = \setofst{((x,y),z)}{(x,y)∈W, z=(1≤x≤2 ∧ y≥1)}$

$R = \setofst{((x,y),z)}{(x,y)∈W, z=(0≤x≤2 ∧ y≤1)}$

or:

$\begin{array}{lcc}
 P = P(x,y) = (x≤1 ∧ y≥1)    &=& \sm{\V&\V&\F&\F \\ \V&\V&\F&\F \\ \F&\F&\F&\F} \\[7pt]
 Q = Q(x,y) = (1≤x≤2 ∧ y≥1)  &=& \sm{\F&\V&\V&\F \\ \F&\V&\V&\F \\ \F&\F&\F&\F} \\[7pt]
 R = R(x,y) = (0≤x≤2 ∧ y≤1)  &=& \sm{\F&\F&\F&\F \\ \V&\V&\V&\F \\ \V&\V&\V&\F} \\
 \end{array}
$

\newpage

% «propositions-2» (to ".propositions-2")
% (lodp 10 "propositions-2")
% (loda    "propositions-2")

{\bf Propositions (2)}

In a (long) series of exercises the students learned to visualize
these and lots of other propositions on $W$ --- actually this set of
propositions,

$\calS = \{
  ⊤,\;
  ⊥,\;
  P,\;
  Q,\;
  R,\;
  P∧Q,\;
  P∨Q,\;
  P→Q
  \}
$

and I asked them to draw the Hasse diagram of the partial order on
$\calS$. They got this:
%
%D diagram hasse-props
%D 2Dx     100 +20 +20 +15  +20
%D 2D  100     T 
%D 2D
%D 2D  +20     PvQ     P->Q R
%D 2D
%D 2D  +20 P       Q
%D 2D
%D 2D  +20     P&Q
%D 2D
%D 2D  +20     F
%D 2D
%D ren T F PvQ P&Q P->Q ==> ⊤ ⊥ P{∨}Q P{∧}Q P{→}Q
%D
%D (( F P&Q ->
%D    P&Q P -> P&Q Q ->
%D    P PvQ -> Q PvQ -> Q P->Q ->
%D    PvQ T -> P->Q T ->
%D    F R -> .curve= _10pt R T -> .curve= _10pt
%D ))
%D enddiagram
%D
%D diagram hasse-props-2
%D 2Dx     100 +20 +20 +15  +20
%D 2D  100     T 
%D 2D
%D 2D  +20     PvQ     P->Q R
%D 2D
%D 2D  +20 P       Q
%D 2D
%D 2D  +20     P&Q
%D 2D
%D 2D  +20     F
%D 2D
%D ren T    ==> \sm{1111\\1111\\1111}
%D ren F    ==> \sm{0000\\0000\\0000}
%D ren P    ==> \sm{1100\\1100\\0000}
%D ren Q    ==> \sm{0110\\0110\\0000}
%D ren R    ==> \sm{0000\\1110\\1110}
%D ren PvQ  ==> \sm{1110\\1110\\0000}
%D ren P&Q  ==> \sm{0100\\0100\\0000}
%D ren P->Q ==> \sm{0111\\0111\\1111}
%D
%D (( F P&Q ->
%D    P&Q P -> P&Q Q ->
%D    P PvQ -> Q PvQ -> Q P->Q ->
%D    PvQ T -> P->Q T ->
%D    F R -> .curve= _10pt R T -> .curve= _10pt
%D ))
%D enddiagram
%D
\pu
$$\resizebox{0.6\width}{!}{$
  \diag{hasse-props}
  $}
$$

\newpage

% «propositions-3» (to ".propositions-3")
% (lodp 11 "propositions-3")
% (loda    "propositions-3")

{\bf Propositions (3)}

Using `0's and `1's instead of `$\F$'s and `$\T$'s, what they got was:

\msk

$\diag{hasse-props-2}
 \quad
 \diag{hasse-props}
$

\newpage

%  ____                              _       
% / ___|  ___  __ _ _   _  ___ _ __ | |_ ___ 
% \___ \ / _ \/ _` | | | |/ _ \ '_ \| __/ __|
%  ___) |  __/ (_| | |_| |  __/ | | | |_\__ \
% |____/ \___|\__, |\__,_|\___|_| |_|\__|___/
%                |_|                         
%
% «context-sequents» (to ".context-sequents")
% (lodp 12 "context-sequents")
% (loda    "context-sequents")

{\bf Comprehensions $→$ contexts $→$ sequents}

The part at the left of the `;' in a `$\{\ldots;\ldots\}$'

is called the ``context''. For example:
%
$$\{\und{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a≠b}, \ug{c∈\{1,\ldots,a+b\}}}{context};
    \ue{10a+c}\}
$$

The {\sl set of possible values} for this context is:
%
$$\{\uC{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a≠b}, \ug{c∈\{1,\ldots,a+b\}}};
    \ue{(a,b,c)}\}
$$

\newpage

% «context-sequents-2» (to ".context-sequents-2")
% (lodp 13 "context-sequents-2")
% (loda    "context-sequents-2")

{\bf Comprehensions $→$ contexts $→$ sequents (2)}

This is surprisingly similar to contexts in sequents!
%
$$\uC{\ug{a∈\Z}, \ug{b∈\{1,2,3\}}, \uf{\mathsf{prime}(4a+b)}}⊢b=3$$

The sequent above can be seen as a (false!) proposition.

We used this in the course to debug proofs.

Our formal proofs were written as series of numbered lines,

each line starting by either ``Suppose'' of ``Then''.

Each ``Then'' line had an associated sequent ---

its context was made of all the open ``Suppose''s.

For each ``Then'' line in a valid proof its associated sequent

had to be a true proposition.



\newpage

%  ____            _     ____  
% |  _ \ __ _ _ __| |_  |___ \ 
% | |_) / _` | '__| __|   __) |
% |  __/ (_| | |  | |_   / __/ 
% |_|   \__,_|_|   \__| |_____|
%                              
% «part-2» (to ".part-2")
% (lodp 14 "part-2")
% (loda    "part-2")

\begin{center}

\Large 

{\bf Part 2: a course

% (an ``optativa'')

about $λ$-Calculus,

Logic and Categories,

with almost no prerequisites}

\bsk

\footnotesize

See: \url{http://angg.twu.net/math-b.html\#lclt}

\end{center}


\newpage

%  _     ____ _   _____ 
% | |   / ___| | |_   _|
% | |  | |   | |   | |  
% | |__| |___| |___| |  
% |_____\____|_____|_|  
%                       
% «lclt» (to ".lclt")
% (lodp 15 "lclt")
% (loda    "lclt")

{\bf $λ$-Calculus, Logics and Translations}

In the semesters 2016.1, 2016.2, 2017.1, 2017.2, and 2018.1

I gave a hands-on seminar course (an ``optativa'' in Portuguese)

called ``$λ$-Calculus, Logics and Translations'' ---

``LCLT'' from here on.

{\sl It was all based on exercises.}

I organized it to be as beginner-friendly as possible,

and I expected it to have some Psychology students

at least in the first classes, but they never came

(even though they said they would)...

\newpage

% «evaluating-exprs» (to ".evaluating-exprs")
% (lodp 16 "evaluating-exprs")
% (loda    "evaluating-exprs")

{\bf Evaluating expressions}

It started as this. Suppose that we forget all the algebra

we know; we only know how to calculate expressions step-by-

step by adding, subtracting, or multiplying two {\sl numbers}.

Then there are several paths from any initial expression

to its final result, and we can draw that as a directed graph

where each arrow $α→β$ means a ``one-step reduction''...

Example:
%
%D diagram 2x4+4x5
%D 2Dx     100  +50  +40
%D 2D  100 A    B
%D 2D
%D 2D  +30 C    D    E
%D 2D
%D ren  A  B      ==>   2·3+4·5   2·3+20
%D ren  C  D  E   ==>     6+4·5     6+20  26
%D (( A B ->   A C -> B D ->
%D    C D ->   D E ->
%D ))
%D enddiagram
%D
\pu
$$\diag{2x4+4x5}$$

\newpage

% «evaluating-exprs-2» (to ".evaluating-exprs-2")
% (lodp 17 "evaluating-exprs-2")
% (loda    "evaluating-exprs-2")

{\bf Evaluating expressions (2)}

Then I added rules for evaluating

a named function $g(a) = a·a+4$,

an unnamed function $λa.\,a·a+4$, and

I defined $h = λa.\,a·a+4$...

\msk

%D diagram reduce-g
%D 2Dx     100 +30 +30
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +40 C ----> D
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  g(2+3)       g(5)
%D ren  E  F  ==>  (2+3)·(2+3)+4  (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4       5·5+4
%D ren  I  J  ==>  25+4            29
%D (( A B ->   E F -> F H ->   G H ->
%D    A E -> E G ->            B H -> H I -> I J ->
%D ))
%D enddiagram
%D
% $$\Diag{reduce-g}$$

%D diagram reduce-h
%D 2Dx     100 +35 +35
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 CL ---> DL
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 CS ---> DS
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  h(2+3)            h(5)
%D ren  CL DL ==>  (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5)
%D ren  CS DS ==>  (a·a+4)[a:=2+3]   (a·a+4)[a:=5]
%D ren  E  F  ==>  (2+3)·(2+3)+4     (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4         5·5+4
%D ren  I  J  ==>  25+4              29
%D (( A B ->   CS DS ->  CL DL ->   E F -> F H ->   G H ->
%D    A CL ->  CL CS ->  CS E -> E G ->
%D    B DL ->  DL DS ->  DS H -> H I -> I J ->
%D ))
%D enddiagram
%D
\pu
$\resizebox{0.5\width}{!}{$
 \diag{reduce-g}
 \qquad
 \diag{reduce-h}
 $}
$

\newpage

% «evaluating-exprs-2-zoom»  (to ".evaluating-exprs-2-zoom")
% (lodp 18 "evaluating-exprs-2-zoom")
% (loda    "evaluating-exprs-2-zoom")

$\resizebox{0.76\width}{!}{$
 \diag{reduce-g}
 \quad
 \diag{reduce-h}
 $}
$

\newpage

%  ____   ____     
% |  _ \ / ___|___ 
% | | | | |  _/ __|
% | |_| | |_| \__ \
% |____/ \____|___/
%                  
% «directed-graphs» (to ".directed-graphs")
% (lodp 19 "directed-graphs")
% (loda    "directed-graphs")

{\bf Directed graphs}

Only then I introduced the concept of directed graph,

and how DGs are represented formally in Mathematics

as pairs of the form (points, arrows)...

And I introduced two ways to convert subsets of $\Z^2$ to

graphs: adding black (or white) pawns moves...

%R local B, W = 2/    bp    \, 2/wp  wp  wp\
%R               |  swsose  |   |  nwnone  |
%R               \bp  bp  bp/   \    wp    /
%R
%R local T = {bp="\\bullet", wp="\\circ",
%R            sw="↙", so="↓", se="↘",
%R            nw="↖", no="↑", ne="↗"}
%R B:tozmp({def="Bmne", scale="10pt", meta=nil}):addcells(T):output()
%R W:tozmp({def="Wmne", scale="10pt", meta=nil}):addcells(T):output()
$$\pu \Bmne \qquad \Wmne
$$
%
%R local K =
%R 1/ o \
%R  |o o|
%R  | o |
%R  \ o /
%R K:tomp({def="Kmini", scale="4pt", meta="s"}):addbullets()             :output()
%R K:tomp({def="Kb", scale="6pt",  meta=nil}):addbullets()               :output()
%R K:tomp({def="KB", scale="18pt", meta=nil}):addbullets():addarrows(nil):output()
%R K:tomp({def="Kn", scale="24pt", meta=nil}):addxys    ():addarrows(nil):output()
%R -- mp:output()
%
\pu
$$K = \Kb
  \quad
  (K, \BPM(K)) = 
  \resizebox{0.76\width}{!}{$
  \KB
  $}
  % = \Kn =
$$

\newpage

% __        __   _                 _       _   
% \ \      / /__| |_   _ __   __ _(_)_ __ | |_ 
%  \ \ /\ / / _ \ __| | '_ \ / _` | | '_ \| __|
%   \ V  V /  __/ |_  | |_) | (_| | | | | | |_ 
%    \_/\_/ \___|\__| | .__/ \__,_|_|_| |_|\__|
%                     |_|                      
%
% «wet-paint» (to ".wet-paint")
% (lodp 20 "wet-paint")
% (loda    "wet-paint")

{\bf Wet paint}

A {\sl ZSet} is a finite subset of $\Z^2$. {\color{red!40!white}(Modulo a detail)}

A {\sl ZDAG} is a ZSet plus its black (or white) pawns moves.

Let $A$ be a ZSet. Let $B$ be a subset of $A$.

%L kite  = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W     = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex   = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite",  meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW",     meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex",   meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu

We will represent $B$ as the characteristic function of $B⊆A$;

for example, $B=\dagKite10110$.

Imagine that the `1's are painted with wet black paint,

that can flow down through the arrows (black pawns moves).

If there is an arrow $1→0$ then black paint will flow

from the 1 to the 0 and will paint the 0 black.

\msk

This is unstable: $\dagKite10110$ --- it changes when the paint flows.

This is stable: $\dagKite00111$ --- it doesn't change.

\newpage

%  ____  _        _     _      
% / ___|| |_ __ _| |__ | | ___ 
% \___ \| __/ _` | '_ \| |/ _ \
%  ___) | || (_| | |_) | |  __/
% |____/ \__\__,_|_.__/|_|\___|
%                              
% «stable-subsets» (to ".stable-subsets")
% (lodp 21 "stable-subsets")
% (loda    "stable-subsets")

{\bf Stable subsets}

I gave the students a ZSet (a finite subset of $\Z^2$),

for example, $H=\dagHouse•••••$, and I asked them to find all

stable subsets of it... Notation:

$\Pts(H)$ is the set of all subsets of $H$,

$\Opens(H)$ is the set of all stable subsets of $H$.

We have
$\Opens(H) =$

$ \{
 \dagHouse00000,
 \dagHouse00001,
 \dagHouse00010,
 \dagHouse00011,
 \dagHouse00101,
 \dagHouse00111,
 \dagHouse01010,
 \dagHouse01011,
 \dagHouse01111,
 \dagHouse11111,
\}
$

\newpage

%   ___   ____        ____  
%  / _ \ / /\ \      / /\ \ 
% | | | | |  \ \ /\ / /  | |
% | |_| | |   \ V  V /   | |
%  \___/| |    \_/\_/    | |
%        \_\            /_/ 
%
% «stable-subsets-order» (to ".stable-subsets-order")
% (lodp 22 "stable-subsets-order")
% (loda    "stable-subsets-order")

{\bf Stable subsets: partial order}

Then I asked them to draw the partial order on $\Opens(H)$,

with $\dagHouse11111$ at the top, and an arrow $α→β$ when

$β$ is $α$ with one `0' changed to a `1'...



%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 local guill, oguill = 2/  #1  #2\, 8/                !g111111                \
%R                        |#3  #4  |   |        !g101111        !g011111        |
%R                        \  #5  #6/   |                !g001111        !g010111|
%R                                     |        !g001011        !g000111        |
%R                                     |!g001010        !g000011                |
%R                                     |        !g000010        !g000001        |
%R                                     \                !g000000                /
%R  guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R  guill:tomp({def="zdagGuill",    scale="7pt", meta="t"}):addbullets():addarrows():output()
%R  guill:tomp({def="zdagGuill",    scale="20pt",  meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill",   scale="28pt",  meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill",  scale="12pt",  meta="s"}):addlrs():addarrows():output()
%
%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({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW",  scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({def="zdagOW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%
\pu
$\resizebox{0.75\width}{!}{$
    (H,\BPM(H)) = \zdagHouse
    \qquad
    (\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse
  $}
$

\newpage

% «stable-subsets-order-2» (to ".stable-subsets-order-2")
% (lodp 23 "stable-subsets-order-2")
% (loda    "stable-subsets-order-2")

$\resizebox{1.1\width}{!}{$
    % (H,\BPM(H)) = \zdagHouse
    % \qquad
    (\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse
  $}
$



\newpage

%   ___          _             _                  
%  / _ \ _ __ __| | ___ _ __  | |_ ___  _ __  ___ 
% | | | | '__/ _` |/ _ \ '__| | __/ _ \| '_ \/ __|
% | |_| | | | (_| |  __/ |    | || (_) | |_) \__ \
%  \___/|_|  \__,_|\___|_|     \__\___/| .__/|___/
%                                      |_|        
%
% «order-topologies» (to ".order-topologies")
% (lodp 24 "order-topologies")
% (loda    "order-topologies")

{\bf Order topologies}

In standard terms, $\Opens(W)$ is the {\sl order topology} on $W$.

More gerally, let $(P,A)$ be a directed graph; $A⊆P×P$.

Each arrow $p→q$ in $A$, i.e., $(p,q)∈A$, can be seen as a

\ColorRed{condition} on open sets: if an open set contains $p$ then it

\ColorRed{has to} contain $q$.

$(P,A) = (\{1,2,3\}, \csm{(1,3),\\(2,3)})$

$⇒ \;\; \Opens_A(P) = \setofst{U⊆P}{\psm{1∈U→3∈U \;\;∧ \\ 2∈U→3∈U \;\;\;\;}}
$

\bsk

Notation:

If $W$ is a ZSet,

$\Opens(W) = \Opens_{\BPM(W)}(W)$

The ``set of stable subsets of $W$'' is a \ColorRed{topology}.


\newpage

%  _____                                  _   _    _        
% |_   _|__  _ __  ___    __ _ _ __ ___  | | | |  / \   ___ 
%   | |/ _ \| '_ \/ __|  / _` | '__/ _ \ | |_| | / _ \ / __|
%   | | (_) | |_) \__ \ | (_| | | |  __/ |  _  |/ ___ \\__ \
%   |_|\___/| .__/|___/  \__,_|_|  \___| |_| |_/_/   \_\___/
%           |_|                                             
%
% «topologies-are-has» (to ".topologies-are-has")
% (lodp 25 "topologies-are-has")
% (loda    "topologies-are-has")

{\bf Topologies are Heyting Algebras}

\ColorRed{Topologies are Heyting Algebras} $⇒$

We can interpret Intuituionistic Propositional Logic (``\ColorRed{IPL}'')

on topologies: \ColorRed{$⊤,⊥,∧,∨,→,¬,↔$}.

Remember --- from the big exercise for MD students ---

that when our set of worlds $W$ is 

\msk

$W = \picturedotsa(0,0)(3,2){ 0,2 1,2 2,2 3,2   0,1 1,1 2,1 3,1   0,0 1,0, 2,0, 3,0 }
   = \picturedots (0,0)(3,2){ 0,2 1,2 2,2 3,2   0,1 1,1 2,1 3,1   0,0 1,0, 2,0, 3,0 }$

\msk

then we can represent \ColorRed{propositions} by the

\ColorRed{set of worlds} in which they're true,

and we use characteristic functions to draw them...
%
$$P = \sm{1100\\1100\\0000}
  \quad
  Q = \sm{0110\\0110\\0000}
  \quad
  P∧Q = \sm{0100\\0100\\0000}
$$

\newpage

%  ___ ____  _                             _              
% |_ _|  _ \| |       ___  _ __     __ _  | |_ ___  _ __  
%  | || |_) | |      / _ \| '_ \   / _` | | __/ _ \| '_ \ 
%  | ||  __/| |___  | (_) | | | | | (_| | | || (_) | |_) |
% |___|_|   |_____|  \___/|_| |_|  \__,_|  \__\___/| .__/ 
%                                                  |_|    
%
% «ipl-on-a-topology» (to ".ipl-on-a-topology")
% (lodp 26 "ipl-on-a-topology")
% (loda    "ipl-on-a-topology")

{\bf Propositional Logic on a topology}

How do we interpret \ColorRed{Intuitionistic} Propositional Logic

on a topology? Conjunction an disjunction are easy...

If $P=\dagHouse00011$ and $Q=\dagHouse00101$ then

$P∧Q = \dagHouse00001$ and

$P∨Q=\dagHouse00111$...

But $P→Q$ is problematic...

\newpage

%  ___ ____  _                             _                ____  
% |_ _|  _ \| |       ___  _ __     __ _  | |_ ___  _ __   |___ \ 
%  | || |_) | |      / _ \| '_ \   / _` | | __/ _ \| '_ \    __) |
%  | ||  __/| |___  | (_) | | | | | (_| | | || (_) | |_) |  / __/ 
% |___|_|   |_____|  \___/|_| |_|  \__,_|  \__\___/| .__/  |_____|
%                                                  |_|            
%
% «ipl-on-a-topology-2» (to ".ipl-on-a-topology-2")
% (lodp 27 "ipl-on-a-topology-2")
% (loda    "ipl-on-a-topology-2")

{\bf IPL on a topology (2)}

\def\und#1#2{\underbrace{#1}_{#2}}

$P→Q \;\;=\;\;
 \und{ 
 \und{¬\und{P}{\dagHouse00011}}{\ColorRed{\dagHouse11100}} ∨
 \und{Q}{\dagHouse00101}
 }{\ColorRed{\dagHouse11101}}
 \;\;=\;\; \ColorRed{\dagHouse11101}
$, not stable/open!

The fix is totally artificial.

We distinguish modal operations (easy)

from intuitionistic operations (hard --- use interior).

\newpage

%  ___ ____  _                             _                _____ 
% |_ _|  _ \| |       ___  _ __     __ _  | |_ ___  _ __   |___ / 
%  | || |_) | |      / _ \| '_ \   / _` | | __/ _ \| '_ \    |_ \ 
%  | ||  __/| |___  | (_) | | | | | (_| | | || (_) | |_) |  ___) |
% |___|_|   |_____|  \___/|_| |_|  \__,_|  \__\___/| .__/  |____/ 
%                                                  |_|            
%
% «ipl-on-a-topology-3» (to ".ipl-on-a-topology-3")
% (lodp 28 "ipl-on-a-topology-3")
% (loda    "ipl-on-a-topology-3")

{\bf IPL on a topology (3)}

\def\M{\mathsf{M}}
\def\I{\mathsf{I}}
\def\Int{\mathsf{Int}}

$\begin{array}{rcl}
   ¬_\M P &:=& ⊤∖P \\
 P →_\M Q &:=& ¬_M P ∨ Q \\
    P → Q &:=& P →_\I Q \\
          &:=& \Int(P →_\M Q) \\
          &=& \Int(¬_\M P ∨ Q) \\
          &=& \Int((⊤∖P) ∨ Q) \\
      ¬P  &:=& P→⊥ \\
          &=& P →_I ⊥ \\
          &=& \Int(P →_\M ⊥) \\
          &=& \Int(¬_M P ∨ ⊥) \\
          &=& \Int(¬_M P) \\
          &=& \Int(⊤∖P)
  \end{array}
$

\msk

$\dagHouse00011 → \dagHouse00101
 \;=\;
 \Int(\dagHouse11100 ∨ \dagHouse00101)
 \;=\;
 \Int(\dagHouse11101)
 \;=\;
 \dagHouse00101
$

\newpage

% __     ___                 _ _               __  
% \ \   / (_)___ _   _  __ _| (_)_______       \ \ 
%  \ \ / /| / __| | | |/ _` | | |_  / _ \  _____\ \
%   \ V / | \__ \ |_| | (_| | | |/ /  __/ |_____/ /
%    \_/  |_|___/\__,_|\__,_|_|_/___\___|      /_/ 
%                                                  
% «visualize-imp» (to ".visualize-imp")
% (lodp 29 "visualize-imp")
% (loda    "visualize-imp")

{\bf How do we visualize the intuitionistic `$→$'?}

How do we \ColorRed{visualize} how the

intuitionistic implication works?

$⊤$ and $⊥$ are easy: the top and the bottom elements,

$∧$ and $∨$ are easy: ``meet'' and ``join'' in the lattice.

We need a more convenient way to draw our topologies.
%
%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()
\pu
%
$$\resizebox{0.45\width}{!}{$
  \def\h{\zfHouse}\zdagOHouse
  $}
  \quad ⇒ \quad
  \ohouse
$$
%
Each open set will be written as two digits.


\newpage

%  _     ____                            _     
% | |   |  _ \    ___ ___   ___  _ __ __| |___ 
% | |   | |_) |  / __/ _ \ / _ \| '__/ _` / __|
% | |___|  _ <  | (_| (_) | (_) | | | (_| \__ \
% |_____|_| \_\  \___\___/ \___/|_|  \__,_|___/
%                                              
% «lr-coordinates» (to ".lr-coordinates")
% (lodp 30 "lr-coordinates")
% (loda    "lr-coordinates")

{\bf LR-coordinates}

$(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$.

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")
% (lodp 31 "2cgs")
% (loda    "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")
% (lodp 32 "2cgs-2")
% (loda    "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")
% (lodp 33 "2cgs-and-piles")
% (loda    "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")
% (lodp 34 "2cgs-and-piles-2")
% (loda    "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

%  ____   ____ ____                       _       __  
% |___ \ / ___/ ___|___    __ _ _ __   __| |      \ \ 
%   __) | |  | |  _/ __|  / _` | '_ \ / _` |  _____\ \
%  / __/| |__| |_| \__ \ | (_| | | | | (_| | |_____/ /
% |_____|\____\____|___/  \__,_|_| |_|\__,_|      /_/ 
%                                                     
% «2cgs-and-implication»  (to ".2cgs-and-implication")
% (lodp 35 "2cgs-and-implication")
% (loda    "2cgs-and-implication")

{\bf 2CGs and implication}

\def\squigbij{\;\; \diagxyto/<~>/<300> \;\;}

We are using

$(P,A)=\foo$, $\Opens_P(A) = \zfoo$

%L tcgmed("pia") :cs("110", "1000"):hs():output()
%L tcgmed("pib") :cs("100", "1100"):hs():output()
%L tcgmed("pina"):cs("001", "0111"):hs():output()
%L tcgmed("pic") :cs("101", "1111"):hs():output()
%L tcgmed("pid") :cs("100", "1110"):hs():output()
\pu

Then $21→12 = \pia→\pib = \Int(\dots)...$

\newpage

% «2cgs-and-implication-2»  (to ".2cgs-and-implication-2")
% (lodp 36 "2cgs-and-implication-2")
% (loda    "2cgs-and-implication-2")

{\bf 2CGs and implication (2)}

Then $21→12 = \pia→\pib$

\ssk

$= \Int(\pina∨\pib)$

\ssk

$= \Int(\pic)$

\ssk

$= \pid = 13$


\newpage

% «2cgs-and-implication-3»  (to ".2cgs-and-implication-3")
% (lodp 37 "2cgs-and-implication-3")
% (loda    "2cgs-and-implication-3")

{\bf 2CGs and implication (3)}

In $(P,A)=\foo$, $\Opens_P(A) = \zfoo$,

$21→12 = 13$.


\newpage

% «back-to-LCLT»  (to ".back-to-LCLT")
% (lodp 38 "back-to-LCLT")
% (loda    "back-to-LCLT")

{\bf Back to LCLT}

In LCLT I followed a different path.

The students learned first a lot of $λ$-calculus

(it's useful for them, they're from CompSci!)

then a bit of Curry-Howard,

then topologies, then Heyting Algebras,

and we used 2CGs and finite,

planar Heyting Algebras (``ZHAs'')

to develop a lot of intuition about IPL ---

we saw several classical tautologies that are

falsifiable in ZHAs.

Then we saw Categories and Cartesian Closed

Categories (``CCCs''), and how using $\Int$ to

calculate `$→$' corresponds to an adjunction.




\newpage

% «five-applications»  (to ".five-applications")
% (lodp 39 "five-applications")
% (loda    "five-applications")

{\bf Where do we go from here?}

This is the abstract that I submitted to EBL 2019:

\msk

{\bf Five applications of the ``Logic for Children'' project to Category Theory}

Category Theory is usually presented in a way that is too abstract,
with concrete examples of each given structure being mentioned
briefly, if at all. One of the themes of the ``Logic for Children''
workshop, held in the UNILOG 2018, was a set of tools and techniques
for drawing diagrams of categorical concepts in a canonical shape, and
for drawing diagrams of particular cases of those concepts in
essentialy the same shape as the general case; these diagrams for a
general and a particular case can be draw side by side ``in parallel''
in a way that lets us transfer knowledge from the particular case to
the general, and back.

In this talk we will present briefly five applications of these
techniques: 1) a way to visualize planar, finite Heyting Algebras ---
we call them ``ZHAs'' --- and to develop a feeling for how the logic
connectives in a ZHA work; 2) a way to build a topos with a given
logic (when that ``logic'' is a ZHA); 3) a way to represent a closure
operator on a ZHA by a ``slashing on that ZHA by diagonal cuts with no
cuts stopping midway''; 4) a way to extend a slashing on a ZHA $H$ to
a ``notion of sheafness'' on the associated topos; 5) a way to start
from a certain very abstract factorization of geometric morphisms
between toposes, described in Peter Johnstone's ``Sketches of an
Elephant'', and derive some intuitive meaning for what that
factorization ``means'': basically, we draw the diagrams, plug in it
some very simple geometric morphisms, and check which ones the
factorization classifies as ``surjections'', ``inclusions'',
``closed'', and ``dense''.





\newpage

% «a-nonplanar-topology»  (to ".a-nonplanar-topology")
% (lodp 42 "a-nonplanar-topology")
% (loda    "a-nonplanar-topology")

{\bf A topology that is not planar}

$\resizebox{0.95\width}{!}{$
  (\Opens(W), ⊂_1) = \def\w{\zfW}\zdagOW
  $}
$




\end{document}



$$\begin{array}{ccl}
  (G,\BPM(G)) = \zdagGuill
    & \qquad
    & (\Opens(G), ⊂_1) = \def\g{\zfGuill}\zdagOGuill \\
    \\
  (W,\BPM(W)) = \zdagW
    & \qquad
    & (\Opens(W), ⊂_1) = \def\w{\zfW}\zdagOW \\
  \end{array}
$$








% (find-angg "LATEX/2018-2-MD-set-compr.tex")
% (find-xpdfpage "~/LATEX/2018-2-MD-set-compr.pdf")
% (find-LATEX "2018-2-MD-set-compr.tex" "comprehension-gab")



% (find-angg "LATEX/2018-2-MD-demonstracoes.tex")
% (find-xpdfpage "~/LATEX/2018-2-MD-demonstracoes.pdf")

% (ph1)

% (ph1p 22 "topologies")
% (ph1     "topologies")






% (find-LATEX "2018-2-MD-ordem-prop.tex")
% (find-xpdfpage "~/LATEX/2018-2-MD-ordem-prop.pdf")
















\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "lod"
% End:
