As usual the soundness lemma is proved by induction on the way a deduction is built up using the rules of inference.
For example if we have a deduction of B from zero, one or more of A1,...,An,A, then we can use one of the rules of inference to get a deduction of (A->B) from zero, one or more of A1,...,An, discharging the assumption A. By the induction hypothesis we have that there is a method for getting a proof of [[B]] from proofs of [[A1]],...,[[An]],[[A]]. The hypothesis can be reformulated to say that we can get a method for getting a proof of [[B]] from any proof of [[A]], from proofs of [[A1]],...,[[An]]; i.e. we can get a proof of [[A->B]] from proofs of [[A1]],...,[[An]]. This takes care of the induction step for this particular rule of inference.
The other rules of inference of intuitionistic logic can be taken care of in a similar way. But the classical argument-by-contradiction inference step cannot be justified in this way unless one makes some very non-constructive assumptions about proofs such as that for any proposition A there is a proof of (Av-A).
They are the evidence for the truth of the proposition. We now want to take the view that proofs are mathematical objects, like numbers etc, and moreover that the proofs of a proposition form a type. We shall go even further and make the simplifying assumption that a proposition is the type of its proofs.
It is natural to make yet one further assumption. Given any type, A, we can form the proposition `there is an object of type A'. What should a proof of this proposition be? We answer that any object of type A provides the evidence for the truth of the proposition and so will be treated as a proof of the proposition.
Summarising we have been led to identify the notion of a proposition in constructive mathematics with the notion of type, the proofs of a proposition being identified with the objects of the type.
This turns out to be a very elegent and natural identification, which should be compared with the classical identification of propositions with truth values. In order to make this work we need to understand the logical operations as operations on types.
Next, given types A,B we explain the types (A->B), (AxB) and (A+B). These are the function type (A->B), the binary cartesian product type (AxB) and the binary disjoint union type (A+B).
Clearly we have in mind to identify the propositions (A->B), (A&B), (AvB) with the types we have just described.
We now now assume given a type D and a predicate P(x) on D; so that P(a) is a proposition (i.e. a type) for each object a of type D. So P is just a family of types indexed by the type D. We want to explain the types (Pi x:D)P(x) and (Sigma x:D)P(x). These are the indexed cartesian product type (Pi x:D)P(x) and the indexed disjoint union type (Sigma x:D)P(x).
Of course we have in mind to identify the quantified propositions (forall x:D)P(x) and (exist x:D)P(x) with these types.
Note: (A->B) and (AxB) are the special cases of (Pi x:D)P(x) and (Sigma x:D)P(x) when D is A and P(a) is constantly B for each object a of type A. Further (A+B) is the special case of (Sigma x:D)P(x) when D is the two element type 2 and P(t) is A, P(f) is B.
So far we have given a very informal treatment of some of the key ideas of Martin-Lof's approach to type theory. A rigorous approach would need to spend more time on the philosophical and computational aspects of the subject. Here we will have to stay at this very informal level. So far we have described the following primitive forms of type.
In order to have a framework for constructive mathematics, and in particular constructive set theory, we need a few more forms of type. In fact it will suffice for most elementary purposes to have just two more primitive forms of type. We will need inductive types (Wx:A)B(x) of well-founded trees and we will need a type universe U of small types.
In type theory we express that Nat is to be inductively generated following these introduction rules by having a rule for defining function on Nat by primitive recursion.
Then there is a unique function f:(Pi x:Nat)B(x) such that
f(0)=b0:B(0) and f(S(n))=h(n)(f(n)):B(S(n)) for each n:Nat.
Note the use of equality on the type B(0) and also on the types B(S(n)). It was part of the typing principle that each type has a notion of equality for the objects of that type.
Observe that, when we think of B(x) as a predicate on Nat, definition by primitive recursion is giving us proof by mathematical induction; i.e. from B(0) and (forall n:Nat)[B(x)->B(S(x))] we can infer (forall x:Nat)B(x)
See Lecture 8
Draft. Last Revised: 22nd May, 1998.