博士（理学）上野岳史
学位論 文題名Natural Deductions for Substructural Logics（ 部 分 構 造 論 理 の 自 然 演 繹で の 定 式 化）
学 位 論 文内 容 の 要 旨

この論文の目的は、従来シークェント計算で研究が進められていた部分構造論理を自然演
繹で定式化し、3つの構造推論規則の特徴付け定理を証明することである。部分構造論理とは、そのシステムの推論規則の中に構造推論規則を、一部又は全く含まない論理のことである 。ここで 言う構 造推論規則とはG．G
entzenがシークエント計算LK,LJを定めたときに導入された推論規則のことで、weakening規則、contraction規則、exchange規則の三種類ある。この三つのルールはそれぞれ、次のような意味を持っている。weakning規則は、与えられた仮定から結論にいたる証明において、任意の仮定を添加しても同じ結論が証明される、という規則である。contraction
規則は、ある証明の仮定の中に同一のものが複数個ある時はそれをーっにまとめて良い、という規則である。exchange
則は、証明の中の仮定が有る順序で並んでいるとき、隣り合った仮定同士の位置を交換することができる、という規則である。
近年、分配則や交換則など、従来の数学では当たり前と思われてきた法則の使用を制限する研究が重要になってきている。例えば、計算科学や量子力学の基礎における束論研究などである。部分構造論理は、これらの分野の論理的性質を明らかにするのに活用されている。
部分構造論理の研究は、シークェント計算によって定式化されたシステムに対する研究が主であった。これは、もともと構造推論規則というものがシークェント計算の推論規則として導入され、特徴付けられていたからである。従来の自然演繹では、それがG．Gentzenで導入されて以来、構造推論規則が個別の推論規則として明確に取り出されたことはなく、構造推論規則の働きは他の論理記号の推論規則の中に埋もれてしまっていた。構造推論規則が明示されていなかった為、自然演繹での構造推論規則の研究は従来ほとんど行われていなかった。
しかし、自然演繹では、証明全体の構造の中で、仮定相互の関係、及び仮定と結論の間の依存関係が木構造として明示される。その上、自然演繹の各推論規則は、証明全体の構造を変換する操作として定義される。他方、シークェント計算においては、各推論規則は個々のシークェントに対する操作として定義される。また、直観主義論理の自然演繹シス
テ ムN
Jと型 付きラム ダ計算と の間に はC
urry‑Howard
対応 と言う 対応関係が有る。このCurry−Howard
対応によってN
Jは構成的プログラミングや関数型プ口グラミングの基礎など、計算論の研究にも使われている。
部分構造論理の自然演繹による定式化、という我々の結果から、Curry‑Howard対応を部分構造論理と「部分構造化されたラムダ計算」との対応に制限することができる。この新しい対応を研究することにより、計算論のより詳細な考察をすることができるようになろう。
本論文は大きくニつの部分に分かれている。
ー 75―

第一部では、自然演繹におけるweakening
規則とcontration
規則を特徴化付ける。従来の自然演繹のシステム（NK、ND
では、合 意の導入規則が適用される際、除去される仮定の数は通常区別されない。ここでは除去される仮定の数（n）を区別して、含意の導入を三つに分 ける 。す なわ ち、 n ‑0， n‑1，n≧ 2の 場合 であ る 。そして、weakening
規則はn‑0に対応し、contraction規則はn≧2に対応していることを示す（定理1Characterizationofweakening、定理2C
haracterizationofcontraction)。
第 二 部 で は 、 自 然 演 繹 に お け る exchange規 則 の 特 徴 化 付 け を 行 う 。
まず、weakening
規則、contraction規則とexchange規則という、構造推論規規則を全く持たない自然演繹のシステムを導入する 。それをNFL(NaturalfullLambek)と呼ぶ。N
FLの証明には、その証明を木とみなした反辞書式順序が入っている。仮定の除去を伴う推論規則の適用条件は、除去されていない仮定の中でその順序の一番小さいものを除去するときしか適用できないように、制限されている。このように推論規則の適用条件を制限することによって、NFL
ではexc
hange
規則の除去を実現している。
そ して、部分構造論理のシークェント計 算のシステムFL (full Lambek)とNF
Lが同値であ るこ とを 証明 する （ 定理 3 Equival
ence of NFL and FL)。F
Lはweakenin
g規則、cont
ract
ion
規則とexchange
規則という、構造推論規則を全く持たないシークェント計算のシステムで、部分構造論理や、線形論理に共通の土台を与える基本的なシステムである。FLは 小 野 に よ っ て Cut除 去 定 理 や 健 全 性 定 理 、 完 全 性 定 理 が 証 明 さ れ て い る 。
次に、上記の適用条件の制限を無効に する推論規則をNFLに付け加える。すると、この新し いシ ステ ムで はexcha
nge規則が実現されている。このことはFLにexc
hange規則を加えァこシステムと新しいシステムが同値になることで証明される（定理4C
haracterizationofexchange)
。

― 76―

学位論 文審査の要旨
主査
副査
副査
副査

教授

辻下徹

教授

吉田知行

教授

津田一郎

助教授

中 戸川孝治（ 北海道 大学文学部哲学科）

学位論文題名NaturalDeductionsf
orSubstructuralLogics（部分構造論理の自然 演繹での定式化）
近年、数理論理学の分野において主に計算機科学からの要請で、非古典論理と総称される、古典的な推論規則を変更した論理系の研究が広範に進められている。排中律を認めない直観主義的論理は、種々の文脈で重要性が認識されており、その研究は長い歴史をもっているが、論理式の数や並び方まで情報として取り入れる部分構造論理は、長く趣味的なテーマとみなされてきた。しかし近年、計算科学において、資源の量的な面まで考慮にいれたプ口セスの記述法として脚光を集めるようになり、多くの研究者が取り組み多くの研究成果を産むようになってきた。
従来、部分構造論理は従来シークエント計算と呼ばれる証明論に基づいて定式化され研究されてきた。しかし、20世紀前半に証明の別の定式化である自然演繹体系を導入されて以来、構造推論規則が個別の推論規則として明確に取り出されたことはなく、構造推論規則の働きは他の論理記号の推論規則の中に埋もれてしまっていた。構造推論規則が明示されていなかった為、自然演繹での構造推論規則の研究は従来ほとんど行われていなかった。
その理由は、推論過程における証明図の変化が局所的であるシークェント計算体系と比べた場合、素朴な証明過程を直に形式化した自然演繹体系では、推論過程において含意導入・ 除去規則 適用時に 証明図の全 体的構造 が変化す るため、 推論過程の分析が容易ではないた めである 。
申請 論文は、自然演繹体系におしゝて、構造規則がどのように表現されるかを吟味し次の結果 を得た。
（1）自然 演繹にお ける弱化規 則と縮約 規則とを 定式化し 、新しい 推論規則 による自然演繹 体系にお ける証明 可能性と、 シークェ ント計算 体系から 弱化規則と縮約規則とを除外した 体系にお ける証明 可能性とが 一致する 。
（ 2） NFLと呼 ぶ 自 然演 繹 体系 を 導 入し 、 そ れの 証 明可 能 概 念と 、 FLと 呼 ばれ る シ ー
クエ ント計算 体系の証 明可能概念 とが一致 する。
（3）NFLに つい て の 4つ の含 意 に関 す る 導入 ・ 除去 規 則 を定 式化し、 証明可能 性に関
レ て は、 こ れら の う ちい ず れか ー つ をNFLに 添 加す る こと と 、FLに可 換規則を 追加する
こと と同じ効 果を持つ ことを示し た。
これ を要する に、本論 文は、従来 専らシー クエント 計算体系に基づいて展開されてきた部分 構造論理 の研究を 、自然演繹 体系に基 づいて展 開する端 緒を開くものということがで
き 、 非 古 典 論 理 の 分 野 に 対 する 、貢 献す る 所大 なる もの があ る 。
よっ て 著者 は 、 北海 道 大 学博 士（理学 ）の学位 を授与さ れる資格 あるもの と認める。