Proof Theory for Quantificational Logic

In the last chapter we explored the semantics of QL. We now present the proof theory for QL. A proof in QL is just like a proof in PL. We construct derivations of conclusions from premises, or in the case of theorems, from no premises. We employ rules of inference, equivalence rules, and new rules to deal with the special nature of quantifiers.

As we found with the semantics, the proof theory of QL is a superset of the proof theory of PL. Our Rules of Inference and Rules of Equivalence all apply. We will add rules to deal with quantified propositions and their negations. We will have three kinds of rules:

• Quantifier Negation rules: These rules enable us to replace negations of quantified wffs with quantified wffs.

• Instantiation rules: These rules enable us to infer instantiations of quantified wffs from quantified wffs.

• Generalization rules: These rules enable us to infer existential and universal generalizations from instantiated wffs.

We turn to each of these rule sets.