このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

ともかくシーケントなんだから、頼むよ、皆んな (A12)

RSS練習問題

※この記事は「記事12」

シーケントは論理の中核的な概念であり、演繹システムを構成するにしろ、意味論を考察するにしろ、シーケントを基本的対象物とみなすことなる（そうするのが、現状では最良の選択肢だと思われる）。

「シーケントとは何であるか？」という問に、「シーケントとはシーケントである」と答えるのが最も正確で安全なんだけど、それじゃー身も蓋もない。不正解さと誤解される危険を免れないが、シーケント周辺の余計な話を書いておく。「ちゃんとロンリする」際の必須のツールであるシーケントで挫折されては困るから。

※ 今回、練習問題はありません。が、問題意識についてはたくさん書いてます。

内容：

  1. ゲンツェンのLKシーケント計算をご存知の方への注意
  2. 定理記述としてのシーケント
  3. 形式化とシーケント
  4. 演繹システムへの意志を持ち続けること
  5. シーケントから、その先へ

ゲンツェンのLKシーケント計算をご存知の方への注意

検索などでたまたまここに辿り着いた人が誤解するのも困るので、毎回この節を冒頭に置くことにする。

  1. '⇒'は含意〈条件法〉の論理結合子で、'→'がシーケントの左右を区切る記号である。
  2. ゲンツェンのLKシーケントでは、左辺のカンマは連言的に、右辺のカンマは選言的に解釈をする。ここでのシーケントでは、出現位置の情報を使わずに、カンマは常に連言的であり、選言的な区切り記号に縦棒'|'を使う。
  3. (x∈R, n∈N) のような書き方は、集合論の命題ではなくて、自由変数の型宣言（のリスト）である。自由変数の型宣言のリストをコンテキストと呼ぶ。
  4. 暗黙のコンテキストを使う場合もあるが、できるだけ、シーケント内に明示的にコンテキストを書き込むようにしている。

定理記述としてのシーケント

シーケントの用途としては、まずは定理の記述に使えることは分かるだろう。

例えば、因数分解できれば2次方程式が解けることの根拠は、次の“定理”だと言えるだろう。



実数 a, b に対して、

実数 x に対して、

(x - a)(x - b) = 0 だとする。

これらから

  x = a

または

  x = b

が出る。

英語風だと、



For a, b∈R

For x∈R

Given (x - a)(x - b) = 0

Holds

  x = a

Or

  x = b

End

そしてシーケントは：

  • (a, b∈R), (x∈R), (x - a)(x - b) = 0 → x = a | x = b

自然数の引き算は出来るときと出来ないときがあるが、出来るのは次の“定理”があるからだろう。



自然数 n, m に対して、

n ≦ m だとする。

これらから

  ∃k∈N.(n + k = m)

が出る。

英語風だと、



For n, m∈N

Given n ≦ m

Holds

  ∃k∈N.(n + k = m)

End

そしてシーケントは：

  • (n, m∈N), n ≦ m → ∃k∈N.(n + k = m)

2次方程式の判別式が正ならば、（異なる）2つの解が存在することを主張する“定理”なら、いきなりシーケントで：

  • (a, b, c∈R), ¬(a = 0), b2 - 4ac > 0 → ∃s, t∈R.( ¬(s = t) ∧ (as2 + bs + c = 0) ∧ (at2 + bt + c = 0) )

フェルマー／ワイルズの“定理”なら：

  • (n∈N), n ≧ 3 → ¬∃x, y, z∈N.(xn + yn = zn)

形式化とシーケント

「命題」「定理」「証明」などの言葉は、現実世界で生きた人間が行う行為・活動としての数学のなかで使われる言葉である。現実世界で生きた人間が行う数学的行為・活動の一部をコンピューターで動作するソフトウェアシステムで実現しようとすると、「命題」「定理」「証明」などを、コンピューターが処理可能なデータとコンピューターが実行可能なアルゴリズムとして記述しなくてはならない。

我々現実世界に生活している人間達の言葉・概念を、コンピューターが扱えるナニカとして再定義する行為を形式化〈formalize〉と呼ぶ。「命題」に関しては、論理記号を使った論理式として満足できる形式化が出来ている。よって、「命題」という言葉は、コンピューターが扱えるナニカとしての意味でも使ってよい。

前節で「“定理”」という書き方をしていたが、これには理由がある。そう、形式化が済んでない。現時点において、

  • 形式化された命題 → 論理式として形式化が済んでいる
  • 形式化された定理 → よく分からない
  • 形式化された証明 → よく分からない

シーケントは、構文的形式〈syntactic form〉としては文句なく定義されている〈well-defined〉。命題と命題のリスト（連言的リストと選言的リスト）が定義されているなら、リストを左右に並べた形式がシーケントなのだから、文句の付けようがない。コンピューターが扱えるデータとしてシーケントを実装することも容易だ。興味ある人のために（ない人はスキップ）、TypeScriptによる*1データ型定義を書いておこう。

// 論理式
// それなりに複雑なツリー構造になる
// めんどくさいから省略
type Formula = /* ダミーとして文字列、うそぴょーん */string;

// 単一の型宣言
type TypeDecl = {
    varName: string,
    typeName: string// 本格的にしたいなら、型名ではなくて type expression
};

// コンテキスト ＝ 型宣言のリスト(配列ともいう)
type Context = Array<TypeDecl>;

// 連言的(conjunctive)か選言的(disjunctive)かの識別マーク
enum Junctive {
    CONJ,
    DISJ
};

// 連言的か選言的かマークされた、
// コンテキストと論理式が混じったリスト
// シーケントの左辺はこの形
type MarkedMixedList = {
    // 識別マーク
    mark: Junctive,
    // コンテキストと論理式が混じったリスト
    mixedList: Array<Context | Formula>
};

// 連言的か選言的かマークされた、
// 論理式のリスト
// シーケントの右辺はこの形
type MarkedList = {
    // 識別マーク
    mark: Junctive,
    // 論理式のリスト
    list: Array<Formula>
};

// シーケント
type Sequent = {
    left: MarkedMixedList,
    right: MarkedList
};

「シーケントとはシーケントである」とは、シーケントと呼ばれる構文形式に我々生きている人間がどのような思い〈感情〉を抱くかに関係なく、演繹システムが扱うデータとして文句なく定義されている〈well-defined〉のだから、それでいいだろう、ということだ。

シーケントの形式的定義については、次の記事を参照。

「シーケントとは定理の記述形式である」は、人間に対する説明としては悪くないが、演繹システム内における形式化された定理がよく分かんない現状では、形式的には（演繹システムに関する話題としては）なにごとも言ってない。演繹システムの外の世界＝我々が生きているこの世界における、雰囲気的・気分的な人間同士でしか通用しない他愛も無い語りに過ぎない。

演繹システムへの意志を持ち続けること

我々の目的は、演繹システムの外の世界＝我々が生きているこの世界における、雰囲気的・気分的な人間同士でしか通用しない他愛も無い語りを繰り広げることではない。人工的な演繹システムを構成し、その性質・能力を調べることである。この目的のために、心理的な状態を整備するために、人間同士のコミュニケーションとして、目的に至る手段として、他愛も無い語りを繰り広げることはあるだろうし、実際、今、それをしている。

演繹システムをどう作ろうか？ 演繹システムはどんな性質・能力を持つんだろうか？ という話では、雰囲気的・気分的な他愛も無い語りは何の意味も持たない。完全に形式化された正確な議論だけをし続けなくてはならない。これはけっこうシンドイ作業なのだ。

シンドイので、馴染みがあり楽ちんな我々が生きているこの世界における、雰囲気的・気分的な人間同士でしか通用しない他愛も無い語りへと逃げたい誘惑にかられる。あるいは、いつのまにか雰囲気的・気分的な他愛も無い語りをしてしまう。

例えば、「x + y ≧ 0」という命題は正しいだろうか？ 「正しくない気がする」としたら、正しくない根拠は何か？ 実際には正しくないのではなくて、単に解釈ができない。変数x, y の変域を明示して、

  • (x, y∈N) → x + y ≧ 0

なら正しい。しかし、

  • (x, y∈R) → x + y ≧ 0

なら正しくない。だが、条件（仮定）を足して、

  • (x, y∈R), x ≧ 0, y ≧ 0 → x + y ≧ 0

なら正しい。

今出したシーケント (x, y∈R), x ≧ 0, y ≧ 0 → x + y ≧ 0 が正しい理由・根拠が「正しいような気がするから」だとしたら、「俺は正しくないよう気がするから正しくないぞ」に対抗できない。

数理的な議論において、素朴集合論を信頼し、素朴集合論の内部で正当化できることは認めようというコンセンサスは得られている。「正しいような気がするから」ではなくて、テクニカルタームとしての「正しい」として、素朴集合論の内部で正当化できる定義と計算法を提示できるならば、もはや雰囲気的・気分的な語りではなくて、数理的な議論の一部になる。

実際に、命題の形式化であるところの論理式に対して、その正しさ（の程度）を出力する関数としてスコット・ブラケットを定義して、スコット・ブラケットの値により「正しさ」は定義している。論理式は構文的対象物〈syntactic object〉であり、その全体は（素朴集合論で認められる）集合となり、スコット・ブラケットはその集合を域〈domain〉として、適当な集合Xのベキ集合Pow(X)を余域〈codomain〉とする関数である（Xはコンテキストの領域なので、コンテキストに応じてXも変化する）。

素朴集合論で認められる集合、写像、集合演算、集合の比較などを使って「正しさ」を定義したのなら、その「正しさ」概念は、「素朴集合論の内部で正当化できることは認めようというコンセンサス」のもとで正当かつ正確な意味を持ち、雰囲気的・気分的な語りではなくなる。

我々が、演繹システムを、理論的な構築物として、あるいは実際にコンピューターで動くソフトウェアとして実現しようとするとき、その入力データや内部処理データが何であるかが分からないでは話にならない。そこで、論理式、論理式のリスト、シーケントなどを、「素朴集合論の内部で正当化できることは認めようというコンセンサス」に合致する形で定義する必要があった。

仮に我々が、演繹システムを作ったとして、その挙動が期待通りかどうかをテストするとき、「システムの応答が期待通りか、期待外れか」を、システムの外部にいる我々が判断できなかったらどうにもならない。「なんか、うまく動いているような気がする」「いや、どうも奇妙な感じが俺はする」じゃ埒が明かない。その話を昨日「シーケントに親しもう」の後半でした。

シーケントから、その先へ

シーケント概念を十分に説明したわけではないが、シーケントという構文的対象物を定義して、ベキ集合に値をとる関数であるスコット・ブラケットも定義する必要性・必然性があったことは、ある程度は同意いただけたろう。

しかし、「定理」も「証明」も形式化が全然出来てない。現時点では、「定理」「証明」などの言葉はインフォーマルに（人間同士のコミュニケーションにおいて雰囲気的・気分的に）しか使えない。今後、「定理」や「証明」を形式的に扱うためのデータ構造やアルゴリズム（処理方式）を、「素朴集合論の内部で正当化できることは認めようというコンセンサス」に合致する形で定義していくことになる。雰囲気的・気分的な語りでお茶を濁すわけにはいかない。

※注意： 実際には、「定理」「証明」という言葉は形式化しないかも知れない。理由は、形式化された定理、形式化された証明の意味があまりにもバラバラ色々すぎるので、使わないのが無難と思われるから。「推論」「リーズニング」という言葉を選んで形式化すると思う、たぶん。

*1:TypeScriptの型定義構文は、かつて僕等が作っていた某システムの構文とあまりにも似ていて、僕には書きやすい。