|| 証明の記号操作の根拠になるもの
「証明」について「記号化したもの」
スポンサーリンク
目次
シークエント「証明の記号的な表現方法」
シークエント計算「シークエントを使った計算」
構造規則「証明の構造から考えて明らかな規則」
コンテキスト「規則が適用されない記号の集まり」
推件式 Sequent
|| 前提と結論を記号で分けた表現方法
『証明を表現する形』をした「記号表現」のこと
\begin{array}{ccc} 前提 & \overset{←から→が導かれる}{\longrightarrow} & 結論 \\ \\ Γ&⊢&φ \end{array}
これの『記号と意味を分離する』ための概念で
（「記号である」などのメタレベルの意味は残る）
\begin{array}{lcl} 構文段階 && Γ\vdash φ の形をした記号 \\ \\ 記号要請段階 && Γやφや\vdash の具体的な中身 \\ \\ 全体要請段階 && Γ\vdash φ 全体の振る舞いの形式表現 \end{array}
その意味はこのような形で区分されています。
（実際の運用ではメタレベルの意味しか持たない記号を指す）
記号 \vdash の変遷
これは以前ちょっと曖昧に使われていた記号で
（『最終的に証明を表現する』点では一致していた）
\begin{array}{ccc} 証明 &\overset{中身を記号で表現して整理}{\longrightarrow}& 前提\vdash 結論 \\ \\ Γ\vDash φ &\overset{モデル内での表現に形成}{\longrightarrow}& Γ\vdash φ \end{array}
だいたいこのような意味で使われていました。
（本質的には同じだが役割と厳密さに差異がある）
\begin{array}{ccc} Γ\vdash φ &\longrightarrow& この記号表現を推件式と呼ぼう \end{array}
これを整備したのが「推件式」で
（ここで \vdash は「ただ置かれるだけの記号」になる）
\begin{array}{ccc} 直感的な意味での証明 &\to& 推件式の形 \\ \\ 記号的な意味での証明 &←& 推件式の形 \end{array}
これにより「証明である（述語）」を
より厳密な形で定義できるようになりました。
（証明？文の記号表現 → 記号の形チェック）
推件式の意味的な要請的定義
↑ では「推件式の形」は定義されましたが
\begin{array}{ccl} Γ && 前提を表しているはず \\ \\ \vdash && 左側から右側が導かれるを意味するはず \\ \\ φ && 結論を表しているはず \end{array}
これらについての定義はまだされていません。
（チェック対象の範囲がまだ広過ぎる）
\begin{array}{ccl} Γ,\vdash,φ &←& この定義も必要 \\ \\ Γ\vdash φ &←& これがどう振る舞うかも必要 \end{array}
この部分が「意味的に要請される定義」であり
（ここでの『意味』はメタレベルの意味以外の意味）
\begin{array}{ccc} 規則上は大丈夫な記号操作 &\to& 証明計算 \end{array}
この「定義に従う」という形で
『証明の計算』は定義されています。
使われる記号への要請的定義
これについては
\begin{array}{ccc} Γ &\Longleftrightarrow& 前提 \\ \\ φ &\Longleftrightarrow& 結論 \\ \\ Γ\vdash φ &\Longleftrightarrow& Γからφが導かれる \end{array}
この感覚的な定義から
（ ↑ の時点では真偽が重要だが ↓ からは問われない）
\begin{array}{ccc} Γ &\Longleftrightarrow& 論理式の有限列 \\ \\ φ &\Longleftrightarrow& １つの論理式 \\ \\ \vdash &\Longleftrightarrow& 置かれる記号 \end{array}
このような形で厳密に定義されています。
（これでもまだ『証明自体の振る舞い』は曖昧）
推件式で出てくる論理式
構文レベルでは真偽が与えられませんが
（つまりこれも推件式で用いる記号への意味的な要請）
\begin{array}{ccl} Γ &\Longleftrightarrow& 真と仮定されている論理式の有限列 \\ \\ φ &\Longleftrightarrow& 真と仮定されている論理式 \end{array}
「推件式で出てくる論理式を表す記号」には
『真であると仮定されている』という条件が付きます。
（偽の前提が入るということは全体の破綻を意味する）
\begin{array}{lcl} 推件式の論理式の真偽 &\to& 全て真と仮定 \\ \\ &\to& 真偽の確認不要 \\ \\ \\ 推件式の論理式記号 &\to& ただの記号 \\ \\ &\to& 真偽の確認不要 \end{array}
なのでそういった意味でも
「真偽を問う必要」は無い状態にあります。
（意味レベルでも構文レベルでも真仮定は自然な帰結）
推件式かどうかのチェックの流れ
補足しておくと
\begin{array}{ccl} チェック対象 &\to& 導かれるなどを記号⊢に変換 \\ \\ &\to& 自然言語表現を論理式に翻訳 \\ \\ &\to& 自然言語が残っているか \\ \\&\to& 無いならチェック対象は加工済み \end{array}
まず「論理式への変換」はこんな感じ。
（これを通過できないものはそもそも数学では扱えない）
\begin{array}{ccc} チェック対象 &\to& 加工済み対象 &\to& 推件式？ \end{array}
その上で定義される
「推件式であるか」のチェック方法は
\begin{array}{lcl} 加工済み対象 &\to& 推件式の概形 Γ\vdash φ を目指す \\ \\ &\to& とりあえず記号 \vdash を置く \\ \\ &\to& φに該当する記号を\vdash の右側に置く \\ \\ &\to& Γに該当する記号を\vdash の左側に置く \\ \\ &\to& Γ \vdash φ に含まれない記号があるか \\ \\ &\to& 無いなら推件式である \end{array}
こんな感じになります。
（これにより「推件式の記号的な形」は完全に定義される）
それが証明であるのなら
以上のことが定義された時点で
『構文レベルの推件式』は定義できてるんですが
\begin{array}{ccc} 証明文 &\overset{何かしらの操作}{\longrightarrow}& 言い換えた証明文 \end{array}
『証明であるならこれができるはず』という
\begin{array}{ccc} 証明への操作 & \left\{ \begin{array}{lcccl} A,B\vdash φ &&\to&& B,A\vdash φ \\ \\ A,A\vdash φ &&\to&& A\vdash φ \end{array} \right. \end{array}
「推件式ならできるはずのこと」は
この時点ではまだ定義できていません。
（推件式を表現する記号の意味を考える段階の話）
シークエント計算 Sequent Calculus
|| シークエントの規則を元にした計算のこと
「推件式の振る舞い」から定義される『記号操作』
\begin{array}{ccc} 推件式 & \overset{推件式の振る舞い}{\longrightarrow} & 変更後推件式 \\ \\ A,A⊢φ &\to& A⊢φ \end{array}
「証明文の振る舞い」を利用したもの
（振る舞いをまとめたものが推件式全体への定義）
証明の自然言語表現と形式化
「振る舞い」と言うとちょっと曖昧ですが
\begin{array}{ccc} 自然言語表現 & & 感覚的統一 & & 記号表現 \\ \\ \\ \left( \begin{array}{c} AだしBだ \\ \\ AでありBだ \\ \\ \vdots \end{array} \right) &\to& \left(\begin{array}{ccc} Aだ＋Bだ \\ \\ A ∧ B \\ \\ \vdots \end{array}\right) &\to& A,B \end{array}
要はこういう感じの話で
（真と仮定された論理式という意味的定義がスタート）
\begin{array}{ccc} AでありBである &\Longleftrightarrow& BでありAである \\ \\ A,B &\Longleftrightarrow& B,A \\ \\ \\ AでありAである &\Longleftrightarrow& Aである \\ \\ A,A &\Longleftrightarrow& A \end{array}
「推件式の振る舞い」というのは
ここで許される記号操作のことを指しています。
（これを形式としてまとめたものが構造規則になる）
整理すると
\begin{array}{lcl} 意味的な要請 && 前提は全て真であるべき \\ \\ 直感的な観察 && 実際の証明文の振る舞い \\ \\ 直感的な構造 && 明らかに許される操作の発見 \\ \\ 記号的な定義 && 許される操作を記号的な確定操作へ \end{array}
定義はこのような階層に分けられています。
（一番下の段階まで整理されたものが構造規則と呼ばれる）
構造規則 Structure Rules
|| 証明でやって良いこと
「推件式の振る舞い」を記号操作としてまとめたもの
\begin{array}{ccl} L &=& φ_1,φ_2,...,φ_n &(0≤n) \\ \\ R &=& ψ_1,ψ_2,...,ψ_n &(0≤n) \end{array}
「コンテキスト」と呼ばれる記号 L,R を使って表現される
（「0個以上の論理式の有限列」の省略表現のこと）
\begin{array}{rcccr} L,A,B,R⊢φ &&→&& L,B,A,R⊢ φ \\ \\ L,A,A,R⊢φ &&→&&L,A,R⊢φ \\ \\ L,A,R⊢φ&&→&&L,A,B,R⊢φ \end{array}
こういった形の『許される記号操作』のことを
（ L,R を使うと「好きな位置の変更」をうまく定義できる）
\begin{array}{ccc} 直感的に発見される構造 &\to& 構造規則 \\ \\ ほぼ全ての文が満たす &\to& 満たすやつ全て \end{array}
「構造規則（推件式で許すべき記号操作）」と言います。
（「ほぼ全て」を「全て」にするためにルールとする）
転置規則 Permutation,Exchange
いわゆる「交換法則」に当たるもの
\begin{array}{c} L,A,B,R⊢φ &&→&& L,B,A,R⊢ φ \\ \\ Γ ⊢ L,A,B,R &&→&& Γ ⊢ L,B,A,R \end{array}
自然言語表現である ↓ を形式化した「構造規則」が
\begin{array}{ccc} AであるしBでもある &\to& BであるしAでもある \\ \\ AあるいはBである &\to& BあるいはAである \\ \\ Aである,Bである &\to& Bである,Aである \end{array}
「転置規則」と呼ばれるものになります。
（ \mathrm{and} も \mathrm{or} も含めて統一的に表現する形）
縮約規則 Contraction
同様にこれも直感的に当然の話で
\begin{array}{cc} L,A,A,R⊢φ &&→&& L,A,R⊢ φ \\ \\ Γ ⊢ L,A,A,R &&→&& Γ ⊢ L,A,R \end{array}
自然言語表現の「重複統合」の感覚を
\begin{array}{ccc} AであるしAでもある &\to& Aである \\ \\ AあるいはAである &\to& Aである \\ \\ Aである,Aである &\to& Aである \end{array}
そのまま記号的に表現したものになります。
（これと転置規則は直感的に明らか）
弱化規則 Weakening
問題となるこれは
「記号への意味的な要請的定義」に由来するもので
\begin{array}{cc} L,A,R⊢φ &&→&& L,A,B,R⊢ φ \\ \\ Γ ⊢ L,A,R &&→&& Γ ⊢ L,A,B,R \end{array}
「無関係な文（論理式）」を入れる
（真と仮定されているなら追加しても変化無し）
\begin{array}{lcl} Aである &\to& AでありBでもある && ？ \\ \\ Aである &\to& AあるいはBである && 〇 \end{array}
そんな記号操作を許可する規則になります。
（記号への意味的要請が無い場合は明らかに成立しない）
シークエント計算の記法
↑ で紹介した「構造規則」を用いたものが
「シークエント計算」なんですが
\begin{array}{ccc} L,A,R⊢φ &&→&& L,A,B,R⊢ φ \end{array}
これはこのままでは横に伸びてしまいます。
（これも計算の形の１つではある）
\begin{array}{ccc} 横表記だと & \left\{ \begin{array}{ll} 長くなると比較し辛い \\ \\ 単純に横方向のペースが不足する \end{array} \right. \end{array}
これによって起きる問題を解消したい
そんな要望によって得られた成果が縦に伸ばす記法で
\begin{array}{l} \mathrm{Permutation} && \displaystyle \frac{L,A,B,R\vdash φ}{L,B,A,R\vdash φ}(\mathrm{PL}) & \displaystyle \frac{Γ\vdash L,A,B,R}{Γ\vdash L,B,A,R}(\mathrm{PR}) \\ \\ \\ \mathrm{Contraction} && \displaystyle \frac{L,A,A,R\vdash φ}{L,A,R\vdash φ}(\mathrm{CL}) & \displaystyle \frac{Γ\vdash L,A,A,R}{Γ\vdash L,A,R}(\mathrm{CR}) \\ \\ \\ \mathrm{Weakening} && \displaystyle \frac{L,A,R\vdash φ}{L,A,B,R\vdash φ}(\mathrm{WL}) & \displaystyle \frac{Γ\vdash L,A,R}{Γ\vdash L,A,B,R}(\mathrm{WR}) \end{array}
これが「推件式計算」の基本的な表現方法になります。
（ ↑ から ↓ が導かれるという形で証明文の変形が表現される）
コンテキスト
「コンテキスト L,R 」という記号は
\begin{array}{ccc} コンテキスト &\Longleftrightarrow& 規則を適用しない記号の有限列 \end{array}
『変えない記号』を表すものなので
\begin{array}{c} A,B,C,D,E⊢φ &&→&& A,C,B,D,E⊢ φ \\ \\ A,B,C,D,E⊢φ &&→&& A,B,D,C,E⊢ φ \\ \\ A,B,C,D,E⊢φ &&→&& A,B,C,E,D⊢ φ \\ \\ A,B,C,D,E⊢φ &&→&& B,A,C,D,E⊢ φ \end{array}
「転置規則」による並べ替えを根拠とすると
\begin{array}{ccc} \displaystyle \frac{A,B,C,D,E\vdash φ}{A,B,D,C,E\vdash φ}(\mathrm{PL}) &&\to&& \displaystyle \frac{L,B,D,R\vdash φ}{L,D,B,R\vdash φ}(\mathrm{PL}) \end{array}
任意に「使わない記号」として整理され
（使わない記号を左か右に寄せればコンテキストへ）
\begin{array}{lcll} A,Bだけ変更 &\to& Lは無 & RはC,D,E \\ \\ B,Cだけ変更 &\to& LはA & RはD,E \end{array}
『統合（記号の有限列という意味は保持）』が可能になります。
（厳密には中身が変化する記号だが要請的意味は変化無し）
コンテキストの解釈
「中身に変更がある」のに
『同じ記号を使うのは変』じゃないか？
\begin{array}{ccc} 整理前コンテキスト &\to& 整理後コンテキスト \\ \\ L &\to& L^{\prime} \end{array}
これはもっともな指摘なんですが
\displaystyle \frac{L,A,B,R\vdash φ}{L^{\prime},B,A,R^{\prime}\vdash φ}(\mathrm{PL})
「別の記号を使う」と『見辛く』なります。
（その上コンテキスト自体はあまり重要では無い）
\begin{array}{ccc} 本筋とは無関係な記号 &\to& 変化を追う必要は？ \end{array}
なので「コンテキスト」の仕様として
『意味の消失と再定義が起きる』
\begin{array}{lcl} 規則適用前 && コンテキストはそのまま \\ \\ 規則適用 && 適用されない記号を左右に寄せられる \\ \\ L,Rの変更 && 適用されない記号をL,Rに吸収できる \\ \\ L,Rの初期化 && ここでL,Rの記号の中身を初期化する \\ \\ L,Rの再定義 && 記号L,Rを再利用することが可能 \\ \\ 規則適用後 && コンテキストの中身には変更があった \end{array}
これを予め定義しておくことで
\begin{array}{ccl} ↑ のL,R &\to& ↑ 時点でのみ同一 \\ \\ &\to& ↓ 時点では同一とは限らない \end{array}
この問題は解消することにします。
（この定義を根拠としないなら厳密には別記号が必要）
LKの推論規則
これに加える形で
「命題記号」や「述語記号」を入れたもの
\begin{array}{ccc} 純粋化された推件式 &\to& \mathrm{LK}の推論規則 \\ \\ 基礎的な振る舞い &\to& より実際的な振る舞い \end{array}
それが「LKの推論規則」と呼ばれるもので
「構造規則まで」が『純粋な推件式の体系』になります。