数理逻辑导论 学习笔记

Intro

History

Reduction to Absurdity 归谬法:

• 从一个主张推出了矛盾，则这个主张是错的。

Syllogism 三段论:

• Major premise

• Minor premise

• Conclusion

The Validity of Reasoning:

• Truth for statements

• Validity for arguments / reasoning (推理过程)

Early Phase:

• Natural language is not reliable for logical reasoning.

• We need a “universal language”, “calculus of reasoning”

Development:

• Propositional Logic (PL, 命题逻辑)

• First-Order Logic (FOL, 一阶逻辑)

Introduction to Reasoning

Logic studies forms of reasoning.

Learning Goals:

• How do we express ambiguous natural language reasoing formally?

  Formal Language (形式语言).

• How do we prove that a reasoning is valid?

  Formal Deduction System (形式推演系统).

For PL and FOL:

• Modeling

• Syntax 语法

• Semantics 语义

• Deduction 推理

---

Prerequisite Knowledge

Set

Definition:

• Extension (外延): define by listing all elements.

• Intension (内涵): define by common characteristics.

  If $\varphi(x)$ represents a property (common characteristics), then $\{x \mid \varphi(x)\}$ denotes the set of all elements that have this property.

Axiom (公理) of Extension:

• Two sets are equal if and only if they have the same members.

Subset: $\subseteq$

Proper Subset 真子集: $\subset$

Power Set 幂集:

• The set of all subsets of $A$, i.e., $\mathcal P(A)$.

Set Operations:

• Union: $A \cup B = \{x \mid x \in A \lor x \in B\}$.

• Intersection: $A \cap B = \{x \mid x \in A \land x \in B\}$.

• Difference: $A - B = \{x \mid x \in A \land x \not\in B\}$.

Relation

$n$-tuples 有序 $n$ 元组: $\langle 1, 2, 3, 2 \rangle$

Binary Relation 二元关系:

• Cartesian Product (笛卡尔积): $A \times B = \{\langle x, y \rangle \mid x \in A \land y \in B\}$.
• A Binary relation $R$ over sets $X$ and $Y$ is a subset of Cartesian product $A \times B$, denoted as $R \subseteq A \times B$.
• $\langle x, y \rangle \in R$ reads “$x$ is $R$-related to $y$”, and is denoted by $R(x, y)$ or $xRy$.
• Let’s define $X = \{x \mid \langle x, y \rangle \in R\}$，$Y = \{y \mid \langle x, y \rangle \in R\}$. When $X = Y$, we call $R$ is a relation over $X$.

$n$-ary Relation:

• Cartesian product of sets $A_1, A_2, \cdots, A_n$: $A_1 \times A_2 \times \cdots \times A_n = \{\langle x_1, x_2, \cdots, x_n \rangle \mid x_1 \in A_1, x_2 \in A_2, \cdots, x_n \in A_n\}$.

• Denoted as $A^n$ if $A_1 = A_2 = \cdots = A_n = A$.

• If $R \subseteq A^n$, $R$ is denoted as an $n$-ary relation over $A$.

We also have Unary Relation (一元关系), Ternary Relation(三元关系), etc.

Equivalence Relation 等价关系:

• Reflexive (自反): $\forall x \in A$, $xRx$.

• Sysmmetric (对称): $\forall x \in A$, if $xRy$, then $yRx$.

• Transitive (传递): $\forall x, y, z \in A$, if $xRy$ and $yRz$, then $xRz$.

• A binary relation $R$ on a nonempty set $A$ is an equivalence relation if and only if $R$ is reflexive, sysmmetric and transitive.

Equivalence Class 等价类:

• $[x]_R = \{y \in A \mid xRy\}$ is the set of all elements of $A$ that are equivalent to $x$. ($R$ is an equivalence relation over a set $A$)

• Every element belongs to exactly one equivalence class.

• Different equivalence classes are disjoint.

• The set of all equivalence classes forms a partition of $A$.

Partial Order Relation 偏序关系:

• Antisymmetric (反对称): $\forall x, y \in A$, if $xRy$ and $yRx$, then $x = y$.

• A binary relation $R$ on a nonempty set $A$ is a partial order if and only if $R$ is reflexive, antisysmmetric and transitive.

• Minimal Element: For $x \in A$, no $y \in A$ that satisfys $yRx$ exists.

• Maximal Element: For $x \in A$, no $y \in A$ that satisfys $xRy$ exists.

Total Order Relation 全序关系 / Linear Order Relation:

• A partial order relation $R$ on a set $A$ is a total order (linear order), iff $\forall x, y \in A$, either $xRy$ or $yRx$.

• Intuitively, ant two elements are comparable.

Mathematical structures are defined with sets, plus various relations (e.g., $<$) and functions (e.g., $+$).

Function

Definition:

• 每个 $x \in X$ 都能找到唯一一个确定的 $y \in Y$ 与之对应。

Denoted by $f: A \to B$. We use $f(x) = y$ to denote $\langle x, y \rangle \in f$.

• Domain: the set of input values.

• Codomain (陪域, 上域): the set of possible output values.

• Range (值域): the set of actual output values, i.e., a subset of the $B$.

$n$-ary Function:

• The domain of $f$ is the Cartesian product $A_1 \times A_2 \times \cdots \times A_n$.

• An $n$-ary function maps ordered $n$-tuples from its domain to elements in its codomain.

• $f : A^n \to A$ is called an $n$-ary function in $A$.

Injective, Surjective & Bijective:

• Injective (one-to-one, 单射): Each element of the codomain is mapped to by at most one element of the domain.

• Surjective (onto, 满射): Each element of the codomain is mapped to by at least one element of the domain.

• Bijective (one-to-one correspondence, 双射): Each element of the codomain is mapped to by exactly one element of the domain. (both injective and surjective)

Mathematical Definitons & Proof

Inductive Definition 归纳定义:

• Definition of the set $\N$ of natural numbers:

  • $0 \in \N$.

  • $\forall n \in \N$, $n + 1 \in \N$.

  • Only $n$ generated by (finite iterations of) the previous two steps, $n \in \N$.

• The above definition can be equivalently stated as:

  $\N$ is the smallest inductive subset of $S$ that satisfies:

  • $0 \in S$.

  • $\forall n \in S$, $n + 1 \in S$.

• Let $P$ be a property, and $P(x)$ denotes that $x$ has property $P$. If

  • $P(0)$.

  • $\forall n \in S$, if $P(n)$, then $P(n')$ ($n'$ is the successor of $n$)

  Then, for any $n \in S$, $P(n)$.

Proof by Induction 归纳证明:

• Base Case: We need to show that $P(n)$ is true for the smallest possible value of $n$. e.g., $P(n_0)$ is true.

• Inductive Hypothesis: Assume that the statement $P(k)$ is true for any positive integer $k \ge n_0$.

• Inductive Step: Show that the statement $P(k + 1)$ is true.

Recursive Definition 递归定义:

• $\forall n \in \N$, the value of $f(n)$ can be computed from the above definition using $f(0), f(1), \cdots, f(n − 1)$.

Proof by Contradiction

---

Propositional Logic

Propositions & Connectives & Language in General

Proposition 命题:

• Proposition: A proposition is a declarative sentence that can be judged as either true or false.

  e.g., $2 + 2 = 5$ is a proposition, while $x + y < 0$ is not a proposition.

• Atomic Proposition (原子命题): A proposition that does not contain any smaller part that is still a proposition is called an atomic proposition.

• Compound Proposition (复合命题): A proposition that involves the assembly of multiple propositions is called a compound proposition.

Logical Connectives:

Connectives	Read as	名称	Term
$\land$	and	合取	conjunction
$\lor$	or	析取	disjunction
$\neg$	not	否定	negation
$\to$	if…then…	蕴含	implication
$\leftrightarrow$	if and only if	等价	equivalence

Language Components:

• Alphabet

• Syntax (语法)

• Semantics (语义)

Syntax

Alphabet:

• Atomic Proposition (Atom): $p, q, r, \cdots, p_1, r_2, \cdots$

• Logic Connectives: $\land, \lor, \neg, \to, \leftrightarrow$

• Punctuation: opening and closing brackets

Expressions:

• Expressions are finite strings of symbols.

• The length is the number of occurrences of symbols in it.

• Order matters.

Well-Formed Formulas (WFF):

• Every atom is a WFF.

• If $\alpha$ is a WFF, then so is $(\neg \alpha)$.

• If $\alpha$ and $\beta$ are WFF, then so are $(\alpha \land \beta), (\alpha \lor \beta), (\alpha \to \beta), (\alpha \leftrightarrow \beta)$.

• Nothing else is a WFF.

e.g., $(p)$ is not a WFF.

Formulas:

• $\text{Atom}\left(\mathscr{L}^P\right)$: the set of expressions of $\mathscr{L}^P$ consisting of an atom proposition symbol only.

• $\text{Form}\left(\mathscr{L}^P\right)$: is the smallest set of expressions that satisfies:

  • $\text{Atom}\left(\mathscr{L}^P\right) \subseteq \text{Form}\left(\mathscr{L}^P\right)$.

  • If $\alpha \in \text{Form}\left(\mathscr{L}^P\right)$， then $(\neg \alpha) \in \text{Form}\left(\mathscr{L}^P\right)$.

  • If $\alpha, \beta \in \text{Form}\left(\mathscr{L}^P\right)$, then $(\alpha \land \beta), (\alpha \lor \beta), (\alpha \to \beta)$, $(\alpha \leftrightarrow \beta) \in \text{Form}\left(\mathscr{L}^P\right)$.

Some Definitions:

• Segment (段, 子串): $v$ is a segment of $u$ if $u = w_1 v w_2$.

• Proper Segment (真子段): $v$ is a segment of $u$ and $u \ne v$.

• Initial Segment / Prefix: $u = vw$, $v$ is an initial segment of $u$. If $w$ is non-empty, $v$ is a proper prefix of $u$.

• Terminal Segment / Suffix: $u = vw$, $w$ is a terminal segment of $u$. If $v$ is non-empty, $v$ is a proper suffix of $u$.

Common Properties of WFF:

• WFFs in $\mathscr{L}^P$ are non-empty expressions.

• Every WFF in $\mathscr{L}^P$ has an equal number of opening and closing brackets.

• Every proper prefix of WFF in $\mathscr{L}^P$ has more opening brackets than closing brackets. Every proper suffix of WFF in $\mathscr{L}^P$ has more closing brackets than opening brackets.

  Hence, proper prefix and proper suffix are not WFF in $\mathscr{L}^P$.

Parse Tree 解析树:

• Definition:

  • The root is the formula.

  • Leaves are atoms.

  • Each internal node is formed by applying some formation rule on its children.

• WFF $\leftrightarrow$ a parse tree of it.

• Subformula: If $G$ occurs within $F$, then $G$ is a subformula of $F$.

  Proper Subformula: $G \ne F$.

• Immediate Subformula: The children of a formula in its parse tree.

  Leading Connective: The connective that is used to join children.

Unique Readability Theorem:

• There is a unique way to construct every WFF.

Simplification:

• Convention (公约): We may drop the outermost parentheses, i.e., $F$ is the same as $(F)$.

• Precedence (优先级):

  • Parentheses take the highest precedence.

  • From highest to lowest: $\neg, \land, \lor, \to, \leftrightarrow$.

  • First group the rightmost occurrence. e.g., $p \to q \to r$ means $p \to (q \to r)$.

Semantics

Truth Value:

• There are only $2$ truth values of propositions: True ($1$) or False ($0$).

• Truth Table of $\neg, \land, \lor$.

• Truth Table for $p \to q$: (maybe $p \le q$?)

  $p$	$q$	$p\to q$
  $0$	$0$	$1$
  $0$	$1$	$1$
  $1$	$0$	$0$
  $1$	$1$	$1$

• Truth Table for $p \leftrightarrow q$: (maybe $p = q$?)

  $p$	$q$	$p\leftrightarrow q$
  $0$	$0$	$1$
  $0$	$1$	$0$
  $1$	$0$	$0$
  $1$	$1$	$1$

Truth Valuation / Assignment:

• Definition: a function $v: \text{Atom}(\mathscr{L}^P) \to \{0, 1\}$.

  We use $v(p)$ or $p^v$ to denote the truth value of $p$.

• Theorem: Fix a truth valuation $v$. Every formula $\alpha \in \text{From}(\mathscr{L}^P)$ has a value $\alpha^v \in \{0, 1\}$.

• Tautology (永真式 / 重言式): $\forall v$, $A^v = 1$.

  Contradiction (永假式 / 矛盾式): $\forall v$, $A^v = 0$.

  Satisfiable: $\exists v$, $A^v = 1$.

Valuation Tree:

Logical Equivalence:

• Definition: Two formulas $A$ and $B$ are logically equivalent iff they have the same value under any valuation.

  i.e., $A$ and $B$ have the same final column in their truth tables.

  i.e., $A \leftrightarrow B$ is a tautology.

• It’s an equivalence relation on $\text{Form}(\mathscr{L}^P)$.

Logical Identities:

• Identity Laws (恒等率): $p \land T \equiv p$, $p \lor F \equiv p$.

• Domination Laws (支配律): $p \land F \equiv F$, $p \lor T \equiv T$.

• Idempotent Laws (幂等率) : $p \land p \equiv p$, $p \lor p \equiv p$.

• Double Negation Laws (双非率): $\neg (\neg p) \equiv p$.

• Commutative Laws (交换律)

• Associative Laws (结合律): $(p \land q) \land r \equiv p \land (q \land r)$, $(p \lor q) \lor r \equiv p \lor (q \lor r)$.

• Distributive Laws (分配率): $p \lor (q \land r) \equiv (p \lor q) \land (p \lor r)$, $p \land (q \lor r) \equiv (p \land q) \lor (p \land r)$.

• De Morgan’s Laws (德摩根率): $\neg (p \land q) \equiv \neg p \lor \neg q$, $\neg (p \lor q) \equiv \neg p \land \neg q$.

• Absorption Laws (吸收率): $p \lor (p \land q) \equiv p$, $p \land (p \lor q) \equiv p$.

• Negation Laws (否定率): $p \land \neg p \equiv F$, $p \lor \neg p \equiv T$.

• Implication: $p \to q \equiv \neg p \lor q$.

• Contrapositive (逆否): $p \to q \equiv \neg q \to \neg p$.

• Equivalence: $p \leftrightarrow q \equiv (p \to q) \land (q \to p)$.

Substitution:

• e.g., $(r \to s) \land (t \to s)$ is a substitution instance of $p \land q$.

  e.g., $(p \leftrightarrow p) \leftrightarrow (p \leftrightarrow p)$ is a substitution instance of $p \leftrightarrow p$.

• Theorem: If $B$ is a substitution instance of a tautology $A$, then $B$ is again a tautology.

• Substitution Theorem: Substitute $C$ in $A$ by $D$ ($C \equiv D$) to get $B$, then $A \equiv B$. (all WFF)

Semantic Entailment

Set of Formulas & its Satisfiability

• Definition: Let $\Sigma \subseteq \text{Form}(\mathscr{L}^P)$. Define:

  $$\Sigma^v = \begin{cases} 1 & \forall B \in \Sigma, B^v = 1 \\ 0 & \text{otherwise} \end{cases}$$

• Satisfiable: $\Sigma$ is satisfiable iff $\exists v$, $\Sigma^v = 1$. And we say $v$ satisfies $\Sigma$.

Entailment / Consequence:

• Definition: We say:

  • $A$ is a logical consequence (逻辑推论) of $\Sigma$, or

  • $\Sigma$ (semantically) entails (逻辑蕴含) $A$, or

  • $\Sigma \models A$,

  iff $\forall v$, if $\Sigma^v = 1$, then $A^v = 1$.

• Proof:

  • Direct proof

  • Using a truth table

  • Proof by contradiction

• Properties:

  • $A \equiv B$ iff both $A \models B$ and $B \models A$.

  • $\varnothing \models A$ iff $A$ is a tautology.

  • $A \models B$ iff $A \to B$ is a tautology.

  • $\{A_1, \cdots, A_n\} \models A$ iff $\varnothing \models (A_1 \land \cdots \land A_n \to A)$.

$n$-ary Boolean Functions:

• Definition: An $n$-ary boolean function takes $n$ boolean inputs and returns a single boolean output.

• There are $2^{2^n}$ different $n$-ary boolean functions.

• Notation: $fA_1A_2\cdots$

More Binary Connectives:

• Joint Denial (或非词): neither…nor…, denoted by $p \downarrow q \equiv \neg(p \lor q)$.

• Alternative Denial (与非词): not both…, denoted by $p \uparrow q \equiv \neg(p \land q)$.

• Exclusive Disjunction (异或词): either…or…, denoted by $p \otimes q \equiv \neg (p \leftrightarrow q)$.

Adequate Set:

• Redundancy (累赘): $\to$ is said to be definable in terms of $\neg$ and $\lor$, because $(p \to q) \equiv ((\neg p) \lor q)$.

• Definition: Every WFF is logically equivalent to a WFF using only connectives from an adequate (完备的) set.

• Theorem 1: $\{\neg, \land, \lor\}$ is adequate.

  Theorem 2: Each of the sets $\{\neg, \land\}$, $\{\neg, \lor\}$, $\{\neg, \to\}$ is adequate.

• Claim: Every $n$-ary boolean function is definable in terms of only connectives from an adequate set.

Proof Systems

A formal proof is syntatic (语法上的), rather than semantic (语义上的).

Definition & Notation:

• Definition: A formal proof system (deductive system, 形式推演系统) consists of the language part and the inference part.

• Notation: $\Sigma \vdash A$ means that there is a proof premises (前提) $\Sigma$ and conclusion $A$.

Types:

• Hilbert-style System

• Natural Deduction System

• Resolution

Key Properties:

• Soundness (可靠性): If $\Sigma \vdash A$, then $\Sigma \models A$.

• Completioness (完备性): If $\Sigma \models A$, then $\Sigma \vdash A$.

Hilbert-style Proof System

Language:

• Alphabet: $(, ), \neg, \to, p, q, r, \cdots$

• Formulas: WFF (connectives only $\neg$ and $\to$)

Axioms 公理:

• $A_1 : A \to (B \to A)$

• $A_2 : (A \to (B \to C)) \to ((A \to B) \to (A \to C))$

• $A_3 : (\neg A \to \neg B) \to (B \to A)$

Inference Rule:

• Modus Ponens (MP, 分离规则): $A$ and $A \to B$ imply $B$.

  $$r_{mp} : \frac{A, A \to B}{B}$$

Formal Proof:

• Definition: A proof of formula $A$ is a finite sequence of formulas $A_1, A_2, \cdots, A_n$ such that $\forall i \le n$, $A_i$ is either

  • an axiom in $\mathscr{H}$, or

  • $A_j$ ($j < i$), or

  • derived from $A_j, A_k$ ($j, k < i$) by the MP rule.

  $A$ is provable, denoted by $\vdash A$.

• Theorem H1: $\vdash A \to A$.

  

• Soundness (可靠性): If $\vdash \alpha$, then $\models \alpha$, which means $\alpha$ is a tautology.

Proof from Assumptions:

• Definition: $A_i$ can also be a formula in $\Sigma$.

  If $\Sigma = \varnothing$, then $\Sigma \vdash A$ is simply $\vdash A$.

• Theorem 6.2: Monotonicity (单调性): If $\Sigma \vdash A$ and $\Sigma \subseteq \Sigma'$, then $\Sigma' \vdash A$.

Derived Rules:

• Deduction Rule: $\Sigma \cup \{A\} \vdash B$ iff $\Sigma \vdash A \to B$.

  Theorem H2: $\vdash (A \to B) \to ((B \to C) \to (A \to C))$.

• Contrapositive Rule: $\Sigma \vdash \neg B \to \neg A$ iff $\Sigma \vdash A \to B$.

  Theorem H3: $\vdash \neg \neg A \to A$.

• Transitivity Rule: If $\Sigma \vdash A \to B$ and $\Sigma \vdash B \to C$, then $\Sigma \vdash A \to C$.

• Exchange of Antecedent Rule: If $\Sigma \vdash A \to (B \to C)$, then $\Sigma \vdash B \to (A \to C)$.

  Theorem H4: $\vdash \neg A \to (A \to B)$ and $\vdash A \to (\neg A \to B)$.

• Double Negation Rule: $\Sigma \vdash A$ iff $\Sigma \vdash \neg \neg A$.

  Theorem H5: $\vdash \text{true}$ and $\vdash \neg \text{false}$ (introduced as derived concepts just for convenience)

• Ratio ad Adsurdum: If $\Sigma \vdash \neg A \to \text{false}$, then $\Sigma \vdash A$.

  Theorem H6: $\vdash (A \to \neg A) \to \neg A$.

Natural Deduction Proof System

Language:

• Alphabet: $(, ), \neg, \land, \lor, \to, \leftrightarrow, p, q, r, \cdots$

• Formulas: WFF

Inference Rules:

• Reflexivity (Premise): $\Sigma, \alpha \vdash \alpha$.

• $\land$-introduction & $\land$-elimination:

  $$\frac{\alpha \quad \beta}{(\alpha \land \beta)} \quad \quad \frac{(\alpha \land \beta)}{\alpha}, \frac{(\alpha \land \beta)}{\beta}$$

• $\to$-introduction & $\to$-elimination:

  $$\frac{\boxed{\begin{array}{c} \alpha \\ \vdots \\ \beta \end{array}}}{(\alpha \to \beta)} \quad \quad \frac{(\alpha \to \beta) \quad \alpha}{\beta}$$

  This box denotes a sub-proof. Assumptions inside a sub-proof cannot be used outside. e.g.:

  

• $\lor$-introduction & $\lor$-elimination:

  $$\frac{\alpha}{(\alpha \lor \beta)}, \frac{\alpha}{(\beta \lor \alpha)} \quad \quad \frac{(\alpha_1 \lor \alpha_2) \quad \boxed{\begin{array}{c} \alpha_1 \\ \vdots \\ \beta \end{array}} \quad \boxed{\begin{array}{c} \alpha_2 \\ \vdots \\ \beta \end{array}}}{\beta}$$

• $\neg$-introduction & $\neg$-elimination:

  $$\frac{\boxed{\begin{array}{c} \alpha \\ \vdots \\ \bot \end{array}}}{(\neg \alpha)} \quad \quad \frac{\alpha \quad (\neg \alpha)}{\bot}$$

  where $\bot$ represents any contradiction.

• $\neg \neg$-elimination:

  $$\frac{(\neg (\neg \alpha))}{\alpha}$$

Derived Rules:

• Contradiction Elimination:

  $$\frac{\bot}{\alpha}$$

• Modus Tollens (MT, 否定后件):

  $$\frac{(p \to q) \quad (\neg q)}{\neg p}$$

• $\neg \neg$-introduction:

  $$\frac{\alpha}{(\neg (\neg \alpha))}$$

• Proof by Contradiction (PBC):

  $$\frac{\boxed{\begin{array}{c} (\neg \alpha) \\ \vdots \\ \bot \end{array}}}{\alpha}$$

• Law of Excluded Middle (tertiam non datur, LEM, 排中律):

  $$\frac{}{(\alpha \lor (\neg \alpha))}$$

Soundness & Completeness:

• Soundness (可靠性): If $\Sigma \vdash \alpha$, then $\Sigma \models \alpha$.

• Completeness (完备性): If $\Sigma \models \alpha$, then $\Sigma \vdash \alpha$.

• The natrual deduction proof system is sound and complete.

Resolution Proof System

aka. Refutation (反驳) System.

Normal Form:

• This is a standardized representation of logical formulas.

• Literal (单式, 文字): An atomic formula of the negation of that.

• Conjunctive Clause (合取子句): A conjuction of literals.

  Disjunctive Clause (析取子句): A disjuction of literals.

• Conjunctive Normal Form (CNF, 合取范式): A conjuction of disjunctive clauses.

  $$(a \lor \cdots \lor b) \land \cdots \land (c \lor \cdots \lor d)$$

  Disjunctive Normal Form (DNF, 析取范式): A disjunction of conjunctive clauses.

  $$(a \land \cdots \land b) \lor \cdots \lor (c \land \cdots \land d)$$

Properties:

• If $A$ is a formula in CNF, then $\neg A$ is logically equivalent to a formula in DNF.

  If $A$ is a formula in DNF, then $\neg A$ is logically equivalent to a formula in CNF.

• Every formula $A \in \text{Form}\left(\mathscr{L}^P\right)$ is logically equivalent to some formula in CNF and DNF.

• Principal CNF / DNF: Each clause in a principal CNF / DNF contains all propositional variables exactly once, and no two clauses are the same. e.g., $(p \lor \neg q \lor r) \land (p \lor q \lor \neg r)$.

Resolution proof system applies only to formulas in CNF. It is used to prove contradictions ($\bot$).

Inference Rule:

• Resolution Inference Rule:

  $$\frac{(\alpha \lor p) \quad ((\neg p) \lor \beta)}{(\alpha \lor \beta)}$$

  Each step of the proof produces one clause (Resolvent, 消解子句) from two previous clauses by applying the resolution rule.

  Special cases:

  • Unit Resolution: $\dfrac{(\alpha \lor p) \quad (\neg p)}{\alpha}$

  • Contradiction: $\dfrac{p \quad (\neg p)}{\bot}$

Proof Procedure:

• To prove $\Sigma \vdash \varphi$, we prove $\Sigma \cup \{\neg \varphi\} \vdash \bot$ instead.

• First, convert each formula in $\Sigma$ and $\neg \varphi$ to CNF.

• Next, split CNF formulas at the $\land$s.

  • A CNF can be split to a set of disjunctive clauses. e.g., $(p \lor q) \land (q \lor \neg r) \land s$ can be split to $\{p, q\}, \{q, \neg r\}, \{s\}$.

  • We treat $\bot$ as a clause containing no literal, i.e., the empty set $\varnothing$. Since it contains no true literal, it is false.

• Then, keep applying the resolution inference rule until either:

  • we have the empty clause $\bot$, which means we have proved that $\Sigma \vdash \varphi$, or

  • the rule can no longer be appiled to give a new formula, which means $\varphi$ cannot be proven from $\Sigma$.

Soundness & Completeness:

• The resolution proof system is sound and complete.

---

First-Order Logic

aka. Predicate Logic.

Basic Concepts of FOL:

• Domain (论域): A non-empty set of objects.

• Constants: Specific, concrete, individual objects in the domain.

• Variables

• Predicates (谓词): A predicate represents:

  • a property of a individual object in the domain, or

  • a relationship among multiple individuals.

• Quantifiers (量词):

  • Universal Quantifier $\forall$ (全称量词)

  • Existential Quantifier $\exists$ (存在量词)

  Propositions:

  • Universal Proposition (全称命题): $\forall xP(x)$.

  • Existentail Proposition (存在命题): $\exists xP(x)$.

• Functions: A function with $n$ arity (元数) is denoted as $f^{n}$.

Syntax

Alphabet:

• Non-Logical Symbols:

  • Constant Symbols (个体常元): $c_1, c_2, c_3, \cdots$

  • Predicates: $P, Q, P_1, P_2^1, Q_1^2, \cdots$

  • Function Symbols (函词): $f, g, f_1, f_2^1, g_1^2, \cdots$

• Logical Symbols:

  • Quantifiers: $\forall, \exists$

  • Variables (个体变元): $x, y, z, x_1, x_2, y_1, \cdots$

  • Connectives: $\neg, \land, \lor, \to, \leftrightarrow$

  • Punctuation: $(, )$ & comma

  • Equality (a special binary relation): $=$

Formulas:

• $\text{Term}(\mathscr{L})$ includes:

  • Constant Symbols $c$, or

  • Variables $x$, or

  • Function Symbols $f^n(t_1, t_2, \cdots, t_n)$, where $t_1, t_2, \cdots t_n \in \text{Term}(\mathscr{L})$.

• $\text{Atom}(\mathscr{L})$ includes:

  • $P(t_1, t_2, \cdots, t_n)$, where $t_1, t_2, \cdots t_n \in \text{Term}(\mathscr{L})$.

  • $= (t_1, t_2)$ (also denoted as $t_1 = t_2$), where $t_1, t_2 \in \text{Term}(\mathscr{L})$.

• $\text{Form}(\mathscr{L})$ can be generated by:

  • $\text{Atom}(\mathscr{L}) \subseteq \text{Form}(\mathscr{L})$.

  • If $\alpha \in \text{Form}(\mathscr{L})$, then $(\neg \alpha) \in \text{Form}(\mathscr{L})$.

  • If $\alpha, \beta \in \text{Form}(\mathscr{L})$, then $(\alpha * \beta) \in \text{Form}(\mathscr{L})$, where $*$ representes $\land, \lor, \to, \leftrightarrow$.

  • If $\alpha \in \text{Form}(\mathscr{L})$ and $x$ is a variable, then $(\forall x \alpha), (\exists x \alpha) \in \text{Form}(\mathscr{L})$.

  Conventions: Parentheses can be omitted as in PL. Parentheses around quantifiers can be also omitted.

  Precedence: $\forall$ and $\exists$ have the same precedence level as $\neg$, which are higer than all binary connectives.

Parse Tree:

• Similar to that in PL.

Semantics

Scope of Variables:

• The formula adjacent to the quantifier.

Types of Variables:

• Free Variables: $x$ is not within the scope of a quantified variable $x$.

  Bound Variables: The occurrence of $x$ is lies in the scope of some quantifier of $x$.

• An occurrence of $x$ is free if it is a leaf node in the parse tree such that there is no path upwards from that node $x$ to a node $\forall x$ or $\exists x$.

Sentences / Closed Formula:

• Formulas with no free variables.

Interpretation / Structure $\mathcal{I}$:

An interpreattion consists of:

• Domain / Universe: A domain $D$, which must be a non-empty set.

• Every constant / function / predicate is something of $\mathcal{I}$.

Environment $E$:

• Assigns a value in the domain to every variable symbol in the language. (similar to assignment in PL)

Values:

• $\forall t \in \text{Term}(\mathscr{L})$, its value $t^{(\mathcal{I}, E)}$ is

  • $c^{\mathcal{I}}$, if $t$ is a constant $c$; or

  • $x^E$, if $t$ is a variable $x$; or

  • $f^{\mathcal{I}}\left(t_1^{(\mathcal{I}, E)}, \cdots, t_n^{(\mathcal{I}, E)}\right)$, if $t$ is a function $f(t_1, \cdots, t_n)$.

• $\forall P \in \text{Atom}(\mathscr{L})$,

  • $P(t_1, \cdots, t_n)^{(\mathcal{I}, E)} = P^{\mathcal{I}}\left(t_1^{(\mathcal{I}, E)}, \cdots, t_n^{(\mathcal{I}, E)}\right)$;

  • $(t_1 = t_2)^{(\mathcal{I}, E)} = 1$ iff $t_1^{(\mathcal{I}, E)} = t_n^{(\mathcal{I}, E)}$.

• $\forall \varphi \in \text{Form}(\mathscr{L})$, its truth value…

Logical Equivalence:

• Duality (二元性): $\neg \forall x A(x) \equiv \exists x \neg A(x)$, $\neg \exists x A(x) \equiv \forall x \neg A(x)$.

• Substitution: logical equivalence in PL still hold.

• Commutativity: $\forall x \forall y A(x, y) \equiv \forall y \forall x A(x, y)$, $\exists x \exists y A(x, y) \equiv \exists y \exists x A(x, y)$.

• Distributivity: $\forall x (A(x) \land B(x)) \equiv \forall x A(x) \land \forall x B(x)$, $\exists x (A(x) \lor B(x)) \equiv \exists x A(x) \lor \exists x B(x)$.

• Quantifier Removal: $\forall \equiv \cdots \land \cdots$, $\exists \equiv \cdots \lor \cdots$.

Sementic Entailment

Satisfiability & Validity:

• $\mathcal{I}$ and $E$ satisfy a formula $\alpha$, denoted by $\mathcal{I} \models_E \alpha$, iff $\alpha^{(\mathcal{I}, E)} = 1$.

• If $\forall E$, $\mathcal{I} \models_E \alpha$, then $I$ satisfies $\alpha$, denoted by $\mathcal{I} \models \alpha$.

• For a set of formulas $\Sigma$, if $\forall \varphi \in \Sigma$, $I \models_E \varphi$, then $I \models_E \Sigma$.

• A formula $\alpha$ is:

  • valid, if $\forall I, E$, $I \models_E \alpha$; (denoted by $\varnothing \models \alpha$)

  • satisfiable, if $\exists I, E$, $I \models_E \alpha$;

  • unsatisfiable, if $\forall I, E$, $I \not\models_E \alpha$.

Entailment:

• Definition: We say:

  • $\Sigma$ semantically entails / logically implys $\alpha$, or

  • $\Sigma \models \alpha$,

  iff $\forall I, E$, if $I \models_E \Sigma$, then $I \models_E \alpha$.

Undecidability:

• PL is decidable, but FOL is undecidable.

Natural Deduction Proof System

Substitution:

• $\alpha[t / x]$ denotes the resulting formula by replacing each free occurrence of variable $x$ in $\alpha$ with term $t$.

  Term $t$ must be “fresh” to avoid capture.

Inference Rule:

• $\forall$-introduction & $\forall$-elimination:

  $$\frac{\boxed{\begin{array}{c} y \text{ fresh} \\ \vdots \\ \alpha[y / x] \end{array}}}{(\forall x \alpha)} \quad \quad \frac{(\forall x \alpha)}{\alpha[t / x]}$$

• $\exists$-introduction & $\exists$-elimination:

  $$\frac{\alpha[t / x]}{(\exists x \alpha)} \quad \quad \frac{(\exists x \alpha) \quad \boxed{\begin{array}{c} \alpha[u / x], u \text{ fresh} \\ \vdots \\ \beta \end{array}}}{\beta}$$

Soundness & Completeness:

• The natrual deduction proof system is sound and complete.

Normal Form:

• Prenex Normal Form (前束范式): $Q_1 x_1 Q_2 x_2 \cdots Q_k x_k B$, where $Q_i$ is a quantifier, and $B$ is quantifier free.

  Every formula in FOL is logically equivalent to a formula in prenex normal form.

Higher-Order Logic

Temporal Logic: for reasoning about how truths change over time.

Modal Logic: extends classical logic with operators for necessity and possibility.

Hoare Logic: for proving the correctness of computer programs.

---

Program Verification

Process of program verification:

• Convert an inital description into a logical formula.

• Write a program.

• Prove the program satisfies the formula.

We will focus on the third part.

Formal Specification

Two important components of a specification:

• Precondition: The state before the program executes.

• Postcondition: The state after the program executes.

Our formal notation:

• is based on FOL logic.

• applies to imperative programs.

• uses Hoare Triples.

Hoare Triple:

• A Hoare triple $(|P|) ~ C ~ (|Q|)$:

  • Precondition: $P$ (FOL formula)

  • Code to be verified: $C$

  • Postcondition: $Q$ (FOL formula)

Correctness

Partial Correctness:

• Hoare triple $(|P|) ~ C ~ (|Q|)$ is satisfied under partial correctness iff

  • for every state $s_1$ that satisfies $P$,
  • if execution of $C$ starting from state $s_1$ terminates in a state $s_2$,
  • then state $s_2$ satisfies condition $Q$.
  • (if execution of $C$ does not terminate, it’s ok)

  which is denoted as

  $$\models_{\text{par}} (|P|) ~ C ~ (|Q|)$$

Total Correctness:

• Hoare triple $(|P|) ~ C ~ (|Q|)$ is satisfied under total correctness iff

  • for every state $s_1$ that satisfies $P$,
  • execution of $C$ starting from state $s_1$ terminates in a state $s_2$,
  • then state $s_2$ satisfies condition $Q$.
  • (execution of $C$ must terminate)

  which is denoted as

  $$\models_{\text{tot}} (|P|) ~ C ~ (|Q|)$$

Hoare Logic

Presentation of a Proof:

Axioms:

• Assignment:

  $$\frac{}{(|Q[E / x]|) ~ x = E ~ (|Q|)}$$

• Implied Rule: Precondition Strengthening:

  $$\frac{P \to P' \quad (|P'|) ~ C ~ (|Q|)}{(|P|) ~ C ~ (|Q|)}$$

• Implied Rule: Postcondition Weakening:

  $$\frac{(|P|) ~ C ~ (|Q'|) \quad Q' \to Q}{(|P|) ~ C ~ (|Q|)}$$

• Composition:

  $$\frac{(|P|) ~ C_1 ~ (|Q|) \quad (|Q|) ~ C_2 ~ (|R|)}{(|P|) ~ C_1; C_2 ~ (|R|)}$$

• If Statements:

  $$\frac{(|P \land B|) ~ C_1 ~ (|Q|) \quad (|P \land \neg B|) ~ C_2 ~ (|Q|)}{(|P|) ~ \text{if } B ~ \{C_1\} \text{ else } \{C_2\} ~ (|Q|)}$$

• While Statements / Partial-While: (do not yet require termination)

  $$\frac{(|I \land B|) ~ C ~ (|I|)}{(|I|) ~ \text{while } B ~ \{C\} ~ (|I \land \neg B|)}$$

  where $I$ is a loop invariant which holds both before we execute $C$ and after $C$ terminates.

  To prove termination (total correcness), we need to find a variant, which is an integer expression that:

  • always stays non-negative, and
  • strictly decrease in every loop iteration.

  The automatic extraction of useful variants or termination expressions cannot be realized.

Decidability

Decision Problem:

• The answer is yes or no.

Decidable:

• If there exists an algorithm that always halts (停止) with a yes / no answer for every input.

e.g.

• Collatz Conjecture: Algorithmically undecidable.
• The Halting Problem: Undecidable.
• The Partial Correctness Problem: Undecidable.