逻辑系统的可靠性和完备性

给定一个逻辑 (Theory),以及这个逻辑的推演系统(inference system)。如果通过推演系统,判断一个公式 ϕ\phi 是为真的,并且,通过语义(比如命题逻辑中根据真值表判断)判断公式 ϕ\phi ,的确为真,则该逻辑是可靠sound的。
如果根据语义判断后,对于每个为真的公式,都可以利用推演系统证明,则称该逻辑是完备complete的。
Whether everything that can be proven with a given inference system is indeed valid (in this case the system is called sound), and whether there exists a proof of validity using the inference system for every valid formula (in this case it is called complete).

命题逻辑的可靠性定理:Soundness.. ϕ1,ϕ2,...,ϕn\phi_1, \phi_2, ..., \phi_n 为命题逻辑公式,如果 ϕ1,ϕ2,...,ϕnψ\phi_1, \phi_2, ..., \phi_n \vdash \psi 成立,则 $\phi_1, \phi_2, …, \phi_n \models \psi $ 也成立。(ϕ1,ϕ2,...,ϕnψ\phi_1, \phi_2, ..., \phi_n \vdash \psi 成立,表示可以通过前提,推演得到结论 ψ\psi,$\phi_1, \phi_2, …, \phi_n\models \psi $ 成立,表示根据真值表判断,各个前提 ϕi\phi_i为真,ψ\psi也为真)。

命题逻辑的完备性定理:Completeness.. 命题逻辑的推演规则是complete的:任何时候如果 $\phi_1, \phi_2, …, \phi_n\models \psi $ 成立,则存在推演过程使得 $\phi_1, \phi_2, …, \phi_n \vdash \psi $ 成立。


基本定义

赋值

Definition 1.1 (assignment). Given a formula φ, an assignment of φ from a domain DD is a function mapping φ’s variables to elements of DD. An assignment to φ is full if all of φ’s variables are assigned, and partial otherwise.

可满足性

Definition 1.2 (satisfiability, validity and contradiction). A formula is satisfiable if there exists an assignment of its variables under which the formula evaluates to true. A formula is a contradiction if it is not satisfiable. A formula is valid (also called a tautology) if it evaluates to true under all assignments.

What does it mean that a formula “evaluates to true” under an assignment? To evaluate a formula, one needs a definition of the semantics of the various functions and predicates in the formula. In propositional logic, for example, the semantics of the propositional connectives is given by truth tables, as presented above. Indeed, given an assignment of all variables in a propositional formula, a truth table can be used for checking whether it satisfies a given formula, or, in other words, whether the given formula evaluates to true under this assignment.

Example. The propositional formula: $A ∧ B $
is satisfiable because there exists an assignment, namely {A → true, B → true}, which makes the formula evaluate to true.

αϕ,ϕ\alpha \models \phi, \models \phi

Given a formula φ and an assignment α of its variables, we write α \models φ to denote that α satisfies φ. If a formula φ is valid (and hence, all assignments satisfy it), we write $ \models φ$

判断问题

Definition (the decision problem for formulas). The decision problem for a given formula φ is to determine whether φ is valid (under all assignments).

判定过程的可靠性

Definition (soundness of a procedure). A procedure for the decision problem is sound if when it returns “Valid”, the input formula is valid.
判定过程是可靠的,如果对一个公式返回“Valid”,而这个公式的确是valid的。(是不是不太好理解?因为一个公式valid与否,是判定过程给出答案,既然判定过程给出valid,那公式就是valid的了。)

判定过程的完备性

**Definition (completeness of a procedure).**A procedure for the decision problem is complete if

  • it always terminates, and
  • it returns “Valid” when the input formula is valid.

判定过程

Definition (decision procedure). A procedure is called a decision procedure for theory TT if it is sound and complete with respect to every formula of TT.

判定性 decidability

Definition (decidability of a theory). A theory is decidable if and only if there is a decision procedure for it.


公式的基本定义

NNF 范式

Definition (negation normal form (NNF)). A formula is in negation normal form (NNF) if negation is allowed only over atoms, and ∧,∨,¬ are the only allowed Boolean connectives.

For example, ¬(x1 ∨ x2) is not an NNF formula, because the negation is applied to a subformula which is not an atom.

literal

Definition (literal). A literal is either an atom or its negation. We say that a literal is negative if it is a negated atom, and positive otherwise. For example, in the propositional-logic formula
$(a ∨ ¬b) ∧ ¬c $
the set of literals is \{a, ¬b, ¬c\},

Definition (state of a literal under an assignment). A positive literal is satisfied if its atom is assigned true. Similarly, a negative literal is satisfied if its atom is assigned false.

Definition (pure literal). A literal is called pure in a formula φ, if all occurrences of its variable have the same sign.

DNF 范式

Definition 1.16 (disjunctive normal form (DNF)). A formula is in dis- junctive normal form if it is a disjunction of conjunctions of literals, i.e., a formula of the form
i(jlij)\lor_i(\land_j lij)
where lijlij is the jj-th literal in the ii-th term (a term is a conjunction of literals). For example:
$(a∧c∧¬b) ∨ (¬a∧d) ∨ (b∧¬c∧¬d) ∨ …$

CNF范式

Definition (conjunctive normal form (CNF)). A formula is in conjunctive normal form if it is a conjunction of disjunctions of literals, i.e., it has the form
i(jlij)\land_i(\lor_j lij)
where lijlij is the jj-th literal in the ii-th clause (a clause is a disjunction of literals).