# 希尔伯特演绎系统

## 形式定义

${\displaystyle \forall y(\forall xPxy\to Pty)}$

${\displaystyle \forall xPxy\to Pty}$ 的普遍化。

### 逻辑公理

1. ${\displaystyle \phi \to \left(\psi \to \phi \right)}$
2. ${\displaystyle \left(\phi \to (\psi \rightarrow \xi \right))\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$
3. ${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

4. ${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$ 这里的t可以代换在${\displaystyle \phi }$ x
5 ${\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}$
6 ${\displaystyle \phi \to \forall x\left(\phi \right)}$ 这里的x不是${\displaystyle \phi }$ 中的自由变量

1. ${\displaystyle x=x}$ 对于所有变量x
2. ${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

## 元定理

• 演绎定理${\displaystyle \Gamma ;\phi \vdash \psi }$ 当且仅当${\displaystyle \Gamma \vdash \phi \to \psi }$
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$ 当且仅当${\displaystyle \Gamma \vdash \phi \to \psi }$ 并且${\displaystyle \Gamma \vdash \psi \to \phi }$
• 对置（Contraposition）:如果${\displaystyle \Gamma ;\phi \vdash \psi }$ ${\displaystyle \Gamma ;\lnot \psi \vdash \lnot \phi }$
• 普遍化：如果${\displaystyle \Gamma \vdash \phi }$ 并且x不自由的出现在${\displaystyle \Gamma }$ 的任何公式中，则${\displaystyle \Gamma \vdash \forall x\phi }$

## 参考文献

### 引用

1. Máté & Ruzsa 1997:129

### 来源

• Curry, Haskell B.; Feys, Robert. Combinatory Logic Vol. I 1. Amsterdam: North Holland. 1958.
• Monk, J. Donald. Mathematical Logic. New York; Heidelberg; Berlin: Springer-Verlag. 1976.
• Ruzsa, Imre; Máté, András. Bevezetés a modern logikába. Budapest: Osiris Kiadó. 1997 （匈牙利语）.
• Tarski, Alfred. Bizonyítás és igazság. Budapest: Gondolat. 1990 （匈牙利语）. It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.