Skip to content

Propositions: Statements that can be either true or false.

No ambiguity.

Syntax of Propositional Logic

Use \(T,F\) to denote the constants True and False.

Use uppercase letters to denote atomic formulas.

Well-formed Formulae

\(\varphi::=A|B|\cdots|(\varphi)|\neg\varphi|\varphi\land\varphi|\varphi\lor\varphi|\varphi\Rightarrow\varphi|\varphi\Leftrightarrow\varphi|\varphi\oplus\varphi\)

Negation, conjunction, disjunction, implications, xor...

Operators can be defined in terms of each other:

  • Negation and conjunction is a minimal set.
  • Negation and disjunction is also a minimal set.

Truth Tables

omitted

Truth Assignments and Satisfiability

Truth Assignments

A truth assignment is a mapping from propositions to Boolean values: $$ \sigma:\text{Propositions}\to{T,F}. $$ For example: \(\varphi=A\lor(B\to(A\land C))\) has \(8\) possible truth assignments.

The assignment \(\sigma\) making the formula \(\varphi\) true, we say that the assignment satisfies, aka \(\sigma\vDash\varphi\). (The assignment is a model for the formula)

The assignment \(\sigma\) making the formula \(\varphi\) false, \(\sigma\nvDash\varphi\).

⚠The satisfiability check can be done in polynomial time.

Given 2 formulae \(\varphi_1,\varphi_2\), we write \(\varphi_1\vDash\varphi_2\) if all the models for \(\varphi_1\) are also models for \(\varphi_2\).

Satisfiability

Let models of \(\varphi\) be the set of all assignment that satisfy \(\varphi\): \(\text{models}(\varphi)\)

  • \(\varphi\) is satisfiable if \(\text{models}(\varphi)\neq\emptyset\)
  • \(\varphi\) is unsatisfiable if \(\text{models}(\varphi)=\emptyset\)
  • \(\varphi\) is valid if all assignments satisfy it.

Propositions:

  1. \(\varphi\) is valid iff \(\neg\varphi\) is unsatisfiable.
  2. \(\varphi\) is satisfiable iff \(\neg\varphi\) is not valid.

Some Equivalences

  • \((A\to B)\Leftrightarrow(\neg A\lor B)\)
  • \((A\lor B)\Leftrightarrow\neg(\neg A\land\neg B)\)
  • \((A\land B)\Leftrightarrow\neg(\neg A\lor\neg B)\)
  • \((A\to B)\Leftrightarrow(\neg B\to\neg A)\)
  • \(\neg(A\land B)\Leftrightarrow(\neg A\lor\neg B)\)
  • \(\neg(A\lor B)\Leftrightarrow(\neg A\land\neg B)\)
  • \(A\land(B\lor C)\Leftrightarrow(A\land B)\lor(A\land C)\)
  • \(A\lor(B\land C)\Leftrightarrow(A\lor B)\land(A\lor C)\)

The SAT Problem

A decision problem: decide whether a given formula \(f\) is SATisfiable.

Equivalently:

  • Is there an assignment that satisfies the formula?
  • Does the formula have a model?

Important: SAT is NP-complete. (Cook et al, 1971)

Minimal Sets of Operators and Normal Forms

A literal is either an atom or a negation of an atom.

A term is a conjunction of literals, e.g., \(\neg A\land\neg B\land C\).

A clause is a disjunction of literals, e.g., \(\neg A\lor\neg B\lor C\).

Negation Normal Form

A formula is Negation Normal Form if

  • It contains only negation, conjunction, disjunction.
  • Negation is only applied to atoms.

E.g. \(\neg A\lor\neg B\).

Every formula can be converted to NNF in linear time.

Disjunctive Normal Form

A DNF is composed of disjunctions of items. (a disjunction of conjunctions)

E.g., \((A\land B\land\neg C)\lor(\neg C\land D)\lor\neg A\).

To convert to DNF, we first convert to NNF, then distribute conjunctions.

In the worst case, conversion takes exponential time and space.

Observation: SAT of DNF is polynomial (We only need to check whether there are contradictions in each term)

Conjunctive Normal Form

A CNF is composed of conjunctions of clauses. (a conjunction of disjunctions)

E.g., \((A\lor B\lor\neg C)\land(\neg C\lor D)\land\neg A\).

In the worst case, conversion to CNF takes exponential time and space.

Tseitin's Encoding

By adding new variables, any formula can be converted to a CNF in linear time and space that is equisatisfiable!

First, build the parse tree and introduce a new proposition for each node.

Then replace the node by certain rules.

Linear-time algorithm, linearly increase in number of variables and clauses.

Deduction for Validity

A deduction system is a set of axioms and rules.

Example of rules:

Modus Ponens: $$ {{\varphi\to\psi,\varphi}\over\psi}(\text{M.P.}) $$ Transitivity $$ {{\varphi\to\psi,\psi\to\theta}\over\varphi\to\theta}(\text{Trans.}) $$ In general, $$ {\text{Premise}\over\text{Consequence}}(\text{Rule Name}) $$

Hilbert-style System for Propositional Logic

\(\Gamma\vdash_{\mathcal H}\varphi\) means that \(\varphi\) can be deduced from premises in \(\Gamma\) using axioms and rules of \(\mathcal H\).

A system is sound if every theorem is valid in every model: \(\vdash_{\mathcal H}\varphi\) implies \(\vDash\varphi\).

A system is complete if every valid formula is a theorem: \(\vDash\varphi\) implies \(\vdash_{\mathcal H}\varphi\).

Let \(\mathcal H\) include Modus Ponens and

  • H1: \(\varphi\to(\psi\to\varphi)\)
  • H2: \((\varphi\to(\psi\to\theta))\to((\varphi\to\psi)\to(\varphi\to\theta))\)
  • H3: \((\neg\varphi\to\neg\psi)\to(\psi\to\varphi)\)

then \(\mathcal H\) is sound and complete for propositional logic.

Natural Deduction for Propositional Logic

A system \(\mathcal N\) with no axioms, only rules. Some rules: $$ {\varphi \psi\over\varphi\land\psi}(\land\text{-I}) $$

\[ {\varphi\land\psi\over\varphi}(\land\text{-E1}) \]
\[ {\varphi\land\psi\over\psi}(\land\text{-E2}) \]

There are additional rules for disjunction etc. that make this system sound and complete.