1Propositional calculus

II Logic and Set Theory


1.3 Syntactic implication
While semantic implication captures the idea of truthfulness, syntactic impli-
cation captures the idea of proofs. We want to say
S
syntactically implies
t
if
there we can prove t from S.
To prove propositions, we need two things. Firstly, we need axioms, which
are statements we can assume to be true in a proof. These are the basic building
blocks from which we will prove our theorems.
Other than axioms, we also need deduction rules. This allows as to make
deduce statements from other statements.
Our system of deduction composes of the following three axioms:
1. p ⇒ (q ⇒ p)
2. [p ⇒ (q ⇒ r)] ⇒ [(p ⇒ q) ⇒ (p ⇒ r)]
3. (¬¬p) ⇒ p
and the deduction rule of modus ponens: from p and p ⇒ q, we can deduce q.
At first sight, our axioms look a bit weird, especially the second one. We
will later see that how this particular choice of axioms allows us to prove certain
theorems more easily. This choice of axioms can also be motivated by combinatory
logic, but we shall not go into details of these.
Definition (Proof and syntactic entailment). For any
S ⊆ L
, a proof of
t
from
S
is a finite sequence
t
1
, t
2
, ···t
n
of propositions, with
t
n
=
t
, such that each
t
i
is one of the following:
(i) An axiom
(ii) A member of S
(iii) A proposition t
i
such that there exist j, k < i with t
j
being t
k
⇒ t
i
.
If there is a proof of
t
from
S
, we say that
S
proves or syntactically entails
t
,
written S ⊢ t.
If ∅ ⊢ t, we say t is a theorem and write ⊢ t.
In a proof of
t
from
S
,
t
is the conclusion and
S
is the set of hypothesis or
premises.
Example. {p ⇒ q, q ⇒ r} ⊢ p ⇒ r
We go for (p ⇒ q) ⇒ (p ⇒ r) via Axiom 2.
1. [p ⇒ (q ⇒ r)] ⇒ [(p ⇒ q) ⇒ (p ⇒ r)] Axiom 2
2. q ⇒ r Hypothesis
3. (q ⇒ r) ⇒ [p ⇒ (q ⇒ r)] Axiom 1
4. p ⇒ (q ⇒ r) MP on 2, 3
5. (p ⇒ q) ⇒ (p ⇒ r) MP on 1, 4
6. p ⇒ q Hypothesis
7. p ⇒ r MP on 5, 6
Example. ⊢ (p ⇒ p)
We go for [p ⇒ (p ⇒ p)] ⇒ (p ⇒ p).
1. [p ⇒ ((p ⇒ p) ⇒ p)] ⇒ [(p ⇒ (p ⇒ p)) ⇒ (p ⇒ p)] Axiom 2
2. p ⇒ ((p ⇒ p) ⇒ p) Axiom 1
3. [p ⇒ (p ⇒ p)] ⇒ (p ⇒ p) MP on 1, 2
4. p ⇒ (p ⇒ p) Axiom 1
5. p ⇒ p MP on 3, 4
This seems like a really tedious way to prove things. We now prove that the
deduction theorem, which allows as to find proofs much more easily.
Proposition (Deduction theorem). Let S ⊂ L and p, q ∈ L. Then we have
S ⊢ (p ⇒ q) ⇔ S ∪ {p} ⊢ q.
This says that ⊢ behaves like the connective ⇒ in the language.
Proof. (⇒) Given a proof of p ⇒ q from S, append the lines
– p Hypothesis
– q MP
to obtain a proof of q from S ∪{p}.
(
⇐
) Let
t
1
, t
2
, ··· , t
n
=
q
be a proof of
q
from
S ∪ {p}
. We’ll show that
S ⊢ p ⇒ t
i
for all i.
We consider different possibilities of t
i
:
– t
i
is an axiom: Write down
◦ t
i
⇒ (p ⇒ t
i
) Axiom 1
◦ t
i
Axiom
◦ p ⇒ t
i
MP
– t
i
∈ S: Write down
◦ t
i
⇒ (p ⇒ t
i
) Axiom 1
◦ t
i
Hypothesis
◦ p ⇒ t
i
MP
– t
i
= p: Write down our proof of p ⇒ p from our example above.
– t
i
is obtained by MP: we have some
j, k < i
such that
t
k
= (
t
j
⇒ t
i
). We
can assume that
S ⊢
(
p ⇒ t
j
) and
S ⊢
(
p ⇒ t
k
) by induction on
i
. Now
we can write down
◦ [p ⇒ (t
j
⇒ t
i
)] ⇒ [(p ⇒ t
j
) ⇒ (p ⇒ t
i
)] Axiom 2
◦ p ⇒ (t
j
⇒ t
i
) Known already
◦ (p ⇒ t
j
) ⇒ (p ⇒ t
i
) MP
◦ p ⇒ t
j
Known already
◦ p ⇒ t
i
MP
to get S ⊢ (p ⇒ t
i
).
This is the reason why we have this weird-looking Axiom 2 — it enables us to
easily prove the deduction theorem.
This theorem has a “converse”. Suppose we have a deduction system system
that admits modus ponens, and the deduction theorem holds for this system.
Then axioms (1) and (2) must hold in the system, since we can prove them using
the deduction theorem and modus ponens. However, we are not able to deduce
axiom (3) from just modus ponens and the deduction theorem.
Example. We want to show
{p ⇒ q, q ⇒ r} ⊢
(
p ⇒ r
). By the deduction
theorem, it is enough to show that
{p ⇒ q, q ⇒ r, p} ⊢ r
, which is trivial by
applying MP twice.
Now we have two notions:
|
= and
⊢
. How are they related? We want to
show that they are equal: if something is true, we can prove it; if we can prove
something, it must be true.
Aim. Show that S ⊢ t if and only if S |= t.
This is known as the completeness theorem, which is made up of two directions:
(i) Soundness: If S ⊢ t, then S |= t. “Our axioms aren’t absurd”
(ii)
Adequacy: If
S |
=
t
,
S ⊢ t
. “Our axioms are strong enough to be able to
deduce, from S, all semantic consequences of S.”
We first prove the easy bit:
Proposition (Soundness theorem). If S ⊢ t, then S |= t.
Proof.
Given valuation
v
with
v
(
s
) = 1 for all
s ∈ S
, we need to show that
v(t) = 1. We will show that every line t
i
in the proof has v(t
i
) = 1.
If
t
i
is an axiom, then
v
(
t
i
) = 1 since axioms are tautologies. If
t
i
is a
hypothesis, then by assumption
v
(
s
) = 1. If
t
i
is obtained by modus ponens, say
from t
j
⇒ t
i
, since v(t
j
) = 1 and v(t
j
⇒ t
i
) = 1, we must have v(t
i
) = 1.
Note that soundness holds whenever our axioms are all tautologies. Even if
we had silly axioms that are able to prove almost nothing, as long as they are
all tautologies, it will be sound.
Now we have to prove adequacy. It seems like a big and scary thing to prove.
Given that a statement is true, we have to find a proof for it, but we all know
that finding proofs is hard!
We first prove a special case. To do so, we first define consistency.
Definition (Consistent).
S
is inconsistent if
S ⊢ ⊥
.
S
is consistent if it is not
inconsistent.
The special case we will prove is the following:
Theorem (Model existence theorem). If
S |
=
⊥
, then
S ⊢ ⊥
. i.e. if
S
has no
model, then
S
is inconsistent. Equivalently, if
S
is consistent, then
S
has a
model.
While we called this a “special case”, it is in fact all we need to know to
prove adequacy. If we are given
S |
=
t
, then
S ∪ {¬t} |
=
⊥
. Hence using the
model existence theorem, we know that
S ∪ {¬t} ⊢ ⊥
. Hence by the deduction
theorem, we know that S ⊢ ¬¬t. But ⊢ (¬¬t) ⇒ t by Axiom 3. So S ⊢ t.
As a result, some books call this the “completeness theorem” instead, because
the rest of the completeness theorem follows trivially from this.
The idea of the proof is that we’d like to define v : L → {0, 1} by
p 7→
(
1 if p ∈ S
0 if p ∈ S
However, this is obviously going to fail, because we could have some
p
such that
S ⊢ p
but
p ∈ S
, i.e.
S
is not deductively closed. Yet this is not a serious problem
— we take the deductive closure first, i.e. add all the statements that
S
can prove.
But there is a more serious problem. There might be a
p
with
S ⊢ p
and
S ⊢ ¬p
. This is the case if, say,
p
never appears in
S
. The idea here is to
arbitrarily declare that
p
is true or false, and add
p
or
¬p
to
S
. What we have
to prove is that we can do so without making S consistent.
We’ll prove this in the following lemma:
Lemma. For consistent
S ⊂ L
and
p ∈ L
, at least one of
S ∪{p}
and
S ∪{¬p}
is consistent.
Proof.
Suppose instead that both
S ∪ {p} ⊢ ⊥
and
S ∪ {¬p} ⊢ ⊥
. Then by the
deduction theorem,
S ⊢ p
and
S ⊢ ¬p
. So
S ⊢ ⊥
, contradicting consistency of
S.
Now we can prove the completeness theorem. Here we’ll assume that the
primitives
P
, and hence the language
L
is countable. This is a reasonable thing
to assume, since we can only talk about finitely many primitives (we only have
a finite life), so uncountably many primitives would be of no use.
However, this is not a good enough excuse to not prove our things properly.
To prove the whole completeness theorem, we will need to use Zorn’s lemma,
which we will discuss in Chapter 3. For now, we will just prove the countable
case.
Proof. Assuming that L is countable, list L as {t
1
, t
2
, ···}.
Let
S
0
=
S
. Then at least one of
S ∪ {t
1
}
and
S ∪ {¬t
1
}
is consistent. Pick
S
1
to be the consistent one. Then let
S
2
=
S
1
∪{t
2
}
or
S
1
∪{¬t
2
}
such that
S
2
is consistent. Continue inductively.
Set
¯
S
=
S
0
∪S
1
∪S
2
···
. Then
p ∈
¯
S
or
¬p ∈
¯
S
for each
p ∈ L
by construction.
Also, we know that
¯
S
is consistent. If we had
¯
S ⊢ ⊥
, then since proofs are finite,
there is some
S
n
that contains all assumptions used in the proof of
¯
S ⊢ ⊥
. Hence
S
n
⊢ ⊥, but we know that all S
n
are consistent.
Finally, we check that
¯
S
is deductively closed: if
¯
S ⊢ p
, we must have
p ∈
¯
S
.
Otherwise, ¬p ∈
¯
S. But this implies that
¯
S is inconsistent.
Define v : L → {0, 1} by
p 7→
(
1 if p ∈
¯
S
0 if not
.
All that is left to show is that this is indeed a valuation.
First of all, we have v(⊥) = 0 as ⊥ ∈
¯
S (since
¯
S is consistent).
For p ⇒ q, we check all possible cases.
(i)
If
v
(
p
) = 1
, v
(
q
) = 0, we have
p ∈
¯
S
,
q ∈
¯
S
. We want to show
p ⇒ q ∈
¯
S
.
Suppose instead that
p ⇒ q ∈
¯
S
. Then
¯
S ⊢ q
by modus ponens. Hence
q ∈
¯
S
since
¯
S
is deductively closed. This is a contradiction. Hence we
must have v(p ⇒ q) = 0.
(ii)
If
v
(
q
) = 1, then
q ∈
¯
S
. We want to show
p ⇒ q ∈
¯
S
. By our first axiom,
we know that
⊢ q ⇒
(
p ⇒ q
). So
¯
S ⊢ p ⇒ q
. So
p ⇒ q ∈
¯
S
by deductive
closure. Hence we have v(p ⇒ q) = 1.
(iii) If v(p) = 0, then p ∈
¯
S. So ¬p ∈
¯
S. We want to show p ⇒ q ∈
¯
S.
– This is equivalent to showing ¬p ⊢ p ⇒ q.
– By the deduction theorem, this is equivalent to proving {p, ¬p} ⊢ q.
– We know that {p, ¬p} ⊢ ⊥. So it is sufficient to show ⊥ ⊢ q.
– By axiom 3, this is equivalent to showing ⊥ ⊢ ¬¬q.
–
By the deduction theorem, this is again equivalent to showing
⊢ ⊥ ⇒
¬¬q.
– By definition of ¬, this is equivalent to showing ⊢ ⊥ ⇒ (¬q ⇒ ⊥).
But this is just an instance of the first axiom. So we know that
¯
S ⊢ p ⇒ q
.
So v(p ⇒ q) = 1.
Note that the last case is the first time we really use Axiom 3.
By remark before the proof, we have
Corollary (Adequacy theorem). Let S ⊂ L, t ∈ L. Then S |= t implies S ⊢ t.
Theorem (Completeness theorem). Le
S ⊂ L
and
t ∈ L
. Then
S |
=
t
if and
only if S ⊢ t.
This theorem has two nice consequences.
Corollary (Compactness theorem). Let
S ⊂ L
and
t ∈ L
with
S |
=
t
. Then
there is some finite S
′
⊂ S has S
′
|= t.
Proof. Trivial with |= replaced by ⊢, because proofs are finite.
Sometimes when people say compactness theorem, they mean the special
case where
t
=
⊥
. This says that if every finite subset of
S
has a model, then
S
has a model. This result can be used to prove some rather unexpected result in
other fields such as graph theory, but we will not go into details.
Corollary (Decidability theorem). Let
S ⊂ L
be a finite set and
t ∈ L
. Then
there exists an algorithm that determines, in finite and bounded time, whether
or not S ⊢ t.
Proof. Trivial with ⊢ replaced by |=, by making a truth table.
This is a rather nice result, because we know that proofs are hard to find in
general. However, this theorem only tells you whether a proof exists, without
giving you the proof itself!