証明図の読み方¶
証明図では，横線の上に前提，横線の下に結論を書きます． 右側の \((\to I)\) や \((\land E)\) は，使っている推論規則の名前です． ここでの証明図は自然演繹の規則を表示しています． シーケント計算では，\(\Gamma \vdash P\) のようなシーケントそのものを左規則・右規則で変形しますが，この章では論理結合子を導入する規則と，すでにある証明から情報を取り出す除去規則を中心に見ます． たとえば
\[
\frac{\Gamma \vdash P \to Q \quad \Gamma \vdash P}{\Gamma \vdash Q}\;(\to E)
\]
は，「同じ仮定の集まり \(\Gamma\) のもとで \(P \to Q\) と \(P\) が証明できるなら，\(Q\) が証明できる」と読みます．
ここで \(\Gamma\) は「現在使ってよい仮定や変数の集まり」です．
Lean のコードでは，通常 \(\Gamma\) という記号は直接書きません．
かわりに，example や theorem の引数，intro で導入した仮定，cases で場合分けして得た仮定が，Lean のローカルコンテキストとして管理されます．
VS Code の Infoview では，ゴールの上に並ぶ変数や仮定が，証明図の \(\Gamma\) に対応します．
たとえば
では，Lean のローカルコンテキストにはおおよそP : Prop と hP : P があります．
このうち hP : P は「\(P\) の証明を仮定として使ってよい」という意味で，証明図の \(P \in \Gamma\) に対応します．
述語論理では，x : α のような対象変数もコンテキストに入ります．
証明図では，命題の仮定と対象変数をまとめて \(\Gamma\) と省略している，と考えるとよいです．
intro hP は，含意を示す途中で一時的に hP : P をコンテキストに追加する操作です．
証明図では，これは横線の上側に出てくる \(\Gamma, P \vdash Q\) の \(P\) に対応します．
証明が終わると，その仮定は「もし \(P\) ならば」という含意の中に閉じ込められ，結論は \(\Gamma \vdash P \to Q\) になります．