命题逻辑由命题和命题逻辑符号组成。每个命题都可以判断真假。

1. 命题

命题是在一个域内可以判断真假的语句。

2. 命题逻辑中的符号:

  • ¬: 命题的否定,p的否定与p的真值相反;
  • ∨: 两个命题的或符号;
  • ∧: 两个命题的与符号;
  • →: 蕴含符号,如果p则q,表示成 p→q
  • ⊤:特殊符号,表示真
  • ⊥:特殊符号,表示假

3. 自然演绎 Natural deduction

在自然演义中,我们有证明规则proof rules,用于从一个公式推演到另一个公式,这样我们可以从前提,得到我们想要的结论。

假设我们有公式φ1, φ2, φ3, …, φn, 我们称这些公式为前提promises,我们还有一个公式ψ,如果从前提出发,运用证明规则,我们想要得到ψ,这个推理表示为:

φ1, φ2, …, φn ⊢ ψ.

我们把ψ称为结论conclusion

3.1 自然演绎中的规则

规则1:and-introduction $ \land_i $

ϕ    ψϕψi\frac{\phi\ \ \ \ \psi}{\phi \land \psi}\land_i

规则2:and-elimination

ϕ  ψϕ,    ϕ  ψψ\frac{\phi\ \land\ \psi}{\phi}, \ \ \ \ \frac{\phi\ \land\ \psi}{\psi}

规则3:double negation ¬¬e,¬¬i\neg\neg e, \neg\neg i

¬¬ϕϕ¬¬e,    ϕ¬¬ϕ¬¬i\frac{\neg\neg\phi}{\phi}\neg\neg e, \ \ \ \ \frac{\phi}{\neg\neg\phi}\neg\neg i

规则4: eliminating implication $\rightarrow e $

ϕ    ϕψϕe\frac{\phi \ \ \ \ \phi \rightarrow \psi}{\phi} \rightarrow e

规则5:modules tollens MTMT

ϕψ     ¬ψ¬ϕMT\frac{\phi \rightarrow \psi \ \ \ \ \ \neg\psi }{\neg\phi} MT

规则6:disjunction

ϕϕψ,    ψϕψ\frac{\phi }{\phi \lor \psi } , \ \ \ \ \frac{\psi}{\phi \lor \psi}

3.2 直觉主义逻辑 VS 经典逻辑

例:(反证法) 我们现在要证明 ϕ\phi成立,我们在前提中假设¬ϕ\neg \phi 成立,并且推断出矛盾 contradiction, 由此得到ϕ\phi 成立。

这在经典逻辑里,反证法是正确的推理过程。但是在直觉主义逻辑里,这个推理过程需要商榷。直觉主义学者认为,要证明ϕ\phi 成立,需要直接证明,或者证明 ¬ϕ\neg\phi 不可能存在,假设是不成立。在直觉主义逻辑里,一下的规则是不成立的:

ϕ¬ϕLEM,    ¬¬ϕϕ¬¬e,\frac{}{\phi \lor \neg\phi } LEM, \ \ \ \ \frac{\neg\neg\phi}{\phi}\neg\neg e,

要证明$\phi \lor \neg\phi ,直觉主义认为要me证明\phi,要么证明\neg\phi$ 。我们举个例子,来说明两种主义对于证明的看法:

定理:存在两个无理数a,ba,b,使得aba^{b}是一个有理数。

证明:假设 bb2\sqrt{2},所以 bbb^{b} 要么是无理数,要么是有理数。

  1. 假设bbb^{b}是有理数。因此命题中,选择aa2\sqrt{2},则aba^{b}等于bbb^{b},是个有理数,得证。
  2. 假设bbb^{b}是无理数。因此我们选择aa22\sqrt{2}^{\sqrt{2}}(因为bbb^{b}是无理数,令b=2b=2),因此ab=222=2(2×2)=22=2a^{b}=\sqrt{2}^{\sqrt{2}^{\sqrt{2}}} = \sqrt{2}^{(\sqrt{2} \times \sqrt{2})} = \sqrt{2}^2 = 2,是有理数。((xy)z=x(xz))((x^y)^z = x^{(x\cdot z)})

所以不管我们怎么假设,我们都得到命题的结论。

但是,这个推理对于直觉主义来说,是不成立的。因为我们没有给出确切的a,ba,b的值。在上述证明中,两个假设1和2是相互依赖的,但是假设时选择的aa的值是不一样的。


4 命题逻辑语法

ϕ::=p  (¬ϕ)  (ϕϕ)  (ϕϕ)  (ϕϕ)\phi ::= p\ |\ (\neg\phi)\ |\ (\phi \land \phi)\ |\ (\phi \lor \phi)\ |\ (\phi \rightarrow \phi)


5 符号语义(semantics)

命题逻辑中,每个符号的含义都用真值表来定义(1表示真,0表示假)。当然,每个符号,也可以定义成另外的含义。

p ¬p p q p∨q
1 0 1 0 1
0 1 0 1 1
0 0 0
1 1 1
p q p∧q p q p→q
1 0 0 1 0 0
0 1 0 0 1 1
0 0 0 0 0 1
1 1 1 1 1 1

根据真值表,可以得出ϕψ\phi \rightarrow \psi¬ϕψ\neg \phi \lor \psi 具有一样的真值情况,所以是语义对等的。


6. 命题逻辑的可靠性(soundness)

$\phi_1, \phi_2, …, \phi_n \vdash \psi $ 如果成立,表示可以通过推演系统,由前提ϕ1,ϕ2,...,ϕn\phi_1, \phi_2, ..., \phi_n,推演得到结论 ψ\psi 。但是,我们有证据表明,通过真值表的语义,也能得到相同的结论吗?

定义: 如果通过真值表,得到前提 $\phi_1, \phi_2, …, \phi_n $皆为真,并且结论 ψ\psi 也为真,我们就说下面的公式成立:

ϕ1,ϕ2,...,ϕnψ\phi_1, \phi_2, ..., \phi_n\models \psi

符号 \models 称为 semantic entailment relation .

例子1:pqpp \land q \models p 成立吗?
通过真值表判断,pqp \land q 为真时,pp 也为真,所以成立。

例子2:pqpp \lor q \models p 成立吗?
通过真值表判断,pqp \land q 为真时,pp 也为假,所以不成立。

可靠性定理:Soundness.. ϕ1,ϕ2,...,ϕn\phi_1, \phi_2, ..., \phi_n 为命题逻辑公式,如果$\phi_1, \phi_2, …, \phi_n \vdash \psi $ 成立,则$\phi_1, \phi_2, …, \phi_n\models \psi $ 也成立。

证明过程:略。(如果$\phi_1, \phi_2, …, \phi_n \vdash \psi $ 成立,则可以用推演系统,从前提$\phi_1, \phi_2, …, \phi_n $ 推演到结论。假设,推理过程用了kk 步(推理过程的长度,运用推演规则一次记为一步)……)

可靠性定理的作用:可靠性定义可以用来说明证明过程是否存在。假设我们要证明$\phi_1, \phi_2, …, \phi_n \vdash \psi $ ,但是经过我们的努力,我们没找到适合的推演过程,但是,这并无代表不存在合理的推演过程,我们只是没找到而已。如果我们根据真值表,得出前提ϕ1,ϕ2,...,ϕn\phi_1, \phi_2, ..., \phi_n为真,ψ\psi为假,所以$\phi_1, \phi_2, …, \phi_n\models \psi $ 不成立,根据可靠性定理,我们可以知道,不存在推理过程,使得$\phi_1, \phi_2, …, \phi_n \vdash \psi $ 成立。

7. 命题逻辑的完备性(Completeness)

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

  • step1:证明 ϕ1(ϕ2(ϕ3(...(ϕnψ)...)))\models \phi_1 \rightarrow ( \phi_2 \rightarrow ( \phi_3 \rightarrow ( ... (\phi_n \rightarrow \psi)...)) ) 成立;
  • step2:证明 ϕ1(ϕ2(ϕ3(...(ϕnψ)...)))\vdash \phi_1 \rightarrow ( \phi_2 \rightarrow ( \phi_3 \rightarrow ( ... (\phi_n \rightarrow \psi)...)) ) 成立;
  • step3:证明 $\phi_1, \phi_2, …, \phi_n \vdash \psi $ 成立

证明过程:略。

结合命题逻辑的可靠性,我们得到如下:

ϕ1,ϕ2,...,ϕnψ is valid iff ϕ1,ϕ2,...,ϕnψ holds.\phi_1, \phi_2, ..., \phi_n \vdash \psi\ is\ valid\ iff\ \phi_1, \phi_2, ..., \phi_n \models \psi\ holds.

引理:Given formulas ϕ1,ϕ2,...,ϕn\phi_1, \phi_2, ..., \phi_n and ψ\psi of propositional logic, $\phi_1, \phi_2, …, \phi_n \models \psi\ $ holds iff ϕ1(ϕ2(ϕ3(...(ϕnψ)...)))\models \phi_1 \rightarrow ( \phi_2 \rightarrow ( \phi_3 \rightarrow ( ... (\phi_n \rightarrow \psi)...)) ) holds.


8. 命题逻辑的可满足性(Satisfiability)

定义:Semantic equivalence. Let ϕ\phi and ψ\psi be formulas of propositional logic. We say that ϕ\phi and ψ\psi are semantically equivalent iff ϕψ\phi \models \psi and ψϕ\psi \models \phi hold. In that case we write ϕ\phiψ\psi. Further, we call ϕ\phi valid if ϕ\models \phi holds.

定义:conjunctive normal form (CNF)范式 A literal LL is either an atom pp or the negation of an atom ¬p\neg p. A formula CC is in conjunctive normal form (CNF) if it is a conjunction of clauses, where each clause DD is a disjunction of literals:

  • L::=p  ¬pL ::= p\ |\ \neg p
  • D::=L  L DD ::= L\ |\ L\ \lor D
  • C::=D  DCC ::= D\ |\ D\land C

定义:Satisfiability. Given a formula ϕ\phi in propositional logic, we say that ϕ\phi is satisfiable if it has a valuation in which is evaluates to true.

命题逻辑公式转换到CNF范式的算法:

1
2
3
4
5
6
7
8
9
10
11

function CNF(φ):
/* precondition: φ implication free and in NNF */
/* postcondition: CNF (φ) computes an equivalent CNF for φ */
begin function
case
φ is a literal : return φ
φ is φ1 ∧φ2: return CNF(φ1)∧CNF(φ2)
φ is φ1 ∨ φ2 : return DISTR (CNF (φ1), CNF (φ2))
end case
end function
1
2
3
4
5
6
7
8
9
10
function DISTR(η1,η2):
/* precondition: η1 and η2 are in CNF */
/* postcondition: DISTR (η1, η2) computes a CNF for η1 ∨ η2 */
begin function
case
η1 is η11 ∧ η12 : return DISTR (η11, η2) ∧ DISTR (η12, η2)
η2 is η21 ∧ η22 : return DISTR (η1, η21) ∧ DISTR (η1, η22)
otherwise (= no conjunctions) : return η1 ∨ η2
end case
end function

定义:negation normal form (NNF)否定范式 Formulas which only negate atoms are said to be in negation normal form (NNF).

1
2
3
4
5
6
7
8
9
10
11

function CNF(φ):
/* precondition: φ implication free and in NNF */
/* postcondition: CNF (φ) computes an equivalent CNF for φ */
begin function
case
φ is a literal : return φ
φ is φ1 ∧φ2: return CNF(φ1)∧CNF(φ2)
φ is φ1 ∨ φ2 : return DISTR (CNF (φ1), CNF (φ2))
end case
end function

9. SAT solvers