A formal proof system for propositional logic

The natural deduction proof system is both sound and complete—every provable consequence is valid and every logical entailment is provable. We'll view compactness as an abstract form of completeness.

One of the remarkable developments in twentieth-century logic has been the rise of formal systems of reasoning, proof systems capable of proving logical validities, indeed, proving all and only the logical validities, and moreover doing so in a controlled framework using only very specific, limited modes of deductive inference. That we can design such proof systems underlines how well we understand the nature of our logic—our grasp is so complete that we can itemize modes of reasoning exactly sufficient to deduce every conceivable logical validity. Amazing!

In this installment, I shall present such a proof system for reasoning in propositional logic. This will be an easier case than first-order predicate logic, the more powerful and expressive logic that we shall see in later posts, and yet this easier case nevertheless engages with all the core proof-theoretic issues. So let us use it as a introduction to formal deduction.

There are a variety of formal proof systems to choose from, with different styles and modes of reasoning, and some logicians express preferences amongst them, sometimes quite strongly. Ultimately, however, all the various proof systems of classical propositional logic are equivalent to one another in that they prove exactly the same theorems—the logical validities. In that sense, perhaps there can be no truly fundamental reason to prefer one system to another, if such a reason would be grounded in the capacity of the system to prove validities accurately.

I shall present a proof system in what is known as the natural deduction style. In natural deduction, a formal proof or deduction is an arrangement of propositional assertions in the form of a tree, in which the reasoning process proceeds downward from premises in the tops of the tree to the final conclusion, the theorem that has been proved, at the base.

We shall use the following notation: