计算机数理逻辑-命题逻辑-语法与语义

1. Introduction

Logic formalizes valid methods of reasoning

  • 逻辑将有效的推理方法正规化

  • 比如syllogism/ˈsɪləˌdʒɪz(ə)m/三段论

  • atomic/əˈtɒm.ɪk/ proposition

    • statements that have no internal structure
    • 原子命题是没有内部结构的语句
    • cannot be further decomposed and can be assigned a truth value of true or false
    • often shortened to atoms

  • syntax

    • define the legal structure of formulas in propositional logic

  • semantics

    • the meaning of formulas
      • T or F
      • Another notation is ⊤ for true and ⊥ for false

  • Proof

    • A proof is a deduction of a formula from a set of formulas called axioms using rules of inference.
    • 证明是利用推理规则从一组称为公理的公式中推导出一个公式

Propositional logic is central to the design of computer hardware because hardware is usually designed with components having two voltage levels that are arbitrarily assigned the symbols 0 and 1. Circuits/ˈsərkət/ are described by idealized elements called logic gates

命题逻辑是计算机硬件设计的核心，因为硬件的设计通常有两个电压电平，被任意分配为符号0和1。电路由称为逻辑门的理想化元素描述

  • automated reasoning是建立在语法正确的前提上，探讨语义真值
    • 命题一定是一个格式正确的公式 ，在命题逻辑中，这意味着它既是由逻辑在句法上定义的，又具有用于其语义评估的真值表
      • 语法定义了哪些符号串构成合法的公式（就语言而言是合法的程序）
      • 而语义定义了合法公式的含义（合法程序的计算）
      • 语义表时检测公式是否为真的有效的决策程

2. Propositional Formulas命题公式

  • expression 表达式
    • denoted the computation of a value from other values
    • 表示从其他数值中计算出一个数值
    • In propositional logic, the term formula is used instead
  • atomic propositions
    • An unbounded set of symbols P
  • Boolean operators

2.1. subformulas

2.2. Formulas as Trees

  • unary/ˈjuːnəri/ operator 单目运算符 vs binary operators 双目运算符
  • implication 实质条件 实质蕴涵
    • 理解为assignment
    • 若A，则B (要么A为假 要么B为真（或二者同时成立）)
    • A $\rightarrow$ B == $¬A∨B$ 相当于只是一个简写denote
    • 区别于语义蕴含⊨
  • nor和nand就是在or和and之后再取一次反

命题逻辑中的公式可以是一棵递归定义的树（defined recursively）

  • 一个公式是由一个原子命题标记（labeled）的叶子。
  • 一个公式是一个由¬标记的节点，它的一个子节点是一个公式
  • 一个公式是一个由二元运算符之一标记的节点，同时两个子节点自身也是公式

2.3. Formulas as Strings

命题逻辑中的公式也可以是字符串

  • The string associated with a formula is obtained by an inorder traversal/trəˈvərs(ə)l/
    of the tree
  • 一个公式的字符串表示是通过对树的中序遍历得到的
    • 先左子树，后根结点，最后右子树
  • ambiguity /æmbɪˈɡjuːɪti/ 模糊性

2.4. Resolving Ambiguity in the String Representation

parentheses/pəˈrenθəsiːz/ 圆括号

  • The simplest way to avoid ambiguity is to use parenthesesto maintain the structure of the tree when the string is constructed.
  • 避免歧义的最简单方法是在构建字符串时使用圆括号来保持树的结构
  • 缺点：verbose冗长 and hard to read and write

Precedence/ˈpresɪdəns/ 优先级

  • define precedence and associativity conventions among the operators as is done in arithmetic, so that we immediately recognize a∗b∗c+d∗e as (((a∗b)∗c)+(d∗e))
    • 解决模棱两可的公式的第二种方法是在运算符之间定义优先级和关联性约定，就像在算术中所做的那样，这样我们就可以立即将a∗b∗c+d∗e识别为(((a∗b)∗c)+(d∗e))
  • Parentheses are used only if needed to indicate an order different from that imposed by the rules for precedence and associativity
    • 只有在需要表示与优先权和关联性规则所规定的顺序不同时，才使用括号
  • precedence from high to low

Polish Notation 波兰式（前缀表示法）和 reverse Polish notation 逆波兰式（后缀表示法）

波兰表达式和逆波兰表达式有个好处，就算将圆括号去掉也没有歧义

逆波兰表达式的解释器一般是基于堆栈的。解释过程一般是：操作数入 栈；遇到操作符时，操作数出栈，求值，将结果入栈；当一遍后，栈顶就是表达式的值。因此逆波兰表达式的求值使用堆栈结构很容易实现，并且能很快求值

  • 用于简化命题逻辑
  • 先序遍历 preorder
    • 表达式a*(b+c)-e/f
      • 中序遍历，就是日常用的表达式写法。对于加法和减法需要加括号。
      • 用前序遍历，对应前缀表达式：-*a+bc/ef
      • 用后序遍历，对应后缀表达式：abc+*ef/-

2.5. Structural induction 结构归纳法

Structural induction is used to prove that a property holds for all formulas. This form of induction is similar to the familiar numerical induction that is used to prove that a property holds for all natural numbers

结构归纳法被用来证明一个属性对所有公式都成立。这种形式的归纳法类似于我们熟悉的数字归纳法，后者是用来证明一个属性对所有自然数都成立的

To show that a property holds for all formulas $A\in{F}$ :

  1. Prove that the property holds all atoms $p$.
  2. Assume that the property holds for a formula $A$ and prove that the property holds for $¬A$.
  3. Assume that the property holds for formulas $A_1$ and $A_2$ and prove that the property holds for $A_1 op A_2$, for each of the binary operators.

so a proof that a property holds for all formulas can be done using structural induction with the base case and only two inductive steps. 一个初始例子和两个归纳步骤

3. Interpretations 解释

一个函数

  • An interpretation for A is a total function $I_A:P_A \rightarrow{ { T,F } }$ that assigns one of the truth values T or F to every atom in $P_A$, $P_A$ 是 $A$ 的原子命题子集，$A$ 是公式集合 $F$ 中的一个
  • An interpretation is a mapping of atomic propositions to the values {T,F}.
    • 换句话说解释$I_A$就是“计算并返回A的真值”的函数

true value

a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth

真理值，有时也被称为逻辑值，是一个表明命题与真理关系的数值。

  • 真值表Truth Tables
    • 拆分为subformula

设 A 为命题，v 为赋值.

  1. v 满足(satisfies) A，记为 v ⊧ A，指 ˆv(A) = T；即当atom取值为v时A为真
  2. A 为永真式 (tautology)，记为 ⊧ A，指对任何 v 有 ˆv(A) = T；
  3. A 可满足指存在 v 使 v ⊧ A；
  4. 设 Γ 为命题集，A 为 Γ 的语义结论，记为 Γ ⊧ A，指对所有 v，若对任何 B ∈ Γ 有 ˆv(B) = T 则 ˆv(A) = T.

3.1. partial interpretation

  • A partial interpretation for A is a partial function $I_A:P_A\rightarrow{}{T,F}$ that assigns one of the truth values T or F to some of the atoms in $P_A$

3.2. Model

  • If a formula is true under an interpretation, then that interpretation is called a model of that formula
    • 如果一个公式在某个解释下为真，那么这个解释就被称为该公式的模型(可以理解为”解“)
    • 注意是一个解释（或者说一个取值），而不是atom本身

3.3. The Relationship Between ↔ and ≡

  • Equivalence, ↔, is a Boolean operator in propositional logic and can appear in formulas of the logic
  • Logical equivalence, ≡, is not a Boolean operator; instead, is a notation for a property of pairs of formulas in propositional logic.
    • 集合有吗?还是说只是命题?
  • $A_1$≡$A_2$ iff $A_1 ↔ A_2$ is true in every interpretation.

3.4. Substitution

A is a subformula of B if A is a subtree of B.

  • If A is not the same as B, it is a proper subformula of B.

B{A←A′}, the substitution of A′ for A in B(在B中用A’代替A), is the formula obtained by replacing all occurrences of the subtree for A in B by A′

  • Let A be a subformula of B and let A′ be a formula such that A≡A′. Then B≡B{A←A′}

3.5. law 常用公式与定律

  • ⇔/↔ 等价符号

    • 相当于if and only if
    • A ↔ B ≡ (A → B) ∧ (B → A)

  • Idempotent/ˌīdemˈpōt(ə)nt/ Law幂等律

    • A⇔A∨A
    • A⇔A∧A

  • commutative law交换律

    • The binary Boolean operators are commutative, except for implication.
    • A∨B⇔B∨A
    • A∧B⇔B∧A
    • A↑B⇔B↑A

  • associative law结合律

    • (A∨B)∨C⇔A∨(B∨C)
    • (A∧B)∧C⇔A∧(B∧C)

  • Distributive law分配律

    • A∨(B∧C)⇔(A∨B)∧(A∨C)
    • A∧(B∨C)⇔(A∧B)∨(A∧C)

4. Satisfiability, Validity and Consequence

  • A is satisfiable可满足的 iff $v_I(A)=T$ for some interpretation .
    • A satisfying interpretation is a model for A.
  • A is valid有效的, denoted ⊨A, iff $v_I(A)=T$ for all interpretations .
    • A valid propositional formula is also called a tautology永真式（重言式）.
  • A is unsatisfiable不可满足的 iff it is not satisfiable, that is, if $v_I(A)=F$ for all interpretations
    • $I \not\models p \equiv I \models \lnot p$
  • A is falsifiable可证伪的 (区别于unsatisfiable), denoted $\not\models$ , iff it is not valid, that is, if $v_I(A)=F$ for some interpretation
  • A is valid if and only if ¬ A is unsatisfiable. A is satisfiable if and only if ¬ A is falsifiable.

符号之间的联系

  • A formula A is valid if and only if ¬A is unsatisfiable.

    • ⊨ A iff ¬A ⊨ ⊥

  • A formula A is satisfiable if and only if ¬A is not valid.

  • A formula A is valid if and only if A is equivalent to ⊤.

  • Formulas A and B are equivalent if and only if the formula A ↔ B is valid.

    • $A\equiv B \iff A\leftrightarrow B \iff \forall v, v\models A iff v\models B$

  • Propositional satisfiability is NP-complete NP完全（计算复杂度相关）.

  • Propositional validity is coNP-complete.

4.1. decision procedure决定程序

  • Let $U\subseteq{F}$ be a set of formulas. An algorithm is a decision procedure for $U$ if given an arbitrary formula $A\in{F}$ , it terminates and returns the answer yes if $A\in{U}$ and the answer no if $A\notin{U}$ .

没有unsure

  • If $U$ is the set of satisfiable formulas, a decision procedure for is called a decision procedure for satisfiability, and similarly for validity
    • 如果U是可满足公式的集合，那么一个可满足性的决策程序被称为可满足性的决策程序，同样地，有效性的决策程序也是如此。
  • A reasoning method RM is a decision procedure for Φ if RM is sound, refutationally complete and terminating for Φ.
  • The truth table method is a decision procedure for propositional logic

4.2. Logical Consequence 蕴涵（结论）

  • Let U be a set of formulas and A a formula. A is a logical consequence of U, denoted U⊨A, iff every model of U is a model of A
  • Let A=(p∨r)∧(¬ q∨¬ r). Then A is a logical consequence of {p,¬ q}, denoted {p,¬ q}⊨A

To see whether a formula F2 is a logical consequence of a formula F1, write out their joint truth table. Find the rows in which F1 is true; those are essentially the models that satisfy F1. Check to see whether F2 is also true in all of those rows/models; if it is, then every model that satisfies F1 automatically satisfies F2, and F2 is therefore a logical consequence of F1.

要看一个公式F2是否是公式F1的逻辑结果，请写出它们的联合真值表。找出F1为真的那几行；这些基本上是满足F1的模型。检查F2是否在所有这些行/模型中也是真的；如果是，那么每个满足F1的模型都自动满足F2，因此F2是F1的逻辑结果

蕴含是讨论“命题和命题之间的真值传递关系的”

  • U⊨A iff ⊨ $⋀_iA_i→A$

注意⊨不是该语言中的符号，而是在上层语言 (meta-language) 中.在上层语言中，人们也需要用联结词如 iff，not，and，or，imply 等

4.3. Logical Equivalence 逻辑等价性

5. Semantic Tableauxta·blowz 语义表

While truth tables can be used as a decision procedure for the satisfiability or validity of formulas of propositional logic, semantic tableaux are usually much more efficient. In a semantic tableau, a tree is constructed during a search for a model of a formula; the construction is based upon the structure of the formula. A semantic tableau is closed if the formula is unsatisfiable and open if it is satisfiable.

  • 单数形式tableau(/tæˈbloʊ)
  • an efficient decision procedure for satisfiability (and by duality validity) in propositional logic
  • An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula
    • 一个分析表是为一个逻辑公式计算的树状结构，在每个节点上都有一个要证明或反驳的原公式的子公式。通过计算构建了这棵树，并使用它来证明或反驳整个公式。

5.1. Literal文字 （vs atoms）

  • A literal is an atom or the negation of an atom. An atom is a positive literal and the negation of an atom is a negative literal.
  • For any atom p, {p,¬ p} is a complementary互补的 pair of literals.
  • A set of literals is satisfiable if and only if it does not contain a complementary pair of literals.
    • 对于A=p∧(¬ q∨¬ p)，当且仅当集合{p,¬ p}和{p,¬ q}中至少有一个不包含互补的一对文字时，A是可满足的。显然，只有第二个集合不包含一对互补的文字

Decomposing Formulas into Sets of Literals

  • $A=p\land{(\lnot{q}\lor{\lnot{p}})}$ => literal={p,¬ q}

求解规则

  1. 拆分
  1. A set of literals is satisfiable if and only if it does not contain a complementary pair of literals
    1. 一个文字集是可满足的，当且仅当它不包含一对互补的文字的时候
    2. 在上面的例子中{p,¬ p}因此被排除

（另一个例子）Both sets of literals {p,¬ p,¬ q} and {q,¬ p,¬ q} contain complementary pairs, so both set of literals are unsatisfiable. We conclude that it is impossible to find a model for B; in other words, B is unsatisfiable

5.2. Construction of Semantic Tableaux

The initial formula labels the root of the tree; each node has one or two child nodes depending on how a formula labeling the node is decomposed. The leaves are labeled by the sets of literals. A leaf labeled by a set of literals containing a complementary pair of literals is marked ×, while a leaf labeled by a set not containing a complementary pair is marked ⊙

  • 初始公式标注为树的根部；
  • 每个节点有一个或两个子节点，取决于标注节点的公式是如何分解的。
  • 叶子是由文字集标记的。由包含互补对的文字集标注的叶子被标记为×（也就是closed），而由不包含互补对的文字集标注的叶子被标记为⊙(也就是open)
  • The tableau construction is not unique; here is another tableau for B
  • α-formulas are conjunctive and are satisfiable only if both subformulas $α_1$ and $α_2$ are satisfied
  • β-formulas are disjunctive and are satisfied even if only one of the subformulas $β_1$ or $β_2$ is satisfiable

The formula p∧q is classified as an α-formula because it is true if and only if both p and q are true. The formula ¬ (p∧q) is classified as a β-formula. It is logically equivalent to ¬ p∨¬ q and is true if and only if either ¬ p is true or ¬ q is true.

构建语义表的算法

  • A completed tableau is closed if all its leaves are marked closed. Otherwise (if some leaf is marked open), it is open

6. Soundness可靠性 and Completeness完备性

  • We need to prove that the algorithm for semantic tableaux is sound and complete as a decision procedure for satisfiability
  • Soundness means that you cannot prove anything that’s wrong. Completeness means that you can prove anything that’s right
    • Soundness is the property of only being able to prove “true” things.
    • Completeness is the property of being able to prove all true things.
      So a given logical system is sound if and only if the inference rules of the system admit only valid formulas. Or another way, if we start with valid premises, the inference rules do not allow an invalid conclusion to be drawn.

    A system is complete if and only if all valid formula can be derived from the axioms and the inference rules. So there are no valid formula that we can’t prove

6.1. Soundness

The theorem to be proved is: if the tableau for a formula A closes, then A is unsatisfiable.

  • if $T_n$, the subtree rooted at node n of $T$, closes then the set of formulas U(n) labeling n is unsatisfiable

6.1.1. vs validity

  • An argument is sound if it meets these two criteria: (1) It is valid. (2) Its premises前提 are true.
    • 总之很类似

6.2. Completeness

if A is unsatisfiable then every tableau for A closes

  • let A=p∨(q∧¬ q)

The open branch of the tableau terminates in a leaf labeled with the singleton set of literals ${p}$. We can conclude that any model for A must define $I(p)=T$. However, an interpretation for A must also define an assignment to q and the leaf gives us no guidance as to which value to choose for $I(q)$. But it is obvious that it doesn’t matter what value is assigned to q; in either case, the interpretation will be a model of A

6.3. Refutation completeness 反向的完备性

  • A formal system S is refutation-complete if it is able to derive false from every unsatisfiable set of formulas

7. 辩经：formula in propositonal logic

一种说法

In propositional logic there are no formulæ. There are only atomic and compound propositions.

  • The atomic propositions are the propositional variables, often written as A,B,C,etc
  • Compound propositions are formed using atomic propositions and logical connectives. These connectives include things like not, implies, and, or, etc.

    It is only in first order logic that we need the notion of formulæ. This is because in first order logic, we don’t only consider propositions but also ‘objects’ and predicates on ‘objects’. First Order logic includes a sub-language to express these ‘objects’ and operations on these ‘objects’.