|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2021logicday.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021logicday.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2021logicday.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021logicday.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021logicday.pdf"))
% (defun e () (interactive) (find-LATEX "2021logicday.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021logicday"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (find-pdf-page "~/LATEX/2021logicday.pdf")
% (find-sh0 "cp -v ~/LATEX/2021logicday.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021logicday.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021logicday.pdf
% file:///tmp/2021logicday.pdf
% file:///tmp/pen/2021logicday.pdf
% http://angg.twu.net/LATEX/2021logicday.pdf
% (find-LATEX "2019.mk")
% http://www.logica-universalis.org/wld3-rio-de-janeiro
% https://www.mariamartinezordaz.com/uploads/1/2/4/3/124357943/[cveng]maor2020.pdf
% «.defs» (to "defs")
% «.title-page» (to "title-page")
% «.discrete-bmos» (to "discrete-bmos")
% «.non-tautologies-1» (to "non-tautologies-1")
% «.non-tautologies-2» (to "non-tautologies-2")
% «.non-tautologies-3» (to "non-tautologies-3")
% «.calculating» (to "calculating")
% «.set-comprehensions» (to "set-comprehensions")
% «.links-to-fav» (to "links-to-fav")
% «.links-about-core» (to "links-about-core")
\documentclass[oneside]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\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
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
% «defs» (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#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}}
\def\True {\mathbf{T}}
\def\V {\mathbf{T}}
\def\False{\mathbf{F}}
\def\F {\mathbf{F}}
\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}%
}}%
}
\noedrxfooter % (find-LATEX "edrxheadfoot.tex")
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (lod21p 1 "title-page")
% (lod21 "title-page")
% (excp 1 "title-page")
% (exc "title-page")
% (ecop 1 "title-page")
% (eco "title-page")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\begin{tabular}{c}
{\Large {\bf The Logic for Children Project}} \\[1pt]
{\Large {\bf (is trying to translate its}} \\[1pt]
{\Large {\bf categorical diagrams}} \\[1pt]
{\Large {\bf to Type Theory)}} \\[1pt]
\ColorGray{(talk @ Logic Day 2021)}
\end{tabular}
\bsk
\begin{tabular}[c]{r}
By: \\
Eduardo Ochs $→$ \\
\ColorGray{(original author)} \\
\\
Selana Ochs $→$ \\
\ColorGray{(recent contributor)} \\
\end{tabular}
\!\!\!\!\!\!\!
\begin{tabular}[c]{c}
% $\includegraphics[height=85pt]{2019emacsconf-eu-e-selana.jpg}$
$\includegraphics[height=85pt]{2021logicday-selana2.jpg}$
\end{tabular}
% \msk
% \url{http://angg.twu.net/\#eev}
\end{center}
\newpage
Note: this presentation is a kind of
mini-rehearsal for a longer presentation titled
``Category Theory as An Excuse to Learn Type Theory''
that I submitted to the
``Encontro Brasileiro em Teoria das Categorias''.
For more information on it, see:
\url{http://angg.twu.net/math-b.html\#2021-excuse-tt}
\newpage
{\bf Logic for Children / Categories for Children}
\ssk
Here I will refer a lot to:
\begin{enumerate}
\item \cite{PH1}: ``Planar Heyting Algebras for Children'' (E. Ochs,
SAJL, 2019). From its abstract:
\begin{quote}
In a wider context these ZHAs are interesting because toposes of
the form $\Set^{(P,A)}$ are one of the basic tools for doing
``Topos Theory for Children'', in the following sense. We can {\sl
define} ``children'' as people who think mathematically in a
certain way --- as {\sl people who prefer to start from particular
cases and finite examples that can be drawn explicitly,
\ColorRed{and only then generalize}} --- and we can define a
method for working on a particular case (less abstract, ``for
children'') and on a general case (``for adults'') in parallel,
using \ColorRed{parallel diagrams with similar shapes; we have
some ways of transfering knowledge from the general case to the
particular case, {\sl and back}. This method is sketched in the
introduction.}
\end{quote}
\item \cite{FavC}: ``On my favorite conventions for drawing the
missing diagrams in Category Theory''. Published on Arxiv in 2020...
\ColorRed{unpublishable?} From its abstract:
\begin{quote}
People in CT usually only share their ways of visualizing things
when their diagrams cross some threshold of mathematical
relevance --- and this usually happens when they \ColorRed{prove
new theorems} with their diagrams, or when they can show that
their diagrams can translate calculations that used to be huge
into things that are much easier to visualize. \ColorRed{The
diagrammatic language that I present here lies below that
threshold --- and so it is a ``private'' diagrammatic language,
that I am making public as an attempt to establish a dialogue
with other people who have also created their own private
diagrammatic languages.}
\end{quote}
\newpage
\item \cite{CWM2}: Mac Lane's ``Categories for the Working
Mathematician''. \ColorRed{The} standard text on CT. Very hard to
read --- should have 100 times more diagrams that it has, but they
are left to the reader. ``Normal'' people start from a state in
which CWM is impossible, then they switch to a state in which CWM is
\ColorRed{obvious}. I got stuck studying it in many. many, many
times. One of the main themes of \cite{FavC} is formalizing
``notions of obviousness'', and it ends with:
\begin{quote}
I am especially interested in how people write when they turn
their level-of-detail knob to a very high position.
\end{quote}
\newpage
\item Proof assistants based of Type Theory. From the introduction of
\cite{HOTT}:
\begin{quote}
Type theory (...) Although it is not generally regarded as the
foundation for classical mathematics, set theory being more
customary, type theory still has numerous applications, especially
in computer science and the theory of programming languages (...)
This is the basis of the system that we consider here; it was
originally intended as a rigorous framework for the formalization
of constructive mathematics.
\end{quote}
\newpage
\item Haskell. From its Wikipedia page:
\begin{quote}
At the conference on Functional Programming Languages and Computer
Architecture (FPCA '87) in Portland, Oregon, there was a strong
consensus that a committee be formed to define an open standard
for such languages. The committee's purpose was to consolidate
existing functional languages into a common one to serve as a
basis for future research in functional-language design.
\end{quote}
Haskell is based on a Type Theory that is simpler than the one in
HOTT, and many universities in Europe teach Haskell to first-year
students... so there is a lot of very readable material on it.
\item Idris: essentially Haskell plus \ColorRed{dependent types} and
other bells and whistles. Its type system is close enough to the one
in HOTT (from my beginner's point of view). Idris can be used as a
proof assistant, and the authors of \cite{IdrisCT2019} have
formalized some CT in Idris.
\item Discrete Mathematics. I taught DM for years, and a good part of
my students entered the university without knowing how to use
variables, and without knowing what is a theorem.
Their difficulties with learning new levels of abstraction were very
similar to my difficulties trying to learn Category Theory and Type
Theory.
I also gave some seminar courses whose pre-requisites were only
Discrete Mathematics (or not even that). I only found the right
approach for writing \cite{PH1} after these seminars --- they were
on $λ$-calculus, Heyting Algebras, S4, and Intuitionistic Logic
``for children'', using finite examples everywhere...
% «non-tautologies-1» (to ".non-tautologies-1")
%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
% (ph1p 10 "prop-calc")
% (ph1 "prop-calc")
% (ph1p 11 "prop-calc" "{\\sl not} a tautology")
% (ph1 "prop-calc" "{\\sl not} a tautology")
\def\und#1#2{\underbrace{#1}_{#2}}
$(P∨Q)→(P∧Q)$ is not a tautology:
%
$$\und{\und{\und{P}0 ∨ \und{Q}1}{1} → \und{\und{P}0 ∧\und{Q}1}{0}}{0}$$
\newpage
% «non-tautologies-2» (to ".non-tautologies-2")
% (ph1p 11 "prop-calc-ZHA")
% (ph1 "prop-calc-ZHA")
% (ph1p 12 "prop-calc-ZHA" "not tautologies in this ZHA")
% (ph1 "prop-calc-ZHA" "not tautologies in this ZHA")
%R local znotnotP =
%R 1/ T \
%R | . |
%R | . c |
%R |b . a|
%R | P . |
%R \ F /
%R local T = {F="⊥", T="⊤", a="P'", b="P''", c="→"}
%R znotnotP:tozmp({def="znotnotP", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R local zdemorgan =
%R 1/ T \
%R | o |
%R | . . |
%R |q . p|
%R | P Q |
%R \ a /
%R local T = {F="⊥", T="⊤", p="P'", q="Q'", a="∧", o="∨"}
%R zdemorgan:tozmp({def="zdemorgan", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse", scale="12pt", meta=nil}):addlrs():output()
%
%UB (¬ ¬ P) → P
%UB -- --
%UB 10 10
%UB ---
%UB 02
%UB -----
%UB 20
%UB -----------
%UB 12
%L
%L defub "notnotP"
%
%UB ¬(P ∧ Q) → (¬ P ∨ ¬ Q)
%UB -- -- -- --
%UB 10 01 10 01
%UB ----- --- ---
%UB 00 02 20
%UB ------- ---------
%UB 32 22
%UB ----------------------
%UB 22
%L
%L defub "demorgan"
%
Two classical tautologies that are not
intuitionistic tautologies:
$\pu
\hspace{-0.5cm}
\scalebox{0.75}{$
\begin{array}{ccccl}
\ohouse && \znotnotP && \mat{\ub{notnotP}} \\ \\
&& \zdemorgan && \mat{\ub{demorgan}} \\
\end{array}
$}
$
\newpage
% «non-tautologies-3» (to ".non-tautologies-3")
The connection with S4 and (order) topologies
% (ph1p 32 "topologies-as-HAs")
% (ph1 "topologies-as-HAs")
% (ph1p 33 "topologies-as-HAs" "``topological'' way")
% (ph1 "topologies-as-HAs" "``topological'' way")
\msk
%UB (¬ ¬ P) → P
%UB -- --
%UB 10 10
%UB ---
%UB 02
%UB -----
%UB 20
%UB -----------
%UB 12
%L
%L defub "ntntP -> P"
%
%UB (¬ ¬ P ) → P
%UB ------- -------
%UB \h00010 \h00010
%UB --------
%UB \h00101
%UB ---------
%UB \h01010
%UB ----------------------
%UB \h00111
%L
%L defub "ntntP -> P : houses"
%L
$\pu
\ub{ntntP -> P}
\qquad
\qquad
\def\h{\dagHouse}
\ub{ntntP -> P : houses}
$
\end{enumerate}
% (favp 2 "missing-diagrams")
% (fav "missing-diagrams")
\newpage
% «discrete-bmos» (to ".discrete-bmos")
% (lod21p 12 "discrete-bmos")
% (lod21 "discrete-bmos")
{\bf A trick for teaching Discrete Mathematics}
\ssk
$\bbA$ is our set of \ColorRed{atoms:}
the integers plus $\True$ and $\False$ (and later also ascii strings)
\msk
$\bbB$ is our set of basic mathematical objects:
$\bbB$ contains $\bbA$, and is closed by
forming \ColorRed{finite} sets and by forming \ColorRed{finite} lists
(a \ColorRed{finite} number of times)
\msk
In the first part of the course all objects that we \ColorRed{build}
are elements of $\bbB$. We use $\N$, $\Z$, $\Q$ and $\R$ sometimes,
but expressions like $\N×\N$ and $a∈\N.a^2≥a$ only appear
in the second part of the course.
\msk
\ColorRed{Why?}
\newpage
% «calculating» (to ".calculating")
% (lod21p 13 "calculating")
% (lod21 "calculating")
% (lodp 4 "dm-layers" "Calculating")
% (lod "dm-layers" "Calculating")
% (lodp 5 "dm-layer-1" "Calculating")
% (lod "dm-layer-1" "Calculating")
{\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")
% (lod21p 14 "set-comprehensions")
% (lod21 "set-comprehensions")
% (lodp 6 "set-comprehensions")
% (lod "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}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\{\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
In the rest of the talk I will use diagrams from...
\msk
\cite{IDARCT}:
\url{http://angg.twu.net/math-b.html\#idarct}
\url{http://angg.twu.net/LATEX/idarct-preprint.pdf}
\msk
\cite{PH1}:
\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}
\url{http://angg.twu.net/LATEX/2017planar-has-1.pdf}
\msk
\cite{FavC}:
\url{http://angg.twu.net/math-b.html\#favorite-conventions}
\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}
\newpage
% «links-to-fav» (to ".links-to-fav")
% (favp 2 "toc")
% (fav "toc")
% (favp 8 "the-conventions")
% (fav "the-conventions")
% (favp 11 "to-deserve-a-name")
% (fav "to-deserve-a-name")
% (favp 11 "to-deserve-a-name" "term inference")
% (fav "to-deserve-a-name" "term inference")
% (favp 14 "freyd")
% (fav "freyd")
% (favp 16 "freyd-with-functors")
% (fav "freyd-with-functors")
% (favp 16 "freyd-with-functors" "universalness")
% (fav "freyd-with-functors" "universalness")
% (favp 19 "internal-views")
% (fav "internal-views")
% (favp 19 "reductions")
% (fav "reductions")
% (favp 24 "internal-view-adjunction")
% (fav "internal-view-adjunction")
% (favp 29 "basic-example-as-skel")
% (fav "basic-example-as-skel")
% (favp 29 "basic-example-full")
% (fav "basic-example-full")
% «links-about-core» (to ".links-about-core")
% (find-books "__comp/__comp.el" "marlow-peyton-jones")
% (find-books "__logic/__logic.el" "altenkirch-dtwos" "sugar")
% (find-bradytddpage (+ 26 83) "3.4.2 Bound and unbound implicits")
% (find-bradytddtext (+ 26 83) "3.4.2 Bound and unbound implicits")
% https://dl.acm.org/doi/10.1145/1190315.1190324
% (find-pdf-page "~/books/System_F_with_type_equality_coercions.pdf")
% (find-pdf-text "~/books/System_F_with_type_equality_coercions.pdf")
% Rings
%
% Abuses of language
\cite{HOTT}
\cite{HaskellCore}
\cite{Kamareddine}
\cite{Sommaruga}
% (find-books "__logic/__logic.el" "hott")
\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021logicday veryclean
make -f 2019.mk STEM=2021logicday pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "lod21"
% End: