A form of
proof in
propositional logic that determines whether a
proposition follows from other propositions, by working through the
truth tables for the
premisses, and checking whether the
consequent is true whenever the premisses are. If so, the consequent is proved. The method is guaranteed to be correct but is impossibly cumbersome beyond small examples because the size of the calculation is
exponential on the number of premisses.
Contrast syntactic proof, which uses logical operations such as modus ponens to rearrange and combine theorems derived from the premisses, but which is not guaranteed to find an elegant solution.
Suppose we know that (A) I won't need my umbrella just in case it doesn't rain today, (B) it always rains on Saturdays, and (C) today is Saturday. We want to prove whether I'll need my umbrella. Let these propositions be built out of simple ones:
P = I'll need my umbrella
Q = it will rain today
R = today is Saturday
Then the propositions we know as premisses (know to be true; are
assuming to be true) are:
(A) ~Q <-> ~P
(B) R -> Q
(C) R
And what we want to ascertain is whether P (I'll need my umbrella) is a valid
deduction from these.
Now we build the truth table for these:
P Q R ~Q <-> ~P , R -> Q
T T T
T T F
T F T
T F F
F T T
F T F
F F T
F F F
Boolean operators inside complex propositions need to evaluated in order of
bracketing or
binding, innermost to outermost. So do the
negatives first:
P Q R ~Q <-> ~P , R -> Q
T T T F F
T T F F F
T F T T F
T F F T F
F T T F T
F T F F T
F F T T T
F F F T T
Now do the
biconditional and the
implication:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
T F T T F F F
T F F T F F T
F T T F F T T
F T F F F T T
F F T T T T F
F F F T T T T
We want to work out what follows if all three of our premisses are true. The first premiss (A), which is ~Q <-> ~P, is true in the following lines of the table:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
F F T T T T F
F F F T T T T
The next one, (B) which is R -> Q, is true in the following lines of that
subtable:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
F F F T T T T
The final premiss (C) is R, and that's true in the following part of the previous subtable:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
The
conclusion we're looking for is P. We see that in all lines of the current table, P is true. So P follows
deductively from the three premisses.