Defining Logics

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.

• Constructive Logic
• Classical Logic
• Other Logical Operators