mirror of
https://github.com/abuseofnotation/category-theory-illustrated.git
synced 2024-09-11 08:55:55 +03:00
last edits, submitted for review
This commit is contained in:
Boris Marinov
parent
545ce22d5f
commit
593b095612
210
_chapters/04_order/lattice_meet_join.svg
Normal file
210
_chapters/04_order/lattice_meet_join.svg
Normal file
@ -0,0 +1,210 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
xmlns:dc="http://purl.org/dc/elements/1.1/"
|
||||
xmlns:cc="http://creativecommons.org/ns#"
|
||||
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
|
||||
xmlns:svg="http://www.w3.org/2000/svg"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
width="595.29999"
|
||||
height="177"
|
||||
version="1.1"
|
||||
id="svg8680"
|
||||
sodipodi:docname="lattice_meet_join.svg"
|
||||
inkscape:version="0.92.5 (2060ec1f9f, 2020-04-08)">
|
||||
<metadata
|
||||
id="metadata8686">
|
||||
<rdf:RDF>
|
||||
<cc:Work
|
||||
rdf:about="">
|
||||
<dc:format>image/svg+xml</dc:format>
|
||||
<dc:type
|
||||
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
|
||||
<dc:title></dc:title>
|
||||
</cc:Work>
|
||||
</rdf:RDF>
|
||||
</metadata>
|
||||
<defs
|
||||
id="defs8684" />
|
||||
<sodipodi:namedview
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1"
|
||||
objecttolerance="10"
|
||||
gridtolerance="10"
|
||||
guidetolerance="10"
|
||||
inkscape:pageopacity="0"
|
||||
inkscape:pageshadow="2"
|
||||
inkscape:window-width="1920"
|
||||
inkscape:window-height="1016"
|
||||
id="namedview8682"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.9601497"
|
||||
inkscape:cx="297.64999"
|
||||
inkscape:cy="183.04094"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="27"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg8680" />
|
||||
<ellipse
|
||||
cy="49.774296"
|
||||
cx="183.96703"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.048471"
|
||||
ry="28.48292"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8632" />
|
||||
<ellipse
|
||||
cy="48.985752"
|
||||
cx="181.80623"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.048471"
|
||||
ry="28.48292"
|
||||
fill="#cee7cc"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8634" />
|
||||
<ellipse
|
||||
cy="116.34947"
|
||||
cx="113.95921"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.501013"
|
||||
ry="28.92638"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8636" />
|
||||
<ellipse
|
||||
cy="114.52618"
|
||||
cx="111.04417"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.501013"
|
||||
ry="28.92638"
|
||||
fill="#caebfc"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8638" />
|
||||
<ellipse
|
||||
cy="117.33477"
|
||||
cx="253.97536"
|
||||
stroke-miterlimit="10"
|
||||
rx="30.254747"
|
||||
ry="29.665482"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8640" />
|
||||
<ellipse
|
||||
cy="115.4131"
|
||||
cx="251.01039"
|
||||
stroke-miterlimit="10"
|
||||
rx="30.254747"
|
||||
ry="29.665482"
|
||||
fill="#f8f7cb"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8642" />
|
||||
<path
|
||||
d="m 243.06997,87.886225 c 0,0 -0.24721,-0.420758 -0.73002,-1.164401 a 87.338135,87.338135 0 0 0 -2.09219,-3.056804 c -0.88995,-1.24714 -1.99533,-2.620911 -3.21119,-4.082466 -1.2658,-1.45651 -2.63655,-2.951363 -4.10264,-4.387693 a 70.868018,70.868018 0 0 0 -4.46589,-4.004267 c -1.48981,-1.186095 -2.91958,-2.27936 -4.17278,-3.142571 -1.25369,-0.862706 -2.33637,-1.545303 -3.14307,-2.007935 -0.10595,-0.03935 -0.16094,-0.08324 -0.21593,-0.127136 -0.0555,-0.04389 -0.10494,-0.03885 -0.16043,-0.08274 l -0.11049,-0.08778 2.91151,-4.953244 c -2.49075,-0.142776 -5.01631,-0.133694 -7.4556,0.21391 -1.19417,0.171028 -2.37824,0.440435 -3.50733,0.753229 -1.12404,0.362235 -2.19258,0.768363 -3.1456,1.311212 a 15.851592,15.851592 0 0 1 2.52254,1.873737 c 0.73304,0.717912 1.41615,1.44087 1.99885,2.174422 1.17651,1.564475 2.10783,3.203616 2.9443,4.902289 l 2.91151,-4.953748 c 0,0 0.0555,0.04389 0.10493,0.03885 0.0505,-0.005 0.0555,0.04389 0.111,0.08829 0.055,0.04389 0.15992,0.08274 0.21492,0.126127 0.75171,0.419245 1.78494,1.106887 3.03813,1.970098 1.20376,0.868255 2.62798,1.912079 4.06784,3.103219 1.43986,1.191139 2.94531,2.524045 4.35591,3.916483 1.4106,1.392438 2.7763,2.838353 3.98711,4.250971 1.21082,1.412618 2.26624,2.791434 3.15064,3.989637 0.88491,1.198203 1.54884,2.220333 2.03216,2.963975 a 33.428596,33.428596 0 0 1 0.72951,1.164401 z m -117.158,0.375857 c 0,0 0.2124,-0.415713 0.50148,-1.085697 0.1675,-0.361732 0.3804,-0.77694 0.58825,-1.241591 0.25781,-0.469191 0.56152,-0.992364 0.86019,-1.56397 1.29456,-2.297017 3.23842,-5.197425 5.55562,-7.885435 2.3172,-2.687506 4.91793,-5.055155 7.03333,-6.68471 0.51308,-0.442957 1.04029,-0.739102 1.46206,-1.074599 0.42227,-0.336001 0.79913,-0.61802 1.13514,-0.79712 0.28655,-0.175064 0.42731,-0.287064 0.42731,-0.287064 l 3.27576,4.697963 a 42.308414,42.308414 0 0 1 6.41228,-10.537625 c -4.35591,-0.688652 -9.00645,-0.756255 -13.84568,-0.162956 l 3.27576,4.697964 -0.47726,0.2911 c -0.33146,0.228542 -0.70833,0.510561 -1.18054,0.851103 -0.42228,0.335496 -0.94444,0.681083 -1.50747,1.12858 -2.1608,1.683034 -4.90683,4.113241 -7.26943,6.854729 -2.41255,2.746029 -4.44723,5.754401 -5.78265,8.153833 -0.34862,0.576147 -0.64729,1.148257 -0.90509,1.617448 -0.25831,0.469191 -0.46616,0.933337 -0.63366,1.295572 -0.33449,0.723463 -0.54739,1.139176 -0.54739,1.139176 z"
|
||||
fill="#808285"
|
||||
id="path8648"
|
||||
style="stroke-width:0.504506" />
|
||||
<ellipse
|
||||
cy="48.283623"
|
||||
cx="408.12823"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.048471"
|
||||
ry="28.48292"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8650" />
|
||||
<ellipse
|
||||
cy="47.495064"
|
||||
cx="405.96741"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.048471"
|
||||
ry="28.48292"
|
||||
fill="#cee7cc"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8652" />
|
||||
<ellipse
|
||||
cy="114.85828"
|
||||
cx="338.1199"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.501013"
|
||||
ry="28.92638"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8654" />
|
||||
<ellipse
|
||||
cy="113.03498"
|
||||
cx="335.20535"
|
||||
stroke-miterlimit="10"
|
||||
rx="29.501013"
|
||||
ry="28.92638"
|
||||
fill="#caebfc"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8656" />
|
||||
<ellipse
|
||||
cy="115.84409"
|
||||
cx="478.13657"
|
||||
stroke-miterlimit="10"
|
||||
rx="30.254747"
|
||||
ry="29.665482"
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8658" />
|
||||
<ellipse
|
||||
cy="113.92243"
|
||||
cx="475.1716"
|
||||
stroke-miterlimit="10"
|
||||
rx="30.254747"
|
||||
ry="29.665482"
|
||||
fill="#f8f7cb"
|
||||
stroke="#808285"
|
||||
stroke-width="2.98567"
|
||||
id="ellipse8660" />
|
||||
<path
|
||||
d="m 376.7676,55.92184 c 0,0 -0.45204,0.19676 -1.25622,0.59129 a 89.797604,89.797604 0 0 0 -3.31713,1.7244 c -1.35712,0.73961 -2.86459,1.67546 -4.47245,2.71071 -1.60837,1.08419 -3.26718,2.26675 -4.87504,3.54769 a 70.925027,70.925027 0 0 0 -4.52341,3.94221 c -1.35712,1.33089 -2.61334,2.61183 -3.61832,3.74546 -1.00498,1.13312 -1.80916,2.11893 -2.3621,2.85803 -0.0505,0.0984 -0.1009,0.14782 -0.15085,0.19676 -0.0505,0.0494 -0.0505,0.0989 -0.1009,0.14832 l -0.0999,0.0984 -4.7242,-3.35093 c -0.40209,2.41457 -0.65333,4.87858 -0.55294,7.29314 0.0505,1.18257 0.2008,2.36563 0.40209,3.49876 0.25125,1.13362 0.55294,2.21781 1.00498,3.20361 a 15.6957,15.6957 0 0 1 2.16131,-2.26725 c 0.80368,-0.64072 1.60786,-1.23201 2.41204,-1.72491 1.70877,-0.9853 3.46798,-1.7244 5.27714,-2.36512 l -4.7242,-3.35094 c 0,0 0.0504,-0.0494 0.0504,-0.0984 0,-0.0494 0.0505,-0.0494 0.1004,-0.0989 0.0505,-0.0489 0.1009,-0.14782 0.15085,-0.19676 0.50248,-0.69016 1.30667,-1.62652 2.31164,-2.75965 1.00498,-1.08468 2.21126,-2.36563 3.56838,-3.64657 1.35712,-1.28144 2.86459,-2.61183 4.4225,-3.84434 1.55792,-1.2315 3.16628,-2.41406 4.7242,-3.4488 1.55792,-1.03525 3.06589,-1.92217 4.37256,-2.66127 1.30667,-0.73911 2.41204,-1.28145 3.21623,-1.67497 0.80418,-0.39452 1.25622,-0.59178 1.25622,-0.59178 z m 57.29326,2.95692 c 0,0 0.4021,0.2462 1.05543,0.59077 0.35215,0.19727 0.75373,0.44397 1.20628,0.69017 0.45254,0.29564 0.95503,0.64072 1.50797,0.9853 2.21125,1.4782 4.97544,3.64657 7.48788,6.16002 2.51295,2.51295 4.67425,5.2726 6.13177,7.49041 0.40209,0.54184 0.65334,1.08418 0.95453,1.52765 0.30169,0.44346 0.55294,0.83748 0.70379,1.18256 0.15084,0.29564 0.25124,0.44346 0.25124,0.44346 l -5.07584,2.75965 a 43.290688,43.290688 0 0 1 10.10173,7.2437 c 1.10538,-4.18841 1.60786,-8.7219 1.45752,-13.5021 l -5.07634,2.75965 -0.25125,-0.49291 c -0.20079,-0.34508 -0.45203,-0.7391 -0.75373,-1.232 -0.30169,-0.44346 -0.60288,-0.9853 -1.00498,-1.57709 -1.50797,-2.26674 -3.71922,-5.17421 -6.28211,-7.7366 -2.56289,-2.61183 -5.42798,-4.87858 -7.73963,-6.40623 -0.55294,-0.39402 -1.10588,-0.7391 -1.55792,-1.03423 -0.45254,-0.29615 -0.90508,-0.54235 -1.25622,-0.73961 a 36.323454,36.323454 0 0 1 -1.10588,-0.64072 z"
|
||||
fill="#808285"
|
||||
id="path8666"
|
||||
style="stroke-width:0.504506" />
|
||||
<text
|
||||
style="font-weight:400;font-size:20.67840004px;line-height:1.25;font-family:sans-serif;letter-spacing:0;word-spacing:0;fill:#7e7e7e;stroke-width:0.51689899"
|
||||
x="383.28946"
|
||||
y="163.8709"
|
||||
font-weight="400"
|
||||
font-size="20.6784px"
|
||||
letter-spacing="0"
|
||||
word-spacing="0"
|
||||
id="text8674">
|
||||
<tspan
|
||||
x="383.28946"
|
||||
y="163.8709"
|
||||
id="tspan8672"
|
||||
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.51689899">AND</tspan>
|
||||
</text>
|
||||
<text
|
||||
style="font-weight:400;font-size:21.88019943px;line-height:1.25;font-family:sans-serif;letter-spacing:0;word-spacing:0;fill:#7e7e7e;stroke-width:0.54709399"
|
||||
x="162.58644"
|
||||
y="164.60921"
|
||||
font-weight="400"
|
||||
font-size="21.8802px"
|
||||
letter-spacing="0"
|
||||
word-spacing="0"
|
||||
id="text8678">
|
||||
<tspan
|
||||
x="162.58644"
|
||||
y="164.60921"
|
||||
id="tspan8676"
|
||||
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.54709399">OR</tspan>
|
||||
</text>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 9.7 KiB |
@ -170,7 +170,7 @@ If we view logical operators as functions, from and to the set of boolean values
|
||||
|
||||
|
||||
|
||||
If we want to be formal about it, we might say that applying negation two times is equivalent to applying the identity function.
|
||||
If we want to be formal about it, we might say that applying negation two times is equivalent to applying the *identity* function.
|
||||
|
||||
|
||||
|
||||
@ -371,22 +371,22 @@ The second part involves converting a category into a logical system - this is m
|
||||
|
||||
These criteria have to guarantee that a category has objects that correspond to all valid logical propositions and no objects that correspond to invalid ones.
|
||||
|
||||
Categories that adhere to these criteria are called *cartesian closed categories*. We won't describe them here directly, but instead we would start with a similar but simpler structures that are instance of them and that we already examined - orders.
|
||||
Categories that adhere to these criteria are called *cartesian closed categories*, but we won't look into them directly. Instead, we would present logic using a similar but simpler structures that we already examined - orders.
|
||||
|
||||
Logics as orders
|
||||
---
|
||||
|
||||
We will now do something that is quite characteristic of category theory - examining a concept in a more limited version of the theory, in order to make things simpler for ourselves.
|
||||
|
||||
So we already saw that a logical system, along with the set of primary propositions forms a category.
|
||||
So we already saw that a logical system, along with a set of its propositions, forms a category.
|
||||
|
||||
|
||||
|
||||
If we assume that there is only one way to go from proposition **A**, to proposition **B** (or there are many ways, but we are not interested in the difference between them), then logic is not only a category, but a *preorder* in which the relationship "bigger than" is taken to mean "implies".
|
||||
If we assume that there is only one way to go from proposition **A**, to proposition **B** (or that there are many ways, but we are not interested in the difference between them), then logic is not only a category, but a *preorder* in which the relationship "bigger than" is taken to mean "implies".
|
||||
|
||||
|
||||
|
||||
Furthermore, if we count propositions that follow from each other (or sets of propositions that have the same truth value and can be proven by the same proof) as equivalent, then logic is a proper *partial order*.
|
||||
Furthermore, if we count propositions that follow from each other (or sets of propositions that are proven by the same proof) as equivalent, then logic is a proper *partial order*.
|
||||
|
||||
|
||||
|
||||
@ -394,14 +394,16 @@ And so it can be represented by a Hasse diagram, yey.
|
||||
|
||||
|
||||
|
||||
Now let's examine the question that we asked before - exactly which ~~categories~~ orders represent logic and what laws does an order have to obey so it is isomorphic to a logic? We will attempt to answer this question as we examine the elements of logic again, this time in the context of orders.
|
||||
Now let's examine the question that we asked before - exactly which ~~categories~~ orders represent logic and what laws does an order have to obey so it is isomorphic to a logical system? We will attempt to answer this question as we examine the elements of logic again, this time in the context of orders.
|
||||
|
||||
The **and** and **or** operations
|
||||
---
|
||||
|
||||
By now you probably realized that the **and** and **or** operations are the bread and butter of logic (although it's not clear which is which). As we saw, in the BHK interpretation those were represented by set *products* and *sums*. And the equivalent constructs in the realm of order theory are *meets* and *joins* (in category-theoretic terms *products* and *coproducts*.)
|
||||
By now you probably realized that the **and** and **or** operations are the bread and butter of logic (although it's not clear which is which). As we saw, in the BHK interpretation those are represented by set *products* and *sums*. The equivalent constructs in the realm of order theory are *meets* and *joins* (in category-theoretic terms *products* and *coproducts*.)
|
||||
|
||||
Here comes the first criteria for an order to represent logic accurately - it has to have **meet** and **join** operations for all elements. Having two elements without a meet would mean that you would have a logical system where there are propositions for which you cannot say that one or the other is true. And this not how logic works, so our order has to have meets and joins for all elements. Incidentally we already know how such orders are called - they are called *lattices*.
|
||||
|
||||
|
||||
Here comes the first criteria for an order to represent a logical system accurately - *it has to have **meet** and **join** operations for all elements*. Having two elements without a meet would mean that you would have a logical system where there are propositions for which you cannot say that one or the other is true. And this not how logic works, so our order has to have meets and joins for all elements. Incidentally we already know how such orders are called - they are called *lattices*.
|
||||
|
||||
One more important law concerning the **and** and **or** operations that is not always present in the **meet**-s and **join**-s concerns the connection between the two, i.e. way that the **and** and **or** operations distribute, over one another.
|
||||
|
||||
@ -409,26 +411,22 @@ One more important law concerning the **and** and **or** operations that is no
|
||||
|
||||
Lattices that obey this law are called *distributive lattices*.
|
||||
|
||||
Wait, where have we heard about distributive lattices before? In the previous chapter we said that they are isomorphic to *inclusion orders* i.e. orders which contain all combinations of sets of a given number of elements.
|
||||
|
||||
And if you think about the BHK interpretation you'll see why: "logical" orders are isomorphic to inclusion orders. The elements which participate in the inclusion are our prime propositions. And the inclusions are all combinations of these elements, in an **or** relationship (for simplicity's sake, we are ignoring the **and** operation.)
|
||||
Wait, where have we heard about distributive lattices before? In the previous chapter we said that they are isomorphic to *inclusion orders* i.e. orders which contain all combinations of sets of a given number of elements. The fact that they popped up again is not coincidental - "logical" orders are isomorphic to inclusion orders. To understand why, you only need to think about the BHK interpretation - the elements which participate in the inclusion are our prime propositions. And the inclusions are all combinations of these elements, in an **or** relationship (for simplicity's sake, we are ignoring the **and** operation.)
|
||||
|
||||
|
||||
|
||||
So in order for our distributive lattice to represent logic accurately, it has to have a minimum and maximum objects.
|
||||
|
||||
**NB: For historical reasons, the symbols for *and* and *or* logical operations are flipped when compared to arrows in the diagrams ∧ is *and* and ∨ is *or*.**
|
||||
|
||||
The *negation* operation
|
||||
---
|
||||
|
||||
In order for a distributive lattice to represent logic, it has to also have objects that correspond to the values **True** and **False**. But in order for us to mandate that these objects exist, we must first find a way to specify what they are in order/category-theoretic terms.
|
||||
In order for a distributive lattice to represent a logical system, it has to also have objects that correspond to the values **True** and **False**. But in order to mandate that these objects exist, we must first find a way to specify what they are in order/category-theoretic terms.
|
||||
|
||||
A well-known result in logic, called *the principle of explosion*, states that if we have a proof of **False** (or if "**False** is true" if we use the terminology of classical logic), than any and every statement can be proven. And it is also obvious that no true statement implies False. So here is it.
|
||||
A well-known result in logic, called *the principle of explosion*, states that if we have a proof of **False** (or if "**False** is true" if we use the terminology of classical logic), then any and every other statement can be proven. And we also know that no true statement implies **False** (in fact in intuinistic logic this is the definition of a true statement). Based on these criteria we know that the **False** object would look like this when compared to other objects:
|
||||
|
||||
|
||||
|
||||
Circling back to the set-theoretic BHK interpretation, we see that the empty set fits both conditions.
|
||||
Circling back to the BHK interpretation, we see that the empty set fits both conditions.
|
||||
|
||||
|
||||
|
||||
@ -436,18 +434,19 @@ Conversely, the proof of **True** (or the statement that "**True** is true") is
|
||||
|
||||
|
||||
|
||||
So **True** and **False** are just the *greatest* and *least* objects of our order (in category-theoretic terms *terminal* and *initial* object.) This is another example of the categorical concept of duality - **True** and **False** are dual to each other, just like **and** and **or**.
|
||||
So **True** and **False** are just the *greatest* and *least* objects of our order (in category-theoretic terms *terminal* and *initial* object.)
|
||||
|
||||
|
||||
|
||||
This is another example of the categorical concept of duality - * **True** and **False** are dual to each other*, (which makes a lot of sense if you think about it).
|
||||
|
||||
So in order to represent logic, our distributive lattice has to also be *bounded* i.e. it has to have greatest and least elements.
|
||||
|
||||
The *implies* operation
|
||||
---
|
||||
|
||||
Finally, if a lattice really is isomorphic to a set of propositions, we it also has to have *function objects* i.e. there needs to be a rule that identifies a unique object **A → B** for each pair of objects **A** and **B**, such that all axioms of intuinistic logic are followed.
|
||||
|
||||
How would this object be described? You guessed it, using categorical language i.e. by recognizing a structure that consists of set of relations between objects in which (A → B) plays a part.
|
||||
Finally, if a lattice really represents a logical system (that is, it is isomorphic to a set of propositions) it also has to have *function objects* i.e. there needs to be a rule that identifies a unique object **A → B** for each pair of objects **A** and **B**, such that all axioms of logic are followed.
|
||||
How would this object be described? You guessed it, using categorical language i.e. by recognizing a structure that consisting of set of relations between objects, in which (**A → B**) plays a part.
|
||||
|
||||
|
||||
|
||||
@ -459,7 +458,9 @@ This definition is not complete, however, because **(A → B)** is *not the onl
|
||||
|
||||
|
||||
|
||||
Or, using the logic terminology, we say that **A → B ∧ C** and **A → B ∧ C ∧ D** etc. are all "stronger" results than (**A → B**) and so (**A → B**) is the weakest result that fits the criteria (stronger results lay lower in the diagram).
|
||||
Or, using the logic terminology, we say that **A → B ∧ C** and **A → B ∧ C ∧ D** etc. are all "stronger" results than (**A → B**) and so (**A → B**) is the weakest result that fits the formula (stronger results lay lower in the diagram).
|
||||
|
||||
So this is the final condition for an order/lattice to be a representation of logic - for each pair **A** and **B**, it has to have a unique object **X** which obey the formula **A ∧ X → B** and the universal property. In category theory this object is called the *exponential object*.
|
||||
|
||||
Without being too formal, let's try to test if this definition captures the concept correctly by examining a few special cases.
|
||||
|
||||
@ -481,6 +482,8 @@ And what if **B** is lower than **A**. In this case the topmost object that fits
|
||||
|
||||
Translated to logical language, says that if **B → A**, then the proof of **(A → B)** is just the proof of **B**.
|
||||
|
||||
So this is the final condition for an order to be a representation of logic - for each pair **A** and **B**, it has to have a unique object **X** which obey the formula **A ∧ X → B** and the universal property. In category theory this object is called the *exponential object*.
|
||||
Note that this definition does not follow the one from the truth tables exactly. This is because this definition is valid specifically for intuinistic logic. For classical logic, the definition of **(A → B)** is simpler - it is just equivalent to (**-A ∨ B**).
|
||||
|
||||
By the way, distributivity follows from this criteria, so we are left with just the following two points: Logic is represented by an order that has with *meet and joins* and a *functional object*. Which is, I think, the neatest definition of logic there is.
|
||||
By the way, the law of distributivity follows from this criteria, so the only criteria that are left for an lattice to follow the laws of intuinistic logic is for it to be *bounded* i.e. to have greatest and least objects (**True** and **False**) and to have a function object as described above. Lattices that follow these criteria are called *Heyting algrebras*.
|
||||
|
||||
And for a lattice to follow the laws of classical logic it has to be *bounded* and *distributive* and to be *complemented* which is to say that each proposition **A** should be complemented with a unique proposition **-A** (such that **A ∨ -A = 1** and **A ∧ -A = 0**). These lattices are called *Boolean algebras*.
|
||||
|
||||
186
_chapters/05_logic/lattice_meet_join.svg
Normal file
186
_chapters/05_logic/lattice_meet_join.svg
Normal file
@ -0,0 +1,186 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
xmlns:dc="http://purl.org/dc/elements/1.1/"
|
||||
xmlns:cc="http://creativecommons.org/ns#"
|
||||
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
|
||||
xmlns:svg="http://www.w3.org/2000/svg"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
width="595.29999"
|
||||
height="177"
|
||||
version="1.1"
|
||||
id="svg8680"
|
||||
sodipodi:docname="lattice_meet_join.svg"
|
||||
inkscape:version="0.92.5 (2060ec1f9f, 2020-04-08)">
|
||||
<metadata
|
||||
id="metadata8686">
|
||||
<rdf:RDF>
|
||||
<cc:Work
|
||||
rdf:about="">
|
||||
<dc:format>image/svg+xml</dc:format>
|
||||
<dc:type
|
||||
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
|
||||
<dc:title></dc:title>
|
||||
</cc:Work>
|
||||
</rdf:RDF>
|
||||
</metadata>
|
||||
<defs
|
||||
id="defs8684" />
|
||||
<sodipodi:namedview
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1"
|
||||
objecttolerance="10"
|
||||
gridtolerance="10"
|
||||
guidetolerance="10"
|
||||
inkscape:pageopacity="0"
|
||||
inkscape:pageshadow="2"
|
||||
inkscape:window-width="1920"
|
||||
inkscape:window-height="1016"
|
||||
id="namedview8682"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.9601497"
|
||||
inkscape:cx="297.64999"
|
||||
inkscape:cy="183.04094"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="27"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg8680" />
|
||||
<ellipse
|
||||
cy="66.158188"
|
||||
cx="210.19122"
|
||||
stroke-miterlimit="10"
|
||||
rx="15.777238"
|
||||
ry="15.470067"
|
||||
id="ellipse8632"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="65.729904"
|
||||
cx="209.01761"
|
||||
stroke-miterlimit="10"
|
||||
rx="15.777238"
|
||||
ry="15.470067"
|
||||
id="ellipse8634"
|
||||
style="fill:#cee7cc;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="102.31749"
|
||||
cx="172.16754"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.023029"
|
||||
ry="15.710926"
|
||||
id="ellipse8636"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="101.32719"
|
||||
cx="170.58427"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.023029"
|
||||
ry="15.710926"
|
||||
id="ellipse8638"
|
||||
style="fill:#caebfc;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="102.85265"
|
||||
cx="248.21519"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.432407"
|
||||
ry="16.112358"
|
||||
id="ellipse8640"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="101.80891"
|
||||
cx="246.60481"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.432407"
|
||||
ry="16.112358"
|
||||
id="ellipse8642"
|
||||
style="fill:#f8f7cb;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<path
|
||||
d="m 242.29209,86.858106 c 0,0 -0.13427,-0.228528 -0.3965,-0.632427 a 47.436386,47.436386 0 0 0 -1.13634,-1.660257 c -0.48336,-0.677365 -1.08373,-1.423508 -1.74411,-2.217329 -0.6875,-0.791082 -1.432,-1.602988 -2.22829,-2.383109 a 38.490892,38.490892 0 0 0 -2.42558,-2.174857 c -0.80916,-0.64421 -1.58572,-1.238 -2.26638,-1.70684 -0.68092,-0.468566 -1.26896,-0.839308 -1.70711,-1.09058 -0.0575,-0.02137 -0.0874,-0.04521 -0.11728,-0.06905 -0.0301,-0.02384 -0.057,-0.0211 -0.0871,-0.04494 l -0.06,-0.04768 1.58135,-2.69028 c -1.35282,-0.07755 -2.72454,-0.07261 -4.0494,0.116182 -0.64859,0.09289 -1.2917,0.239216 -1.90495,0.409105 -0.61051,0.196743 -1.19087,0.417325 -1.70849,0.712165 a 8.6095523,8.6095523 0 0 1 1.37008,1.017692 c 0.39814,0.389923 0.76916,0.782587 1.08565,1.181005 0.639,0.849721 1.14483,1.739995 1.59915,2.662604 l 1.58134,-2.690554 c 0,0 0.0301,0.02384 0.057,0.0211 0.0274,-0.0027 0.0301,0.02384 0.0603,0.04795 0.0299,0.02384 0.0869,0.04494 0.11673,0.0685 0.40828,0.227706 0.96946,0.601189 1.65012,1.070029 0.6538,0.471579 1.42734,1.038516 2.20938,1.685466 0.78204,0.646949 1.5997,1.370897 2.36585,2.127178 0.76614,0.756282 1.5079,1.541609 2.16554,2.308851 0.65763,0.767242 1.23087,1.516125 1.71122,2.166911 0.48062,0.650786 0.84123,1.20594 1.10374,1.609838 a 18.156236,18.156236 0 0 1 0.39622,0.632427 z m -63.63259,0.204141 c 0,0 0.11536,-0.225788 0.27237,-0.58968 0.091,-0.196469 0.2066,-0.421983 0.3195,-0.674351 0.14002,-0.254834 0.30498,-0.538988 0.46719,-0.849447 0.70313,-1.24759 1.7589,-2.822903 3.01746,-4.282854 1.25855,-1.459679 2.67109,-2.745631 3.82004,-3.6307 0.27867,-0.240585 0.56502,-0.401432 0.7941,-0.583652 0.22935,-0.182494 0.43403,-0.335668 0.61653,-0.432943 0.15564,-0.09508 0.23209,-0.155915 0.23209,-0.155915 l 1.77918,2.551628 a 22.979175,22.979175 0 0 1 3.48273,-5.723352 c -2.36584,-0.374031 -4.89172,-0.410748 -7.52007,-0.08851 l 1.77918,2.551628 -0.25922,0.158107 c -0.18002,0.124129 -0.38472,0.277303 -0.64119,0.462263 -0.22935,0.18222 -0.51296,0.36992 -0.81876,0.612971 -1.1736,0.914115 -2.66507,2.234045 -3.94828,3.723043 -1.31034,1.491464 -2.41545,3.125416 -3.14076,4.428631 -0.18935,0.312925 -0.35156,0.623658 -0.49158,0.878492 -0.1403,0.254834 -0.25319,0.506928 -0.34417,0.703671 -0.18167,0.392938 -0.2973,0.618726 -0.2973,0.618726 z"
|
||||
id="path8648"
|
||||
style="fill:#808285;stroke-width:0.2740148"
|
||||
inkscape:connector-curvature="0" />
|
||||
<ellipse
|
||||
cy="63.818054"
|
||||
cx="390.60999"
|
||||
stroke-miterlimit="10"
|
||||
rx="15.777238"
|
||||
ry="15.470067"
|
||||
id="ellipse8650"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="63.389763"
|
||||
cx="389.43637"
|
||||
stroke-miterlimit="10"
|
||||
rx="15.777238"
|
||||
ry="15.470067"
|
||||
id="ellipse8652"
|
||||
style="fill:#cee7cc;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="99.977081"
|
||||
cx="352.58603"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.023029"
|
||||
ry="15.710926"
|
||||
id="ellipse8654"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="98.986778"
|
||||
cx="351.00302"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.023029"
|
||||
ry="15.710926"
|
||||
id="ellipse8656"
|
||||
style="fill:#caebfc;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="100.5125"
|
||||
cx="428.63394"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.432407"
|
||||
ry="16.112358"
|
||||
id="ellipse8658"
|
||||
style="opacity:0.13999999;stroke:#000000;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<ellipse
|
||||
cy="99.468781"
|
||||
cx="427.02356"
|
||||
stroke-miterlimit="10"
|
||||
rx="16.432407"
|
||||
ry="16.112358"
|
||||
id="ellipse8660"
|
||||
style="fill:#f8f7cb;stroke:#808285;stroke-width:1.62162149;stroke-miterlimit:10" />
|
||||
<path
|
||||
d="m 373.57692,67.966639 c 0,0 -0.24551,0.106867 -0.68229,0.32115 a 48.77221,48.77221 0 0 0 -1.80165,0.936582 c -0.7371,0.401708 -1.55586,0.910001 -2.42914,1.472281 -0.87357,0.588862 -1.77452,1.231151 -2.64781,1.926874 a 38.521855,38.521855 0 0 0 -2.45682,2.141152 c -0.7371,0.722853 -1.4194,1.418576 -1.96524,2.03429 -0.54584,0.615437 -0.98261,1.150865 -1.28294,1.552296 -0.0274,0.05344 -0.0548,0.08029 -0.0819,0.106867 -0.0274,0.02683 -0.0274,0.05372 -0.0548,0.08056 l -0.0543,0.05344 -2.56588,-1.820007 c -0.21839,1.311437 -0.35484,2.649727 -0.30032,3.961159 0.0274,0.642295 0.10906,1.284856 0.21839,1.900298 0.13646,0.615709 0.30032,1.20457 0.54584,1.739993 a 8.524882,8.524882 0 0 1 1.17388,-1.231423 c 0.43651,-0.347997 0.87329,-0.669147 1.31007,-0.936859 0.92809,-0.53515 1.88358,-0.936581 2.8662,-1.284579 l -2.56588,-1.820012 c 0,0 0.0274,-0.02683 0.0274,-0.05344 0,-0.02683 0.0274,-0.02683 0.0545,-0.05372 0.0274,-0.02656 0.0548,-0.08029 0.0819,-0.106867 0.27291,-0.37485 0.70969,-0.88342 1.25553,-1.498862 0.54584,-0.589128 1.20101,-1.284856 1.93811,-1.980579 0.7371,-0.695995 1.55586,-1.418576 2.40201,-2.087995 0.84616,-0.668871 1.71972,-1.311161 2.56588,-1.873164 0.84616,-0.56228 1.66519,-1.043997 2.37489,-1.445428 0.7097,-0.401437 1.31006,-0.696001 1.74685,-0.909735 0.43678,-0.214278 0.68229,-0.321416 0.68229,-0.321416 z m 31.11797,1.606006 c 0,0 0.2184,0.13372 0.57324,0.320868 0.19127,0.107144 0.40938,0.241136 0.65518,0.374856 0.24579,0.160572 0.51871,0.347997 0.81903,0.53515 1.201,0.802862 2.70233,1.98058 4.06693,3.345722 1.36487,1.364871 2.53874,2.863733 3.33037,4.068303 0.21839,0.294292 0.35486,0.588856 0.51844,0.82972 0.16386,0.240858 0.30032,0.454864 0.38226,0.642289 0.0819,0.160573 0.13645,0.240859 0.13645,0.240859 l -2.75686,1.498862 a 23.512682,23.512682 0 0 1 5.4866,3.934306 c 0.60037,-2.274871 0.87328,-4.737168 0.79163,-7.333461 l -2.75714,1.498862 -0.13646,-0.267717 c -0.10906,-0.187425 -0.24551,-0.401431 -0.40938,-0.669142 -0.16386,-0.240858 -0.32744,-0.535151 -0.54584,-0.856572 -0.81903,-1.231146 -2.02004,-2.810294 -3.41203,-4.202018 -1.392,-1.418575 -2.94813,-2.649726 -4.20366,-3.479446 -0.30033,-0.214006 -0.60065,-0.401431 -0.84616,-0.561727 -0.2458,-0.160849 -0.49159,-0.294569 -0.6823,-0.401708 a 19.728534,19.728534 0 0 1 -0.60064,-0.347997 z"
|
||||
id="path8666"
|
||||
style="fill:#808285;stroke-width:0.2740148"
|
||||
inkscape:connector-curvature="0" />
|
||||
<text
|
||||
style="font-weight:400;font-size:11.23116016px;line-height:1.25;font-family:sans-serif;letter-spacing:0;word-spacing:0;fill:#7e7e7e;stroke-width:0.28074586"
|
||||
x="378.64966"
|
||||
y="142.92282"
|
||||
font-weight="400"
|
||||
font-size="20.6784px"
|
||||
letter-spacing="0"
|
||||
word-spacing="0"
|
||||
id="text8674">
|
||||
<tspan
|
||||
x="378.64966"
|
||||
y="142.92282"
|
||||
id="tspan8672"
|
||||
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.28074586">AND</tspan>
|
||||
</text>
|
||||
<text
|
||||
style="font-weight:400;font-size:11.88389969px;line-height:1.25;font-family:sans-serif;letter-spacing:0;word-spacing:0;fill:#7e7e7e;stroke-width:0.29714581"
|
||||
x="200.10918"
|
||||
y="143.83398"
|
||||
font-weight="400"
|
||||
font-size="21.8802px"
|
||||
letter-spacing="0"
|
||||
word-spacing="0"
|
||||
id="text8678">
|
||||
<tspan
|
||||
x="200.10918"
|
||||
y="143.83398"
|
||||
id="tspan8676"
|
||||
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.29714581">OR</tspan>
|
||||
</text>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 10 KiB |
@ -1,37 +1,42 @@
|
||||
Functors
|
||||
===
|
||||
|
||||
With this chapter, we will change the tactic a bit, (as I am sure you are a bit tired of jumping through different subjects). We will examine some purely categorical concepts, using the structures that we saw so far as context and we will also generalize some of the concepts that we saw in these structures so they are valid for all categories.
|
||||
With this chapter, we will change the tactic a bit, (as I am sure you are a bit tired of jumping through different subjects) and we will examine some purely categorical concepts, using the structures that we saw so far as context. We will also generalize some of the concepts that we saw in these structures so they are valid for all categories.
|
||||
|
||||
Connecting categories
|
||||
Categories we saw so far
|
||||
===
|
||||
|
||||
We already saw a lot of different types of categories:
|
||||
We already saw a many different types of categories, like categories that have just one *object* (monoids, groups) and categories that have only one *morphism* between any two objects (preorders, partial orders).
|
||||
|
||||
Categories that have just one object (monoids, groups)
|
||||
|
||||
|
||||
Categories that have only one morphism between any two objects (preorders, partial orders)
|
||||
We also defined a lot of categories, most notably the ones based on logics/programming languages, but also less serious categories, as for example the color-mixing one
|
||||
|
||||
Categories based on logic (here each collection of assertions forms its own category)
|
||||
|
||||
|
||||
And (somewhat related) programming language categories.
|
||||
We saw that we can make a category out of everything, as for example our city's road system, or a soccer ranglist starring me and my grandmother.
|
||||
|
||||
We saw the category of sets and related to it - various categories that are subcategories of the category of sets, as for example the set inclusion orders, which only consists of sets of a given number of elements.
|
||||
While examining all of this, we also saw the mother of all categories - the category of sets, as well as various *subcategories* to that category, as for example the set inclusion orders. We saw that many other categories are similar to subcategories of the category of sets.
|
||||
|
||||
|
||||
|
||||
But how can we utilize the insights that we get from the fact that so many different things are actually one and the same thing in disquise? To do so we must specify ways to connect categories to one another. This is the topic of this chapter.
|
||||
|
||||
Categorical Isomorphisms
|
||||
===
|
||||
|
||||
In chapter 1 we talked about set isomorphisms, which establish the equivalence between two sets.
|
||||
In chapter 1 we talked about set isomorphisms, which establish the equivalence between two sets. If you remember a set isomorphism consisted of two functions between the sets that when composed are equivalent to the identity function. Or more simply put, of one invertible function.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Then in chapter 4 we mentioned order isomorphisms, which were just set isomorphisms, with the extra condition that not only the objects, but the arrows should be the same, so for any two elements **a** and **b**, *a ≤ b** iff **F(a) ≤ F(b)**.
|
||||
|
||||
|
||||
|
||||
It's a little (but not a lot) more complex to define extend this definition to work for categories as well. Given two categories, an isomorphism between them is an isomorphism between the underlying sets of objects, plus an isomorphism between the morphisms that connect them.
|
||||
It's a little (but not a lot) more complex to extend this definition to work for categories as well. Given two categories, an isomorphism between them is an invertible function between the underlying sets of objects, plus an isomorphism between the morphisms that connect them.
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user