# Motivation for propositional logic

### From Learning Logic for Computer Science

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).