Motivation for propositional logic

Propositional formulas work with truth values in the same way as arithmetic expressions work with numbers.

Suppose a tax of 10 % is levied on the sale of goods. Then the arithmetic expression \(x * 1.1\) is a good way to represent the gross price of a good in terms of its pre-tax price. This expression could, for instance, be used in a spread sheet to automatically calculate gross prices.

Now suppose we have a digital circuit:

Then the propositional formula \(X_0 \leftrightarrow \neg X_1\) is a good way of representing the output of the circuit in terms of its inputs. Here, one can think of \(X_0\) and \(X_1\) as representing the top and the bottom input, respectively, and \(\leftrightarrow\) and \(\neg\) standing for if, and only if and not, respectively.

Representing the output of a digital circuit in such a way has many advantages. For instance, suppose we had a much larger circuit. If we were in doubt that our circuit does what it is supposed to do we could—for a start—try to carry out some sanity checks. We could check whether there is a way to feed bits into the circuit such that the output is 1 and, symmetrically, that there is a way to feed bits into the circuit that the output is 0. (In other words, our circuit is somehow non-trivial if it passes the two tests.)

Given a so-called SAT solver, we could easily do that in practice. We would construct a propositional formula corresponding to the digital circuit (as above) and run a so-called SAT solver on it. This program would return "ok" if, and only if, 1 is a possible output.

We could then run the same program on the negation of the formula (prefix it with \(\neg\)): if the program returns "ok" it means that 0 is a possible output.

If we really wanted to check the circuit is correct we could ask an expert to give us a propositional formula which describes the desired behaviour in detail—a specification of the circuit. We would then have two propositional formulas, say \(\varphi\) and \(\psi\), one constructed from our circuit, one constructed by the expert.

We could then run the SAT solver on the formula \(\neg \varphi \leftrightarrow \psi\). The SAT solver would return "ok" if, and only if, the circuit was correct—doing what the specification requires.

In the above example, the formula \(\psi\) could just be \((X_0 \wedge \neg X_1) \vee (\neg X_0 \wedge X_1)\), which lists all the possible ways of getting 1 as an output.

This illustrates that propositional formulas may come in handy (just as arithmetic expressions do).