# Logical Consequence

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.

## Example 1

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) = ⊥ ```

## Example 2

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)`.

## References

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.