Topic RS: Completeness and Soundness

2 Why the rules are good, part 2

In Topic RS02, 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 exercise in Topic 1.2.3,
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) models ~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?


2.1 Is the system strong enough?

Exercise 2.1a

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

The formula in exercise 2.1a 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.

Exercise 2.1b

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

Exercise 2.1c

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


2.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 models φ then proves φ.

and

For any formula φ, and list of formulas X,
if X models φ then X proves φ.

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.

2.3 Are all the rules necessary?

Exercise 2.3a

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.

Exercise 2.3b

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?


2.4 Two methods

One way 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 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.


2.5 Within and about the system

In Topic RS01 and Topic RS02 you have learned that our system
of sentential logic is both sound and complete.
In these Topics, 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.