|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
* COMMENT el
# (find-istfile "glyphs.el")
#
# (load "~/LATEX/istanbulglyphs.el")
# (eev-uc-set-composes)
# (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
* -defs
# (find-istfile "quotes.tex" "\\def\\BF")
\def\BF#1{\noindent{\bf#1}\quad}
\def\liml{\underleftarrow {\lim}{}}
\def\limr{\underrightarrow{\lim}{}}
\def\frakCat{\mathfrak{Cat}}
\def\frakTop{\mathfrak{Cat}}
\def\elephantpage#1{((page #1))}
\def\ob{{\operatorname{ob}}}
\def\sh{\mathbf{sh}}
\def\Sh{\mathbf{Sh}}
\def\Sp{\mathbf{Sp}}
\def\Lop{\mathbf{Lop}}
\def\Hom{\mathrm{Hom}}
\def\sdd{\ssk{\scriptsize (...)}\ssk}
\def\mdd{\msk{\scriptsize (...)}\msk}
* -title
{\bf Logic and Categories, or:
Heyting Algebras for Children}
A tutorial presented at the UniLog 2015 conference (Istanbul),
June 20-22, 2015
\msk
By Eduardo Ochs
{\tt eduardoochs@gmail.com}
\url{http://angg.twu.net/math-b.html#istanbul}
\msk
Version: 2015jun22
* ---
* TEXED :big: (Non-mathematical) introduction
\bsk
** TEXED Why study CT {\sl now}?
\includegraphics[width=8.5cm]{garota_de_ipanema.jpg}
\par Public education in Brazil is being dismantled -
\par maybe we should be doing better things than studying
\par very technical \& inaccessible subjects
\par with no research grants -
** TEXED Category theory should be more accessible
\par Most texts about CT are for specialists in research universities...
\par {\sl Category theory should be more accessible.}
\msk
\par To whom?...
\begin{itemize}
\item Non-specialists (in research universities)
\item Grad students (in research universities)
\item Undergrads (in research universities)
\item Non-specialists (in conferences - where we have to be quick)
\item Undergrads (e.g., in CompSci - in teaching colleges) - (``Children'')
\end{itemize}
** DONE What do we mean by "accessible"?
1) Done on very firm grounds:
mathematical objects made from numbers, sets and tuples
FINITE, SMALL mathematical objects whenever possible
avoid references to non-mathematical things like
windows, cars and pizzas (like the OO people do)
avoid reference to Physics - avoid QM at all costs
time is difficult to draw - prefer static rather than changing
2) People have very short attention spans nowadays
3) Self-contained, but not isolated or isolating -
our material should make the literature more accessible
4) We learn better by doing.
Our material should have lots of space for exercises.
5) Most people with whom I interact are not from Maths/CS/etc
6) Proving general cases is relatively hard.
Checking and calculating is much easier.
People can believe that something can be generalized after
seeing a convincing particular case.
(Sometimes leave them to look for the right generalization
by themselves)
** DONE Generalizations
General case Full things
| ^ | ^
projection | : lifting projection | : lifting
v : v :
Particular case Things for children
Paper:
Internal Diagrams and Archetypal Reasoning in Category Theory
Eduardo Ochs 2103 - Logica Universalis
http://angg.twu.net/ <- my home page
http://angg.twu.net/math-b.html
http://angg.twu.net/math-b.html#idarct
The type-theorical view of the formalization of all that
is something that I can discuss with very few people =(
The parts "for children" are more fun
(esp. because I don't have to do them alone)
so I have to get good excuses for working on that
instead of on the very technical type-theoretical parts
** DONE Yesterday and slides
To do: apologize for yesterday
I overestimated my TeXnical skills!!! =(
Some of my diagrams need LuaLaTeX extensions
that took me _much_ longer to write than I expected,
and the emergency tools that let me use ascii+utf8 slides
also took me one (_very_ frantic) day more than I had -
...so things were not ready yesterday - and as I could not
connect my computer directly to the projector, and I did not
have enough material in PDF form, I had to cancel -
These ascii slides will be at
http://angg.twu.net/math-b.html
soon.
Nice (Lua)(La)TeXed slides should be ready soon,
for some adequate, not-very-small value of "soon".
* ---
* :big: The very basics
** DONE Evaluation: steps
# (find-es "tex" "underbrace")
How do we evaluate an expression like 2*3+4*5
to obtain its value, 26?
This involves a series of steps...
There are several ways to represent these steps:
2*3+4*5 2*3+4*5 -> 2*3+20
\-/ \-/ | |
6 20 v v
\-----/ 6+4*5 ---> 6+20 --> 26
26
2*3+4*5 = 2*3+20
2*3+4*5 = 6+20 = 6+20
= 26 = 26
The technical term for the arrows is ``reductions''.
Informally, they are ``evaluation steps''.
** DONE Evaluation sequences
2*3+4*5 2*3+4*5 -> 2*3+20
\-/ \-/ | |
6 20 v v
\-----/ 6+4*5 ---> 6+20 --> 26
26
2*3+4*5 = 2*3+20
2*3+4*5 = 6+20 = 6+20
= 26 = 26
To evaluate is to reduce, and reduce, and reduce
until there is nothing more to do - until we reach
someting that is ``fully evaluated''.
Note that two ``evaluation sequences'' starting
at the same expression may ``diverge'' at some point,
but they necessarily ``converge'' later - this is
what assures us that the result of evaluation is
unique.
(Technical terms: ``confluence'', ``diamond lemma'',
``normalization''...)
** DONE Algebra: tables
Some expressions, e.g. (a+b)(a-b) and a*a-b*b,
return equal values for all inputs...
We can /test/ whether (a+b)(a-b)=a*a-b*b
in a /finite number/ of cases using tables,
a b (a+b)(a-b) a*a-b*b (a+b)(a-b)=a*a-b*b
------------------------------------------------
0 0 0 0 T
2 3 -5 -5 T
10 1 99 99 T
but we can not /know/ that (a+b)(a-b)=a*a-b*b
just by checking a finite number of table lines...
** DONE Algebra: reductions
To understand why (a+b)(a-b)=a*a-b*b we need /algebra/,
which includes reductions like these, which use associativity
always in the "expansion" direction, i.e., x(y+z)->xy+xz,
(a+b)(a-b) -> (a+b)a-(a+b)b -> (a+b)a-ab-bb
| | |
| v v
| aa+ba-(a+b)b -> aa+ba-ab-bb
| :
v :
a(a-b)+b(a-b) -> a(a-b)+ba-bb :
| | :
v v v
aa-ab+b(a-b) -> aa-ab+ba-bb - - -> aa-bb
...but then we don't get confluence!
To get the two "- - ->" arrows we need
commutativity of + and ·, plus x-x=0...
We need several new things to learn how to do
"calculations with letters"!...
We can teach evaluation to small children.
We can only teach algebra to /older/ children,
who have already learned evaluation.
The important thing:
evaluation comes first,
algebra comes later.
** DONE Logic: evaluation and tautologies
Logic is simpler than algebra (for children),
because we can prove lots of things just by
looking at tables with a finite number of lines.
For example, we can check that P&Q->P∨Q just by
calculating the result of P&Q->P∨Q in all four cases.
(P -> Q)∨(Q -> P) P Q P->Q Q->P (P->Q)∨(Q->P)
\-/ \-/ \-/ \-/ -------------------------------
0 1 1 0 0 0 1 1 1
\------/ \------/ 0 1 1 0 1
1 0 1 0 0 1 1
\--------------/ 1 1 1 1 1
1
P Q P&Q P∨Q P->Q
--------------------
0 0 0 0 1
0 1 0 1 1
1 0 0 1 0
1 1 1 1 1
When we teach logic to children it is
good karma to spend a LONG time on this:
what propositions are tautologies?
** DONE A glimpse at other logics
The truth values of classical logic are {0,1}.
The truth values of O(2)-logic are {00,01,11}.
Some propositions, like ¬¬P->P, are tautologies
in classical logic but not in O(2)-logic...
P Q P&Q P∨Q P->Q P ¬P ¬¬P ¬¬P->P
-------------------- ------------------
00 00 00 00 11 00 11 00 11
00 01 00 01 11 01 00 11 01
00 11 00 11 11 11 00 11 11
01 00 00 01 00
01 01 01 01 11
01 11 01 11 11
11 00 00 11 00
11 01 01 11 01
11 11 11 11 11
** DONE $λ$-calculus: subtopics
Lambda-calculus, even for children, is a big topic...
We will see it as this series of subtopics:
* the usual way of defining (named) functions
* the meaning of `:' and `->' in f:A->B
* the meaning of `|->'
* evaluation, a.k.a., reduction
* lambda-notation
* beta-reduction
* the diamond lemma
* name clashes
* pairing and projection
* types
* contexts, pre-judgments and judgments
* unions of contexts
* type inference
* Set as model for lambda1
** DONE Defining named functions
The usual notation for defining functions is like this:
f: N -> R (*)
n |-> 2+sqrt(n)
name: domain -> codomain
variable |-> expression
It creates _named_ functions.
To use this notation we have to fill up five slots,
and use a ":", an "->" and a "|->" in the right places.
After stating (*) we can "reduce" expressions with f, like this:
f(4+5) ---> 2+sqrt(4+5)
: :
: :
v v
f(9) ---> 2+sqrt(9) ---> 2+3 ---> 5
** DONE $λ$-calculus: defining unnamed functions
Now compare
name: domain -> codomain
variable |-> expression name = \variable.expression
g: N -> R
a |-> a*a+4 h = \a.a*a+4
g(2+3) -----------> g(5) h(2+3) ------------> h(5)
| | | |
| | v v
| | (\a.a*a+4)(2+3) ---> (\a.a*a+4)(5)
| | | |
v | v |
(2+3)*(2+3)+4 | (2+3)*(2+3)+4 |
| \ | | \ |
| v | | v |
| (2+3)*5+4 | | (2+3)*5+4 |
| \ | | \ |
v v v v v v
5*(2+3)+4 -----> 5*5+4 5*(2+3)+4 -----> 5*5+4
Note that the parentheses are important...
2+3*2+3+4 != (2+3)*(2+3)+4
Note also that in h = \a.a*a+4 we have not used
neither the domain nor the codomain...
** DONE Functions as lists of `$\mapsto$'s
Functions can be regarded as sets of (input,output) pairs.
For example,
f:{4,5,6} -> R
a |-> 10a
_is_ the set {(4,40),(5,50),(6,60)}.
Just as we saw to fully evaluate expressions like 2·3+4·5 -
the _value_ of 2·3+4·5 is 26 because on numbers there are
no futher evaluation steps to be done -
the _value_ of the f above is {(4,40),(5,50),(6,60)}.
Alternative notations:
\csm{(4,40), && (5,50), && (6,60)} =
\csm{4↦40, && 5↦50, && 6↦60} =
\csm{4↦40 && 5↦50 && 6↦60} =
\sm {4↦40 && 5↦50 && 6↦60}
We will be sloppy with commas in the {}/↦ notation.
** DONE Trees
We are going to use tree for lots of things, e.g.:
represent constructions
compare general and particular cases (with parallel trees)
add and erase information
track free variables / undischarged hypotheses
understand translations (including Curry-Howard)
p (-2,5) (-2,5)
--- -------- ------
p π'p f (-2,5) π'(-2,5) sqrt (-2,5) 5 sqrt
-- ------ ------- -------------- ------ ---------
πp f(π'p) π(-2,5) sqrt(π'(-2,5)) -2 sqrt(5)
----------- ------------------------ ------------------
(πp,f(π'p)) (π(-2,5),sqrt(π'(-2,5))) (-2,sqrt(5))
p:A×B (-2,5)∈Z×N
----- ----------
p:A×B π'p:B f:B->C (-2,5)∈Z×N 5∈N sqrt:N->R
----- -------------- ---------- -----------------
πp:A f(π'p):C -2∈Z sqrt(5)∈R
---------------- ----------------------------
(πp,f(π'p)):A×C (-2,sqrt(5))∈Z×R
** DONE Trees: free variables, discharges, sequents, Curry-Howard...
----
[p]^1 p|-p [P&Q]^1
----- ---- ------ ---- -------
[p]^1 π'p f p|-p p|-π'p f|-f [P&Q]^1 Q Q->R
----- ------ ----- ------------ ------- -----------
πp f(π'p) p|-πp f,p|-f(π'p) P R
------------- -------------------- ---------------
(πp,f(π'p)) f,p|-(πp,f(π'p)) P&R
--------------1 ------------------ --------1
λp.(πp,f(π'p)) f|-λp.(πp,f(π'p)) P&Q->P&R
p:A×B
----- ------------
p:A×B π'p:B f:B->C p:A×B|-π'p:B f:B->C
----- -------------- ----------- ---------------------
πp:A f(π'p):C p:A×B|-πp:A p:A×B|-f(π'p):C
---------------- -------------------------------
(πp,f(π'p)):A×C p:A×B|-(πp,f(π'p)):A×C
---------
π':A×B->B f:B->C
-----------------
π:A×B->A f∘π':A×B->C
-------------------------
\ang{π,f∘π):A×B->A×C
** DONE Alice's logic and Bob's logic
(For students of Discrete Mathematics)
Our friends Alice and Bob have both publish books on logic,
with some stylistic differences...
For Alice, Classical Propositional Logic is this,
(Ω,⊤,⊥,∧,∨,→,¬,↔) =
({0,1}, 1, 0, {(0,0)↦0, {(0,0)↦0, {(0,0)↦1, {0↦1, {(0,0)↦1, }
(0,1)↦0, (0,1)↦1, (0,1)↦1, 1↦0}, (0,1)↦0,
(1,0)↦0, (1,0)↦1, (1,0)↦0, (1,0)↦0,
(1,1)↦1 }, (1,1)↦1 }, (1,1)↦1 }, (1,1)↦1 }
In Bob's book, Classical Propositional Logic is
(Ω,⊤,∧,¬) = ...
with all the other operators being defined from this one...
How do we translate from one of these notions to another?
Suppose that Alice's book has a theorem that is not in Bob's book.
We may need to translate both the /theorem/ and the /proof/.
At one point, when we were studying Alice's book and feeling that
we were on shaky ground, we thought of "∧" as being the 4th
component of the structure above...
A very low-level translation uses things like "4th component".
A higher-level translation refers to components by their names.
* ---
* :big: (Planar) Heyting Algebras for children
** DONE A game - on $N^2$
Let's consider a game played
on an infinite board, N^2,
with black and white pieces.
* This is a black piece.
It is solid. It is heavy.
It tends to sink.
/Black pieces move down/.
O This is a white piece.
It is hollow. It is light.
It tends to float.
/White pieces move up/.
Black moves: * (x,y) (0,y)
/|\ / | \ | \
v v v v v v v v
(x-1,y-1) (x,y-1) (x-1,y-1) (0,y-1) (1,y-1)
White moves: (x-1,y+1) (x,y+1) (x-1,y+1) (0,y+1) (1,y+1)
^ ^ ^ ^ ^ ^ ^ ^
\|/ \ | / | /
O (x,y) (0,y)
Note that moves are only possible
between /valid positions/ -
this rules out positions with x=-1.
** DONE A game - on subsets of $N^2$
Let's consider a game played
on an infinite board, N^2,
with black and white pieces...
Note that moves are only possible
between /valid positions/ -
this rules out positions with x=-1.
We may restrict the
valid positions even more.
Let A ⊆ N^2.
Let BM(A) be the set of black moves
starting and ending on points of A, and
let WM(A) be the set of white moves
starting and ending on points of A.
Then BM(A) and WM(A) are sets of arrows,
and (A,BM(A)) and (A,WM(A)) are graphs.
(A,BM(A)) and (A,WM(A)) are directed,
acyclical graphs - DAGs.
** DONE A game - on $K$
Let K ("Kite") be this subset of N^2:
K = {(1,3),(0,2),(2,2),(1,1),(1,0)}
Then (K,BM(K)) is the DAG at the left below,
which is isomorphic to the DAG K' at the right...
(1,3) 1
/ \ / \
v v v v
(0,2) (2,2) 2 3
\ / \ /
v v v v
(1,1) 4
| |
v v
(0,0) 5
(K,BM(K)) = ({(1,3), (0,2),(2,2), (1,1), (1,0)},
{((1,3),(0,2)), ((1,3),(2,2)),
((0,2),(1,1)), ((2,2),(1,1)),
((1,1),(0,0))})
K' = ({1, 2,3, 4, 5},
{(1,2),(1,3), (2,4),(3,4), (4,5)})
** DONE A game - definition aborted
When I talked about ``game'' that was a trick...
I just wanted to define BM(A) and WM(A) on an A ⊆ N^2.
We don't need notions like ``initial position'',
``turn'', ``winning'', etc.
From now on we will forget the idea of a ``game''.
** DONE Transitive-reflexive closure
Let (A,R) be a (directed) graph; note that R ⊆ A^2.
We will write
(A,R^+) for the transitive closure of (A,R), and
(A,R^*) for the transitive-reflexive closure of (A,R).
(A,R^+) is (A,R) ``plus all the identity arrows'',
(A,R^*) is (A,R^+) ``plus all the composites''.
Remember that when A ⊆ N^2
then (A,BM(A)) and (A,WM(A)) are DAGs...
When we pass to (A,BM(A)^*) and (A,WM(A)^*)
we don't get cycles - except for the identity maps!
(A,BM(A)^*) and (A,WM(A)^*) are directed,
``almost acyclical'' graphs...
More precisely, (A,BM(A)^*) and (A,WM(A)^*)
are /partial orders/!
** DONE Well-positioned subsets of $N^2$
Let A ⊆ N^2, and let (Δx,Δy) ∈ Z^2.
Let A' = {(x+Δx,y+Δy) | (x,y)∈A}.
Then (A,BM(A)) and (A',BM(A')) are isomorphic!
For example, if A=K and (Δx,Δy)=(80,90),
then (A,BM(A)) and (A',BM(A')) are:
(1,3) (81,93)
/ \ / \
v v v v
(0,2) (2,2) (80,92) (82,92)
\ / \ /
v v v v
(1,1) (81,91)
| |
v v
(0,0) (80,90)
We are only interested in the /graphs/
generated by subsets of N^2 - so let's
create a notion of ``canonical position''...
Also, we are only interested in the graphs
generated by /finite/, /nonempty/ subsets of N^2...
** DONE Well-positioned subsets of $N^2$ (2)
Definition:
a subset A of N^2 is /well-positioned/
when it contains a point of the form (0,y)
and a point of the form (x,0), i.e.,
it touches both axes, i.e.,
it can't be translated left or down
without going outside of N^2...
For any non-empty subset A of N^2,
there is exactly one (Δx,Δy)∈N^2
such that A-(Δx,Δy) is well-positioned.
(1,3) (81,93)
/ \ / \
v v v v
(0,2) (2,2) (80,92) (82,92)
\ / \ /
v v v v
(1,1) (81,91)
| |
v v
(0,0) (80,90)
** DONE ZSets
Definition:
A /ZSet/ is a finite, nonempty,
well-positioned subset of N^2.
The nice thing about ZSets is that
we can represent them unambiguously
using a bullet notation. For example,
*
* *
*
*
is {(1,3), (0,2), (2,2), (1,1), (0,0)}.
** DONE ZSets, ZDAGs, ZPosets
Definitions:
A /ZSet/ is a finite, nonempty, well-positioned subset of N^2.
A /ZDAG/ is a DAG (A,BM(A)) or (A,WM(A)), where A is a ZSet.
A /ZPoset/ is a poset (A,BM(A)^*) or (A,WM(A)^*), where A is a ZSet.
Examples:
Let H ("House") be this zset here:
*
* *
* *
then:
(H, BM(H)) and (H, WM(H)) are ZDAGs
(H, BM(H)^*) and (H, WM(H)^*) are ZPosets
** DONE Zfunctions
A Zfunction is a function whose domain is a ZSet.
We can represent Zfunctions using a positional notation.
For example, with K={(1,3), (0,2),(2,2), (1,1), (1,0)},
the function f:K->N such that
f = {((1,3),1), ((0,2),2),((2,2),3), ((1,1),4), ((1,0),5)}
can be represented as:
1
2 3
4
5
Note that its domain, K, can be inferred from the shape
*
* *
*
*
but its codomain has to be deduced from the context.
** DONE The reading order
The /reading order/ for a ZSet A
is the bijection from A to {1, 2, ..., |A|}
that enumerates the elements of A from top
to bottom, going from left to right in each line.
Here are some reading orders:
1
1 1 2 3
2 3 2 3 4 5
4 4 5 6 7 8 9
The reading order can be used to formalize
a way to ``read aloud'' Zfunctions. For example,
we can read aloud
3
2 40
1 50
as 3, 2, 40, 1, 50.
(And this gives a kind of a lexicographic order on
Zfunctions on the same ZSet)
** DONE ZHAs
A Heyting Algebra, as we will see later,
is a structure (a logic!) (Ω,≤,⊤,⊥,∧,∨,→,¬)
in which ≤,⊤,⊥,∧,∨,→,¬ obey the axioms
of /intuitionistic/ propositional calculus.
A ZHA is a ZPoset having:
a bottom point and a top point,
a left wall and a right wall,
all the same-parity points between the two walls,
and no other points.
Some examples of ZHAs:
o o
o o o o o
o o o o o o o o
o o o o o o o o o
o o o o o o o o o o o
o o o o o o o o o
o o o o o o o o
o o o o o o
o o o
(dot) (diamond5) (L) (squiggle) (weird)
** DONE ZHAs (2)
A ZHA is a ZPoset having:
a bottom point and a top point,
a left wall and a right wall,
all the same-parity points between the two walls,
and no other points.
o o
o o o o o
o o o o
o o o o o o
o o o o o o
o o o o o o o
o o o o o o o
o o o o o o
o o o o o o
o o o o o o
o o o
This is This is This is
a ZHA a ZHA NOT a ZHA
** DONE ZHAs (formally)
A ZHA is a ZPoset having:
a bottom point and a top point,
a left wall and a right wall,
all the same-parity points between the two walls,
and no other points.
A ZHA D is generated by:
a height maxy ≥ 0
a bottom point (x_0, 0)
left wall and right wall functions L,R:{0,1,...,maxy}->N
obeying:
L(0)=R(0)=x_0 (bottom point)
L(maxy) = R(maxy) (top point)
0 ≤ L(i) ≤ R(i) (left wall ≤ right wall)
L(y+1) = L(y)±1 (left wall changes in unit steps)
R(y+1) = R(y)±1 (right wall changes in unit steps)
L(y)=0 for some y (to ensure well-positionedness)
then
D ∩ {(x,y)|x ∈ N} is empty when y>maxy,
D ∩ {(x,y)|x ∈ N} = {L(y), L(y)+2, L(y)+4, ..., R(y)}
when y∈{0,1,...,maxy}.
** DONE ZHAs (formally) (2)
A ZHA is a ZPoset having:
a bottom point and a top point,
a left wall and a right wall,
all the same-parity points between the two walls,
and no other points.
o L(9)=1 R(9)=1 maxy=9 L(maxy)=R(maxy)
o o
o
o
o
o o
o o o
o o
o o L(1)=3 R(1)=5
o L(0)=4 R(0)=4 L(0)=R(0)=x_0=4
** DONE ZHAs: the (l,r) coordinates
# (find-dn5 "zha.lua" "ZHA-tests")
We can define the (l,r) coordinates
on a ZHA /informally/ in this way:
the bottom point has (l,r)=(0,0);
when we go one unit northwest,
i.e., from (x,y) to (x-1,y+1),
the l coordinate increases by 1;
when we go one unit northeast,
i.e., from (x,y) to (x+1,y+1),
the r coordinate increases by 1;
We usually write the (l,r) coordinates
of a point as just lr - two digits together,
without the `(', `,', `)'.
Here are two examples:
46
45 36 63
35 26 62 53
34 25 52 43
24 51 42 33
23 50 41 32 23
22 40 31 22
21 30 21 12
20 11 20 11 02
10 01 10 01
00 00
** DONE ZHAs are Heyting Algebras (introduction)
Magic fact / big theorem:
ZHAs are Heyting Algebras.
Version for children: we will learn
1. how to interpret ≤,⊤,⊥,∧,∨,→,¬,↔ in any given ZHA
2. what properties that ≤,⊤,⊥,∧,∨,→,¬,↔ have to obey in a HA
3. that our ZHA operations from (1) obey the properties in (2)
The properties are these:
(id) ∀P.(P≤P)
(comp) ∀P,Q,R.(P≤Q)∧(Q≤R)→(P≤R)
(⊤) ∀P.(P≤⊤)
(⊥) ∀P.(⊥≤P)
(∧) ∀P,Q,R.(P≤Q∧R)↔(P≤Q)∧(P≤R)
(∨) ∀P,Q,R.(P∨Q≤R)↔(P≤R)∧(Q≤R)
(→) ∀P,Q,R.(P≤Q→R)↔(P∧Q≤R)
(¬) ¬P := P→⊥
(↔) P↔Q := (P→Q)∧(Q→P)
** DONE Operations in ZHAs: $≤, ⊤, ⊥, ∧$ and $∨$
In a ZHA H,
⊤ is the top element of H,
⊥ is the bottom element (00), and
P≤Q is true iff P_L≤Q_L and P_R≤Q_R, or, equivalently,
P≤Q is true iff the ZPoset (H,WM(H)^*) has an arrow P->Q.
Also:
(P_L,P_R)&(Q_L,Q_R) := (min(P_L,Q_L),min(P_R,Q_R))
(P_L,P_R)∨(Q_L,Q_R) := (max(P_L,Q_L),max(P_R,Q_R))
Visually, this is:
(diagram)
** DONE Operations in ZHAs: $→$
In a ZHA H,
P≤Q returns 0 or 1, (≤:H×H→{0,1})
P→Q returns an element of H (→:H×H→H).
The definition of →:H×H→H is by cases.
(Note: before I explain this to people I usually
ask them to remember how weird they felt the
definition of →:{0,1}×{0,1}→{0,1} was when
they first saw it...)
Q→R := if Q is below R then ⊤ <-- case 1
elseif Q at left of R then (↗)(Q∧R) <-- case 2
elseif Q at right of R then (↖)(Q∧R) <-- case 3
elseif Q is above R then R <-- case 4
end
Note that the order matters!
If R=22, this is λQ.(which case we use to calculate Q→R):
4
4 4
2 4 3
2 2 3 3
2 2 1 3 3
2 1 1 3
1 1 1
1 1
1
# (find-dn5 "zha.lua" "ZHA-tests-imp")
# (λQ.Q->22) =
# (λR.22->R) =
** DONE Operations in ZHAs: $¬$ and $↔$
The operations ¬ and <-> in a ZHA are
defined in terms of others.
¬P := P->⊥
P<->Q := (P->Q)&(Q->P)
** DONE Some non-tautologies: DeMorgan
# (find-ist "all.lua" "ubs-tests")
In classical logic both DeMorgan laws hold:
¬(P&Q)<->(¬P∨¬Q)
¬(P∨Q)<->(¬P&¬Q)
In intuitionistic logic these three implications are provable,
(¬P∨¬Q)->¬(P&Q)
¬(P∨Q)->(¬P&¬Q) (¬P&¬Q)->¬(P∨Q)
While this one
¬(P&Q)->(¬P∨¬Q)
is false in some ZHAs, for example here:
32
22
21 12
20 11 02
10 01
00
¬(P & Q)->(¬ P ∨ ¬ Q)
-- -- -- --
10 01 10 01
------ ---- ----
00 02 20
--------- ------------
32 22
-----------------------
22
** DONE Some non-tautologies: $¬¬P≤P$
Exercise (homework!):
check that in the obvious ZHA -
the same as in the previous slide -
we have:
00
00
00 00
(λP.¬P) = 02 00 20
02 20
32
32
32
32 32
(λP.¬¬P) = 20 32 02
20 02
00
1
0
(λP.¬¬P=P) = 0 0
(λP.¬¬P≤P) = 1 0 1
0 0
1
** DONE Lindenbaum Algebras
We've been working with algebras of truth values.
What happens when we try to pass to an algebra of propositions?
"Wff" = "well-formed formula".
Let A = Wffs(⊤,⊥,∧,∨,→,¬,↔,P,Q,R) be the set of wffs built from
the constants ⊤,⊥, the operators ∧,∨,→,¬,↔ and the
atomic propositions P,Q,R - plus parentheses.
Let D be the set of triples (P,Q,δ) where
δ is a /intuitionistic/ proof of P⊢Q. <- what is that????
Let D^- be the set of pairs (P,Q) obtained by deleting
the third component of each triple (P,Q,δ)∈D.
Then (A,D^-) is a directed graph.
(A,D^-) is reflexive and transitive - it is a /preorder/ on A.
It induces a quotient ~ on A.
(A/~,D^-/~) is a partial order - the Lindenbaum Algebra
geerated by etc etc etc etc.
** DONE Lindenbaum Algebras (2)
Let A = Wffs(⊤,⊥,&,∨,→,P,Q,R).
Let D be the set of triples (P,Q,δ) where
δ is a intuitionistic proof of P⊢Q (P,Q∈A).
Let D^- be the set of pairs (P,Q) obtained by deleting
the third component of each triple (P,Q,δ)∈D.
Then (A,D^-) is a directed graph,
and the partial order (A/~,D^-/~) is the Lindenbaum Algebra (...)
Lindenbaum Algebras are (free) Heyting Algebras.
We can visualize Lindenbaum Algebras by writing some
wffs in A and
1) treating them as vertices in a directed graph
2) drawing the arrows in D between them
3) making each wff stand for its equivalence class.
** DONE Lindenbaum Algebra for classical logic
Let A = Wffs(⊤,⊥,&,∨,→,¬,↔,P) be the set of wffs...
Let D be the set of triples (P,Q,δ) where
δ is a /classical/ proof of P⊢Q.
Then the Lindenbaum Algebra (A/~,D^-/~) looks like this -
more precisely, it is transitive-reflexive closure of this:
⊤
P ¬P
⊥
This is a Heyting Algebra - but it is not free.
It is a Boolean Algebra - the free one on one generator.
** DONE Lindenbaum Algebras for classical logic (2)
Let A = Wffs(⊤,⊥,&,∨,→,¬,↔,P,Q) be the set of wffs...
Let D be the set of triples (P,Q,δ) where
δ is a /classical/ proof of P⊢Q.
Then the Lindenbaum Algebra (A/~,D^-/~) looks like this -
more precisely, it is the transitive-reflexive closure of
this hypercube:
F
7 E
B 6 D
3 5 A C
2 9 4
1 8
0
This is the free Boolean Algebra on two generators.
(Hint: take P=3 and Q=5)
** DONE Lindenbaum Algebras for IPL are infinite
# https://en.wikipedia.org/wiki/Intuitionistic_logic
# https://en.wikipedia.org/wiki/File:Rieger-Nishimura.svg
Let I_1 = Wffs(⊤,⊥,&,∨,→,¬,↔,A) be the set of wffs...
Let D be the set of triples (P,Q,δ) where
δ is an /intuitionistic/ proof of P⊢Q.
Then the Lindenbaum Algebra (I_1/~,D^-/~) has at least
these distinct points:
43 G G:=F∨F'
42 33 F' F F:=E∨E' F':=F→E
32 23 E E' E:=D∨D' E':=E→D
31 22 D' D D:=C∨C' D':=D→C
21 12 C C' C:=B∨B' C':=C→B
20 11 B' B B:=A∨A' B':=B→A
10 01 A A' A:=10 A':=¬A
00 00
A, A', B, B', ... are all distinct in the ZHA at the left above,
so there cannot be an intuitionistic proof that any two of them -
say, E and C - are equal.
^ This is an argument for adults!!!
We will make it children-friendly soon.
** DONE A computer library
# (find-dn5 "zha.lua" "ZHA")
# (find-dn5 "zha.lua" "ZHA-tests")
The "spec" for a ZHA uses one char per line...
> ZHA.fromspeclr("123LLR432L1"):drawf()
64
63 54
53 44
52 43 34 <- 3
51 42 33 24 <- 4
41 32 23 <- R (means 3 again, but moved right)
40 31 22 <- L (means 3 again, but moved left)
30 21 12 <- L (means 3 again, but moved left)
20 11 02 <- 3
10 01 <- 2
00 <- 1 <- first char of the spec
>
** DONE A computer library (2)
# (find-dn5 "zha.lua" "ZHA")
# (find-dn5 "zha.lua" "ZHA-tests")
We can define functions using a very compact lambda-notation,
and use them to draw the values of Zfunctions.
L0 "P Eq(P, Not(Not(P)))"
--> "function (P) return Eq(P, Not(Not(P))) end"
The ":drawL" method draws Zfunctions.
The global functions Eq, Not, And, Imp, etc
use the global variable "z" - that's why the "z =".
> z = ZHA.fromspeclr("123LLRR21"):drawf()
(...)
> z:drawL "P Not(P) "
(...)
> z:drawL "P Not(Not(P)) "
(...)
> z:drawL "P Eq(P, Not(Not(P)))"
11
00 00
00 00 00
00 00 00
11 00 00
00 00 00
00 00 11
00 00
11
>
** TEXED When in doubt use brute force
# (find-dn5 "zha.lua" "ZHA-tests-bf")
# (find-ist "quotes.tex" "fourman")
\begin{quote}
{\sl When in doubt use brute force.}
Dennis Ritchie
\end{quote}
In the beginning, and for several years, I had very little
intuition about how the $→$ behaved in a Heyting Algebra...
And to make things worse, there are lots of things
that are important in Topos Theory -
namely: the $¬¬$ operator, modalities, sheaves, forcing -
about which I had no intuition whatsoever!
It {\sl had} to be possible to visualize them -
\msk
That was my main motivation for working with ZSets, ZHAs, etc.
\msk
Status of the project:
now I know how to visualise {\sl most} of the operations and theorems
in Fourman/Scott79 -
and {\sl some} things about sheaves and geometric morphisms,
mainly from Peter Johnstone's ``Sketches of an Elephant''
and now I am in a position to get help from adult toposophers! =) =) =)
# (find-xdvipage "~/LATEX/istanbulquotes.dvi" 1 "Fourman")
# (find-xdvipage "~/LATEX/istanbulquotes.dvi" 6 "Elephant")
* ---
* :big: Categories
** DONE Categories
# (find-854 "" "more-on-wd" "is a tuple:")
# (find-854page 25 "is a tuple:")
A category
C = (C_0, Hom_C, id_C, o_C; idL_C, idR_C, assoc_C)
is a directed graph on steroids.
C_0 is the set (<- version for children) of ``objects'' of C.
Hom_C(A,B) returns the set (<- same)
of arrows (``morphisms'', ``maps'') from A to B.
id_C(A) returns and ``identity map'' id_A:A->A.
o_C tells how ``composable'' maps (whose tails and heads meet)
compose; we use ``;'' to write the composition in ``diagrammatic order''.
f g
A ---> B ---> C
---------->
(gof)=(f;g)
idL_C and idR_C tell us that identity maps are cancellable
at the left and at the right: (id_A;f)=f, (f;id_B)=f.
assoc_C tells us that composition is associative: (f;g);h=f;(g;h).
A proto-category is just this:
C^- = (C_0, Hom_C, id_C, o_C)
Note (for adults!!!):
the ``properties'' idL_C, idR_C, assoc_C only make sense
when we know how to compare morphisms for equality.
** DONE Set is a category
This is our archetypal category:
Set = (Set_0, Hom_Set, id_Set, o_Set; idL_Set, idR_Set, assoc_Set)
The objects of Set are sets - so, for example,
{0,1}, {2,3,4,5,6}, {7,8,9}, \empty, \N, \R ∈ Set_0.
The morphisms of Set are the maps between sets - so, for example,
Hom_Set({0,1}, {2,3,4,5,6}) has 2^5 elements (functions!),
Hom_Set({2,3,4,5,6}, {7,8,9}) has 5^3 elements.
Composition in Set is compostion of functions. For example:
2|->7
3|->8
4|->9
0|->4 5|->9
1|->2 6|->9
{0,1} ------> {2,3,4,5,6} -----> {7,8,9}
------------------------->
0|->9
1|->7
And id_{7,8,9} = {7|->7, 8|->8, 9|->9}.
** DONE ZPosets are categories
A ZPoset, like K_↓*
(the "kite" with the (transitive-reflexive closure of) BM(K))
can be seen as a category, in which
Hom (A,B) = / {(A,B)} when there is an arrow from A to B,
K_↓* |
\ empty when there isn't an arrow from A to B.
For example:
((1,3),(0,2)) ((0,2),(1,0))
(1,3) -------------> (0,2) -------------> (1,0)
---------------------------------->
((1,3),(1,0))
Posets can be seen as categories in which
each Hom-set has at most one element.
Warning (for children!):
The ``can be seen'' is important!!!
Many slides ago we saw K_↓* as a pair
made of a ZSet K and subset of K×K...
But K_↓* ``as a category'' is a 7-uple!
Abuse of language!
Also, morphisms here are funny things -
they are not functions, they are /pairs/!
** DONE Categories: associativity
Associativity assures us that
diagrams whose cells commute
commute fully.
Example:
A ---> B ---> C
| | |
v v v
D ---> E ---> F
ab;bc;cf = ab;(bc;cf)
= ab;(be;ef)
= (ab;be);ef
= (ad;de);ef
** DONE Categories: iso(morphisms) and identities
An iso is a map f:A->B
for which there is a f¹:B->A
such that (f;f¹)=id_A and (f¹;f)=id_B.
f
A --> B
\ | \
id_A\ f¹ \id_B
v v v
A --> B
f
Inverses are unique. When we have both
(f;g)=id_A and (g;f)=id_B and
(f;h)=id_A and (h;f)=id_B
then we can prove that g=h:
g,h
B --> A g = g;id_A
\ | \ = g;(f;h)
id_B\ f \id_A = (g;f);h
v v v = id_B;h
B --> A = h
g,h
Note that we used identities (id_C) to define isos
and the properties (idL_C, idR_C)
that say that they identities are neutral elements
to prove that inverses are unique.
** DONE Functors
A functor F: C → D is:
F = (F_0, F_1; respids_F, respcomp_F)
it is made of an _action on objects_, F_0,
that takes objects of C to objects of D,
and an _action of morphisms_, F_1,
that takes morphisms in C to morphisms in D...
and ``properties'' (that appear after the ";"):
respids_F = ∀A∈C_0. id_D(F_0(A)) = F_1(id_C(A))
respcomp_F = ∀A,B,C∈\C_0. ∀f:A->B, g:B->C. F_1(f;g)=F_1(f);F_1(g)
** DONE Functors - on diagrams
A functor F:\C->\D takes
1. composable maps in \C to composable maps in \D
2. diagrams in \C to diagrams in \D
3. commutative diagrams in \C to commutative diagrams in \D
4. isos in \C to isos in \D
Exercise / homework:
show that if the diagram at the left below commutes
then its image by F commutes too, and F_1(f¹)=F_1(f)¹.
Note: it has lots of (common!) shorthands...
You will have to figure them all out.
f f
A --> B FA --> FB
\ | \ \ | \
id\ f¹ \id id\ f¹ \id
v v v F v v v
A --> B |----> FA --> FB
| f | | f |
g| |h g| |h
v v v v
C --> D FC --> FD
k k
** DONE Functors: $(A×)$ and $({0,1}x)$
B |---> FB B |--> F_0(B)
| | | |
f| |-> |Ff f| |-> |F_1(f)
v v v v
C |---> FC C |--> F_0(C)
F F
\C ---> \D \C ---> \D
B |---> (A×)B B |--> (A×)_0(B) B |--> A×B
| | | | | |
f| |-> |(A×)f f| |-> |(A×)_1(f) f| |-> |λp.(πp,f(π'p))
v v v v v v
C |---> (A×)C C |--> (A×)_0(C) C |--> A×C
(A×) (A×) (A×)
\Set ---> \Set \Set ---> \Set \Set ---> \Set
{2,3} |--> {0,1}×{2,3}
| |
2|->4 | |--> | (0,2)|->(0,4), (1,2)|->(1,4),
3|->6 | | (0,3)|->(0,6), (1,3)|->(1,6)
v v
{4,5,6} |--> {0,1}×{4,5,6}
** TEXED Functors: why $(A×)_1(f) = λp.(πp,f(π'p))$ ?
%: p:? p:A{×}B
%: ----- -----
%: p:? π'p:? f:B→C p:A{×}B π'p:B f:B→C
%: ----- -------------- ----- --------------
%: πp:? f(π'p):? πp:A f(π'p):C
%: ---------------- ----------------
%: (πp,f(π'p)):? (πp,f(π'p)):A{×}C
%: ---------------- ----------------
%: λp.(πp,f(π'p)):A{×}B→A{×}C λp.(πp,f(π'p)):A{×}B→A{×}C
%:
%: ^why1 ^why2
\pu
$$\ded{why1} \quad \ded{why2}$$
How would someone {\sl find} the expression $λp.(πp,f(π'p))$?
Idea: let's try to construct a function $?:A×B→A×C$ from $f:B→C$...
%: ?:A{×}B p:A{×}B
%: -----π' -----
%: ?:A{×}B ?:B f:B→C p:A{×}B π'p:B f:B→C
%: -----π -------------app ----- --------------
%: ?:A ?:C πp:A f(π'p):C
%: ----------\ang{,} ----------------
%: ?:A{×}C (πp,f(π'p)):A{×}C
%: -----------λ ----------------
%: ?:A{×}B→A{×}C λp.(πp,f(π'p)):A{×}B→A{×}C
%:
%: ^why3 ^why4
\pu
$$\ded{why3}$$
% $$\ded{why3} \qquad \ded{why4}$$
** DONE Categories with
Almost all the time in Category Theory
we work with categories with extra structure
(and extra properties).
For example, Set, and each ZHA, is
(1) a category with a terminal object
(2) a category with binary products
(3) a category with finite products (= 1+2)
(4) a category with exponentials (needs 2)
(5) a cartesian-closed category (= all the above)
(6) a category with an initial object
(7) a category with binary coproducts (a.k.a. binary sums)
(8) a category with finite coproducts (a.k.a. finite sums; = 6+7)
(9) a cartesian-biclosed category (= all the above)
** DONE BiCCCs
A Cartesian-biclosed category has these operations
(we use some nested uples for clarity):
(C_0, Hom, id, ∘,
(1,!),(×,π,π', <,>),(→,♭,♯),
(0,¡),(+,ι,ι', [,]))
We are omitting the ``properties'' that these operations obey.
Trick: a (bi-)Heyting Algebra has exactly the same structure
as a (bi-)CCC.
A (bi-)Heyting Algebra is a (bi-)CCC in which each Hom-set
has at most one element.
(See the handouts!)
* ---
* :big: Logic on subsets of ZDAGs
** DONE Order topologies
Let (A,R) be a graph.
Example: (A,R) = ({1,2,3}, {(1,3),(2,3)}).
1 2
\ /
v v
3
A _topology_ on a set X is a set of subsets of X (the "open sets").
A graph R ⊆ A×A induces a topology on A.
Here's how:
O(A) = {U⊆A | (1∈U → 3∈U) ∧ (2∈U → 3∈U)}
\---------/ \---------/
condition condition
induced by induced by
1->3 2->3
If we order the open sets by inclusion
we get a partial order, (O(A),⊆).
Let's draw it as a graph.
** DONE Order topologies (2)
{1,2,3} 1 1 ⊤
^ ^ 1 ^ ^
/ \ ^ ^ / \
/ \ / \ / \
1 2 {1,3} {2,3} 1 0 0 1 P Q
\ / ^ ^ 1 1 ^ ^
\ / \ / ^ ^ \ /
v v \ / \ / \ /
3 {3} 0 0 P∧Q
^ 1 ^
| ^ |
| | |
{} 0 0 ⊥
0
(A,R) (O(A),⊆) (O(A),⊆)
** DONE Topologies are Heyting Algebras
Look into almost any CT book
and you find this:
for any topological space (X,O(X))
the poset (O(X),⊆) is a Heyting Algebra.
A HA is a structure (Ω,≤,⊤,⊥,∧,∨,→,¬)
obeying certain properties.
What are Ω,≤,⊤,⊥,∧,∨,→,¬?
Ω := O(X) the open sets are the truth values.
⊤ := X because ⊤ is true everywhere
⊥ := {} because ⊥ is true everywhere
≤ := ⊆
P∧Q := {x∈X | x∈P ∧ x∈Q} P∧Q is true where both P and Q are
P∨Q := {x∈X | x∈P ∨ x∈Q} P∨Q is true where either P or Q are
P→Q := {x∈X | x∈P → x∈Q} P→Q is true where P implies Q <- oops...
Problem: the definition of P→Q does not work always -
it _sometimes_ produces a non-open output even when
both its inputs are open... example:
0 0 1
0 0 -> 1 0 = 1 1
1 1 1 0 1 0
(open) (open) (non-open)
** DONE Order topologies: non-open subsets
A subset B⊆A is non-open when it has a 1 above a 0
with an arrow 1->0 between them... for example,
{2} is not open:
1 2 0 1
\ / \ /
v v v v
3 0
** DONE Order topologies: stable subsets
When I explain these things to children I find it better
to start using the term ``stable subset'' (or stable function)
instead of ``open subset''.
The idea:
`1's are ``things'' (which are heavy),
`0's are ``empty spaces''.
The `1's want to fall down.
For example, 010 is unstable:
0 1 0 0
\ / \ /
v v - - > v v
0 1
Then
P(* *) = {0 0, 0 0, 0 1, 0 1, 1 0, 1 0, 1 1, 1 1}
* 0 1 0 1 0 1 0 1
O(* *) = {0 0, 0 0, 0 1, 1 0, 1 1}
* 0 1 1 1 1
The `P' means ``parts'', but
The `O' means ``open sets'',
for technical reasons that we will understand much later...
(Children don't know topology - I mean, usually)
** DONE Fixing the implication
The fix:
P→Q := {x∈X | x∈P → x∈Q} <-- bad
P→Q := {x∈X | x∈P → x∈Q}° <-- good ("°" means "interior")
** DONE Modal logic for children (...but not now)
We can do MUCH better than just adding an "°".
Let (A,R) be a graph, and (A,O(A)) its order topology.
These are two logics:
I = (Ω , ≤ , ⊤ , ⊥ , ∧ , ∨ , → , ¬ )
I I I I I I I I
M = (Ω , ≤ , ⊤ , ⊥ , ∧ , ∨ , → , ¬ , ⋅ , ⋄ )
M M M M M M M M M M
"I" is the intuitionistic logic we've been working on.
"M" is a modal logic (S4).
Ω_I = O(A)
Ω_M = P(A)
P -> Q := ⋅ (P -> Q)
I M M
This gives us
1) Modal Logic for children
2) Gödels embedding of intuitionistic logic into S4,
for children
But we won't go that way now!!!
** DONE Some order topologies are ZHAs
For example,
1
1 1
1 1
0
1 1
1 1
0 0
1 1 0 0 1
/ \ 1 1 1 1
v v 0 0 0
2 3 ---> 1 0 0 0 0 1
| | 1 0 1 1 0 1
v v 0 0
4 5 0 0 0 0
1 0 0 1
0
0 0
0 0
** DONE The generators of a ZHA
Let (A,BM(A)) be a ZDAG, and
let (H,WM(H)) be a ZHA such that (H,WM(H)^*)≃(O(A),⊆).
Let G=Gen(H) - the ``generators'' of H - be the points of H
with exactly one arrow going into them (in the ZDAG).
Then Gen(H) is /exactly/ the image of $A$ in $H$ by the inclusion '↓'!
Magic! =)
1
1 1
1 1
0
1 1
1 1
0 0
1 1 0 0 1
/ \ 1 1 1 1
v v 0 0 0
2 3 ---> 1 0 0 0 0 1
| | 1 0 1 1 0 1
v v 0 0
4 5 0 0 0 0
1 0 0 1
0
0 0
0 0
Can we recover $(A,BM(A))$ from $G⊆H$?
Well, sort of.
** DONE The generators of a ZHA (2)
Let (A,BM(A)) be a ZDAG, and
let (H,WM(H)) be a ZHA such that (H,WM(H)^*)≃(\Opens(A),⊆).
Let G=Gen(H).
Can we recover $(A,BM(A))$ from $G⊆H$?
Almost - we can make G inherit an order from H...
Important: we need to look at H as a ZPoset, not as a ZDAGs,
and we need to invert the direction of the arrows.
** DONE The generators of a ZHA (3)
# (find-xpdfpage "~/LATEX/2014sfc-slides2.pdf" 12)
Look: (A,BM(A)^*) ≃ (G,R^*).
33 .. 32 13
32 23 32 .. | \ |
32 13 22 13 .. 13 v v v
20 12 21 12 .. 12 20 12
10 01 20 11 20 .. | / |
10 01 10 01 v v v
00 .. 10 01
(A,BM(A)) (H,WM(H)) (G,R)
≃(\Opens(A),⊆)
Now let's divide the generators in G⊆H into two classes
according to the direction of the (only) arrow
that points to them. In the example above we have
Gennw(H)={10,20,32} and Genne(H)={01,12,13}.
The order on G is the columns 32->20->10 and 13->12->01,
plus some intercolumn arrows.
** HALF The generators of a ZHA (4)
What happens when we "omit the other digit",
and write 1_, 2_, 3_... for the left-wall generators
and _1, _2, _3... for the right-wall generators?
33 .. 3_ _3
3_ 23 3_ .. | \ |
3_ _3 22 _3 .. _3 v v v
2_ _2 21 _2 .. _2 2_ _2
1_ _1 2_ 11 2_ .. | / |
1_ _1 1_ _1 v v v
00 .. 1_ _1
(A,BM(A)) (H,WM(H)) (G,R)
≃(\Opens(A),⊆)
It becomes easier to create homework problems!!!
We can specify the two-column graphs as
(height of the left column,
height of the right column,
inter-wall arrows from left to right,
inter-wall arrows from right to right)
The ZHA above is generated by the two-column graph
(3, 3, {3->2}, {2->1}).
** HALF The generators of a ZHA: homework ideas
1) Draw the ZHA correponding to each of the 2-column
graphs specified below:
(3, 4, {}, {})
(3, 4, {}, {_4->_4})
(3, 4, {}, {_4->_3})
(3, 4, {}, {_4->_2})
(3, 4, {}, {_3->_2})
(3, 4, {}, {_4->_3, _3->_2})
(3, 4, {_2,_1}, {})
(3, 4, {_2,_1}, {_4->_3})
(3, 4, {_2,_1}, {_4->_3, _3->_2})
2) Draw the ZHA etc etc for these string specs:
"123RRLL2L321"
(...)
3) Find the 2-column graph and the string spec that
generate each of the ZHAs below:
(...)
4) For each of the ZPosets below draw its topology as a graph.
o o
o o o o o o o o o
o o o o
(They are not going to be ZDAG-ish or ZPoset-ish,
because when we have three independent points the
topology contains a cube)
* ---
* :big: Modalities for children
** DONE The axioms
# (find-books "__cats/__cats.el" "fourman")
A modality on Omega is an operation J: Ω -> Ω obeying these axioms:
M1: P <= J(P)
M2: J(J(P)) <= J(P)
M3: J(P&Q) = J(P)&J(Q)
What do these axioms _mean_ (e.g., geometrically, on ZDAGs)?
* Equivalent elements form diamond-shaped regions
* Stable elements form a sub-ZDAG
To understand and prove this we start with _consequences_ of M1, M2, M3
What familiar operations obey these axioms?
* I(P) := P (the "identity" modality)
* T(P) := ⊤ (the "true" modality)
* O_A(P) := A or P (the "or" modality)
* E_A(P) := A -> P (the "implication" (exponential) modality)
* B_A(P) := (P -> A) -> A ("boolean quotient" - general case)
* B(P) := B_⊥(P) ("boolean quotient" - particular case))
= (P -> ⊥) -> ⊥
= ¬¬P
What other operations obey these axioms?
* Modalities on ZDAGs correspond to dividing by diagonal lines
** TEXED Fourman/Scott1979: ``Sheaves and Logic''
# (find-ist "quotes.tex" "fourman")
This is an excerpt -- pages 329-331 -- from M.P. Fourman and D.S.
Scott's ``Sheaves and Logic'', that was published in SLNM0753
(``Applications of Sheaves: Proceedings of the Research Symposium on
Applications of Sheaf Theory to Logic, Algebra and Analysis - Durham,
july 9-21, 1977'').
\bsk
\BF{2.18. ELEMENTARY J-OPERATORS.} In these examples $Ω$ is a given cHa.
(i) {\sl The closed quotient.} The operator is defined by
%
$$J_a p = a ∨ p.$$
%
This is obviously a J-operator, and the congruence relation is:
%
$$a∨p = a∨q.$$
%
The set of fixed points (quotient lattice) is:
%
$$\setofst{p ∈ Ω}{a≤p}.$$
Classically speaking in the spatial case where $Ω=\Opens(X)$, the
quotient corresponds to the topology on the {\sl closed} subspace
complementary to the open set $a$.
This quotient makes the element $a$ ``false'' and is the least such.
** TEXED Fourman/Scott1979 (2)
(ii) {\sl The open quotient.} The operator is defined by:
%
% (find-slnm0753page (+ 14 330))
%
$$J^a p = a→p.$$
%
The congruence relation is:
%
$$a∧p = a∧q \qquad \text{(equivalently, $a ≤ p↔q$)}.$$
%
The set of fixed points is thus isomorphic to
%
$$Ω_a = \setofst{p∈Ω}{p≤a}.$$
Intuitionistically speaking in the spatial case, this quotient
corresponds to the topology on the open subspace $a$. This quotient
makes $a$ ``true'' and is the leat such.
** TEXED Fourman/Scott1979 (3)
(iii) {\sl The Boolean quotient}. The operator is defined by:
%
$$B_a p = (p→a)→a.$$
%
The congruence relation is:
%
$$p→a = q→ a.$$
%
The set of fixed points is
%
$$\setofst{p∈Ω}{(p→a)→a≤p}.$$
In case $a=⊥$, this is the well-known $¬¬$-quotient giving the
(complete) Boolean algebra of ``stable'' elements. For arbitrary $a$,
we could first form $Ω/J_a$ and follow this by the $¬¬$-quotient to
obtain $Ω/B_a$. (In general, if $J≤K$, then $Ω/K$ is a quotient of
$Ω/J$.)
We remark that in general $Ω/J$ is a cBa iff $J=B_{J_⊥}$. Further, is
$Ω$ is already Boolean, then {\sl every} J-operator on $Ω$ is of the
form $B_a = J_a$.
** TEXED Fourman/Scott1979 (4)
(iv) {\sl The forcing quotient}. The operator is a combination of
previous ones:
%
$$(J_a∧J^b)p = (a∨b)∧(b→p).$$
%
The congruence relation is a conjunction:
%
$$a∨b=a∨q \quad \text{and} \quad b∧p=b∧q.$$
%
The set of fixed points is:
%
$$\setofst{p∈Ω}{b→p≤ a→p}.$$
The point of the quotient is that it provides the {\sl least}
J-operator such that $Ja≤Jb$; that is, we take the least quotient that
``forces'' $a→b$ to be true. If we want to force a sequence of
statements $a_i→b_i$, for $i<n$, the operator needed is $\bigvee_{i<n}
(J_{a_i}∧J{b_i})$. It is important to note that in general sup's of
J-operators cannot be calculated pointwise. We shall see below,
however, that it is possible to find a finite expression for this
particular sup. (We owe this remark to John Cartmell).
** TEXED Fourman/Scott1979 (5)
# (find-slnm0753page (+ 14 331))
(vi) {\sl A mixed quotient.} The interest of this example lies in the fact
that it has a neat finite definition:
%
$$(B_a∧J^a)p = (p→a)→p.$$
%
The congruence relation is:
%
$$(p→a)→p = (q→a)→q,$$
%
which is equivalent to the conjunction:
%
$$a∧p = a∧q \quad\text{and}\quad p→a = q→a.$$
%
The set of fixed points is:
%
$$\setofst{p∈Ω}{(p→a)→p ≤ p}.$$
It is difficult to make this set vivid except to say that it is the
set of elements p satisfying Pierce's law (for a fixed a).
** TEXED Fourman/Scott1979 (6)
If we take a polynomial in $→$, $∧$, $∨$, $⊥$, say $f(p,a,b,\ldots)$,
it is a decidable question whether for all $a$, $b$, $\ldots$ it
defines a J-operator. This does not, however, help us very much in
cataloguing such operators (nor in seeing what good they are!) Some
techniques can be developed from the following formulae, which were
pointed out to us by Cartmell, see also [33] and [47].
\msk
\BF{2.19. PROPOSITION.} In the following, $K$ is an arbitrary
J-operator, $⊤$ is the constant function (the greatest J-operator with
the most trivial quotient), and $⊥$ is the least J-operator (namely,
the identity function on $Ω$):
$$
\def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} (ii) J^a∨J^b = J^{a∧b}
\li (iii) J_a∧J_b = J_{a∧b} (iv) J^a∧J^b = J^{a∨b}
\li (v) J_a∧J_a = ⊥ (vi) J_a∨J^a = ⊤
\li (vii) J_a∨K = K∘J_a (viii) J^a∨K = J^a∘K
\li (ix) J_a∨B_a = B_a (x) J^a∨B_b = B_{a→b}
\end{array}
$$
Proof. Equations (i)-(iv) are easy calculations; while (v) comes down
to showing $p=(a∨p)∧(a→p)$. Formula (vi) is a direct consequence of
(vii) (equally, of (viii)).
** DONE How different modalities interact
(There is an algebra of modalities!)
How does a modality interact with ∧, ∨, →, etc?
What interesting things can we do with modalities?
* Quotients
* Sheafness, sheaves, sheafification (from topos theory)
* Geometric morphisms (from topos theory)
** DONE Diamond-shaped regions
# (find-books "__alg/__alg.el" "gratzer")
A region (i.e., a subset) of a ZDAG is _diamond-shaped_ if it has
* a top element
* a bottom element
* all elements between the top and the bottom, and nothing else
Formally, the _diamond between A and B_ is
Db(A,B) := {P in Omega | A <= P <= B}
Example: in
33 ..
32 23 .. ..
22 13 22 ..
12 03 we have Db(01,22) = 12 ..
11 02 {01,02,11,12,22} = 11 02
10 01 .. 01
00 ..
(Note: the standard terminology is "intervals")
** DONE Stable and equivalent truth-values
Remember: a modality on Ω is an operation J: Ω -> Ω obeying these axioms:
M1: P ≤ J(P)
M2: J(J(P)) ≤ J(P)
M3: J(P∧Q) = J(P)∧J(Q)
M1 means that applying J once moves up,
M2+M1 mean that applying J a second time does not move further up.
(What is M3?)
Let's say that P is _stable_ when P = J(P),
and that P and Q are _equivalent_ when J(P) = J(Q).
Formally:
St(P) := (P = J(P)) (returns true or false)
Sts := {P in Om | St(P) (returns a set)
P==Q := (J(P) = J(Q)) (returns true or false)
E(P) := {Q in Om | P==Q) (returns a set)
Es := {E(P) | P in Om} (returns a partition)
** DONE Stable and equivalent truth-values (2)
# (find-books "__cats/__cats.el" "fourman")
Let's look at an example.
When J(P) := B(P) = not not P, we have
33 33 ..
32 23 33 33 .. ..
22 13 33 33 .. ..
Om == 12 03 (P|->J(P)) == 33 03 Sts == .. 03
11 02 33 03 .. ..
10 01 10 03 10 ..
00 00 10
and the equivalence classes are:
.. .. .. 33
.. .. .. .. .. .. 32 23
.. .. .. .. .. .. 22 13
.. .. .. .. .. 03 12 ..
.. .. .. .. .. 02 11 ..
.. .. 10 .. .. 01 .. ..
00 .. .. ..
i.e., Es = {{00}, {10}, {01,02,03}, {11,12,13,22,23,32,33}}
** DONE What is axiom M3? Introduction
Remember: a modality on Ω is an operation J: Ω -> Ω obeying these axioms:
M1: P ≤ J(P)
M2: J(J(P)) ≤ J(P)
M3: J(P∧Q) = J(P)∧J(Q)
M3 implies _monotonicity_, which is:
Mo: P ≤ Q implies J(P) ≤ J(Q)
but this is not obvious. Let's prove that in several steps.
..
.. ..
.. .. ..
.. .. .. ..
.. 64 .. 46 .. J(P) J(Q)
.. .. .. .. .. .. ^ ^
.. .. .. 44 .. .. .. \ /
.. .. .. .. .. .. .. .. J(P)&J(Q)
.. .. .. .. .. .. ..
.. .. .. .. .. ..
.. 31 .. 13 .. P Q
.. .. .. .. ^ ^
.. 11 .. \ /
.. .. P&Q
..
Let P=31, Q=13, J(P)=64, J(Q)=46.
Then P∧Q=11 and J(P)∧J(Q)=44, but without M3 we wouldn't know
where is J(P∧Q)=J(11)... it could be anything above 11.
M3 tells us that J(11)=J(P∧Q)=J(P)∧J(Q)=64∧46=44,
which is below J(P)=64 and J(Q)=46...
(Actually J(11) is the topmost value below J(P) and J(Q).)
** DONE What is axiom M3? Monotonicity for products
M3 implies that J(P&Q)=J(P)&J(Q),
so let's rewrite the "J(P)&J(Q)" as "J(P&Q)" in our diagram.
M3 implies that when we apply J to all elements of a
product diagram P <- P&Q -> Q, we do have arrows
in its image J(P) <- J(P&Q) -> J(Q).
Formally, this is
Mp: J(P&Q) <= J(P), and J(P&Q) <= J(Q)
("monotonicy for products")
..
.. ..
.. .. ..
.. .. .. ..
.. 64 .. 46 .. J(P) J(Q)
.. .. .. .. .. .. ^ ^
.. .. .. 44 .. .. .. \ /
.. .. .. .. .. .. .. .. J(P&Q)
.. .. .. .. .. .. ..
.. .. .. .. .. ..
.. 31 .. 13 .. P Q
.. .. .. .. ^ ^
.. 11 .. \ /
.. .. P&Q
..
** DONE What is axiom M3? Monotonicity
When P <= Q we have P = P&Q,
and a part of the previous diagram collapses..
If P=P&Q=11, Q=13, J(P)=J(P&Q)=44, J(Q)=46,
and we have:
..
.. ..
.. .. ..
.. .. .. ..
.. .. .. 46 .. J(Q)
.. .. .. .. .. .. ^
.. .. .. 44 .. .. .. /
.. .. .. .. .. .. .. .. J(P) = J(P&Q)
.. .. .. .. .. .. ..
.. .. .. .. .. ..
.. .. .. 13 .. Q
.. .. .. .. ^
.. 11 .. /
.. .. P = P&Q
..
** DONE What is axiom M3? Monotonicity (2)
Formally:
----------------M3 ---------------
J(P&Q)=J(P)&J(Q) J(P)&P(Q)<=J(Q)
------------Mp := -----------------------------------
J(P&Q)<=J(Q) J(P&Q)<=J(Q)
P<=Q
=====
P=P&Q
----------- ------------Mp
P<=Q J(P)=J(P&Q) J(P&Q)<=J(Q)
----------Mo := -------------------------
J(P)<=J(Q) J(P)<=J(Q)
** DONE The sandwich lemma
From
M1: P <= J(P)
M2: J(J(P)) <= J(P)
M3: J(P&Q) = J(P)&J(Q)
We can prove that if P <= Q <= J(P) then P and Q (and J(P)) are equivalent.
More formally ("sandwich lemma"):
SL: If P <= Q <= J(P) then P==Q.
Proof:
Q<=J(P)
-------------Mo -------------M2
P<=Q J(Q)<=J(J(P)) J(J(P))<=J(P)
----------Mo -------------------------------
P<=Q Q<=J(P) J(P)<=J(Q) J(Q)<=J(P)
-------------SL := --------------------------------
J(P)=J(Q) J(P)=J(Q)
** DONE The sandwich lemma: equivalence classes don't have holes
Sandwich lemma:
SL: If P<=Q<=J(P) then P==Q.
What does that mean? Let's look again at our example.
This was an equivalence class,
33
32 23
22 13
12 ..
11 ..
.. ..
..
and J(12) = 33.
Making P=12 and Q=22 in the sandwich lemma,
we have P <= Q <= J(P), i.e., 12 <= 22 <= 33,
and, by C1, P==Q, i.e., 12==22, i.e., J(12)=J(22)=33.
The sandwich lemma is very powerful.
If we know that J(11)=33, then,
using it for all elements between 11 and 33,
we get that J(12)=J(13)=J(22)=J(23)=J(32)=33.
The sandwich lemma says that equivalence classes do not have "holes".
** DONE Equivalence classes: the bottom element lemma
The axiom
M3: J(P&Q) = J(P)&J(Q)
can be extended to P&Q&R, P&Q&R&S, etc. Look:
J(P&Q&R) = J(P&(Q&R))
= J(P)&J(Q&R)
= J(P)&J(Q)&J(R)
What happens when we take the "&" of all the truth-values in an
equivalence class, and then we apply J to it?
Let's look at an example.
Let E := {11,12,13,22,23,32,33}
and &E := 11&12&13&22&23&32&33 (= 11).
33
32 23
22 13
12 ..
11 ..
.. ..
..
J(&E) = J(11 & 12 & 13 & 22 & 23 & 32 & 33)
= J(11) & J(12) & J(13) & J(22) & J(23) & J(32) & J(33)
= 33 & 33 & 33 & 33 & 33 & 33 & 33
= 33
** DONE Equivalence classes: the bottom element lemma (2)
Let E := {11,12,13,22,23,32,33}
and &E := 11&12&13&22&23&32&33 (= 11).
33
32 23
22 13
12 ..
11 ..
.. ..
..
J(&E) = J(11 & 12 & 13 & 22 & 23 & 32 & 33)
= J(11) & J(12) & J(13) & J(22) & J(23) & J(32) & J(33)
= 33 & 33 & 33 & 33 & 33 & 33 & 33
= 33
So, &E is ==-equivalent to all other elements of E,
and &E is below all other elements of E...
That means that &E is the bottom element of that equivalence class,
and, by the sandwich lemma, the equivalence class is made of
all elements between &E and J(&E).
TYPESET THIS IN RED:
(That only works for _finite_ conjunctions, but we are working only
with finite cases...)
** DONE Equivalence classes: the bottom element lemma (3)
A small modification of that previous argument leads to this:
let E be any non-empty set of equivalent elements of Om.
Then the diamond-shaped region
E' := D(&E,J(&E))
having &E as its bottom element and J(&E) as its top element
contains E, and all elements in E' are equivalent.
For example, in
33
32 23
22 13
12 ..
11 ..
.. ..
..
let E := {13, 22}; note that J(13)=J(22)=33, and that &E = 13&22 = 12.
Then
J(&E) = J(13 & 22)
= J(13) & J(22)
= 33 & 33
= 33...
** DONE Equivalence classes: the bottom element lemma (4)
let E := {13, 22}; note that J(13)=J(22)=33, and that &E = 13&22 = 12.
Then
J(&E) = J(13 & 22)
= J(13) & J(22)
= 33 & 33
= 33,
and all elements in the diamond-shaped region
E' := D(&E,J(&E)) = D(12,33) = {12,13,22,23,32,33}
are equivalent; this new lemma takes any arbitrary non-empty set of
equivalent elements, and extends it to a diamond-shaped set of
equivalent elements. In our example it extends E={13,22} to
E={12,13,22,23,32,33}, ie.,
.. 33
.. .. 32 23
22 13 22 13
.. .. to: 12 ..
.. .. .. ..
.. .. .. ..
.. ..
** DONE An operation dual to J
Let Eq(P) be the equivalence class of P.
Formally,
Eq(P) := {Q | J(P)=J(Q)}.
We know that J(P) returns the top element of Eq(P).
We saw, by the bottom element lemma, that each Eq(P) has a bottom element.
Let's denote that bottom element by B(P).
Formally, B(P) is the "&" of all elements of Eq(P).
(A finite conjunction because we are in the finite case!)
We have that Eq(P) is made of all elements between B(P) and J(P),
and nothing else...
We will return to this later.
** DONE How J interacts with $∧$
We know (proofs later!) that "&" is monotonous on both its inputs,
and that P<=J(P) and that J is monotonous, i.e.,
P<=P' Q<=Q' P<=Q
--------- --------- ------- ----------
P&Q<=P'&Q P&Q<=P&Q' P<=J(P) J(P)<=J(Q)
These things mean that for any truth-values P and Q we know some
relations between P&Q, J(P)&Q, ..., J(J(P)&J(Q)):
J(J(P)&J(Q))
^ ^ ^
/ | \
/ | \
J(J(P)&Q) J(P)&J(Q) J(P&J(Q))
^ ^ ^ ^ ^ ^
| \/ \/ |
| /\ /\ |
J(P)&Q J(P&Q) P&J(Q)
^ ^ ^
\ | /
\ | /
P&Q
But M3 tells us that J(P&Q)=J(P)&J(Q), so at least the two middle
vertices in the cube-shaped diagram above yield the same result...
Actually we can prove more: J(P&Q) is equal to all the four upper
truth-values in the diagram above. Proofs:
J(J(P)&Q) = J(J(P))&J(Q) = J(P)&J(Q)
J(P&J(Q)) = J(P)&J(J(Q)) = J(P)&J(Q)
J(J(P)&J(Q)) = J(J(P))&J(J(Q)) = J(P)&J(Q)
** DONE How J interacts with $∨$
We know (proofs later!) that "∨" is monotonous on both its inputs,
and (again!) that P<=J(P) and that J is monotonous, i.e.,
P<=P' Q<=Q' P<=Q
--------- --------- ------- ----------
PvQ<=P'vQ PvQ<=PvQ' P<=J(P) J(P)<=J(Q)
These things mean that for any truth-values P and Q we know these
relations between PvQ, J(P)vQ, ..., J(J(P)&J(Q)):
J(J(P)∨J(Q))
^ ^ ^
/ | \
/ | \
J(J(P)∨Q) J(P)∨J(Q) J(P∨J(Q))
^ ^ ^ ^ ^ ^
| \/ \/ |
| /\ /\ |
J(P)∨Q J(P∨Q) P∨J(Q)
^ ^ ^
\ | /
\ | /
P∨Q
But we know more. We can prove that we have J(J(P)∨J(Q))<=J(P∨Q),
** DONE How J interacts with $∨$ (2)
But we know more. We can prove that we have J(J(P)∨J(Q))<=J(P∨Q),
------ ------
P<=P∨Q Q<=P∨Q
------------Mo ------------Mo
J(P)<=J(P∨Q) J(Q)<=J(P∨Q)
---------------------------
J(P)∨J(Q)<=J(P∨Q)
-----------------------Mo ----------------M2
J(J(P)∨J(Q))<=J(J(P∨Q)) J(J(P∨Q))=J(P∨Q)
--------------------------------------------
J(J(P)∨J(Q))<=J(P∨Q)
and this implies that all the 4 truth-values in the upper lozenge are
equal...
** DONE How ZHAs are cut into equivalence classes
We saw that the equivalence classes of J are diamond-shaped regions,
but we don't know yet how which ways of splitting a ZHA into
diamond-shaped regions correspond to "J"s that obey M1, M2 and M3...
For example, does this correspond a valid J?
/\
55 / \
55 55 / /\
55 55 35 / / \
55 55 35 35 /\ /\ \
51 55 33 35 35 /\ \/ \ \ (*)
50 51 33 33 35 35 \ \ \ /\ /
50 51 33 13 35 \ \/\/ \/
50 21 13 13 \/ / /
21 13 13 \/ /
13 13 \ /
13 \/
It turns out that no.
Look at the frontiers between equivalence classes.
We will see two separate arguments.
** DONE How ZHAs are cut into equivalence classes (2)
The first, based on the fact that J(Q)=J(R) implies J(P&Q)=J(P&R),
shows that borders that make lambda and mirrored lambdas are not
possible,
/\ /\ /\ /\
/\ \ / /\ /\/\ /\/\
\/\/ \/\/ \/ / \ \/
\/ \/ \/ \/
(lambda) (mirrored lambda) (y) (mirrored y)
and a second one, based on the fact that St(P) and St(Q) implies
St(P&Q), that shows that borders that make "y"s and mirrored "y"s are
not possible.
** DONE Borders like lambdas are not possible
Lemma: if Q==R then P&Q==P&R ("`&' preserves equivalence").
Proof:
J(Q)=J(R)
-------------------
J(Q)=J(R) J(P)&J(Q)=J(P)&J(R)
-------------&pe := ===================
J(P&Q)=J(P&R) J(P&Q)=J(P&R)
Diagrammatically, we can use "P&" to "move southwest", as here:
P Q 52 34
\ / \ \ / \
P&Q R 32 14
\ / \ /
Q&R 12
In the diagram (*) we have J(34)=J(14)=35, but J(32)=33 and J(12)=13;
if we take P=52, Q=34, R=14, the lemma &pe would imply that J(32)=J(12),
which does not hold. Diagrammatically, the lemma "&pe" implies that
the lines marking the frontiers between different equivalence classes
cannot make either a "lambda" or its mirror image...
/\ /\
/\ \ / /\
\/\/ \/\/
\/ \/
(lambda) (mirrored lambda)
** DONE Borders like "y"s are not possible
# (find-equailfile "sgml-input.el" ";; LEFT SEMIDIRECT PRODUCT")
# (find-equailfile "sgml-input.el" ";; RIGHT SEMIDIRECT PRODUCT")
Lemma: St(P) and St(Q) implies St(P&Q) ("& preserves stability")
Proof:
P=J(P) Q=J(Q)
============== ----------------M3
P=J(P) Q=J(Q) P&Q=J(P)&J(Q) J(P)&J(Q)=J(P&Q)
--------------&ps := ---------------------------------
P&Q=J(P&Q) P&Q=J(P&Q)
We start with the case in which our ZHA is a lozenge.
We know that equivalence classes are diamond-shaped regions.
When the ZHA is a lozenge, the equivalence classes are lozenges too.
Let's look at this example. Here are a ZHA H and a function J: H -> H
on it; J obeys M1 and M2 - remember the geometrical meaning of M1 and
M2! - and we want to show that that J cannot obey M3 too.
33 33 /\
32 23 33 33 / \
31 22 13 31 33 13 /\ /\
30 21 12 03 31 31 13 13 / \/ \
20 11 02 31 13 13 \ / /
10 01 13 13 \/ /
00 13 \ /
\/
** DONE Borders like "y"s are not possible (2)
Let's look at this example. Here are a ZHA H and a function J: H -> H
on it; J obeys M1 and M2 - remember the geometrical meaning of M1 and
M2! - and we want to show that that J cannot obey M3 too.
33 33 /\
32 23 33 33 / \
31 22 13 31 33 13 /\ /\
30 21 12 03 31 31 13 13 / \/ \
20 11 02 31 13 13 \ / /
10 01 13 13 \/ /
00 13 \ /
\/
Let P' be the truth-value at the left of the vertex of the "y",
and Q' be the truth-value at the right of the vertex of the "y".
In this example, P'=12 and Q'=21.
Let P be J(P'),
and Q be J(Q').
The line from P' to P points exactly northwest, and
the line from Q' to Q points exactly northeast;
because of this, P'&Q' is equal to P&Q, and P'&Q' is the truth-value
just below the vertex of the "y".
Let R be P&Q = P'&Q'.
P and Q are stable, and so, by "&ps", R=P&Q=P'&Q' must be stable too.
But, by hypothesis, the top element of the equivalence class of R is Q,
so R is not stable, and thus the J in our example cannot obey M3.
** COMMENT Borders like "y"s are not possible (3)
When our ZHA is not a lozenge, it is not trivial to show that the path
from P' to P is exactly northwest, and that the path from Q' to Q is
exactly northeast.
An example:
(...)
[I don't know how to complete the details]
** HALF Stable elements and diamond-shaped regions
Two slogans:
Equivalent elements form diamond-shaped regions
Stable elements form a sub-ZHA
Definitions:
P==Q := P* <-> Q* (P==Q is true or false)
St(P) := P == P* (St(P) is true or false)
Sts := {P in Omega | P == P*} (Sts is a set)
Di(P) := {Q in Omega | P == Q} (Di(P) is a set)
Dis := {Di(P) | P in Omega} (Dis is a partition of Omega)
33 33 33
32 23 33 33 33 33
22 13 33 13 33 33
12 03 13 13 33 03
11 02 11 13 33 03
10 01 11 11 10 03
00 11 00
Pid PJ Pnotnot
** TODO Modalities induce Z-quotients
** TODO Z-quotients are modalities
** TODO Modalities correspond to morphisms of HAs
* ---
* :big: Sheaves
# (find-djvupage "$S/http/angg.twu.net/MINICATS/sheaves_for_children__1_to_7.djvu")
# (find-books "__cats/__cats.el" "moerdijk")
** DONE Restriction, compatibility, glueing
2|->20 3|->300
3|->300 4|->4000
{2,3,4} {3,4,5} 4|->4000 5|->50
^ ^ - -
\ / \ /
\ / v v
{3,4} 3|->300
4|->4000
The domain of 20,300,4000 is {2,3,4}.
The domain of 300,4000,50 is {3,4,5}.
The common domain of 20,300,4000 and 300,4000,50
is {2,3,4}∩{3,4,5} = {3,4}.
The restriction of 20,300,4000 to {3,4} is 300,4000.
The restriction of 300,4000,50 to {3,4} is 300,4000. ← same!
20,300,4000 and 300,4000,50 are compatible.
We are moving down, toward smaller sets, using intersections.
Is there a way to move up - to unions?
Yes, by glueing.
But we have to see some other things first.
** DONE Compatible families
Let's write the domain of a function in its subscript.
Suppose that f_A compat g_B compat h_C compat k_D,
and that E⊆A∩B∩C∩D.
Then the restrictions of f_A, g_B, h_C, k_D to E all coincide!!!
The diagram below should make
A B C D f_A g_B h_C k_D
A∩B B∩C C∩D ?_A∩B ?_B∩C ?_C∩D
^ ^ ^ \ | /
\ | / \ | /
\ | / \ | /
\ | / v v v
E ?_E
?_A∩B = f_A|A∩B = g_B|A∩B f_A|E = f_A|A∩B|E = g_B|A∩B|E = g_B|E
?_B∩C = g_B|B∩C = h_C|B∩C g_B|E = g_B|B∩C|E = h_C|B∩C|E = h_C|E
?_C∩D = h_C|C∩D = k_D|C∩D h_C|E = h_C|C∩D|E = k_D|C∩D|E = k_D|E
We say that the family {f_A, g_B, h_C, k_D} is
/pairwise-compatible/ when any two elements in it
are compatible - f_A compat g_B compat h_C compat k_D
plus f_A compat h_C, g_B compat k_D, f_A compat k_D.
** DONE Compatible families: naming
A notation trick...
Compare:
f_A g_B h_C k_D f_A f_B f_C f_D
?_A∩B ?_B∩C ?_C∩D f_A∩B f_B∩C f_C∩D
\ | / \ | /
\ | / \ | /
\ | / \ | /
v v v v v v
?_E ?_E
?_A∩B := f_A|A∩B = g_B|A∩B f_A∩B := f_A|A∩B = f_B|A∩B
?_B∩C := g_B|B∩C = h_C|B∩C f_B∩C := f_B|B∩C = f_C|B∩C
?_C∩D := h_C|C∩D = k_D|C∩D f_C∩D := f_C|C∩D = f_D|C∩D
?_E := f_A|E = g_B|E = h_C|E = k_D|E f_E := f_A|E = f_B|E = f_C|E = f_D|E
A compatible family {f_A,f_B,f_C,f_D}
induces a bigger family having one f_U
for each empty set U that is smaller
than _some_ of the sets A, B, C, D...
And these `f_U's are well-defined,
all ways of defining them from the
original {f_A,f_B,f_C,f_D} by restriction
yield the same result.
** DONE Saturating downwards
Remember that we had and operation `↓' on DAGs
that regarded each `1' as black paint that was too liquid
and that would flow down, painting the `0's below it
in black...
0 0
0 0 0 0
0 0 0 0 0 0
↓ 0 0 1 0 = 0 0 1 0
1 0 0 1 1 1
0 0 1 1
0 1
Let's use the same symbol, ↓, for an operation that
starts with a compatible family, say {f_A,f_B,f_C,f_D},
and produces a (possible much bigger!) family made of
all the restrictions of f_A, f_B, f_C, f_D.
Also:
dom f_A = A
dom {f_A, f_B, f_C, f_D} = {A, B, C, D}
** DONE An operation for all kinds of restrictions
This operation simplifies things magically.
(I learned it from Simmons's paper on Omega Sets).
U · V = U∧V
U · g_V = (error)
f_U · V = f_U|U∧V
f_U · g_V = f_U|U∧V
So: U · V = V · U is true always
f_U · g_V = g_V · f_U is true iff f_U and g_V
are compatible
Now: U · {V, W} = {U·V, U·W} = {U∩V, U∩W}
U · O(X) = all (open) subsets of U = ↓{U}
f_U · O(X) = all restrictions of f_U
{f_U,g_V,h_W}·O(X) = all restrictions of f_U, g_V, h_W,
which yields somthing nice when
f_U, g_V, h_W are compatible,
and something messy when they are not.
We can define ↓A := A·O(X), and this works for all interesting cases!
** DONE Sheaves of functions
For each open set U⊆R,
C∞(U,R) is the set of smooth functions from U to R.
Warning: here (a,b) sometimes mean an open interval, not a pair!
(4,6) |--> C∞((4,6),R) f_{(4,6)}:(4,6)->R
^ | -
incl| |restr |restr
| v v
(5,6) |--> C∞((5,6),R) f_{(4,5)}:(4,5)->R
O(R) - - - - -> Set
We can regard C∞(-,R) as a (contravariant) functor.
Hey:
C∞(-,R): O(R)^op -> Set
is a sheaf because compatible families can be glued
in a unique way!
** DONE Limited functions are not sheaves
Let L(-,R): O(R)^op -> Set
be the contravariant functor that returns
the _limited_ functions on open sets.
Certain families of limited functions
are compatible, but their glueing is not limited,
so it "does not exist".
L(-,R) violates one of the conditions for being a sheaf:
that glueings must exist.
The other condition is that glueings must be unique.
To violate that we need to go away from the realm of
the presheaves of functions, and use arbitrary functors.
** DONE The evil presheaf
E_1 {0,1}
/ \ / \ 0|->3
/ \ / \ 1|->4
v v v v
E = E_2 E_3 = {2} {3,4}
\ / \ /
\ / \ /
v v v v
E_4 {5}
| |
| | 5|->6
v v
E_5 {6,7}
The compatible family {2,3} has two different glueings: 0 and 1.
The compatible family {2,4} can't be glued.
The compatible family {} has two different glueings: 6 and 7.
** DONE Sheaves in $Set^{K^\op}$
...with the "obvious" notion of sheafness, are the ones that obey:
A_1 = A_2 ×_A_4 A_3
/ \
/ \
v v
A = A_2 A_3
\ /
\ /
v v
A_4
|
|
v
A_5 = 1
So: A_1 and A_5 carry only redundant information,
and sheaves on Set^K^op are equivalent to objects
of Set^V !!!
* ---
* :big: Toposes
** TODO A formal definition for children
A _pullback_ for the diagram A->C<-B is an object D,
together with morphisms A<-D->B, that behaves like this:
{(a,b)∈A×B | f(a)=g(b)} ----> B
| |
| | g
v f v
A --------------> C
A _subobject_ of A is a diagram A' -> A
that behaves like an inclusion.
Notation: A' >-> A means that the arrow is a monic.
A _subobject classifier_ is an object Ω
that behaves like {0,1},
plus an arrow 1 >-> Ω (called "true")
that makes the curved arrow at the left have an inverse.
{a∈A | P(a)} ------> 1 A' ---------> 1
v v v v
| <--\ | | --\ |
| | | i| | |
v | P v v v v
A -----------> Ω A ----------> Ω
λa.a∈i(A)
A _topos_ is a CCC that has pullbacks and a subobject classifier
(-> extra structure and extra properties).
** DONE The main theorems
1) CCCs are exactly the categories in which we can interpret
(the system λ1 os simply-typed) λ-calculus
2) HAs are exactly the categories in which we can interpret
(intuitionistic) propositional logic
3) Every HA is a CCC
4) Set is a CCC
5) Every ZHA is a HA
6) Every (O(X),⊆) is a HA
7) Every ZTopos is a CCC <-- ZToposes are in the next slide
8) Every ZTopos is a topos
9) Topos are exactly the categories in which we can interpret
(the system IST of intuitionistic, typed) set theory
There are many other ways of constructing toposes,
but I believe that ZToposes are the perfect tool for
doing Topos Theory for Children -
** HALF ZToposes
When we did logic on subsets of a ZHA - K, say -
each truth-value P was in fact a K-shaped diagram, e.g.,
0 P_1
P = 1 0 = P_2 P_3
1 P_4
1 P_5
We are going to do the same with sets.
An object A of Set^(K^op) is a K-shaped diagram of sets
and maps.
A_1
/ \
v v
A = A_2 A_3
\ /
v v
A_4
|
v
A_5
A _notion of sheafness_ on Set^K^op is something that tells us
which objects of Set^K^op "are" sheaves.
The "sheaves" of Set^K^op form a subcategory of Set^K^op
which is also a topos. <- Magic!!!
In the case of ZToposes these subcategories of sheaves are
not something weird and new - we have this:
for any ZDAG D,
for notion of sheafness on Set^D^op,
there is a ZDAG D'
such that Sh(Set^D^op)≅Set^D'^op.
** TODO Quotes from the Elephant
** COMMENT Pullbacks
** COMMENT Subobjects
** COMMENT Classifier
** COMMENT λ-calculus in a topos
** COMMENT Logic in a topos
** COMMENT Sequents
** COMMENT Quantifiers
** COMMENT Mixed sequents
** COMMENT Geometrical morphisms
** COMMENT Maps between ZDAGs induce geometrical morphisms
** COMMENT Sheaves: saturated covers
** COMMENT Sheaves: glueing a cover
** COMMENT Sheaves in general
* ---
* ---
* ---
* ---
* Partitions into contiguous classes
A partition of {0,...,n} into contiguous classes (a "picc") is one in
which this holds: if a,b,c∈{0,...,n}, a<b<c and a~c, then a~b~c. So,
for example, {{0,1},{2},{3,4,5}} are partitions into contiguous
classes, and {{0,2},{1}} is not.
A partition of {0,...,n} into contiguous classes induces an
equivalence relation ·~_P·, a function [·]_P that returns the
equivalence class of an element, a function
·^P:{0,...,n}->{0,...,n}
a|->max [a]_P
that takes each element to the top element in its class, a set St_P :=
{a∈{0,...,n} | a^P=a} of the "stable" elements of {0,...,n}, and a
graphical representation with a bar between a and a+1 when they are in
different classes:
01|2|345 == {{0,1},{2},{3,4,5}},
which will be our favourite notation for partitions into contiguous
classes from now on.
* The algebra of piccs
When P and P' are two piccs on {0,...,n} we say that P≤P' when
∀a∈{0,...,n}.a^P≤a^P'. The intuition is that P≤P' means that the graph
of the function ·^P is under the graph of ·^P':
a^P a^P a^P a^P
^ ^ ^ ^
5 | * 5 | * * 5 | * * * * 5 * * * * * *
4 | * 4 | 4 | 4 |
3 | * <= 3 | * * <= 3 | <= 3 |
2 | * 2 | 2 | 2 |
1 | * 1 * * 1 * * 1 |
0 *----------> a 0 +----------> a 0 +----------> a 0 +----------> a
0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5
0|1|2|3|4|5 <= 01|23|45 <= 01|2345 012345
This yields a partial order on piccs, whose bottom element is the
identity function 0|1|...|n, and the top element is 01...n, that takes
all elements to n.
It turns out that the piccs form a (Heyting!) algebra, in which we can
define ⊤, ⊥, ∧, ∨, and even →.
01234 ⊤
^ ^
| |
01|234 P∨Q
^ ^ ^ ^
/ \ / \
0|1|234 01|2|34 P Q
^ ^ ^ ^
\ / \ /
0|1|2|34 P∧Q
^ ^
| |
0|1|2|3|4 ⊥
The operations ∧ and ∨ are easy to understand in terms of cuts (the
"|"s):
Cuts(P∨Q) = Cuts(P)∩Cuts(Q)
Cuts(P∧Q) = Cuts(P)∪Cuts(Q)
The stable elements of a picc on {0,...,n} are the ones at the left of
a cut plus the n, so we have:
St(P∨Q) = St(P)∩St(Q)
St(P∧Q) = St(P)∪St(Q)
Here is a case that shows how ·^(P∨Q) can be problematic. The result
of a^(P∨Q) must be stable by both P and Q. Let:
E := 01|2|34|56|789
O := 01|23|45|6|789
E∨O = 01|23456|789
E∧O = 01|2|3|4|5|6|789
We can define a^(P∧Q) := a^P∧a^Q, and this always works. But
a^(P∨Q) := a^P∨a^Q does not, we may have to do something like
iterating the two functions many times:
O∨E = 0123456
2^(O∨E)=6
a^(O∨E)=(((a^O)^E)^O)^E
O=01|23|45|6 E=0!12|34|56
O∧E=0|1|2|3|4|5|6
2^(O∧E)=2^O∧2^E=3∧2=2
a^(O∧E)=a^O∧a^E
The "→" in the algebra of piccs will not be relevant to us, so we will
not discuss it.
* ZQuotients
A _ZQuotient_ for a ZHA with top element 46 is a partition of
{0,...,4} into contiguous classes (a "partition of the left wall"),
plus a partition of {0,...,6} into contiguous classes (a "partition of
the right wall"). Our favourite short notation for ZQuotients is with
"/"s and "\"s, like this, "4321/0 0123\45\6", because we regard the
cuts in a ZQuotient as diagonal cuts on the ZHA. The graphical
notation is this:
/ \
46
/ \ \
45 36
\ \ \
35 26
/ \ /
34 25
\ /
24
/ \ \
23 14
/ \ / \
22 13 04
\ / \ /
12 03
/ / /
11 02
\ / /
01
/ /
00
\ /
4321/0 0123\45\6
which makes clear how we can adapt the definitions of ·~_P·, [·]_P,
·^P, St_P, which were on (one-dimensional!) PICCs in section ..., to
their two-dimensional counterparts on ZQuotients. If P is the
ZQuotient of the figure above, then
34 ~_P 25 is true
23 ~_P 24 is false
[12]_P = {11, 12, 13, 22, 23}
22^P = 23
St_P = {03, 04, 23, 45, 46}
* The algebra os ZQuotients
The ideas of the last section apply to ZQuotients, with a few
adjustments. The
St(P∧Q) = St(P)∪St(Q)
would mean, for P = 54/32/10 and Q = 01/23/45, that
St(P_cuts) = St(
* 2-column graphs
A 2-column graph is a graph like the one in the picture below,
composed of a _left column_ 4_->3_->2->1_->0_, a _right column_
6_->5_->4_->3_->2->1_->0_, and some intercolumn arrows: _, _ and _
going from the left column to the right column, _ and _ going from the
right column to the left column.
(example)
A compact way to specify a 2-column graph is this: (left height, right
height, left-to-wall arrows, right-to-left arrows). In the graph of
the example this is (5, 7, {...}, {...}).
We need to attribute a precise meaning for 0_,...,_4 and _0,...,_6.
For the moment let's use this one:
vdots vdots
(0,3) = 3_ _4 = (2,4)
(0,2) = 2_ _2 = (2,2)
(0,1) = 1_ _1 = (2,1)
(0,0) = 0_ _0 = (2,0)
Later we will see a different way of identifying the points of the
columns with points of R^2, that is more complex but quite convenient.
Let's write (5, 7, {...}, {...})^* for the transitive-reflexive
closure of of the graph, and O(5, 7, {...}, {...}) for its order
topology. O(5, 7, {}, {}) is a rectangle,
Every open set of a 2-column graph is made of a pile of $a$ elements
at the bottom of the left column, and a pile of $b$ elements at the
bottom of the right column. If we write these piles as $ab$ then the
connection with ZHAs becomes clear:
Every open set of a 2-column graph is made of a pile of $a$ elements
at the bottom of the left column and a pile of $b$ elements at the
bottom of the right column. If we write these ''2-piles'' as $ab$ then
the connection with ZHAs becomes clear:
0
0
0
0 1 = 23
1 1
1 1
48
47 38
46 37 28
45 36 27 18
44 35 26 17 08
43 34 25 16 07
42 33 24 15 06
41 32 23 14 05
O(5, 7, {}, {}) = 40 31 22 13 04
30 21 12 03
20 11 02
10 01
00
What happens when we add intercolumn arrows? Let A := O(5, 7, {}, {}).
If we add 2_->_1, we get A' := O(5, 7, {2_->_1}, {}) where 31 ==
(diagram) and all 2-piles of the form (diagram), which were open in A,
become non-open in A', and we get this: a dent in the left wall.
48
47 38
46 37 28
45 36 27 18
44 35 26 17 08
43 34 25 16 07
33 24 15 06
23 14 05
O(5, 7, {2_->_1}, {}) = 22 13 04
21 12 03
20 11 02
10 01
00
If we add _3->_1, which is in the transitive closure of (5, 7,
{2_-L1), {}), nothing changes: A'' := O() is equal to A'.
If we add _____, we get another dent in the left wall; if we add ____,
we get a dent in the right wall. We got this:
48
47 38
46 37
36
35 26
34 25 16
33 24 15 06
23 14 05
O(5, 7, {2_->_1}, {}) = 22 13 04
21 12 03
20 11 02
10 01
00
Up to this point all of the A, A', ..., A''' were ZHAs. Let's now add
the arrow .... . It creates a cycle in the 2-column graph, which was
previously acyclic; the new dent in the right wall touches a previous
dent in the left wall, making A'''' = O(5, 7, {2_->_1}, {})
disconnected.
* Proper 2-column graphs
Let's call a 2-column graph _proper_ if it has no redundant arrows,
like the ... that we added between ... and ..., and no cycles, like
the one that was created by adding ... after ... . It turns out that a
2-column graph has no redundant arrows iff its arrows from the left
wall can be put in a list (l1_->_r1, l2_->_r2, ln_->_rn) in which
l1<l2<...<ln and r1<r2<...<rn, and the same thing for arrows from the
right, but with (_r1'->l1'_, ..., _rm'->lm'_) and r1'<...<rm',
l1'<...<lm'; as for having no cycles, the condition is that shouldn't
be an arrow l_->_r and an arrow _r'->l'_ which form a cycle, i.e.,
with r>=r' and l'>=l.
It should now be clear how to convert between proper 2-column graphs
and ZHAs, and that they are in bijection. The following figure may
help.
/-----> _6 /-----> 16
5_ -/ _5 56 -/ 15
4_ /------ _4 43 /------ 14
3_ | /-> _3 33 | /-> 03
2_ --+--/ _2 23 --+--/ 02
1_ <-/ _1 10 <-/ 01
56 56
46 ..
45 36 .. ..
44 35 26 .. .. ..
43 34 25 16 43 .. .. 16
33 24 15 33 .. 15
23 14 23 14
13 ..
12 03 .. 03
11 02 .. 02
10 01 10 01
00 ..
* Wiggly 2-column graphs
Let A be a proper 2-column graph. It is better to work on an example,
so let A be (5, 6, {2_->_3, 5_->_6}, {1_<-_4}), which is:
/-----> _6
5_ -/ _5
4_ /------ _4
3_ | /-> _3
2_ --+--/ _2
1_ <-/ _1
For each point in its two columns, we can put a 0 in its "_", regard
that as a 2-pile, find the smallest open set containing it, and
represent that using the 2-digit notation. For example, if we start
with 4_, we get:
/-----> _6
5_ -/ _5
4_ /------ _4
40 == 3_ | /-> _3
2_ --+--/ _2
1_ <-/ _1
/-----> 0 /-----> 0
0 -/ 0 0 -/ 0
1 /------ 0 1 /------ 0
dn 40 == dn 1 | /-> 0 = 1 | /-> 1 = 43
1 --+--/ 0 1 --+--/ 1
1 <-/ 0 1 <-/ 1
Earlier we said that we were going to interpret a_ as (0,a) and _b as
(2,b) at that moment, but that that was just one way. What happens
when we interpret a_ as dn a_ and _b as dn _b? _Lots_ of good things!
See:
(...)
We gen an embedding of A into O(A), in a way that takes each a_ to the
a-th generator (in the sense of sec ___) of the left wall, and each _b
to the b-th generator of the right wall; also, all the inter-column
arrows become either straight southeast or straight southwest, and
when we abbreviate the a_->_b and a_<-_b as ab, as this,
(5, 6, {2_->_3, 5_->_6}, {1_<-_4}) = (5, 6, {23, 56}, {14})
we see that 23 and 16 are exactly the generators of the left wall that
come immediately above a dent, or, equivalently, the first ones in
which the value of their r-coordinate
(56) 56
46 ..
45 36 .. ..
44 35 26 .. .. ..
(43) 34 25 (16) 43 .. .. 16
(33) 24 (15) 33 .. 15
(23)(14) 23 14
13 ..
12 (03) .. 03
11 (02) .. 02
(10)(01) 10 01
00 ..
(with arrows)
* ---
* ---
* ---
* COMMENT :big: Intuitionistic (propositional) logic
** COMMENT Gödel's translation
# http://plato.stanford.edu/entries/goedel/
# http://plato.stanford.edu/entries/goedel/#GodWorIntLogAri
# http://plato.stanford.edu/entries/goedel/#IntProLogIntS4 ***
# http://plato.stanford.edu/entries/goedel/#PriSou [1933f]
# http://plato.stanford.edu/entries/logic-modal-origins/#KriPosWorSem
# http://plato.stanford.edu/entries/logic-intuitionistic/
# (find-books "__modal/__modal.el")
** COMMENT How I arrived at ZHAs?
** COMMENT Where in the literature is this?
# (find-books "__alg/__alg.el" "gratzer")
# (find-gratzerpage (+ 31 35) "3.5 Intervals")
"ZHAs are distributive lattices": Gratzer (sort of)
"ZHAs are Heyting Algebras": Gratzer (sort of)
"All planar HAs are isomorphic to ZHAs", or, better,
"If a ZPoset is a HA then it is isomorphic to a ZHA":
maybe I can claim authorship on that =) (?!?!)
(I'll sketch proofs of the missing parts soon)
(L,r) coordinates, bullet notation, Zfunction notation:
maybe I can claim authorship on that too =)
But what is really interesting to explain
is _how I arrived_ at ZHAs!
** COMMENT ZHAs are topologies
Let H ("house") be this ZSet:
*
* *
* *
Here is the graph obtained from H by using black moves
and the reading order:
1
/ \
v v
2 3
| |
v v
4 5
BM(H) induces a topology on H.
A _topology_ on H is a set of subsets of H (the "open sets").
Notation:
O(H) ⊆ P(H)
(opens) (parts)
We will work on {1,2,3,4,5} for convenience
instead of on H = {(1,2), (0,1),(2,1), (0,0),(2,0)}.
** COMMENT Topologies are Heyting Algebras
This is very well-known:
For any topological space (X,\Opens(X)),
the poset (\Opens(X), ⊆) is a Heyting Algebra.
We take ⊤:=X, ⊥:=\empty, and if P,Q,R∈\Opens(X), then
P&Q := {x∈X|(x∈P)&(x∈Q)}
= P∩Q
P∨Q := {x∈X|(x∈P)∨(x∈Q)}
= P∪Q
Q→R := {x∈X|(x∈Q)→(x∈R)}^\int
= {x∈X|¬(x∈Q)∨(x∈R)}^\int
= ((X\bsl Q)∪R)^\int
= \bigcup {P∈\Opens(X) | P&Q⊆R}
If we define Ω:=\Opens(X) and ⊤,⊥,&,∨,→ as above
then (Ω,⊤,⊥,&,∨,→) is a HA.
** COMMENT Finite topologies
As I wanted to visualize how &,∨,→ functioned,
I started to work with the set of open sets ``generated by''
a few open sets - typically just U and V, or, U, V and W,
maybe with some extra equations...
The ``top'' ⊤ would be on top,
the ``bottom'' ⊥ would be at the bottom.
X=U∪V ⊤=P∨Q
^ ^ ^ ^
/ \ / \
U V P Q
^ ^ ^ ^
\ / \ /
U∩V P&Q
^ ^
| |
\empty ⊥
** COMMENT Order topologies and their posets of open sets
Let's write ``↓B'' for ``the smallest open set cointaing B''.
Then ↓{1}={1,3}, ↓{2}={2,3}, ↓{3}={3}, or, better:
↓{1}=↓100=101, ↓{2}=↓010=011, ↓{3}=↓001=001.
`↓{-}' takes each point of the DAG (A,R)
to a /different/ open set in (A,\Opens(A)),
in a way that inverts the arrows!
111
^ ^
/ \
1 2 101 011
\ / ^ ^
v v \ /
3 001
^
|
000
** COMMENT When is $(\Opens(A),⊆)$ a ZPoset?
# (find-LATEXgrep "grep -niH -e guill *.tex")
# (find-LATEX "2014sfc-slides2.tex" "unpriming")
# (find-xpdfpage "~/LATEX/2014sfc-slides2.pdf" 12)
The diagram below blew my mind, and motivated everything.
Every time that I started with a ZDAG that was
small enough to handle, then (\Opens(A),⊆)
would be a ZPoset. But why? And what exactly was ``small enough''?
(diagrams)
** COMMENT All intuitionistic theorems are tautologies in a ZHA
** COMMENT Intuitionistic theorems
** COMMENT Intuitionistic derivations
** COMMENT Intuitionistic theorems are true in Heyting Algebras
** COMMENT Intuitionistic derivations are constructions in HAs
** COMMENT Natural Deduction
* COMMENT :big: Heyting Algebras by diagrams
** TODO A translation diagram for Heyting Algebras
# (find-854 "" "CCCs")
** TODO A translation diagram for BiCCCs
# (find-854 "" "CCCs")
** HALF Do our operations $∧,∨,→$ on ZHAs really deserve their names?
Many slides ago we talked about Alice's logic and Bob's logic...
Alice's logic was this,
(copy)
and we were sort of leaving implicit that any other similar tuple, like
(random logic)
would be ``a logic'' in Alice's book-world...
But things are not like that!!!
I just explained a version for children first!!!!!!!!
What's missing:
structure properties (new!)
/-----------\ /--------\
a logic = (Om,and,or,...;eq_T,eq...)
where eq_T, ... are the properties (equations) that T,...
have to obey to ``deserver their names'', to ``behave as expected''.
They are:
(...)
** HALF The properties of $⊥,⊤,∧,∨,→$: a diagram
[diagrammatic mnemonic]
[deduction rules (sequents with le)]
[forall-ish formulation]
We will return to this diagram /many/ times...
** COMMENT ZPosets, ZToposes
** COMMENT Elephant
(All from section A4, in vol.1)
# (find-books "__cats/__cats.el" "johnstone-elephant")
** Definition 4.1.1
# (find-elephantpage (+ 17 161) "A4 Geometric Morphisms - Basic Theory")
# (find-elephantpage (+ 17 161) "Definition 4.1.1")
# (find-elephantpage (+ 17 163) "Example 4.1.4")
# (find-elephantpage (+ 17 164) "Lemma 4.1.5")
# (find-elephantpage (+ 17 165) "Example 4.1.8")
# (find-elephantpage (+ 17 165) "Example 4.1.10")
# (find-elephantpage (+ 17 180) "Example 4.2.6 (ii) and (iii)")
# (find-elephantpage (+ 17 181) "Example 4.2.7")
# (find-elephantpage (+ 17 182) "inclusion")
# (find-elephantpage (+ 17 182) "Lemma 4.2.9")
# (find-elephantpage (+ 17 183) "Theorem 4.2.10")
# (find-elephantpage (+ 17 184) "Examples 4.2.12 (b) and (c)")
# (find-elephantpage (+ 17 189) "Grothendieck coverages")
# (find-elephantpage (+ 17 190) "(b) (i) and (ii)")
# (find-elephantpage (+ 17 192) "Theorem 4.3.9")
# (find-elephantpage (+ 17 205) "Example 4.5.2")
# (find-elephantpage (+ 17 209) "Proposition 4.5.8 (i)")
# (find-elephantpage (+ 17 211) "Example 4.5.9")
# (find-elephantpage (+ 17 211) "We write Lop(E)")
# (find-elephantpage (+ 17 211) "Lemma 4.5.10")
# (find-elephantpage (+ 17 215) "(e)")
# (find-elephantpage (+ 17 219) "Corollary 4.5.20")
# (find-elephantpage (+ 17 219) "the local operator ¬¬ of 4.5.9 is dense")
# (find-elephantpage (+ 17 224) "Examples 4.6.2 (a), (c), (f)")
# (find-elephantpage (+ 17 226) "Theorem 4.6.5")
# (find-elephantpage (+ 17 226) "Proposition 4.6.6 (i) and (iv)")
# (find-elephantpage (+ 17 231) "Proposition 4.6.10 (i) and (iii)")
Definition 4.1.1 (a) Let \scrE and \scrF be toposes. A /geometric
morphism/ f:\scrF -> \scrE consists of a pair of functors f_*:\scrF->\scrE
* ---
* COMMENT eev-composes-utf8
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-eev "eev-compose.el")
# (find-evardescr 'eev-composes-all)
recode l1..u8 < ~/eev-current/eev-compose.el | awk '91<NR && NR<116' | tee /tmp/o
# (find-fline "/tmp/o")
# (find-efunction 'ee-wrap-anchor0)
* COMMENT transfer: edrx.tgz
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
mkdir /tmp/pen/
sudo mount -o uid=$UID /dev/sdb1 /tmp/pen/
makeL
makeLedrxtgz
laf ~/TH/L/edrx.tgz ~/edrx.tgz /tmp/pen/edrx.tgz
cp -v ~/TH/L/edrx.tgz /tmp/pen/
# (find-fline "/tmp/pen/")
sudo umount /tmp/pen
sync
* COMMENT transfer: istanbul1.org between computers
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
mkdir /tmp/pen/
sudo mount -o uid=$UID /dev/sdb1 /tmp/pen/
# (find-fline "~/LATEX/istanbul1.org")
cp -v ~/LATEX/istanbul1.org /tmp/pen/
tkdiff /tmp/pen/istanbul1.org ~/LATEX/istanbul1.org
sudo umount /tmp/pen
sync
* -
%L print(); print(table.concat(sectionnames, "\n"))
\pu
* COMMENT Local variables
# coding: raw-text-unix
# (find-es "org" "TODO-and-DONE")
#+TODO: TODO | DONE | HALF | TEXED
# Local Variables:
# coding: utf-8-unix
# modes: (org-mode emacs-lisp-mode fundamental-mode)
# End: