Mathematical logic (2) Propositional logic 命题逻辑

1. Syntax 语法

1.1 Proposition 命题

A declarative sentence that can be judged as either true or false is called Proposition.

1.1.1 Atomic Proposition 原子命题

The proposition can’t be devided into a smaller one.

Typically symbolized as $p, q, r, \dots$

1.1.2 Compound Proposition 复合命题

The proposition is built by two or more atomic proposition is called composition proposition.

Typically symbolized as $A, B, C, \dots$

1.2 Logical Connectives 逻辑连接词

Connectives	Meaning	Term
$\land$	and	conjuction
$\lor$	or	disjunction
$\neg$	not	negation
$\to$	if…then…	implication
$\leftrightarrow$	if and only if	equivalence

1.3 Alphabet 符号系统

• Atomic proposition: $p, q, r, \dots$
• Logic connectives: $\land,\lor,\neg,\to,\leftrightarrow$
• Punctuations: ( , )

1.4 Expressions 表达式

Finite strings of symbols is called expression.

Empty expression is denoted by $\lambda$.

1.5 Formulas 公式

Definition for $Atom(\mathscr{L}^P)$: A set of expressions consisting of one symbol only.

Induction definition for $Form(\mathscr{L}^P)$:

1. $Atom(\mathscr{L}^P) \subseteq Form(\mathscr{L}^P)$.
2. If $A \in Form(\mathscr{L}^P)$, then $(\neg A) \in Form(\mathscr{L}^P)$.
3. If $A, B \in Form(\mathscr{L}^P)$, then $(A \land B), (A \lor B), (A \to B), (A \leftrightarrow B) \in Form(\mathscr{L}^P)$.

A well-formed formula(WFF) can be and only be derived by this way.

1.5.1 Parse Tree 解析树

A parse tree for $Form(\mathscr{L}^P)$ is a tree satisfying:

1. The root is the formula.
2. Leaves are atomic formulas.
3. Each internal node is formed by applying some formation rule on its children.

e.g. The parse tree for $p \lor q \to \neg p \land r$ is:

An expression of $\mathscr{L}^P$ is a WFF if and only if there is a parse tree of it.

Each well-formed formula of $\mathscr{L}^P$ has a unique parsing tree.

From this, we can verify whether an expression is WFF programmably by building a parse tree for it.This is a sample Python program used to verify the validity of an input formula.

# /usr/bin/env python3
# -*- coding: utf-8 -*-
# python version: 3.10.6

# define a binary tree as the parse tree
class parseTree:

    # initialize the a leaf of the parse tree
    def __init__(self, char = ''):
        self.char = char
        self.left = None
        self.right = None
        self.parent = None
        self.flag = False # flag to check if this leaf is valid
    
    # insert a character at the current leaf
    def insert(self, char):
        self.char = char
    
    # visit the left child of the current leaf
    def visit_left_child(self):
        if self.left == None:
            self.left = parseTree('')
            self.left.parent = self
        return self.left
    # visit the right child of the current leaf
    def visit_right_child(self):
        if self.right == None:
            self.right = parseTree('')
            self.right.parent = self
        return self.right

    # visit the parent of the current leaf
    def visit_parent(self):
        if self.parent != None:
            return self.parent
        else:
            self.flag = True # if the current leaf is the root, then it is invalid
            return self

# build the parse tree from the input string
def build_parse_tree(string):
    root = parseTree() # the root of the parse tree
    cur = root
    alphabet = "abcdefghijklmnopqrstuvwxyz" # the set of all possible atomic propositions

    for c in string:
        if c == '(':
            cur = cur.visit_left_child() # '(' means the a branch of the parse tree is needed
        elif c == ')': 
            cur = cur.visit_parent() # ')' means the current branch of the parse tree is finished
        else:
            if cur.char == '' and c in alphabet: # if the current leaf is empty and the character is an atomic proposition
                cur.char = c
            elif c == '¬': # if the character is a negation
                cur = cur.visit_parent()
                cur.insert(c)
                cur = cur.visit_left_child()
            elif c == '∧' or c == '∨' or c == '→' or c == '↔': # if the character is a binary connective
                cur = cur.visit_parent()
                cur.insert(c)
                cur = cur.visit_right_child()
            elif c == ' ': # if the character is a space, then skip
                continue
            else:
                cur.flag = True # if the character is invalid, then the current leaf is invalid
    return root

def check_parse_tree(parse_tree):
    if parse_tree.flag:
        return False
    if parse_tree.char == '':
        return False

    # check if the parse tree is valid, using preorder traversal method
    # A parse tree is of an well-formed formula if and only if all of its leaves are valid and non-empty
    if parse_tree.left != None:
        if not check_parse_tree(parse_tree.visit_left_child()):
            return False
    if parse_tree.right != None:
        if not check_parse_tree(parse_tree.visit_right_child()):
            return False
    return True

# Main function
if __name__ == '__main__':
    s = input()
    parse_tree = build_parse_tree(s)
    if check_parse_tree(parse_tree):
        print(True)
    else:
        print(False)

1.5.2 Subformula 子公式

A formula $G$ is a subformula of $F$ if $G$ occurs within $F$. Specially we called $G$ a proper subformula when $G \neq F$.

Immediate formula are the branch of a formula in parse tree, and leading connectives is the connective that is used to join the branch.

1.5.3 Structure 结构

Lemma $1$: Well-formed formulas of $\mathscr{L}^P$ are non-empty expressions.

Lemma $2$ : Every well-formed formula of $\mathscr{L}^P$ has an equal number of opening and closing brackets.

Given a non-empty expression $u=w_1vw_2$

• Segment: $v$ is a segment of $u$.
• Proper Segment: $v$ is non-empty and $v \neq u$.
• Prefix (Initial Segment): $v$ is a prefix of $u$ if $w_2=\lambda$, specially $v$ is called proper prefix if $v \neq u$.
• Suffix (Terminal Segment): $v$ is a suffix of $u$ if $w_1=\lambda$m specially $v$ is called proper suffix if $v \neg u$.

Lemma $3$:

• Every proper prefix of a well-formed formula in $\mathscr{L}^P$ has more opening brackets than closing brackets.
• Similarly, every proper suffix of a well-formed formula in $\mathscr{L}^P$ has more closing brackets than opening brackets.

$Unique$ $Readability$ $Theorem$: There is a unique way to construct every well-formed formula.

1.6 Precendence 优先顺序

• Connectives: $\neg,\land,\lor,\to,\leftrightarrow$ (Less priority from left to right).
• Parentheses (with punctuations"()") take the highest precendence.
• With connectives of the same precedence, the rightmost occurrence have more priority (e.g. $p \to q \to r \equiv p \to (q \to r)$ ).

2. Semantics 语义

2.1 Truth Table 真值表

2.2 Truth Valuation 真值指派

A truth valuation is a function $v: Atom(\mathscr{L}^P) \to \{0, 1\}$.

For $p \in Atom(\mathscr{L}^P)$, we use $p^v$ to denote the truth value of $p$ under the truth valuation $v, p^v \in \{0, 1\}$

• Atomic proposition: $p \in \{0, 1\}$

• Negation:

$$(\neg A)^v=\left\{ \begin{aligned} 1 &\text{ if } A^v = 0 \\ 0 &\text{ else} \\ \end{aligned} \right.$$

• Conjuction:

$$(A \land B)^v=\left\{ \begin{aligned} 1 &\text{ if } A^v=B^v=1 \\ 0 &\text{ else} \\ \end{aligned} \right.$$

• Disjunction:

$$(A \lor B)^v=\left\{ \begin{aligned} 1 &\text{ if } A^v=1 \text{ or } B^v=1 \\ 0 &\text{ else} \\ \end{aligned} \right.$$

• Implication:

$$(A \to B)^v=\left\{ \begin{aligned} 1 &\text{ if } A^v=0 \text{ or }B^v=1 \\ 0 &\text{ else} \\ \end{aligned} \right.$$

• Equivalence:

$$(A \leftrightarrow B)^v=\left\{ \begin{aligned} 1 &\text{ if } A^v=B^v \\ 0 &\text{ else} \\ \end{aligned} \right.$$

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

Proof :

1. Initial Condition: If $\alpha \in Atom(\mathscr{L}^P)$, then there must exist $\alpha^v \in \{0, 1\}$ (definition).
2. Inductive Step:
   • If $a^v \in \{0, 1\}$, then $(\neg a)^v \in \{0, 1\}$ according to the truth table.
   • If $\alpha, \beta \in \{0, 1\}$, then $(\alpha \star \beta)$ also does for every binary connetives $\star$.
3. Conclusion: By this induction, every formula in $\mathscr{L}^P$ has a truth value in $\{0, 1\}$; and by the Unique Readablitity Theorem we proved that $\alpha$ has only one value under a fixed $v$.

2.3 Truth Properties of Formulas 公式的性质

Let $A \in Form(\mathscr{L}^P)$

• $A$ is tautogy(永真式) when $\forall v, A^v = 1$.
• $A$ is contradiction(矛盾式) or unsatisfiable when $\forall v, A^v = 0$.
• $A$ is satisfiable(可满足的) when $\exists x, A^V = 1$.

2.4 Logic Equivalence 逻辑等价

Formulas $A, B$ are logically equivalent iff $\forall v, A^v=B^v$.

2.4.1 Laws for Logic Equivalence 逻辑等价律

• Identity laws:
  • $p \land T \equiv p$
  • $p \lor F \equiv p$
• Domination laws:
  • $p \lor T \equiv T$
  • $p \land F \equiv F$
• Idempotent laws:
  • $p \lor p \equiv p$
  • $p \land p \equiv p$
• Double negation laws:
  • $\neg(\neg p) \equiv p$
• Commutative laws:
  • $p \lor q \equiv q \lor p$
  • $p \land q \equiv q \land p$
• Associative laws:
  • $(p \lor q) \lor r \equiv p \lor (q \lor r)$
  • $(p \land q) \land r \equiv p \land (q \land 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 law:
  • $\neg(p \lor q) \equiv \neg p \land \neg q$
  • $\neg(p \land q) \equiv \neg p \lor \neg q$
• Absorption laws:
  • $p \lor (p \land q) \equiv p$
  • $p \land (p \lor q) \equiv p$
• Negation laws:
  • $p \lor \neg p \equiv T$
  • $p \land \neg p \equiv F$
• Implicative laws:
  • $p \to q \equiv \neg p \lor q$
• Contrapositive laws:
  • $p \to q \equiv \neg q \to \neg p$
• Equivalence laws:
  • $p \leftrightarrow q \equiv (p \to q) \land (q \to p)$

2.4.2 Substitution 代换

$B$ is a substitution instance of $A$ iff B may be obtained from $A$ by substituting formulas for propositional variables in $A$, replacing each occurrence of the same variable by an occurrence of the same formula.

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

Theorem $1$: $A, B \in (\mathscr{L}^P)$. If $A$ is a tautology and $B$ is a susbtitution instance of $A$, then $B$ is again a tautology.

Theorem $2$: $A \in Form(\mathscr{L}^P)$. $A$ contain a subformula $C$ (i.e., $C$ is a segment of $A$ and is itself a well-formed formula). If $C \equiv D$, then replacing some occurrences (not necessarily all) of the subformula $C$ in $A$ with $D$ to obtain the formula $B$, then $A \equiv B$.

3. Entailment 蕴涵

Let $\Sigma \subseteq Form(\mathscr{L}^P), A \in Form(\mathscr{L}^P)$. We say:

• $A$ is a logical consequence of $\Sigma$
• $\Sigma$ entails $A$
• $\Sigma \models A$

Iff for all truth valuation $v$ if $\Sigma^v=1$ then $A^v=1$

Also, $\Sigma \not\models A$ denotes there exists a truth valuation $v$ such that $\Sigma^v=1$ and $A^v=0$.

3.1 Prove Entailment 蕴涵证明

• Direct Proof: For every truth valuation under which all of the premises are true, show that the conclusion is also true under this valuation.
• Using Truth Table: Consider all rows of the truth table in which all of the formulas in $\Sigma$ are true. Verify that $A$ is true in all of these rows.
• Proof by Contradiction Assume that the entailment does not hold, which means that there is a truth valuation under which all of the premises are true and the conclusion is false. Derive a contradiction.

4. Proof 形式化证明

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

• Language part
  • Symbols and alphbet
  • Set of formulas
• Inference part
  • Set of axioms(公理)
  • Inference rules

4.1 Notation 记号

$$\Sigma \vdash A$$

denotes that "there is a proof with premises $\Sigma$ and conclusion $A$.

4.2 Types 类型

• Hilbert-Style System ($\Sigma \vdash_H A$)
• Natural Deduction System ($\Sigma \vdash_{ND} A$)
• Resolution ($\Sigma \vdash_{Res} A$)