2008年4月28日月曜日

1 一階述語論理


  • 1.1 シンタックスとセマンティックス

    • 曖昧だが、言語のシンタックスは、意味を忘れて文について議論することらしい。
    • 「言語に属する文は、有限種類の文字からなる有限の文字列によって表現される」
    • 文脈自由文法を知らないので、算術式のくだりがあまりわからない。。。
      とりあえず、BNF記号で定義するものはシンタックスである、ということが言いたいのだろうと、思っておく。
    • 「一般に、言語に属する実際の文字列に表れる記号を終端記号という」
    • 「セマンティックスとは、言語に属する文の意味を議論することをいう」
    • メタ言語と対象言語を区別する。
    • メタ言語が対象言語を語るときに、対象言語の何かを変数かして表現する場合、その変数をメタ変数と呼ぶ。特にシンタックス上の話であるならば、シンタックス変数と呼ぶ。
    • 演繹は、一般的な理論によってお、特殊なものを推論し、説明すること。帰納とは、個々の具体的な事例から一般に通用するような原理・法則などを導き出すこと。
    • 形式論理学をやったことがなく、形式論理がいまいちわからない。字句通りに用語を整理すると、

      • 形式論理には次のものがある。

        • 命題(何を命題とするか=形式論理のシンタックス)
        • 命題の真偽(真偽を決める何らかの方法=形式論理のセマンティックス)
        • 公理と呼ばれる命題
        • 定理というもの。もっとも基本的な定理は公理。
        • 推論規則(定理から定理を導くためのもの)

      • 推論規則の適用によって、公理からある定理を導くことをその定理の証明という。
      • また、定理とは証明できる命題のことである。
      • 「証明可能性は、形式論理のシンタックスに関する概念である」う、わからん。
      • 「命題の正しさ(真偽)は、形式論理のセマンティックスに関する概念である。一般に、命題の真偽を直接に計算することはできない」う、わからん。



  • 1.2 一階述語論理のシンタックス

    • 一階述語論理における項と命題について説明するそうな。演繹体系(公理+推論規則)は後の章だと。
    • 「述語とは、ものの間の関係のことである」これは、言葉のイメージの説明。
    • ものを表す変数を一階の変数、ものの集合やものの関数を表す変数を二階の変数という。
    • 一階述語論理では、一階の変数しか使わない。関数や述語を記号であらわしたとき、それは定数である。
    • 一階述語論理の登場人物?

      • もの
      • ものの間の述語
      • ものからものへの関数
      • ものを表す定数を定数記号という。(略称は定数)
      • 述語を表す定数を述語記号という。(略称は述語)
      • 関数を表す定数を関数記号という。(略称は関数)
      • 変数は、ものを動く変数のみである。
      • 項は次のように定義される。

        • 変数
        • 定数
        • 任意個の項から関数によって得られた出力

      • 一階述語論理では、命題を一階論理式と呼ぶ。
      • 一階論理式の定義。

        • P(t1,...,tn) は『t1,...,tnは述語Pを満たす』という論理式である。
        • Pは『Pという命題定数(引数の数が0の述語)が成り立つ』という論理式である。
        • (¬A)は『Aという論理式が成立しない』という論理式である。
        • (A1∨A2)は『A1という論理式が成立するか、または、A2という論理式が成立する』という論理式である。
        • (∀xA)は『Aという論理式が任意のxに対して成立する』という論理式である。

      • ここで、¬∨∀は、論理式から論理式を作るためのものであり、論理記号と呼ぶ。
      • それぞれの関数や述語のアリティは、固定とする。
      • 一階述語論理を議論するとき、シンタックス変数は、変数、定数、関数、項、述語、論理式について使用する。この中で一階述語論理における変数となるのは変数だけである。
      • シンタックス上の等しさを≡で表す。シンタックス上の等しさは、メタ言語に属する概念である。
      • 「一階言語とは、定数、関数、述語の集りのことである」
      • 変数の全体は、「x0 x1 x2 ...」であり、加算無限個存在する。
      • 一階言語を特定すると、それは対象言語を特定したことになる(?)。
      • 「一階述語論理の一般論に関して議論する場合は、一階言語という概念を導入し、定数、関数、述語を特定せずにオープンにしておく」
      • 「変数、定数、関数、述語はアトミックな記号であり、それ以上分解することができない。」
      • 「これに対して、項や論理式はアトミックな記号から作られるデータ構造である」
      • 項や論理式を文字列で表現していくが、それは構文木の何らかの表現であるとする。構文木をイメージしやすい文字列表現を採用しているだけと考える。
      • 出現は、部分項または部分論理式が構文木のどこにあるかという位置のこと。
      • 出現には、束縛する出現と、束縛される出現がある。∀の後の出現が束縛する出現。
      • ∀x(...)の...の中の出現は、∀の直後のxのスコープの中にある、という。
      • 束縛してもいないし、束縛されてもいない変数の出現を自由な出現という。
      • 「論理式Aの中に変数xの自由な出現があるとき、xをAの自由変数という。束縛する出現を持つ変数を束縛変数という」
      • 「自由変数を持たない論理式を閉じた論理式という」
      • 「閉じた論理式を文という」
      • 「変数を含まない項を閉じた項という」
      • 「閉じた論理式の意味は真か偽に確定する」
      • 「∀xAを∀yBに書き換えることを束縛変数の名前換えという」
      • 束縛変数の名前換えを有限回適用することによって、論理式Aを論理式Bに書き換えられるとき、互いにα同値であるという。≡α で表す。
      • ≡αは、反射的かつ対照的かつ推移的なので、同値関係である。
      • A ≡α B をみたす論理式Bの全体のことをAのα同値類と呼ぶ。
      • …A…が論理式Aに関する概念であるとき、A ≡α A' かつ…A…ならば…A'…が成り立つならば、α同値な論理式を同一視してよい。
      • 代入の記法。A[t/x]。ここで、tは項であり論理式Aに現れる変数を含まないもの。これによってAに現れる変数xの自由な出現を全てtで置き換える。
      • A ≡α B ならば A[t/x] ≡α B[t/x] が成り立つ。
      • 論理記号には、省略形と呼ばれるものがある。∧⊃⇔∃であり、これらは論理記号¬∨∀を用いて定義できる。


  • 1.3 一階述語論理のセマンティックス

    • 「一階述語論理に対して、項と論理式の解釈を与えるための数学的な構造をストラクチャーという」
    • 「一つのストラクチャーは、領域と呼ばれる空でない集合と、各種記号の解釈から成り立っている」
    • 記号の解釈はその記号を[[と]]で囲んで記す。
    • 各定数cについて[[c]] ∈ U。
    • 各関数記号fについて[[f]] : U^n → U
    • 各述語Pについて[[P]]⊂U^n
    • n = 0のとき、U^0とφのみ。TをU^0、⊥をφと定義する。それぞれ真と偽。
    • ここまでは一階述語論理汎用かな。
    • ストラクチャーを決めるには、

      • Uの数学的対象を決める。例,N。
      • 定数記号の解釈を前項のUの数学的対象から選ぶ。例,[[0]] = 0 ∈ N。
      • 関数記号の解釈を決める。例, [[+]](u,v) = u + v ∈ N。
      • 述語記号の解釈を決める。例,[[<]] = {〈u,v〉| u < v, u,v∈N } ⊂ N x N
      • これらにおいて、左辺が対象言語であり、右辺がメタ言語。
      • とりあえず、ここまで。

  • 0 件のコメント: