"truth values and proof theory" (Greg Restall) - あいまいな本日の私 blog

Studia Logicaに掲載予定、著者のweb siteから取得可能。
推論主義の立場から「真理値とは何か」を説明しています。要約すると以下の通りです。

"Mutiple conclusion"論文に倣って、ある文の「否定を主張 (negate)」することと、それを「却下する (reject)」ことは概念として違う、という主張からスタートする。そして、[ A, B : D, E] を、「A, B の全てを主張し、D, E の全てを却下する」と読む。また、のとき、Aを主張しておきながら DとEを否定したら整合的でないので、そういうケースを除外し、整合的な文の集合のペア（"position"と呼ぶ*1）を考える。
- positonを拡大する際には、整合性の要請から、例えば [ A∧B : A, C] は [ A∧B : C] の拡大とはなりえないとか、[ A∧B : C] を含む limit position は必ず [ A∧B, A B: C]を含むとかいう（おなじみの）性質が導かれる。
- さて、任意の有限のpositionは、整合性を保持したまま、いくらでも文を付加して新しいpositionにすることが出来る（が、もちろん上限はある）。従って、Zornの補題により、極大集合を（ペアで）取ることが可能（それを"limit position"と呼ぶ）。
後はルーチンで position の拡大をしていくと…
- 古典論理において、limit positionは通常のタルスキ・モデルと同じもの（limit positionの左側にある文は「真なる文」、右側にある文が「偽なる文」）となる。また、結果的に真理関数的になる。
- 直観主義論理の場合、limit positionは作り方によって beth semantics になるか、Kripke frameになる。
  - Gentzen流のLJ（ $\vdash$ の右側には論理式は一個しか存在できない）に基づき、positionの右側の解釈を変更し、[A,B : C, D]を「 $A, B\neg\vdash C$ かつ $A, B\neg\vdash D$ 」とすれば、最終的には Beth Semantics が構成される
  - LJではなく、 $\vdash$ の右側に複数の式を許すけれど、⇒の導入などは右に一つの論理式があるときのみ許す列計算のバージョンに基づいて limit position を構成すると、通常の Kripke frame となる。
- S5の場合、Hypersequentによる定式化から出発すれば、通常のKripke semanticsになる。
この意味で、証明論は（集合論の助けを借りることで）伝統的な「真理値」を構成することが出来、その意味で「真理値」概念は、基礎的なものではなく「証明論的構造の理想化(idealization)」だと考えることが出来る。
- 論文のアイディア自体は、古くから言われること*2を使用している（その意味で新しいことは何もない）。
- ポイントは、この論文では古典論理や直観主義論理など多くの論理について、統一的に、そして推論主義の立場からもっとも基礎的な概念である「論理的帰結関係」をベースに真理値について語ることが出来る点である。