形式體系の好い性質
meta 定理
完全性定理 (completeness theorem)
不完全性定理 (incompleteness theorems) Löwenheim-Skolem の定理 (Löwenheim-Skolem theorem)
Herbrand の定理 (Herbrand's theorem)
節の有限集合$ Fに就いて、$ Fが充足不能である事と、$ Fから得られる基礎例 (Herbrand 基底) の有限集合に充足不能なものが在る事とが、同値である事 Herbrand 領域 (Herbrand universe)
定數 (個體定項) と變數 (個體變項) と n 引數函數からなる式に就いて、變數を持たない項 (閉項。closed term) 全體の集合 基礎例 (ground instance)
變數を持たない述語又は節
Herbrand 基底 (Herbrand basis)
或る述語に就いて、Herbrand 領域の要素を引數とする述語の集合
述語論理式を命題論理式として扱へる
Herbrand 解釋 (Herbrand interpretation)
Herbrand 基底の任意の部分集合
compact 性定理 (compactness theorem)
文の集合$ S=\{P,Q,…\}が model を持つ (充足可能)$ \exist M(M\vDash S)事と、その文の集合の任意の有限部分集合が model を持つ$ \forall T_{\subseteq S\land T~is~finite}\exist N(N\vDash T)事とが、同値である事 演繹定理 (deduction theorem)
形式體系$ Tに於いて$ P\vdash Qならば$ \vdash P\to Qである事
cut 除去定理 (cut-elimination thorem)
形式體系$ Tに於いて、定理$ Pが cut 規則$ \frac{A,B,…\vdash C\quad C\vdash D,E,…}{A,B,…\vdash D,E,…}を用ゐて證明できるならば、cut 規則を用ゐなくても證明できる (解析的證明 (analytic proof)) 事
cut 除去定理が成り立つならば、その形式體系では空の sequent (矛盾) を證明できない