TT2026 Introduction to Proof Systems notes

Remaining TODOs: 11

1. Logic

Definition 1.1: Logic is the study of the principles of correct reasoning.

This requires:

an unambiguous language in which we can formulate statements
a mathematical framework to determine the truth of a statement

Definition 1.2: A logical syllogism is an example of correct reasoning.

For example:

All beings are mortal;
All humans are beings;
Therefore all humans are mortal.

2. Propositional logic

2.1. Syntax

Definition 2.1.1: Basic sentences in propositional logic are atomic propositions.

For example, $𝑎 :$ Alice is an architect.

Definition 2.1.2: Compound sentences can be formed by logical connectives: $\neg$ (negation), $\lor$ (disjunction), $\land$ (conjunction).

e.g. $\neg 𝑎$ ; $𝑎 \lor 𝑏$ .

Example:

{\neg 𝑐, 𝑎 \lor 𝑏, 𝑏 \to 𝑐}

⊨𝑎

“⊨” means “entails”; we have some propositions and we draw a conclusion.

Definition 2.1.3: Let $𝑋 = {𝑥_{1}, 𝑥_{2}, \dots}$ be a countably infinite set of propositional variables.

Formulas of propositional logic are defined inductively:

(basis clause) true,false and every propositional variable $𝑥$ are propositional formulae
(inductive clause) If $𝐹, 𝐺$ are formulae, then so are $\neg 𝐹$ (negation), $𝐹 \lor 𝐺$ (disjunction, with $𝐹$ and $𝐺$ the disjuncts), and $𝐹 \land 𝐺$ (conjunction, with $𝐹$ and $𝐺$ the conjuncts)
(extremal clause) Nothing else is a formula

Remark: The extremal clause of the above definition ensures that the set of propositional formulae is the minimal set that satisfies the basis and inductive clauses.

Definition 2.1.4: There are some derived connectives:

implication: $𝐹 \to 𝐺 ≔ \neg 𝐹 \land 𝐺$ . Here $𝐹$ is the antecedent and $𝐺$ is the consequent
bi-implication: $𝐹 \leftrightarrow 𝐺 ≔ (𝐹 \to 𝐺) \land (𝐺 \to 𝐹)$
Exclusive-OR: $𝐹 \oplus 𝐺 ≔ (𝐹 \land \neg 𝐺) \lor (\neg 𝐹 \land 𝐺)$
Indexed conjunction: $⋀_{𝑖 = 1}^{𝑛} 𝐹_{𝑖} ≔ (\dots ((𝐹_{1} \land 𝐹_{2}) \land 𝐹_{3}) \land \dots \land 𝐹_{𝑛})$
Indexed disjunction: $⋁_{𝑖 = 1}^{𝑛} 𝐹_{𝑖} ≔ (\dots ((𝐹_{1} \lor 𝐹_{2}) \lor 𝐹_{3}) \lor \dots \lor 𝐹_{𝑛})$

Definition 2.1.5: The set of all formulae of proposition logic over

𝑋

is denoted by

ℱ︀ (𝑋)

Definition 2.1.6: The operate precedence for propositional logic is:

\underset{𝑖}{⋁}, \underset{𝑖}{⋀} ≪ \leftrightarrow ≪ \to ≪ \land, \lor ≪ \neg

Definition 2.1.7: A literal is an atomic proposition or its negation.

Definition 2.1.8: We say that $𝐹$ is in conjunctive normal form (CNF) if

𝐹 = ⋀_{𝑖 = 1}^{𝑛} ⋁_{𝑗 = 1}^{𝑚_{𝑖}} 𝐿_{𝑖, 𝑗},

where each $𝐿_{𝑖, 𝑗}$ is a literal.

$𝐹$ is in disjunctive normal form (DNF) if $𝐹$

𝐹 = ⋁_{𝑖 = 1}^{𝑛} ⋀_{𝑗 = 1}^{𝑚_{𝑖}} 𝐿_{𝑖, 𝑗} .

Definition 2.1.9: $𝐹$ is in $𝑘$ -CNF if it is in CNF, and all the $𝑚_{𝑖}$ s are equal to some fixed $𝑘$ .

$𝐹$ is in $𝑘$ -DNF if it is in DNF with all the $𝑚_{𝑖}$ s equal to fixed $𝑘$ .

Remark: Normal forms are particularly well-suited for algorithmic treating.

Definition 2.1.10: Functions on formulae of propositional logic are uniquely defined by specifying the function values for “base cases” and “inductive steps”, following the cases in Definition 2.1.3. Such a definition is said to use structural induction.

Example: Suppose we want to define a function that returns the set of all subformulae of a formula $𝐹$ .

We define $sub : 𝐹 (𝑋) \to 𝒫︀ (𝐹 (𝑋))$ using structural induction,

\begin{matrix} sub ( \end{matrix}

true)≔{true}sub(false)≔{false}sub(𝑥)≔{𝑥}sub(¬𝐹)≔sub(𝐹)∪{¬𝐹}sub(𝐹∧𝐺)≔sub(𝐹)∪sub(𝐺)∪{𝐹∧𝐺}sub(𝐹∨𝐺)≔sub(𝐹)∪sub(𝐺)∪{𝐹∨𝐺}

2.2. (Tarski-style) semantics

Definition 2.2.1: An assignment is a function $𝒜︀ : 𝑋 \to {0, 1}$ that induces a function $\hat{𝒜︀} : ℱ︀ (𝑋) \to {0, 1}$ . That is $𝒜︀$ maps propositional variables to truth values, and $\hat{𝒜︀}$ maps formulae to truth values.

We define $\hat{𝒜︀}$ using structural induction.

\begin{aligned} \hat{𝒜︀} ( \end{aligned}

false)≔0;𝒜︀̂(true)≔1;𝒜︀̂(𝑥)≔𝒜︀(𝑥)for every𝑥∈𝑋;𝒜︀̂(¬𝐹)≔{1if𝒜︀̂(𝐹)=00otherwise;𝒜︀̂(𝐹∧𝐺)≔{1if𝒜︀̂(𝐹)=1and𝒜︀̂(𝐺)=10otherwise;𝒜︀̂(𝐹∨𝐺)≔{1if𝒜︀̂(𝐹)=1or𝒜︀̂(𝐺)=10otherwise.

Note that we define $\hat{𝒜︀}$ in a kind of meta language - the “and” and “or” here are not the same as in propositional logic.

From now we write $𝒜︀$ instead of $\hat{𝒜︀}$ for convenience.

Remark: We can construct truth tables for logical and derived connectives in the obvious manner. Implication may be surprising:

$𝑎$	$𝑏$	$𝑎 \to 𝑏$
true	true	true
true	false	false
false	false	false
false	true	true

In particular this means that you can use false to show anything to be true, i.e. we should start with true assumptions when trying to prove something (obviously).

Definition 2.2.2: Let $𝐹, 𝐺 \in ℱ︀ (𝑋), 𝒮︀ \subseteq ℱ︀ (𝑋)$ and $𝒜︀ : 𝑋 \to {0, 1}$ . Then

If $𝒜︀ (𝐹) = 1$ then $𝒜︀ ⊧ 𝐹$ (“ $𝒜︀$ is a model of $𝐹$ ”, or “ $𝐹$ holds under $𝒜︀$ ”).
If $𝒜︀ ⊧ 𝐹$ for all $𝐹 \in 𝒮︀$ , then we write $𝐴 ⊧ 𝑆$ (“ $𝒜︀$ models $𝒮︀$ ”)
$𝐹$ is satisfiable is there is some $𝒜︀ : 𝑋 \to {0, 1}$ s.t. $𝒜︀ (𝐹) = 1$ , or $𝒜︀ ⊧ 𝐹$ . Otherwise, $𝐹$ is unsatisfiable.
If $𝐹$ holds under any assignment, we say that $𝐹$ is valid, or that $𝐹$ is a tautology.
If, for all assignments $𝒜︀$ , $𝒜︀ ⊧ 𝒮︀$ implies $𝒜︀ ⊧ 𝐹$ for some $𝐹$ (not neccessarily an $𝐹 \in 𝒮︀$ from statement 2), then $𝒮︀$ entails $𝐹$ , written $𝒮︀$ ⊨𝐹. We write $𝐺$ ⊨𝐹 if ${𝐺}$ ⊨𝐹.
If $𝐹$ ⊨𝐺 and $𝐺$ ⊨𝐹, then $𝐹$ and $𝐺$ are logically equivalent, $𝐹 \equiv 𝐺$ .
If $𝐹$ is satisfiable iff $𝐺$ is satisfiable, then $𝐹$ and $𝐺$ are equisatisfiable.

Example:

\begin{matrix} {𝑥, 𝑥 \to 𝑦} \end{matrix}

⊨𝑦𝑥→(𝑦→𝑧)≡(𝑥∧𝑦)→𝑧𝑥∨𝑦is equisat with(𝑥∨𝑧)∧(𝑦∨¬𝑧)

Example (Encoding constraint satisfaction problem - Hamiltonian path problem): For undirected graph $𝐺 ≔ (𝑉, 𝐸)$ , is there a path visiting every vertex exactly once?

Introduce propositional variables $𝑥_{𝑖, 𝑗}$ expressing whether a Hamiltonian path visits vertex $𝑖$ at time $𝑗$ in a Hamiltonian path.

\begin{matrix} 𝐹_{1} ≔ ⋀_{𝑖 = 1}^{𝑛} ⋁_{𝑗 = 1}^{𝑛} 𝑥_{𝑖, 𝑗} \\ 𝐹_{2} ≔ ⋀_{𝑖 = 1}^{𝑛} \underset{1 \leq 𝑗 \leq 𝑘 \leq 𝑛}{⋀} \neg (𝑥_{𝑖, 𝑗} \land 𝑥_{𝑖, 𝑘}) \\ 𝐹_{3} ≔ ⋀_{𝑖 = 1}^{𝑛} ⋀_{𝑘 = 1}^{𝑛} ⋀_{𝑗 = 1}^{𝑛 - 1} 𝑥_{𝑖, 𝑗} \land 𝑥_{𝑘, 𝑗 + 1} \to 𝑒_{𝑖, 𝑘} \\ 𝐹_{4} : \underset{{𝑖, 𝑗} \in 𝐸}{⋀} 𝑒_{𝑖, 𝑗} \land \underset{{𝑖, 𝑗} \notin 𝐸}{⋀} \neg 𝑒_{𝑖, 𝑗} . \end{matrix}

Then $𝐹_{1} \land 𝐹_{2} \land 𝐹_{3} \land 𝐹_{4}$ iff $𝐺$ has a Hamiltonian path.

This is a practical example of why satisfiable is an important concept.

Remark: This is nonconstructive, and also uses the law of the excluded middle; some claim that using the law of the excluded middle for nonconstructive proofs is invalid.

2.3. Minimal calculus (minimal logic)

Definition 2.3.1: The minimal calculus, $𝐌_{0}$ consists of a finite number of axioms:

$𝑃 𝐿_{1} : 𝐴 \to (𝐴 \land 𝐴)$
$𝑃 𝐿_{2} : (𝐴 \land 𝐵) \to (𝐵 \land 𝐴)$
$𝑃 𝐿_{3} : (𝐴 \to 𝐵) \to [(𝐴 \land 𝐶) \to (𝐵 \land 𝐶)]$
$𝑃 𝐿_{4} : [(𝐴 \to 𝐵) \to (𝐵 \to 𝐶)] \to (𝐴 \to 𝐶)$
$𝑃 𝐿_{5} : 𝐵 \to (𝐴 \to 𝐵)$
$𝑃 𝐿_{6} : (𝐴 \land (𝐴 \to 𝐵)) \to 𝐵$
$𝑃 𝐿_{7} : 𝐴 \to (𝐴 \lor 𝐵)$
$𝑃 𝐿_{8} : (𝐴 \lor 𝐵) \to (𝐵 \lor 𝐴)$
$𝑃 𝐿_{9} : [(𝐴 \to 𝐶) \land (𝐵 \to 𝐶)] \to [(𝐴 \lor 𝐵) \to 𝐶]$
$𝑃 𝐿_{10} : [(𝐴 \to 𝐵) \land (𝐴 \to \neg 𝐵)] \to \neg 𝐴$

We also have a single inference rule, modus ponens: From $𝐴$ and $𝐴 \to 𝐵$ , infer $𝐵$ .

Remark: Modus ponens is basically

𝑃 𝐿_{6}

, but it allows us to actually perform pattern-matching on the proof and reduce it.

Remark:All of the axioms are also valid formulae in Tarski-style semantics

Remark: Implication needs to be a primitive in the minimal logic, so that we can deal very carefully with negation.

Remark: The subscript 0 in

𝐌_{0}

indicates that this is a propositional logic (as opposed to, e.g., predicate logic)

Definition 2.3.2: A derivation in the minimal calculus is a finite sequence of formulae $𝐴_{1}, \dots, 𝐴_{𝑛}$ , each $𝐴_{𝑖}$ being either an axiom, or obtained from $𝐴_{𝑗}, 𝐴_{𝑘}, 𝑗, 𝑘 < 𝑖$ by application of modus ponens. If some $𝐴_{𝑖}$ is neither an axiom nor MP-derived, it is a hypothesis.

We write $⊢_{𝐌_{0}} 𝐵$ if $𝐵$ is derivable; then $𝐵$ is a theorem or provable in $𝐌_{0}$ .

Example:

$⊢ 𝐶 (hypothesis)$
$⊢ 𝐶 \to (𝐷 \to 𝐶) (𝑃 𝐿_{5})$
$⊢ 𝐷 \to 𝐶 (𝑀 𝑃 1, 2)$
$⊢ (𝐷 \to 𝐶) \to [(𝐷 \to 𝐷) \to (𝐶 \land 𝐷)] (𝑃 𝐿_{3})$
$⊢ (𝐷 \land 𝐷) \to (𝐶 \land 𝐷) (𝑀 𝑃 3, 4)$
$⊢ 𝐷 \to (𝐷 \land 𝐷) (𝑃 𝐿_{1})$
$⊢ 𝐷 (hypothesis)$
$⊢ 𝐷 \land 𝐷 (𝑀 𝑃 6, 7)$
$⊢ 𝐶 \land 𝐷 (𝑀 𝑃 5, 2)$

This gives us a new proof rule, conjunction introduction:

\land_{INTRO} : If ⊢_{𝐌_{0}} 𝐶 and ⊢_{𝐌_{0}} 𝐷 then ⊢_{𝐌_{0}} 𝐶 \land 𝐷 .

Example:

$𝐴 \to 𝐵$ (hypothesis)
$𝐵 \to 𝐶$ (hyp)
$(𝐴 \to 𝐵) \land (𝐵 \to 𝐶)$ ( $\land_{INTRO}$ (1, 2))
$[(𝐴 \to 𝐵) \land (𝐵 \to 𝐶)] \to (𝐴 \to 𝐶)$ (PL4)
$𝐴 \to 𝐶$ (MP (3, 4))

This gives us a new rule, transitivity of implication,

\to_{TRANS} : If ⊢_{𝐌_{0}} 𝐴 \to 𝐵 and ⊢_{𝐌_{0}} 𝐵 \to 𝐶 then ⊢_{𝐌_{0}} 𝐴 \to 𝐶 .

Definition 2.3.3: Ex falso quodlibet (“from falsehood, anything follows”) is the principal that

\neg 𝐴 \to (𝐴 \to 𝐵)

, i.e. anything is provable from a false hypothesis.

Definition 2.3.4: Tertium non datur (“no third [possibility] is given”) is the law of the excluded middle,

\neg \neg 𝐴 \to 𝐴

(equivalently,

𝐴 \land \neg 𝐴

is a tautology).

Remark: Not every valid statement in Tarski-style semantics is derivable using the minimal calculus.

In particular, it is not possible to derive ex falso quodlibet or tertium non datur.

Proposition 2.3.5: $⊬_{𝐌_{0}} \neg 𝐴 \to (𝐴 \to 𝐵)$

Proof: Let $ℎ : ℱ︀ (𝑋) \to {0, 1}$ be such that:

Propositional and template variables are given an arbitrary but fixed value
$ℎ (\neg 𝐹) = 0$
The remaining logical connectives are reduced inductively according to the following table
$ℎ (𝐹)$ $ℎ (𝐺)$ $ℎ (𝐹 \land 𝐺)$ $ℎ (𝐹 \lor 𝐺)$ $ℎ (𝐹 \to 𝐺)$
0 0 1 0 0
0 1 0 1 1
1 0 0 1 0
1 1 0 1 0

$ℎ (𝐹)$	$ℎ (𝐺)$	$ℎ (𝐹 \land 𝐺)$	$ℎ (𝐹 \lor 𝐺)$	$ℎ (𝐹 \to 𝐺)$
0	0	1	0	0
0	1	0	1	1
1	0	0	1	0
1	1	0	1	0

Then choose $ℎ$ such that $ℎ (𝐴) = 0, ℎ (𝐵) = 1$ , and observe that all aaxioms of $𝐌_{0}$ evaluate to 0 under $ℎ$ , while $ℎ (\neg 𝐴 \to (𝐴 \to 𝐵)) = 1$ .

Observe also that if $ℎ (𝐴) = ℎ (𝐴 \to 𝐵) = 0$ , then applying modus ponens to get $𝐵$ must have $ℎ (𝐵) = 0$ , otherwise $ℎ (𝐴 \to 𝐵)$ would evaluate to 1 by the definition of $ℎ$ .

Therefore, starting from axioms and using modus ponens, we cannot create a formula $𝐹$ that evaluates to 1 under $ℎ$ ; therefore $\neg 𝐴 \to (𝐴 \to 𝐵)$ is not derivable from the axioms and modus ponens.

Definition 2.3.6: If we add ex falso quodlibet as an extra axiom, PL11 $\neg 𝐴 \to (𝐴 \to 𝐵)$ , then we get intuitionistic logic, denoted $𝐉_{0}$ .

If we add tertium non datur, the law of the excluded middle, as a 12th axiom, we get classical logic, denoted $𝐊_{0}$ .

Theorem 2.3.7: For any formula

𝐹

⊧ 𝐹

(

𝐹

is valid) iff

⊢_{𝐊_{0}} 𝐹

⟸

is soundness and is simple.

⟹

is completeness and is more difficult to prove.

2.4. Equational reasoning

Idea: substitute subformulae by equivalent ones, according to the axioms of Boolean algebras.

Definition 2.4.1: A Boolean algebra is a structure that satisfies the following axioms:

$𝐴 \lor 𝐴 \equiv 𝐴$
$𝐴 \land 𝐴 \equiv 𝐴$ (idempotence)
$𝐴 \land 𝐵 \equiv 𝐵 \land 𝐴$
$𝐴 \lor 𝐵 = 𝐵 \lor 𝐴$ (commutativity)
$(𝐴 \land 𝐵) \land 𝐶 \equiv 𝐴 \land (𝐵 \land 𝐶)$
$(𝐴 \lor 𝐵) \lor 𝐶 \equiv 𝐴 \lor (𝐵 \lor 𝐶)$ (associativity)
$𝐴 \land (𝐴 \lor 𝐵) \equiv 𝐴$
$𝐴 \lor (𝐴 \land 𝐵) \equiv 𝐴$ (absorption)
$𝐴 \land (𝐵 \lor 𝐶) \equiv (𝐴 \land 𝐵) \lor (𝐴 \land 𝐶)$
$𝐴 \lor (𝐵 \land 𝐶) \equiv (𝐴 \lor 𝐵) \land (𝐴 \lor 𝐶)$ (distributivity)
$\neg \neg 𝐴 \equiv 𝐴$ (double negation)
$\neg (𝐴 \land 𝐵) \equiv \neg 𝐴 \lor \neg 𝐵$
$\neg (𝐴 \lor 𝐵) \equiv \neg 𝐴 \land \neg 𝐵$ (de Morgan)
$𝐴 \lor \neg 𝐴 \equiv$ true
$𝐴 \land \neg 𝐴 \equiv$ false (complementation)
$𝐴 \lor$ true≡true
$𝐴 \land$ false≡false (zero laws)
$𝐴 \lor$ false≡𝐴
$𝐴 \land$ true≡𝐴 (identity laws)

Remark: Sets form a Boolean algebra.

Definition 2.4.2: We write $𝐺 [𝐹 / 𝐻]$ to mean the formula obtained from $𝐺$ by replacing every occurrence of $𝐻$ in $𝐺$ by $𝐹$ .

This is a substitution.

Formally, $𝐺 [𝐹 / 𝐻] ≔ 𝐹$ if $𝐺 = 𝐻$ . For $𝐹 \neq 𝐻$ , we proceed by structural induction:

Base case: $𝑥 [𝐹 / 𝐻] ≔ 𝑥$ for all $𝑥 \in 𝑋$
Inductive steps:
- $(\neg 𝐺) [𝐹 / 𝐻] = \neg (𝐺 [𝐹 / 𝐻])$
- $(𝐺_{1} \land 𝐺_{2}) [𝐹 / 𝐻] = (𝐺_{1} [𝐹 / 𝐻]) \land (𝐺_{2} [𝐹 / 𝐻])$
- $(𝐺_{1} \lor 𝐺_{2}) [𝐹 / 𝐻] = (𝐺_{1} [𝐹 / 𝐻]) \lor (𝐺_{2} [𝐹 / 𝐻])$

Theorem 2.4.3 (Substitution theorem): Let $𝐹, 𝐺, 𝐺^{'}, 𝐻$ be formulae s.t. $𝐺^{'} = 𝐺 [𝐹 / 𝐻]$ and $𝐹 \equiv 𝐻$ , then $𝐺^{'} \equiv 𝐺$ .

Proof: By structural induction on $𝐺$ .

If $𝐺 \equiv 𝐻$ then $𝐺 [𝐹 / 𝐻] = 𝐹 \equiv 𝐻$ , hence $𝐺^{'} \equiv 𝐺$ .

Otherwise:

If $𝐺 = 𝑥$ , then $𝐺^{'} = 𝑥$ , hence $𝐺 \equiv 𝐺^{'}$
If $𝐺 = \neg 𝐽$ , then $𝐺^{'} = 𝐺 [𝐹 / 𝐻] = \neg (𝐽 [𝐹 / 𝐻])$ , by inductive hypothesis, $= \neg 𝐽^{'}$ where $𝐽^{'} \equiv 𝐽$
Conjunction and disjunction follow similarly.

Definition 2.4.4: A proof by equational reasoning of

𝐹 \equiv 𝐺

is a sequence

𝐹_{1}, \dots, 𝐹_{𝑛}

such that

𝐹_{1} = 𝐹

𝐹_{𝑛} = 𝐺

, and

𝐹_{𝑖 + 1}

is obtained from

𝐹_{𝑖}

by a substitution according to the Boolean algebra axioms.

Theorem 2.4.5 (soundness): If we have an equational proof starting in $𝐹$ and ending in $𝐺$ , then $𝐹 \equiv 𝐺$ .

Proof: Consequence of the substitution theorem.

Definition 2.4.6: A formula is in negation normal form if negation appears only in front of propositional variables.

Lemma 2.4.7: Every formula can be transformed into DNF by equational reasoning.

Proof:

We exhaustively apply de Morgan’s laws, and rewrite $\neg$ true≡false and $\neg$ false≡true. This gives us the negation normal form of $𝐹$ .

Then we exhaustively apply distributivity and the identity laws.

We can then reintroduce any variables $𝑥_{𝑖}$ that were eliminated, by replacing any disjunct $𝐷$ with $(𝐷 \land 𝑥_{𝑖}) \lor (𝐷 \land \neg 𝑥_{𝑖})$ . Thus we obtain a canonical (up to disjunct ordering) DNF for the formula.

Theorem 2.4.8 (comleteness): If $𝐹 \equiv 𝐺$ , then there is an equational proof starting in $𝐹$ and ending in $𝐺$ .

Proof: Given $𝐹, 𝐺$ s.t. $𝐹 \equiv 𝐺$ , then $𝐹$ and $𝐺$ have the same truth table, hence the same DNF $𝐻$ . Then we apply Lemma 2.4.7 to $𝐹$ to obtain $𝐻$ by proof $𝑃_{1}$ , and to $𝐺$ to obtain $𝐻$ by proof $𝑃_{2}$ .

Then the equational proof of $𝐹 \equiv 𝐺$ is $𝑃_{1}$ concatenated with the reverse of $𝑃_{2}$ .

2.5. Resolution

Use formulae in CNF, presented as sets.

E.g. if $𝐹 = \overset{clause}{\overset{⏞}{(𝑝_{1} \lor \neg 𝑝_{2})}} \land (𝑝_{3} \lor \neg 𝑝_{4} \lor 𝑝_{5}) \land (\neg 𝑝_{2})$ .

We represent this as ${\overset{clause}{\overset{⏞}{{𝑝_{1}, \neg 𝑝_{2}}}}, {𝑝_{3}, \neg 𝑝_{4}, 𝑝_{5}}, {\neg 𝑝_{2}}}$ .

We represent the empty clause as $□ \equiv$ false. ${□} \equiv$ false,{}≡true.

Remark: The set representation naturally expresses commutativity, associativity and idempotence.

Definition 2.5.1: Given literal $𝐿$ , we define

\overset{̅}{𝐿} = {\begin{cases} \neg 𝑝 & if 𝐿 = 𝑝 \\ 𝑝 & if 𝐿 = \neg 𝑝 . \end{cases}

Definition 2.5.2: Let $𝐶_{1}, 𝐶_{2}$ be clauses s.t. $𝐿 \in 𝐶_{1}$ and $\overset{̅}{𝐿} \in 𝐶_{2}$ . Then the resolvent of $𝐶_{1}$ and $𝐶_{2}$ is

𝑅 = (𝐶_{1} \ {𝐿}) \cup (𝐶_{2} \ {\overset{̅}{𝐿}}) .

We say that $𝑅$ is derived by resolution from $𝐶_{1}$ and $𝐶_{2}$ ; we write $.$

Definition 2.5.3: A derivation (or proof) of a clause $𝐶$ from the set of clauses $𝐹$ is a sequence $𝐶_{1}, \dots, 𝐶_{𝑚}$ of clauses such that

$𝐶_{𝑚} = 𝐶$
For each $1 \leq 𝑖 \leq 𝑚$ , either $𝐶_{𝑖} \in 𝐹$ (an assumption), or $𝐶_{𝑖}$ is the resolvent of $𝐶_{𝑗}$ and $𝐶_{𝑘}$ , for some $𝑗 \neq 𝑘, 𝑗, 𝑘 < 𝑖$ .

Definition 2.5.4: A derivation of

□

demonstrates a refutation of

𝐹

Remark: To show that

𝒮︀ ⊧ 𝐹

, we can demonstrate a refutation of

𝒮︀ \cup {\neg 𝐹}

Definition 2.5.5: Given $𝐹$ , define

Res (𝐹) = 𝐹 \cup {𝑅 | 𝑅 is a resolvent from two clauses in 𝐹} .

Also define ${Res}^{0} (𝐹) = 𝐹$ ; ${Res}^{𝑛_{1}} (𝐹) = Res ({Res}^{𝑛} (𝐹))$ .

Also ${Res}^{*} (𝐹) = ⋃_{𝑛 > 0} {Res}^{𝑛} (𝐹)$ . Note that this is computable in finite time. TODO is it?

Proposition 2.5.6:

𝐶 \in {Res}^{*} (𝐹)

iff there exists a resolution derivation of

𝐶

from

𝐹

Lemma 2.5.7 (Resolution lemma): If $𝑅$ is the resolvent of $𝐶_{1}, 𝐶_{2} \in 𝐹$ , then $𝐹 \equiv 𝐹 \cup {𝑅}$ .

Proof: $𝐹 \equiv 𝐹 \cup {𝑅}$ if we have that $𝒜︀ ⊧ 𝐹$ iff $𝒜︀ ⊧ 𝐹 \cup {𝑅}$ .

$⟸$ : If $𝒜︀ ⊧ 𝐹 \cup {𝑅}$ , then clearly $𝒜︀ ⊧ 𝐹$ .

$⟹$ : Let $𝒜︀ ⊧ 𝐹$ , $𝑅 = {𝐶_{1} \ {𝐿}} \cup {𝐶_{2} \ {\overset{̅}{𝐿}}}$ . Then we have two cases:

$𝒜︀ ⊧ 𝐿$ , then since $𝒜︀ ⊧ 𝐶_{2}$ , we have $𝒜︀ ⊧ 𝐶_{2} \ {\overset{̅}{𝐿}}$ . Hence $𝒜︀ ⊧ 𝑅$ .
$𝒜︀ ⊧ \neg 𝐿$ , then since $𝒜︀ ⊧ 𝐶_{1}$ , we have $𝒜︀ ⊧ 𝐶_{1} \ {𝐿}$ , so $𝒜︀ ⊧ 𝑅$ .

Theorem 2.5.8 (soundness): If $□$ can be derived by resolution from $𝐹$ , then $𝐹$ is unsatisfiable.

Proof: By induction on the length of the resolution proof.

$𝐹 \equiv 𝐹_{1} \equiv \dots \equiv 𝐹_{𝑛} \equiv □ \equiv$ false.

Theorem 2.5.9 (completeness): If $𝐹$ is unsatisfiable, then $□$ can be derived from $𝐹$ by resolution.

Proof: By induction on the number of propositional variables that appear in $𝐹$ , $𝑛$ .

If $𝑛 = 0$ , then $𝐹 = {□}$ . Trivial.

Then suppose true for $𝑛$ , and consider $𝑛 + 1$ .

$𝐹$ mentions prop. vars. $𝑝_{1}, \dots, 𝑝_{𝑛 + 1}$ . Let $𝐹_{0} = 𝐹 [$ false/𝑝𝑛+1],𝐹1=𝐹[true/𝑝𝑛+1].

Since $𝐹$ is unsatisfiable, both $𝐹_{0}$ and $𝐹_{1}$ are unsatisfiable. By the inductive hypothesis, we have $𝐶_{0}, 𝐶_{1}, \dots, 𝐶_{𝑚} = □$ being a refutation of $𝐹_{0}$ .

Note that $𝐶_{𝑖}$ or $𝐶_{𝑖} \cup {𝑝_{𝑛 + 1}}$ are already in $𝐹$ . By reintroducing $𝑝_{𝑛 + 1}$ , we either obtain a proof of $□$ , or of $𝑝_{𝑛 + 1}$ .

In the latter case, we can apply the same reasoning to $𝐹_{1}$ and obtain a proof of $\neg 𝑝_{𝑛 + 1}$ . Then the final resolution step gives us $□$ .

Remark: Constructing equivalent CNF formulae can be expensive. But because resolution only checks unsatisfiability, we only need an equisatisfiable formula.

Give $𝐹$ , do the following:

Introduce fresh prop. vars for every subformula $𝐺$ of $𝐹$ , whenever $𝐺$ is not a literal; call it $𝑥_{𝐺}$
Introduce $𝑥_{𝐺} \leftrightarrow 𝐺^{'}$ , where $𝐺^{'}$ is $𝐺$ , with the top-level subformulae replaced by the new prop. vars.
Use equational transformation to transform all of the $𝑥_{𝐺} \leftrightarrow 𝐺^{'}$ s into CNF
The final formula is all new CNF formulae, plus $𝑥_{𝐹}$ .

Example: Consider the formula $𝐹 = \neg (𝑝 \land 𝑞) \land 𝑟$ . The subformulae of $𝐹$ , excluding literals, are ${\neg (𝑝 \land 𝑞) \land 𝑟, \neg (𝑝 \land 𝑞), 𝑝 \land 𝑞}$ . Then we introduce new propositional variables $𝑥_{𝐹}$ , $𝑥_{\neg (𝑝 \land 𝑞)}$ , $𝑥_{𝑝 \land 𝑞}$ , and say that:

$𝑥_{𝐹} \leftrightarrow 𝑥_{\neg (𝑝 \land 𝑞)} \land 𝑟$
$𝑥_{\neg (𝑝 \land 𝑞)} \leftrightarrow \neg 𝑥_{𝑝 \land 𝑞}$
$𝑥_{𝑝 \land 𝑞} \leftrightarrow 𝑝 \land 𝑞$

We then transform these into CNF:

$\begin{aligned} (\neg 𝑥_{𝐹} \lor (𝑥_{\neg (𝑝 \land 𝑞)} \land 𝑟)) \land (\neg (𝑥_{\neg (𝑝 \land 𝑞)} \land 𝑟) \lor 𝑥_{𝐹}) \\ \equiv (\neg 𝑥_{𝐹} \lor 𝑥_{\neg (𝑝 \land 𝑞)}) \land (\neg 𝑥_{𝐹} \lor 𝑟) \land (\neg 𝑥_{\neg (𝑝 \land 𝑞)} \lor \neg 𝑟 \lor 𝑥_{𝐹}) \end{aligned}$
$(𝑥_{\neg (𝑝 \land 𝑞)} \to \neg 𝑥_{𝑝 \land 𝑞}) \land (\neg 𝑥_{𝑝 \land 𝑞} \to 𝑥_{\neg (𝑝 \land 𝑞)}) \equiv (\neg 𝑥_{\neg (𝑝 \land 𝑞)} \lor \neg 𝑥_{𝑝 \land 𝑞}) \land (𝑥_{𝑝 \land 𝑞} \lor 𝑥_{\neg (𝑝 \land 𝑞)})$
$\begin{aligned} (𝑥_{𝑝 \land 𝑞} \to (𝑝 \land 𝑞)) \land ((𝑝 \land 𝑞) \to 𝑥_{𝑝 \land 𝑞}) & \equiv (\neg 𝑥_{𝑝 \land 𝑞} \lor (𝑝 \land 𝑞)) \land (\neg (𝑝 \land 𝑞) \lor 𝑥_{𝑝 \land 𝑞}) \\ \equiv (\neg 𝑥_{𝑝 \land 𝑞} \lor 𝑝) \land (\neg 𝑥_{𝑝 \land 𝑞} \lor 𝑞) \land (\neg 𝑝 \lor \neg 𝑞 \lor 𝑥_{𝑝 \land 𝑞}) \end{aligned}$
and combine them all with $𝑥_{𝐹}$ to get:
$\begin{aligned} { \\ {𝑥_{𝐹}}, \\ {\neg 𝑥_{𝑝 \land 𝑞}, 𝑝}, {\neg 𝑥_{𝑝 \land 𝑞}, 𝑞}, {\neg 𝑝, \neg 𝑞, 𝑥_{𝑝 \land 𝑞}}, \\ {\neg 𝑥_{\neg (𝑝 \land 𝑞)}, \neg 𝑥_{𝑝 \land 𝑞}}, {𝑥_{𝑝 \land 𝑞}, 𝑥_{\neg 𝑝 \land 𝑞}}, \\ {\neg 𝑥_{𝑓}, 𝑥_{\neg (𝑝 \land 𝑞)}}, {\neg 𝑥_{𝐹}, 𝑟}, {\neg 𝑥_{\neg (𝑝 \land 𝑞)}, \neg 𝑟, 𝑥_{𝐹}} \\ } . \end{aligned}$

2.6. Natural deduction

Definition 2.6.1: The calculus of natural deduction has no axioms. Proofs begin by assumptions, and we use rules for Boolean connectives. A proof is a tree.

Temporary assumptions that are discharged are denoted by square brackets in the proof rules. If, at the end of a proof, all assumptions are discharged, the proof is valid.

Definition 2.6.2: The natural deduction rules are as follows:

Conjunction introduction:
Conjunction elimination:
Disjunction introduction:
Disjunction elimination:
This says that, in order to derive $𝐶$ from $𝐴 \lor 𝐵$ , it is sufficient to derive $𝐶$ from $𝐴$ and also $𝐶$ from $𝐵$ . Then both assumptions $[𝐴]$ and $[𝐵]$ are discharged. This is informally proof by cases.
Implication introduction:
Implication elimination:
Negation introduction:
Negation elimination:
Ex falso quodlibet:
Reductio ad absurdum:

Remark: Without

⊥

J or

⊥

K, natural deduction is equivalent to

𝐌_{0}

; with

⊥

J it is equivalent to

𝐉_{0}

; and with

⊥

K, it is equivalent to

𝐊_{0}

Definition 2.6.3: A deduction of a formula

𝐹

is a finite tree of formulae in which every leaf is an assumption, and every other formula is the conclusion of an application of one of the inference rules. The open assumptions of a deduction are those that are not discharged by any rule in the tree. A deduction of

𝐹

with no open assumptions is a proof of

𝐹

, and

𝐹

is a theorem if such a proof exists.

Remark: Natural deduction is sound and complete.

2.7. Sequent calculus

Definition 2.7.1: A sequent is an expression of the form

𝐴_{1}, \dots, 𝐴_{𝑛} ⟹ 𝐵_{1}, \dots, 𝐵_{𝑚},

where the $𝐴_{𝑖}$ s and $𝐵_{𝑖}$ s are propositional forumlae.

Such a sequent is valid if the following is valid in classical logic:

$𝐴_{1} \land \dots \land 𝐴_{𝑛} \to 𝐵_{1} \lor \dots \lor 𝐵_{𝑚}$ , if $𝑛, 𝑚 \neq 0$
$𝐵_{1} \lor \dots \lor 𝐵_{𝑚}$ , if $𝑛 = 0, 𝑚 \neq 0$
$\neg (𝐴_{1} \land \dots \land 𝐴_{𝑛})$ , if $𝑛 \neq 0, 𝑚 = 0$ ,
false otherwise.

The left-hand side of the sequent is the antecedent, and the right-hand side is the succedent.

Remark: The sequent with an empty antecedent and empty succedent is the empty sequent and is always invalid, by the last case in the definition above.

Remark:

𝐴 ⟹ 𝐴

is a tautology/axiom.

Remark: In declarations of sequent inference rules, we use the Greek letters

Γ, Δ, Σ, Π, Φ, Θ, Λ, Ξ

to denote (possibly empty) ordered lists of propositional formulae.

Definition 2.7.2: The inference rules of sequent calculus are either structural rules, which manipulate the list structure of a sequent, and operational rules, which provide rules for introducing logical connectives in the antecent or succedent. Inference rules take one or more premises from which a conclusion is drawn.

Definition 2.7.3: The structural rules are as follows:

Interchange allows consecutive formulae to be swapped, on both the left and right-hand sides:
Weakening allows formulae to be added to the left or right:
Contraction allows duplicate formulae to be merged:

Definition 2.7.4: The operational rules are as follows:

Conjunction:
Disjunction:
Conditional:
Negation:

Definition 2.7.5: A proof in the sequent calculus is a finite tree of sequents in which every leaf is an axiom ( $𝐴 \Rightarrow 𝐴$ ), and every other node is obtained from its children (where children are written above their parent) by an inference rule.

A sequent is provable or derivable if it is the root of such a proof.

Remark: To prove validity of $𝐹$ in the sequent calculus, we want to obtain an empty left-hand side, with $𝐹$ on the right:

Example: To prove that $(𝑝 \land 𝑞) \to 𝑝$ :

Example: To prove $(𝑝 \to 𝑞) \to (\neg 𝑞 \to \neg 𝑝)$

Theorem 2.7.6: The sequent calculus is a sound and complete proof system for classical logic.

2.8. The compactness theorem

Theorem 2.8.1 (compactness theorem):

A set of formulae $𝒮︀$ is satisfiable iff every finite subset of $𝒮︀$ is satisfiable.

Equivalently, a set of formulae $𝒮︀$ is unsatisfiable iff there is some unsatisfiable finite ${𝒮︀}^{'} \subseteq 𝒮︀$ .

Proof:

“ $⟹$ ”: Suppose that $𝒮︀$ is satisfiable, then there exists $𝒜︀$ s.t. $𝒜︀ ⊧ 𝐹$ for all $𝐹 \in 𝒮︀$ , hence $𝒜︀ ⊧ 𝐺$ for all $𝐺 \in {𝒮︀}^{'}$ for any finite subset ${𝒮︀}^{'} \subseteq 𝑆$ .

“ $⟸$ ”:

Define a partial assignment to be a function $𝒜︀ : 𝑋 \to {0, 1}$ , where $dom (𝒜︀) = {𝑥_{1}, \dots, 𝑥_{𝑛}}$ .

We say that a partial assignment $𝒜︀$ is good if $𝒜︀ ⊧ 𝐹$ for all $𝐹 \in 𝒮︀$ s.t. $𝐹$ only mentions the variables in $dom (𝒜︀)$ .

Suppose that every finite subset of $𝒮︀$ is satisfiable, then for every $𝑛$ , there is a partial assignment $𝒜︀$ s.t. $dom (𝒜︀) = {𝑥_{1}, \dots, 𝑥_{𝑛}}$ that is good:

Let ${𝒮︀}^{'} \in 𝑆$ be all formulae over $𝑥_{1}, \dots, 𝑥_{𝑛}$ .
${𝒮︀}^{'}$ might be infinite, but contains only finitely many formulae, up to logical equivalence.
Choose representatives for each equivalence class and put them in ${𝒮︀}^{″} \subseteq {𝒮︀}^{'}$ , ${𝒮︀}^{″}$ finite.
By assumption, there is some $𝒜︀$ such that $𝒜︀ ⊧ 𝐹$ for all $𝐹 \in {𝒮︀}^{″}$ . Moreover, $𝒜︀$ will satisfy every formula in ${𝒮︀}^{'}$ , because they are all logically equivalent to a formula in ${𝒮︀}^{″}$

Now we plan to construct a sequence ${𝒜︀}_{0}, {𝒜︀}_{1}, \dots$ of partial assignments that are good, and such that ${𝒜︀}_{𝑖 + 1}$ extends ${𝒜︀}_{𝑖}$ ; that is, $dom ({𝒜︀}_{𝑖}) \subseteq dom ({𝒜︀}_{𝑖 + 1})$ , and ${𝒜︀}_{𝑖} (𝑥_{𝑗}) = {𝒜︀}_{𝑖 + 1} (𝑥_{𝑗})$ for all $𝑥_{𝑗} \in dom ({𝒜︀}_{𝑖})$ .

We do this while maintaining the invariant that, for all $𝑛 \geq 0$ , there are infinitely many good extensions of ${𝒜︀}_{𝑛}$ .

We construct the ${𝒜︀}_{𝑛}$ s by induction on $𝑛$ .

The base case is clear: ${𝒜︀}_{0}$ is the empty assignment, which vacuously satisfies the empty subset of $𝒮︀$ , and there are clearly an infinite number of good assignments that extend the empty assignment, since every finite subset of $𝒮︀$ is satisfiable.

Then suppose we constructed ${𝒜︀}_{1}, \dots, {𝒜︀}_{𝑛}$ , and consider two assignments $ℬ︀, {ℬ︀}^{'}$ that extend ${𝒜︀}_{𝑛}$ , with $ℬ︀ (𝑥_{𝑛 + 1}) = 0, ℬ︀ (𝑥_{𝑛 + 1}) = 1$ . Since ${𝒜︀}_{𝑛}$ has infinitely many good extensions, one of $ℬ︀$ and ${ℬ︀}^{'}$ must have infinitely many good extensions. Pick the $ℬ︀$ or ${ℬ︀}^{'}$ that has infinitely many good extensions to be ${𝒜︀}_{𝑛 + 1}$ . Then by induction we have constructed our sequence ${𝒜︀}_{0}, \dots, {𝒜︀}_{𝑛}$ .

Now we take $𝒜︀$ such that $𝒜︀ (𝑥_{𝑖}) = {𝒜︀}_{𝑖} (𝑥_{𝑖})$ for all $𝑖 \geq 1$ . Then $𝒜︀ ⊧ 𝐹$ for all $𝐹 \in 𝒮︀$ , because we can take the largest index of a prop. var. that appears in $𝐹$ , and we know that $𝒜︀$ extends a model of $𝐹$ , so $𝒜︀ ⊧ 𝐹$ .

Example (an application of the compactness theorem):

Proposition: Let $𝐺 ≔ (𝑉, 𝐸)$ be a graph with $𝑉 = {𝑣_{𝑖} | 𝑖 \in ℕ}$ , and suppose that every finite subgraph of $𝐺$ is $𝑘$ -colourable, then $𝐺$ is $𝑘$ -colourable.

Proof: For every $𝑣 \in 𝑉$ , introduce a propositional variabel $𝑥_{𝑣, 𝑖}$ ( $𝑣$ has colour $𝑖$ ).

\begin{aligned} 𝐹_{𝑣} ≔ ⋁_{𝑖 = 1}^{𝑘} 𝑥_{𝑣, 𝑖} & \forall 𝑣 \in 𝑉 \\ 𝐺_{𝑣} ≔ ⋀_{𝑖 = 1}^{𝑘 - 1} ⋀_{𝑗 = 𝑖 + 1}^{𝑘} \neg (𝑥_{𝑣, 𝑖} \land 𝑥_{𝑣, 𝑗}) & \forall 𝑣 \in 𝑉 \\ 𝐻_{𝑢, 𝑣} ≔ ⋀_{𝑖 = 1}^{𝑘} \neg (𝑥_{𝑣, 𝑖} \land 𝑥_{𝑢, 𝑖}) & \forall (𝑢, 𝑣) \in 𝐸 \end{aligned}

Then let

𝒮︀ ≔ {𝐹_{𝑣}, 𝐺_{𝑣} | 𝑣 \in 𝑉} \cup {𝐻_{𝑢, 𝑣} | (𝑢, 𝑣) \in 𝐸},

and we claim that $𝒮︀$ is satisfiable iff $𝐺$ has a colouring (proof is easy).

Observe that any finite $𝑆^{'} \subseteq 𝑆$ “talks about” a finite subgraph of $𝐺$ ; by assumption, $𝑆^{'}$ is satisfiable. By the compactness theorem, $𝑆$ is satisfiable; therefore $𝐺$ is $𝑘$ -colourable.

3. 1st-order logic

3.1. Syntax

Definition 3.1.1: A signature, $𝜎$ , is a tuple of

constant symbols ( $𝑐, 𝑑$ )
function symbols ( $𝑓, 𝑔$ )
predicate symbols ( $𝑃, 𝑄, 𝑅$ )

with function and predicate symbols each having nonzero arity $𝑘$ .

We also keep a set of variables $𝑋 = {𝑥_{1}, 𝑥_{2}, \dots}$ , independently from the signature.

Definition 3.1.2: A $𝜎$ -term is defined by structural induction:

every $𝑥$ is a term
every $𝑐$ is a term
if $𝑡_{1}, \dots, 𝑡_{𝑘}$ are terms, then $𝑓 (𝑡_{1}, \dots, 𝑡_{𝑘})$ is a term (assuming $𝑓$ has arity $𝑘$ )
nothing else is a term

Definition 3.1.3: A formula of 1st-order logic over $𝜎$ is defined by structural induction.

$𝑃 (𝑡_{1}, \dots, 𝑡_{𝑘})$ is an atomic formula for a $𝑘$ -ary relation symbol $𝑃$ and terms $𝑡_{1}, \dots, 𝑡_{𝑘}$
If $𝐹, 𝐺$ are formulae, and $𝑥 \in 𝑋$ , then the following are formulae:
- $\neg 𝐹$ , $𝐹 \land 𝐺$ , $𝐹 \lor 𝐺$
- $\exists 𝑥 𝐹$ (existential quantifier)
- $\forall 𝑥 𝐹$ (universal quantifier)
Nothing else is a formula

Definition 3.1.4: For existential/universal quanitifiers $\exists 𝑥 𝐹$ / $\forall 𝑥 𝐹$ , we say that $𝐹$ is in the scope of $\exists 𝑥$ / $\forall 𝑥$ , and moreover $𝑥$ is bound by $\exists 𝑥$ / $\forall 𝑥$ .

If a variable is not bound, it is free.

A formula with no free variables is a sentence, or closed.

TODO quantifier depth

3.2. Semantics

Definition 3.2.1: A $𝜎$ -structure or $𝜎$ -assignment $𝒜︀$ is a tuple consisting of:

A non-empty universe ${𝒰︀}_{𝒜︀}$
For every $𝑘$ -ary function symbol $𝑓$ , a function $𝑓_{𝒜︀} : {𝒰︀}_{𝒜︀}^{𝑘} \to {𝒰︀}_{𝒜︀}$
For every $𝑘$ -ary predicate symbol $𝑃$ , a $𝑘$ -ary relation $𝑃_{𝒜︀} \subseteq {𝒰︀}_{𝒜︀}^{𝑘}$
For every constant $𝑐$ , a $𝑐_{𝒜︀} \in {𝒰︀}_{𝒜︀}$
For every variable $𝑥$ , a $𝑥_{𝒜︀} \in {𝒰︀}_{𝒜︀}$ .

Definition 3.2.2: For $𝜎$ -structure $𝒜︀$ and term $𝑡$ , we define the value of $𝑡$ under $𝒜︀$ by structural induction:

$𝒜︀ (𝑐) ≔ 𝑐_{𝒜︀} \in {𝒰︀}_{𝒜︀}$
$𝒜︀ (𝑥) ≔ 𝑥_{𝒜︀} \in {𝒰︀}_{𝒜︀}$
$𝒜︀ (𝑓 (𝑡_{1}, \dots, 𝑡_{𝑘})) ≔ 𝑓_{𝒜︀} (𝒜︀ (𝑡_{1}), \dots, 𝒜︀ (𝑡_{𝑘}))$

Definition 3.2.3: We define the satisfaction relation $𝒜︀ ⊧ 𝐹$ by structural induction:

$𝒜︀ ⊧ 𝑃 (𝑡_{1}, \dots, 𝑡_{𝑘})$ iff $(𝒜︀ (𝑡_{1}), \dots 𝒜︀ (𝑡_{𝑘})) \in 𝑃_{𝒜︀}$
$𝒜︀ ⊧ \neg 𝐹$ iff $𝒜︀ ⊧ 𝐹$
$𝒜︀ ⊧ 𝐹 \land 𝐺$ iff $𝒜︀ ⊧ 𝐹$ and $𝒜︀ ⊧ 𝐺$
$𝒜︀ ⊧ 𝐹 \lor 𝐺$ iff $𝒜︀ ⊧ 𝐹$ or $𝒜︀ ⊧ 𝐺$
$𝒜︀ ⊧ \exists 𝑥 𝐹$ iff there is $𝑎 \in {𝒰︀}_{𝒜︀}$ s.t. ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹$
$𝒜︀ ⊧ \forall 𝑥 𝐹$ iff for all $𝑎 \in {𝒰︀}_{𝒜︀}$ , ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹$

Definition 3.2.4: A 1st-order logic formula $𝐹$ is satisfiable if there is a $𝜎$ -structure $𝒜︀$ s.t. $𝒜︀ ⊧ 𝐹$ .

$𝐹$ is unsatisfiable if there is no such structure.

Definition 3.2.5: 1st-order logic formulae

𝐹, 𝐺

are equivalent (

𝐹 \equiv 𝐺

) if

𝒜︀ ⊧ 𝐹 \Leftrightarrow 𝒜︀ ⊧ 𝐺

for all

𝒜︀

Definition 3.2.6: 1st-order formulae are equisatisfiable if

𝐹

is satisfiable iff

𝐺

is satisfiable.

3.3. Equivalences & Skolem form

Definition 3.3.1: A formula

𝐺

is in Skolem form if

𝐺 = \forall 𝑥_{1} \forall 𝑥_{2} \dots \forall 𝑥_{𝑘} 𝐹

, where

𝐹

is quantifier-free.

Lemma 3.3.2 (Relevance Lemma): Let

𝐹

be a formula, and assignments

𝒜︀, {𝒜︀}^{'}

coinciding on their interpretation of constants, function symbols, predicate symbols and variables that are free in

𝐹

. Then

𝒜︀ ⊧ 𝐹

iff

{𝒜︀}^{'} ⊧ 𝐹

Remark: Propositional logic laws for logical equivalence still carry over, e.g. $(\neg 𝐹 \land 𝐺) \equiv \neg 𝐹 \lor \neg 𝐺$ .

Moreover, logical equivalence is still a congruence, e.g. $𝐹 \land 𝐺 \equiv 𝐹^{'} \land 𝐺^{'}$ iff $𝐹 \equiv 𝐹^{'}$ and $𝐺 \equiv 𝐺^{'}$ .

Also, if $𝐹 \equiv 𝐺$ , then $\forall 𝑥 𝐹 \equiv \forall 𝑥 𝐺$ , and $\exists 𝑥 𝐹 \equiv \exists 𝑥 𝐺$ .

Theorem 3.3.3:

Let $𝐹, 𝐺$ be formulae, then the following equivalences hold in 1st-order logic:

$\neg \forall 𝑥 𝐹 \equiv \exists 𝑥 \neg 𝐹$ , $\neg \exists 𝑥 𝐹 \equiv \forall 𝑥 \neg 𝐹$ (these allow us to establish a negation-normal form for 1st-order logic)
If $𝑥$ does not appear free in $𝐺$ , then
- $\forall 𝑥 𝐹 \land 𝐺 \equiv \forall 𝑥 (𝐹 \land 𝐺)$ , $\forall 𝑥 𝐹 \lor 𝐺 \equiv \forall 𝑥 (𝐹 \lor 𝐺)$
- $\exists 𝑥 𝐹 \land 𝐺 \equiv \exists 𝑥 (𝐹 \land 𝐺)$ , $\exists 𝑥 𝐹 \lor 𝐺 \equiv \exists 𝑥 (𝐹 \lor 𝐺)$
$\forall 𝑥 𝐹 \land \forall 𝑥 𝐺 \equiv \forall 𝑥 (𝐹 \land 𝐺)$ , $(\exists 𝑥 𝐹 \lor \exists 𝑥 𝐺) \equiv \exists 𝑥 (𝐹 \lor 𝐺)$
$\forall 𝑥 \forall 𝑦 𝐹 \equiv \forall 𝑦 \forall 𝑥 𝐹$ , $\exists 𝑥 \exists 𝑦 𝐹 \equiv \exists 𝑦 \exists 𝑥 𝐹$

Proof:

$𝐴 ⊧ \neg \forall 𝑥 𝐹$ iff $𝒜︀ ⊧ \forall 𝑥 𝐹$
iff ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹$ for some $𝑎 \in {𝒰︀}_{𝒜︀}$
iff ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ \neg 𝐹$ for some $𝑎 \in {𝒰︀}_{𝒜︀}$
iff $𝒜︀ ⊧ \exists 𝑥 \neg 𝐹$
and similar for the second equivalence.
$𝒜︀ ⊧ (\forall 𝑥 𝐹) \land 𝐺$ iff $𝒜︀ ⊧ \forall 𝑥 𝐹$ and $𝒜︀ ⊧ 𝐺$
iff, for all $𝑎 \in {𝒰︀}_{𝒜︀}$ , ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹$ and $𝒜︀ ⊧ 𝐺$
iff, for all $𝑎 \in {𝒰︀}_{𝒜︀}$ , ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹$ and ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐺$
(by the Relevance Lemma, since $𝑥$ does not appear free in $𝐺$ )
iff, for all $𝑎 \in {𝒰︀}_{𝒜︀}$ , ${𝒜︀}_{[𝑥 \mapsto 𝑎]} ⊧ 𝐹 \land 𝐺$
iff $𝒜︀ ⊧ \forall 𝑥 (𝐹 \land 𝐺)$
and similarly for the other equivalences.
TODO exercise
TODO exercise

Definition 3.3.4: A formula $𝐺$ is in prenex form if

𝐺 = 𝑄_{1} 𝑥_{1} \dots 𝑄_{𝑛} 𝑦_{𝑛} 𝐺^{'}, 𝑄_{𝑖} \in {\exists, \forall},

where $𝐺^{'}$ is quantifier-free.

Lemma 3.3.5: Any formula

𝐹

is equivalent to one in prenex form.

Definition 3.3.6: Let $𝐹$ be a formula, $𝑥$ a variable, and $𝑡$ a term, then $𝐹 [𝑡 / 𝑥]$ is a substitution obtained by replacing every free occurrence of $𝑥$ in $𝐹$ with $𝑡$ .

TODO define by structural induction.

Lemma 3.3.7 (translation-lemma): If $𝑡$ is a term and $𝐹$ a formula such that no variable in $𝑡$ occurs bound in $𝐹$ , then we have that $𝒜︀ ⊧ 𝐹 [𝑡 / 𝑥]$ iff ${𝒜︀}_{[𝑥 \mapsto 𝒜︀ (𝑡)]} ⊧ 𝐹$ .

Proof:TODO, optional

Lemma 3.3.8: Let $𝐹 = 𝑄 𝑥 𝐺$ with $𝑄$ a quantifier, and $𝑦$ a variable not occurring in $𝐺$ . Then $𝐹 \equiv 𝑄 𝑦 𝐺 [𝑦 / 𝑥]$ .

Proof:TODO

Definition 3.3.9: A formula is rectified if no variable occurs both bound and free at the same time, and all quantifiers refer to different variables.

Lemma 3.3.10: Every formula is equivalent to a rectified formula, and moreover one in rectified prenex form.

Proof: TODO by the lemmas above.

Lemma 3.3.11: Let $𝐹 = \forall 𝑦_{1} \forall 𝑦_{2} \dots \forall 𝑦_{𝑘} \exists 𝑧 𝐺$ where $𝐺$ is rectified. Let $𝑓$ be a fresh function symbol of arity $𝑘$ , then $𝐹$ is equisatisfiable with $𝐹^{'} ≔ \forall 𝑦_{1} \forall 𝑦_{2} \dots \forall 𝑦_{𝑘} 𝐺 [𝑓 (𝑦_{1}, \dots, 𝑦_{𝑘}) / 𝑧]$ .

Proof sketch: Suppose $𝒜︀ ⊧ 𝐹$ . We define ${𝒜︀}^{'}$ extending $𝒜︀$ such that $𝑓_{{𝒜︀}^{'}} (𝑎_{1}, \dots, 𝑎_{𝑘}) ≔ 𝑎$ , where $𝑎$ is such that ${𝒜︀}_{[𝑦_{1} \mapsto 𝑎_{1}] \dots [𝑦_{𝑘} \mapsto 𝑎_{𝑘}] [𝑥 \mapsto 𝑎]} ⊧ 𝐺$ .

Then ${𝒜︀}^{'} ⊧ 𝐹^{'}$ .

Remark: If

𝑘 = 0

, then

𝑓

is a constant symbol.

Theorem 3.3.12: Any 1st-order formula $𝐹$ is equisatisfiable with a formula in Skolem form.

Proof: We get

𝐹

in prenex form, and utilise Lemma 3.3.11 to eliminate existential quanitifiers from left to right.

Remark: The quantifier-free part of a Skolem-form formula is sometimes known as the matrix of the formula.

3.4. Herbrand’s Theorem & Ground Resolution

Definition 3.4.1: A ground term (of

𝜎

) is a variable-free term.

Definition 3.4.2: A $𝜎$ -structure $ℋ︀$ is a Herband structure if the following are true:

${𝒰︀}_{ℋ︀}$ is the set of ground terms
$𝑐_{ℋ︀} = 𝑐$ for every constant symbol $𝑐$
For every $𝑘$ -ary function symbol $𝑓$ and ground terms $𝑡_{1}, \dots, 𝑡_{𝑘}$ , $𝑓_{ℋ︀} (𝑡_{1}, \dots, 𝑡_{𝑘}) = 𝑓 (𝑡_{1}, \dots, 𝑡_{𝑘})$

Remark: The interpretations of constant and function symbols are just strings of symbols.

Remark: The only thing we are free to choose is the interpretation of predicate symbols.

Remark: The interpretation of a term in a Herbrand structure is

ℋ︀ (𝑡) = 𝑡

Corollary 3.4.3 (translation lemma for Herbrand structures):

$ℋ︀ ⊧ 𝐹 [𝑡 / 𝑥]$ iff ${ℋ︀}_{[𝑥 \mapsto 𝑡]} ⊧ 𝐹$ .

Theorem 3.4.4 (Herbrand's theorem): Let $𝐹 = \forall 𝑥_{1} \dots 𝑥_{𝑘} 𝐹^{*}$ be a closed formula in Skolem form. Then $𝐹$ is satisfiable iff $𝐹$ has a Herbrand model.

Proof:

“ $⟸$ ”: obvious.

“ $⟹$ ”: Suppose $𝒜︀ ⊧ 𝐹$ . We define $(𝑡_{1}, \dots, 𝑡_{𝑛}) \in 𝑃_{ℋ︀}$ iff $𝒜︀ ⊧ 𝑃 (𝑡_{1}, \dots, 𝑡_{𝑛})$ . Then we show that $ℋ︀$ is a model of $𝐹$ by induction on the number of quantifiers $𝑘$ .

If $𝑘 = 0$ , then $𝐹$ is a Boolean combination of atomic formulae $𝑃 (𝑡_{1}, \dots, 𝑡_{𝑛})$ for ground terms $𝑡_{1}, \dots, 𝑡_{𝑛}$ . By construction, $ℋ︀ ⊧ 𝑃 (𝑡_{1}, \dots, 𝑡_{𝑘})$ iff $𝒜︀ ⊧ 𝑃 (𝑡_{1}, \dots, 𝑡_{𝑘})$ , so $ℋ︀ ⊧ 𝐹$ , iff $𝒜︀ ⊧ 𝐹$ .

Then suppose true for Skolem-form sentences with $𝑘$ quantifiers, and consider $𝐹$ with $𝑘 + 1$ quantifiers, where $𝐹 = \forall 𝑥_{1} 𝐺$ . By the translation lemma, $𝒜︀ ⊧ 𝐺 [𝑡 / 𝑥_{1}]$ iff ${𝒜︀}_{[𝑥_{1} \mapsto 𝒜︀ (𝑡)]} ⊧ 𝐺$ . Hence $𝒜︀ ⊧ 𝐺 [𝑡 / 𝑥_{1}]$ for all ground terms $𝑡$ . $𝐺 [𝑡 / 𝑥_{1}]$ is closed, so by the i.h. $ℋ︀ ⊧ 𝐺 [𝑡 / 𝑥_{1}]$ for all ground terms $𝑡$ . By the translation lemma, ${𝒜︀}_{[𝑥_{1} \mapsto 𝑡]} ⊧ 𝐺$ for all $𝑡 \in {𝒰︀}_{ℋ︀}$ , hence $ℋ︀ ⊧ \forall 𝑥_{1} 𝐺$ , .

Corollary 3.4.5: For any formula with an uncountable model, there is a countable model.

Definition 3.4.6: Let $𝐹 = \forall 𝑥_{1} \dots \forall 𝑥_{𝑛} 𝐹^{*}$ be closed in Skolem form, and define the Herbrand expansion $𝐸 (𝐹)$ to be

𝐸 (𝐹) ≔ {𝐹^{*} [𝑡_{1} / 𝑥_{1}] \dots . [𝑡_{𝑛} / 𝑥_{𝑛}] | 𝑡_{1}, \dots 𝑡_{𝑛} are ground terms} .

Remark: Each formula in

𝐸 (𝐹)

is a Boolean combination of atomic formulae. This means that

𝐸 (𝐹)

has a Herbrand model iff it is propositionally satisfiable, i.e. there is an assignment to the set of closed atomic formulae that makes all formulae in

𝐸 (𝐹)

evaluate to true.

Theorem 3.4.7: A closed Skolem-form formula $𝐹 ≔ \forall 𝑥_{1} \dots \forall 𝑥_{𝑘} 𝐹^{*}$ is satisfiable iff $𝐸 (𝐹)$ is satisfiable when viewing atomic formulae as propositional variables.

Proof:

$𝐹$ sat. iff exists a Herbrand model $ℋ︀$ of $𝐹$ , by Herbrand’s Theorem
iff $ℋ︀ ⊧ 𝐹$
iff ${ℋ︀}_{([𝑥_{1} \mapsto 𝑡_{1}] \dots [𝑥_{𝑛} \mapsto 𝑡) 𝑛]}) ⊧ 𝐹^{*}$ for all ground terms $𝑡_{1}, \dots, 𝑡_{𝑛} \in {𝒰︀}_{ℋ︀}$
iff $ℋ︀ ⊧ 𝐹^{*} [𝑡_{1} / 𝑥_{1}] \dots [𝑡_{𝑛} / 𝑥_{𝑛}]$ , by the Translation Lemma for Herbrand structures
iff $ℋ︀ ⊧ 𝐸 (𝐹)$ by defn of Herbrand expansion
iff $𝐸 (𝐹)$ is satisfiable, by Herbrand’s Theorem.

Theorem 3.4.8 (Ground Resolution): A closed Skolem-form formula $𝐹$ is unsatisfiable iff there is a propositional resolution refutation of $𝐸 (𝐹)$ .

Proof: TODO

Remark:

To prove validity of $𝐹$ , we can provide a ground resolution refutation of $𝐺 ≔ \neg 𝐹$ .

Transform into negation normal form
Transform into rectified prenex form
Skolemise
Transform into CNF
Do a propositional resolution proof on the Herband expansion
If $□$ is derived, then $𝐺$ is unsatisfiable, so $𝐹$ is valid

Example:

Let $𝐹 = (\forall 𝑥 (𝑃 (𝑥) \to 𝑄 (𝑥)) \land \exists 𝑥 𝑃 (𝑥)) \to \exists 𝑥 𝑄 (𝑥)$ , $𝐺 ≔ \neg 𝐹$ .

\begin{aligned} 𝐺 & \equiv \forall 𝑥 (𝑃 (𝑥) \to 𝑄 (𝑥) \land \exists 𝑥 𝑃 (𝑥) \land \neg \exists 𝑥 𝑄 (𝑥) \\ \equiv \forall 𝑥 (\neg 𝑃 (𝑥) \land 𝑄 (𝑥)) \land \exists 𝑥 𝑃 (𝑥) \land \forall 𝑥 \neg 𝑄 (𝑥) \\ \equiv \forall 𝑥 (\neg 𝑃 (𝑥) \lor 𝑄 (𝑥)) \land \exists 𝑦 𝑃 (𝑦) \land \forall 𝑧 \neg 𝑄 (𝑧) \\ \equiv \forall 𝑥 \exists 𝑦 \forall 𝑧 ((\neg 𝑃 (𝑥) \lor 𝑄 (𝑥)) \land 𝑃 (𝑦) \land \neg 𝑄 (𝑧)) \\ equisat w/ \forall 𝑥 \forall 𝑧 ((\neg 𝑃 (𝑥) \lor 𝑄 (𝑥)) \land 𝑃 (𝑓 (𝑥)) \land \neg 𝑄 (𝑧)) ≕ 𝐻 \end{aligned}

Note that the set of ground terms is empty because there are no constant symbols. However, we can introduce a fresh constant symbol $𝑎$ , and now the set of ground terms is ${𝑎, 𝑓 (𝑎), 𝑓 (𝑓 (𝑎)), \dots}$ .

𝐸 (𝐻) = {\neg 𝑃 (𝐴) \lor 𝑄 (𝐴), 𝑃 (𝑓 (𝑎)), \neg 𝑄 (𝑎), \neg 𝑃 (𝑓 (𝑎)) \lor 𝑄 (𝑓 (𝑎)), \neg 𝑄 (𝑓 (𝑎)), \dots}

TODO resolution refutation

3.5. Natural deduction and sequent calculus in 1st-order logic

Definition 3.5.1: We introduce new natural deduction proof rules for quantifiers:

Universal elimination:
Universal introduction:
where $𝑐$ is free and must not occur in any undischarged assumption on which the deduction of $𝐴 (𝑐)$ relies.
Existential introduction:
Existential elimination:
provided that $𝑐$ does not occur in $𝐶$ , and all assumptions $[𝐴 (𝑐)]$ must be discharged when $\exists$ E is applied.

Example:

Definition 3.5.2: We extend the sequent calculus with new proof rules for quantifier.

Universal quantification:
where the exclamation mark (!) indicates that $𝑎$ must not occur in $Γ, Θ$ .
- Existential quantification:

Example:

TODO IMPORTANT: exercise 22 (ground resolution), 23 (natural deduction), 26 (sequent calculus)