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 `Φ={φ`

is a set of formulas, _{0},...,φ_{n-1}}`ψ`

a formula, and
`Φ⊨ψ`

, then we can write `φ`

_{0}∧...∧φ_{n-1}⊨ψ

**Theorem 1**
`φ`

if and only if
_{0}∧...∧φ_{n-1}⊨ψ`⊨φ`

.
_{0}∧...∧φ_{n-1}⇒ψ

*Proof:*
(`⇒`

) Assume that `φ`

.
For every truth assignment _{0}∧...∧φ_{n-1}⊨ψ`γ`

such that `γ⊨φ`

then we have
_{0}∧...∧φ_{n-1}`γ⊨ψ`

, so `γ⊨φ`

.
Every truth assignment _{0}∧...∧φ_{n-1}⇒ψ`γ`

such that `γ⊭φ`

then
_{0}∧...∧φ_{n-1}`γ⊨φ`

by the definition of implication.
Hence _{0}∧...∧φ_{n-1}⇒ψ`⊨φ`

.
_{0}∧...∧φ_{n-1}⇒ψ

(`⇒`

) Assume `⊨φ`

.
If _{0}∧...∧φ_{n-1}⇒ψ`γ`

is a truth assignment, then `γ⊨φ`

.
So, if _{0}∧...∧φ_{n-1}⇒ψ`γ⊨φ`

then _{0}∧...∧φ_{n-1}`γ⊨ψ`

by the definition of implication.
Therefore `φ`

.
_{0}∧...∧φ_{n-1}⊨ψ

**Theorem 2**
`φ`

if and only if _{0}∧...∧φ_{n-1}⊨ψ`⊭φ`

.
_{0}∧...∧φ_{n-1}∧¬ψ

*Proof*
If `⊨φ`

then
_{0}∧...∧φ_{n-1}⇒ψ`⊭¬(φ`

.
Now
_{0}∧...∧φ_{n-1}⇒ψ)`¬(φ`

_{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.