In propositional logic
the formula ψ
is a logical consequence or follows logically from the set of formulas
Φ
if every truth assignment that satisfies Φ
satisfies ψ
.
In first-order logic
the formula ψ
is a logical consequence or follows logically from the set of formulas
Φ
if ψ
is true in every model of Φ
.
If Φ={φ0,...,φn-1}
is a set of formulas, ψ
a formula, and
Φ⊨ψ
, then we can write φ0∧...∧φn-1⊨ψ
Theorem 1
φ0∧...∧φn-1⊨ψ
if and only if
⊨φ0∧...∧φn-1⇒ψ
.
Proof:
(⇒
) Assume that φ0∧...∧φn-1⊨ψ
.
For every truth assignment γ
such that γ⊨φ0∧...∧φn-1
then we have
γ⊨ψ
, so γ⊨φ0∧...∧φn-1⇒ψ
.
Every truth assignment γ
such that γ⊭φ0∧...∧φn-1
then
γ⊨φ0∧...∧φn-1⇒ψ
by the definition of implication.
Hence ⊨φ0∧...∧φn-1⇒ψ
.
(⇒
) Assume ⊨φ0∧...∧φn-1⇒ψ
.
If γ
is a truth assignment, then γ⊨φ0∧...∧φn-1⇒ψ
.
So, if γ⊨φ0∧...∧φn-1
then γ⊨ψ
by the definition of implication.
Therefore φ0∧...∧φn-1⊨ψ
.
Theorem 2
φ0∧...∧φn-1⊨ψ
if and only if ⊭φ0∧...∧φn-1∧¬ψ
.
Proof
If ⊨φ0∧...∧φn-1⇒ψ
then
⊭¬(φ0∧...∧φn-1⇒ψ)
.
Now
¬(φ0∧...∧φn-1⇒ψ)
= ¬(¬(φ0∧...∧φn-1)∨ψ)
= ¬¬(φ0∧...∧φn-1)∧¬ψ)
= φ0∧...∧φn-1∧¬ψ
According to the two theorems just given, logical consequence can be demonstrated by a proof of validity or unsatisfiability.
We demonstrate that P∧Q
is a logical consequence of the propositional formula P∧(P⇒Q)
:
1) we can use a truth table to show that every truth assignment that satisfies P∧(P⇒Q)
satisfies P∧Q
:
P | Q | P⇒Q | P∧(P⇒Q) | P∧Q |
---|---|---|---|---|
f | f | t | f | f |
f | t | t | f | f |
t | f | f | f | f |
t | t | t | t | t |
2) we can use a truth table to show that (P∧(P⇒Q))⇒(P∧Q)
is a tautology:
P | Q | P⇒Q | P∧(P⇒Q) | P∧Q | (P∧(P⇒Q))⇒(P∧Q) |
---|---|---|---|---|---|
f | f | t | f | f | t |
f | t | t | f | f | t |
t | f | f | f | f | t |
t | t | t | t | t | t |
3) we can use a truth table to show that (P∧(P⇒Q))∧¬(P∧Q)
is a contradiction:
P | Q | P⇒Q | P∧(P⇒Q) | ¬(P∧Q) | (P∧(P⇒Q))∧¬(P∧Q) |
---|---|---|---|---|---|
f | f | t | f | t | f |
f | t | t | f | t | f |
t | f | f | f | t | f |
t | t | t | t | f | f |
4) we can transform(P∧(P⇒Q))⇒(P∧Q)
into conjunctive normal form to show that is a tautology:
(P∧(P⇒Q))⇒(P∧Q)
= ¬(P∧¬(P∨Q))∨(P∧Q)
= (¬P∨¬¬(P∨Q))∨(P∧Q)
= (¬P∨P∨Q)∨(P∧Q)
= (⊤∨Q)∨(P∧Q)
= ⊤∨(P∧Q)
= ⊤
5) we can transform(P∧(P⇒Q))∧¬(P∧Q)
into disjunctive normal form to show that is a contradiction:
(P∧(P⇒Q))∧¬(P∧Q)
= (P∧(¬P∨Q))∧¬(P∧Q)
= (P∧(¬P∨Q))∧(¬P∨¬Q)
= (P∧¬P)∨(P∧Q)∧(¬P∨¬Q)
= ⊥∨(P∧Q)∧(¬P∨¬Q)
= (P∧Q)∧(¬P∨¬Q)
= (P∧Q∧¬P)∨(¬P∧¬Q∧Q)
= (⊥∧Q)∨(⊥∧¬P)
= ⊥
We demonstrate that mortal(barry)
is a logical consequence of the first-order formula man(barry)∧(∀X man(X)⇒mortal(X))
.
Consider an arbitrary model M
such that M⊨man(barry)∧(∀X man(X)⇒mortal(X))
and M⊭mortal(barry)
.
We have M⊨man(barry)∧(man(barry)⇒mortal(barry))
and since man(barry)⇒mortal(barry)
is equivalent to
¬man(barry)∨mortal(barry))
we have a contradiction. Therefore M⊨mortal(barry)
.
Chang, C-L, Lee, R C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Copyright © 2016 Barry Watson. All rights reserved.