

Introduction to Logic

Tools for Thought


By writing down premises, writing instances of axiom schemas, and applying rules of inference, it is possible to derive conclusions that cannot be derived in a single step. This idea of stringing things together in this way leads to the notion of a linear proof.
A direct proof of a conclusion from a set of premises is a sequence of sentences terminating in the conclusion in which each item is either (1) a premise, (2) an instance of an axiom schema, or (3) the result of applying a rule of inference to earlier items in sequence.

Here is an example. Suppose we have the set of sentences we saw earlier. We start our proof by writing out our premises. We believe p; we believe (p ⇒ q); and we believe that (p ⇒ q) ⇒ (q ⇒ r). Using Implication Elimination on the first premise and the second premise, we derive q. Applying Implication Elimination to the second premise and the third premise, we derive (q ⇒ r). Finally, we use the derived premises on lines 4 and 5 to arrive at our desired conclusion.
1.  p  Premise 
2.  p ⇒ q  Premise 
3.  (p ⇒ q) ⇒ (q ⇒ r)  Premise 
4.  q  Implication Elimination: 2, 1 
5.  q ⇒ r  Implication Elimination: 3, 2 
6.  r  Implication Elimination: 5, 4 

Here is another example. Whenever p is true, q is true. Whenever q is true, r is true. With these as premises, we can prove that, whenever p is true, r is true. On line 3, we use Implication Creation to derive (p ⇒ (q ⇒ r)). On line 4, we use Implication Distribution to distribute the implication in line 3. Finally, on line 5, we use Implication Elimination to produce the desired result.
1.  p ⇒ q  Premise 
2.  q ⇒ r  Premise 
3.  p ⇒ (q ⇒ r)  Implication Creation: 2 
4.  (p ⇒ q) ⇒ (p ⇒ r)  Implication Distribution: 3 
5.  p ⇒ r  Implication Elimination: 4, 1 

Let R be a set of rules of inference. If there exists a proof of a sentence φ from a set Δ of premises using the rules of inference in R, we say that φ is provable from Δ using R. We usually write this as Δ _{R} φ, using the provability operator  (which is sometimes called single turnstile). If the set of rules is clear from context, we usually drop the subscript, writing just Δ  φ.

Use the arrow keys to navigate.
Press the escape key to toggle all / one.

