日本語表現、非形式的記号表現、形式的記号表現 (G2 A3P2)

※この記事は「記事3 問題集2」

内容:

人間とシステム

演繹システム〈deduction system〉とは、人間の論理的行為/論理的能力をシミュレート〈模倣〉するソフトウェア・システムだと思えばよい。演繹システムは、人間がゼロから作り出す完全に人工的なシステムである。自然物や神様がくれるモノではない!

演繹システムは人工物なので、そこで使うデータの形式や処理のアルゴリズムは、ゼロから設計・定義・構成する必要がある。前もって自然にあるモノではないし、神様が決めてくれるモノでもない。

人間の行為/能力をシミュレートするので、

  • データは、人間の使っている言語に似ているほうがよい。
  • 動作は、人間が行っている行為に似ているほうがよい。

だが、

  • データは、人間の使っている言語(日本語や英語)と同じではない。
  • システムの内部動作が人間と同じかどうかを確認する方法がない(人間の脳や知的行為の内部メカニズムが分かってない)。入出力が似ていることは実験によりある程度確認できる。

次の混同・混乱はしばしば起こり、数理論理学を学ぶ上での大きな障害になっている。

  • 人間の使っている言語と、演繹システムが使うデータが区別できない。ゴッチャにしてしまう。
  • 人間の行為と、演繹システムの動作を区別できない。ゴッチャにしてしまう。

人間の言語/行為と、演繹システムのデータ/動作がシッカリ区別できるようになれば、数理論理学の議論は通常の数学としてスムーズに進行する。

[補足]
数理論理学は数理科学〈mathematical science〉であって、巷の「論理的な話し方・考え方 講座」などでやっている“論理”とはまったく違う。数理論理学で最初に行うことは、人間が使っている言語の一部と人間が行っている知的行為の一部を数学の土俵に乗せることである。この最初のセットアップが出来ないと、スタートが切れない。

最初のセットアップとはつまり、演繹システムの設定である。数理論理学の対象物が演繹システムなのだから、演繹システムがないとはじまらない。演繹システムは、人間の行為/能力をシミュレートする目的で設計・定義・構成されるが、一度作られてしまえば、それは現実世界とは別なシステムとなる。現実世界と混同してはならない。[/補足]

三種の表現の区別

日本語による表現は、作為的に記号を使わないようにする。例えば、「1 + 3」を「一足す三」のように。実際には、記号を使わないで日本語だけの表現を使うことはないのだが、対比を強調するためにわざとらしい日本語表現を使う。

演繹システムの入力/出力/処理に使われるデータとしての命題を論理式〈formula〉と呼ぶ。論理式を構成する中間段階で、次のような記号的表現も必要になる。

  1. 定数記号: 1, 3, 258, π など
  2. 変数記号: x, y, z, a, b, c など
  3. 演算子記号、関数記号〈関数名〉: +, ×, - など*1
  4. 関係記号: =, >, <, ≧, ≦ など

これらの記号は、既に日常的に使われているものをそのまま使う。例えば、我々が日常使っている式「x + 2×y」に対応する演繹システムのデータも「x + 2×y」とする(のが普通)。

ただし、見た目が同じでも目的が異なる(人間のコミュニケーション用と、システムの入力/出力/処理用)ので、演繹システムのデータは二重引用符で囲むことにする。

  • 人間のコミュニケーション用は、x + 2×y
  • システムの入力/出力/処理用は "x + 2×y"

話がややこしくなるのは論理記号である。論理記号は、基本的には演繹システムのデータとして使う。しかし、人間のコミュニケーションでも使いたい。

  • 目的1: 論理記号は、演繹システムのデータとして使う。
  • 目的2: 論理記号を、人間のコミュニケーションでも使いたい。

二つの目的に同じ論理記号を使うと、シッチャカメッチャカになるので、人間のコミュニケーション用の論理記号は丸括弧で囲むことにする。

日本語 人間のコミュニケーション用論理記号 システムのデータ用論理記号
かつ (∧)
または (∨)
ではない (¬)
ならば (⇒)
任意の (∀)
存在する (∃)

システムのデータ用ではなくて、人間のコミュニケーション用に使う論理記号をメタ論理記号〈meta logical symbol〉と呼ぶ。今導入したルールは:

  • メタ論理記号は、論理記号を丸括弧で囲む。

システムのデータ用ではなくて、人間のコミュニケーション用に使う論理式をメタ論理式〈meta formula〉と呼ぶ。メタ論理式は人間のコミュニケーション用なので、役割は日本語と同じであるし、日本語に置き換えることができる。

  • メタ論理式は、使ったほうがコミュニケーションが正確になるが、使わないで済ませることができる。

建前としては「メタ論理記号/メタ論理式はなくてもよい」のだが、本音としては「メタ論理記号/メタ論理式を一切使わないのは辛すぎる!」ので、使いますよ

「論理記号」/「論理式」に限らず、「人間が使う/人間が行っている」「通常の数学の」という意味で、形容詞「メタ」を付ける。「メタ」という言葉に、「人間を超えている」とか「通常以上の」という意味はまったくないので注意!

日本語表現、メタ記号表現、記号表現(練習問題あり)

ここから先、三種の表現を、「日本語表現」「メタ記号表現」「記号表現」と呼ぶ。

  • 日本語表現: 日本語による表現だが、作為的に記号の使用を避けている表現。
  • メタ記号表現: 人間どうしのコミュニケーション用の記号表現。メタレベルの表現/形式化されてない表現/非形式的な表現ともいう。既に日常的に使っているものもある。
  • 記号表現: 演繹システムの入力/出力/処理に使うデータとしての記号表現。見た目が同じでも、人間のコミュニケーション用とは別物。二重引用符で囲むことにする。

三種の表現の、幾つかの例を挙げる。コンテキスト(変数の変域指定)が省略されているが、すべての変数はN(自然数の集合)上を動くとする。日本語における変数は「甲乙丙丁戊己庚辛壬癸」(十干*2)を使う。

日本語表現 メタ記号表現 記号表現
3 "3"
一足す三 1 + 3 "1 + 3"
甲、乙、丙 x, y, z "x", "y", "z"
甲に三を足す(甲と三の和) x + 3 "x + 3"
甲に乙の百倍を足す x + 100×y "x + 100×y"
甲は零より大きい x > 0 "x > 0"
甲は零より大きい かつ 乙は一以上 x > 0 (∧) y ≧ 1 "x > 0 ∧ y ≧ 1"
甲は零より大きい ならば 乙は一以上 x > 0 (⇒) y ≧ 1 "x > 0 ⇒ y ≧ 1"
自然数である任意の甲に対して、「甲は零より大きい ならば 乙は一以上」 (∀)x∈N.(x > 0 (⇒) y ≧ 1) "∀x∈N.(x > 0 ⇒ y ≧ 1)"

コンテキストの書き方は次のように約束しよう(もちろん、ここだけのローカルルール)。

日本語表現 メタ記号表現 記号表現
甲は実数だとして、… For x∈R, … "x∈R | …"
甲は実数、乙は自然数だとして、… For x∈R, y∈N, … "x∈R, y∈N | …"
(甲, 乙) は実数と自然数の対だとして、… For (x, y)∈R×N, … "(x, y)∈R×N | …"

「2次方程式の判別式が非負なら、その2次方程式は解を持つ」は、さまざまな表現の仕方があるが、(作為的な)日本語表現で書けば:

  • 甲、乙、丙は実数だとして、甲は零ではない かつ 「乙の平方と「甲と丙の積の四倍」との差」が零以上 ならば 実数である丁が存在して、「「甲と「丁の平方」の積 と 乙と丁の積 と 丙」らの和」が零 となる。

この鬱陶しさ*3を見れば、日常的にも記号表現を使わざるを得ないことが分かるだろう。

  1. 練習問題: 上の日本語表現を、コンテキストを表す「For …」とメタ論理記号を使って、メタ記号表現に“直訳”せよ。
  2. 練習問題: 同様に、上の日本語表現を記号表現(演繹システムが使うデータ)に“直訳”せよ。

練習問題: 日本語表現 → メタ記号表現、記号表現

以下の日本語表現を、メタ記号表現(人間のコミュニケーション用だが記号を使用)と記号表現(演繹システムのデータ)に翻訳せよ。記号表現は二重引用符で囲むこと。なお、命題としての真偽は問題にしてない、表現の書き換えだけをする。

  1. 二百五十八
  2. 円周率の二倍
  3. 二百五十八と円周率の二倍との差
  4. 円周率の二倍は二百五十八に等しい。
  5. 円周率の二倍は六以上である。
  6. 甲、乙は自然数として、甲と乙の和
  7. 甲、乙は実数として、甲と円周率の二倍との差*4
  8. 甲、乙は自然数として、甲と乙の和は乙と甲の和に等しい。
  9. 甲、乙は実数として、甲と乙の和は乙と甲の積より大きい。
  10. 甲、乙、丙は実数として、「甲と丙の積」と乙との和は零に等しい。
  11. 甲、乙、丙は実数として、「甲と丙の積」と乙との和は零に等しくない。
  12. 甲、乙は実数として、甲の三倍と乙との和は零に等しくない。
  13. 甲、乙は実数として、甲は零以上 かつ 乙は零以上 ならば 甲と乙の和は一 である。
  14. 甲、乙は自然数として、甲と乙の積はニと等しい。
  15. 甲は自然数として、自然数である乙が存在して、甲と乙の積はニと等しい。*5
  16. 甲は自然数として、実数である乙が存在して、甲と乙の積はニと等しい。
  17. 甲は自然数として、実数である任意の乙に対して、甲と乙の積はニと等しい。
  18. 甲は実数として、「自然数である任意の乙に対して、甲と乙の積は零と等しい」ならば 甲は一に等しくない。
  19. 甲は実数として、「自然数である任意の乙に対して、甲と乙の積は零と等しい」ならば「実数である丙が存在して、甲と丙の積は一に等しい」。
  20. 実数である任意の甲に対して、実数である任意の乙に対して、「甲が零以上 かつ 乙が零以上」ならば 甲と乙の和は零以上である。

練習問題: 記号表現 → メタ記号表現

我々の記号・記法の約束では、記号表現 → メタ記号表現 の翻訳はきわめて簡単である。

  1. 二重引用符を外す。
  2. 論理式をメタ論理記号(丸括弧付き)に置き換える。

これは、メタレベル(人間どうしの日常・通常のコミュニケーション)と演繹システムのデータをできるだけ似せる設計方針だからである。しかし、演繹システムはゼロから設計・定義・構成していくので、「メタレベルに似せないといけない」という縛りはない。システムの設計者は、自分の目的と好みに応じて、自由に設計してよい。既存の演繹システムは、各設計者(論理学者)が恣意的に自由に(つまり、てんでんばらばらに)設計したものである。

次の設計方針を採用するとしよう。

  1. 定数記号と変数記号はメタレベル(人間どうしの日常・通常のコミュニケーション)と同じ。
  2. 足し算の演算子記号を"□"とする。
  3. 掛け算の演算子記号はなし、代わりに関数記号"mul"(multiplyから)を使う。
  4. 関係記号(等号、不等号)はメタレベル(人間どうしの日常・通常のコミュニケーション)と同じ。
  5. 論理記号は以下のようにする。
日本語 論理記号 備考
かつ ナカグロ記号
または 二重の縦棒
ではない 後置で使う
ならば よく使われる含意記号
任意の 通常の「かつ」を別用途に転用
存在する 通常の「または」を別用途に転用

この設計方針で作られた演繹システムの記号表現(演繹システムのデータ)を考える。メタ記号表現と記号表現との対応を幾つか挙げる。

メタ記号表現 記号表現 備考
3 "3" 同じ
1 + 3 "1 □ 3" 足し算は"□"
x, y, z "x", "y", "z" 同じ
x + 3 "x □ 3" 足し算は"□"
x + 100×y "x □ mul(100, y)" 掛け算は"mul"
x > 0 "x > 0" 同じ
x > 0 (∧) y ≧ 1 "x > 0 ・ y ≧ 1" 「かつ」はナカグロ
x > 0 (⇒) y ≧ 1 "x > 0 ⊃ y ≧ 1" 「ならば」は、論理界隈では標準的記号の"⊃"
(∀)x∈N.(x > 0 (⇒) y ≧ 1) "∧x.(x > 0 ⊃ y ≧ 1)" "∧"を転用
(¬) y ≧ 1 "y ≧ 1 ~" 否定記号は後置、日本語と同じ語順

コンテキストの表現は、縦棒で区切る方式を引き続き採用する。

練習問題: 次の記号表現(演繹システムのデータ)を、メタ記号表現(常識に近い、人間のコミュニケーション用の記号表現)に翻訳せよ。

  1. "1□2"
  2. "mul(mul(2, 3□5), 100)"
  3. "mul(1, mul(100, mul(2, 3)))"
  4. "x, y∈R | x □ mul(2, y)"
  5. "x∈R | mul(x, x) = 1 ⊃ (x = 1 ‖ x = -1)"
  6. "x, y∈N | ∨c∈N.(y = mul(x, c))"
  7. "a∈N | ∨x∈N.∨y∈N.(a = mul(x, y) ⊃ (x = 1 ‖ y = 1))"
  8. "∧x∈R.(x = 0 ~ ⊃ ∨y∈R.(mul(x, y) = 2))"
  9. "a, b∈R | (a > 0 ・ b > 0) ⊃ ∨n∈N.(mul(n, a) > b)"
  10. "∧a∈R.∧b∈R.(mul(a, b) = 0 ~ ⊃ (a = 0 ~)・(b = 0 ~))"

練習問題: 前節の練習問題の日本語表現(20個)を、この節で定義した記号表現に翻訳せよ。

*1:マイナス記号は、引き算の二項演算子記号と、符号反転の単項演算子記号の両方で使われている(多義的使用〈オーバーロード〉という)。多義的記号〈オーバーロードされた記号〉は、その扱いを事前にハッキリさせておく必要がある。

*2:十干の本来の意味は無視して、単なる変数記号として使う。実際に契約書などで、「甲」「乙」を単なる変数記号として使っている。

*3:鬱陶しいだけでなく、区切り目がよく分からない。事前の知識なしに区切り目が判読できるようにするには、もっと鉤括弧が必要だろう。

*4:コンテキストに出現した変数をすべて使う必要はない。例えば、"x, y, z∈R | x2 + 1" や "x, y, z∈R, a∈N | y≦z" は何の問題もない。

*5:自然数と実数の足し算や掛け算をどう定義するかは事前に決めておく必要がある。ここでは、自然数を実数とみなして演算して、結果は実数だとする。

第1回 宿題+追加説明

以下のナントカの例に対して、実例がほんとにナントカであることを証明(自分で確信が持てるまで確認)せよ。素材である集合と関数は与えられているので、法則を満たすことを証明すればよい。

モノイドの例

モノイドの定義は p.9。

  1.  
    1. Nは特定の集合(自然数の集合)
    2. モノイドの書き方は p.9
  2. N≧1 = {n∈N | n≧1}
  3. Mat[N](2, 2), ・, I2 は行列の圏の説明参照。I2 = I(2)
  4. max(x, y) = if (x ≦ y) y else x
  5.  
    1. ∞ は自然数でなければなんでもいい。順序の定義は下の個別固有な定義を参照
    2. min(x, y) = if (x ≦ y) x else y
  6.  
    1. ⊥はなんでもいいが、Xには含まれないモノ。記号'⊥'('T'のひっくり返し)は「ボトム」と呼ぶ。
    2. leftは、下の個別固有な定義を参照
  7. プラス記号をオーバーロードしている。通常の足し算とは違う。下の個別固有な定義を参照。「「イチ、ニ、サン、イッパイ」の算数と分配代数」も参照。
  8. Pow(X)、∪、∅ は、別資料「補足: 基本的な概念・用語」参照。参照しても説明はないけど。
  9. ∩も、別資料「補足: 基本的な概念・用語」参照。
  10. △は、下の個別固有な定義を参照。
  11. ♡は、下の個別固有な定義を参照。
  12.  
    1. 一般に、集合 A, B に対して、Map(A, B) は、AからBへのすべての写像からなる集合。
    2. ; は写像の結合〈合成〉の図式順〈{diagrammatic | graphical | pictorial} order〉演算子記号。図式順とは「左が先〈前〉、右が後」の順序のこと。
    3. idXは、集合Xの恒等写像。∀x∈X. idX(x) = x
  13. X*、#、ε については、「補足: 基本的な概念・用語」のリストのところを参照。
  14. 自明モノイドとは、要素がただ1つであるモノイド。
半環の例

半環の定義は p.9。

  1. お馴染みだろう。
  2. 行列の圏の説明参照。
  3. 間違い訂正して max。
  4. Xの部分集合の半環、∪が足し算。
  5. Xの部分集合の半環、∩が足し算。
  6. 間違い訂正して max, 1。△は、下の個別固有な定義を参照。
  7. (M, ・, e) はモノイドで、
    1. ∪、∅ は集合の演算と空集合。
    2. A, B∈Pow(M) に対して、A◎B = {x・y∈M | x∈A かつ y∈B}
  8.  
    1. MonMap(N, N) = {f:NN 写像 | ∀n, m∈N. f(n + m) = f(n) + f(m)} = (足し算すると値も足し算になる写像の集合)
    2. 写像の足し算は、(f + g)(n) = f(n) + g(n)
    3. ∀n∈N. C0(n) = 0
    4. ; は写像の結合〈合成〉の図式順演算子記号。
    5. IdNは、Nの恒等写像。大文字'I'になっているのに意味はない。
順序集合の例

順序集合の定義は p.8。

  1. お馴染みだろう。
  2. お馴染みだろう。
  3. 集合の包含関係、お馴染みだろう。
  4. A, B∈Mat[N](2, 2) に対して、A≦B ⇔ ∀i, j∈{1, 2}. Ai,j ≦ Bi,j
  5. (A, ≦) を順序集合として、f, g∈Map(X, A) に対して、f≦g ⇔ ∀x∈X. f(x)≦g(x)
  6. (n, m), (n', m')∈N2 に対して、(n, m)≦(n', m') ⇔ n≦n' かつ m≦m'
  7. これは次回説明する。
圏の例

圏の定義は p.10。

  1. しりとりの圏 →「はじめての圏論 その第1歩:しりとりの圏」参照
  2. 行列の圏 →「はじめての圏論 その第2歩:行列の圏」参照
  3. p.7 の「そう言えば」の圏

[補足]「そう言えば」の圏は、サンプルのために作為的にでっち上げた印象があります。が、少し変更すると、特定の状況で実際に出現する圏です。

有限体の圏をFinFieldとします。FinFieldの射は、体の拡大(体のあいだの単射準同型写像)とします。有限体Fの、集合としての基数〈cardinality〉を card(F) とします。i:F→F' という拡大(単射)が存在するなら、crad(F)はcard(F')の約数になるので、card:FinField→(Nの約数倍数順序からのやせた圏) という関手になります。この関手の像圏は、「そう言えば」の圏を少し縮めたものです。[/補足]

第1回 正誤表

配布印刷物の誤りとその訂正。ご指摘、ご協力ありがとうございます。

ページ番号 場所
1 全般的な注意の次の行 言った(はず)だが 言った(はずだ)が
1 なかほど 約語 訳語
1 なかほど transformatioin transformation
4 最初の箇条書き4番 min (2箇所) max
4 最初の箇条書き5番 max (2箇所) min
4 二番目の箇条書き8番 min max
4 二番目の箇条書き10番 max min
5 半環の例の3番 min max
5 半環の例の6番 min max
5 半環の例の6番 0 1
5 半環の例の8番 ∘ IdN ∘, IdN
5 見出し 準備集合 順序集合
7 注意事項の1番 : (2箇所) ;
8 順序集合 順j集合 順序集合
9 左単位的マグマの書き方 (A, m) (スライドも) (A, m, ℓ)
9 有向グラフ cod::X→A cod:X→A
10 cod::X→A cod:X→A

丸括弧より山形括弧('〈'と'〉')のほうがふさわしい所が何箇所かありますが、それはいいとします。

他にまだ誤りがありましたら、twitterツイート内に文字列 @m_hiyama を含めれば(メンション)通知が来ます。ただし、メンションの内容自体はタイムラインに表示されるので、プライベートなやり取りにはなりません。LINEコミュニティ経由の連絡なら(ある程度は)プライベートです。公開されている檜山のメールアドレス宛メールでもかまいません。

現実世界の不整合や不合理は受け入れよう

※この記事は「記事2」

なんか社会問題を論じようとしているわけじゃないですよ。論理〈数理論理 | 形式論理〉での話。

僕(檜山)の経験・観測によると、言葉や記号へのこだわり・固執や、現実には存在しない整合性を期待していることが、学習を阻害していることが思いのほか多い*1。こういうこだわりや期待は、早急に捨てましょう。

論理に限らず、たいていの分野でそうだと思うのだけど; 用語と記法は、歴史的経緯とかその他の事情により、グチャグチャで混乱している。暗黙の省略や独特の習慣もある。それは致し方ない。改善される見込みはまったくない。そういうものだと諦める。

事実として、混乱して不合理な用語法・記法があるのだが、それに惑わされ学習が阻害されないように、自分で気をつけるしかない。

  1. たくさんの同義語のなかから、自分の好みのものをひとつ選んでそれを使う。
  2. 類義語の微妙なニュアンスは人により解釈が違う。神経質にならない。気にしてもしょうがない。
  3. 語源やエピソードを調べることは、(それが好きなら別にかまわないが)時間・手間がかかり過ぎるし得るものも少ないので推奨しない。
  4. 今まで使っていた用語法・記法が拡張/一般化されるとき、抵抗しないでサッサと乗り換える。
  5. 別な人が、自分と違う用語法・記法を使っていても目くじらを立てない。用語法・記法に、どれが正しいなんてない -- どうせ偶発的・恣意的に決まり、惰性で使い続けているだけだから。
  6. 自分と違う用語法・記法を使っている人と対話が必要なときは、相手の用語法・記法を調べて、コミュニケーションが成立するように努力する。
  7. どのような分野の用語法・記法もローカル・ルールである。グローバル・スタンダードを期待しても、そんなものはほとんどない(稀に存在するが)。
  8. そもそも、ヒルベルトが言うように、ネーミング/ラベリングを変更しても理論そのものへの影響はない。ネーミング/ラベリングは何でもいいのだから、それにこだわることに(心理的以外の)意味はない。

もちろん、とはいえ、自分で用語や記号を選ぶときは、自然言語からみても心理的(あるいは教育的)にも適切なものを選ぶべきだけど、事実として不適切/不合理な用語法・記法があるのだら、それはもうしょうがない。

*1:[追記]比較的最近、ここ数年くらいの経験・観測です。言葉にこだわる人が多い(比率が高い)ことと、極端にこだわる人がいることに、僕はビックリしてしまいました。「言霊とはこういうことなのか」と思ったくらい。「正確な記述と演繹のための非日本語記法」参照。[/追記]

命題と、そのコンテキスト/真理集合 (G2 A1P1)

※この記事は「記事1 問題集1」

与えられた論理式〈形式化された命題〉に対して、そのスコット・ブラケットを実際に計算する練習。スコット・ブラケット(の値)と真理集合は同じもの。予備知識として、中学・高校で習った、方程式・不等式と図形の関係が必要になる。

「もう分かった。同じタイプの問題をこれ以上やり続けるのは辛い。」と感じたらやめてよい。逆に、「もっと練習したい。」と感じたら、同種の問題を自作するのは容易だから、作って解く。

内容:

正しさの程度を測ること

「たかし君よりゆかりさんのほうが背が高いんじゃないの」
「いや、ゆかりさんは女の子だから、大きく見えるだけだよ」
「そうじゃなくて、ゆかりさん、ほんとに大きいよ」
「俺はたかし君が大きいと思うな、感じとして」

こんな話をグダグダしていても埒が明かない!

人の量的属性である身長について語っているのだから、適切な測定装置 -- つまり身長計で測ればいい。測った結果が、

  • たかし 161.3cm
  • ゆかり 162.1cm

であれば、「ゆかりさんのほうが背が高い」が正しい。身長計を使えば、「クラスのなかで誰が一番背が高いか?」も疑義なく明白に決定できるだろう。

数理的手法、あるいは自然科学一般の方法論は、対象物の属性を適切な測定装置で測ることを基本とする。ときには、複数の測定値を組み合わせた計算値として結果が得られることもある。例えば、肥満度を表すBMI(Body Mass Index)は、身長と体重から計算される量的属性である。

測定値(算出された値も含む)の集合として、自然数N(個数)や実数R(連続量)だけではなくて、集合Xのベキ集合Pow(X)を使うこともできる。命題の「正しさ」の測定値は実際Pow(X)に値をとる。

「(x∈R| x2 > 0) より (x∈R| ¬(x = 0)) のほうが正しいんじゃないの」
「いや、(x∈R| ¬(x = 0)) は否定が入ってるから、より正しいように見えるだけだよ」
「そうじゃなくて、(x∈R| ¬(x = 0))、ほんとに正しいよ」
「俺は (x∈R| x2 > 0) がより正しいと思うな、感じとして」

こんな話をグダグダしていても埒が明かない!(2回目) サッサと正しさの程度を適切な測定装置で測って比べなさい。その測定装置がスコット・ブラケットというものだ。対象物(今は命題)に対して、雰囲気的に語ったり、思弁的に論じたり、私的感慨を縷縷述べあり、そんなことをしても何も始まらない。グダグダ言ってないでチャンと測りましょうね。

限量子を含まない閉論理式

次の等式/不等式の組み合わせは、閉論理式(自由変数をまったく含まない論理式)である。その真偽を常識的に解釈して、スコット・ブラケットを使って記述せよ。

例: 〚1 + 1 = 2〛 = 1, 〚1 > 3〛 = 0. 〚1 > 3 ∨ 1 = 1〛 = 1

もう少し複雑な例題をやっておく。

  • 1 + 1 = 2 ⇒ ((2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5) のスコット・ブラケットを計算せよ。

混乱を避けるために、真偽値(1 = {0} の部分集合)としての 0, 1 は 0, 1 (太字)と書く。自分で計算するときは、0, 1 (普通の太さ)でも混乱はないだろう。記号 '⇒' を集合演算の意味でもオーバーロードして使う。下の「:=」は、左側を右側のように定義する、という意味。

  • (なんかの親集合の)部分集合 V, W に対して、 V ⇒ W := Vc ∪ W

この書き方を使うと:

  • 〚A ⇒ B〛 = 〚A〛 ⇒ 〚B〛

左側の'⇒'は論理結合子、右側の'⇒'は集合演算である。

例えば次のように計算するが、この計算は、Pow(1) = {0, 1} における部分集合の計算である。

〚1 + 1 = 2 ⇒ ((2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5)〛
 = 〚1 + 1 = 2〛 ⇒ 〚(2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5 〛
 =  1c ∪ 〚(2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5 〛
 =  0 ∪ 〚(2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5 〛
 = 〚(2 ≦ 1 ∧ 2 ≦ 3) ⇒ 1 + 2 > 5 〛
 = 〚2 ≦ 1 ∧ 2 ≦ 3〛 ⇒ 〚1 + 2 > 5〛
 =  (〚2 ≦ 1〛∩〚2 ≦ 3〛) ⇒ 〚1 + 2 > 5〛
 =  (01) ⇒ 〚1 + 2 > 5〛
 =  0 ⇒ 〚1 + 2 > 5〛
 =  0c ∪ 〚1 + 2 > 5〛
 =  1 ∪ 〚1 + 2 > 5〛
 =  1

以下、練習問題。

  1. 1 + 2 = 3
  2. 1 + 2 < 3
  3. 12 = 22
  4. 3 ≦ 5 ∧ 3 ≦ 3
  5. 1 + 2 < 3 ⇒ 12 = 22
  6. 1 + 2 < 3 ∨ 12 = 22 ∨ 3 ≦ 3
  7. (3 ≦ 5 ∧ 3 ≦ 3) ⇒ 1 + 2 < 3
  8. (3 ≦ 5 ∨ 3 ≦ 3) ⇒ ¬(1 + 2 < 3)
  9. ¬(1 + 2 < 3) ⇒ (1 + 2 = 2)
  10. 1 + 2 = 3 ⇒ (1 + 2 < 3 ⇒ 12 = 22)

※注意: 閉論理式は、空なコンテキストを持つコンテキスト付き論理式とみなせる。例えば、1 + 2 = 3 は (| 1 + 2 = 3) である。

限量子を含む閉論理式

次の論理式は変数を含むが、変数が限量子で束縛されているので閉論理式である。その真偽を常識的に解釈して、スコット・ブラケットを使って記述せよ。

例: 〚∀x∈R.( x2 ≧ 0 )〛 = 1, 〚∃x∈R.( x2 < 0 )〛 = 0

  1. ∀n∈N.(n ≧ 0)
  2. ∃n∈N.(n < 0)
  3. ∀n∈N.∃m∈N.(m ≧ n)
  4. ∀n∈N.∃m∈N.(m < n)
  5. ∀x∈R.∃y∈R.(y2 = x)
  6. ∀x∈R.∃y∈R.(x ≧ 0 ⇒ y2 = x)
  7. ∃y∈R.∀x∈R.(x ≧ 0 ⇒ y2 = x)
  8. ∀x∈R.∀y∈R.∃n∈N.((x ≧ 0 ∧ y > 0) ⇒ yn ≧ x)

※注意:限量子を含む閉論理式も、空なコンテキストを持つコンテキスト付き論理式とみなせる。例えば、∀n∈N.(n ≧ 0) は (| ∀n∈N.(n ≧ 0)) である。

念のため(?)、感情表現をタップリ混じえた日本語で表現しておく。

  1. ∀n∈N.(n ≧ 0) : 自然数nをどんなに勝手に選んだところで、n ≧ 0 である。
  2. ∃n∈N.(n < 0) : n < 0 である自然数nが、頑張って探せば必ず見つかる。
  3. ∀n∈N.∃m∈N.(m ≧ n) : 自然数nをどんなに勝手に選んだところで、m ≧ n である自然数mが、頑張って探せば必ず見つかる。
  4. ∀n∈N.∃m∈N.(m < n) : 自然数nをどんなに勝手に選んだところで、 m < n である自然数mが、頑張って探せば必ず見つかる。
  5. ∀x∈R.∃y∈R.(y2 = x) : 実数xをどんなに勝手に選んだところで、 y2 = x である実数yが、頑張って探せば必ず見つかる。
  6. ∀x∈R.∃y∈R.(x ≧ 0 ⇒ y2 = x) : 実数xをどんなに勝手に選んだところで、 「x ≧ 0 ならば y2 = x」である実数yが、頑張って探せば必ず見つかる。
  7. ∃y∈R.∀x∈R.(x ≧ 0 ⇒ y2 = x) : どんなに勝手に選んだ実数xに対しても「x ≧ 0 ならば y2 = x」である実数yが、頑張って探せば必ず見つかる。
  8. ∀x∈R.∀y∈R.∃n∈N.((x ≧ 0 ∧ y > 0) ⇒ yn ≧ x) : 実数xをどんなに勝手に選んだところで、実数yをどんなに勝手に選んだところで、「(x ≧ 0 かつ y > 0) ならば、yn ≧ x」となる自然数nが、頑張って探せば必ず見つかる。

コンテキスト付き論理式

※注意: 自由変数を含む論理式にコンテキストがないと、解釈不可能・意味不明なので、単に「論理式」と言った場合でも、たいていはコンテキスト付き論理式を意味する。

Rは直線、R2 = R×R は平面とみなして、次のコンテキスト付き論理式のスコット・ブラケットを図示せよ。

例: コンテキスト付き論理式 (x∈R| x + 1 ≦ 3 ∧ -1 ≦ x) のスコット・ブラケット 〚(x∈R| x + 1 ≦ 3 ∧ -1 ≦ x)〛 = 〚x∈R| x + 1 ≦ 3 ∧ -1 ≦ x〛 は、集合 {x∈R| x + 1 ≦ 3 ∧ -1 ≦ x} のことだから、図としては、直線内の区間 [-1, 2] 。

この練習問題は、内容的には数直線/座標平面内の図形を描くものだが、「コンテキスト付き論理式の真理集合を求める」という意図と解釈を持つ。

  1. (x∈R| x < 0 ∨ 1 < x)
  2. (x∈R| 0 < x ∧ x < 1)
  3. (x∈R| 0 < x ∧ 1 < x)
  4. (x∈R| x < 0 ⇒ x2 = 1)
  5. (x∈R| x2 = 1 ⇒ x < 0)
  6. (x∈R| x2 = 1 ⇒ x = 0)
  7. (x∈R| x2 = 1 ⇒ x = 1)
  8. (x∈R| x2 = 1 ⇒ (x = 1 ∨ x = -1))
  9. (x∈R| (x2 = 1 ∧ x ≧ 0) ⇒ x = 1)
  10. (x∈R| (x2 = 1 ∧ x ≧ 0) ⇒ (x = 1 ∨ x = -1))
  11. (x, y∈R| x2 + y2 = 1)
  12. (x, y∈R| x2 + y2 = 4 ∧ x + y ≧0)
  13. (x, y∈R| x2 + y2 = 4 ∧ x + y ≧ -1)
  14. (x, y∈R| x2 + y2 = 1 ∨ x + y = 0)
  15. (x, y∈R| x2 + y2 = 1 ⇒ x = 1)
  16. (x, y∈R| x = 1 ⇒ x2 + y2 = 1)
  17. (x, y∈R| (x = 1 ∧ y = 0) ⇒ x2 + y2 = 1)
  18. (x, y∈R| x2 + y2 = 1 ⇒ x + y ≦ 2)
  19. (x, y∈R| x2 + y2 = 1 ⇒ x + y ≦ 1)
  20. (x, y∈R| x2 + y2 ≦ 1 ⇒ x + y ≦ 2)
  21. (x, y∈R| x2 + y2 ≦ 1 ⇒ x + y ≦ 1)
  22. (x, y∈R| (x2 + y2 ≦ 1 ∧ x + y ≦ 0) ⇒ x + y ≦ 1)

コンテキストの水増し

以下のコンテキスト付き論理式は、前問の論理式のコンテキストを水増し〈thinning〉したものである。そのスコット・ブラケット〈真理集合〉を図示せよ。

  1. (x, y∈R| x < 0 ∨ 1 < x)
  2. (x, y∈R| 0 < x ∧ x < 1)
  3. (x, y∈R| 0 < x ∧ 1 < x)
  4. (x, y∈R| x < 0 ⇒ x2 = 1)
  5. (x, y∈R| x2 = 1 ⇒ x < 0)
  6. (x, y∈R| x2 = 1 ⇒ x = 0)
  7. (x, y∈R| x2 = 1 ⇒ x = 1)
  8. (x, y∈R| x2 = 1 ⇒ (x = 1 ∨ x = -1))
  9. (x, y∈R| (x2 = 1 ∧ x ≧ 0) ⇒ x = 1)
  10. (x, y∈R| (x2 = 1 ∧ x ≧ 0) ⇒ (x = 1 ∨ x = -1))

以下のコンテキスト付き論理式は、最初の問題と二番目の問題の論理式のコンテキストを水増ししたものである。そのスコット・ブラケット〈真理集合〉を図示せよ。自由変数と束縛変数の名前がかぶっているが、理論的には問題にならない(紛らわしいので、現実的には避けたほうがよい)。

  1. (x, y∈R| 1 + 2 = 3)
  2. (x, y∈R| 1 + 2 < 3)
  3. (x, y∈R| 12 = 22)
  4. (x, y∈R| 3 ≦ 5 ∧ 3 ≦ 3)
  5. (x, y∈R| 1 + 2 < 3 ⇒ 12 = 22)
  6. (x, y∈R| 1 + 2 < 3 ∨ 12 = 22 ∨ 3 ≦ 3)
  7. (x, y∈R| (3 ≦ 5 ∧ 3 ≦ 3) ⇒ 1 + 2 < 3)
  8. (x, y∈R| (3 ≦ 5 ∨ 3 ≦ 3) ⇒ ¬(1 + 2 < 3))
  9. (x, y∈R| ¬(1 + 2 < 3) ⇒ (1 + 2 = 2))
  10. (x, y∈R| 1 + 2 = 3 ⇒ (1 + 2 < 3 ⇒ 12 = 22))
  11. (x, y∈R| ∀n∈N.(n ≧ 0))
  12. (x, y∈R| ∃n∈N.(n < 0))
  13. (x, y∈R| ∀n∈N.∃m∈N.(m ≧ n))
  14. (x, y∈R| ∀n∈N.∃m∈N.(m < n))
  15. (x, y∈R| ∀x∈R.∃y∈R.(y2 = x))
  16. (x, y∈R| ∀x∈R.∃y∈R.(x ≧ 0 ⇒ y2 = x))
  17. (x, y∈R| ∃y∈R.∀x∈R.(x ≧ 0 ⇒ y2 = x))
  18. (x, y∈R| ∀x∈R.∀y∈R.∃n∈N.((x ≧ 0 ∧ y > 0) ⇒ yn ≧ x))

様々な論理式を作ってみる

コンテキストの水増しにより、今まで登場した40個の論理式のコンテキスト領域は、すべてR2(平面)であるとしてよい。

  1. (x, y∈R| 1 + 2 = 3)
  2. (x, y∈R| 1 + 2 < 3)
  3. (x, y∈R| 12 = 22)
  4. (x, y∈R| 3 ≦ 5 ∧ 3 ≦ 3)
  5. (x, y∈R| 1 + 2 < 3 ⇒ 12 = 22)
  6. (x, y∈R| 1 + 2 < 3 ∨ 12 = 22 ∨ 3 ≦ 3)
  7. (x, y∈R| (3 ≦ 5 ∧ 3 ≦ 3) ⇒ 1 + 2 < 3)
  8. (x, y∈R| (3 ≦ 5 ∨ 3 ≦ 3) ⇒ ¬(1 + 2 < 3))
  9. (x, y∈R| ¬(1 + 2 < 3) ⇒ (1 + 2 = 2))
  10. (x, y∈R| 1 + 2 = 3 ⇒ (1 + 2 < 3 ⇒ 12 = 22))
  11. (x, y∈R| ∀n∈N.(n ≧ 0))
  12. (x, y∈R| ∃n∈N.(n < 0))
  13. (x, y∈R| ∀n∈N.∃m∈N.(m ≧ n))
  14. (x, y∈R| ∀n∈N.∃m∈N.(m < n))
  15. (x, y∈R| ∀x∈R.∃y∈R.(y2 = x))
  16. (x, y∈R| ∀x∈R.∃y∈R.(x ≧ 0 ⇒ y2 = x))
  17. (x, y∈R| ∃y∈R.∀x∈R.(x ≧ 0 ⇒ y2 = x))
  18. (x, y∈R| ∀x∈R.∀y∈R.∃n∈N.((x ≧ 0 ∧ y > 0) ⇒ yn ≧ x))
  19. (x, y∈R| x < 0 ∨ 1 < x)
  20. (x, y∈R| 0 < x ∧ x < 1)
  21. (x, y∈R| 0 < x ∧ 1 < x)
  22. (x, y∈R| x < 0 ⇒ x2 = 1)
  23. (x, y∈R| x2 = 1 ⇒ x < 0)
  24. (x, y∈R| x2 = 1 ⇒ x = 0)
  25. (x, y∈R| x2 = 1 ⇒ x = 1)
  26. (x, y∈R| x2 = 1 ⇒ (x = 1 ∨ x = -1))
  27. (x, y∈R| (x2 = 1 ∧ x ≧ 0) ⇒ x = 1)
  28. (x, y∈R| (x2 = 1 ∧ x ≧ 0) ⇒ (x = 1 ∨ x = -1))
  29. (x, y∈R| x2 + y2 = 1)
  30. (x, y∈R| x2 + y2 = 4 ∧ x + y ≧0)
  31. (x, y∈R| x2 + y2 = 4 ∧ x + y ≧ -1)
  32. (x, y∈R| x2 + y2 = 1 ∨ x + y = 0)
  33. (x, y∈R| x2 + y2 = 1 ⇒ x = 1)
  34. (x, y∈R| x = 1 ⇒ x2 + y2 = 1)
  35. (x, y∈R| (x = 1 ∧ y = 0) ⇒ x2 + y2 = 1)
  36. (x, y∈R| x2 + y2 = 1 ⇒ x + y ≦ 2)
  37. (x, y∈R| x2 + y2 = 1 ⇒ x + y ≦ 1)
  38. (x, y∈R| x2 + y2 ≦ 1 ⇒ x + y ≦ 2)
  39. (x, y∈R| x2 + y2 ≦ 1 ⇒ x + y ≦ 1)
  40. (x, y∈R| (x2 + y2 ≦ 1 ∧ x + y ≦ 0) ⇒ x + y ≦ 1)

同じコンテキスト領域を持つ論理式(単に「論理式」と言ってもコンテキスト付きと考える)は、論理演算をしてもよいので、上記40個の論理式をもとに自由に複合論理式を作れる。

次の手順で、好きなだけ練習をせよ(お腹いっぱいになったら、それ以上やらなくてもよい)。

  1. 1から40のなかから適当に(乱数的に)番号を選んで、Aに割り当てる。必要があれば、B, C にも番号を割り当てる。
  2. 下の総称論理式の命題パラメータ(論理式を代入できる変数)A, B, C に、選んで割り当てた番号の論理式を代入する。
  3. 出来た具体的な論理式に対して、そのスコット・ブラケットを求める。

総称論理式:

  1. ¬A
  2. A∧B
  3. A∨B
  4. A⇒B
  5. A⇒¬B
  6. (A∧B)⇒C
  7. (A∨B)⇒C
  8. A⇒B∧C
  9. A⇒B∨C
  10. (A∧B)∨C

総称論理式をもっと増やせば、練習問題を増やせる。

※注意: 全称と総称は似た言葉だが違う。全証命題は、全称記号∀が頭にある命題、総称命題は、論理式を代入してよい変数〈命題パラメータ〉を持つ命題。すぐ上の論理式は命題パラメータ A, B, C を持っているので総称命題だが、全称命題ではない。なお、「総称」は論理の言葉というより計算科学の言葉である。

限量子も使ってみる

前問と同様に、次の手順で、好きなだけ練習をせよ。

  1. 1から40のなかから適当に(乱数的に)番号を選んで、Aに割り当てる。
  2. 下の総称論理式の命題パラメータ(論理式を代入できる変数)Aに、選んだ番号の論理式を代入する。
  3. 出来た具体的な論理式は限量子を持ち、そのコンテキスト領域はRまたは1になる。そのスコット・ブラケットを求める(図示する)。コンテキスト領域が1のときは、図示はあまり意味がないので、値 0, 1 で答えればよい。
  1. ∀x.A
  2. ∀y.A
  3. ∀x.∀y.A
  4. ∃x.A
  5. ∃y.A
  6. ∃x.∃y.A
  7. ∀x.∃y.A
  8. ∀y.∃x.A

限量子(∀, ∃)と論理結合子(∧, ∨, ¬, ⇒)を組み合わせた総称論理式、例えば ∀x.(A∧B⇒C) や A⇒¬∃y.B などを準備すれば、練習問題を増やせる。興味と気力があれば、やってみよ。

TeXコードの実験 05-14(2nd)

  •  G(A) := \coprod_{x\in X} A_x

ジャーム空間G(A)は、\(\coprod_x A_x\) と書けました。茎〈ストーク〉の寄せ集めですね。各茎には、前の補足で述べた射影 qxσx→Ax があります。これらの射影を寄せ集めると、次の写像を定義できます。

  • \( p:\coprod_{x\in X}\sigma_x \rightarrow \coprod_{x\in X} A_x \)

\(\coprod_{x\in X}\sigma_x \) は、\( (\coprod_{U\in |Open(X)|} A(U))\times X \) の部分集合としても実現できます。a∈A(U) ⇔ def(a) = U として、

  • \( \{(a, x) \in (\coprod_{U\in |Open(X)|} A(U))\times X | x \in def(a)\} \)

同じTeXコードなのだが (2nd)


\(
T(f^{-1})( (y_1, \ldots, y_{m}),
\begin{pmatrix}
\eta_1 \\
\vdots \\
\eta_{m}
\end{pmatrix}) \\ = \\
(f^{-1}(y_1, \ldots, y_{m}), \\
\begin{pmatrix}
\frac{\partial f_1}{\partial x_1}(f^{-1}(y_1, \ldots, y_{m})) & \ldots & \frac{\partial f_1}{\partial x_{\ell}}(f^{-1}(y_1, \ldots, y_{m})) \\
\vdots & \ddots & \vdots \\
\frac{\partial f_{m}}{\partial x_1}(f^{-1}(y_1, \ldots, y_{m})) & \ldots & \frac{\partial f_{m}}{\partial x_{\ell}}(f^{-1}(y_1, \ldots, y_{m})) \\
\end{pmatrix}^{\triangleleft}
\cdot \\
\begin{pmatrix}
\eta_1 \\
\vdots \\
\eta_{m}
\end{pmatrix}
)
\)

用語対応表の予定地

ここに、論理関係の用語の対応表を書く予定です。でも、今週は無理で、来週(15日)以降。

順不同、備忘のための羅列:

  1. 命題論理
  2. 述語論理
  3. 古典論理
  4. 命題
  5. 述語
  6. 証明
  7. 意味
  8. モデル
  9. 基本、基礎
  10. 原子、アトム、個体
  11. コンテキスト
  12. 算術
  13. 推論
  14. 演繹
  15. 論理式
  16. 推論規則
  17. 公理
  18. 公理シェマ
  19. 命題変数
  20. 導入規則
  21. 除去規則
  22. 証明プリミティブ
  23. 証明コンビネータ
  24. 証明オブジェクト
  25. リーズニング・プリミティブ
  26. リーズニング・コンビネータ
  27. リーズニング・オブジェクト
  28. 真理関数
  29. 命題関数
  30. 命題関数=インデックス付き命題
  31. 型関数=インデックス付き型
  32. 総称型=パラメータ付き型
  33. 総称命題=パラメータ付き命題≒真理関数
  34. 真理集合
  35. コンテキスト
  36. 帰納と再帰
  37. 計算
  38. 計算可能
  39. 素朴集合論
  40. 素朴論理
  41. メタナントカ
  42. 論理和、選言、論理OR
  43. 論理積、連言、論理AND
  44. 否定
  45. 限量子、量化子、量記号
  46. 全称、総称、普遍
  47. 存在
  48. 結合子
  49. 含意、条件法

データ算術と符号化 (A27)

※この記事は「記事27」

演繹システム付属(むしろ内蔵)のプログラミングシステムとして、自然数の算術を使うことにはメリットがあります。自然数は誰にとってもお馴染みで、自然数の算術は非常に確実性が高いとみんな信じています。しかし、プログラミングの観点からは、自然数の算術システムは貧弱・低機能で、プログラミングの労力・負担が大きく、ちょっとシンド過ぎます。

リストとツリーは、高水準で便利なデータで、リスト・ツリーが使えれば、プログラミング負担は劇的に軽くなります。ここでは、データとしてリスト・ツリーを使った算術システム(演繹システムの一部となるプログラミングシステム)を紹介します。

関連記事:

リストとツリーは、データとしては実は同じものだとして、気持ちと名前だけで区別することにします。

内容:

リストの構成

基本型領域としては、N = (自然数の集合) と S = (文字列の集合) をとります。他に、B=(ブーリアン、真偽値の集合) も使いますが、これは B = {0, 1} ⊆N とみても、独立な集合 B = {true, false} でもどっちでも(二値なら何でも)いいです。

自然数、文字列、ブール値〈真偽値〉に関してよく知られた演算は、すべて基本〈組み込み〉関数とします。実在のプログラミング言語と標準ライブラリに備わっている演算は最初から使って良いとします(禁欲的な態度は取らない)。

A = NSB として、Aの要素はアトミックなデータ〈atomic data〉と呼びます。次のルールでリスト〈list〉を導入して、アトミックなデータを拡張します。

  1. アトミックなデータはデータである。
  2. 空リストεはリストである。
  3. xがデータで、yがリストのとき、x・y はリストである。
  4. リストはデータである。
  5. 以上のルールで定義されるモノがデータの全てである。

計算科学では、このような定義の数学的定式化を「再帰的領域方程式の最小解」と呼んでいます。ここでは直感的理解でよいとしましょう。

x・y の意味は、リストyの先頭にデータxを挿入したものです。空リストεは [] とも書くことにします。幾つか例を挙げると:

  1. 3・[] = [3]
  2. "hello"・[3] = ["hello", 3]
  3. ["hello", 3]・[] = [["hello", 3]]
  4. ["hello", 3]・[0, "good morning"] = [["hello", 3], 0, "good morning"]
  5. ""・[["hello", 3], 0, "good morning"] = ["", ["hello", 3], 0, "good morning"]

リストはいくらでも入れ子にできて、入れ子をたどっていくと、いずれはアトミックなデータにたどり着きます。

先のデータの定義(ルール)を見ると、データはアトミックかリストかに大分類されて、アトミックは、自然数か文字列かブーリアン(自然数の一部でもいい)に細分化されます。この程度の豊かなデータ領域があると、かなり楽にプログラミングができます。

リストに対する演算と述語

リストに関して、次のような演算〈関数〉は使えるとします。引数によってはエラーを引き起こす演算もあります。

  1. cons(x:Data, y:List) : 中置演算子の'・'と同じ。
  2. firstItem(x:List) : リストの最初の項目を返す。
  3. rest(x:List) : リストの最初の項目を取り除いた残りのリストを返す。
  4. secondItem(x:List) : リストの二番目の項目を返す。
  5. lastItem(x:List) : リストの最後の項目を返す。
  6. getItme(x:List, k:Nat) : リストのk番目の項目を返す。1から勘定(別に0からでもいいが)。
  7. putFirst(x:Data, y:List) : consの別名。
  8. putLast(x:Data, y:List) : リストの最後に項目を追加したリストを返す。
  9. putItem(x:Data, k:Nat, y:List) : リストのk番目に項目を追加したリストを返す。
  10. length(x:List) : リストの長さ(自然数)を返す。
  11. concat(x:List, y:List) : 2つのリストを連接〈concatenate〉して返す。

データ領域上の全域述語:

  1. isAtomic(x:Data) : アトミックかどうかを返す。
  2. isNatural(x:Data) : 自然数かどうかを返す。
  3. isString(x:Data) : 文字列かどうかを返す。
  4. isBool(x:Data) : ブーリアンかどうかを返す。
  5. isList(x:Data) : リストかどうかを返す。
  6. isEmpty(x:Data) : 空リストかどうかを返す。

自然数・文字列・ブール値に対する常識的な演算・述語に加えて、このような演算・述語があれば、ひととおりのデータ処理ができます。

ツリーデータ

リストとは別にツリーを定義するほうが使い勝手はいいのですが、ここでは、リストでツリーを代用します。正式なツリーデータは定義せず、リストを「ツリーとして」扱うことでお茶を濁します。

ツリーを扱っている気持ち(あくまで気持ち)になるために、演算〈関数〉に別名を割り当てます*1

リスト演算・述語 なんちゃってツリー演算・述語
cons(x, y) treeCons(x, y)
firstItem(x) rootNode(x)
rest(x) children(x)
secondItem(x) firstChild(x)
lastItem(x)(長さ2以上) lastChild(x)
getItem(k + 1) getChild(k)
putLast(x, y) addLastChild(x, y)
putItem(x, k + 1, y) insertChild(x, k, y)
length(x) - 1 numberOfChildren(x)
isList(x) isTree(x)
isEmpty(x) isEmptyTree(x)

行きがかり上、ルートノードも持たない空ツリーもツリーとみなします。

リストかツリーかは、システムが認識できるわけではなくて、あくまでプログラマ(人間)が心で認識しているだけなので、型チェックなどは人間の注意力に頼ることになり、あまり望ましくはありません。が、自然数の範囲内でツリーデータの処理をシミュレートするのに比べれば、格段に楽です。

データの例

自然数の割り算の原理を表す論理式を考えます。

  • ∀n, m∈N.∃q, r∈N.(n = qm + r ∧ 0 ≦ r < m)

太字を使いたくないので、N = Nat として、論理結合子や掛け算記号を省略しないで書くと:

  • ∀n, m∈Nat.∃q, r∈Nat.(n = q×m + r ∧ (0 ≦ r ∧ r < m))

これを構文解析して次のようなツリーができます。

          "∀"
        /     \
      "∈"      (サブツリー1)
     /   \
["n", "m]   "Nat"


(サブツリー1)

          "∃"
        /     \
      "∈"      (サブツリー2)
     /   \
["q", "r"]  "Nat"


(サブツリー2)

           "∧"
        /     \
      "="      (サブツリー3)
    /   \
  "n"     "+"
         / \
       "×"  "r"
       / \
     "q"   "m"


(サブツリー3)

           "∧"
        /     \
     "≦"      (サブツリー4)
    /   \
  "0"     "r"


(サブツリー4)

    "<"
   /  \
 "r"    "m"

これをデータとしてエンコード〈符号化〉すると:

"∀"・[
    "∈"・[
        ["n", "m"],
        "Nat"
    ],
    "∃"・[
        "∈"・[
            ["q", "r"],
            "Nat"
        ],
        "∧"・[
            "="・[
                "n",
                "+"・[
                    "×"・[
                        "q",
                        "m"
                    ],
                    "r"
                ]
            ],
            "∧"・[
                "≦"・[
                    "0",
                    "r"
                ],
               "<"・[
                   "r",
                   "m"
               ]
            ]
        ]
    ]
]

「論理式だけでなく、シーケント、推論図、リーズニング図なども入れ子のツリーにより表現できるだろう」と想像はできるでしょう。このように、論理的な操作・処理に使った諸々の式(テキスト表現)や図(ビジュアル表現)が、ことごとくデータ領域のデータとしてエンコード〈符号化〉できることが、自己言及メカニズムの基本になります。



ふー、これでゲーデル符号化について語る準備はできただろう。

*1:檜山は DOM API にけっこう詳しいが、DOM互換にはなってない。