# Propositional formulas: syntax and semantics¶

In the following, we give a formal description for the syntax and semantics of propositional formulas and define the satisfiability problem.

## Syntax¶

We assume some countable set $$\Vars$$, such as $$\Set{a,b,c,...,z,x_1,x_2,...,y_1,y_2,...}$$, of Boolean variables. Boolean formulas can then be defined inductively:

• ​ Each Boolean variable in $$\Vars$$ is a formula.

• ​ The Boolean constants $$\FF$$ and $$\TF$$ are formulas.

• ​ If $$\LHS$$ and $$\RHS$$ are formulas, then so are

• $$(\neg \LHS)$$, the negation of $$\LHS$$, read “not $$\LHS$$”,

• $$(\LHS \land \RHS)$$, the conjunction of $$\LHS$$ and $$\RHS$$, read “$$\LHS$$ and $$\RHS$$”,

• $$(\LHS \lor \RHS)$$, the disjunction of $$\LHS$$ and $$\RHS$$, read “$$\LHS$$ or $$\RHS$$”,

• $$(\LHS \Xor \RHS)$$, the exclusive-or of $$\LHS$$ and $$\RHS$$, read “$$\LHS$$ xor $$\RHS$$” or “$$\LHS$$ or $$\RHS$$ but not both”,

• $$(\LHS \Implies \RHS)$$, the implication, read “$$\LHS$$ implies $$\RHS$$”, and

• $$(\LHS \Iff \RHS)$$, the bi-implication between $$\LHS$$ and $$\RHS$$, “$$\LHS$$ if and only if $$\RHS$$”.

• ​ (There are no other formulas.)

Example: Formulas

• $$a$$, $$b$$, $$(\neg b)$$, $$(a \land (\neg b))$$, and $$((a \land (\neg b)) \Implies ((\neg a) \lor c))$$ are formulas, but

• $$a \land \Implies b$$ is not.

One usually defines the following precedence, from the strongest to the weakest, between the operators: $$\neg$$, $$\land$$, $$\lor$$, $$\Xor$$, $$\Implies$$, $$\Iff$$. Parentheses can then be omitted if the precedence makes reading of the formula unambiguous. But when in doubt, use parentheses.

Example: Precedence

$${a \land \neg b} \Implies {\neg a \lor c}$$ means $$((a \land (\neg b)) \Implies ((\neg a) \lor c))$$.

Furthermore,

• ​ the operators $$\land$$, $$\lor$$, and $$\Xor$$ are associative and commutative: $$a \lor b \lor c$$ is the same as $$(a \lor b) \lor c$$ and $$a \lor (b \lor c)$$.

• $$\Implies$$ is right-associative: $$a \Implies b \Implies c$$ means $$a \Implies (b \Implies c)$$.

• $$\Iff$$ is left-associative and commutative: $$a \Iff b \Iff c$$ means $$(a \Iff b) \Iff c$$.

• $$\bigvee_{i \in I} x_i$$ means $$(x_{i_1} \lor ... \lor x_{i_n})$$ and $$\bigwedge_{i \in I} x_i$$ means $$(x_{i_1} \land ... \land x_{i_n})$$ for any finite index set $$I = \Set{i_1,...,i_n}$$.

Example

$$\bigvee_{i \in [1..3]}\bigwedge_{j \in [1..2]} x_{i,j}$$ means $$(x_{1,1} \land x_{1,2}) \lor (x_{2,1} \land x_{2,2}) \lor (x_{3,1} \land x_{3,2})$$

## Semantics¶

For a formula $$\phi$$, let $$\VarsOf{\phi}$$ be the set of variables occurring in it. A truth assignment for $$\phi$$ is a function $$\TA : \VarsOf{\phi} \to \Set{\False, \True}$$, meaning that it associates each variable in the formula to a truth value $$\False$$ (read “false”) or $$\True$$ (read “true”). A truth assignment $$\TA$$ on the variables can be extended to formulas inductively:

• $$\TA(\FF) = \False$$ and $$\TA(\TF) = \True$$

• $$\TA((\neg \LHS)) = \True$$ iff $$\TA(\LHS) = \False$$

• $$\TA((\LHS \land \RHS)) = \True$$ iff $$\TA(\LHS) = \True$$ and $$\TA(\RHS) = \True$$

• $$\TA((\LHS \lor \RHS)) = \True$$ iff $$\TA(\LHS) = \True$$ or $$\TA(\RHS) = \True$$

• $$\TA((\LHS \Xor \RHS)) = \True$$ iff either $$\TA(\LHS) = \True$$ or $$\TA(\RHS) = \True$$ but not both

• $$\TA((\LHS \Implies \RHS)) = \True$$ iff $$\TA(\LHS) = \False$$ or $$\TA(\RHS) = \True$$

• $$\TA((\LHS \Iff \RHS)) = \True$$ iff $$\TA(\LHS) = \TA(\RHS)$$

Example

For the formula $$a \Iff (a \Xor b)$$, the truth assignment $$\TA = \Set{a \mapsto \True, b \mapsto \False}$$ evaluates the sub-formulas so that $$\TA(a \Xor b) = \True$$ and $$\TA(a \Iff (a \Xor b)) = \True$$.

The truth assignment $$\TA = \Set{a \mapsto \True, b \mapsto \True}$$ evaluates the sub-formulas to $$\TA(a \Xor b) = \False$$ and $$\TA(a \Iff (a \Xor b)) = \False$$.

## Satisfiability and validity¶

A formula $$\phi$$ is satisfiable if there exists at least one truth assignment $$\TA$$ such that $$\TA(\phi) = \True$$. Such an assignment is also called a satisfying truth assignment (or model) for $$\phi$$. If $$\phi$$ is not satisfiable, it is called unsatisfiable.

Example

The formula $$(a \lor b) \land (a \Implies c) \land (b \Implies \neg c)$$ is satisfiable as both $$\Set{a \mapsto \True, b \mapsto \False, c \mapsto \True}$$ and $$\Set{a \mapsto \False, b \mapsto \True, c \mapsto \False}$$ evaluate it to true.

On the other hand, the formula $$(a \land b) \land (a \Implies c) \land (b \Implies \neg c)$$ is unsatisfiable.

The propositional satisfiability problem is the following computational problem:

Problem: Propositional satisfiability (SAT)

Instance: A propositional formula $$\phi$$.

Question: Is $$\phi$$ satisfiable?

A tool that solves the satisfiability problem is called a SAT solver. Such a tool takes a propositional formula $$\phi$$ as an input and then decides whether the formula is satisfiable or not. In addition to a simple “sat” (meaning “yes”) or “unsat” (meaning “no”) answer, a SAT solver usually also provides a satisfying truth assignment when the formula is satisfiable. If the formula is unsatisfiable, some solvers are also able to provide a machine verifiable proof of this. Such a proof is expressed in some proof system such as resolution (see The resolution proof system section) or an extension of it.

A formula $$\phi$$ is valid if $$\TA(\phi) = \True$$ for all truth assignments $$\TA$$ for $$\phi$$, meaning that there are no truth assignments that would evaluate the formula to false. Obviously, a formula $$\phi$$ is valid if and only if its negation $$\neg\phi$$ is unsatisfiable.

Example

The formula $$(a \lor b) \land (a \Implies c) \land (b \Implies \neg c)$$ is not valid as, for instance, $$\Set{a \mapsto \True, b \mapsto \False, c \mapsto \False}$$ evaluates it to false.

On the other hand, the formula $$\neg((a \land b) \land (a \Implies c) \land (b \Implies \neg c))$$ is valid.

## Logical consequences and equivalence¶

A formula $$\RHS$$ is a logical consequence of a formula $$\LHS$$, denoted by $$\LHS \models \RHS$$, if for all truth assignments $$\TA: (\VarsOf{\LHS} \cup \VarsOf{\RHS}) \to \Set{\False, \True}$$ it holds that if $$\TA(\LHS) = \True$$, then $$\TA(\RHS) = \True$$. That is, $$\LHS \models \RHS$$ if $$\RHS$$ evaluates to true whenever $$\LHS$$ does.

Example

• $$(a \lor \neg b) \land (\neg a \lor c) \models (\neg b \lor c)$$

• $$(a \lor \neg b) \land (\neg a \lor c) \not\models (\neg b)$$

Formula $$\LHS$$ and $$\RHS$$ are logically equivalent, denoted by $$\LHS \Equiv \RHS$$, if for all truth assignments $$\TA: (\VarsOf{\LHS} \cup \VarsOf{\RHS}) \to \Set{\False, \True}$$ it holds that $$\TA(\LHS) = \TA(\RHS)$$.

Example

$$(a \Implies b \lor c) \land (\neg a \Implies b \lor c)$$ and $$b \lor c$$ are logically equivalent.

Observe that $$\LHS$$ and $$\RHS$$ are logically equivalent iff $$\LHS \Iff \RHS$$ is valid iff $$\LHS \Xor \RHS$$ is unsatisfiable. The following lists some commonly applied logical equivalences, some others can be found this wikipedia page.

• ​ Identity laws: $$\LHS \land \True \Equiv \LHS$$ and $$\LHS \lor \False \Equiv \LHS$$

• ​ Domination laws: $$\LHS \land \False \Equiv \False$$ and $$\LHS \lor \True \Equiv \True$$

• ​ Double negation law: $$\neg(\neg \LHS) \Equiv \LHS$$

• ​ Negation laws: $$\LHS \land \neg \LHS \Equiv \False$$ and $$\LHS \lor \neg \LHS \Equiv \True$$

• ​ De Morgan’s laws: $$(\LHS \lor \RHS) \Equiv \neg(\neg \LHS \land \neg \RHS)$$ and $$(\LHS \land \RHS) \Equiv \neg(\neg \LHS \lor \neg \RHS)$$.

• ​ Distributive laws: $$\LHS \lor (\RHS_1 \land \RHS_2) \Equiv (\LHS \lor \RHS_1) \land (\LHS \lor \RHS_2)$$ and $$\LHS \land (\RHS_1 \lor \RHS_2) \Equiv (\LHS \land \RHS_1) \lor (\LHS \land \RHS_2)$$

• $$(\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS)$$

• $$(\LHS \Iff \RHS) \Equiv \neg(\LHS \Xor \RHS)$$

• $$\LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS$$

• $$(\LHS_1 \land ... \land \LHS_k) \Implies (\RHS_1 \lor ... \lor \RHS_m) \Equiv (\neg \LHS_1 \lor ... \lor \neg \LHS_k \lor \RHS_1 \lor ... \lor \RHS_m)$$

As we will see later, logical equivalences can be used to transform formulas to others as we can substitute sub-formulas with equivalent ones.

Example

The formula $$a \land (\neg a \lor (b \Iff c)) \land \neg(a \land \neg(b \Xor c))$$ can be simplified to

1. $$a \land (a \Implies (b \Iff c)) \land \neg(a \land \neg(b \Xor c))$$ by using the equivalence $$(\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS)$$,

2. $$a \land (b \Iff c) \land \neg(a \land \neg(b \Xor c))$$ by using $$\LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS$$,

3. $$a \land (b \Iff c) \land \neg(\neg(\neg a \lor \neg(\neg(b \Xor c))))$$ by using De Morgan’s law,

4. $$a \land (b \Iff c) \land (\neg a \lor (b \Xor c))$$ by using the double negation law,

5. $$a \land (b \Iff c) \land (a \Implies (b \Xor c))$$ by using the equivalence $$(\LHS \Implies \RHS) \Equiv (\neg \LHS \lor \RHS)$$,

6. $$a \land (b \Iff c) \land (b \Xor c)$$ by using $$\LHS \land (\LHS \Implies \RHS) \Equiv \LHS \land \RHS$$,

7. $$a \land \neg(b \Xor c) \land (b \Xor c)$$ by using $$(\LHS \Iff \RHS) \Equiv \neg(\LHS \Xor \RHS)$$

8. $$a \land \False$$ by using the negation law, and

9. $$\False$$ by the domination law.

Thus the original formula is unsatisfiable.