[SL17] Completeness

In the last tutorial, you learned one reason why the rules of our natural deduction system are good: the system is sound. But this is not all we want to know about our system. We also want to know whether or not the rules are strong enough to show everything we need to show. In one of the previous exercises, you derived the tautology "(A → A)". But is the system strong enough to let you derive any tautology?

For example, is the system strong enough to let you derive "(A → (A ∨ B))" or "(~A ∨ A)"? What about a valid sequent like "A, (B → ~A) ⊨ ~B"? WIll the system permit you to derive the conclusion "~B" from the premises "A" and "(B → ~A)"? WIll the system permit you to derive the conclusion of any valid sequent from its premises?

§1. Is the system strong enough?

Every row in the truth table for "(A → (A ∨ B))" is "T": 

A B	(A → (A ∨ B)) 
T T 	   T 
T F 	   T 
F T 	   T 
F F 	   T 

So "(A → (A ∨ B))" is a tautology. 

"(A → (A ∨ B))" is derivable in our system with no dependencies: 

1	1. A 			A 
1	2. (A ∨ B) 		1 ∨I 
	3. (A → (A ∨ B)) 	1,2 →I 

Since our system is sound, any formula derivable with no dependencies is a tautology. 
So "(A → (A ∨ B))" is a tautology. 

This formula is not very difficult to derive in our natural deduction system. But, as you have seen, sometimes it is not easy to make a certain derivation. Sometimes, you get stuck, and you are not certain how to reach your goal.

Suppose you are trying to derive "((A ∨ ~B) → ~(~A & B))". This is a tautology. So we would like to be able to derive this formula using our rules.

But suppose you start making the derivation, and you get stuck. What should you think then? Perhaps there is a derivation of this formula, but you have not tried hard enough to find it. Maybe if you work harder you will eventually find a derivation. But, on the other hand, maybe there is no derivation of this formula in our system. Perhaps the system is not strong enough to derive this formula. Perhaps the system has the wrong rules, or not enough rules.

Every row in the truth table for 
"((A ∨ ~B) → ~(~A & B))" is "T": 

A B 	((A∨~B)	→ ~(~A & B)) 
T T 		T 
T F 		T 
F T 		T 
F F 		T 

So "((A ∨ ~B) → ~(~A & B))" is a tautology. 

"((A ∨ ~B) → ~(~A & B))" is derivable in our system with no dependencies: 

1 	1. (A ∨ ~B) 			A 
2 	2. (~A & B) 			A 
2 	3. ~A 				2 &E 
1,2 	4. ~B 				1,3 ∨E 
2 	5. B 				2 &E 
1,2 	6. (B&~B) 			4,5 &I 
1 	7. ~(~A & B) 			2,6 ~I 
	8. ((A ∨ ~B) → ~(~A & B))	1,7 →I 

Since our system is sound, any formula derivable 
with no dependencies is a tautology. 
So "(A → (A ∨ B))" is a tautology. 

§2. The system is complete

Our system is strong enough to derive every tautology. Indeed, our system is strong enough to derive the conclusion of every valid sequent from its premises. In a word, the system is complete. Being complete is a good thing, because it means that we are not missing any rules. Our rules are strong enough.

Here is completeness defined, in symbols:

For any formula φ, if ⊨ φ then ⊢ φ.

and

For any formula φ, and list of formulas X, if X ⊨ φ then X ⊢ φ.

It is possible to prove that our system is complete by careful reasoning. But that is a job for a more advanced course. For now, the main thing is to understand what completeness is.

§3. Are all the rules necessary?

If we remove rules ↔I and ↔E the system will no longer be complete. There are formulas which we can no longer derive. For example, we can no longer derive "(A↔A)".

Thus, if we revise our system by removing some rules, then the system might no longer be complete. The revised system is not complete if there is some formula which was derivable in the original system, but not derivable in the revised system.

§4. Two methods

One way to show that a sequent is valid is to make a truth table. You learned how in a previous topic. If there is no line in the truth table where all the premises are T and the conclusion is F then the sequent is valid.

Another way to show that a sequent is valid is to make a derivation in our natural deduction system. If you can derive the conclusion of the sequent from its premises then that sequent is valid.

One way to show that a sequent is not valid is to make a truth table. If there is a line in the truth table where all the premises are T and the conclusion is F then the sequent is not valid.

Is there another way to show that a sequent is not valid? Our natural deduction system does not provide a method that can always show that an invalid sequent is invalid. If the sequent is invalid there is no derivation of the conclusion from the premises in our system. (If there were a derivation then our system would not be sound.) Following the rules of our system does not tell us that there is no derivation. Trying to make a derivation and failing is not a method to show that there is no derivation. (Maybe you haven't tried hard enough!)

So in one important respect the truth table method is more powerful than our natural deduction system for sentential logic. The truth table method can always determine whether or not a sequent is valid. However, our natural deduction system does not provide a method to determine in every case whether or not a sequent is valid.

§5. Within and about the system

In this tutorial and the previous one, you have learned that our system of sentential logic is both sound and complete. Instead of working within the system, you have studied about the system. This sort of study is called metalogic or metatheory, and is an important part of the study of logic. For any tool, one should learn not only how to use the tool, but one should learn about the tool -- what the tool can and cannot do.