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.