Proof Systems

A proof system is a finite set of axiom schemata and rules of inference. Although it is interesting to consider proof systems with non-valid axiom schemata or unsound rules of inference, in this book we concentrate exclusively on proof systems with valid axiom schemata and sound rules of inference.

The Hilbert System is a well-known proof system for Propositional Logic. It has one rule of inference, viz. Implication Elimination.

In addition, the Hilbert systems has three axiom schemas. See below. These are the axiomatic versions of rules of inference we saw earlier. In the Hilbert system, each rule takes the form of an implication. The premises of each rule are written as antecedents of an implication and the rule's conclusion is written as the consequent of the implication.

As an example of the Hilbert system in action, consider the proof shown below. Our premises are (p ⇒ q) and (q ⇒ r), and our goal is to prove (p ⇒ r). We start our proof by writing out our premises. We write down an instance of our Implication Creation schema and then use Implication Elimination to conclude (p ⇒ (q ⇒ r)). We then write down an instance of our Implication Distribution Schema to conclude ((p ⇒ q) ⇒ (p ⇒ r)). Finally, we use Implication Elimination to produce the desired conclusion.

The Hilbert System is interesting in that is sufficient to prove all logical consequences from any set of premises expressed using only ¬ and ⇒. And, as we shall see later, this subset of sentences is interesting because, for every sentence in Propositional Logic, there is a logically equivalent sentence written in terms of just these two operators. Moreover, there is an inexpensive algorithm for converting every Propositional Logic sentence to its equivalent sentence in this form.