
Introduction to Logic

Tools for Thought

Structured proofs are similar to linear proofs in that they are sequences of reasoning steps. However, they differ from linear proofs in that they have more structure. In particular, sentences can be grouped into subproofs nested within outer superproofs.
As an example, consider the structured proof shown below. It resembles a linear proof except that we have grouped the sentences on lines 3 through 5 into a subproof within our overall proof.
1.  p ⇒ q   Premise 
2.  q ⇒ r   Premise 
3.    Assumption 
4.    Implication Elimination: 3, 1 
5.    Implication Elimination: 4, 2 
6.  p ⇒ r   Implication Introduction: 3, 5 

The main benefit of structured proofs is that they allow us to prove things that cannot be proved using only ordinary rules of inference. In structured proofs, we can make assumptions within subproofs; we can prove conclusions from those assumptions; and, from those derivations, we can derive implications outside of those subproofs, with our assumptions as antecedents and our conclusions as consequents.

Our sample structured proof illustrates this. On line 3, we begin a subproof with the assumption that p is true. Note that p is not a premise in the overall problem. In a subproof, we can make whatever assumptions that we like. From p, we derive q using the premise on line 1; and, from that q, we prove r using the premise on line 2. That terminates the subproof. Finally, from this subproof, we derive (p ⇒ r) in the outer proof. Given p, we can prove r; and so we know (p ⇒ r). The rule used in this case is called Implication Introduction, or II for short.
1.  p ⇒ q   Premise 
2.  q ⇒ r   Premise 
3.    Assumption 
4.    Implication Elimination: 3, 1 
5.    Implication Elimination: 4, 2 
6.  p ⇒ r   Implication Introduction: 3, 5 

As this example illustrates, there are three basic operations involved in creating useful subproofs  (1) making assumptions, (2) using ordinary rules of inference to derive conclusions, and (3) using structured rules of inference to derive conclusions outside of subproofs. Let's look at each of these operations in turn.

In a structured proof, it is permissible to make an arbitrary assumption in any subproof. The assumptions need not be members of the initial premise set. Note that such assumptions cannot be used directly outside of the subproof, only as conditions in derived implications, so they do not contaminate the superproof or any unrelated subproofs.
For example, in our sample proof, we used this assumption operation in the nested subproof even though p was not among the given premises.
1.  p ⇒ q   Premise 
2.  q ⇒ r   Premise 
3.    Assumption 
4.    Implication Elimination: 3, 1 
5.    Implication Elimination: 4, 2 
6.  p ⇒ r   Implication Introduction: 3, 5 

An ordinary rule of inference applies to a particular subproof of a structured proof if and only if there is an instance of the rule in which all of the premises occur earlier in the subproof or in some superproof of the subproof. Importantly, it is not permissible to use sentences in subproofs of that subproof or in other subproofs of its superproofs.
For example, in the structured proof we have been looking at, it is okay to apply Implication Elimination to 1 and 3. And it is okay to use Implication Elimination on lines 2 and 4.
1.  p ⇒ q   Premise 
2.  q ⇒ r   Premise 
3.    Assumption 
4.    Implication Elimination: 3, 1 
5.    Implication Elimination: 4, 2 
6.  p ⇒ r   Implication Introduction: 3, 5 

However, it is not acceptable to use a sentence from a subproof in applying an ordinary rule of inference in a superproof.
The last line of the malformed proof shown below gives an example of this. It is not permissible to use Implication Elimination as shown here because it uses a conclusion from a subproof as a premise in an application of an ordinary rule of inference in its superproof.
 1.  p ⇒ q   Premise 
 2.  q ⇒ r   Premise 
 3.    Assumption 
 4.    Implication Elimination: 1, 3 
 5.    Implication Elmination: 2, 4 
 6.  p ⇒ r   Implication Introduction: 3, 5 
Wrong!  7.  r   Implication Elimination: 2, 4  Wrong! 

The malformed proof shown below is another example. Here, line 8 is illegal because line 4 is not in the current subproof or a superproof of this subproof.
 1.  p ⇒ q   Premise 
 2.  q ⇒ r   Premise 
 3.    Assumption 
 4.    Implication Elmination: 1, 3 
 5.    Implication Elmination: 2, 4 
 6.  p ⇒ r   Implication Introduction: 3, 5 
 7.    Assumption 
Wrong!  8.    Implication Elmination: 2, 4  Wrong! 
 9.  ¬r ⇒ r   Implication Introduction: 7, 8 

Correctly utilizing results derived in subproofs is the responsibility of a new type of rule of inference. Like an ordinary rule of inference, a structured rule of inference is a pattern of reasoning consisting of one or more premises and one or more conclusions. As before, the premises and conclusions can be schemas. However, the premises can also include conditions of the form φ  ψ, as in the following example. The rule in this case is called Implication Introduction, because it allows us to introduce new implications.
Once again, looking at the correct example above, we see that there is an instance of Implication Introduction (shown here on the left) in deriving line 6 from the subproof on lines 3  5. The application of Implication Introduction in the malformed proof is also okay in deriving line 7 from the subproof in lines 4  6.

Finally, we define a structured proof of a conclusion from a set of premises to be a sequence of (possibly nested) sentences terminating in an occurrence of the conclusion at the top level of the proof. Each step in the proof must be either (1) a premise (at the top level) or an assumption (other than at the top level) or (2) the result of applying an ordinary or structured rule of inference to earlier items in the sequence (subject to the constraints given above).

Use the arrow keys to navigate.
