Logic for Computer Science/Propositional Logic

Propositional Logic

Propositional logic is a good vehicle to introduce basic properties of logic. It does not provide means to determine the validity (truth or false) of atomic statements. Instead, it allows you to evaluate the validity of compound statements given the validity of its atomic components.

For example, consider the following:

I like Pat or I like Joe.

If I like Pat then I like Joe.

Do I like Joe?

Accept as facts the first two statements, noting that the use of "or" here is not exclusive and thus could really be thought of as saying "I like Pat, or I like Joe, or I like them both". Do these statements imply that "I like Joe" is true? Try to convince yourself that "I like Joe" is true, and consider another line of reasoning:

Pigs can fly or fish can sing.

If pigs can fly then fish can sing.

Can fish sing?

We can see that the answer is yes in both cases. The above two sets of statements can be both abstracted as follows:

${\begin{aligned}&P\lor Q\\&P\to Q\\&Q\end{aligned}}$?

Here, we are concerned about the logical reasoning itself, and not the statements. Thus, instead of working with pigs or Pats, we simply write $Q$s or $P$s. We begin our study first with the syntax of propositional logic: that is, we describe the elements in our language of logic and how they are written. We then describe the semantics of these symbols: that is, what the symbols mean.

Syntax

The syntax of propositional logic is composed of propositional symbols, logical connectives, and parenthesis. Rules govern how these elements can be written together. First, we treat propositional symbols merely as a set of some symbols, for our purposes we'll use letters of the Roman and Greek alphabets, and refer to the set of all symbols as ${\text{Prop}}$:

Propositional symbols: A set ${\text{Prop}}$ of some symbols. For example $p,q,r,\ldots$

Second, we have the logical connectives:

Logical connectives: $\land ,\lor ,\neg ,\to$

Note that these are not the minimal required set; they can be equivalently represented only using the single connective NOR (not-or) or NAND (not-and) as is used at the lowest level in computer hardware. Finally, we use parenthesis to denote expressions (later on we make parenthesis optional):

Parentheses: $(,)$

An expression is a string of propositional symbols, parenthesis, and logical connectives.

The expressions we consider are called formulas. The set ${\textrm {Form}}$ of formulas is the smallest set of expressions such that:

1. ${\text{Prop}}\subseteq {\text{Form}}$
2. If $\phi ,\psi \in {\text{Form}}$ then
   1. $(\phi \land \psi )\in {\text{Form}}$ ,
   2. $(\phi \lor \psi )\in {\text{Form}}$ ,
   3. $(\phi \to \psi )\in {\text{Form}}$ , and
   4. $(\neg \phi )\in {\text{Form}}$ .

Another way to define formulas is as the language defined by the following context-free grammar (with start symbol ${\text{Form}}$):

${\text{Form}}\Rightarrow {\text{Prop}}$ , where ${\text{Prop}}$ stands for any propositional symbol

${\begin{aligned}{\text{Form}}\Rightarrow ({\text{Form}}\land {\text{Form}})\\{\text{Form}}\Rightarrow ({\text{Form}}\lor {\text{Form}})\\{\text{Form}}\Rightarrow ({\text{Form}}\to {\text{Form}})\\{\text{Form}}\Rightarrow (\neg {\text{Form}})\end{aligned}}$

Fact 1 (Unique Readability): The above context free grammar is unambiguous.

Semantics

The function of a formula is to create meanings of statements given meanings of atomic statements. The semantics of a formula $\phi$ with propositional symbols $p_{1},\ldots ,p_{n}$ is a mapping associating to each truth assignment $V$ to $p_{1},\ldots ,p_{n}$ a truth value (0 or 1) for $\phi$ . (The truth values true and false can be used instead of 1 or 0, respectively, as well as the abbreviations T and F.)

The semantics are well defined due to Fact 1 (seen just above).

One way to specify semantics of a logical connective is via a truth table:

$p$	$q$	$p\land q$ (p and q)
0	0	0
0	1	0
1	0	0
1	1	1

Can one always find a formula that implements any given semantics? Yes, any truth table is realized by a formula. The formula can be found as follows. "Represent" the rows where $\phi =1$ with conjunctions of the true proposition symbols and negations of the false ones. Finally write the disjunction of the results.

For example,

$p$	$q$	$\phi$	Conjunctions (true values only)
0	0	1	$\neg p\land \neg q$
0	1	0
1	0	1	$p\land \neg q$
1	1	0

$\phi :(p\land \neg q)\lor (\neg p\land \neg q)$

Corollary: Every formula is equivalent to a disjunction of conjunctions of propositional symbols or negation of propositional symbols (DNF).

Dual of DNF is CNF.

To get $\phi$ in CNF:

1. Describe cases when $\phi$ is false.
2. Note that $\phi$ is true when $\neg \psi$ is false. Hence, negate $\psi$ using DeMorgan's laws.

There are cases when DNF (resp. CNF) is exponentially larger than the original formula. For example, for $(x_{1}\lor y_{1})\land \cdots \land (x_{n}\lor y_{n})$ the equivalent DNF is exponential in size.

Does each truth table have a polynomial size formula implementing it? More precisely, does there exist $k$ such that every truth table with $n$ propositional symbols has a form $\phi$ of size $\leq n^{k}$ ? Answer: no.

Proof: Assume there exists such $k$ . The number of truth tables for $n$ propositional symbols is $2^{2^{n}}$ . The number of formulas of size $\leq n^{k}$ is $(n+6)^{n^{k}}$ ($n$ propositional symbols, 4 connectives and parentheses.) Clearly, $(n+6)^{n^{k}}<2^{2^{n}}$ , for sufficiently large $n$.

[TODO: exposition to explain what these definitions are and provide their context]

• Satisfaction: Satisfaction of a formula $\phi$ by a truth assignment $\tau$ . Notation: $\tau \models \phi$ ($\phi$ is true for $\tau$).
• Implication: A set of formulas $\Sigma$ implies $\phi$ . Notation: $\Sigma \models \phi$ . $\Sigma$ implies $\phi$ if and only if every truth assignment that satisfies $\Sigma$ also satisfies $\phi$ .

Formula Classes of Special Interest

• ${\text{VALID}}$ – the set of formulas that are always true (also known as tautologies). For example, $(p\lor \neg p),(p\to p),([(p\lor q)\land (p\to q)]\to q)$ are valid formulas.
• ${\text{UNSAT}}$ – the set of formulas that are never true (unsatisfiable).
• In between: ${\text{SAT}}$ - the set of formulas for which there exists a satisfying assignment (not unsatisfiable).

Note. $\phi \in {\text{VALID}}\iff \neg \phi \in {\text{UNSAT}}$ .

Claim: $\Sigma \models \phi \iff (\Sigma \cup \{\neg \phi \})\in {\text{UNSAT}}$

Claim: ${\text{SAT}}$ is NP-complete.

Proof:

• ${\text{SAT}}\in {\text{NP}}$ : guess a satisfying assignment, then verify that the formula is true (a satisfying assignment is a certificate).
• Hardness. graph 3-coloring $\in {\text{NP}}$ (there also exists a direct proof). We reduce 3-coloring to ${\text{SAT}}$. Let $G=(V,E)$ be a graph with $n$ nodes $\{1,\ldots ,n\}$ . We use propositional variables $p_{i,g},p_{i,r},p_{i,b}$ to indicate that vertex $i$ is colored with green, red, or blue. Construct $\phi$ as follows:

${\begin{aligned}\phi =&\bigwedge _{i=1}^{n}{\bigl (}(p_{i,g}\land \neg p_{i,r}\land \neg p_{i,b})\lor (p_{i,r}\land \neg p_{i,g}\land \neg p_{i,b})\lor (p_{i,b}\land \neg p_{i,r}\land \neg p_{i,g}){\bigr )}\\&\wedge \bigwedge _{(i,j\in E)}\neg (p_{i,g}\land p_{j,g})\land \neg (p_{i,r}\land p_{j,r})\land \neg (p_{i,b}\land p_{j,b})\end{aligned}}$

Claim: $G\in {\text{3-Coloring}}\iff \phi \in {\text{SAT}}$ .

It is also possible to prove that ${\textrm {SAT}}\in {\text{NP}}$ directly

Claim: ${\text{VALID}}\in {\text{coNP}}$ .

Horn Clauses

Special case for which SAT is in polynomial time. Example:

$(p\lor \neg q\lor r)\land (\neg p\lor q\lor \neg r)$

A Horn clause is a disjunction of literals of which at most one is positive. There are two kinds of possible Horn clauses:

1. clause has 1 positive literal
   1. $p$ , or
   2. $p\lor \neg x_{1}\lor \cdots \lor \neg x_{k}:x_{1}\land \cdots \land x_{k}\to p$
2. no positive literal
   1. $\neg x_{1}\lor \cdots \lor \neg x_{k}:\neg (x_{1}\land \cdots \land x_{k})$
   2. $x_{1}\land \cdots \land x_{k}\to {\text{false}}$

Claim: For every set $\Sigma$ of Horn formulas, checking whether $\Sigma$ is satisfiable is in ${\text{P}}$ .

Proof Idea: Let $\Sigma _{1}$ be the subset of $\Sigma$ containing only clauses of type 1, and $\Sigma _{2}$ the subset of $\Sigma$ containing clauses of type 2. Note first that $\Sigma _{1}$ is satisfiable. To obtain a minimum satisfying assignment $\sigma$ , start with literals from single-literal clauses and crank the rules. It now remains to check consistency of $\sigma$ with the clauses in $\Sigma _{2}$ . To do this, it is enough to check that for each clause $x_{1}\land \cdots \land x_{k}\to {\text{false}}$ in $\Sigma _{2}$ , $\sigma$ is not true for all of $x_{1},\ldots ,x_{k}$ .

Example: Consider the set $\Sigma$ of Horn clauses:

${\begin{aligned}&p\\&q\\&r\\&\neg p\lor \neg q\lor s\\&\neg s\lor \neg r\lor t\\&\neg t\end{aligned}}$

The set $\Sigma _{1}$ of clauses of type 1 consists of the first 5 clauses, and $\Sigma _{2}$ consists of the last clause. Note that $\Sigma _{1}$ can also be written as:

${\begin{aligned}&p\\&q\\&r\\&p\land q\to s\\&s\land r\to t\end{aligned}}$

The minimum satisfying assignment for $\Sigma _{1}$ is obtained as follows:

1. start with $\{p,q,r\}$
2. use the first implication to infer $s$
3. use the second implication to infer $t$

Thus, the minimum satisfying assignment makes $\{p,q,r,s,t\}$ true. This contradicts $\Sigma _{2}$ , which states that $t$ must be false. Thus, $\Sigma$ is not satisfiable.

Deductive Systems

A deductive system is a mechanism for proving new statements from given statements.

Let $\Sigma$ be a set of known valid statements (propositional formulas). In a deductive system, there are two components: inference rules and proofs.

Inference rules

An inference rule indicates that if certain set of statements (formulas) $\varphi _{1},\ldots ,\varphi _{k}$ is true, then a given statement $\varphi$ must be true. An inference rule $H$ is denoted as $H:{\frac {\varphi _{1},\ldots ,\varphi _{k}}{\varphi }}$ .

Example (modus ponens): ${\frac {p,~~p\to q}{q}}$

Proofs

A proof of $\varphi$ from $\Sigma$ is sequence of formulas $\varphi _{1},\ldots ,\varphi _{n}$ such that $\varphi _{n}=\varphi$ and for all $i\leq n$

• Each formula $\varphi _{i}\in \Sigma$ , or
• There are a subset of formulas $\varphi _{i_{1}},\ldots ,\varphi _{i_{k}}:i_{1},\ldots ,i_{k}<i$ , such that ${\frac {\varphi _{i_{1}},\ldots ,\varphi _{i_{k}}}{\varphi _{i}}}$ is an inference rule.

If $\varphi$ has a proof from $\Sigma$ using inference rule $H$ we write $\Sigma \vdash _{H}\varphi$ .

Properties:

• Soundness: If $\Sigma \vdash _{H}\varphi$ then $\Sigma \models \varphi$ (i.e., all provable sentences are true). This property is fundamental for the correctness of the deductive system.
• Completeness: If $\Sigma \models \varphi$ then $\Sigma \vdash _{H}\varphi$ (i.e., all true sentences are provable). This is a desirable property in deductive systems.

Natural Deduction

Natural deduction is a collection of inference rules. Let $\perp$ denote contradiction, falsity. The following are the inference rules of natural deduction:

1. $\left\{{\frac {\varphi ,\psi }{\varphi \land \psi }}\right.$
2. $\left\{{\frac {\varphi \land \psi }{\varphi }}\right.$
3. $\left\{{\frac {\varphi \land \psi }{\psi }}\right.$
4. $\left\{{\frac {\varphi ,\varphi \to \psi }{\psi }}\right.$
5. $\left\{{\frac {\varphi ,\neg \varphi }{\perp }}\right.$
6. $\left\{{\frac {\neg (\neg \varphi )}{\varphi }}\right.$
7. $\left\{{\frac {\perp }{\varphi }}\right.$
8. $\left\{{\frac {\varphi \to \psi ,\psi \to \varphi }{\varphi \leftrightarrow \psi }}\right.$
9. $\left\{{\frac {\varphi \leftrightarrow \psi }{\varphi \to \psi }}\right.$
10. $\left\{{\frac {\varphi \leftrightarrow \psi }{\psi \to \varphi }}\right.$
11. $\left\{{\frac {\varphi }{\varphi \lor \psi }}\right.$
12. $\left\{{\frac {\psi }{\varphi \lor \psi }}\right.$
13. ${\begin{cases}{\dfrac {\begin{matrix}\varphi \\\vdots \\\psi \end{matrix}}{\varphi \to \psi }}\end{cases}}$
14. ${\begin{cases}{\dfrac {\begin{matrix}\varphi \\\vdots \\\perp \end{matrix}}{\neg \varphi }}\end{cases}}$
15. ${\begin{cases}{\dfrac {\begin{matrix}\neg \varphi \\\vdots \\\perp \end{matrix}}{\varphi }}\end{cases}}$
16. ${\begin{cases}{\dfrac {\begin{matrix}\varphi \lor \psi &\varphi &\psi \\&\vdots &\vdots \\&\rho &\rho \end{matrix}}{\rho }}\end{cases}}$

Rule (13) allows us to prove valid statements of the form "If $\varphi$ then $\psi$" even if we don't know the truth value of the $\varphi$ statement (i.e., $\varphi$ is not in the set $\Sigma$ of known valid statements). Indeed, for this rule, we start assuming $\varphi$ is valid. If we can conclude $\psi$ is valid in a world where $\Sigma \cup \varphi$ are valid, then we conclude that the relation $\varphi \to \psi$ is true, and we "release" the assumption $\varphi$ is valid.

We now show how to apply the above inference rules.

Example: De Morgan's Law for negated or-expressions says:

$\neg (\varphi \lor \psi )\leftrightarrow (\neg \varphi \land \neg \psi )$

Proof: By rule $(8)$ if we can prove $\neg (\varphi \lor \psi )\to (\neg \varphi \land \neg \psi )$ and $(\neg \varphi \land \neg \psi )\to \neg (\varphi \lor \psi )$ we can infer the desired result.

To prove the first direction, we use rule 13 and assume the hypothesis $\neg (\varphi \vee \psi )$. Then

$\neg (\varphi \lor \psi )$ (assumed)

$\varphi$ (assumed)

$\varphi \lor \psi$ (by rule 11)

$\perp$ (by rule 5)

$\neg \varphi$ (by rule 14)

$\psi$ (assumed)

$\varphi \lor \psi$ (by rule 11)

$\perp$ (by rule 5)

$\neg \psi$ (by rule 14)

$\neg \varphi \land \neg \psi$ (by rule 1)

$\neg (\varphi \lor \psi )\to (\neg \varphi \land \neg \psi )$ (by rule 13)

We now prove the second direction.

$\neg \varphi \land \neg \psi$ (assumed)

$\neg \varphi$ (by rule 2)

$\neg \psi$ (by rule 3)

$\varphi \lor \psi$ (assumed)

$\varphi \psi$ (assumed)

$\perp \perp$ (by rule 5)

$\perp$(by rule 16)

$\neg (\varphi \lor \psi )$ (by rule 14)

$(\neg \varphi \land \neg \psi )\to \neg (\varphi \lor \psi )$ (by rule 13)

Proof of Pierce's Law:

$[(A\to B)\to A]\to A$

$(A\to B)\to A$ (assumed) (1*)

$\neg A$ (assumed)

$A$ (assumed)

$\perp$ (by rule 5)

$B$ (by rule 7)

$A\to B$ (by rule 13)

$A$ (by assumption (1*) and rule 4)

$\perp$ (by rule 5)

$A$ (by rule 14)

$[(A\to B)\to A]\to A$ (by rule 13)

Fact 2: Natural deduction is sound.

To show that natural deduction is also complete we need to introduce propositional resolution.

Propositional Resolution

Resolution is another procedure for checking validity of statements. It involves clauses, formulas and a single resolution rule.

Some terminology:

Clause

A clause is a propositional formula composed by disjunction of literals. For example $p\lor q\lor \neg r$ . It is usually denoted as the set of literals, e.g. $\{p,q,\neg r\}$ .

The empty clause, denoted as an open box "$\Box$", is the disjunction of no literals. It is always false.

Formula

A set of clauses, each of them satisfiable. For example, ${\bigl \{}\{p,\neg q\},\{r\},\{\neg r,s\}{\bigr \}}$ represents the CNF formula $(p\lor \neg q)\land (r)\land (\neg r\lor s)$.

The empty formula, denoted as $\varnothing$ , is the set that contains no clauses. It is always true.

Resolution Rule

It is a rule that, given two clauses $C$ (containing some literal $y$) and $C'$ (containing some literal $\neg y$), allows to infer a new clause, called the resolvent of $C$ and $C'$ (with respect to $y$).

A proof system for resolution contains a single resolution rule, where the resolvent is defined as follows. Assume $C$ and $C'$ are clauses such that $y\in C$ and $\neg y\in C'$ , then

${\text{Res}}_{y}(C,C')=(C-\{y\})\cup (C'-\{\neg y\})$

The smallest set of clauses containing $\varphi$ and closed under resolution is denoted ${\text{Res}}(\varphi )$ .

Example: If $C=\{p,y\}$ and $C'=\{q,\neg y\}$ , then ${\text{Res}}_{y}(C,C')=\{p,q\}$ .

It is possible to show that the resolution rule, as defined, computes a clause that can be inferred using natural deduction.

Claim: Let $C$ and $C'$ be any two clauses such that $y\in C$ and $\neg y\in C'$ . Then $C\land C'\implies {\text{Res}}_{y}(C,C')$ .

In order to prove the validity of a statement $\psi$ , we will prove the negated statement $\neg \psi$ is unsatisfiable. To prove unsatisfiability of a formula $\varphi$ , we need to define the resolution refutation of the formula $\varphi$ :

The resolution refutation tree of the formula $\varphi$ is a tree rooted at the empty clause, where every leaf is a clause in $\varphi$ and each internal node is computed as the resolvent of the two corresponding children.

Notice that clauses of $\varphi$ can appear repeated as leaves. From above claim we can conclude that:

Claim: If there exists a resolution refutation tree for formula $\varphi$ , then $\varphi \implies \Box$ , that is, $\varphi$ is unsatisfiable.

Example: The formula

$\varphi =(p\lor q)\land (\neg q\lor r)\land (\neg r)\land (\neg p\lor \neg s)\land (s\lor \neg t)\land (t)$

has the following resolution refutation tree:

The order in which clauses are selected to compute the resolvent matters when computing the resolution refutation tree, as the following example shows: Consider the formula

$\psi =(p\lor q)\land (\neg q\lor r)\land (\neg p)\land (\neg q)$

Even though a resolution refutation tree may exist for $\psi$ , order is important when trying to build the tree. Below are two different resolution refutation trees, but only one is successful:

Unsuccessful attempt of resolution refutation tree for $\psi$

A successful resolution refutation tree for $\psi$

Properties of Propositional Resolution

Soundness: Propositional resolution is sound, that is, if there exists a resolution refutation tree for a given formula $\varphi$ , then $\varphi$ must be unsatisfiable.

Theorem: For any formula $\varphi$, if $\Box \in Res(\varphi )$, then $\varphi \implies \Box$.

Completeness: Propositional resolution is complete, that is, if a given formula $\varphi$ is unsatisfiable, then $\varphi$ has a resolution refutation tree.

Theorem: For any formula $\varphi$, if $\varphi \implies \Box$, then $\Box \in Res(\varphi )$.

Proof: By induction on the number of variables in $\varphi$.

Basis: We have one variable, say $p$. All possible clauses of $\varphi$ are $\{p\}$ and $\{\lnot p\}$. If $\varphi$ is unsatisfiable then both clauses occur, and therefore $\Box \in Res(\varphi )$.

Induction step: Suppose the hypothesis is true for formulas with less than $n$ variables. Let $\varphi$ be a formula with $n$ variables. Suppose $\Box \notin Res(\varphi )$; we will show $\varphi$ is satisfiable. Let $p$ be a variable of $\varphi$. Then either $\{p\}\notin Res(\varphi )$ or $\{\lnot p\}\notin Res(\varphi )$ (if both hold then $\Box \in Res(\varphi )$ immediately).

Assume $\{\lnot p\}\notin Res(\varphi )$. We define the formula $\varphi ^{p}$ as containing all clauses that do not contain $\{p\}$ and where the literal $\lnot p$ has been removed from each clause (in other words, $\varphi ^{p}$ is equivalent to the formula resulting from setting $p$ true).

Formally,

$\varphi ^{p}=\{C-\{\lnot p\}:C\in \varphi ,\,p\notin C\}$.

First, notice that

$Res(\varphi ^{p})=\{C-\{\lnot p\}:C\in Res(\varphi ),\,p\notin C\}$

and thus,

$\{\lnot p\}\notin Res(\varphi ^{p})$.

Also, since $\Box \notin Res(\varphi )$ we have that $\Box \notin Res(\varphi ^{p})$. By the induction hypothesis, $\varphi ^{p}$ is satisfiable. Then $\varphi$ is satisfiable by an extension of the satisfying assignment of $\varphi ^{p}$ with $p$ equal true. The case $\{p\}\in Res(\varphi )$ is analogous.

Completeness of Natural Deduction

Theorem: Let $H$ be the set of inference rules of Natural Deduction. If $\Sigma \models \varphi$ then $\Sigma \vdash _{H}\varphi$.

The idea behind the proof of completeness of natural deduction is as follows. Suppose $\varphi$ is valid (then $\lnot \varphi$ is unsatisfiable). We then show there exists a resolution refutation for $\varphi$ and then by applying the contradiction rule (rule 15):

${\frac {\begin{matrix}\neg \varphi \\\vdots \\\perp \end{matrix}}{\varphi }}$

we conclude $\varphi$ can be inferred.

Proof: (Sketch) Given a formula $\varphi$ valid under $\Sigma$, we perform the following steps:

1. Prove that $\lnot \varphi$ is equivalent to some $\psi$, where $\psi$ is in CNF.
2. Prove that $\psi \implies Res(\psi )$, for all $\psi$.
3. By completeness of resolution, if $\psi$ is unsatisfiable then $\Box \in Res(\psi )$. Therefore, $\{p\}$ and $\{\lnot p\}\in Res(\psi )$ for some literal $p$. This implies $Res(\psi )\implies \bot$.
4. Conclude that $\lnot \varphi \implies \bot$ and therefore $\varphi$ is valid.

Step (1) can be easily done by repeated application of De Morgan's laws. Step (2) can be proven using natural deduction. Finally, step (3) can be proven by induction on the number of steps to obtain $Res(\psi )$. Clearly, each step can be simulated using natural deduction.

It is very likely that any algorithm for propositional resolution will take very long on the worst case (recall that checking validity of a formula $\varphi$ is co-NP complete).

Linear Resolution and PROLOG

Linear resolution is a particular resolution strategy that always resolves the most recent resolvent with a clause. The resolution refutation tree so obtained is therefore linear. It is possible to prove that, if the set of clauses are Horn clauses, there exists a linear resolution strategy for any formula. That is, linear resolution is complete for the set of Horn clauses.

The language PROLOG uses resolution on a set of Horn clauses. Each clause is called a program clause. Moreover, clauses composed by a single literal are called facts. A clause with a single negated literal is called a query. The table below shows a comparison of the different notations. In PROLOG, to query a statement $t$, the idea is to negate the statement ($\lnot t$) and to perform resolution with the set of known true statements. If a resolution refutation tree is found, the statement $t$ is implied by the program.

Example: An example of linear resolution for the formula

$\phi =(p)\land (q)\land (r)\land (t\lor \lnot s\lor \lnot r)\land (s\lor \lnot p\lor \lnot q)\land (\lnot t)$

is shown here: