# 希尔伯特演绎系统

## 形式定义

${\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
2. ^ Máté & Ruzsa 1997:129

## 引用

• Curry, Haskell B.; Robert Feys. 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.

## 外部链接

Farmer, W. M. Propositional logic (PDF). （原始内容 (pdf)存档于2007-09-26）. It describes (among others) a part of the Hilbert-style deduction system（restricted to propositional calculus）。