logicI - 41semicolon/41semicolon.github.io GitHub Wiki

照井氏のテキストをベースに。

オブジェクトレベルの取り決め

  • 再帰的に 項・式を定義する。逆に 項・式は一意に分解可能であるようにする。
  • 論理記号は以下を採用: ⊥,⋀,⋁,→,∀,∃ (⊤は⊥→⊥,¬ψはψ→⊥という明示的定義で導入)
  • 追加記号は以下を採用: 定数として 0, 関数として S, +,・, 述語として=。
  • 0にSをn回演算してできる項の略記としてnを導入。同様に 1,2,3,... も導入される。

メタレベルの取り決め

  • 推件/シーケントには⇒をあてる。Γ⇒φのように使われるので Power(F)×F な順序対である。
  • 証明/導出/帰結 には ⊢ をあてる。T⊢φのように使われるので Power(F)×F な関係である。
  • ⊢の F×F への制限に対しても同じ記号 ⊢ をあてることで、F上の二項関係としても使う。

証明系 NJ の取り決めとメタ定理

  • 自然演繹NJ:(init),(⊥)に加え、論理記号ごとに導入・除去規則を加えた 全12個の推論規則
  • (F上に制限された方の)⊢は合同関係になるので 同値関係 ～を定める。
  • つまり ⊢ は F/～ における半順序になる。⋀は上限, ⋁は下限の構造を取るので
  • (F/～,⊢,⋀,⋁)は束という構造を持ち、 ⊥・⊤がそれぞれ最小元・最大元になる。

NJの証明能力

NJは（古典論理で使う証明系である）NKから背理法の推論規則を除去したものとみなせるので 証明能力は劣る。NKで証明できるがNJで証明できないものとして以下が挙げられる:

  • φ⋁¬φ: 排中律, (lem)
  • ¬¬φ→φ: 二重否定除去, (neg)
  • ドモルガンの法則の一
  • (ψ→φ)⋁(φ→ψ): 前線形性
  • ∃x(φ(x)→∀yφ(y)): 酒場の法則

証明図の代数

ある証明図が与えられたとき、その部分に対して（例えば）導入規則と除去規則が連続するようなパターンが存在する場合、ランクの小さい証明図が得られる。このような証明図の変形を簡約といい、他にも幾つかの簡約規則が得られる（置換簡約規則）。どんな場合でも簡約が有限回で停止することが知られており（弱正則化定理・強正則化定理）、したがって証明図における正規形という概念に至る。そこからの重要な帰結として次が挙げられる:

  • 選言特性: ⊢φ1⋁φ2 ⇒ ⊢φ1 または ⊢φ2
  • 存在特性: ⊢∃xφ(x) ⇒ ある項t について φ(t)
  • 部分論理式性: ⊢φ ⇒ φの部分論理式しか含まないような証明図が存在する

LKと証明探索

話は一旦古典に。完全な証明系としてLKがある。その特徴:

  • (⋀L)と(⋁R)が双対. (⋀R)と(⋁L)が双対. (∀L)と(∃R)が双対. (∀R)と(∃L)は双対.
  • (cut) 以外は、上の推件に現れる論理式は全て下の推件に現れる論理式の部分論理式
    • 証明探索=下の推件から上の推件を探す手続きにおいて、(cut)は扱いずらい
  • (cut) は不要、つまり証明があれば(cut)を使わない証明図がある(基本定理)。
    • よって証明探索の機械的な手続きが得られる

NJと同等の証明能力にする方法:

  • LJ: 推件の右側を高々1に制限する
  • LJ': (→R)と(∀R)に制限する

どちらの場合もカット除去は成立。

古典論理(CL)と直観主義論理(IL)

CLがILに埋め込める: ILはCLより証明能力が劣る。しかし ILの証明能力は想定される以上に強力。否定論理式(⊥と基本述語の否定から構成される論理式)を定義すると、任意の式φには(CLにおいて)同値な ある否定論理式φNが存在することを示せる。このように任意の式・文・理論は、否定論理式のみで記述でき、これを否定翻訳(Nと記載)と呼ぶ。すると以下の定理が成立する: T ⊢CL φ ⇔ TN ⊢IL φN。 TN は T の部分集合であり φ と φN は(CLにおいて)同値であるので「φN(≡ φ)を証明するのに ILはCLよりも弱い理論でよい」という一種逆説的な言明が得られる。

ペアノの公理の下でのCLとILの違い: ペアノ算術において、古典(PAと呼ぶ)と直観(HAと呼ぶ)はどこまで証明能力の違い:

  • PAの定理 全てが HAの定理 とは限らない
  • しかし PA の定理の中で ∀∃式 の式 は全て HA の定理でもある
  • また PA の定理の中で パイ0-2言明 は全て HA の定理でもある

証明＝プログラムという主張

NJを(ペアノの公理を証明できるように)拡張した NHA という証明系を作る。NHA においても弱正規化定理と選言特性・存在特性が成立する。なので パイ0-2言明 ∀x∃yφ(x,y)が PA の定理であるならば、証明図を NHA で作ることができる。任意に与えられた n に対して ⊢HA φ(n,m) となる m は、証明図の機械的な書き換えにより求めることができる。この考察は、証明とプログラムを同一視できることを示す。

証明論

「証明」＝「公理＋推論規則による形式的な式の導出」という枠組みがあるので古典論理と直観論理であまり違わない（意味論との比較という意味で）。推論規則の違い

  • 推論規則 OUT: ￢￢A から A を導出してよい（二重否定除去）
  • 推論規則 IN: D∧￢D からは任意の A を導出してよい（否定除去）

これに伴い、推論規則から導かれる派生規則である背理法にも影響：

  • 派生規則 OK: 「Aを仮定して矛盾」から ￢A を導出してよい
  • 派生規則 NG: 「￢Aを仮定して矛盾」から A を導出してよい

推論規則が違うので当然定理も違う:

  • 定理でない
    • A∨￢A : 排中律
    • ￢￢A → A : 二重否定除去
    • ￢(A∧B)→(￢A∨B) : ドモルガンの法則の4つのうちの1つ
  • 定理
    • A→￢￢A : 二重否定導入

意味論

いくつかの意味論があるが、以降、クリプキモデルに基づく。

真であるという概念: ある命題 Pがあった時に「Pが真である」という概念はもはや持ちえない。真偽という言葉を辞書から抹消し、代わりに「Pが証明可能である」と言い換えたほうが直観論理ではスッキリする。もちろん「証明可能である」という文字列自体に意味はない。それは、古典論理において「真である」という文字列に意味がなく「1 である」「T である」などと表現してもよいのと同じ意味だ。日常言語やメタ論理における「証明可能」という単語から想起されるイメージが、直観理論における命題 P に対する判断を表すのに適当な単語であるために、この単語を選択するとスッキリすると言っている。じゃあ、わざわざ変えずに「P は真である」という言葉を古典論理と別の意味で使えば？と思うかもしれないが、「真」という単語には真か偽かといった二元論的な響きがあるので直観論理と相性が悪い。

論理記号の意味論: （野矢氏が『論理学』でいう）認識史という概念をかぶせた意味論を念頭に以下を記述。論理記号はそれ単独では意味をなさない。古典論理では真理関数としてそれらを解釈した。同様に、直観論理においても各地点における原子命題の証明可能性から、（その地点における、もしくはそれ以降の地点における）分子命題の可能性を与える関数として論理記号を定義する。特に￢の意味論に注意。

妥当式の定義と認識史分析: トートロジーがその（真理値分析による）恒真性で定義されたように、直観論理における論理的真理である妥当式を、上記の意味論を使って定義する。ある式 A が妥当式であるかを分析するために、認識史分析と呼ばれるタブローのような方法論がある。

a