(My answer is only about how non-termination relates to inconsistency.)
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.
