形式的体系（命題論理）

定理1.4.6 は論理式の形だけを見れば論理値を考えなくても適用できるようになっている。この節では、意味を考えなくても、決められた式の変形だけで正しい命題を作成できるような規則を与える。

記号列の集合を形式的な規則で定義したものを形式的体系（formal system）と呼び、記号列がその集合に属することをこの形式的な規則に沿って示したものをその体系における証明と呼ぶ。形式的規則は証明の書き方を規定しているといってもよい。

古典命題論理の自然推論NKは形式的体系の一種である。