Intuitionistic logic

These days I’ve read (part of) a nice introductory book in french by Pierre Ageron on intuitionistic logic.

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 C of objects and F 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 P we have either P or \neg P. 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 x and y of an arbitrary set we have either x=y or x\neq y. 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 x=y or x\neq y is assumed to be valid in intuitionistic logic just like in the classical one.

Reductio by Absurdum (RA): for any proposition P we have \neg\neg P\Rightarrow P.

Theorem: TND \Leftrightarrow RA

Fake examples of RA which actually use only the very definition of \neg P (namely that P\Rightarrow a contradiction): proof of irrationality of \sqrt{2} ; Euclid’s proof of the infinity of primes ; proof that \mathbb{R} is not countable starting from a bijection of \mathbb{N} on \mathbb{R}.

Reasoning by Contraposition (RC): if \neg Q \Rightarrow \neg P then Q \Rightarrow P.

Theorem: RA \Leftrightarrow RC

Morgan Laws (ML): [\neg(P\ \text{or}\ Q) ] \Leftrightarrow [\neq P\ \text{and}\ \neg Q] and [\neg(P\ \text{and}\ Q) ] \Leftrightarrow [\neq P\ \text{or}\ \neg Q]. 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 X is said to be inhabited if it contains at least one element. We have that if X is inhabited then X\neq\emptyset. But the reverse statement that if X 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 M of inhabited sets there exists a choice function, i.e. an f which to an element X of M associates an element f(X)=x in X.

Theorem: AC \Rightarrow TND

So AC is not compatible with intuitionism. On the other hand the Countable Axiom of Choice (CAC) (i.e. when M 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 X, the set \mathcal{P}(X) of subsets of X is not equipotent to X.

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 \underbar{n}:=\{0,1,\dots ,n-1\}.

A set X is finite if for a certain integer n there exists a bijection \varphi : \underbar{n}\rightarrow X. A set X is of finite type if for a certain integer n there exists a surjection \psi : \underbar{n}\rightarrow X.

Theorem: TND \Leftrightarrow 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] \Rightarrow 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.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: