We can think of Type Theory as being a catalog of a variety of notions of computation. The type structure determines the “programming language features”. For example, whether you have higher order functions amounts to saying “do you have exponential types”; whether you have structs or tuples amounts to saying “do you have Cartesian product types”; whether you have choices or multiple classes of data corresponds to “whether you have sum types”. A programming language is really just a collection of types. So type theory is just a theory of construction. From that point of view, logic is just an application of type theory, because there are particular constructions which correspond to proofs. Other constructions like natural numbers or geometric objects don’t correspond to proofs of particular propositions. They are just mathematical constructions. What type theory is intersted in is the general concept of what is a mathematical construction. That’s why intuitionistic logic is also called constructive logic. From this point of view, we can say that logic is just a corner of mathematics, and mathematics is just a corner of computer science ;)

Intuitionistic Logic/Constructive Logic

“Logic as if people matters”. We are talking about communication of knowledge. We treat proofs as mathematical objects, or programs. We claim that $A$ is true, we actually mean that we have a proof of $A$. $M:A$ means that $M$ is a proof of $A$, or $M$ is of type $A$, they are the same thing. There are many strong connections among proof theory, type theory, and category theory.

Some connections between Intuitionisitc Propositional logic:proof theory ($\vdash$) and Heyting Algebra:category theory(Cartesian closed pre-order, which follows Reflexivity and Transitivity) ($\leq$)

Sythetic Judgement vs Analytic Judgement

For synthetic judgement, we have something like “$A$ is true”, which requires a proof. It means that we need to do some proof searching.

For analytic judgement, we have “$M:A$”, which gives me a proof of $A$ which is $M$. All we need to do is to check whether $M$ is actually a proof of $A$, which is much easier than searching a proof. It is also called self-evident.

Equivalence of Proofs

1. Definitional Equality (analytic judgement): equality of sense \(\Gamma\vdash M\equiv N:A\)

2. Denotational Equality (synthetic judgement): equality of reference \(\Gamma\vdash M=N:A\)

3. (Homotopy) Equivalence (synthetic judgement) \(\Gamma\vdash\alpha:M\cong N:A\), where $\alpha$ is an evidence of equivalence.

Example to distinguish 1 and 2:

Define addition as follows:

Then we have the following equalities:

For Denotational Equality, we are suppressing the trivial evidence which is always reflexivity/identity. But for Equivalence, $\alpha$ can be reflexivity but can also be something else.

Negation (\(\urcorner\)) in Heyting Algebra

Introduction rule:

Elimination rule:

Note: negation in Heyting algebra is not complement!!!

Namely, we don’t have the following:

or in logic, we don’t expect

Boolean Algebra is Heyting Algebra with negation equals complement, which is also called law of excluded middle.

We can define in Heyting Algebra:

It just means that there are propositions that we neither have a proof nor refutation. Example: $P=NP$.

Note: Failing to affirm the decidability of every proposition is not the same as refuting the decidability of every proposition.

We have the following theorm in intuitionistic logic:

To put it in human language, it says: intuitionistic logic does not refute the law of excluded middle. It does not affirm it, but it does not refute it also.

The importance is: we can always heuristically assume a proposition is decidable even if we don’t have a proof. The apparent limitations of intuitionistic logic are the very source of its strength/expressiveness.

So far we have some elementry constructions:

or to write it in logic