命题逻辑演算

前置

• 命题逻辑

命题逻辑演算

• Zero-order language(零阶语言) ${\mathcal{L}}_0$:

  • Alphabet(字母表)(是countable的): $\{\neg ,\to ,(,)\}\cup \{p_i|i\in \mathbb{N}\}$
  • The set of well-formed formulas(良形公式)(wfs):
    • $p_i$ is a wfs
    • If $\mathcal{A}$ and $\mathcal{B}$ are wfs, then $\neg \mathcal{A}$ and $(\mathcal{A}\to \mathcal{B})$ are wfs
    • The set of all wfs generated by the above rules is called the set of wfs.

• Formal system(形式系统) $L$ of statement calculus(命题演算):

  • Zero-order language(零阶语言) ${\mathcal{L}}_0$:
  • Axioms(公理):
    • (L1) $(\mathcal{A}\to (\mathcal{B}\to \mathcal{A}))$
    • (L2) $(\mathcal{A}\to (\mathcal{B}\to \mathcal{C}))\to ((\mathcal{A}\to \mathcal{B})\to (\mathcal{A}\to \mathcal{C}))$
    • (L3) $(\neg \mathcal{A}\to \neg \mathcal{B})\to (\mathcal{B}\to \mathcal{A})$
  • Rules of reduction(归约规则):
    • MP(modus ponens) Rules of deduction: from $\mathcal{A}$ and $(\mathcal{A}\to \mathcal{B})$, $\mathcal{B}$ is a direct consequence where $\mathcal{A}$ and $\mathcal{B}$ are wfs of $L$.

• Proof(证明): A proof in $L$ is a sequence of wfs. ${\mathcal{A}}_1,{\mathcal{A}}_2,\cdots ,{\mathcal{A}}_n$ such that for each $i(1<i<n)$, either ${\mathcal{A}}_i$ is an axiom of $L$ or ${\mathcal{A}}_i$ follows from two previous members of the sequence, say ${\mathcal{A}}_j$ and ${\mathcal{A}}_k$ ($j<i,k<i$) as a direct consequence using the rule of deduction MP. Such a proof will be referred to as a proof of ${\mathcal{A}}_n$ in $L$, and ${\mathcal{A}}_n$ is said to be a theorem of $L$.

• Deduction(归约): let $\Gamma$ be a set of wfs. of $L$ (which may or may not be axioms or theorems of $L$). A sequence ${\mathcal{A}}_1,{\mathcal{A}}_2,\cdots ,{\mathcal{A}}_n$ of wfs. of $L$ is a deduction from $\Gamma$ (记作$\Gamma {⊢}_L{\mathcal{A}}_n$) if for each $i(1<i<n)$, one of the following holds:

  • ${\mathcal{A}}_i$ is an axiom of $L$
  • ${\mathcal{A}}_i$ is a member of $\Gamma$
  • ${\mathcal{A}}_i$ follows from two previous members of the sequence, say ${\mathcal{A}}_j$ and ${\mathcal{A}}_k$ ($j<i,k<i$) as a direct consequence using the rule of deduction MP.

• Valuation(赋值): A valuation of $L$ is a function $v$ whose domain is the set of wfs. of $L$ and whose range is the set $\{T,F\}$ such that, for any wfs. $\mathcal{A},\mathcal{B}$ of $L$,

  • $v(\mathcal{A})\ne v(\neg \mathcal{A})$
  • $v(\mathcal{A}\to \mathcal{B})=F$ if and only if $v(\mathcal{A})=T$ and $v(\mathcal{B})=F$

• Tautology(重言式): A wf $\mathcal{A}$ is a tautology if $v(\mathcal{A})=T$ for every valuation $v$ of $L$.

• Extension(扩张): An extension of $L$ is a formal system obtained by altering or enlarging the set of axioms so that all theorems of $L$ remain theorems (and new theorems are possibly introduced).

• Consistent(一致): A extension of $L$ is consistent if there is not exist a wf $\mathcal{A}$ of $L$ such that $\mathcal{A}$ and $\neg \mathcal{A}$ are both theorems of extension of $L$. 即对所有的 wf. $\mathcal{A}$ 都有 $\mathcal{A}$ 或 $\neg \mathcal{A}$ 不是 theorem of extension of $L$。

• Complete(完备): A extension of $L$ is complete if for every wf. $\mathcal{A}$ of $L$, either $\mathcal{A}$ or $\neg \mathcal{A}$ is a theorem of extension of $L$.

性质

1. ${⊢}_L(\mathcal{A}\to \mathcal{A})$,where $\mathcal{A}$ is any wf of $L$
2. Deduction theorem: $\Gamma \cup \{\mathcal{A}\}{⊢}_L\mathcal{B}$ $⟺$ $\Gamma {⊢}_L(\mathcal{A}\to \mathcal{B})$
3. (Hypothetical syllogism): $\{(A\to B),(B\to C)\}{⊢}_L(A\to C)$
4. ${⊢}_L(\neg \mathcal{B}\to (\mathcal{B}\to \mathcal{A}))$
5. ${⊢}_L((\neg \mathcal{A}\to \mathcal{A})\to \mathcal{A})$
6. Every theorem of $L$ is a tautology.
7. $L$ is consistent.
8. An extension $L^{\ast }$ of $L$ is consistent if and only if there is a wf. which is not a theorem of $L^{\ast }$.
9. 设$L^{\ast }$是$L$的一致扩张，$\mathcal{A}$是$L$的一个 wf.，且$\mathcal{A}$不是$L^{\ast }$的定理，则向$L^{\ast }$中添加$\neg \mathcal{A}$作为公理，所得的扩张$L^{\ast \ast }$也是一致的。
10. Let $L^{\ast }$ be an extension of $L$. Then there is a consistent complete extension of $L^{\ast }$
11. If $L^{\ast }$ is a consistent extension of $L$ then there is a valuation in which each theorem of $L^{\ast }$ is true.
12. (The Adequacy Theorem for $L$): If $\mathcal{A}$ is a wf. of $L$ and $\mathcal{A}$ is a tautology, then $\mathcal{A}$ is a theorem of $L$.