思考の外在化

ずっと昔からプログラミングに関して、いろんな本を読んだり、色々なプログラム言語に取り組んだりしているが、まとまったプログラムを書いたことはない。便利なツールはとっくに他の人が作っているし、定番のプログラムを活用すれば、日常的にやりたいことはそのプログラムでできてしまう。

かといって、出来合いのプログラムの扱い方に精通するという根気もないし、興味もあまり湧かない。それでは、何のためにプログラミングの学習を続けているのかということになる。このまま一生プログラミング周辺でつまみ食いを続けていくのだろうか。

確かに、プログラミングの実用的な側面に興味がないのは事実のようだ。何かのツールを作るということの大変さも分かるようになったし、特定の用途のプログラムを完成させることによる時間のロスが勿体なく感じるのだ。それでは、実用的なプログラムを書かないのなら、何で依然としてプログラムの勉強を続けているのだろう。

自分でもよくわからなかったが、最近自分が、プログラミングを自分の思考を具体化するための道具と考えているのではないかと思うようになった。

プログラミングをやっていて最も嬉しいのは、デバッグの終わったプログラムを走らせる時だ。それまで自分の頭の中にしかなかったアイディアが、実体化して自分で動き始めるのを見るのが面白い。自分にとってプログラミングの醍醐味とは自分の頭の中にしか存在しない思考を、実際に動くプログラムとして外在化させることだったのだ。頭の中でモヤモヤしていた考えが、アルゴリズムとしてプログラムできることで、その実態についてさらに深く考えることができる。

こう考えると、何の役にも立たないスニペットを作ったり、実用にはならないプログラミングの知識を蓄えたりし続けていることにも意味があるような気がする。「虎は死して皮を残し、人は死して名を残す。」というが、プログラミングに関して皮も名も残さなくても、プログラムすることは、日々の食事と同じように、自分という人間の新陳代謝を支えている栄養だったのだ。

[PR]
# by tnomura9 | 2016-09-29 07:03 | 考えるということ | Trackback | Comments(0)

A -> (B -> A)

ウカシェビッチの次の公理と前件肯定 modus ponens を組み合わせるとどんなことが言えるだろうか。

P1. A -> (B -> A)

これは公理だから前件肯定の推論から A が定理であれば、

B -> A

は定理である。この時、B が定理なら、やはり前件肯定から A は定理である。そうするとこの推論は循環論法に陥ってしまい、新しい定理を見つけることはできない。したがって、公理 P1 については、これに前件肯定を適用しても新しい定理は導けないことがわかる。

それゆえ、公理 P1 については、これを条件文として前件肯定を適用するというよりは、

A -> (B -> A)

自体が定理であるということが重要な意味を持っていることがわかる。なぜなら、B にどのような命題を持ってきてもこれは定理であるからだ。A -> (B -> A) が定理であることの重要性は次のような推論でわかる。

A -> (B -> A) を公理 P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C)) の前件に置き換えると、

(A -> (B -> A)) -> ((A -> B) -> (A -> A))

が定理である。この論理式の前件は定理(公理)なので後件も定理である。

(A -> B) -> (A -> A)

そこで、B を (B -> A) に置き換えると、

(A -> (B -> A)) -> (A -> A)

となり、前件は公理だから前件肯定によって、後件

A -> A

が定理であることがわかる。P1 に前件肯定を適用しても循環論法だったのが、P1 を P2 の前件に置き換えることにより新しい定理 A -> A を導き出すことができた。

また、A -> (B -> A) が公理だから、A が定理の時、

B -> A

は定理である。つまり定理が後件の場合、前件が任意の命題でもその命題は定理だ。したがって、B -> A が定理なので、

C -> (B -> A)

は定理である。こうして定理を後件にすることによって、任意の命題を前件に持ってきたものは定理なので、

D -> (C -> (B -> A))
E -> (D -> (C -> (B -> A)))
.....

と、どんどん新しい命題を導入した定理を作ることができる。しかし、このようにして作られた定理は、含意の入れ子の階層の最も深いところの後件が定理であるという共通した性質がある。

また、A -> (B -> A) からは、前件肯定によらなくても原始式の置き換えによっても定理を導くことができる。例えば、

A -> ((C -> D) -> (E -> F)) -> A)

なども定理となる。これらの定理も A と B を置き換える論理式によって、無限の組み合わせが考えられるが、含意の階層の際上層では P -> (P -> Q) というパターンを取るところは共通である。

このように、A -> (A -> B) という公理と前件肯定からは無限の定理が演繹できるが、そのパターンは、前件肯定によるものと、公理図式のプレースホルダーの任意の論理式の置き換えによるものの2つのあり方がある。

そこで興味が湧いてくるのは、A -> (B -> A) という公理と前件肯定から演繹される定理を要素とする集合はどのようなものになるかということだ。それは、次のようなものになるだろう。

まず、A -> (B -> A) は公理なので定理である。これは定理の演繹をするときの根幹になるもので、演繹されずに定理であるのは、この論理式だけである。これは、構成的集合を作るときの唯一の集合が空集合であるのと似ている。

次に、公理図式の A, B を任意の論理式で置き換えたものは定理である。公理図式の性質から、A, B に置き換える論理式には制限がないので、論理式全体の集合を L とすると、このようにして作られる公理の全体は L の直積である L x L 個存在することになる。

次に、A -> (B -> A) を唯一の公理とした時に、これに前件肯定を適用した時にどのような定理が得られるだろうか。表現を簡単にするために P = A -> (B -> A) と置くと、まず考えられるのが、

P -> (C -> P)

である。これは明らかに公理 A -> (B -> A) のプレースホルダーの置き換えで作られているから公理である。この条件文について、P は公理だから前件肯定によって

(C -> P)

も定理である。このようなやり方で次のように定理を次々に演繹していくことができる。

D -> (C -> P)
E -> (D -> (C -> P))
F -> (E -> (D -> (C -> P)))
....

ここで、プレースホルダーの置き換えで作られた公理の集合と前件肯定を用いた定理の集合に共通部分がないかどうかという興味が湧いてくる。そこで、これらの論理式の含意の入れ子構造の最上層の構造を見てみると、プレースホルダーの置き換えで作られた公理は全て P -> (Q -> P) という構造をしている。C -> P という定理は明らかにこの構造は取らない。その他の論理式もあきらかに A -> B -> C というパターンを取るものはない。このようにして作られた定理は原始式の数と同じくらい作ることができるので加算無限である。

しかしながら、D を P に置き換えた P -> (C -> P) は公理の形態をとる。したがって、P に前件肯定を適用して作られた定理のプレースホルダーの置き換えかた次第では、公理の集合との共通部分が存在することが分かる。

さらに、このようにして作られた無数の公理や定理に対してそれぞれにプレースホルダーの置き換えや、前件肯定による演繹を行ってさらに多くの定理を演繹することができる。A -> (B -> A) というたった1個の公理からは無限の定理が演繹できてしまうのだ。そうしてこのようにして演繹された定理全体の集合の性質は掴み難いものがある。この定理の集合が、全てのトートロジーを網羅しているのかそうでないのかすら判然としない。

このように公理系によって演繹される定理全体の性質を推論規則から調べるのは非常に困難だ。命題論理の完全性定理によって、これが命題計算のトートロジーと同値であることが証明されているのは非常にありがたいことなのだ。

命題論理というと、公理から2、3の定理を証明したり、トートロジーを真理表で確認したりしたら学ぶことはそれでおしまいと考えやすいが、実際には、まだまだ未踏の不可思議な世界が広がっているような気がする。その不可思議な性質の根元の一つは、プレースホルダーの原子命題を任意の論理式に置き換えていいという定理やトートロジーの驚くべき性質だろう。この性質が、論理式に幾重にも重なった含意の入れ子構造を与え、その全体像を見極めるのを難しくしている。

この記事を持って、一連の命題論理の記事の最後としたい。命題論理について考えることよりもさらに学習することの方が大切になってきたような気がするからだ。知識の森は入り口は簡単なように見えるが、入り込めば入り込むほどその奥行きがさらに広がっていくという感覚がおもしろい。この感覚に早くから気付いていれば、もっとマシな人生が遅れたのではないかと思うが、手遅れだ。

[PR]
# by tnomura9 | 2016-09-27 23:42 | 考えるということ | Trackback | Comments(0)

公理図式の不思議

ウカシェビッチの3つの公理

P1. A -> (B -> A)
P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C))
P3. (¬B -> ¬A) -> (A -> B)

の原子式 A, B, C は特定の命題を表しているのではなく、ここには任意の命題を当てはめることができる。したがって、これらの公理は特定の命題を表しているのではなく、公理図式だ。

3つの公理を見ると、まず思いつくのが、ベクトル空間との類推だ。ベクトルの場合は少数の基底ベクトルから、ベクトルの演算で導き出される全てのベクトルを考えることができる。しかし、これらの公理は特定の命題を表しているわけではないので、この方法が使えない。

例えば、公理P1 の A -> (B -> A) で定められる命題の集合を考えて見る。プレースホルダー A, B に任意の命題を当てはめることによって新しい命題を作ることができる。例えば B を B -> C で置き換えることによって、次のような新しい命題を導くことができる。

(A -> (B -> C)) -> ((B -> C) -> A)

トートロジーの原子式を任意の命題で置き換えても、それもまたトートロジーになるので、上の命題の A, B, C も任意の命題に置き換えることができる。つまり、公理図式の原子式を任意の命題で置き換えてできる新しい命題もやはり命題図式 (shcema) になる。

しかし、全ての論理式がトートロジーというわけではないので、公理から導かれる命題図式は命題の中でもトートロジーという特殊な命題である。

公理の原子式を他の論理式で置き換えて新しい論理式を作ることができるので、論理式の集合 L を考えるとこの操作は論理式集合 L で定義される関数と考えることができる。しかし、A -> (B -> A) では A, B が任意の論理式で置き換えることができるので、この関数 f1 :: L x L -> L のように L の直積から L への関数である。

A, B と置き換える論理式には制限がないので、この関数 f1 の定義域は、L x L そのものである。また、論理式の一意性から L × L の異なる要素には異なる論理式が対応するので f1 は 単射である。また、f1 は A -> (B -> A) で定められる定理の集合に対し全射である。したがって、f1 は論理式の直積集合 L x L から L への全単射関数である。

論理式の一つ一つの記号列は有限長であるので、L の要素は有限長の論理式である。したがって L は無限集合であるが加算である。この場合 L x L も加算な無限集合なので f1 の像も加算な無限集合である。f1 の像は明らかに L の部分集合であるが、その濃度は L と等しい。このような L の部分集合を F1 としよう。すると、公理 P2, P3 からも同様に部分集合 F2, F3 を定めることができる。

公理から演繹される定理の集合がこれだけなら問題はない。無限集合であって、それぞれが L と同じ濃度であっても L を F1, F2, F3 で類別することができる。ところが、これらの定理にはもう一つ前件肯定という演算規則が適用される。これは、F1, F2, F3 の要素を二つとり、それから新しい定理を作り出す。この新しい定理が、F1, F2, F3 の要素であれば問題はないが、どうも F1, F2, F3 には治らないようだ。

前件肯定で演繹された新しい定理はトートロジーなので、これは定理図式になる。定理図式であれば、上に議論した方法で、L の部分集合を定めるがこれが F1, F2, F3 と独立であれば、類別の数が一つ増えることになる。さらに、これらの L の部分集合から前件肯定によって新しい L の部分集合が作られるとして、それが無限に繰り返すことができるとすると、類別の数が無限に増えることになる。こうなるともはやこれらの集合は L という加算集合には治らなくなる。したがって、類別を無限に増やすことができないか、L が加算ではないかのどちらかということになる。

そこで、最初に論理式の記号列の長さは有限なので、L は加算であると単純に考えていたが、果たしてそれで良いのかという疑問が生じる。論理式の長さは確かに有限だが、それには原子式の種類が無限であるという観点が抜け落ちていたのではないかということだ。A, B, ... という原子式はその種類を無限に考えることができる。A -> B という論理式は長さが3であるが、長さが3である論理式は、原子式の種類によって無限に存在するということである。長さが3である論理式の数が限られていれば、論理式は記号列の長さによって加算であると考えることができるが、長さが3である論理式が無限に存在すると考えると、これは加算ではなくなってくる。

公理や定理による L の部分集合による L の類別が無限に存在するというパラドックスは、L が非加算であると考えることによって解決できるのではないだろうか。

[PR]
# by tnomura9 | 2016-09-26 06:18 | 考えるということ | Trackback | Comments(0)

48時間 Scheme 記事リスト

48時間で Scheme を書こう』というネットの文章の読解記事を2011年12月に書いていたが、記事リストがなかったので作ってみた。読み返すための自分用のメモだ。

48時間でSchemeを書こう 最初の一歩

48時間でSchemeを書こう/構文解析

48時間でSchemeを書こう/構文解析 (2)

48時間でSchemeを書こう/評価: 第一部

『48時間でSchemeを書こう』のこれまでのまとめ

Haskell の例外処理

自前のエラーモナドの作り方

Either モナド?

48時間でSchemeを書こう/エラー処理と例外

48時間でSchemeを書こう/評価: 第二部

条件分岐: パターンマッチ2

リストのプリミティブ: car、cdrとcons

ダック・タイピング

存在型 (Existentially quantified data constructors)

48時間でSchemeを書こう/評価: 第二部 (2)

48時間でSchemeを書こう/REPLの作成

Data.IORef モジュール

48時間でSchemeを書こう/変数と代入

48時間でSchemeを書こう/変数と代入 (2)

48時間でSchemeを書こう/変数と代入 (3)

48時間でSchemeを書こう/変数と代入 (4)

48時間でSchemeを書こう/Scheme関数の定義


一度学習したはずなのに???の記事が多かった。学習は忘却との戦いだ。5年という時間を無駄にしないために。

[PR]
# by tnomura9 | 2016-09-25 10:33 | Haskell 記事リスト | Trackback | Comments(0)

完全性定理の証明についての疑問

『数学基礎論講義』の命題論理の完全性定理の証明の中で、無矛盾な命題の集合を Σ とする時、

任意の論理式 An について An ∈ Σ または ¬An ∈ Σが言える。

という文があったが、これは明らかに間違いだと思う。論理式の文法によって生成される論理式の命題の中には、トートロジーではないものがあるので、An がトートロジーでなければ ¬An もトートロジーではない。上の命題が成立するのは、An がトートロジーであるか、または An が恒偽命題であるかのどちらかの場合だ。

上の命題が間違っていたら、完全性定理の証明に影響がある気がする。完全性定理の最初は 命題 A が定理でなければ {¬A} は無矛盾であるとしているが、命題 A が定理でなくても、命題 A が恒偽命題でなければ、{¬A} は無矛盾ではない。

なぜなら、A -> B はトートロジーではないが、A にトートロジーの命題、B に恒偽の命題を割り当てると、これは恒偽命題になる。明らかに、

{A -> B} |- (A -> B)

であるから、結果として恒偽命題を仮定から演繹できることになるので、{A -> B} は無矛盾ではない。また、その否定 ¬(A -> B) も同様の理由で無矛盾ではない。

したがって、完全性定理は証明できないことになる。

無矛盾は公理系から演繹される考え方で、トートロジーは真理表から計算される概念だ。したがって、命題がトートロジーであることを、公理系の概念である無矛盾性から証明することはできないのではないだろうか。完全性定理で証明できるのは、命題が無矛盾であれば、それは定理であるということで、無矛盾とトートロジーとは異なる概念のような気がする。また、完全性定理で導入される真理関数は、明らかにトートロジーを判別する関数ではなく、命題が無矛盾かどうかを判別する関数である。

トートロジーが定理であることを証明するためには、論理計算の法則が全て公理系から演繹できて、任意のトートロジーについてそれは公理からも演繹できることを言わなければならないのではないだろうか。

数学は素人だが、命題論理の完全性定理の証明が納得できない理由だ。

[PR]
# by tnomura9 | 2016-09-23 06:49 | 考えるということ | Trackback | Comments(0)

論理式のパーサ

ウカシェビッチの公理には論理結合子は次のように否定結合子と含意結合子しかない。

P1. A -> (B -> A)
P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C))
P3. (¬B -> ¬A) -> (A -> B)

これはパーサを書く練習にちょうど良いと思って、Parsec で書いてみた。ソースコードは次のようになる。

module Logic where

import Text.ParserCombinators.Parsec

atom :: Parser String
atom = do {letter; return "atom"}

negation :: Parser String
negation = do {char '~'; return "not"}

imply :: Parser String
imply = do {string "->"; return "imply"}

expression :: Parser String
expression = do {try (do {term; imply; term}) <|> term; return "expression"}

term :: Parser String
term = do {do {negation; factor} <|> factor; return "term"}

factor :: Parser String
factor = do {do {string "("; expression; string ")"} <|> atom; return "factor"}

文法チェックしかしないが、次のように入れ子になった括弧も解釈できる。入れ子になった do 記法が読みにくいかもしれないが、do 記法は複数のモナドを一つのモナドにまとめるための記法だとイメージすると読みやすくなるだろう。

また、factor が再帰呼び出しになっているが、入れ子になった括弧を処理するための定型文だ。

ghci で検証した。

Prelude> :l Logic.hs

[1 of 1] Compiling Logic ( Logic.hs, interpreted )

Ok, modules loaded: Logic.

*Logic> parseTest expression "~(~a->(a->b))"

"expression"


論理だけの作業をしていると、手で動かせる実体が欲しくなる。


[PR]
# by tnomura9 | 2016-09-22 10:48 | Haskell | Trackback | Comments(0)

前件肯定 modus ponens の性質

この記事も典拠はないので、注意喚起しておく。

命題論理の公理系では、ウカシェビッチの公理

P1. A -> (B -> A)
P2. (A -> (B ->C)) -> ((A -> B) -> (A -> C))
P3. (¬B -> ¬A) -> (A -> B)

をもとに、前件肯定 modus ponens の推論規則で定理を導き出す。前件肯定とは命題図式 A と A -> B が定理であれば B も定理であるという推論だ。ウカシェビッチの公理は全てトートロジーだ。また、真理関数を V(x) とすると、V(A -> B) = T となるのは、V(A) = F または V(B) = T の時だから、この時 V(A) = T ならば、V(B) = T である。すなわち、A と A -> B がトートロジーの時は、B もトートロジーである。ウカシェビッチの公理は全てトートロジーなので、これらから前件肯定で推論される定理も全てトートロジーである。

ここで、実際の推論の過程を見てみよう。

A0 = A -> ((B -> A) -> A) ..... : P1
A1 = (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A)) ..... : P2
A2 = (A -> (B -> A)) -> (A -> A) ..... : A1 = A0 -> A2
A3 = A -> (B -> A) ..... : P1
A4 = A -> A ..... : A2 = A3 -> A4

当然ながら、公理図式 A0 .... A4 は定理である。また、それらは同時にトートロジーでもある。

ところで、上の証明で前件肯定を用いて推論されている部分を見てみる。例えば、A0 と A1 = A0 -> A2 から A2 が演繹される。公理系で前件肯定が適用される場合は、前件の論理式は全て定理であり、トートロジーであるから、後件も定理である。これは前件肯定という推論で得られる論理式は全て定理の集合の要素であることを示している。

このように前件肯定で得られる定理は全て定理の集合であるから、前件肯定の適用は、定理の集合の2要素から別の要素への関数である。ただ、この関数は任意の定理を引数とすることはできない。上の例で言えば、含意 A1 の前件の公理図式に A0 が一致していなければ前件肯定は適用されないからだ。従って、定理の集合に単純な二項演算が定義されているわけではない。

また、A -> (B -> A) のような公理の同値類の要素は、例えば A -> ((B -> A) -> A) のようなものでも、入れ子をなす含意のうちの最も外側の含意については、同値類の要素どうしの前件と後件は同じ形をしている。すなわち前件肯定は、定理の同値類についての関数とも考えることができる。この場合も前件肯定の二つの引数は同値類を自由に取れるわけではなく、パターンの適合が必要だ。

前件肯定の推論で現れるもう一つの特徴は、上の A1 のような場合に見られる。A1 は公理 P1 に公理 P2 を適用して造られた新しい定理だ。つまり、A -> (B -> A) に公理 P2 を適用してあたらしい定理、

(A -> (B -> A)) -> ((A -> B) -> (A -> A))

を演繹している。この時前件は公理なので、後件の

((A -> B) -> (A -> A)

は無条件に定理だ。このような例は、公理 P3 と 公理 P1 についても見ることができる。すなわち、

A -> (B -> A) -> (¬(B -> A) -> ¬A)

は定理なので、

¬(B -> A) -> ¬A

は定理である。これらの例の場合は、定理 A に単項演算子 P2' や P3' を作用させて、定理 B を得るという見方もできる。すなわち、P2' や P3' は定理の集合から自分自身への関数と考えることもできる。この場合、P3' . P2' のような合成写像が可能かどうかは気になるが、それは可能だ。公理のままでは問題が起きるが、公理を利用した定理の集合から自分自身への集合の写像を次のように決めると、

p1: A -> (B -> A)
p2: (A -> (B -> C)) -> ((A -> B) -> (A -> C))
p3: (A -> B) -> (¬B -> ¬A)

p1, p2, p3 の任意の順番の合成写像も定義できる。なぜなら、定理はその構造上必ず A -> B という含意の形をしているからだ。ただ、残念ながら、任意というのは言い過ぎで、p2 については関数適用できな場合がある。これは、p2 の引数が A -> (B -> C) の形をしているので後件が含意である必要があるからだ。例えば、定理 A -> A は後件が含意ではないので p2 を関数適用することはできない。

3つの公理に上の関数を適用することで、全ての定理が導き出されるということになると、公理系の構造についてずいぶん見通しが良くなると思ったが、そうはいかないようだ。

このように命題論理の公理系を定理の集合と考え、それに前件肯定や公理という関数が定義されていると考えることで、公理系にも構造があるような気がするが、力不足で解明できそうにない。公理系の構造が解明されると、命題論理の本質にも迫れるのではないかと思うと面白い。

追記

p2 の引数は A -> (B -> C) という形をしているので、A -> A のように後件が含意ではないものには適用できないが、A ⇔ A -> A なので A を A -> A に置き換えればどのような定理にも p2 を適用することができる。ただし、この p1, p2, p3 という関数について結合律が成立するかどうかは不明だ。

何れにしても、定理の集合については、前件肯定という2変数関数と、p1, p2, p3 という1変数関数が定義できることがわかる。

残念ながらこの追記は間違い。A -> (A -> A) は定理だが (A -> A) -> A は定理ではない。しかし、B -> (B -> B) なので、A -> B が定理ならば、推移律から A -> (B -> B) は定理になる。

追記2

公理から最初に導き出される定理は公理 P1, P2, P3 に p1, p2, p3 を関数適用して造られる9つの定理だ。これらの第1段階の定理は公理図式なので、これによって他の定理を変換する1変数関数を考えることができる。第2段階の定理は公理3個と新しい定理9個を含めた12個の定理に対し12個の関数を適用して新しい定理が作られる。このように演繹による新しい定理は爆発的に増加していく。


[PR]
# by tnomura9 | 2016-09-19 12:50 | 考えるということ | Trackback | Comments(0)

公理図式とは何か

この記事は管理人の単なる印象なので、読むと時間を無駄にするかもしれない。

ウカシェビッチの公理系は次の3つの公理を基礎としている。

P1. A -> (B -> A)
P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C))
P3. (¬B -> ¬A) -> (A -> B)

これらは実際は公理図式なので、無限の論理式を含んでいる。論理式とは原子式と論理結合子からなる記号列のことだ。この記号列は有限の長さであり、当面無限の記号列からなる論理式は考えないとする。P1, P2, P3 が独立であれば、これらは論理式の集合のうち、3つの共通部分のない部分集合を表している。そこで、一つの疑問が生じる。果たして、論理式の集合はこの3つの部分集合で類別できるかどうかということだ。

しかし、それは否定的なようだ。公理系では定理は全てトートロジーであり、明らかに論理式にはトートロジーでないものがある。

それでは、定理の集合はこの3つの公理で類別できるだろうか。それもおそらく間違いだろう。公理系の定理には、公理以外に前件肯定 modus ponens によって演繹される定理があるからだ。例えば、A -> A は証明可能な定理だが、どの公理図式にも当てはまらない。

そうなると、次なる疑問が生じる。定理の集合が部分集合で類別できる可能性はあるのだろうか。また、類別不可能ならば、どのような構造になっているのだろうかということだ。A -> A は定理であるが、これもまた無限の定理の集合を表している。その集合には3つの公理との共通部分はないのだろうか。

こういう風に考えてきた時に、気がついたことがある。公理から証明された定理もまた公理図式であるということだ。従って、これは特定の論理式を表すものではなく無限の論理式を表している。これは、合わせ鏡に映る無限の映像のように、とらえどころのない集合になってしまうのではないだろうか。

そこで、A -> A で表される無限の定理の中で、最小の定理はないのだろうかと考えてみた。最小の定理があれば、それを base case として無限の再帰に陥るのを防ぐことができる。例えば、A が命題変数ではなく具体的な命題 A0 を表していたとしたら、A0 -> A0 は A -> A で表される定理の集合の最小のものと言えるのではないだろうか。しかし、このアプローチも採用できない。A -> A はあくまでも公理図式であり、A には任意の命題を当てはめることができなければならないので、A0 -> A0 は A -> A の定理の集合の要素ではありえない。

従って、ウカシェビッチの公理から演繹される定理は全て公理図式であり、それは無限の論理式を含み、また、特定の命題を含んではいない。A -> A の最小の形態とは A -> A という記号の配列そのものであり、特定の命題ではないのだ。だが、記号の配列という観点からは A -> A はそれが表す無限の論理式の最小のものであるということができる。従って、A -> A が表す定理の集合は base case A -> A を持つので、再帰的定義は意味を持つ。

ところで、A -> (B -> A) が無限の論理式を表しているということは、それに含まれる任意の論理式の間に同値関係があるということだ。それを仮に * という記号で表すことにすると、a, b, c が A -> (B -> A) の表す集合の要素であれば、明らかに、

a * a
a * b ならば b * a
a * b かつ b * c ならば a * c

すなわち、これらの論理式の間には同値関係が存在している。そうして、この同値類は [A -> (B -> A)] で表すことができる。

同値関係があれば集合はその同値類で類別できる。従って、公理系における定理の集合は、[A -> (B -> A)], [(A -> (B -> C)) -> ((A -> B) -> (A -> C))], [(¬B -> ¬A) -> (A -> B)], を始めとする同値類によって類別できるはずだ。しかしながら、このような同値類は無限に存在するような気がする。公理系から演繹される定理の集合はその成り立ちから、加算集合であるが、無限の同値類を持つ集合であるということになる。しかし、加算集合であって、無限の同値類が存在するというのは矛盾しているのではないだろうか。無限の同値類を仮定してしまうと、自然数との全単射が失われることになるのではないだろうか。

こういう風に考えてくると、公理系の定理の集合に何か怪しいものが潜んでいるのではないかというような疑いが生じてくる。論理式の集合は明らかに加算のように見えるのに、それは無限集合の同値類を無限に含んでいるという気持ちの悪い性質を持っているような気がするのだ。なぜなら、無限集合の同値類を無限に持つのは、冪集合であり、無限集合の冪集合は非加算だからだ。

この疑問は自分では解決できそうにないし、多分間違っているのだが、公理図式の集合というのが一筋縄ではいかないのではないかという不安も感じる。

[PR]
# by tnomura9 | 2016-09-19 02:17 | 考えるということ | Trackback | Comments(0)

ブログを思考の道具に使うということ

このブログも随分長い間続いている。もともと3日坊主なのでなんで続いているのか自分でも不思議だ。その理由の一つは自分の学習の一つとして利用しているということだ。参考書を読んでわかったようなわからないようなあやふやな時に、他の人に説明するつもりで文章に起こしているうちに次第にアイディアが固まってきて、思いもよらなかった考え方に気づいたりすることが面白いのだ。

しかし、限界もあって、文字以外の記号の入力は煩雑だし、知識の量があがってくると、いちいち断っていては面倒な既知の知識が増えてくる。そうなると文章が必ずしもわかりやすいとは言えなくなる。表現の壁にぶつかってしまうのだ。

ブログのもう一つの利点は、書いた記事が失われないということだ。すっかり忘れてしまっていた知識なども検索できる。また、どこからでも、どのコンピュータからでも読むことができる。ブログを書き溜めてみると学習によってえられた知識がどんなに儚いものであるかがわかる。暗記していたような内容もすっかり失われているのに気が付く。

とりとめもない内容になってきたが、ブログにはいろんな利点や欠点がある。しかし、命題論理についてもどうやら表現の壁にぶつかったようなので一旦終わりにすることにした。

[PR]
# by tnomura9 | 2016-09-18 09:45 | 考えるということ | Trackback | Comments(0)

選言 ∨ の不思議

ウカシェビッチの公理には否定記号 ¬ と含意記号 -> しかないので、選言 ∨ は論理式 ¬A -> B のシンタックスシュガーだ。

A ∨ B = ¬A -> B

ちなみに、二つの真理表は次のように一致する。

A | B | A ∨ B | ¬A -> B
T | T | T (T) T | F (T) T
T | F | T (T) F | F (T) F
F | T | F (T) T | T (T) T
F | F | F (F) F | T (F) F

¬A -> B では A には否定記号がついているが、B にはついていない。A と B は含意記号 -> を挟んで裏と表の関係にあるが、これが公理 P2. (¬B -> ¬A) -> (A -> B) と組み合わされると面白い現象が起きる。

P2 は次のように対偶の論理法則を表している。これも前件は否定記号がつき、後件は否定記号がついていない。また、前件と後件では A と B の順序が逆になっている。

(¬B -> ¬A) -> (A -> B)

そこで、これを選言の論理式に適用できるように、後件の A を ¬A で置き換えてやる。

(¬B -> ¬¬A) -> (¬A -> B)

¬¬A = A だから、

(¬B -> A) -> (¬A -> B)

となり、前件も後件も同じ形になった。おまけにこの論理式はどちらも選言を表しているので、

B ∨ A -> A ∨ B

と選言の交換律が証明されてしまった。この式について A を B、B を A で置き換えると、

A ∨ B -> B ∨ A

と逆も成立することがわかる。

選言の論理式が含意記号を挟んで対照的なのと、対偶が論理記号を挟んで対照的なのが呼応して、交換法則を導くことができたが、この記号の配置の特徴が、選言記号の交換律などの独特な性質を導き出している。

公理系では証明は論理式の記号の配列の変換によって行われるので、論理式の記号の配列の特徴が重要な意味を持ってくる。形式的体系の証明は全てがこのような記号の配列の変換なので、公理や定理の記号の配列の特徴が重要な意味を持っている。

追記

ウカシェビッチの公理は

(¬B -> ¬A) -> (A -> B)

だが、A を ¬B に、B を ¬A に置き換えると、

(¬¬A -> ¬¬B) -> (¬B -> ¬B)

したがって、

(A -> B) -> (¬B -> ¬A)

と逆も定理である。従って、A -> B と ¬B -> ¬A は同値である。

(A -> B) ⇔ (¬B -> ¬A)

このため A -> B の形の定理があれば、その対偶である ¬B -> ¬A は直ちに定理であることがわかる。

この記号列のパズル的な並べ換え方が公理系の定理を証明する時の楽しみの一つだ。命題論理の公理系の定理の証明は最初のうちは何をやっているのかわからなかったが、こういう見方ができるようになってから途端に楽しくなってきた。命題論理の公理系の証明はそれ自身で十分に楽しい。

[PR]
# by tnomura9 | 2016-09-17 19:08 | 考えるということ | Trackback | Comments(0)