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?

Show that "(A → (A ∨ B))" is a tautology in two different ways.

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.

Show that "((A ∨ ~B) → ~(~A & B))" is a tautology in two different ways.

Suppose we remove Rules →I, ~I and ~E from the system. Is it still possible to derive "((A ∨ ~B) → ~(~A & B))"?

answer## §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?

Suppose we get rid of some of the rules. For example, suppose we remove rules ↔I and ↔E. Would the system still be complete?

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.

Suppose we add the following new rule to our system:

**Flip rule**

If you have derived φ, you can write down ~φ, depending on everything φ depends on.

Would the revised system still be complete?

## §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.