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

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

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

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

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

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

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

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