Logical Consequence in Propositional Logic

Logical consequence in propositional logic can be established using truth tables to check that "every model of the axiom set is a model of the formula".

Example 
A = { i_am_clever => i_will_pass,
      i_will_pass => i_am_clever,
      i_am_clever | i_will_pass }
C = i_am_clever & i_will_pass
i_am_cleveri_will_passi_am_clever => i_will_passi_will_pass => i_am_cleveri_am_clever | i_will_passAi_am_clever & i_will_pass
TTTTTTT
TFFTTFF
FTTFTFF
FFTTFFF

It is simply necessary to check that each row that is a model of the axiom set, i.e., in those rows where A is TRUE the conjecture is also TRUE. In this example only the first row needs to be checked. In general, the maximal number of rows to be checked is 2N, where N is the number of propositions in the language. Thus this constitutes a simple decision procedure for logical consequence in propositional logic.

To avoid accidental use of the intended meaning of the propositions, the propositions can be reduced to meaningless symbols. This indicates that the conjecture follows from the axioms, regardless of the meaning of the symbols, i.e., it is a logical consequence. The truth table is the same as before:

Example 
A = { p => q,
      q => p,
      p | q }
C = p & q
pqp => qq => pp | qAp & q
TTTTTTT
TFFTTFF
FTTFTFF
FFTTFFF

When building these truth tables, as soon as an axiom is found to be FALSE in a given interpretation, that interpretation can be ignored for the remaining axioms, because the check is only for interpretations that are models of all the axioms. (This is AI - solving an O(E) problem in O(P) time!) To make this observation most effective, the axioms that are most easily shown to be FALSE in many interpretations should be considered first.

Example 
A = { p => q,
      q => p,
      p | q }
C = p & q
pqp => qq => pp | qAp & q
TTTTTTT
TFF F
FTTF F
FFTTFF

Another example to illustrate logical consequence in propositional logic, using meaningless propositions:

Example 
A = { q | r,
      q => ~p,
      ~(r & p) }
C = ~p
pqrq | rq => ~p~(r & p)A~p
TTTTF F
TTFTF F
TFTTTFF
TFFF F
FTTTTTTT
FTFTTTTT
FFTTTTTT
FFFF F

Each of the three models of the axiom set is also a model of the conjecture, i.e., the conjecture is a logical consequence of the axiom set.

Here is an example illustrating logical consequence in propositional logic by unsatisfiability:

Example 
A = { q | r,
      q => ~p,
      ~(r & p) }
C = ~p
pqrq | rq => ~p~(r & p){~C} = pA ∪ {~C}
TTTTF F
TTFTF F
TFTTTF F
TFFF F
FTTTTTFF
FTFTTTFF
FFTTTTFF
FFFF F

None of the interpretations are models of A ∪ {~C}, i.e. A ∪ {~C} is unsatisfiable and the conjecture is a logical consequence of the axiom set.

Here is an example to illustrate logical consequence by an unsatisfiable axiom set:

Example 
A = { p => q,
      q => p,
      p | q,
      p => ~q }
C = ~r
pqrp => qq => pp | qp => ~qA~r
TTTTTTFF
TTFTTTFF
TFTF F
TFFF F
FTTTF F
FTFTF F
FFTTTF F
FFFTTF F

There are no models of the axiom set, so every model of the axiom set is a model of the conjecture, i.e., the conjecture is a logical consequence of the axiom set. Intuitively, it seems unreasonable to conclude ~r from the axiom set, as r is not even mentioned in the axioms. Thus it is sensible to first check that the axioms are satisfiable, by ensuring that at least one row of the truth tables has all the axioms true.

Here's an example where the formula is not a logical consequence of the axiom set:

Example (of non-logical consequence) 
A = { p => q,
      p | q }
C = p & q
pqp => qp | qAp & q
TTTTTT
TFF F
FTTTTF
FFTFF

The third interpretation is a model of the axiom set, but is not a model of the conjecture. The conjecture is thus not a logical consequence of the axiom set.

From the observation that the truth table for any propositional logic contains 2N rows for N propositions, it is clear that the complexity of determining whether or not a conjecture is a logical consequence of an axiom set is O(E). Note that it is always possible to decide whether or not a conjecture is a logical consequence of a set of axioms, i.e., the problem is decidable. In fact the problem can be shown to be NP-complete [REF].

Exercises

  1. Determine if each Conjecture is a logical consequence of the Axioms. Do some directly and some using unsatisfiability.

    Axioms Conjecture
    a
    a => b     		b
    p => q
    ~q | p
    p | q
    		p & q
    p => q
    p | q
    		p & q
    p | q | r
    r => (p | q)
    (q & r) => p
    ~p | q | r
    		q | r
    p | q | r
    r => (p | q)
    (q & r) => p
    ~p | q | r
    		q & (r => p)
    p => q
    ~q | p
    p | q
    ~(p & q)
    		(~q => p) => (q | ~p)
    q | p
    q => r
    (s & r) => t
    t => p
    		p
    q | p
    p => q
    q => (~r | p)
    r
    		p
    ~n | ~t
    m | q | n
    m => l
    q => l
    ~l | ~p
    r | p | n
    r => ~l
    		~t

  2. Convert the following to propositional logic, and use truth tables to determine whether or not the Conjecture is a logical consequence of the Axioms.

Exam Style Questions

  1. Use a truth table to show that (q => p) | ~(q => (p | r)) is a logical consequence of the set { p | q | r, r => (p | q), (q & r) => p, -p | q | r }
  2. Use a truth table to prove that ~p is a logical consequence of the set { q | r, q => ~p, ~(r & p) }.
  3. Use a truth table to show that p & q is not a logical consequence of the set { p => q, q }.
  4. Encode the following scenario in propositional logic, and prove the conjecture:
    If the races are fixed or the gambling houses are crooked, then the tourist trade will decline. If the tourist trade declines then the police force will be happy. The police force is never happy.
    Conclusion: The races are not fixed