|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: