# On the logical and categorical interpretation of lambda calculi and type systems

There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories.

Some variants of Barendregt's pure type systems have the property of strong normalization, i.e. any term can be reduced to a normal form after a finite number of reduction steps, the other of them don't have this property, system U, for example.

My questions are:

1. In a pure untyped lambda calculus, the ability to construct terms like infinite loop term (\x -> x x) (\x -> x x) or the fixed-point combinator \f -> (\x -> f (x x)) (\x -> f (x x)) entail Curry's paradox (P: P -> Q) or, informally, "if this sentence is true, then Voldemort exists", which leads to the system being able to prove anything. In some pure type systems it's possible to construct such terms even if the system isn't self-referential (as mentioned above, system U is such an example). Does the inconsistency of the logical calculus always correspond to the nontermination of the type system and vice versa?

2. Wikipedia says that the inconsistency of the type system as a proof calculus follows from the impossibility of constructing an uninhabited (empty, or void) type in it. Does it have anything to do with nontermination? If so, how exactly does nontermination lead to the inhabitation of all types, is it not possible to define an empty type axiomatically?

3. It's possible to add some kind of recursion to the calculus of constructions in such a way that it remains strongly normalizing (in which case it's called the "calculus of inductive constructions", for example, it can define natural numbers as Nat: 0 | S Nat). How do these two kinds of recursions differ, if one of them does not make the proof-calculus inconsistent, unlike the other? (Maybe it's primitive and general recursion???)

• This question is too broad for Stack Exchange. Questions (1), (2), (3) are closely related (about how non-termination relates to inconsistency) so it just barely makes sense to keep them together. But you should ask (4) and (5) separately. Jan 20 at 14:29
• As a general rule of thumb, it's best to ask only one question per post. You can ask them separately. The site works best that way. Otherwise, we get to situations where someone has answered one of the questions but not the others, and the site treats the question as answered even though it hasn't fully been. Also, we prefer questions that can be answered in one or a few paragraphs, so that people don't have to write a really long answer to address everything raised in the question. I suggest you edit your post to ask one question, and post the others separately.
– D.W.
Jan 20 at 19:18

The general idea of the Curry-Howard correspondence is that a term having a type, corresponds to a proof for a theorem. A term is an instruction on how to build a proof. A non-terminating term (i.e. a term that does not have a value) does not actually allow constructing a proof of the theorem. If a type has non-terminating terms but no value, it does not correspond to a proven theorem.

A type containing only non-terminating terms corresponds to a theorem for which searching for a proof never actually finds a proof.

Does the inconsistency of the logical calculus always correspond to the nontermination of the type system and vice versa?

Not necessarily, but it usually is.

The only counter-examples I can think of without research are “silly”. For example:

• Suppose non-termination is only allowed for terms that have certain known non-empty types. In other words, somehow, the typing rules ensure that if a type has non-terminating terms, it also has terminating terms. (This “somehow” restricts the compositionality of typing a lot.) Then the existence of these non-terminating terms doesn't affects which theorems are provable, so it doesn't make the type system inconsistent.
• There are other ways to make a type system inconsistent. You can just take False as an axiom, or $$\forall P, P \wedge \neg P$$. But that makes the type system useless. (Useless for the purpose of doing logic — it might be perfectly fine for doing programming.)

inconsistency of the type system as a proof calculus follows from the impossibility of constructing an uninhabited (empty, or void) type in it. Does it have anything to do with nontermination?

I mostly answered that above at the beginning of my post. If a type only has nonterminating terms, it has no values, and thus the corresponding theorem is not guaranteed to have a proof. The set-theoretic denotation of a type is as the set of its values, thus “empty type” means a type with no values unless explicitly defined otherwise.

If so, how exactly does nontermination lead to the inhabitation of all types, is it not possible to define an empty type axiomatically?

If you can make a non-terminating function $$f$$ of type $$A \to B$$, and you can construct a term $$a$$ of type $$A$$, then $$f(a)$$ has the type $$B$$, so $$B$$ is inhabited. In particular, if there is a generic fixpoint combinator, you can build a non-terminating function of type $$A \to B$$ for all types $$A$$ and $$B$$, thus (assuming the existence of at least one term of one type) all types are inhabited.

It is possible to define an empty type. For example, in Coq, the False type is defined as

Inductive False : Prop :=  .


That is, False is a proposition (which is a kind of type in Coq) for which there are zero ways of constructing a term (except by adding extra axioms — and any axiom that allows constructing a value of type False would make the system inconsistent).

How do these two kinds of recursions differ, if one of them does not make the proof-calculus inconsistent, unlike the other? (Maybe it's primitive and general recursion???)

It's possible to have some recursion, but there has to be limits. The general idea is that a recursive call must be made to a smaller value. For example, a function defined recursively on the natural numbers is only allowed to call itself on smaller numbers. More generally, the usual mathematical tool is a well-order: a function that calls itself recursively (directly or indirectly) must only call itself on values that are smaller in some well-order. The well-ordering property guarantees that the recursive call will terminate. In the calculus of inductive constructions, the well-order on terms is based on needing fewer constructors to construct the value.