命題論理をやることにする。

やはり、この本を読むには命題論理までの素朴な部分を済ませておく必要があると思う。
悩んだが、そこをしっかりやるところまで一旦撤退することにする。
ほんとは、途中で別の本にいくのはよくないんだけど、今回はやってみる。

いくつか吟味した結果、戸田山和久さんの「論理学をつくる」をやることにした。

「論理学をつくる」を読む

2 一階述語論理の演繹体系 (続き2)

理解する、ということはどういうことだっけ? という感覚がすこしずつ戻ってきた。
最終的には正しく使える、ということだ。Duck typing。
それには、慣れと、筋のよい概念構築、抽象と具象の自由な往来、が必要。

今回は慣れを得るために問をやる。

ひとつめ。
帰納法が必要かな、と思ったが、いらんかった。

ふたつめ。
¬右：論理式の変形。
¬左：論理式の変形。
∧右：真偽表。これの論理式の変形がおもいつかず。
∧左：シーケントの定義まんま。
∨右：シーケントの定義まんま。
∨左：既出の規則から導出。
⊃右：既出の規則から導出。
⊃左：既出の規則から導出。

みっつめ。
読んでみた。なるほど。そう読んで違和感はない。

よっつめ。
問題なし。

いつつめ。
シーケント計算って、なんというか、四則演算を簡易にやるための筆算式のようなものなんですね。
それがなくても同等のことは可能。だけどそれがあると簡易にできる。
そして、そのやり方自身がそれなりのルールをもっている。

むっつめ。
ここ、概念的にひっかかるところがどうも気になってしまう。
演繹体系が完全であることの意味の説明がどうもわからない。
「正し論理式はすべて定理として証明可能」というが、論理式の正しさはセマンティクスに属しているんじゃなかったっけ?
命題論理のストラクチャーがでてくるけど、これがわからない。命題論理を理解していることが本書の予備知識として求められてはいるのだが。。。
命題論理をきっちりやった方がいいんだろうな。それは別途やろう。
今は、慣れることに重点をおく。
駄目だ。飛ばす。

ななつめ。
飛ばす。。。

やっつめ。
((P∧Q)∨(P∧R))⊃(P∧(Q∨R))：証明できた。
¬(P∧Q)⊃(¬P∨¬Q)：証明できた。
(¬P∨¬Q)⊃¬(P∧Q)：証明できた。
(¬P∨Q)⊃(P⊃Q)：証明できた。
(P⊃Q)⊃(¬P∨Q)：証明できた。
P⊃¬¬P：証明できた。
¬¬P⊃P：証明できた。
((P⊃Q)⊃P)⊃P：証明できた。
((P1∧P2)∨(Q1∧Q2))⊃((P1∨Q1)∧(P2∨Q2))：証明できた。

ここのつめ。
やった。

とお。
Qが真でPが偽。
P1,Q1を真、P2を偽。

これで、命題論理のシーケント計算に少し慣れた。
今日はここまで。

2 一階述語論理の演繹体系 (続き)

再チャレンジ。
スタート時点から、かなり仕事で疲れきった状態。。。

全体の流れ。

シーケント定義
命題論理のシーケント計算
　推論規則
　完全性
　ワングのアルゴリズム
一階述語論理のシーケント計算
　推論規則

これ以降は次章。次章ではエルブランの定理と完全性。

少し読んでみて、手を動かしてみて、アタリは掴めてくる。
だけど、やっぱり自分が何をやっているのかが不明瞭になってくる。

そこで、いったんやろうとしていることの整理。
用語の確認から。

演繹体系とは？
公理と推論規則の組。

推論規則とは？
いくつかの命題を前提として、新たな命題を結論として導くための規則。

シーケント
論理式の簡略表記法のひとつ。
A1,…,Am→B1,…,Bn
は、
∀x1…∀xk(A1∧…∧Am⊃B1∨…∨Bn)
の略記。

恒真シーケント
Γ→Δが恒真ということは、どのようなストラクチャーをもってきても
Γの中のどれかが偽になるか、Δの中のどれかが真になる。
A1∧…∧Am⊃B1∨…∨Bn
が恒真論理式であるということ。

命題論理のシーケント計算
まず、シーケント計算とは、シーケントからシーケントへの一連の変形についてまとめて、それぞれに名前を付けたものである。
一連の変形というのは、複数のシーケントからあるシーケントに変形するときに、前者が恒真シーケントであれば、後者も恒真シーケントであるようなものである。

その記法は、
前提1 … 前提n
------------(変形の名前)
結論
とする。

命題論理の場合、次のものがある。
並べ替え
¬右
¬左
∧右
∧左
∨右
∨左
⊃右
⊃左

おどろいたのは、これらの変形をシーケント計算の記法で書くと、そこそこ綺麗に書けることである。

具体的な推論規則
これがわからない。。。
シーケント計算の推論規則は、命題論理全般に当てはまるものだと思う。恒真だから。
だったら具体的もへったくれもないような。
恒真ということは、もってくるストラクチャーによらない、ということ。いや、今、命題論理だからストラクチャーはいらんか。そうじゃなくて、命題AiやBjの真偽によらず成りたつということ。いや、それは違う。P∨¬Pというのはそうなのだが、シーケントが恒真(またはトートロジー)というのは、また違うことではないか。
具体的な推論規則、については先送りとする。

イニシャル・シーケント
シーケントの両辺に同じ論理式があるとき、それをイニシャル・シーケントと呼ぶ。
イニシャル・シーケントは恒真シーケントである。

証明可能
イニシャル・シーケントに対して推論規則(シーケント計算)を有限回適用して得られるシーケントを証明可能であるという。

証明(証明図もしくは証明木)
シーケント計算を段積みにして、その一番上のシーケントが全てイニシャル・シーケントのものを証明と呼ぶ。

定理
論理式Aについて、→Aというシーケントが証明可能であるとき、論理式Aが証明可能である、という。
証明可能な論理式を定理と呼び、
├A
と表記する。

命題論理のシーケント計算の完全性
ある演繹体系によって、命題論理のなかの任意の恒真論理式が証明可能であるとき、その演繹体系を完全であるという。
命題論理のシーケント計算は、完全である。

恒真かどうかの判定
シーケントまたは論理式が与えられたとき、シーケント計算をつかって、それらが恒真であるかないかを判定(決定)することができる。
そのときに使うアルゴリズムを、ワングのアルゴリズムという。

シーケントを偽にするストラクチャー
命題論理のストラクチャーって定義されていたっけ。。。
字句通りに理解すると、ワングのアルゴリズムである論理式が恒真でないことが判定できたとすると、ワングのアルゴリズムで作成した証明木の葉にイニシャル・シーケンスでないものが含まれており、そのシーケンスを実現するストラクチャーがそれである。


以上で、流れは掴めたような気がする。
詳細を追う&疑問点を確認するのは次回としよう。。。

2 一階述語論理の演繹体系

う、命題論理を復習しなくて理解できるかという不安があるがとりあえず進む。

2時間で玉砕。
鵜呑みにして覚えていくことはできそうなんだけど、
自分が何をやっているのかが不明瞭。。。

ここで一度、立ち止まって、何をやっているかを考えてみる。書籍を見ずに自分の言葉で構築してみる。
うまくいくかなぁ。

• 一階述語論理を理解しようとしている。
  
• 一階述語論理は形式論理である。
  
• 形式論理は、論理を記述するために新しい言語を作る方式。
  
• 形式論理を学ぶとは、第一にその言語自体の性質を学ぶこと、第二にその言語を利用して論理が関わる問題の解決ができること。
  
• 論理って何? 一般的には、「考えや議論などを進めていく筋道。思考や論証の組み立て」
  
• 言語って何? 一般的には、「音声や文字によって、人の意志•思想•感情などの情報を表現•伝達する、または受け入れ、理解するための約束•規則。また、その記号の体系。」
  
• ここで「伝達・受入・理解」なので、新しい言語を作るということは、その言語のための文法を立案して、(その文法に対応した)辞書を立案する必要がある。おおざっぱに言うと、前者がシンタックス、後者がセマンティックス。またセマンティックスは、既存の言語が存在する場合は、その言語を使用することが多い(英和辞典とか)。
  
• さて、論理は一般的には上のようなものであり、そのとき、論じる対象と論理は分離して捉えているようだ。
  
• この論じる対象から分離した論理の言語化をするんだろうな。
  
• 一方、論じる対象も何らかの言語で表現されている。これを対象言語と呼ぶ。
  
• 対象言語は無数にある。自然言語はたくさんあるし、数学を言語とすれば、数学の記法や概念は様々な分野があるから、それぞれ言語を成していると考えられる。
  
• 新しく作ろうとしている言語を、ここで、形式論理言語と呼ぶことにする。
  
• 形式論理言語は、あらゆる対象言語に適用可能な単一のものを作れるかもしれないし、そうでないかもしれない。
  
• まずやってみたのが命題論理言語。
  
• 命題論理言語のシンタックスでは、命題変数、命題に作用する演算子や命題から命題を構成する構成方法を定義している。
  
• 命題論理言語のセマンティックスは、個々の命題から真偽値の割り当て関数である。これがセマンティックスということは、ユークリッド幾何学と非ユークリッド幾何学を比べてみるとわかる。
  
• 命題論理言語では語り切れない論理っていうのがあって(あると思われ)、別の言語を作ってみた。
  
• それが一階述語論理言語。
  
• 一階述語論理言語で特筆すべきは自由変数の存在だろう。
  
• さて、一階述語論理言語のシンタックスでは、まず記号として、定数(ものの名前)、関数、述語、を定義する。もちろん曖昧ながらそれらの概念も導入する。次にこれらに作用する演算子をいくつか定義する。続いて変数(定数限定)を定義する。これらを使って項を定義する。その際、その構成方法を帰納的に示すことで定義とする。命題(論理式)の定義も帰納的に示す。だいたいこんな感じ。
  
• 一階述語論理言語のセマンティックスはフレームワーク方式をとっているように見える。
  
• セマンティックスを定めるための基本的な枠組みと、その枠組みにしたがった具体的な(辞書の)構成である。
  
• そこで、まずフレームワークについて。
  
• 領域という概念を導入する。領域は、定数(ものの名前)の集合である。このような概念としての領域をここではUと記す。
  
• 次に解釈という概念を導入する。これは辞書にしたがって変換するというか、辞書のエントリと思っておく。
  
• すると領域の定義を逆に言うと、定数記号の解釈は領域の元となる、と言える。
  
• 続いて述語記号の解釈を定義する。述語記号の解釈は、その述語を満たす(関係を満たす)ものの組を集めたものである。すなわちn個のものの関係(述語)であれば、それはU^nの部分集合である。
  
• 関数記号の解釈は、U^n→Uの関数であるとする。
  
• 項の解釈は、まず、一般的な状況として項がn個の自由変数を含むときに、U^n→Uの関数であるとする。
  
• もう一段具体的に、項自体の帰納的な定義に呼応しつつ、項の解釈の帰納的な定義を示す。
  
• 続いて、命題の解釈を定義する。命題自体の帰納的な定義に呼応しつつ、命題の解釈の帰納的な定義を示す。
  
• 一階述語論理言語のフレームワークはこんな感じ。
  
• すると、このフレームワークを使用してセマンティックスを決めるには次のものを決めればよい。
  
• 領域たる集合、関数記号の解釈たる関数、述語記号の解釈たる部分集合。
  
• これらの組をストラクチャーという。
  
• ストラクチャーが指定されると、一階述語論理言語が定まり、その言葉をフルに使えるようになる。
  
• その言葉を使って何をするのか、というの次章で述べるようにアルゴリズムにしたがって命題を証明したりするのである。
  
• ただし、ストラクチャーを決めなくても、その前のフレームワークまでの段階において、一階述語論理言語共通の性質などもある。
  
• 一階述語論理としては、そのような共通部分の探求が中心な気がする。
  
• ある命題の集合Γに対して、あるストラクチャーSがそれらの全てを成立させるならば、SはΓのモデルである、と言うことにする。
  
• ストラクチャーによらず成り立つ命題を恒真論理式と言う。
  
  
• とりあえず、まとめとしてはこんな感じだが、疑問もいろいろある。
  
  
• まず、推論規則という概念はどこにいれるべきなんだろ?
  
• 述語の解釈を部分集合にしているが、これがどのようにうまくいっているか定かではない。
  
• SがΓのモデルであるときに、Sが例えば数学的なものであり、ΓがSの公理であったならば、その数学的なものの定理をすべてSを使った一階述語論理言語で表現できるのかどうか。また、表現できたとして、その数学的なものに表われる定理を全て一階述語論理言語で証明できるのかどうか。
  

疑問点に留意しながら、もう一度一章を読んでみる。
読んでみた。5時間くらいかかったような。
上の理解は、まだゆるい。要修正点をピックアップ

• 一階述語論理言語という造語はメタ言語と合致する。
  
• シンタックスには単語の定義も含まれる。それを一階言語と言う。
  
• 前項と関連するが、辞書の比喩は上のものは完全ではなくて、単語自体はシンタックス行き。
  
• 推論規則は次章。
  
• モデルの話をするときのΓは閉じた式に限られる。
  

とりあえず、このくらいの理解でシーケントに臨んでみる。
今日はここまで。

1 一階述語論理 (続き2)

残りの部分は雰囲気だけつかんでおいて、ある程度進んでから再度考えてみることにした。

「解釈」とか、まだよくわかっていない。
「群を語るとき」ということで群を成す数学的な例がいくつか出てくるんだけど、歴史的にいうと、それら数学的な例から群という概念が抽出されて、数学的構造として構成されたと思います。そうすると、群を語るときに、群論というか群の公理自体を使えばいいのではないかと。で、その考えは数学の中で抽象構造に着目していく、ということと、一階述語論理として、群を語るということの関係がわからない。なので、「解釈」がどういことなのかがわからない。

1 一階述語論理 (続き)

えっと、項の解釈、難しかったです。何とか、前へ進んでいいかな、と思えるぐらいの理解にはなりました。

何が難しかったかというと、やっぱりメタなところです。

項の解釈をあのように帰納的に定義すること自体は鵜呑みを決めこめば覚えるだけなのですが、なんで定数cが項であるときの解釈に関数を経由する必要があるの、とか理解するのに整理が必要でした。

で、項の解釈がそれなりにわかったところで、おっ論理式の解釈は分かるじゃん、と思ったら、わからなかった。。。

難関は、n = 0 の場合。

そもそもU^0が一点集合であり全体集合であるというのがわからなかった。

で、集合論を調べる。
U^nはU×...×Uという直積の略記だと。ふむ。
じゃあ、U^0の定義は?

これ、集合が説明してある書籍をいくつか見たが定義されていない。。。
とりあえず、今日はここまで。

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
    
  • これらにおいて、左辺が対象言語であり、右辺がメタ言語。
    
  • とりあえず、ここまで。