数理論理学には、おおざっぱに言って、2つの流派がある。 ひとつはGentzen流といわれて、推論規則の集合について研究する。 もうひとつはHilbert流といわれて、こちらは数学における証明、つまり定義定理を導く証明というものを研究するので、推論規則としては三段論法(cut)だけを使って定理を導くことがらについて研究する。たぶんこういう理解でいいのではないかと思う。 よく、矛盾があったらすべての命題が証明できるから、矛盾がでたらだめだみたいな話をするけれど、これはGentz
ワタシは論理学の専門家ではありませんが、論理学は面白いのでいろいろ考えたりします。矛盾からは任意の論理式が証明できるという、直感的にあやしいことがらについて、すこし考えたので書いておきます。 Gentzen(G)系は推論規則の、Hilbert(H)系は数学の議論の研究が目的のようだ。 論理には、定義/公理と推論規則の二つの部分がある。 Gでは、公理はA⇛A(スキーマとかシェーマと呼ばれるやつ)のみで、論理演算さえも推論規則で決めてる。 その世界で、矛盾から任意の論理式
表現を書く unificationを書きたいのだけど、unificationという理解だと、どうしても手続きになってしまう。 最初は仕方がないと思う。 いろいろやってみたけど、なんか間違っているような気もする・・・ 一番簡単な項として、定数aを考えてみる。 項がaだけのclauseの集合Σがあったとする。このときのDの定義はどうなるだろうか。 まず、項というより、表現(Expr)を定義してみる。 Σ0 : (clauseの集合0) +Expr(a) 定数はaしかな
一階述語で、定数とか関数の形とかの表現を定義してみる。 数理論理学の教科書などでは、普通はこういう定義だと思う。 定数記号をa,b,c,…とし、変数記号はx,y,z,…、関数記号をf,g,…とする。 このとき項は次のように定義される。 1) 定数記号は項である。 2) 変数記号は項である。 3) fを関数記号とし、t1,t2,…を項とするとき、f(t1,t2,…)は項である。 4) 1から3までで定義されるもののみが、項である。 まず、これを一階述語で書けないのは、いくつ
proverを作っているので、述語論理でproverを定義し、それの証明の様子をみてみたい。 とりあえずの目標としてUnificationをと考えたが、その前に必要なのはSubstitutionであり、そもそもExpressionの定義が必要。 表現(Expression; Expr)と呼んでいるのは当分はf(x,y)みたいなtermでよいと思うけれど、変数と定数の区別は気にしなくてよいだろう。(代入は論理の操作ではないので、述語記号やリテラルなどを区別したり、考える必要
clauseの集合Σが与えられた時、Σの中に存在する可能なすへてのmguの集合M = {<L1:L2>| ∀Li ∈ ∀c ∈Σ}は有限であり、Σからのどの証明もその各stepのmguはこのMのどれかのインスタンス(代入{x←t1} が {x←t2}のインスタンスである({x←t1} ⊑ {x←t2})とはt1⊑t2であること)になっている。 resolutionでは、pairとするclauseごとに共通変数がないことが必要なので、もしも同じ変数が出現していたら話がややこし
Σを論理式の集合(考えているのはclauseの集合でしかないけど)とし、そこに入力、出力の指定/条件をつけくわえると、あるプログラムPの仕様と考えることができるだろう。 このとき、ある入力の値に対して計算結果を得るPの計算過程は、もとのΣのある証明に対応する。対応するというのは、証明から計算過程を機械的につくれるし、計算過程から証明も機械的に作れるという意味でいう。 このような個別の証明は入力の値にそれぞれ存在するもので、決してプログラム自体が証明なのではない。そういう証
レシピを書いていたとき、証明ができやすいように、書き直すということを何度もやった。 ひとつの述語をあちこちで使い回すと、曖昧になり、証明を作るのが難しくなる。それを回避するため、述語をわけて書いてみたりした。 数学で、同じ定理を証明するのにいろいろな方法があるのと、簡単には比較できないけれど、そういうことはあるかもしれない。 証明のしやすさを考えて、述語の使い方を変えるのは、プログラムのアルゴリズムを工夫するのと同じような感覚なのかなと思う。 だとすると、prover
懐中電灯とはなにか?! 懐中電灯を通して、仕様と故障箇所検出について考えてみる。 1. 懐中電灯の目的 懐中電灯の目的は何か? 漠然と言えばそれは「闇を照らす」ことだと思う。 なにか ⇒ 闇を照らす … (1) の「なにか」にあたるもののひとつが懐中電灯と言えるだろう。 (1)には室内灯や街灯や車のライトなども含まれるから、「懐中電灯」と減退したい場合には「持ち歩きができる」という条件をつけるべきだ。 なにか ⇒ 闇を照らす ∧ 持ち運びができる … (2)
ケーキのレシピを述語論理で書いてみようと思う。 ケーキのレシピを調べてはみたものの、作ったこともないし、述語論理で書きやすいように変えているから、本当にケーキを作る人からみたら、これはケーキのレシピではないと言われるだろう。 こういうものを述語論理で書くとこんなふうになるかなという好奇心で書いていることを暖かく見守ってほしい。 料理のレシピは、アルゴリズムのようでアルゴリズムではない。なにかもっとふんわりとして、詳細は調理する人間に任されている何かだと思う。 そういうもの
noteにテキストをコピペすると、改行が無視されて全部くっついてしまう。 かと思えば、文章の塊は空行でブロックに分けられる。 つらい
真夜中に中央公園を通り抜けようと考えたのはなぜだったろうか。 深夜でも公園は取り囲まれているビルの灯りで隅々まで見通せる。タチの悪い乱暴者が潜んで いればすぐにわかるはずだ。それでも、夜の闇の塊はあちらこちらにおちているだろう。そんな公 園を誰が通り抜けようとしたのだろうか。 真夜中に中央公園を通り抜けていったのは誰だろう。 それは公園の向こう側にある託児所に預けていた子供を引き取りに行こうと考えていた誰かかも しれない。託児所の終了時間が迫っていて公園を通り抜けなければ
∀と∃と反証法、1引数の場合 (1)]の続き。 4. Σ2=Σ1 ∪ {-B(3), -B(4), -B(5)}の場合 [述語論理で反証に迷う(1引数の場合) 1]では、1と2の枡についてだけ考えてきたが、最初に、コインが置かれる枠が5つあると書いたのに、1と2以外の枠については何も触れてこなかった。コインを頭に思い浮かべているならば、暗黙のうちに{-B(3), -B(4), -B(5)}は前提となっていたかもしれない。 暗黙にそう思っていたとしても、 Σ1 ⊢ -B
述語論理でResolutionを使う場合、命題論理と同じく反証法(refutation)を用いることになる。そこで、述語論理で新しく登場した∃xや∀yを含むconjectureについて、どういうことになるのかを考えてみる。 最初は1引数の述語の場合について考える。 次のような状況であるとする。 例) 黒いコインを2枚を、5つの(1から5まで番号がついている)枠に適当に置いて、それをセンサーで識別する。センサーはその結果をFactとして論理式を作り出力する。たとえば
Unificationは2つの式(論理式や項)から、代入mguを計算するアルゴリズムである。 以下に示す例では、x, y, zは変数、a, b, cは定数、f, g, kは関数記号とする。 2つの式とmguの例) t1,t2 を式として、<t1:t2>でunificationした結果のmguを表す。 (1) <a : b> : unifyできない (2) <f(a) : g(b,c)> : unifyできない (3) <x:b> = {x←b} (4) <f(
Resolutionでは、Unificationによってmguという代入を作るが、Resolutionで用いる代入はすべてこのmguである。2つのclausesが共通の変数を持たないように、変数名を付け替える操作で代入を使う場合は、別の方法で作ることになるが、以下の話ではそれは気にしなくていい。 まず、表現(式)に代入を適用する操作を次のように定義しておく。 代入表現 代入は、siが記号(定数や変数)で、eiは表現(式)であるとして、 {s1←e1, s2←e2, …
