形式証明の用語

形式証明では，「式がどの規則で導かれたか」と「式が何を意味するか」を分けて考えます． この区別は Lean を学ぶ上で重要です．

証明論は，記号列としての命題と，それを変形する推論規則を扱います． この立場での「証明」は，有限個の推論規則を順に適用して結論に到達する構文的な対象です． 自然演繹の証明図でいえば，根に結論をもち，各節点で決められた推論規則だけを使っている木が証明です． Lean の証明項も，この意味で検査可能な構文的対象です．

意味論は，命題を解釈するモデルや構造を与え，その解釈のもとで命題が真か偽かを考えます． たとえば命題論理では，各命題変数に真理値を割り当てたときに式全体の真理値が決まります． この真理値は「意味」の側の概念であり，形式証明そのものではありません． 健全性定理は「証明できる式は意味論的に正しい」と述べ，完全性定理は，対象となる論理に応じて「意味論的に正しい式は証明できる」と述べる定理です．

命題論理や述語論理は，どのような式を作るかを定める論理の言語です． 命題論理では P ∧ Q や P → Q のように命題を論理結合子で組み合わせます． 述語論理ではさらに，対象変数，述語，∀ や ∃ などの量化子を扱います． 一方，自然演繹やシーケント計算は，そのような式をどの規則で証明するかを定める証明体系です． 同じ命題論理や述語論理に対して，自然演繹で証明することも，シーケント計算で証明することもできます．

この章で扱う規則は，主に直観主義自然演繹の導入規則と除去規則です． Gentzen の記法に合わせて，命題論理の直観主義自然演繹を NJ と呼ぶことがあります． 量化子も含めて話すときは，「直観主義一階自然演繹」と呼ぶのが正確です． 後で出てくる排中律や背理法は NJ だけでは証明できないため，古典論理の原理として区別して扱います． それらを自然演繹に追加した体系は，古典自然演繹，あるいは Gentzen の記法では NK と呼ばれます．

なお，この章では \(\Gamma \vdash P\) という形の表記を使いますが，これは「仮定の集まり \(\Gamma\) のもとで \(P\) が証明できる」という判断を表すための記法です． この表記自体はシーケント風ですが，ここで説明している規則はシーケント計算の左規則・右規則ではなく，自然演繹の導入規則・除去規則です． したがって，この章の規則を指すときは「自然演繹の規則」，より具体的には「直観主義自然演繹 NJ の規則」と呼ぶのがよいです．

自動証明では，SAT/SMT solver や theorem prover が，探索によって証明や反例を見つけようとします． 多くの場合，ユーザは問題を入力し，システムができるだけ自動で結論を出します． 一方，Lean のような対話型証明支援系では，ユーザが証明の方針や中間ステップを与え，システムが現在のゴールを表示しながら証明を組み立てます． Lean にも simp や omega などの自動化されたタクティックはありますが，最終的には生成された証明項をカーネルが型検査する，という点が中心です．

Lean の基礎は，ZFC 集合論ではなく，依存型理論です． ZFC では基本的にすべての数学的対象を集合として扱い，定理は一階述語論理の式として表されます． Lean では対象は型をもち，命題は Prop という型の項として扱われ，その命題の証明はその型の項として扱われます． つまり Lean では，P : Prop に対して h : P という項を構成することが，P を証明することです． Mathlib の中で集合や位相空間や群を扱うことはできますが，Lean の基礎そのものは「すべてを集合に還元する」立場ではありません．

この「命題を型，証明を項として見る」対応は，型付きラムダ計算と深く結びついています． 含意 P → Q の証明は，P の証明を受け取って Q の証明を返す関数です． 含意導入はラムダ抽象 fun h : P => ... に対応し，含意除去は関数適用に対応します． 連言の証明はペア，連言除去は射影に対応します． したがって，紙の上の証明木，Lean の tactic proof，Lean が内部で作る証明項は，見た目は違っても同じ証明構造を別の表現で見ていると考えられます． 特に含意や全称命題の証明では，証明項が fun h : P => ... のような関数として現れます．