I haven’t read the later chapters on category theory, about which I’ll only remember the following sentence:
“[…] one distinguishes small categories, those for which the classes of objects and of arrows are sets, from large categories, which are all the others. Beyond merely the language of categories, common to both small and large categories, it’s in reality the dialectic articulation between small and large categories which does constitute the heart of category theory.“
I was more interested by the beginning of the book, which I’ll summarize for myself as follows.
Tertium Non Datur (TND): for any proposition we have either or . Classical logic accepts TND while (sub-)intuitionistic logic does not as it views TND as a non-construtive principle.
For instance, in intuitionistic logic it is not assumed that when considering two elements and of an arbitrary set we have either or . This is done to allow for the possibility that checking either of these statements could be impossible (think real numbers, an infinity of decimals to examine). On the other hand, when restricted to the integers the alternative either or is assumed to be valid in intuitionistic logic just like in the classical one.
Reductio by Absurdum (RA): for any proposition we have .
Theorem: TND RA
Fake examples of RA which actually use only the very definition of (namely that a contradiction): proof of irrationality of ; Euclid’s proof of the infinity of primes ; proof that is not countable starting from a bijection of on .
Reasoning by Contraposition (RC): if then .
Theorem: RA RC
Morgan Laws (ML): and . In intuitionistic logic the second one is not an equivalence, we only have that the lhs implies the rhs. As a result, definitions which are equivalent in classical logic can cease to be so in intuitionistic logic (i.e. it is a richer logic with more concepts).
A set is said to be inhabited if it contains at least one element. We have that if is inhabited then . But the reverse statement that if is non-empty then it contains at least one element is only true assuming TND (i.e. only valid in classical logic). Stated differently, TND allows one to choose an element in a given non-empty set, while such a choice is not possible in intuitionistic logic.
This kind of choice is not to be confused with the Axiom of Choice (AC): on any set of inhabited sets there exists a choice function, i.e. an which to an element of associates an element in .
Theorem: AC TND
So AC is not compatible with intuitionism. On the other hand the Countable Axiom of Choice (CAC) (i.e. when is countable) is something much weaker which does not imply TND, and thus is compatible with intuitionistic logic.
Something which also holds in intuitionism is the weak Cantor theorem: for any set , the set of subsets of is not equipotent to .
On the other hand there is a new type of set which does not occur in classica logic and is neither finite nor infinite. Define .
A set is finite if for a certain integer there exists a bijection . A set is of finite type if for a certain integer there exists a surjection .
Theorem: TND any set of finite type is finite
On the other hand in intuitionistic logic sets of finite type are not necessarily finite, but what is valid is
Theorem: a set of finite type is either inhabited or empty
To finish this summary, here’s a result which shows that dealing with countable sets is not necessarily constructive:
Theorem: [CAC and TND] a union of countable sets is a countable set
That’s it, obviously I’ve glossed over many topics treated in this book. I certainly like the idea that people have explored the possibility that one may need in some instances to reason within a framework which does not assume TND. Never been a so-called Platonist myself. I only feel classical logic and the idea of an actual infinity are (useful) idealizations to model things in many situations (e.g. a liquid as a continuum), but which are not adapted to all situations.