一階述語論理

グロスについて

グロス とは例文の下に書かれる逐語訳です。ここで使っているグロスには独自の規則があるのでそれについて述べます。

グロスは1単語につき、アリティ部、品詞部、情報部の三つの部分に分かれます。但し、このうちいくつかが空文字列である場合もあります。

アリティ部は、その語が統語的にどのような働きをするのかを示す部分で、空文字列、{、}、/、//のいずれかの形を取ります。アリティは多くの場合、品詞によって一意に決まっています。

品詞部はPREやNEGなど、英字大文字3文字の略称で記述します。但し、述語は頻出するので、品詞部は空文字列(無標)とします。

情報部は英字大文字以外の文字体系で書かれる部分です。ここに書かれる情報は品詞によって異なります。

構文木と句

構文木 とは、単語同士の繋がりを木構造で表現したものです。

Varhilの文法はポーランド記法と括弧を併用した形をしているので、以下の規則によって単語列から一意に構文木を構成できます。

• アリティが空である語は末端ノードである
• アリティが/である単語は、後ろに1個の枝を伴って枝となる（1個の子を持つ内部ノードとなる）
• アリティが//である単語は、後ろに2個の枝を伴って枝となる（2個の子を持つ内部ノードとなる）
• アリティが{である語は、アリティが}である語と括弧のように対応して、その内部の句を伴って句を形成する

構文木の枝のことを 句 と呼びます。句に対して一定の手続きをすることで、その意味、つまり（未完成の）論理式を計算することができます。末端に近い小さな句から順に、再帰的な計算をすることで、文全体の意味を計算するのがVarhil文の解析です。

句は論理式の他に、述語ポインタか変数のどちらかを、付加的な情報として持つ場合があります。述語ポインタを持つ句を 述語句 、変数を持つ句を 名詞句 と呼びます。

但し、述語ポインタとは、論理式中のある述語記号の位置の情報です（論理式中に同じ述語記号が複数回現れた場合でも、述語ポインタはそれぞれを区別します）。

述語と格

述語

述語 は述語論理の述語記号を表現する品詞です。Varhilの内容語はすべて述語になります。

格

格 は述語と引数の関係を表す形態素です。 各々の述語には、それが受けることができる有限個の格が決まっていて、それらのすべてに議論対象を対応付ける（受けることができる格の集合から議論対象への写像を与える）ことで厳密に真偽値が定まります。例えば、述語「食べる」は動作主を表す格「が」と、対象を表す格「を」に議論対象を対応させることで、真偽値が決まります。（一部のプログラミング言語にある名前付き引数(named parameter)に似ている）

格はあくまでも述語に対して与えるための添え字であって、格自体の解釈には厳密な意味は要求されません。ある述語がどの格を取るか、異なる述語のどの引数を同じ格とするかに論理的な必然性はなく、辞書作成の恣意によります。

ここでは例として以下のような述語を使います。

リンゴだ(は:x)

xはリンゴだ

人間だ(は:x)

xは人間だ

赤い(は:x)

xは赤い

食べる(が:x, を:y)

xがyを食べる

述語は単独で述語句になることができます。この場合、論理式は引数を持たない状態の述語記号であり、述語ポインタはその述語記号を指します。

pina:リンゴだ

リンゴだ()

moku:食べる

食べる()

変数と限定詞

変数

変数 は、述語論理の変数記号に対応する概念で、一つの議論対象を意味します。

限定詞

限定詞 は間接的に変数を表現する品詞です。

限定詞は、孤立限定詞(au)、新規限定詞(aで始まり、'区切りで母音が続く機能語)、継承限定詞(iで始まり、'区切りで母音が続く機能語)、終了限定詞(uで始まり、'区切りで母音が続く機能語)の4種類に細分化される。また、新規限定詞、継承限定詞、終了限定詞の二文字目以降を ラベル と呼ぶ

文中に出現した限定詞と変数の対応は以下のように決定されます。

• 孤立限定詞は出現毎に他のどの限定詞の出現とも異なる変数を指す
• ラベルが異なる限定詞は、異なる変数を指す
• 新規限定詞は、それまでに出現したどの限定詞とも異なる変数を指す
• 継承限定詞と終了限定詞は、ラベルが同じ限定詞の、一つ前の出現と同じ変数を指す
• 終了限定詞は、それ以後に出現するどの限定詞とも異なる変数を指す
• 上記条件が矛盾する場合、エラー

ある番号の限定詞を語順で見て最後に使用するとき、あるいは、ある番号の限定詞をその変数を指して使う最後のときは、必ず、新規限定詞を使うことで変数が新たに割り当てられたことを明示します。 また、各々の限定詞を最後に使用するときは 終了限定詞を使うことで、その変数がそれ以後使われないことを明示できます（必須ではない）。

いかなる状況に於いても、例えば文や段落を跨いだ場合や、発話者が変わった場合でも、それぞれの限定詞が表す変数はリセットされません。これを利用すれば、限定詞を介して以前の段落で使った変数や他の発話者が使った変数を以後の段落で参照することもできます（そうされたくない場合は終了限定詞を使えばよい）が、逆に以前とは異なる変数を指したいときは必ず新規限定詞を使う必要があります。

限定詞のグロスはラベルの代わりに番号を使います。新規限定詞のグロスはDET番号+、継承限定詞のグロスはDET番号、終了限定詞のグロスはDET番号-とします。また、孤立限定詞のグロスはDETとします。

限定詞は単独でその変数を表す名詞句になれます。この場合、論理式として空積（真）を、変数としてその名詞が表す変数を表します。

au:DET

⊤

前置詞

前置詞 は格を指定して述語句に名詞句を付加する品詞です。e で終わる機能語が前置詞であり、e 以前の部分は格に対応します。

前置詞は直後に名詞句、その後ろに述語句を取って述語句を成す前置二項演算子であり、述語句の述語ポインタが表す述語記号の、前置詞が表す格に、名詞句が表す変数を割り当てる操作を行います。形成される述語句は、それぞれの論理式の論理積と、述語句の述語ポインタを表します。

前置詞のグロスは//PREの後ろに格を表す訳語等を続けた形とします。

e://PREは au:DET pina:リンゴだ

リンゴだ(は:x)

fe://PREが a:DET0+ be://PREを a’a:DET1+ moku:食べる

食べる(が:x, を:y)

引数の省略

文の解釈が最後まで終わっても述語が受けるすべての格に引数が割り当てられていなかったときは、その場限りの変数（つまり孤立限定詞）を補って解釈します。

従って、前置詞の第一引数が孤立限定詞であるとき、その前置詞と孤立限定詞は省略できます。

関係詞

関係詞 は格を指定して名詞句に述語句を付加する品詞です。 ei で終わる機能語が関係詞であり、ei 以前の部分は格に対応します。

関係詞は直後に述語句、その後ろに名詞句を取って名詞句を成す前置二項演算子であり、述語句の述語ポインタが表す述語記号の、関係詞が表す格に、名詞句が表す変数を割り当てる操作を行います。形成される名詞句は、それぞれの論理式の論理積と、名詞句の変数を表します。

関係詞のグロスは//RELの後ろに格を表す訳語等を続けた形とします。

例えば、 名詞句//RELは リンゴだ DET は論理式 リンゴだ(は:x)を表しつつ、その変数xを指す限定詞の代わりとして、前置詞の第一引数や、関係詞の第二引数として使うことができます。

e://PREは ei://RELは pina:リンゴだ au:DET loja:赤い

リンゴだ(は:x) ∧ 赤い(は:x)

fe://PREが ei://RELは jana:人間だ au:DET be://PREを ei://RELは loja:赤い ei://RELは pina:リンゴだ au:DET moku:食べる

人間だ(は:x) ∧ リンゴだ(は:y) ∧ 赤い(は:y) ∧ 食べる(が:x, を:y)

ei://RELは pina:リンゴだ au:DET

リンゴだ(は:x)

ei://RELは loja:赤い ei://RELは pina:リンゴだ au:DET

リンゴだ(は:x) ∧ 赤い(は:x)

無標格と名詞

名詞や形容詞っぽい語の主語（英語のbe動詞の主語）に対応する格（前置詞 e、格助詞 eiで示される）は、格を示す部分が空文字列になっています。この格を 無標格 と呼びます。（繰り返しになりますが、何が「名詞っぽい」「形容詞っぽい」述語であるかは辞書作成の恣意によります。ここで重要なのはその述語が名詞っぽいかどうかではなく、eを受けるかどうかです。）

無標格を表す関係詞が二番目の引数に孤立限定詞を取っている場合（ある述語句が無標格関係詞と孤立限定詞に挟まれている場合）、さらにその名詞句が前置詞の第一引数や関係詞の第二引数に置かれていたとき、その関係詞と限定詞は省略できます。つまり、無標格を取る述語句は単独で名詞句になれます。この名詞句や名詞句になれる述語を便宜上 名詞 と呼びます。

これは、前置詞の第一引数や関係詞の第二引数に述語句が置かれていたとき（またその時に限って）、無標格関係詞と孤立限定詞（つまりその場限りの変数）を補うことで、一意に復元することができます。

e://PREは pina:リンゴだ loja:赤い

リンゴだ(は:x) ∧ 赤い(は:x)

be://PREを ei://RELは loja:赤い pina:リンゴだ moku:食べる

リンゴだ(は:x) ∧ 赤い(は:x) ∧ 食べる(を:x)

文

句を0個以上並べたものが 文 です。特に接続詞のようなものを置く必要はありません。

文はVarhilにおけるトップレベル要素であり、一つの文が一つの命題（論理式）に対応します（つまりVarhil文は全体が文になっています）。

文は、各句が表す論理式の論理積の、すべての変数を存在量化した論理式を表します。但し、否定を含む場合はその限りではありません（後述）。

e://PREは a:DET0+ pina:リンゴだ e://PREは i:DET0 loja:赤い

∃x リンゴだ(は:x) ∧ 赤い(は:x)

否定と量化

否定節

文を nouとnoiで挟むことで、その文が表す命題の否定命題を表す句になります。これを 否定節 と呼びます。否定節も他の句と並べて文を構成したり、他の否定節に入れ子にしたりできます。

nouを 否定開始 と呼び、グロスは{NEGとします。また、noiを 否定終止 と呼び、グロスは}NEGとします。

ある変数がある否定節の中ではじめてつかわれた場合（つまり、あるラベルの限定詞が否定節の中で初期化された場合）、その変数はその否定節の中からのみ参照することができます。その否定節が終わった後にそのラベルの限定詞を使った場合、否定節の中での初期化は無視され、否定節より前で割り当てられていた変数が対応します。

nou:{NEG e://PREは a:DET0+ pina:リンゴだ e://PREは u:DET0- jana:人間だ noi:}NEG

￢ (∃ x リンゴだ(は:x) ∧ 人間だ(は:x))

a:DET0+ nou:{NEG e://PREは i:DET0 pina:リンゴだ e://PREは i:DET0 jana:人間だ noi:}NEG

∃ x ￢ ( リンゴだ(は:x) ∧ 人間だ(は:x))

単独否定

noは、直後の句を否定する前置単項演算子です。これを 単独否定 と呼び、グロスは/NEGとします。

前置詞や関係詞、述語の前にあればそれが形成する述語句や名詞句が表す論理式が、それぞれその否定に置き換わります。単独否定が述語句や名詞句を否定するとき、その述語ポインタや変数は変化させません。

ちなみに単独否定は限定詞の前にも置けますが、これは空積の否定（つまり矛盾）を表すのであまり使いどころがありません。また、単独否定を二つ重ねたり、否定節の前に置いたりすることもできますが、これは二重否定にあたるので、なくても同じです。（古典論理に従い、二重否定を除去しても意味が変わらない意味論を採用します。）

限定詞と変数の対応については否定節と同様です。

no:/NEG fe://PREが au:DET be://PREを pina:リンゴだ moku:食べる

￢ ∃x ∃y (リンゴだ(は:y) ∧ 食べる(が:x, をy))

fe://PREが au:DET no:/NEG be://PREを pina:リンゴだ moku:食べる

∃x ￢ ∃y (リンゴだ(は:y) ∧ 食べる(が:x, を:y))

fe://PREが au:DET be://PREを pina:リンゴだ no:/NEG moku:食べる

∃x ∃y (リンゴだ(は:y) ∧ ￢食べる(が:x, を:y))

fe://PREが au:DET be://PREを no:/NEG pina:リンゴだ moku:食べる

∃x ∃y (￢リンゴだ(は:y) ∧ 食べる(が:x, を:y))

論理表現

一階述語論理での各論理記号（否定￢、論理積∧、論理和∨、含意⇒、同値⇔、存在量化∃、全称量化∀）がVarhilでどう表現されるか見ていきましょう。

今まで見てきたように、任意のVarhil文は否定開始、否定終止で挟むことでその否定を、並べることでそれらの論理積を表現できます。また、すべての変数は無標で存在量化されているので、∃も表現できたといえるでしょう。

論理和 P∨Q は古典論理上で ￢(￢P∧￢Q) と等価であるので、Varhilではこの組み合わせで表現します。

nou:{NEG nou:{NEG ～:～ noi:}NEG nou:{NEG …:… noi:}NEG noi:}NEG

～ ∨ …

含意 P⇒Q は古典論理上で￢(P∧￢Q) と等価であるので、Varhilではこの組み合わせで表現します。

nou:{NEG ～:～ nou:{NEG …:… noi:}NEG noi:}NEG

～ ⇒ …

同値 P⇔Q は (P⇒Q)∧(Q⇒P) の糖衣構文であり、古典論理上で ￢(P∧￢Q)∧￢(￢P∧Q) と等価であるので、Varhilではこの組み合わせで表現します。

nou:{NEG ～:～ nou:{NEG …:… noi:}NEG noi:}NEG nou:{NEG nou:{NEG ～:～ noi:}NEG …:… noi:}NEG

～ ⇔ …

全称量化は ∀x; P は古典論理上で ￢∃x￢Pと等価であるので、Varhilではこの組み合わせで表現します。（限定詞も否定節と並列することができるので、二重の否定の間に限定詞を置けばよいです）

nou:{NEG a:DET0+ nou:{NEG ～:～ noi:}NEG noi:}NEG

∀x ～

従って、以上のような古典論理に従った同一視を行えば、開論理式を除く一階述語論理のすべての論理式と等価な表現をVarhilでも表現できるといえます。

なお、これらは任意のVarhil文同士の結合ができることを示しているのみで、条件が整えば（単独否定を使える場合などは）より短い形で書くことができます。

no:/NEG e://PREは au:DET no:/NEG pina:リンゴだ

∀x リンゴだ(は:x)

no:/NEG e://PREは pina:リンゴだ no:/NEG loja:赤い

∀x リンゴだ(は:x)⇒赤い(は:x)

no:/NEG e://PREは no:/NEG pina:リンゴだ no:/NEG jana:人間だ

∀x リンゴだ(は:x)∨人間だ(は:x)

また、述語論理には述語記号の他に定数記号や関数記号が存在するが、定数記号は、ある一つの値に対して真となる1変数述語記号として、アリティnの関数記号は、ある引数が一つの値に対してのみ真となるアリティn+1の述語記号として、表現できます。

形式文法

ここまでの文法を形式文法にまとめると、以下のようになります。

<文>
 <句>*

<句>
  <述語句>
  <名詞句>
  <否定開始> <文> <否定終止>

<述語句>
  <前置詞> <名詞句> <述語句>
  <単独否定> <述語句>
  <述語>

<名詞句>
  <関係詞> <述語句> <名詞句>
  <単独否定> <名詞句>
  <述語句>
  <限定詞>

<限定詞>
  au
  a('[aeiou])*
  i('[aeiou])*
  u('[aeiou])*
<述語>
  (([^aeiou'][aeiou]){2,})
<前置詞>
  ([^aeiou]?)e
<関係詞>
  ([^aeiou]?)ei
<単独否定>
  no
<否定開始>
  nou
<否定終止>
  noi