|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2014istanbul-a.tex")
% (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
% (defun o () (interactive) (find-angg "ORG/istanbul.org"))
% (defun e () (interactive) (find-LATEX "2015logicandcats.tex"))
% (defun l () (interactive) (find-LATEX "2015logicandcats.lua"))
Logic in O(LL)
Logic in G
* --- 0. Introduction: a view from the top
** What do we mean by ``children''?
** The girl from Ipanema
# (find-LATEX "2014sfc-slides.tex")
# (find-xpdfpage "~/LATEX/2014sfc-slides.pdf" 4)
# (find-xpdfpage "~/LATEX/2014sfc-slides.pdf" 5)
# (find-LATEX "2014sfc-slides.tex" "CT-why-now")
** Generalization / specialization / the right example
** Generalization as lifting
** Reading CT books
** Never underestimate the power of the Sierpinski topos
** Warning for mathematicians
Warning for mathematicians:
We will see particular cases first,
and the general definitions later.
If you are wondering what is definition
for something mentioned in slide n,
it will usually appear at slide n+1.
Sometimes we will explain things using very explicit examples.
Some people (mathematicians!) may find our examples too explicit, and
kindergarden-ish... if you get bored, try to guess what is going on at
the meta-level! One of the themes of this tutorial is a technique for
doing general cases in parallel with "archetypal" particular cases,
and doing parts of proofs in the one side (general or particular) and
parts in the other...
** Alice's Logic and Bob's Logic
** Structure, properties, layers, type theory
** Layers in logic(s): structure vs properties
** HALF Layers in CT
The base layer is constructions and diagrams.
The second layer is properties, equations, proving equalities and commutativites.
Working on the base layer is fun, and feels like play.
Working on the second layer is boring, and feels like heavy, grudging work.
One meaning for ``Categories for children'' is that
we will do the ``play'' part,
and leave the ``work'' part for (much) later.
* ---
* --- 1. Classical logic for children
** DONE Evaluation, and evaluation sequences
# (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''.
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 etc
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/ -
We need to learn how to use commutativies, which let us see
that -ab+ba = -ab+ab = 0... and, of course, we need 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.
** Evaluating expressions with and, or, imp, not
** Tautologies: some and/or/imp/not expressions are always true
** A glimpse of a logic in which P<->¬¬P is not a tautology
** What is ``a'' logic? (First attempt)
** What is ``a'' logic? Names versus values
** Alice's logic vs Bob's logic, and how names help
** What properties do we expect from and/or/imp/not?
Structure
Properties
"To deserve a name"
* ---
* --- 2. Lambda-calculus
** DONE Introduction
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 |-> 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) ---> sqrt(4+5)
: :
: :
v v
f(9) ---> sqrt(9) ---> 3
f(4+5) ---> 2+sqrt(4+5)
: :
: :
v v
f(9) ---> 2+sqrt(9) ---> 2+3 ---> 5
** DONE 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 Sets versus types: `->'
When we say
g: N -> R
a |-> a*a+4
we mean that g in R^N, where R^N is the set of all functions from N to
R... if we define that
A -> B := B^A
then
N -> R := R^N
and
g: N -> R
means that:
g in N -> R
Let's define a precise meaning for `:' now.
We will have to do that in several steps.
In the beginning `:' will be the same as `in',
then we will list which are the few allowed uses for `:',
and only at the end we will have a formal meaning for `:',
where usually `:' is weaker than `in', but that allows
type-inference.
** DONE Set versus types: pairs and application
Suppose that A={1,2}, B={3,4}, C={5,6,7}
(to make things very concrete!)
and that:
a:A
b:B
f:B->C
p:AxB
Now - i.e., below the four `:'-expressions above - we are in a context
where:
a is a variable "ranging over A", i.e., either a=1 ou b=2,
b is a variable ranging over B, i.e., either b=3 ou b=4,
f is a function from B to C, and, as a function can be represented by
its input-output pairs, then f is either
{(3,5),(4,5)}, or
{(3,5),(4,6)}, or
{(3,5),(4,7)}, or
{(3,6),(4,5)}, or ..., or {(3,7),(4,7)},
p is pair made of an a and b (in that order!), so p is either
(1,3) or (1,4) or (2,3) or (2,4).
In this context,
f(b):C (function application)
pi p:A (first projection)
pi'p:B (second projection)
(a,b):AxB (the operation (_,_) forms pairs)
** DONE Set versus types: pairs and application 2
Suppose that A={1,2}, B={3,4}, C={5,6,7} as before, and:
a:A a = 2
b:B b = 3
f:B->C f = {(3,6),(4,7)
p:AxB p = (1,4)
Then (a,f(pi'p)):AxC - which means:
* we know the value of the expression (a,f(pi'p))
* its result if of type AxC, i.e., belongs to AxB
"We know the value of (a,f(pi'p))" means:
we know how to calculate it without syntax errors, type errors, or
stumbling into undefined variables.
we can "prove" that (a,f(pi'p)):AxC using the derivation below:
p:AxB (1,4)
------pi' -----pi'
pi'p:B f:B->C 4 {(3,6),(4,7)}
-----------------app ----------------------app
a:A f(pi'p)):C 2 7
--------------------(,) ------------------(,)
(a,f(pi'p)):AxC (2,7)
** DONE Judgments
If A, B, C are types
and we know the values of
the variables a, b, f, p,
with these types,
a:A
b:B
f:B->C
p:AxB
then we know
(a,f(pi'p)):AxC
i.e., we know the value of a,f(pi'p)
and and we know its type - AxC.
We can write this more compactly.
This is a _judgment_:
a:A, b:B, f:B->C, p:AxB |- (a,f(pi'p)):AxC
But what is a judgment, precisely?
** DONE What is a judgment, precisely?
This is a (valid!) judgment
a:A, b:B, f:B->C, p:AxB |- (a,f(pi'p)):AxC
in an (external) context that is just this: "A, B, and C are types".
From "A, B, and C are types" this we can form many other types - for
example AxB, Bx((AxA)xA), B->C, (A->B)->(B->A),
(AxC)->(B->((CxA)x(A->B))), and so on.
The part
a:A, b:B, f:B->C, p:AxB
is the _context_ (of the judgment).
It is a list of _typings_ (of variables).
The context "declares" variables and their types.
On the right of the `|-' in the context we have
(a,f(pi'p)):AxC
This is the _conclusion_ (of the judgment).
It is a typing, but now of an expression (a "term")
that doesn't need to be just a variable.
The expression (a,f(pi'p)) was formed from a,b,f,p
using pairing, projections and function application,
just like we formed (AxC)->(B->((CxA)x(A->B)))
from A, B, C and x and ->.
** DONE Invalid judgments
This is an invalid judgment:
a:B, a:BxC, c:(A->B)xC |- (a,f(pi f)):C
It is syntactically right, but semantically wrong.
The variable a is defined twice (with different types!),
the variable f is not defined,
(a,f(pi f)) can't have the type C, etc...
However,
BxC and (A->B)xC are generated from A, B, C using x and ->,
and (a,f(pi f)) is generated from a and f using pairing,
the projection operations pi and pi', and function application.
** DONE Pre-judgments
This is a pre-judgment:
a:B, a:BxC, c:(A->B)xC |- (a,f(pi f)):C
Grammar for pre-judgments:
* lowercase letters are variables
* uppercase letters are types
* new types can be formed with x and ->
* variables are terms
* new terms can be formed with (,), pi, pi', and function application
* a _context_ is var:type, ..., var:type (0 or more typings)
* a _pre-judgment_ is context |- term:type
** DONE Pre-judgments and judgments (via derivation trees)
We just saw a grammar that generates all _pre-judgments_.
Some pre-judgments are "semantically right", and are _judgments_.
Some pre-judgments are "semantically wrong", and not judgments.
(An "invalid judgment" is a pre-judgment that is not a judgment).
The _judgments_ are the pre-judgments that can appear in derivation
trees like the one below at the right; note that the tree at the right
is essentially the one at the left - that we have seen before - with
contexts added, and with rules that construct more complex types from
more basic types and rules that create variables of given types; in
the tree at the right the only hypotheses are that A, B and C are
types.
A type B type
---------------x
AxB type B type C type
------------var --------------\to
p:AxB p:AxB|-p:AxB B->C type
------pi' ------------pi' --------------var
pi'p:B f:B->C A type p:AxB|-pi'p:B f:B->C|-f:B->C
-----------------app --------var -------------------------------app
a:A f(pi'p)):C a:A|-a:A p:AxB,f:B->C|-f(pi'p)):C
--------------------(,) -------------------------------------(,)
(a,f(pi'p)):AxC a:A,p:AxB,f:B->C|-(a,f(pi'p)):AxC
The tree at the right is a _derivation_ in system Lambda1.
Only pre-judgments that are judgments are derivable.
** TODO Union of contexts
** TODO Type inference
** TODO Adding Lambda
* ---
* --- 3. Intuitionistic logics for children
** DONE Positional notation
Let Lambda be {(1,1), (0,0), (2,0)} subset N^2, i.e., these points:
(1,1)
(0,0) (2,0)
We can represent a function having Lambda as its domain
using a positional notation - for example, this one,
f: Lambda -> N
(x,y) |-> { 3 if (x,y)=(1,1)
{ 4 if (x,y)=(0,0)
{ 5 if (x,y)=(2,0)
ca be represented "positionally" as:
3
4 5
Note that we have 8 functions from Lambda to {0,1},
namely:
000, 001, ..., 111
These things are going to be the truth-values in a certain logic.
In ``standard logic'' the set of truth-values is {0,1}.
In ``Lambda-modal logic'' the set of truth values is
{000, 001, ..., 111}.
** DONE Logic on {0,1}
Let's call our set of truth-values Om.
In the usual logic Om = {0,1}, and
the operations and, or, not, imp, bij, T, false
are defined as functions:
and: Om x Om -> Om
or: Om x Om -> Om
imp: Om x Om -> Om
bij: Om x Om -> Om
not: Om -> Om
T in Om (T: Om^0 -> Om)
false in Om (false: Om^0 -> Om)
That we usually explain to children using tables:
P Q P&Q PvQ P->Q P<->Q P !P
--------------------------- -----
0 0 0 0 1 1 0 1
0 1 0 1 1 0 1 0
1 0 0 1 0 0
1 1 1 1 1 1
This is a ``well-formed formula'' (wff)
on and, or, not, imp, bij, P, Q:
!(PvQ) -> (!P)&(!Q)
If P is 0 and Q is 1, we can calculate the value of the wff above
doing this:
not (P or Q) -> (not P) and (not Q)
0 1 0 1
------ ----- -----
1 1 0
------------ -----------------
0 0
----------------------------------
1
** DONE wffs as machines
We can also consider
not (P or Q) -> (not P) and (not Q)
as a machine that receives the values of P and Q,
and returns the value of not (P or Q) -> (not P) and (not Q).
We can represent its behavior in a table:
P Q not (P or Q) -> (not P) and (not Q)
-----------------------------------------
0 0 1
0 1 1
1 0 1
1 1 1
Note that it always returns 1 (true), for any inputs.
Expressions that always return true are called _tautologies_.
** DONE Logic for children
When we explain this to children they learn
how to calculate the values of &v-><->TF-expressions
for given values of P and Q, and after that they learn
how to calculate the values of &v-><->TF-expressions
for _all_ values of P and Q...
With that they know that some expressions, like
(!!P) <-> P
are tautologies, and other ones, like PvQ->P&Q, are not.
Logic for them (them=children), at this point, is what they use
to calculate the truth-values of &v-><->TF-expressions,
just like they use arithmetic to calculate the results of things like:
(2*3)+(4*5)
--- ---
6 20
--------
26
** DONE Logic, Arithmetic, tables
A tautology like (!!P)<->P is a &v-><->TF-expression that always
yields the same value - true - and we can test quickly
whether a &v-><->TF-expression is a tautology or not, as the
tables are not _too_ big.
An arithmetic expression like
((a+b)*(a-b))-((a*a)-(b*b))
always yields the same value - zero -, but to verify that
we would have to make an infinite number of tests, i.e.,
fill up all the positions in an infinite table.
Logic is more manageable than arithmetic
(because the tables are smaller)!
To prove that
((a+b)*(a-b))-((a*a)-(b*b))
is always zero we need _algebra_.
There is something similar to algebra for logic,
but we are postponing it - we want to start with just
the idea of filling up tables, and checking tautology-ness.
** DONE Modal logic on Lambda and on House: truth-values
We saw how to do logic when our truth-values are 0 and 1...
Let's now define four other logics:
LL-modal logic LL-intuitionistic logic
HH-modal logic HH-intuitionistic logic
We will see the modal ones first.
To make things pronounceable, LL is "lambda" and HH is "house".
Using letters, L = LL, LL-modal logic is L-modal logic, and so on.
In LL-modal logic our truth values are ways of
substituting 0s and 1s for the *s in LL...
In LL-modal logic the truth values are these:
(8 truth values)
In HH-modal logic, our truth values are ways of
substituting 0s and 1s for the *s in HH...
In H-modal logic the truth values are these (there are 32 of them):
(32 truth values, with "...")
Each "*" in LL or HH is called a "world".
If we number the worlds like this,
1 1
2 3 2 3
4 5
then 00101 is a HH-modal truth-value that is false (0)
in the worlds 1, 2 and 4, and true (1) in the worlds 3 and 5.
If P=00101, then
P_1=0
P_2=0 P_3=1
P_4=0 P_5=1
** DONE Modal Logic on Lambda and on House: &,v,->,<->
In HH-modal logic we have:
Om_HM={0000,00001,...,11111} |Om_HM|=32
We have to define the functions
&_HM: Om_HM x Om_HM -> Om_HM
v_HM: Om_HM x Om_HM -> Om_HM
->_HM: Om_HM x Om_HM -> Om_HM
<->_HM: Om_HM x Om_HM -> Om_HM
A table showing how to calculate &_HM would have 32x32=1024 lines,
so tables are not practical here... We will define &_HM, v_HM, ->_HM,
by an algorithm. The idea is to ___calculate the result in each world
separately___; for example:
0 0 1
0 0 ->_HM 0 1 = 1 1
1 1 0 1 0 1
because
P_1 Q_1 P_1->Q_1 (P->_HMQ)_1
P_2 P_3 ->_HM Q_2 Q_3 = P_2->Q_2 P_3->Q_3 = (P->_HMQ)_2 (P->_HMQ)_3
P_4 P_5 Q_4 Q_5 P_4->Q_4 P_5->Q_5 (P->_HMQ)_4 (P->_HMQ)_5
0 0 0->0 1
0 0 ->_HM 0 1 = 0->0 0->1 = 1 1
1 1 0 1 1->0 1->1 0 1
and the same thing for &, v, <->.
So, for example,
0 0 0
0 0 &_HM 0 1 = 0 0
1 1 0 1 0 1
0 0 0
0 0 v_HM 0 1 = 0 1
1 1 0 1 1 1
0 0 1
0 0 <->_HM 0 1 = 1 0
1 1 0 1 0 1
** DONE Intuitionistic Logic on Lambda and on House: truth-values
Now think that
"1" means "there's a something here" and
"0" means "there's nothing here"
and that things in LL and HH can fall through
these arrows:
* *
/ \ / \
v v v v
* * * *
| |
v v
* *
Then 11010 is unstable, because the top 1 wants to fall - 11011 wants
to become ..., ... wants to become either ... or ..., and so on.
In LL-_intuitionistic_ logic, the truth-values
are the ones from LL-modal logic that are stable. So,
Om_LM = {8 truth values}
Om_LI = {5 truth values}
and the same thing for H-intuitionistic logic. Om_HM has 32 truth values,
but Om_HI has just 10:
Om_HI = {10 truth values}
** DONE Intuitionistic Logic on Lambda and on House: nec
The most naive way to try to define &_HI, v_HI, ->_HI, <->_HI fails...
If we just apply the idea of "calculate the result in each world separately",
sometimes "good" inputs (stable truth values) will produce "bad" outputs
(unstable truth-values)! Remember that we saw that:
0 0 0->0 1
0 0 ->_HM 0 1 = 0->0 0->1 = 1 1
1 1 0 1 1->0 1->1 0 1
Let's define an operation that keeps stable truth-values unchanged,
but converts unstable truth-vales to stabe truth-values.
Remember the idea that when we have a "1" above a "0"
the "1" wants to fall to the position of the "0" just below it
through one of the arrows...
* *
/ \ / \
v v v v
* * * *
| |
v v
* *
We will modify that idea. To calculate nec P (pron: "necessary P")
everything "1" that could fall into a "0" just disappears - instead
of the "1" and the "0" changing places, the "1" becomes a "0" - and
we repeat that idea as many times as needed until we get something
stable. For example,
1 1 0
1 1 --> 0 1 --> 0 1
0 1 0 1 0 1
and 00101 is stable; so nec 11101 = 00101.
We define:
P &_HI Q = nec (P &_HM Q)
P v_HI Q = nec (P v_HM Q)
P ->_HI Q = nec (P ->_HM Q)
Actually &_HM and v_HM always produce "good" (stable) outputs
when they receive "good" (stable) inputs, so we can simplify that to:
P &_HI Q = P &_HM Q
P v_HI Q = P v_HM Q
P ->_HI Q = nec (P ->_HM Q)
** DONE Intuitionistic Logic on Lambda and on House: ! and <->
Usually in intuitionistic logic ! and <-> are not primitive operators,
they are defined from ->, &, bot like this:
!P := P->bot
P<->Q := (P->Q)&(Q->P)
so we would have
P &_HI Q := P &_HM Q
P v_HI Q := P v_HM Q
P ->_HI Q := nec (P ->_HM Q)
!_HI P := P ->_HI bot
= nec (P ->_HM bot)
= nec (P ->_HM 00000)
P <->_HI Q := (P ->_HI Q) &_HI (Q ->_HI P)
= nec (P ->_HM Q) &_HM nec (Q ->_HI P)
but it turns out the formulas for ! and <-> yield the same results
that these ones,
!_HI P := nec (!_HM P)
P <->_HI Q := nec (P <->_HM Q)
which are slightly quicker to calculate.
** DONE !!P->P is not always a tautology
In H-intuitionistic logic, if P=00001, then
!!P->P
means
!_HI !_HI 00001 ->_HI 00001,
and
!_HI 00001 = nec (!_HM 00001) = nec 11110 = 01010
!_HI !_HI 00001 = !_HI 01010 = nec (!_HM 01010) = nec 10101 = 00101
!_HI !_HI 00001 ->_HI 00001 = 00101 ->_HI 00001 = nec (00101 ->_HM 00001) = nec 11011 = 01011
With a bit of practice we can calculate that like this:
! ! 00001 -> 00001
-------
01010
---------
00101
------------------
01011
So in H-intuitionistic logic, when P=00001, then
!!P->P = 01011
which is true is some worlds, but not all;
in this case !!P->P is not equal to T_HI = 11111.
Here are the tables with the values of !!P->P for all values of P,
in H-intuitionistic logic and in classical logic:
P !!P->P ...
---------
...
So H-intuitionistic logic "!!P->P" is not a tautology, while in
classical logic it is.
What does that mean?
In H-intuitionistic logic "!!P<->P" is not a tautology.
In H-intuitionistic logic !!P can be different from P.
In L-intuitionistic logic this - "!!P can be different from P" - also
holds:
! ! 011 -> 011
-----
000
-------
111
--------------
011
** DONE !(P&Q)->(!Pv!Q) is not always a tautology
In classical logic we have the two DeMorgan laws,
!(PvQ)<->(!P&!Q)
!(P&Q)<->(!Pv!Q)
We can split each of those into two implications, and
in H-modal logic three of these implications are tautologies,
but the fourth one is not:
!(PvQ)<-(!P&!Q) is a tautology
!(PvQ)->(!P&!Q) is a tautology
!(P&Q)<-(!Pv!Q) is a tautology
!(P&Q)->(!Pv!Q) is _not_ a tautology
If we take P=00010 and Q=00001, then
!(00010 & 00001)->(!00010 v !00001)
------------- ------ ------
00000 00101 01010
--------------- ---------------
11111 01111
----------------------------------
01111
* ---
* --- 4. ZSets, ZDAGs and ZHAs
** DONE N^2 as a chessboard
In the usual way of representing chess diagrams,
the black pieces start above, the white pieces start below,
the black pawns move down, the white pawns move up.
Let's think of N^2 as an infinite chessboard.
The "positions" of N^2 are the points (x,y), with x,y \in N.
The "positions" of a chessboard are points (x,y), with x,y \in {0,1,...,7}.
Note that in a chessboard we put the pieces in the middle of the squares,
but in N^2 we put them on points.
Diagram: (chessboard in initial position) (N^2)
** DONE N^2 as a chessboard: pawns and monks
In the usual way of representing chess diagrams,
the black pieces start above, the white pieces start below,
the black pawns move down, the white pawns move up.
Let's think of N^2 as an infinite chessboard.
The "positions" of N^2 are the points (x,y), with x,y in N.
The "positions" of a chessboard are points (x,y), with x,y in {0,1,...,7}.
Note that in a chessboard we put the pieces in the middle of the squares,
but in N^2 we put them on points.
The points (x,y) in N^2 with x+y odd have one color - white, say.
The points (x,y) in N^2 with x+y even have the other color - black.
Let's define how some pieces - _inspired_ by chess - move.
We are only interested in how our pieces can _move_ - not in ideas
like "winning" or "losing".
Black pawns move from (x,y) to (x',y-1), where x' in {x-1, x, x+1}.
Black monks move from (x,y) to (x',y-1), where x' in {x-1, x+1}.
(Monks are like bishops, but less powerful).
(x,y) (x,y)
/ | \ / \
v v v v v
(x-1,y-1) (x,y-1) (x+1,y-1) (x-1,y-1) (x+1,y-1)
(x-1,y+1) (x,y+1) (x+1,y+1) (x-1,y+1) (x+1,y+1)
^ ^ ^ ^ ^
\ | / \ /
(x,y) (x,y)
White pawns move from (x,y) to (x',y+1), where x' in {x-1, x, x+1}.
White monks move from (x,y) to (x',y+1), where x' in {x-1, x+1}.
** DONE N^2 as a chessboard: paths
Here are two black pawn's paths.
The one at the left is _not_ a black monk's path,
because it has some (two) vertical moves.
The one at the right _is_ a black monk's path.
(0,7)
(1,6)
(1,5)
(...)
(0,4)
(0,3)
(1,2)
(2,1)
** DONE ZSets
We say that a subset D \subset N^2 is _well-positioned_ when:
* it is non-empty,
* it is finite,
* it touches the vertical axis, i.e., there is an (x,y) in D with x=0,
* it touches the horizontal axis, i.e., there is an (x,y) in D with y=0.
Definition: a _ZSet_ is a subset of N^2 that is well-positioned.
We like ZSets (well-positions subsets of N^2) because we can represent
them unambiguosly using the _bullet notation_:
* { (1,2),
H' := * * == (0,1), (2,1),
* ** (0,0), (2,0),(2,3)}
Later we will have some favourite ZSets, and fixed names for them:
V Vee
K Kite
H House
# (find-LATEX "2014sfc-slides.tex" "ZSets")
** DONE The reading order
The _reading order_ on a ZSet D is how we would read aloud the points
of D as we would read a page of text: top line first, then each
subsequent line until the last; and in each line we go from left to
right.
Formally,
(1,2) << (0,1) << (2,1) << (0,0) << (2,0) << (2,3)
and this is H' with its points _listed_ in reading order:
((1,2), (0,1), (2,1), (0,0), (2,0), (2,3))
** DONE Functions on ZSets (positional notation, and reading aloud)
What happens if we represent function on a given ZSet - say, on
* { (1,2),
H' := * * == (0,1), (2,1),
* ** (0,0), (2,0),(2,0)}
by writing its return values positionally?
Two (super-cool!) things. First, we get something very similar to the
bullet notation... For example, the first and the second projections
on H' can be denoted by just \dagH'102022 and \dagH'211000,
pi: H' -> N == { ((1,2),1), ... } == \dagH'102022
(x,y) |-> x
pi: H' -> N == { ((1,2),1), ... } == \dagH'211000,
(x,y) |-> x
And second, the reading order gives us a way to read aloud the outputs
of these functions in sequence - \dagH'102022 is one-zero-two-etc.
As a bonus, this gives us a way to order functions from a ZSet D to A
when we have an order on A... for example, here are the 8 functions
from Vee to {0,1}:
000 001 010 010 etc
They are listed "in order", because:
000 < 001 < 010
** DONE BPM(D)
If D is ZSet, let's write BPM(D) for the set of black pawn's moves on
D - i.e., the black pawn's moves on N^2 that start and end on points
of D.
For any ZSet D, (D, BPM(D)) is a DAG - a directed acyclical graph,
acyclical because cycles would have to have arrows going up (which we
don't have) to compensate for the arrows going down.
For example, (H', BPM(H')) is this:
(1,2)
/ \
v v
(0,1) (2,1)
| | \
v v v
(0,0) (2,0) (2,3)
Where if we represent BPM(H') as a set of arrows, it becomes this:
{((1,2),(0,1)), ((1,2),(2,1)),
...}
** DONE Transitive-reflexive closures
Let (A,R) be a graph.
R - that represents the arrows - is a relation on A, i.e., R \subseteq A^2.
The transitive closure of (A,R), is obtained by adding all composites of arrows.
The reflexive closure of (A,R) is obtained by adding all identity arrows.
We denote the transitive-reflexive closure of (A,R) by (A,R*).
For exemple, K ("kite") is this, \dagKite*****,
and (K,BPM(K)) and (K,BPM(K)*) are:
(diagram)
** DONE ZDAGs
A _ZDAG_ is a DAG of the form (D,BPM(D)), where D is a ZSet.
A _ZDAG*_ is a directed graph of the form (D,BPM(D)*), where D is a ZSet.
(A ZDAG* has cycles made of identity arrows - it is not acyclical).
Some DAGs are isomorphic to ZDAGs, some DAGs are not...
1
/ \
v v
2 3 == Kv pentagon is not iso to a ZDAG
\ /
v v
4
|
v
5
Some categories - some posets - are isomorphic to ZDAG*s...
For example,
(Kite* and its Hom-sets)
** DONE ZHAs
A ZHA is a ZSet obeying some extra conditions.
A ZHA is a ZSet D that has:
* a top element T_D,
* a bottom element bot_D,
* a left wall, LW_D, that is a black monk's path from T_D to bot_D,
* a right wall, RW_D, that is a black monk's path from T_D to bot_D,
* all the same-color elements between LW_D and RW_D, and nothing else.
This is a ZHA: This is not a ZHA:
* * *
* * * *
*
* * *** *
* * * * *
* * *
* * *
* * is doesn't have a top element,
* its left wall (the red points)
is not a black monk's path,
The red arrows it has points of both colors,
join the points of LW_D, and it has lines without all the
The blue arrows same-color points between the
join the points of RW_D. left wall and the right wall.
This is why we like ZHAs:
If D is a ZHA, then Dup* is a Heyting Algebra,
i.e., we have operations and,or,imp,bij: D->D
that behave as expected
(What does that mean? We will see what
we expect from and, or,imp,bij,T,F soon...)
This - that ZHAs are Heyting Algebras,
and so we can interpret intuitionistic propositional
calculus on them, is an amazing fact, that is
not well-known.
** DONE ZHAs: the (l,r) coordinates
The (l,r) coordinates make it very it easy to define &, v, ->, etc on
ZHAs. Let's use H=... as our example. Here is it with the (x,y)
coordinates of each of its points and the x and y axes,
y
^
9 +
8 + (2,8)
7 +(1,7) (3,7)
6 + (2,6)
5 +(1,5)
4 (0,4) (2,4)
3 +(1,3) (3,3)
2 (0,2) (2,2) (4,2)
1 +(1,1) (3,1)
0 +--+(2,0)+--+--+--+-->x
0 1 2 3 4 5 6
And this is it with the l and r axes drawn on; note that the point
(0,0) in the (l,r) coordinates is the bottom point of H, bot_H=(2,0),
and that when we are talking about the (l,r) coordinates we write lr
instead of (l,r):
l * r 44
^ * * ^ 43 34
\ * / 33
6 X * X 6 32
5 X * * X 5 31 22
4 X * * X 4 21 12
3 * * * 3 20 11 02
2 * * 2 10 01
1 * 1 00
0 0
Formally, the change of coordinates can be done by these formulas.
In a ZDAG whose bottom point is (x0,0),
(x,y) = (x0-l+r,l+r)
(l,r) = (((x-x0)+y)/2,(y-(x-x0))/2)
** DONE ZHAs: True, false, and, or
In a ZHA D,
T_D is the "top" of D,
bot_D is the "bottom" of D (which is always 00),
PvQ is the lowest point above both P and Q,
P&Q is the uppermost point above both P and Q.
In H, T_H=44, bot_H=00, and if P=31 and Q=12 then
PvQ=32 and P&Q=11:
44 top
43 34 ... ...
33 ...
32 PvQ
31 22 .P. ...
21 12 ... .Q.
20 11 02 ... P&Q ...
10 01 ... ...
00 bot
Formally, if P=(l_P,r_P) and Q=(l_Q,r_Q)
then PvQ=(max(l_P,l_Q),max(r_P,r_Q))
and P&Q=(min(l_P,l_Q),min(r_P,r_Q))
(in the (l,r) coordinates).
** DONE ZHAs: <= and ->
In a ZHA D we will have two different notions of "implies".
One - "external" - always returns either "true" or "false", and
another - "internal" - always returns another element of D.
The "external" is written as P<=Q,
and defined as:
P<=Q is true iff l_P<=l_Q and r_P<=r_Q
Intuitively, P<=Q is true iff there is an arrow from P to Q
in Dup*.
The "internal" is written as P->Q,
and we will define it by cases.
(The reasons for this definition will appear later).
If P<=Q, then P->Q=T_D;
otherwise, if P>=Q, then P->Q=Q;
otherwise, let R:=P&Q, and P->Q will be the topmost point in D
belonging to the line that contains both R and Q.
. .
. . . .
. . . . . .
. . . . . .
. . . > > . . .
. P . . . . Q . . .
. . Q . . . P .
. & . . & .
. . . .
. .
** TODO Intuitionistic logic on the ZHAs G, L, S
** TODO Logic on the open subsets of a ZDAG
** TODO Logic on the points of a ZHA
** TODO Sometimes the open subsets of a ZDAG form a ZHA
* ---
* --- 5. A parenthesis: some logics on DAGs (for adults)
** DONE Towards intuitionistic logic
!(P&Q)->(!Pv!Q) is _not_ a tautology in H-intuitionistic logic, but
!(P&Q)->(!Pv!Q) _is_ a tautology in L-intuitionistic logic!
This is easy to check - the table for !(P&Q)->(!Pv!Q) in
L-intuitionistic logic has just 5x5=25 lines:
(table)
Standard logic has lots of tautologies.
L-intuitionistic logic has fewer tautologies.
H-intuitionistic logic has even less.
Pyr-intuitionistic logic has even less.
At the limit we have _intuitionistic logic_, that is defined in a
totally different way, through deduction rules...
But we have this:
if phi(P,Q,...,Z) is not a theorem of intuitionistic logic
then we have a diagram D and truth-values for P,...,Z in
D-intuitionistic logic that make phi(P,Q,...,Z)!=T...
For every non-theorem of intuitionistic (propositional) logic
we have a _finite counter-model_ for it.
This - that every non-theorem of IPL has a finite countermodel - is
not for children (too abstract!), but we are going to see some
examples of how to use tableau methods to produce countermodels; this
should make the meaning of "every non-theorem of IPL has a finite
countermodel" somehow easier to grasp by children.
** TODO Why do our intuitionistic &,v,-> deserve to be called &,v,->?
Our intuitionistic &,v,->,<->, etc obey _most_ of the properties that
we learned to expect from the standard &,v,->,<->... but not all - for
example, !!P may be different from P.
** TODO standard logic = classical propositional calculus
** TODO A positional notation for subsets
** DONE Tarski, Gödel, Kripke, etc (for adults)
A presentation of this for adults could start in this way:
* Every topologic space (X,O(X)) is a model for S4 (Tarski, 1932); nec
P is interpreted as the interior of P.
* The order topology on
GUILL
(or an any other ZDAG) is Alexandroff, and its open sets are exacty
the stable sets, i.e., the ones that don't have a 1 above a 0.
* The Kripke frame on the transitive-reflexive closure of the ZDAG
above (or any other) is a model of S4; nec P corresponds to the
interior of P in the order topology above.
* There is an embedding of intuitionistic logic into the modal logic
S4 (Gödel, 1942) in which the intuitionistic connectives are
translated to modal connectives in this way:
P &_I Q := P &_M Q
P v_I Q := P v_M Q
P ->_I Q := nec (P ->_M Q)
We can connect these four (VERY BIG!) facts, and then conclude that
O(G) is a Heyting Algebra... and we also have this:
* For every non-theorem Phi in intuitionistic propositional logic
there is a ZDAG (finite, planar, etc!...) on which we can build a
countermodel for Phi - we need to use tableau methods.
** DONE Tarski, Gödel, Kripke, etc (for children)
...I apologize to the adults in the audience, but the ideas sketched
in previous slide are is not how we are going to do things here... we
will do everything here "for children", with brief explanations at
some points of what are Kripke frames in general, S4 in general, logic
in arbitrary topologies, tableaux, and so on.
* ---
* --- What properties do we expect of &,v,->,etc?
* ---
* --- Logic in ZHAs
* TODO ! and <->
* ---
* --- Topologies and S4
* TODO Modal and intuitionistic truth-values on a ZDAG
* TODO The order topology on a ZDAG
* TODO The open sets of G correspond to the points of a ZDAG
* TODO The interior of a subset of D
* TODO Some O(D)s are also ZSets
Let G ("Guill") be this ZSet: ,
and let's see if we can represent its set of open subsets, O(G),
in a nice way.
* ---
* --- Priming
Let D be a ZSet, and let's write
* ---
* DONE Interlude (for adults): categories, posets, toposes
Lawvere often says:
Never underestimate the power of the Sierpinski topos.
The Sierpinski topos is the category of functors Set^*->*
(a presheaf).
The category *->* "is" (Two,BPM(Two)^*).
The Sierpinski topos "is" Set^Two.
Toposes of the form Set^bfD, when bfD is a ZDAG seen as a poset, are
great for when we want to work out examples fully, because their
object and morphisms are easy to draw explicitly.
Mathematicians love general things, infinite things, and continuous
things.
"Children" love finite things.
We are going to do categories for children, and toposes for children,
by using categories like
Set^Two, Set^HTwo, Set^V, Set^K...
as archetypal examples for the general theory.
* DONE Interlude (for adults): NSA
In Non-Standandard Analysis we construct an universe with
infinitesimals, Set^*, from the standard universe, Set, using a
ultrapower trick, and we do our proofs half in Set, half in Set^*,
using the transfer theorems to move between both...
We are going to do something _slighly similar_ to that here.
For example, we are going to do a constructions and a proofs in
Set^Vee and in a general topos E, and we will move between Set^Vee and
E - but we will do that by drawing two diagramss with similar shapes,
one corresponding to the general case in E, and another the a
particular case of that in Set^V.
This will happen only at the end.
Before that we will apply the same idea on Heyting Algebras,
The part on Heyting Algebras will be much more accessible and much
easier to understand... I mentioned toposes first only because they
are more famous, and people get more excited when we mention them than
Heyting Algebras... sorry! =)
_End of the interlude_
* TODO ZHAs are Heyting Algebras
* TODO Subsets / Modal truth values
* TODO Open subsets / intuitionistic truth values
* TODO Interior
* ---
* --- Modalities for children
* DONE The axioms
A modality on Omega is an operation J: Omega -> Omega 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) := T (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_bot(P) ("boolean quotient" - particular case))
= (P -> bot) -> bot
= not not P
What other operations obey these axioms?
* Modalities on ZDAGs correspond to dividing by diagonal lines
How do different modalities interact?
(There is an algebra of modalities!)
How does a modality interact with &, or, ->, 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
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 ..
* DONE Stable and equivalent truth-values
Remember: a modality on Om is an operation J: Om -> Om 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)
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 Om is an operation J: Om -> Om 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
..
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
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 (2)
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,
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 or
We know (proofs later!) that "v" 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)vJ(Q))
^ ^ ^
/ | \
/ | \
J(J(P)vQ) J(P)vJ(Q) J(PvJ(Q))
^ ^ ^ ^ ^ ^
| \/ \/ |
| /\ /\ |
J(P)vQ J(PvQ) PvJ(Q)
^ ^ ^
\ | /
\ | /
PvQ
But we know more. We can prove that we have J(J(P)vJ(Q))<=J(PvQ),
------ ------
P<=PvQ Q<=PvQ
------------Mo ------------Mo
J(P)<=J(PvQ) J(Q)<=J(PvQ)
---------------------------
J(P)vJ(Q)<=J(PvQ)
-----------------------Mo ----------------M2
J(J(P)vJ(Q))<=J(J(PvQ)) J(J(PvQ))=J(PvQ)
--------------------------------------------
J(J(P)vJ(Q))<=J(PvQ)
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.
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 J cannot 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.
* TODO Borders like "y"s are not possible (2)
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 Equivalence classes are diamond-shaped regions
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
* HALF Stable elements and diamond-shaped regions
Two slogans:
Equivalent elements form diamond-shaped regions
Stable elements form a sub-ZDAG
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
* ---
* --- Categories for children
* ZDAGs as graphs
* ZDAGs as categories
* K as a category
# (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
* Set as our archetypal category
* Posets, relations, RT-closure
* Products
* Judgments
* Internal language
* Adjunctions
* ZHAs as categories
* ---
* --- Toposes
* Ztoposes
* ---
* Garbage
* ZDAGs: abuse of language (delete this)
Sometimes, by abuse of language, we will say that things like (D,BPM(D)*) are ZDAGs...
A (D,BPM(D)*) is not acyclical, but its only cycles are made of identity arrows
(so we may think that they "don't really count" as cycles...)
We will sometimes use the bullet notation for ZDAGs -
both for the things like (D,BPM(D)) and for the things like (D,BPM(D)*),
and sometimes for (D,BMM(D)), (D,BMM(D)*),
and for (D,BPM(D)*) and (D,BMM(D)*) seen as categories, too...
We will return to this later -
and see the disambiguation tricks.
Note that all these things are isomorphic,
(K,BPM(K)) == (antiK,WPM(antiK)) == (smashedantiK,WPM(smashedantiK)), 12345
but this DAG is not isomorphic to a ZDAG:
(pentagon)
* Local variables
# (find-es "org" "TODO-and-DONE")
#+TODO: TODO | DONE | HALF
# Local Variables:
# coding: raw-text-unix
# coding: utf-8-unix
# modes: (org-mode emacs-lisp-mode fundamental-mode)
# End: