Next: Constructive Logic
Up: Statements and Definitions
Previous: Propositions as Types
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