ラベル Language Proof and Logic の投稿を表示しています。 すべての投稿を表示
ラベル Language Proof and Logic の投稿を表示しています。 すべての投稿を表示

2009年11月11日水曜日

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


  • 9.6 複合名詞句の翻訳

    • この節は、自然言語の文をFOLに翻訳する練習。
    • 特に限量表現が絡むもの。
    • 会話の含みと限量についての説明あり。
    • まず、「空疎に真な一般文」について。
    • 例えば、
      ∀y(Tet(y) → Small(y)).
      これは四面体が存在していて、それらが全てSmallならば真である。しかし真になるのはそれだけではない。四面体がまったく存在しない談話領域でも真である。四面体がまったく存在しないという単純な事実によって真となる、ということを空疎に真という。
    • 続いて、「本質的に空疎」について。
    • 例えば、
      ∀y(Tet(y) → Cube(y))
      も談話領域によっては真となる。ただし、これが真となりえるのは、空疎な真のときだけだ。こういう場合を「本質的に空疎」と言う。



さあ、練習問題。7問、トータル70文くらいの翻訳。のんびりいこう。

こつこつ。

2009年11月10日火曜日

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

9.5節の問題を5問やる。あせらないよう自分にいいきかせる。
次回は、9.6節 複合名詞句の翻訳。

こつこつ。

2009年11月9日月曜日

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

FOLの勉強を再開できるぐらいに復活してきた。あせらず刻んでいこう。


  • 9.5 4つのアリストテレス文型

    • 4つのアリストテレス文型はFOLで表現できる。

      • All P's are Q's.
        ∀x(P(x) → Q(x))
      • Some P's are Q's.
        ∃x(P(x) ∧ Q(x))
      • No P's are Q's.
        ∀x(P(x) → ¬Q(x))
      • Some P's are not Q's.
        ∃x(P(x) ∧ ¬Q(x))




10月体調を崩したのは、どうも夏場に論理に根を詰めすぎたのも原因な気がする。で、一カ月休んだのですが、一カ月休むと、論理について以前にやったものをほとんど忘れている自分がいたり。論理の勉強は、他の勉強とくらべて特にむずかしい気がする。。。

ちょっとスタンスを変えて、まずは「ことば」としてのFOLを使いこなすことに重点を置いてみることにする。「言語」としてのFOLの詳細を理解する、というのは、根を詰めないとできないし、根を詰めてやってもすぐに忘れる。。。「ことば」としての使いこなしの方が忘れにくい気がするし、それがあれば言語としての詳細の探求のスタートポイントをいつも持っていることになる気がする。気がするだけかも。

こつこつ。

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論理で、どの推論がドメイン知識かという関係も明確にしてそれをやってくれる。

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

こつこつ。

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

4章完了。

とにかく問題数が多いのでたくさん訓練できる本。それがありがたい。
そして Grade Grinder が採点してくれるので、今のところ問題数に嫌気は感じない。たぶんGGが無ければ、この問題数にはめげていたと思う。

Grade Grinderの採点結果はこんな感じでメールで来る。

Grade report for aka (aka.xxxxx@xxxxx.xxxx)
Submission ID: xx.xxx.xx.xx.xx.xxxxxxxxxxx
Submission received at: Sun Sep 20 07:52:04 GMT 2009
Submission graded at: Sun Sep 20 07:52:09 GMT 2009
Submission graded by: gradegrinder2.uchicago.edu

#### No instructor name was given. The report was sent only to the student.

The following files were submitted:
Sentences 4.40.sen

EXERCISE 4.40

Sentences 4.40 (Student file: "Sentences 4.40.sen")
Your sentences are all correct. Yes!

---------------------------------
The Grade Grinder is powered by a generous grant from SUN Microsystems.

Funding for the Openproof(TM) project comes from Stanford University's
Center for the Study of Language and Information and Indiana University's
Visual Inference Laboratory.

この本なら FOL を習得できるかなぁ。

こつこつ。

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-可能
    • 「論理的に可能」の定義は曖昧にも関わらず、この関係は厳密に成り立つ。


こつこつ。

【LPL】3章 ブール結合子

ちょこちょこ進めていた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で提供されている! 

というところ。

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

こつこつ。