Editing Natural deduction (section)

=== Substitution theorem ===
{{Unreferenced section|date=May 2024}}
: ''If'' Γ ⊢ π<sub>1</sub> : ''A'' ''and'' Γ, ''u'':''A'' ⊢ π<sub>2</sub> : ''B'', ''then'' Γ ⊢ [π<sub>1</sub>/''u''] π<sub>2</sub> : B.

So far the judgment "Γ ⊢ π : ''A''" has had a purely logical interpretation. In [[type theory]], the logical view is exchanged for a more computational view of objects. Propositions in the logical interpretation are now viewed as ''types'', and proofs as programs in the [[lambda calculus]]. Thus the interpretation of "π : ''A''" is "''the program'' π has type ''A''". The logical connectives are also given a different reading: conjunction is viewed as [[product type|product]] (×), implication as the function [[function type|arrow]] (→), etc. The differences are only cosmetic, however. Type theory has a natural deduction presentation in terms of formation, introduction and elimination rules; in fact, the reader can easily reconstruct what is known as ''simple type theory'' from the previous sections.

The difference between logic and type theory is primarily a shift of focus from the types (propositions) to the programs (proofs). Type theory is chiefly interested in the convertibility or reducibility of programs. For every type, there are canonical programs of that type which are irreducible; these are known as ''canonical forms'' or ''values''. If every program can be reduced to a canonical form, then the type theory is said to be ''[[normalization property (abstract rewriting)|normalising]]'' (or ''weakly normalising''). If the canonical form is unique, then the theory is said to be ''strongly normalising''. Normalisability is a rare feature of most non-trivial type theories, which is a big departure from the logical world. (Recall that almost every logical derivation has an equivalent normal derivation.) To sketch the reason: in type theories that admit recursive definitions, it is possible to write programs that never reduce to a value; such looping programs can generally be given any type. In particular, the looping program has type ⊥, although there is no logical proof of "⊥". For this reason, the ''propositions as types; proofs as programs'' paradigm only works in one direction, if at all: interpreting a type theory as a logic generally gives an inconsistent logic.