形式体系とは — 構文と意味の区別
論理学のすべての出発点
入門（高校〜大学1年レベル）
このページの目標
構文（記号の操作）と意味（真理・解釈）が別物であることを理解する。証明できることを表す $\vdash$ と、真であることを表す $\models$ の違いを言葉で説明できるようになる。
1. 形式体系という考え方
数学の証明を厳密に扱うには、まず「証明とは何の上で行う操作か」をはっきりさせる必要がある。そのための枠組みが形式体系（formal system）である。形式体系は、許される記号と、それらをどう組み立て・書き換えてよいかの規則だけで定義される。
形式体系とは、次の三つを定めたものである。 (1) 記号の集合（アルファベット）、 (2) どの記号列が正しく組み立てられた式かを定める構文規則、 (3) 式から式を導く推論規則と、出発点となる公理。
重要なのは、形式体系の定義のどこにも「意味」や「真理」が出てこないことである。形式体系はあくまで記号を並べ替えるゲームであり、その記号が何を表すかは、別に与える「解釈」の仕事になる。
2. 構文と意味の分離
構文（syntax）とは、記号の形と並べ方に関する規則の総体である。式が正しく組み立てられているか、ある式から別の式が規則で導けるかは、すべて記号の形だけで機械的に判定できる。
意味（semantics）とは、記号列に対象や真偽を割り当てる解釈である。たとえば命題変数 $p$ に「真」または「偽」を割り当てると、式 $p \to q$ が真かどうかが決まる。
式 $p \to (q \to p)$ を考える。
- 構文の視点：これは「$p$」「$\to$」「$($」… という記号が規則どおり並んだ正しい式である。さらに推論規則を使えば、何の仮定もなしにこの式を導けるかもしれない。
- 意味の視点：$p, q$ にどんな真偽を割り当てても、この式は必ず真になる（恒真式）。
「導ける」と「いつも真」は、たまたま一致しているように見えるが、定義としては全く別の話である。
3.「導ける」$\vdash$ と「真である」$\models$
構文と意味の区別は、二つの記号にはっきり現れる。
$\Gamma \vdash A$（構文的帰結）：仮定の集合 $\Gamma$ から、証明体系の公理と推論規則だけを使って式 $A$ を導ける。これは証明という記号列が存在するという主張である。
$\Gamma \models A$（意味的帰結）：$\Gamma$ のすべての式を真にするどの解釈（モデル）でも、$A$ もまた真になる。これは真理が保存されるという主張である。
記号の見た目は似ているが、片方は「証明の存在」、もう片方は「すべてのモデルでの真理」という、まったく別の世界の話をしている。日常語の「証明できる」と「正しい」を、この二つにきれいに分けたところに形式論理の力がある。
多くの教科書では、$\vdash$ を「ターンスタイル」、$\models$ を「ダブルターンスタイル」と呼ぶ。本シリーズでも、構文の話をしているときは $\vdash$、意味の話をしているときは $\models$ と、意識して使い分ける。
4. なぜこの区別が決定的か
構文と意味を分けると、二つの大きな問いが自然に立ち上がる。
- 健全性（soundness）：$\Gamma \vdash A$ ならば $\Gamma \models A$ か？ — 「導けたことは本当に真か」（嘘を証明しないか）。
- 完全性（completeness）：$\Gamma \models A$ ならば $\Gamma \vdash A$ か？ — 「真なら必ず導けるか」（真理を取りこぼさないか）。
この二問は 初級・健全性と完全性 で正面から扱う。さらに、構文を機械的に検査できるという性質は、証明検査 や証明アシスタントの根拠になる。意味ではなく構文に証明の正しさを帰着させるからこそ、計算機に検査を任せられるのである。
まとめ
この章のポイント
- 形式体系：記号・構文規則・公理と推論規則だけで定義される「記号のゲーム」
- 構文：記号の形と操作。機械的に判定できる
- 意味：記号への解釈。真偽が決まる
- $\vdash$：導ける（証明が存在する）／ $\models$：いつも真（すべてのモデルで真）
- この二つがいつ一致するかが、健全性・完全性という中心的な問いになる
よくある質問
構文と意味の違いは何か
構文は記号をどう並べ・どう書き換えてよいかの規則で、記号の形だけで機械的に判定できる。意味はその記号列が何を指し、いつ真になるかという解釈である。「規則で導けること」と「真であること」は原理的に別の事柄であり、両者を区別するのが形式体系を理解する出発点である。
記号 $\vdash$ と $\models$ はどう違うのか
$\Gamma \vdash A$ は「$\Gamma$ から $A$ が証明体系の規則で導ける」という構文的な関係（証明の存在）である。$\Gamma \models A$ は「$\Gamma$ をすべて真にするどの解釈でも $A$ が真」という意味的な関係（真理の保存）である。両者がいつ一致するかが健全性・完全性の問題になる。
なぜ意味を捨てて記号操作だけで論理を扱うのか
構文に限定すると、証明の正しさを記号の形だけで機械的に検査できるからである。意味は人間の解釈に依存しがちだが、構文規則は曖昧さなく定義でき、計算機に検査させられる。証明アシスタントが証明を信頼できるのは、最終的にこの機械的な構文検査に帰着するためである。