Hilbert流演繹体系 - Internet Explorer 2.0

Hilbert流演繹体系

メモ

少なめの推論規則と，いくつかの公理（または公理図式）によって証明体系を特徴づける．

推論規則として

普通の公理である場合は一様代入則なども要請するがそれはあまり本質的ではない．

公理図式として

証明は列としての証明として捉えられる．

古いメモ

証明体系$ \cal{K}が存在する，次の3組が定義される．

記号

公理群

推論規則群

演繹の概念

有限個の論理式の列$ \varphi_1 \dots \varphi_nを，$ \cal{K}における前提$ \Gammaから論理式$ \varphiへの演繹とする．

ただし

$ \Gammaは$ \cal{K}における論理式の列

各々の論理式$ \varphi_iは次の条件を満たす

$ \cal{K}の公理

$ \Gammaのいずれか

$ \varphi_l,\varphi_m \quad (1 \leq l,m < i)から$ \cal{K}の推論規則によって導き出された論理式

$ \cal{K}において$ \Gammaから$ \varphiへの演繹が存在し，そのときのみ，$ \varphiは$ \Gammaから演繹可能であるといい，$ \Gamma \vdash_{\cal{K}} \varphiと表す．

$ \Gammaが空列で$ \varphiへの演繹が存在するなら，その演繹は証明と呼ばれる．

$ \varphiは$ \cal{K}の定理

$ \varphiは$ \cal{K}で証明可能

$ \vdash_{\cal{K}} \varphi