In this section we shall show how one can use the type theory described above to define various logics. The general pattern of presentation will be as follows:

- A series of definitions is
introduced so that one can work directly with
familiar logical notation instead of the underlying type--theoretic notation.
- Theorems are stated using the defined notation.

Thu Sep 14 08:45:18 EDT 1995