計算機とその周辺: What I Talk About When I Talk About Computers: 9月 2009

2009年9月27日日曜日

【LPL】9章限量入門 (2)

9.4 限量子の意味論 (Semantics for the quantifiers)
- 自由変項を含む論理式 (wffs)の真理値:
  自由変項を含む論理式は、真理値をもたない。真でも偽でもない。
- 充足 (satisfaction):
- 充足の取扱いは論理学の方言によって微妙に異なる。
- この本では次のように取扱う。
  - S(x)が、自由変項xのみを含む論理式であるとする。
  - あるobjectについてS(x)を充足するかどうか調べたいとする。
  - そのobjectはb という名前が指しているとする。
  - S(x)におけるxの自由な出現をすべてbに書換えたものをS(b)と呼ぶ。
  - S(b)が真ならば、そのobjectはS(x)を充足する(satisfies)という。
- それを指す名前が存在しないobjectsについてはどうするか。
- 一時的に名前を作ってそれを指させることによって対応する。
- ∃の意味論:
  ∃xS(x)
  S(x)を充足する対象が少なくともひとつ存在する。
- ∀の意味論:
  ∀xS(x)
  すべての対象がS(x)を充足する。
- 談話領域 (domain of discourse):
  - 限量子を含んだ文の真偽は、絶対的なものではなく、相対的なものである。
  - なぜか。それらが充足する、ということを判定するための、なんらかの対象を含む(空でない)集合が存在することを暗黙の前提としている。それに対して相対的、ということ。
  - この集合を、談話領域 (domain of discourse) や限量領域 (domain of quantification) と呼ぶ。
  - 空な談話領域も含めてFOLを構成することもできる。しかし、それは労多くして幸少い。(Quineは空な領域も対象としていた)

こつこつ。

【LPL】9章限量入門

さあ、限量 (quantification) だ。
あせらず、ゆっくりいこう。頭の方は用語の導入が多いので、メモをとりながら。

前説
- 名前 (names):
  Max, Claire など。
  FOLの個体定項 (constant symbols) に対応している。
  普通名詞 (common nouns) とも言う。
- 限定詞 (determiners):
  every, some, most, the, three, no など。
  普通名詞と結び付けて、名詞句 (noun phrases) をなす。
- 限量表現 (quantified expressions):
  限定詞を使った名詞句のこと。
- 限量文 (quantified sentences):
  限量表現を含む文のこと。
- 真理関数的結合子 (truth-functional connectives)と限量 (quantifications) の違い
  限量文の真理値は、それを構成している文の真理値からは決定できない。
  例えば、
  Every rich actor is a good actor.
  の真理値は、rich actorsという集り(collection)とgood actorsという集り(collection)の間の関係によって決まる。
- 隠れた限量 (hidden quantification):
  例えば、論理的に含意する (logically implies) は非真理関数的結合子である。PとQの真理値だけでは、論理的に含意するかどうかは決まらないから。
  これは限量だ。Pを真にするあらゆる状況において、Qも真になる、ということなので、状況・対象・限量を暗黙に含んでいる。
- FOLの限量子 (quantifiers of FOL):
  FOLに含まれる: some, every
  FOLに含まれないが、表現できる: three, no, whenever
  FOLで表現できない: most, many
9.1 変項と原子論理式 (Variables and atomic wffs)
- 変項 (variables):
  副次的な記号 (auxiliary symbols)。
  項 (term)の新種。
  定項 (constants) を置けるところには変項を置ける。しかし、意味に違いがある。定項は具体的な対象を指す。変項は、限量子と述語との関連を明確にするための「場所取り (place holder)」の機能を担う。
- 原子論理式 (atomic well-formed formulas, or atomic wff)
  変項の導入によって、Home(claire)などとしていたものから敷衍して、Home(x)などというものができることになる。これを原子論理式 (atomic wff) と呼ぶ。
  原子論理式は文 (sentences) ではない。
  限量子と一緒に使うと文になることができる。
  ただし、論理式に現れる変項を束縛する限量子とともに使われた場合に限る。
9.2 限量子記号 : ∀ と ∃
- 全称限量子 (∀) (Universal quantifier):
  ∀xHome(x)
  「すべての対象xについて (for every object x)」
- 存在限量子 (∃) (Existential quantifier):
  ∃xHome(x)
  「ある対象xについて (for some object x)」
9.3 論理式と文 (Wffs and sentences)
- 論理式 (wffs):
  Doctor(x) & Smart(x)
  などは、atomic wffsを真理関数的結合子で結合したものである。atomic wffsは文じゃない。これは新種だ。
  これらを論理式と呼ぶ。
- 論理式の定義:
  論理式は再帰的に定義される。
  P,Q,P1,...,Pnを論理式とする。νを変項とする。このとき次のものは論理式である。
  - ~P
  - P1 & ... & Pn
  - P1 | ... | Pn
  - P -> Q
  - P <-> Q
  - ∀νP (Pの中のνは束縛される)
  - ∃νP (Pの中のνは束縛される)
- 限量子の作用域 (scope of quantifier)
  変項は、自由変項 (free variable)、束縛変項(bound variable)の2つのどちらかである。
  束縛をするのは限量子である。
  論理式において、限量子が束縛している範囲を作用域と呼ぶ。

こつこつ。

【LPL】8章条件文の論理

8章完了。

8章だけで練習問題が53問。タフだった。。。
内容的には2つのことだった。
- 条件文の証明について、非形式的なものと形式的なものを導入。
  これで真理関数的結合子の演繹体系が構築完了となった。
- 真理関数的結合子の演繹体系の健全性と完全性の紹介。
用語の整理でありがたかったこと。「健全な論証」と「演繹体系の健全性」との両方に「健全」という言葉がでてくるが、ほとんど関係がないということ。「真理関数的に完全な結合子セット」と「演繹体系の完全性」との両方に「完全」という言葉がでてくるが、これもしかり。
完全性と健全性の覚え方というか、表現に仕方も勉強になった。次のように覚えておくとよい。(Ftを真理関数的結合子の演繹体系とする)
- Ftの完全性：トートロジー的帰結ならば、Ftで証明可能。
- Ftの健全性：トートロジー的帰結でないならば、Ftで証明不可能。
健全性の表現については、この対偶の場合が多いが、こちらの方が実用的である。

第一部命題論理が完了。

ついに、第二部限量子、だ。
この本では挫折せずにやりきれるのだろうか。。。

こつこつ。

2009年9月23日水曜日

【LPL】7章条件文 (2)

7章完了。
練習問題32問。結構時間がかかった。

条件文にて、帰結と同値が論理的真理に降りてきた。これを足掛りに、次章で「代入」が自然演繹にも現われるのかな？
接続詞(結合子)が真理関数的かどうかを判断する手法として、敷衍によって矛盾が発生するかどうかというチェックが紹介された。これは、自然言語とFOLとを相互翻訳するのにとても役立つ。
練習問題後半は、ソフトウエア提出ではなく、担当教師提出のものが多かった。こういうの、担当教師や友人と議論できる機会がないのが残念。そうとう伸びが違うんだろうなぁ。

次は、Quantification前、最後の一章。
こつこつ。

2009年9月22日火曜日

【LPL】7章条件文

条件文(conditional)と双条件文(biconditional)についてはQuineでしっかりやった。
ここではLPLにおける条件文の取扱いの要点を確認する。

まず条件文。

英語の直接法のifに対応したものであり、実質的条件文と呼ぶ。仮定法はFOLでは取り扱わない。
P if Q は、FOLに翻訳すると、Q → P である。このとき、"QはPの十分条件である"と言う。
P only if Q は、FOLに翻訳すると、P → Q である。このとき、"QはPの必要条件である"と言う。
unless について。次のものは同じ状況を表現している。
- Unless P, Q.
- Q unless P.
- Q if not P.
最後の文をFOLに翻訳すると、~P → Q となる。
実質的条件文によって、論理的帰結の概念を論理的真理の概念に組込むことができる。
すなわち、文Qが前提P1,...,Pnの論理的帰結である云々ということは、(P1|...|Pn)→Qが論理的真理であると表現できてしまう。

続いて双条件。

双条件も、実質的双条件。P ↔ Q。
英語、とくに数学者によるバリエーション。
- P if and only if Q.
- P iff Q.
- P just in case Q.
「論理的に同値 ⇔」を論理的真理の概念に組込むのに使える。

さあ、練習問題だ。

こつこつ。

【LPL】6章形式的証明とブール論理

6章完了。

自然演繹(natural deduction) を初めて学べた。うれしい。今まで読んだ論理の本だと結構後半で導入されていたので、辿りつくまえに挫折していた。
自然演繹に、いわゆる代入が存在しないのが興味深い。(同一性不可識別は存在する)
部分証明がそれらのかわりの役割を担っている感じ。
自然演繹はわかりやすいが、「同値な表現の代入」ができないので、証明に結構手間がかかる。このあたり、Quineが気にしていたところか。
ただし、Fitchには taut con、fo con、ana conがあるので、学習目的でなければそれらの手間ははぶける。

quantification まであと二章。

こつこつ。

2009年9月20日日曜日

【LPL】5章ブール論理の証明方法

5章完了。

私が今までに読んだ本とは違っていて、興味深い点がいくつか。

例えばQuineでは、論じているドメインの知識は捨ててしまって、それでも残るのが論理という言語や思考の性質、という感じであり、他にもそういう本がけっこうあり、それは確かに論理の本質なのだが、日常の議論においては、ドメインの制約も論証の一部として利用しているということから、どうもすわりが悪かったのが本当のところ。この本は、その点を明確にし、ドメインと論理の兼ね合いも分析的帰結(Analytic Consequences)として、TW-帰結(TWにおけるドメイン知識活用)、TT-帰結、FO-帰結、論理的帰結などと分類しつつ適切に導入している。これはありがたい。
非形式的証明という名のもとに、自然言語での証明についてもページを割いているのだが、これが前項と相俟って内容豊かになっている。すなわち、論理の推論規則だけだと、骨組みだけの荒涼とした証明となるが、ドメイン知識による推論もカバーしているので、日頃、コンピュータ科学や数学で使われている証明に近い内容になる。しかも、どの推論が(ある意味)pure論理で、どの推論がドメイン知識かという関係も明確にしてそれをやってくれる。

これだけでもこの本を読んだ価値はあった。

こつこつ。

2009年9月19日土曜日

【LPL】4章ブール結合子の論理

新規導入の用語が多いので、私家版整理。

論理的真理(logical truth)
- 文のこと。
- どのような前提達であっても、その論理的帰結になれるような文。
- 例：a = a.
- 例：P | ~P.
真理関数的(truth-functional)
- 構成要素となっている文の真理値からのみその真理値が決まるもの。
- ~、&、|という結合子は真理関数的。
- 真理関数的ではない例："it is necessarily the case that"という結合子を考える。これは"it is necessarily the case that S"としたとき、Sの真理値のみから全体の真理値がきまるわけではない。こ
TW-可能(TW-possible)
- 「物理的」ということよりも「論理的」ということの方がより根源的というか、なんというかである。例えば、「物理的」に言えば、アインシュタインの相対性理論の範囲では、光速を超えて移動することは不可能である。しかし「論理的」に言えば、光速を超えて移動するということは可能である。
- スタートレックで、超光速で宇宙船が移動しているのは、物理的にはありえないが、論理的にはありえる、ということでもある。
- このように、一般的な会話において、「何かが可能」ということは、論理的なこととと物理的なことが混在しているものである。
- Tarski's World も、それ固有の物理世界を成している。
- Tarski's World 上に構成可能な世界のいずれかにおいて真となりうる文のことを、TW-可能と呼ぶ。
論理的に可能(logically possible)、論理的可能性(logical possibility)
- 論理的に可能(な文)というのは、曖昧な定義だが、それを真とするような、状況というか状態というか談話の世界というものが存在する、ということだ。
- これは曖昧でもやもやするのだが、上のTW-可能なものは、論理的に可能であることは間違いない。逆は、間違いないとは言えないけど。
真理値表の方法(truth table method)
- 構成する文の真理値から、全体の真理値を算出する方法。
TT-必然(TT-necessary)、トートロジー(tautology)
- 真理値表にて、構成する文の真理値に関わらず全体は常に真となる文をTT-必然と呼ぶ。ただし歴史的理由によりこれはトートロジーとも呼ばれている。本書ではトートロジーと呼ぶことにする。
- トートロジーは論理的真理である。
- 注：FOLの文 a = a は論理的真理だがトートロジーではない。
TT-可能(TT-possible)
- 真理値表で少くともひとつの行で真となるなら、TT-可能であるという。
TW-必然(TW-necessary)
- 文Sがあるとする。Tarski's World では、いろいろな世界を構成可能だが、そのような世界の中で、Sが真理値を持ち得るすべてのものについてSが真となるならば、SはTW-必然であるという。
- Sが真理値を持ち得るすべての世界というのは、Sを構成している文に含まれるすべての名前について、対象が存在しているような世界である。
必然性の関係
- TT-必然(トートロジー) ⊂ 論理的に必然 ⊂ TW-必然
- 「論理的に必然」の定義は曖昧にも関わらず、この関係は厳密に成り立つ。
可能性の関係
- TW-可能 ⊂ 論理的に可能 ⊂ TT-可能
- 「論理的に可能」の定義は曖昧にも関わらず、この関係は厳密に成り立つ。

こつこつ。

ちょこちょこ進めていた3章が完了。

この本の強みは、やはり付属ソフトウエアだ。
テキストの説明は、意図的に厳密さを求めていない部分が散見される。
こんな簡単な説明じゃ初学者は混乱するのでは、というところもあるが、付属ソフトウエアで問題を解き、可視化を体感すると、そこから意味が読取れるようになっている。

Tarski's world にバグがあるのがおしい。

Ascii文字と論理記号との対応の例を得たのもうれしかった。

記号 : Ascii
= : =
≠ : #
¬ : ~
∧ : &
∨ : |
→ : $
↔ : %
∀ : @
∃ : /
⊆ : _
∈ : \
⊥ : ^

Emacsのキーバインディングを決めるときなどは、自己流じゃなくて、これに準拠しようと思う。

こつこつ。

2009年9月15日火曜日

【LPL】2章原子文の論理

とりあえず、2章原子文の論理まで完了。

ここまではとてもよい感じ。

この段階での等号(同一性)に基づく代入が、同一者不可識別性という定義にすぎない、という知識はありがたい。

ただ、どの論理の本も命題論理の間は簡単なんだよね。。。

問題は quantification。

そこに入ったところで判断することにする。

とにかくFOLを自分の武器と思えるくらいに習熟したい。

やはり、それがないと、何をやっても砂上の楼閣な気がする。

こつこつ。

2009年9月13日日曜日

【MoL】別の本にスイッチを検討

AIMAの推薦ということで、Quine の Methods of Logic をやってきたが、どうも私では英語力が足りない感じ。英語の勉強をしている度合いがどんどん高まってしまっている。英語力は英語力で向上したいのだが、この本を使ってそれをというのは本意ではない。

そこで、別の本、ということで、

論理学の基礎と演習 (Language, Proof and Logic)

を試してみている。とりあえず、一章を完了したところではいい感じ。

この本の特色は、

演習が豊富。
演習をしたり論理を試すためのソフトウエアがついていて、遊びながら進める。
演習問題の約半数はソフトウエアで解くもの。そしてその結果を投稿するとサーバが採点してくれる。
英文だが本文全てがPDFで提供されている！

というところ。

もう少し試して、いけそうならば、こちらにスイッチする。

こつこつ。

2009年9月10日木曜日

eli の使いこなし [起動済みのLispにEmacsを接続]

まず localhost 上。
Lisp にて

(excl:start-emacs-lisp-interface t 1 7666 "~/.eli-startup")

を評価。すると~/.eli-startup というファイルができる。
このファイルの中身は、
```
^A7666 542496 :upper (8 (1) :FINAL 7) 1^A
```
というシンプルなもの。Emacs に渡す接続情報である。
次に、Emacs で、
```
(fi:start-interface-via-file "localhost" "*common-lisp*" "~/.eli-startup")
```
を評価。これでREPLが立ち上がる。メジャーモードは、TCP Common Lisp モード。このモードは、keymap は fi:lisp-listener-mode-map を使っている。
この方法で接続した場合も、fi:common-lisp-mode で開いたソースファイルとの連携ができる。
"localhost"をFQDNまたはIPアドレスに変更すれば、リモートの Lisp に接続できる。ただし起動情報ファイル（ここでは.eli-startup) をEmacsがあるホストで参照できるようにしておくこと。これは、ファイルを転送してもいいし、NFSやsambaで共有してもよい。
この方法で、複数 Lisp に単一 Emacs からREPL接続することができる。ただし、fi:common-lisp-mode で開いた Lisp ソースと連携するのは一番最後に開いた REPL だけ。
listenerを増やすことができるのも、一番最後に開いた REPL の Lisp だけ。
この方法で、2つ以上の Emacs をひとつの Lisp につなぐこともできる。そのときも、

(excl:start-emacs-lisp-interface t 1 7666 "~/.eli-startup")

これは一個でよい。
さて、

(excl:start-emacs-lisp-interface t 1 7666 "~/.eli-startup-1")
(excl:start-emacs-lisp-interface t 1 7667 "~/.eli-startup-2")

として、それぞれに別の Emacs をつなぐこともできる。ただし、

(excl:start-emacs-lisp-interface t 1 7666 "~/.eli-startup")

これひとつに2つの Emacs をつなぐのと、機能上の違いはない。:processes 的には、Editor Server が2つできるので違いはある。
こうしてみると、かなり自由自在というか柔軟なんだな。

時間ができたときに、整理して逆引きCommon Lisp に書こう。
こつこつ。

2009年9月7日月曜日

eli の使いこなし [fi:common-lisp によるリモートLispの起動]

これ、M-x fi:common-lisp の引数指定でホストを指定してあげればよいだけなのですが、うまく起動できない。
ソースを調べてみると、どうやら ssh ではなく rsh 専用になっているようだ。
eli のためだけに、ssh とは別に rsh を運用するというのはちょっと避けたい。
リモート Lisp は fi:start-interface-via-file に一元化かな。

こつこつ。

eli の使いこなし [複数listener]

fi:common-lisp で REPL を起動済みなことが前提。
M-x fi:open-lisp-listener で対話的に新しい listener を起動できる。このときバッファ名は、*lisp-listener* になる。
M-x fi:open-lisp-listener を使ってさらに listener を起動するのはやめたほうがよい。この方法の場合、事前に作成した listener のバッファ名を *lisp-listener* 以外に変更しておいて、M-x fi:open-lisp-listener を実施することになるが、このバッファ名の変更が、Common Lisp に伝わらないからだ。
2つ以上新規に listener を起動する場合は、対話的ではなく、

(fi:open-lisp-listener -1 "*my-lisp-listener*")

などを評価する方がよい。-1 は buffer-number という引数だが、Gnu Emacs 22 の Info では記述されていない。負数を設定すると自動的に空き番号を使うとのことなので、負数運用がいいのかもしれない。
fi:open-lisp-listener で起動した REPL はfi:inferior-common-lisp-mode ではなく、fi:lisp-listener-mode である。
さて、listener はプロセスとどういう関係があるのかというと、まず listener を増やしても、OS上の alisp のプロセスは増えない。Common Lisp 内のスレッドが増える。
listener を終了するときは、:kill で Common Lisp の内部スレッドを停止する。
どの listener においても、:exit すると、全ての listener というか Lisp 本体が停止してしまう。

時間があるときに、整理しながら逆引きCommon Lispに書こう。
こつこつ。

【MoL】28 Substitution Extended

ちょっと間があいてしまった。いかんなぁ。

monadic quantificational schemata から sentences を作るということは、substitution of abstracts によってスムースに取扱うことができた。
- なんだったっけ?
- monadic quantificational schemata から sentences をつくる方法を決める。
- 'Fx'について決めれば、あとは truth-functional でいけるだろう。
- 'Fx'を再度、'F'と'x'に分解して考える。{w: Fw}x <-> Fx であった。
- 'F' は常にa term abstract として書ける。
- 'x' は a free variable であり、'a' などのan object と同等である。
- というわけで、monadic quantificational schemata から sentences をつくるには、term abstracts の部分に open sentences を入れればよい、ということになった。
polyadic schemata ではどうか。また'Fxy'、'Fyx' と 'Fxx' というのはどういう関係にあるのか。
さて、まず sentences となった状態を考える。
∃x(y amuses x more than y amuses y)
∨ ∃x(x amuses y more than y amuses x)
.-> ∃x(x amuses x more than y amuses x).
これが、
∃xFxy ∨ ∃xFyx .-> ∃xFxx.
に対して何らかの substitutions を実施した結果として得られるようにしたい。
polyadic な abstracts を導入する。
ここでいえば、

F : {zw: w amuses z more than y amuses w}.

である。
さて、monadic の場合は、term abstracts というのは英語の関係節の拡張というか抽象であった。
では、polyadic の場合は、何なのか。これも英語の関係節の拡張というか抽象である。ただし英語の中に、よく相当するものは存在しない。
その理由のひとつに、英語での関係節というのは、ほとんどの場合が、関係節単体で使われるのではなく、限量子と関係節の組み合わせとして使われるということがある。
ひとたび、限量子と組み合わせられると、polyadic の term abstracts は monadic の term abstracts で表現できてしまう。
例：
∃{xy: x saved y from drowning}.
∃{x: ∃{y: x saved y from drowning}.
という訳で、polyadic relative clauses というのは、自然言語にはあらわれない a godsend だ！　長い道程、論理と言語を精査してきた結果、自然言語を超えて得られたものだ。

こつこつ。

逆引きCommon Lisp

Common Lisp に関わる基本的なことは、このブログだけでなく、

逆引きCommon Lisp

にもなるべく書こうと思う。その方が、同じ事をするにしても、よっぽど誰かの何かに役立つかもしれない。

とりあえず、eli についてちょこっと書いてみた。

こつこつ。

2009年9月5日土曜日

Emacsでlispファイルを開くときのこと (2)

Franz の fi:common-lisp-mode (eli)ではどうなんだろ、ということで、多少追ってみる。
まず、マニュアルによると、


;; -*- mode: fi:common-lisp-mode; package: mypack; readtable: myrt -*-
(in-package :mypack)
(eval-when (compile 
            load
            eval)
  (setq *readtable* (named-readtable :myrt)))

というのがフルな使い方のようだ。

mode: は eli に関わらない標準的なこと。これ以降は eli 独自だ。

mode specification で package と readtable を指定するということは、これらをEmacsに教えてあげるということだ。これらをEmacsが知っていることによって、eli を通じてEmacsとCommon Lispのやりとりが成り立つということ。

ただし、packageについてはソースを読み込み時にパースして(in-package ...)があれば、それも見てくれる。

ちなみに、Franzのマニュアルでは、'mode line'を'display mode line'、'mode specification' を 'file mode line' と読んで区別している。どうやら以前は両方とも'mode line' と呼ばれていてname conflicts があったようだ。

packageの指定が、file mode line にもなく、(in-package ...)としてもない場合は、

fi:default-package
fi:package

が参照され、readtableの指定がない場合は、

fi:readtable

が参照される。

こつこつ。

Emacsでlispファイルを開くときのこと

EmacsでLispファイルを開くときに妙な確認がでる。それを調べてみる。

まず、出るものはこれ。


The local variables list in paip-study.lisp
contains values that may not be safe (*).

Do you want to apply it?  You can type
y  -- to apply the local variables list.
n  -- to ignore the local variables list.
!  -- to apply the local variables list, and
permanently mark these
      values (*) as safe (in the future, they will
      be set automatically.)

  * Syntax : Common-Lisp

これは該当Lispファイルの一行目に、


-*- Mode: Lisp; Syntax: Common-Lisp -*-

を書いているからだろう。この行のことを「mode line」と言うのかと思っていたら、正確には「mode specification」なんですね。「mode line」はmini bufferの上にあるやつのこと。Redshankもこれをmode lineと読んでいるから、結構用語が混乱しているのかも。

mode specification を info で調べて整理しよう。形式は、


-*- mode: MODENAME; VAR: VALUE; ... -*-

であり、VAR VALUEの組は、File Variablesと呼ぶものだ。これはこのファイルが読み込まれる際に自動的に解釈されてそのbufferのローカル変数となる。

さて、info の Emacs に 57.3.4.2 Safety of File Variables としてまさに疑問に答える節があった。これによると、

Emacsは、variable/value pairs について、safe なもの risky なもの、というようにグループ分けしている。
それによって、上記の確認画面が出たり出なかったりと制御している。
その制御は、enable-local-variables enable-local-eval と safe-local-eval-forms によってカスタマイズできる。

というわけで、内容を確認した上で、"y"を入力すればいいだけですね。

こつこつ。

2009年9月2日水曜日

【MoL】27 Schemata Extended (3)

'∀x∃yFxy' と '∃y∀xFxy' の違い。
'Fxy' を 'x and y are the same thing' であるとする。

すると、

7: '∀x∃y(x and y are the same thing)'
8: '∃y∀x(x and y are the same thing)'

となる。

7について考える。何を an object x として選んでも、そのx自身についてはFはなりたつので、7は真である。
8について考える。an universe が an object x ひとつしか含まないとする。すると、8は真である。しかし、objects が二つ以上ある場合は、「他の全てと同じとなるan objectが存在する」というのは偽である。
さて、この章で導入したものはmonadicに限らない the quantificational schemata である。'p', 'q', 'Fx', 'Fy', 'Gx', 'Hxy', 'Hxx', 'Fxyz' などなど。
これによって、schemataの表現力があがることをここまでみてきた。
schemata が拡張された以外は、interpretation であったり、validityであったりの定義は以前と同じ。
しかし、34章でやることだが、validityやconsistencyを判断するための a decision procedure となる機構は構築不可能なのである。
a decision procedure for validity が無いことは、procedures for proving validity の存在を否定するものではない。これはありえる。それを構築するのがPart III の主題。

こつこつ。

【MoL】27 Schemata Extended (2)

推論(inference)について考える。
All circles are figures; ∴ All who draw circles draw figures.
この推論を monadic schemata に変換してみる。
'F'を「円である」、'G'を「図形である」とすると、前提(the premise)は、

∀x(Fx -> Gx).

となる。
結論(the conclusionは、'H'を'{w: w draws a circle}'として、'J'を'{w: w draws a figure}'とすると、

∀x(Hx -> Jx).

となる。これ、一応それぞれを表現はしているけど、この前提の表現から結論は、推論によっては導かれない。
そこで、dyadic schemata。
'F'と'G'は上のままとし、'Hyx'を'y draws x'とすると、結論は、

∀y[∃x(Fx . Hyx) -> ∃x(Gx . Hyx)].

と表現できる。これ、ちょっとしっくりこない。 ∀y∃x[(Fx . Hyx) -> (Gx . Hyx)] の方が合っているような気もする。でもこちらがよろしくないのは、'∀x(Fx -> Gx)'の内容を含んじゃっているから、だろうな。なので、前提、

∀x(Fx -> Gx).

から、上の結論が imply される、という全体構成になるのが正しいと。
次の例。
Premise : There is a painting that all critics admire;
Conclusion : Every critic admires some painting or other.

これをdyadic schemata で表す。
'Gx' : 'x is a critic'
'Hxy' : 'x admires y'
'Fy' : 'y is a painting'
Premise : '∃y(Fy . ∀x(Gx -> Hxy))'
Conclusion : '∀x[Gx -> ∃y(Fy . Hxy)]'

うーん。dyadic schemata になると自然言語との対応がやたら難しくなる。
次の例。
Premise : There is a philosopher whom all philosophers contradict.
Conclusion : There is a philosopher who contradicts himself.

'Fx' : 'x is a philosopher'
'Gxy' : 'y contradicts x'
Premise : '∃y[Fy . ∀x(Fx -> Gxy)]'
Conclusion : '∃x(Fx . Gxx)'

一日あたりちょっとしか進まないのがなんとも。。。
こつこつ。

登録: 投稿 (Atom)

計算機とその周辺: What I Talk About When I Talk About Computers

2009年9月27日日曜日

【LPL】9章限量入門 (2)

【LPL】9章限量入門

【LPL】8章条件文の論理

2009年9月23日水曜日

【LPL】7章条件文 (2)

2009年9月22日火曜日

【LPL】7章条件文

【LPL】6章形式的証明とブール論理

2009年9月20日日曜日

【LPL】5章ブール論理の証明方法

【LPL】4章ブール結合子の論理 (2)

2009年9月19日土曜日

【LPL】4章ブール結合子の論理

【LPL】3章ブール結合子

2009年9月15日火曜日

【LPL】2章原子文の論理

2009年9月13日日曜日

【MoL】別の本にスイッチを検討

2009年9月10日木曜日

eli の使いこなし [起動済みのLispにEmacsを接続]

2009年9月7日月曜日

eli の使いこなし [fi:common-lisp によるリモートLispの起動]

eli の使いこなし [複数listener]

【MoL】28 Substitution Extended

逆引きCommon Lisp

2009年9月5日土曜日

Emacsでlispファイルを開くときのこと (2)

Emacsでlispファイルを開くときのこと

2009年9月2日水曜日

【MoL】27 Schemata Extended (3)

【MoL】27 Schemata Extended (2)

ラベル

自己紹介

ブログアーカイブ

2009年9月27日日曜日

2009年9月23日水曜日

2009年9月22日火曜日

2009年9月20日日曜日

2009年9月19日土曜日

2009年9月15日火曜日

2009年9月13日日曜日

2009年9月10日木曜日

2009年9月7日月曜日

2009年9月5日土曜日

2009年9月2日水曜日

ラベル

自己紹介

ブログ アーカイブ

ブログアーカイブ