【シプサ】6 計算可能性の理論における先進的な話題 (その2)

上半期末に向けて、業務が膨大に、、、
されど、こつこつ。
「6.2 Decidability of logical theories」から。

• ある数学的言明(statement)が真かどうかを判定するアルゴリズムがあるかどうか、ということは、もちろんその言明が属している数学のドメインによる。判定するアルゴリズムがあるドメインもあるし、それが存在しないドメインもある。
  
• このことをTMで扱うために、言語をつくる。
  
• その言語に含まれる要素は、真である(ある特定された対象ドメインに属する)数学的言明の表現である。
  
• 数学的言明というオブジェクトの表現方法を決める。文字列で表現するルールをきっちり定める、ということ。
  
• ここで定めているのは、一階述語論理っぽい。
  
  
• R(x1, ..., xj)のかたちのもの = atomic formula
  
• 構成ルールにしたがって、atomic formulaからつくったもの = well-formed formula (単にformulaと言うときはこれ)
  
• formulaで、コンティフィアが冒頭にしかないもの = prenex normal form
  
• formulaで、no free variableなもの = sentence or statement
  
  
• さて、これでformulaを整備できた。違う言葉でいうと、数学的言明を表現する方式を確立した。
  
  
• あと、やらねばならぬことが2つ。
  
  
• ひとつは、variableってなんじゃないな、ということ。
  
• それはvariableの値になりうるのはこれこれですよということを明確にする集合があるとする。
  
• その集合をUniverseと呼ぶ。
  
• これを具体的に割当てる必要がある。(これが意味論?)
  
• つぎに、Relationsというのは第一章で確認済みな真偽値を値とする写像なんだが、
  
• この言語におけるRelationsシンボルが、どういう具体的Relationを表現しているのよということの特定。(これが意味論?)
  
  
• で、この具体的に特定された(universe, relation assignments)の組のことを、modelと呼ぶ。
  
• 逆に、あるmodelに対応したstatementの集りのことを、language of a modelと呼ぶ。
  
• ここで「対応した」とは、そのmodelに適合した形(relationシンボルとrelationのarityがポイント)であるということ。
  
• で、ここ、ややこしいというか用語が混乱しているように思うのだが、
  
  
  
  • model Mがあるとする。
    
  • statement Φ が 、Mに対するlanguage of a modelに属しているとする。
    
  • すると、Φは、Mによって、trueとなったりfalseとなったりするでしょう。(ここまではよい。)
    
  • あるMでΦがtrueになったとする。
    
  • そのとき、MはΦの a modelであるという。(ここ、ちょっと混乱している)
    
  
  
• まあ、これが定義なのだからしかたなし。
  
  
• EXAMPLE 6.10 そうか、「∀x∀y(R1(x,y)∨R1(y,x)をモデル(N,<=)で考える」というのが言語とモデルの正式な関係で、これを「∀x∀y(x<=y)∨(y<=x)を考える」といってしまうのはこのモデルを念頭においた略記にすぎないのだな。
  
  
• で、Th(M): theory of M の定義
  
  
  
  • a model たる Mがあるとする。
    
  • すると、Mに対する複数のlanguage of a modelがあるだろう。
    
  • そのなかで、すべてのsentenceがtrueとなるものがあったとする。
    
  • それをtheory of Mと呼ぶ。
    
  
  

TMもずいぶん長くやっているし、「論理学をつくる」で一階述語論理まではかじっているので、すんなり。
とりあえず、ここまで。
次回は、これらについて判定可能性を調べていく。