| 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_clever | i_will_pass | i_am_clever => i_will_pass | i_will_pass => i_am_clever | i_am_clever | i_will_pass | A | i_am_clever ^ i_will_pass |
| T | T | T | T | T | T | T |
| T | F | F | T | T | F | F |
| F | T | T | F | T | F | F |
| F | F | T | T | F | F | F |
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 conclusion 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 conclusion 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
| ||||||
| p | q | p => q | q => p | p | q | A | p & q |
| T | T | T | T | T | T | T |
| T | F | F | T | T | F | F |
| F | T | T | F | T | F | F |
| F | F | T | T | F | F | F |
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. 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
| ||||||
| p | q | p => q | q => p | p | q | A | p & q |
| T | T | T | T | T | T | T |
| T | F | F | F | |||
| F | T | T | F | F | ||
| F | F | T | T | F | F | |
Another example to illustrate logical consequence in propositional logic, using meaningless propositions:
| Example | |||||||
|---|---|---|---|---|---|---|---|
A = { q | r,
q => ~p,
~(r & p) }
C = ~p
| |||||||
| p | q | r | q | r | q => ~p | ~(r & p) | A | ~p |
| T | T | T | T | F | F | ||
| T | T | F | T | F | F | ||
| T | F | T | T | T | F | F | |
| T | F | F | F | F | |||
| F | T | T | T | T | T | T | T |
| F | T | F | T | T | T | T | T |
| F | F | T | T | T | T | T | T |
| F | F | F | F | F | |||
Each of the three models of the axiom set is also a model of the conclusion, i.e., the conclusion is a logical consequence of the axiom set.
Here's an example where the formula is not a logical consequence of the axiom set:
| Example (of non-logical consequence) | ||||
|---|---|---|---|---|
A = { p => q,
q }
C = p & q
| ||||
| p | q | p => q | A | p & q |
| T | T | T | T | T |
| T | F | F | ||
| F | T | T | T | F |
| F | F | F | ||
The third interpretation is a model of the axiom set, but is not a model of the concluion. The conclusion is thus not a logical consequence of the axiom set.
An example to illustrate logical consequence by an unsatisfiable axiom set:
| Example | ||||||||
|---|---|---|---|---|---|---|---|---|
A = { p => q,
q => p,
p | q,
p => ~q }
C = ~r
| ||||||||
| p | q | r | p => q | q => p | p | q | p => ~q | A | ~r |
| T | T | T | T | T | T | F | F | |
| T | T | F | T | T | T | F | F | |
| T | F | T | F | F | ||||
| T | F | F | F | F | ||||
| F | T | T | T | F | F | |||
| F | T | F | T | F | F | |||
| F | F | T | T | T | F | F | ||
| F | F | F | T | T | F | F | ||
There are no models of the axiom set, so every model of the axiom set is a model of the conclusion, i.e., the conclusion 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.
Here is an example illustrating logical consequence in propositional logic by unsatisfiability:
| Example | |||||||
|---|---|---|---|---|---|---|---|
A = { q | r,
q => ~p,
~(r & p) }
C = ~p
| |||||||
| p | q | r | q | r | q => ~p | ~(r & p) | {~C} = p | A U {~C} |
| T | T | T | T | F | F | ||
| T | T | F | T | F | F | ||
| T | F | T | T | T | F | F | |
| T | F | F | F | F | |||
| F | T | T | T | T | T | F | F |
| F | T | F | T | T | T | F | F |
| F | F | T | T | T | T | F | F |
| F | F | F | F | F | |||
None of the interpretations are models of A U {~C}, i.e. A U {~C} is unsatisfiable and the conclusion is 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 conclusion is a logical consequence of an axiom set is O(E). Note that it is always possible to decide whether or not a conclusion 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].
| Axioms | F |
|---|---|
|
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 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 |