|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2014istanbul-a.tex")
% (find-dn4ex "edrx08.sty")
% (find-LATEX "2014-1-GA-P2-gab.tex")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && lualatex --output-format=dvi 2014istanbul-a.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && lualatex 2014istanbul-a.tex"))
% (defun d () (interactive) (find-dvipage "~/LATEX/2014istanbul-a.dvi"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2014istanbul-a.pdf"))
% (defun l () (interactive) (find-LATEX "2014istanbul-a.lua"))
% (defun t () (interactive) (find-LATEX "2014istanbul-a.tex"))
% (find-dvipage "~/LATEX/2014istanbul-a.dvi")
% (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
% (find-twusfile "LATEX/" "2014istanbul-a")
% http://angg.twu.net/LATEX/2014istanbul-a.pdf
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
%\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\usepackage{luacode}
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
% (find-dn4ex "edrxdefs.tex")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\begin{document}
% (find-angg ".emacs" "find-texbookpage")
% (find-texbookpage (+ 12 427))
\def\bsk{\bigskip}
\def\msk{\medskip}
\def\ssk{\smallskip}
\def\N{\mathbb{N}}
\def\Pyr#1#2#3{{}_{#1}{}^{#2}{}_{#3}}
\def\Opens{\mathcal{O}}
\def\Top{\top}
\def\Bot{\bot}
\def\Set{\mathbf{Set}}
\catcode`*=13 \def*{\ensuremath{\bullet}}
{\bf Logic and Categories}
Eduardo Ochs
UniLog 2015
(Version: 2014Sep15 4:32)
\bsk
One way to explain intuitionistic logic to a non-logician is this. The
usual truth-values are just 0 and 1, and we will change that by
decreeing that the new truth-values will be certain diagrams with
several 0s and 1s. We choose a subset of $D$ of $\N^2$, for example
$\Pyr***$, and we say that a {\sl modal truth-value on $D$} is a way
of assigning 0s and 1s to the points of $D$. A modal truth value is
{\sl unstable} when it has a 1 immediately above a 0, for example
$\Pyr110$ is unstable, and an {\sl intuitionistic truth-value on $D$}
is a stable modal truth-value on $D$. Now that we have defined our
(intuitionistic) truth-values we explain to our non-logician friend
how to interpret $\Top$, $\Bot$, $\land$, $\lor$, $\to$ on them, and
we show that if $P=\Pyr101$ then $P \neq \neg\neg P = \Pyr111$, and
some other classical theorems also do not hold. We then explain some
logical axioms and rules that do hold in this system, define
intuitionistic propositional logic from them, show how this particular
case based on $D$ generalizes, present the standard terminology, and
so on.
When we do this we are using several tricks -- finding an insightful
particular case, doing things in the particular and in the general
cases in parallel using diagrams with the same shapes, lifting proofs
from the particular case to the general one --, and this dydactical
method can be defined precisely. In the terminology of [1] this logic
on subsets of $\N^2$ and DAGs on them (ZSets and ZDAGs) is an {\it
archetypal model} for intuitionistic propositional logic (``IPL'').
If we abbreviate ``explaining and formalizing (something) via an
archetypal model'' as ``(that something) for children'', then the
contents of the tutorial become easy to state.
\msk
% ( {\it Heyting Algebras for Children}. The stable assignments of 0s
% and 1s to the points of a ZDAG D correspond the open sets in the
% order topology of D, and any topology has a natural Heyting Algebra
% structure on it, i.e., we can define the logical connectives there
% in a way that they will obey all the expected (intuitionistic)
% logical rules. )
{\it Heyting Algebras for children}. When a ZDAG $D$ doesn't have
three independent points, then the open sets of $(D, \Opens(D))$ are
in bijection with the {\sl points} of another ZDAG, $D'$. This $D'$ is
a Heyting Algebra, and our way of interpreting Intuitonistic Predicate
Logic on open sets of $D$ translates into a way of interpreting IPL on
the {\sl points} of $D'$. The operation $D \mapsto D'$ gives us lots
of examples of {\sl planar} Heyting Algebras -- but not all.
Take any ZDAG $D$ whose points all have the same parity. There is a
simple, visual criterion that can tell us very quickly whether $D$ is
a HA or not. The {\sl ZHAs} are the $D$s that obey this criterion and
the parity condition; an arbitrary ZDAG $D$ is a HA iff it is
isomorphic to a ZHA, and this is also easy to check. This gives us all
planar Heyting Algebras.
There is a system of coordinates that we can put on a ZHA -- the
$(l,r)$ coordinates -- that make $\Top$, $\Bot$, $\land$, $\lor$,
$\to$ trivial to calculate. We will present a computer library that
does all these calculations, and that can produce ascii and \LaTeX{}
diagrams for both ZDAGs and functions on them.
% logical connectives on open sets of $D$ translates into a way of
% interpreting them
%
% by adapting to $D'$
%
% which means that
% we know how to interpret the logical connectives not only on
% $\Opens(D)$ but also on the points of $D'$ -- this $D'$ is Heyting
% Algebra, but not all ZDAGs are HAs.
% There is a simple, visual criterion that tells us whether any given
% ZDAG is or is not a HA. We define a {\sl (tidy) ZHA} as a ZDAG that
% obeys that criterion, and whose points all have the same parity; every
% ZDAG that is a HA is isomorphic to a tidy ZHA, and tidy ZHAs have a
% system of coordinates that make $\Top$, $\Bot$, $\land$, $\lor$, $\to$
% trivial to calculate on them. A {\sl ZHA} is a tidy ZHA;
% non-necessarily-tidy ZHA
%
% so we restrict our attention to them. ZHAs and
% functions on them are easy to represent in ascii diagrams and in
% \LaTeX, and we will present a computer library that does all the hard
% work of doing calculations on them for us.
\msk
{\it Heyting algebra modalities for children}. A {\sl modality} is an
operation ${}^*$ on the points of a HA obeying $P \vdash P^* = P^{**}$
and $(P \land Q)^* = P^* \land Q^*$. The operations
%
$B_\bot(P) = \neg\neg P$,
$B_Q(P) \mapsto ((P \to Q) \to Q)$,
$J_Q(P) = Q \lor P$,
$J^Q(P) = Q \to P$,
%
are modalities, and our computer library can show visually how they
behave on the points of a ZHA and how they can be composed in several
ways (as in [Fourman79], p.331) to obtain new modalities.
The usual way of presenting HA modalities in the literature is by
showing first some basic consequences of the axioms, then how
modalities interact with $\land$, $\lor$, $\to$, then theorems about
how the algebra of modalities behave; I have always found this
aaproach quite opaque. By using ZHAs we can explain these theorems and
exhibit conter-models for all non-theorems visually -- and it turns
out that modalities on a ZHA $D$ correspond to ways of cutting $D$
into equivalence classes using diagonal lines. This visual way of
thinking {\sl complements} the usual formal way... but how, exactly?
{\sl Can we make that precise?}
% -- for example,
% $P \mapsto \neg\neg P$, $P \mapsto Q \lor P$, $P \mapsto ((P \to Q)
% \to Q)$ are modalities --, how different modalities interact with one
% another (as in [Fourman79], p.331), and what basic statements about
% modalities are theorems or non-theorems. An amazing fact is that
% modalities on a ZHA $D$ correspond exactly to quotients on $D$
% obtained by cutting $D$ along diagonal lines.
\msk
{\it Categories for children}. For our purposes, the archetypal
category is $\Set$, and in most examples we can use only finite
subsets of $\N$ as its objects in diagrams. This lets us introduce
quickly two flavors of typed $\lambda$-calculus, the distinction
between {\sl structure} and {\it properties}, a trick to focus only on
structure and leave the ``properties'' part for a second moment, and a
way to regard having a terminal, binary products, and exponentials --
the cartesian-closed structure -- as extra structure on $\Set$. A {\sl
CCC} is a category with that extra structure, and by regarding
$\Set$ as the archetypal case we get a way to interpret the
simply-typed $\lambda$-calculus formally in any CCC.
It turns out that ZDAGs are categories, and ZHAs are CCCs, both
archetypal in slightly weaker ways than $\Set$. By interpreting
$\lambda$-calculus in ZHAs and making a series of changes in the
notation we get the categorical interpretation of intutionistic
predicate calculus, plus Natural Deduction, and Curry-Howard.
\msk
{\it Toposes for children}. Let $D$ be a ZDAG; for example,
$D=\Pyr***$. The category of functors $\Set^D$ is a topos -- a {\sl
ZTopos}, and its objects are $\Pyr***$-shaped diagrams that are easy
to draw explicitly. CCCs are categories with extra structure that lets
us interpret simply-typed $\lambda$-calculus on them; toposes are CCCs
with extra structure, that lets us interpret {\sl Intuitionistic Set
Theory} (IST) on them. By regarding both $\Set$ and our `$\Set^D$'s
as archetypal toposes we can start topos theory from the ``internal
language'', i.e., from the way of interpreting all operations of IST
in terms of basic categorical operations; our approach lets us begin
by examples that show how each operation of IST ought to behave, then
guessing a formalization, than proving that it works and thus toposes
are models for IST, then proving other facts about toposes that are
less logical and more algebraic in character.
\msk
{\it Sheaves for children}. Each modality on a Heyting Algebra $D'$
induces a notion of ``sheafness'' on a ZTopos, plus a quotient from it
into a ``smaller'' topos, which has an adjoint that is a functor from
the ``smaller'' topos back into the ``bigger'' one; the ``sheaves''
are the objects of $\Set^{D'}$ that are in the image of that adjoint
functor.
Using ZToposes as our archetypal toposes we can understand how all
these entities and definitions behave by generalizing a few examples
where the diagrams are not too big. One nice example -- of the {\sl
logical} definition of sheaf -- shows how the notion of sheafness
induced by $B_\bot$ booleanizes the logic of a topos; another example,
motivated by the {\sl topological} definition of sheaf, shows how
sheafification and \'etalification are adjoint functors, using an
order topology.
\msk
The possibilities for exposing tecnicalities using archetypal cases
are endless, but we will dedicate the best part of our energy in this
tutorial not to them, but to something more general and more useful:
how to use archetypal cases to make the literature more accesible, and
to create bridges between different notations.
\bsk
\bsk
References:
[Fourman1979]: "Sheaves and Logic" - in SLNM 0753
% (find-LATEX "catsem.bib" "Fourman")
% (find-books "__cats/__cats.el" "fourman")
% (code-xpdf "slnm0753" "~/books/__cats/fourman_mulvey_scott_eds__applications_of_sheaves_slnm0753.pdf")
[Ochs2013]: "Internal Diagrams and Archetypal Reasoning in Category
Theory" - in Logica Universalis
% (find-angg ".emacs" "idarct")
\newpage
\directlua{
dofile "2014istanbul-a.lua" -- (find-LATEX "2014istanbul-a.lua")
}
% \def\luaexpr#1{\directlua{tex.print(#1)}}
% \luaexpr{print(bigstr2)}
% \luaexpr{bigstr2:gsub("\n", "")}
\input 2014istanbul-a.inc
{\footnotesize \it (Notes for myself - other people should ignore this)}
\msk
\Basic\Intpl\Toposes
\end{document}
% [SETHEADSTYLE [LUCIDA]]
% [lua:
% def [[ -- 0 _ "–" ]]
% def [[ * 0 _ "•" ]]
% def [[ D 0 _ IT"D" ]]
% def [[ D' 0 _ IT"D'" ]]
% def [[ N 0 _ IT"N" ]]
% def [[ N 0 _ "ℕ" ]]
% def [[ Opens 0 _ "𝒪" ]]
% def [[ Opens 0 _ IT"O" ]]
% def [[ Top 0 _ IT"T" ]]
% def [[ Bot 0 _ IT"F" ]]
% def [[ Top 0 _ "⊤" ]]
% def [[ Bot 0 _ "⊥" ]]
% def [[ vdash 0 _ "|-" ]]
% def [[ vdash 0 _ "⊢" ]]
% def [[ vdash 0 _ "≤" ]]
% def [[ msk 0 _ br() ]]
% def [[ Set 0 _ BF"Set" ]]
% def [[ lambda 0 _ "λ" ]]
% def [[ b 0 _ "B" ]]
% def [[ j 0 _ "J" ]]
%
% def [[ '' 1 s "‘$s’" ]]
% def [[ '''' 1 s "“$s”" ]]
%
% -- (find-equailfile "sgml-input.el")
% -- (find-equailgrep "grep -niH -e arrow sgml-input.el")
% def [[ land 0 _ "∧" ]]
% def [[ lor 0 _ "∨" ]]
% def [[ to 0 _ "→" ]]
% def [[ neq 0 _ "≠" ]]
% def [[ neg 0 _ "¬" ]]
% def [[ mapsto 0 _ "↦" ]]
% def [[ LaTeX 0 _ "LaTeX" ]]
%
% def [[ DEF 1 s IT(s) ]]
% def [[ SEC 1 s BF(s) ]]
% def [[ up 1 s "<sup>$s</sup>" ]]
% def [[ down 1 s "<sub>$s</sub>" ]]
% def [[ Pyr 3 a,b,c down(a)..up(b)..down(c) ]]
% -- (find-equailfile "sgml-input.el")
%
% sgmlify_table["\15"] = "•"
%
% ]
% [htmlize0 [J]
%
%
%
% [P [BF Logic and Categories]
% [BR] (or: [BF Planar Heyting Algebras for Children])
% [BR] [R http://angg.twu.net/math-b.html Eduardo Ochs]
% [BR] [MAILTO eduardoochs@gmail.com]
% [BR] UniLog 2015
% ]
%
%
%
% [P One way to explain intuitionistic logic to a non-logician is this.
% The usual truth-values are just 0 and 1, and we will change that by
% decreeing that the new truth-values will be certain diagrams with
% several 0s and 1s. We choose a subset [D] of [N][up 2], for example
% [Pyr [*] [*] [*]], and we say that a [DEF modal truth-value on [D]] is
% a way of assigning 0s and 1s to the points of [D]. A modal truth value
% is [DEF unstable] when it has a 1 immediately above a 0, for example
% [Pyr 1 1 0] is unstable, and an [DEF intuitionistic truth-value on
% [D]] is a stable modal truth-value on [D]. Now that we have defined
% our (intuitionistic) truth-values we explain to our non-logician
% friend how to interpret [Top], [Bot], [land], [lor], [to] on them, and
% we show that if [IT P] = [Pyr 1 0 1] then [IT P] [neq] [neg][neg][IT
% P] = [Pyr 1 1 1], and some other classical theorems also do not hold.
% We then explain some logical axioms and rules that do hold in this
% system, define intuitionistic propositional logic from them, show how
% this particular case based on [D] generalizes, present the standard
% terminology, and so on.]
%
% [P When we do this we are using several tricks [--] finding an
% insightful particular case, doing things in the particular and in the
% general cases in parallel using diagrams with the same shapes, lifting
% proofs from the particular case to the general one [--], and this
% dydactical method can be defined precisely. In the terminology of ['
% [Ochs2013]] this logic on subsets of [N][up 2] and DAGs on them (ZSets
% and ZDAGs) is an [DEF archetypal model] for intuitionistic
% propositional logic (['''' IPL]). If we abbreviate ['''' explaining
% and formalizing (something) via an archetypal model] as ['''' (that
% something) for children], then the contents of the tutorial become
% easy to state.]
%
% [msk]
%
% [P [SEC Heyting Algebras for children]. When a ZDAG [D] doesn't have
% three independent points, then the open sets of ([D], [Opens]([D]))
% are in bijection with the [IT points] of another ZDAG, [D']. This [D']
% is a Heyting Algebra, and our way of interpreting Intuitonistic
% Predicate Logic on open sets of [D] translates into a way of
% interpreting IPL on the [IT points] of [D']. The operation [D]
% [mapsto] [D'] gives us lots of examples of [IT planar] Heyting
% Algebras [--] but not all.]
%
% [P Take any ZDAG [D] whose points all have the same parity. There is a
% simple, visual criterion that can tell us very quickly whether [D] is
% a HA or not. The [DEF ZHAs] are the [D]s that obey this criterion and
% the parity condition; an arbitrary ZDAG [D] is a HA iff it is
% isomorphic to a ZHA, and this is also easy to check. This gives us all
% planar Heyting Algebras.]
%
% [P There is a system of coordinates that we can put on a ZHA [--] the
% ([IT l],[IT r]) coordinates [--] that make [Top], [Bot], [land], [lor],
% [to] trivial to calculate. We will present a computer library that
% does all these calculations, and that can produce ascii and [LaTeX]
% diagrams for both ZDAGs and functions on them.]
%
% [msk]
%
% [P [SEC Heyting algebra modalities for children]. A [DEF modality] is
% an operation [up *] on the points of a HA obeying [IT P] [vdash] [IT
% P][up *] = [IT P][up **] and ([IT P][land][IT Q])[up *] = [IT P][up
% *][land][IT Q][up *]. The operations
%
% [b][down [Bot]]([IT P]) = [neg][neg][IT P],
% [b][down [IT Q]]([IT P]) [mapsto] (([IT P][to][IT Q])[to][IT Q]),
% [j][down [IT Q]]([IT P]) = [IT Q][lor][IT P],
% [j][up [IT Q]]([IT P]) = [IT Q][to][IT P],
%
% are modalities, and our computer library can show visually how they
% behave on the points of a ZHA and how they can be composed in several
% ways (as in [' [FourmanScott79]], p.331) to obtain new modalities.]
%
% [P The usual way of presenting HA modalities in the literature is by
% showing first some basic consequences of the axioms, then how
% modalities interact with [land], [lor], [to], then theorems about how
% the algebra of modalities behave; I have always found this approach
% quite opaque. By using ZHAs we can explain these theorems and exhibit
% conter-models for all non-theorems visually [--] and it turns out that
% modalities on a ZHA [IT D] correspond to ways of cutting [IT D] into
% equivalence classes using diagonal lines. This visual way of thinking
% [IT complements] the usual formal way... but how, exactly? [IT Can we
% make that precise?]]
%
% [msk]
%
% [P [SEC Categories for children]. For our purposes, the archetypal
% category is [Set], and in most examples we can use only finite subsets
% of [N] as its objects in diagrams. This lets us introduce quickly two
% flavors of typed [lambda]-calculus, the distinction between [IT
% structure] and [IT properties], a trick to focus only on structure and
% leave the ['''' properties] part for a second moment, and a way to
% regard having a terminal, binary products, and exponentials [--] the
% cartesian-closed structure [--] as extra structure on [Set]. A [DEF
% CCC] is a category with that extra structure, and by regarding [Set]
% as the archetypal case we get a way to interpret the simply-typed
% [lambda]-calculus formally in any CCC.]
%
% [P It turns out that ZDAGs are categories, and ZHAs are CCCs, both
% archetypal in slightly weaker ways than [Set]. By interpreting
% [lambda]-calculus in ZHAs and making a series of changes in the
% notation we get the categorical interpretation of intutionistic
% predicate calculus, plus Natural Deduction, and Curry-Howard.]
%
% [msk]
%
% [P [SEC Toposes for children]. Let [IT D] be a ZDAG; for example, [D]
% = [Pyr [*] [*] [*]]. The category of functors [Set][up [IT D]] is a
% topos [--] a [DEF ZTopos], and its objects are [Pyr [*] [*]
% [*]]-shaped diagrams that are easy to draw explicitly. CCCs are
% categories with extra structure that lets us interpret simply-typed
% [lambda]-calculus on them; toposes are CCCs with extra structure, that
% lets us interpret [DEF Intuitionistic Set Theory] (IST) on them. By
% regarding both [Set] and our ['' [Set][up [IT D]]]s as archetypal
% toposes we can start topos theory from the ['''' internal language],
% i.e., from the way of interpreting all operations of IST in terms of
% basic categorical operations; our approach lets us begin by examples
% that show how each operation of IST ought to behave, then guessing a
% formalization, than proving that it works and thus toposes are models
% for IST, then proving other facts about toposes that are less logical
% and more algebraic in character.]
%
% [msk]
%
%
%
% [P [SEC Sheaves for children]. Each modality on a Heyting Algebra [IT
% D]' induces a notion of ['''' sheafness] on a ZTopos, plus a quotient
% from it into a ['''' smaller] topos, which has an adjoint that is a
% functor from the ['''' smaller] topos back into the ['''' bigger] one;
% the ['''' sheaves] are the objects of [Set][up [IT D]'] that are in the
% image of that adjoint functor.]
%
% [P Using ZToposes as our archetypal toposes we can understand how all
% these entities and definitions behave by generalizing a few examples
% where the diagrams are not too big. One nice example [--] of the [IT
% logical] definition of sheaf [--] shows how the notion of sheafness
% induced by [b][down [Bot]] booleanizes the logic of a topos; another
% example, motivated by the [IT topological] definition of sheaf, shows
% how sheafification and étalification are adjoint functors,
% using an order topology.]
%
% [msk]
%
% [P The possibilities for exposing tecnicalities using archetypal cases
% are endless, but we will dedicate the best part of our energy in this
% tutorial not to them, but to something more general and more useful:
% how to use archetypal cases to make the literature more accesible, and
% to create bridges between different notations.]
%
%
%
% [msk]
% [msk]
%
% [P References:]
%
% [P [' [FourmanScott1979]]: M.P. Fourman, D.S. Scott: [IT Sheaves and
% Logic] - in [IT Applications of Sheaves] (Springer Lecture Notes in
% Mathematics 753), pp.302-401]
%
% [P [' [Ochs2013]]: E. Ochs: [IT Internal Diagrams and Archetypal
% Reasoning in Category Theory] - in Logica Universalis, vol 7, issue 3,
% pp.291-321]
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: