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.