一阶逻辑演算

前置

• 一阶逻辑

定义

• Fix a first order language $\mathcal{L}$, Define a formal deductive system $K_{\mathcal{L}}$ (abbr. $K$) bythe following axioms and rules of deduction.

  • Axioms
    Let $\mathcal{A},\mathcal{B},\mathcal{C}$ be any wfs. of $\mathcal{L}$. The following are axioms of $K_{\mathcal{L}}$:

    • $K(1)$: $(\mathcal{A}\to (\mathcal{B}\to \mathcal{A}))$.
    • $K(2)$: $(\mathcal{A}\to (\mathcal{B}\to \mathcal{C}))\to ((\mathcal{A}\to \mathcal{B})\to (\mathcal{A}\to \mathcal{C}))$.
    • $K(3)$: $(\neg \mathcal{A}\to \neg \mathcal{B})\to (\mathcal{B}\to \mathcal{A})$.
    • $K(4)$: $(\forall x_i)\mathcal{A}\to \mathcal{A}$, if $x_i$ does not occur free in $\mathcal{A}$.
    • $K(5)$: $(\forall x_i)\mathcal{A}(x_i)\to \mathcal{A}(t)$, if $\mathcal{A}(x_i)$ is a wf. of $K_{\mathcal{L}}$ and $t$ is a term in $\mathcal{L}$ which is free for $x_i$ in $\mathcal{A}(x_i)$.
    • $K(6)$: $(\forall x_i)(\mathcal{A}\to \mathcal{B})\to (\mathcal{A}\to (\forall x_i)\mathcal{B})$, if $\mathcal{A}$ contains no free occurrence of the variable $x_i$.

  • Rules

    • Modus ponens(MP): from $\mathcal{A}$ and $(\mathcal{A}\to \mathcal{B})$ deduce $\mathcal{B}$.
    • Generalisation: from $\mathcal{A}$ deduce $(\forall x_i)\mathcal{A}$, where $x_i$ is any variable.

• A proof in $K_{\mathcal{L}}$ is a sequence of wfs. ${\mathcal{A}}_1,{\mathcal{A}}_2,\dots ,{\mathcal{A}}_n$ such that for each $i(1\le i\le n)$, either ${\mathcal{A}}_i$ is an axiom of $K_{\mathcal{L}}$ or ${\mathcal{A}}_i$ follows from previous members of the sequence by MP or Generalisation.

• If $\Gamma$ is a set of wfs. of $\mathcal{L}$, a deduction from $\Gamma$ in $K_{\mathcal{L}}$ is a similar sequence, in which members of $\Gamma$ may be included.

• A wf. $\mathcal{A}$ is a theorem of $K_{\mathcal{L}}$ if it is the last member of some sequence which constitutes a proof in $K_{\mathcal{L}}$.

• A wf. $\mathcal{A}$ is a consequence in $K_{\mathcal{L}}$ of the set $\Gamma$ of wfs. if $\mathcal{A}$ is the last member of a sequence which constitutes a deduction from $\Gamma$ in $K_{\mathcal{L}}$.

• Write${⊢}_{K_{\mathcal{L}}}\mathcal{A}$ to denote “$\mathcal{A}$ is a theorem of $K_{\mathcal{L}}$”, and $\Gamma {⊢}_{K_{\mathcal{L}}}\mathcal{A}$ to denote “$\mathcal{A}$ is a consequence in $K_{\mathcal{L}}$ of $\Gamma$”, where $\Gamma$ is a set of wfs. of $K_{\mathcal{L}}$.

• For the sake of convenience we shall abbreviate $K_{\mathcal{L}}$ to $K$ unless there is reason to emphasise the particular language being used.

• Let $\mathcal{A}$ and $\mathcal{B}$ be wfs. of $L$. Say $\mathcal{A}$ and $\mathcal{B}$ are provably equivalent if ${⊢}_K(\mathcal{A}⟺\mathcal{B})$.

• If $\mathcal{A}$ is a wf. of containing free occurrences of the variables $y_1,\cdots ,y_n$ only,
  then wf. $(\forall y_1)\cdots (\forall y_n)\mathcal{A}$ is the universal closure of $\mathcal{A}$.The universal closure of $\mathcal{A}$ is usually denoted by ${\mathcal{A}}^{\prime }$.

性质

graph TD
A[Tautology] --> C[Theorem of K]
C[Theorem of K] --> B[Logically Valid]

1. If $\mathcal{A}$ is a wf. of $\mathcal{L}$ and $\mathcal{A}$ is tautology, then $\mathcal{A}$ is a theorem of $K_{\mathcal{L}}$.
2. All instances of axiom schemes (K4), (K5) and (K6) are logically valid.
3. The Soundness Theorem for K: For any wf. $\mathcal{A}$ of $\mathcal{L}$, if ${⊢}_{K_{\mathcal{L}}}\mathcal{A}$ then $\mathcal{A}$ is logically valid.
4. K is consistent (i.e. for no wf. $\mathcal{A}$ are both $\mathcal{A}$ and $\neg \mathcal{A}$ theorems of K).
5. The Deduction Theorem for $K$:Let $\mathcal{A}$ and $\mathcal{B}$ be wfs. of $K$, and let $\Gamma$ be set (possibly empty) of wfs. of $K$. If $\Gamma \cup \{\mathcal{A}\}{⊢}_K\mathcal{B}$, and the deduction contains no application of Generalisation involving a variable which occurs free in $\mathcal{A}$, then $\Gamma {⊢}_K(\mathcal{A}\to \mathcal{B}).$
6. If $\Gamma \cup \{\mathcal{A}\}{⊢}_K\mathcal{B},\text{and}\mathcal{A}\text{is a closed wf., then}\Gamma {⊢}_K(\mathcal{A}\to \mathcal{B}).$
7. For any wfs. $\mathcal{A},\mathcal{B},\mathcal{C}$ of $K$, $(\mathcal{A}\to \mathcal{B}),(\mathcal{B}\to \mathcal{C}){⊢}_K(\mathcal{A}\to \mathcal{C}).$
8. For any wfs. $\mathcal{A}\text{ and }\mathcal{B}\text{ of }\mathcal{L}$, ${⊢}_K(\mathcal{A}⟺\mathcal{B})$ iff ${⊢}_K(\mathcal{A}\to \mathcal{B})$ and ${⊢}_K(\mathcal{B}\to \mathcal{A}).$
9. For any wfs. $\mathcal{A},\mathcal{B},\mathcal{C}$ in $\mathcal{L}$, if $\mathcal{A}$ and $\mathcal{B}$ are provably equivalent, $\mathcal{B}$ and $\mathcal{C}$ are provably equivalent, then $\mathcal{A}$ and $\mathcal{C}$ are provably equivalent.
10. If $x_i$ occur free in $\mathcal{A}(x_i)$ and $x_j$ is variable that not occur, free or bound, in $\mathcal{A}(x_i)$, then ${⊢}_K(\forall x_i\mathcal{A}(x_i)⟺\forall x_j\mathcal{A}(x_j))$.
11. If $\mathcal{A}$ is and wf. of $\mathcal{L}$, whose free variables are $y_1,y_2,\cdots ,y_n$, then ${⊢}_K(\forall y_1)(\forall y_2)\cdots (\forall y_n)\mathcal{A}$ iff ${⊢}_K\mathcal{A}$.
12. ${⊢}_K{A}^{\prime }\to A$
13. Let $\mathcal{A}$ and $\mathcal{B}$ be wfs. of $\mathcal{L}$, and suppose that ${\mathcal{B}}_0$ arises from the wf. ${\mathcal{A}}_0$ by substituting $\mathcal{B}$ for one or more occurrences of $\mathcal{A}$ in ${\mathcal{A}}_0$. Then ${⊢}_K((\mathcal{A}⟺\mathcal{B}{)}^{\prime }\to ({\mathcal{A}}_0⟺{\mathcal{B}}_0))$.
14. If $x_j$ does not appear (free or bound) in the wf. $\mathcal{A}(x_i)$, and the wf. ${\mathcal{B}}_0$ arises from ${\mathcal{A}}_0$ by replacing one or more occurrences of $(\forall x_i)\mathcal{A}(x_i)$ by occurrences of $(\forall x_j)\mathcal{A}(x_j)$, then ${⊢}_K({\mathcal{A}}_0⟺{\mathcal{B}}_0).$