.. title: Logic in Type Theory I: Concepts
.. slug: logic-in-type-theory-i-concepts
.. date: 2020-07-14
.. tags: 
.. category: 
.. link: 
.. description: Intionistic logic
.. type: text
.. has_math: true

Intuistionistic logic and constructivism
########################################

The key insight of the Curry-Howard correspondence or the concept of
'propositions as types' is that there is a direct correspondence between logic
and its operators and `type theory
<https://github-blog.jad-issa.com/2019/08/23/a-primer-on-type-theory/>`_ and its
operators.

This may at first seem strange and quite exotic (and it kind of is), but that's
only because when one thinks of 'logic', it is most common -- by far -- to think
of classical logic whereby every proposition (a statement which can be argued to
be true or false) is assigned a truth value which mathematicians attempt to
discover. A rather different logic is actually necessary to understand the
Curry-Howard correspondence, namely: intuistionistic logic.

Intuitionism is the philosophical approach (in the philosophy of mathematics)
whereby mathematical objects, including theorems and proofs are seen as human
constructions instead of human discoveries. In other words, a `group
<https://en.wikipedia.org/wiki/Group_(mathematics)>`_ for instance is a lot more
like a machine made up of pieces put together than `Newton's second law of
motion <https://en.wikipedia.org/wiki/Newton%27s_second_law>`_ discovered based
on empirical evidence of such law being respected in the Universe (there is
obviously a lot more to be said about mathematics, technology, and physics, but
for a layman in philosophy, this should get the point across).

.. TEASER_END

In intuitionistic logic, propositions are not assigned truth values which are
left to be 'discovered' by the mathematician, instead, propositions are said to
have a proof or not have one (yet?). Roughly speaking, if a proposition has a
proof, then it's true, and if it **cannot** have one, then it's false. However, it's
unhealthy to think of intuistionistic logic as such because the ultimate goal of
it is not to determine a truth value for a proposition, but instead to merely
construct a proof of it.

A 'trivial' tautology has only one possible proof: that it just is a tautology,
while a contradiction cannot have any proof at all. A slightly more elaborate
proposition might have more than one proof. For example, proving an implication
can be done by at least two ways: assuming the premise and deriving the
conclusion, or composing other implications in a series; in general, this may
lead us to 2 distinct proofs. This already gives more 'structure' to
intuistionistic logic than is possible with classical logic, but more
importantly, it allows for the expression of proofs as objects to be compiled
and constructed.

The Curry-Howard correspondence
###############################

The Curry-Howard correspondence is a reformulation of intuistionistic logic
within type theory. In essence, a proposition is to be read as a type, and a
proof is to be read as an object of that type. Just as we can construct the type
of natural numbers (below), we can construct proofs of a proposition.

.. code::

    Nat = Zero | (Succ Nat)

When a proposition has a proof, we say that the type is *inhabited* (there is at
least one element of that type). Conversely, when no proof exists for a
proposition, we say that the type is *uninhabited*.

Below is a table with some basic correspondences

.. table:: Basic correspondences of the Curry-Howard correspondence.

    +-------------------------------+------------------------------------------------------+
    | Logic                         | Type Theory                                          |
    +===============================+======================================================+
    | Proposition                   | Type                                                 |
    +-------------------------------+------------------------------------------------------+
    | Proof                         | Element (of a type)                                  |
    +-------------------------------+------------------------------------------------------+
    | Tautology                     | Type 1, where * : 1 is the only element              |
    +-------------------------------+------------------------------------------------------+
    | Contradiction                 | Type 0 with no way to form elements                  |
    +-------------------------------+------------------------------------------------------+
    | Deriving from premise A       | Elimination rule A → _                               |
    +-------------------------------+------------------------------------------------------+
    | Concluding premise A          | Introduction rule _ → A                              |
    +-------------------------------+------------------------------------------------------+


Most texts on the subject never discuss much philosophy behind this or why it
makes sense, so let's try to see why that is something you might like to invest
yourself into.

Principally, one should realize that intuistionistic logic in type theory does
not have propositions as its basic objects, but rather proofs. A proof is to be
of a proposition, instead of a proposition having a proof. This also reflects a
major conceptual distinction between type theory and set theory, an element
**is** simply of a type, while a set merely **contains** elements with no type.
Working with intuistionistic logic in type theory is about computing, combining,
transforming proofs, not propositions.

From this perspective, a correct grouping of proof that makes sense is to
consider proofs having the type of the proposition that they prove: if you can
make a proof of ``B`` from some proof of ``A``, you better be able to make one
for any proof of ``A`` because if you're concluding ``B`` from ``A``, then any
proof of ``A`` should suffice. In general, anything that you can do with some
proof of ``A`` must be doable with all proofs of ``A``; therefore, it is best to
say that your operations work on the type of proofs of ``A``. Once you realize
that, you realize also that the type of proofs of ``A`` corresponds directly to
the proposition ``A`` itself, and you land on the Curry-Howard correspondence.

Operators on types
==================

.. table:: Basic operators on types and their corresponding logical operators.

    +---------------+---------+------------------------------------------------------+
    | Proposition   | Type    | English explanation (introduction/elimination)       |
    +===============+=========+======================================================+
    | False         | 0       | There is no way to construct an element of type 0.   |
    +---------------+---------+------------------------------------------------------+
    | True          | 1       | \* : 1 is the only element (trivial proof) of 1.     |
    +---------------+---------+------------------------------------------------------+
    | A or B        | A + B   | Given a proof a of A, (Left a) is a proof of A + B.  |
    |               |         | Given a proof b of B, (Right b) is a proof of A + B. |
    |               |         | No other proofs of A + B exist, so A + B corresponds |
    |               |         | to A or B.                                           |
    +---------------+---------+------------------------------------------------------+
    | A and B       | A × B   | If you have a proof p of A × B, (π1 p) is a proof of |
    |               |         | A.                                                   |
    |               |         | With that same proof p, (π2 p) is a proof of B.      |
    |               |         | Every proof of A × B is a pair (a, b), a : A, b : B. |
    +---------------+---------+------------------------------------------------------+
    | A implies B   | A → B   | Given a proof a of A, and f : A → B, you can prove B |
    |               |         | with (f a).                                          |
    |               |         | Given a : A if b[a] is a term of B, then (λ a. b[a]) |
    |               |         | : A → B.                                             |
    +---------------+---------+------------------------------------------------------+
    | not A         | A → 0   | With a proof a : A, and a f : A → 0, (f a) is a      |
    |               |         | contradiction.                                       |
    |               |         | Given a proof of A, and a term n(a) : 0, you get     |
    |               |         | A → 0.                                               |
    +---------------+---------+------------------------------------------------------+


The actual useful correspondences (given in the table) are quite straightforward once the reasoning above is understood. These basic bits of symmetry between operators in logic and operators in type theory give us a glimpse of what it's like to work with proofs under the Curry-Howard correspondence.

In follow-up posts we will explore the tools and consequences of this correspondence.