Asinus's blog

西牟田祐樹のブログです。

もうひとつの自然演繹: Jaśkowski, Theory of deduction based on the method of suppositionを読む

Jaśkowskiの自然演繹についての概要

  • 自然演繹といえばゲンツェンがシーケント計算と共に考案したことで有名だが、ちょうど同年の1934年にヤスコフスキ(Jaśkowski)も自然演繹についての論文を発表した。
  • ゲンツェン流とヤスコフスキ流の大きな違いは、ゲンツェン流では証明はtreeであるのに対して、ヤスコフスキ流の証明はlinearである。
  • また、ゲンツェンは論理結合子に関する推論規則を導入規則と除去規則の二種類に分けたが、ヤスコウスキはそのような概念については述べていない。
  • 現在では通常ゲンツェン流の自然演繹が読みやすさゆえに用いられているが、Prawitz(1965)以前はヤスコフスキ流の自然演繹の別バリエーションがよく用いられていた。その中でもFitchの自然演繹(1952)が特に有名である。
  • 近年Fitch styleは様相論理や様相ラムダ計算との関連で新たに注目を浴び、有用性が再認識されている。例えばClouston (2018)を参照。

Jaśkowskiのテキストについて

以下テキストについての情報は主にHazen&Pelletier(2014)による。

  • 最初に発表されたのはFirst Polish Mathmatical Congress, Lvov, 1927だった。
  • その出版されたproceedings, 1929にはタイトルしか記載がなかった。
  • ヤスコフスキは証明の二つの表記法を考案しているが、この時の表記法は1934年の論文の注で説明されている。
  • 1934年に論文 "The theory of deduction based on the method of suppositions"を発表した。
  • これ以降にヤスコフスキ自身による自然演繹の論文は発表されていない。 それゆえヤスコフスキ自身の考えを知ることができるのは1934年の論文からだけである。

論文解説

以下では論理式の記法はポーランド記法ではなく中置記法で書くことにする。

推論規則

論文内で説明される推論規則を先に説明しておく。ゲンツェン流の規則との対応を書くと以下の通り。

Rule I: 仮定[の導入]に対応

Rule II: 含意の導入規則に対応

Rule III: 含意の除去規則に対応

Rule IV: RAAに対応する。

これはルカシェビッチの公理  (\neg p\Rightarrow p)\Rightarrow p と対応している。ORłowska(1975)によるとŁukasiewicz(1929)で用いられている公理である。

Rule IVa: 否定の導入規則に対応

これはルカシェビッチの公理  p\Rightarrow(\neg p\Rightarrow q) と対応している。

Rule V: 二階全称量化の除去に対応

Rule VI: 二階全称量化の導入に対応

Rule Va: 一階全称量化の除去規則に対応

Rule VIa: 一階全称量化の導入規則に対応

Section 1: 論文のアイデアと目的及び導入的説明

この論文の背後にあるアイデアはルカシェヴッチが講義で語っていた次のような考えである。

In 1926 Prof. J. Ł u k a s i e w i c z called attention to the fact that mathematicians in their proofs do not appeal to the theses of the theory of deduction, but make use of other methods of reasoning. The chief means employed in their method ist that of an arbitrary supposition.

このようなアイデアはGentzen(1935)5.11.でも語られている。

実際の推論に十分に適合していること、そのことを我々は出発点としている。それゆえこのような計算体系は特に数学者の証明を形式化するのに適している。

論文のタイトル通り、ヤスコフスキの提示した体系はSupposition(仮定)というアイデアに基づいている。これはゲンツェンの体系でいう含意や選言の規則に現れる角括弧 [A_1]の部分に相当する。

この論文の目的はウカシェヴィッチのアイデアを形式化し、ウカシェヴィッチの次の問題に答えを与えることである。

The problem raised by Mr. Ł u k a s i e w i c z was to put these methods unter the form of structural rules and to analyze their relation to the theory of deduction. The present paper contains the solution of that problem.

この論文は技術的なものであり、新しい体系やその推論規則に対する思想的な内容については述べられていない。この点はアイデアについても説明したゲンツェンとは異なる。

直観主義論理と古典論理のどちらかのみを用いるといった態度でもない。

上述の論文の目的の説明の後、まずはインフォーマルにSuppositionについて説明している。そして彼の自然演繹の表記法について説明される。仮定と導出された論理式全体のなす集合(クラス)はdomainと呼ばれる。これは導出の各段階ごとに定まる(増大する)。説明される各推論規則については後ろにまとめておく。sec.1ではRule I - IVが説明されている。Rule I-IIIは命題論理の含意の部分体系である。ここで他に否定の規則が説明されていないにも関わらず、reductio ad absurdum (RAA)が扱われているのは奇妙に思えるが、ヤスコフスキは注3で、1927年の記法で含意とRAAを用いた証明の例を書いている。なのでこの例の説明としてはRAAを説明しておく必要があるからここで扱われたのだろう。仮定の中に否定を含む論理式が現れている。

Rule I - IVからなる体系tdの証明の例が二つ挙げられている。一つ目の証明の後では結論は否定記号を含まないが、途中のRAA規則において否定を含む論理式が用いられていることに言及している。RAAがsubformula propertyを損ねる事実に適切にも注意を与えている。RAAを含むのでこの体系は古典論理である。二つ目の演繹では仮定がすべては閉じられていないような例である。domainから得られる公理的体系(system)を考えた時、composite systemとは仮定がすべては閉じられていないようなdomainに相当するものであり、simple systemとはすべて閉じられているdomainに相当する。

Section 2: ウカシェヴィッチの公理系TDの場合

この章から論文の目的であった証明能力の同等性を示す作業が行われる。

ウカシェヴィッチの公理系 TDと自然演繹体系td について、表記の簡略化のためにそれぞれの体系での定理も同じ記号で書かれる。以下定理については、内容が相違しない範囲で表現を変えて述べることにする。

TD1:  (p\to q)\to ( (q\to r)\to (p\to r) )

TD2:  (\neg p\to p)\to p

TD3:  p\to (\neg p \to q)

定理1 TDでの任意の定理に対し、その定理はtdで証明可能である。

TD1-3はsec.1で例として証明されている。TD1-3を対応する演繹に置き換え、TDで用いられるmodus ponensの代わりにRule IIIを適用していけば良い。

tdは仮定1行のみの演繹が考えられるので、逆を言うためには適切な制限を加える必要がある。このような仮定のみを定理と呼ぶのは現代の用語法ではないが、ヤスコフスキではそう呼ばれている。development (containing a formula A) という用語が導入されるが、これは条件化によってすべての仮定が閉じられた(Aを含む)論理式を表す。

定理2 tdの任意の定理に対し、その定理のdevelopmentはTDで証明可能である。

この定理の証明には意味論が用いられている。真理値モデルに関するTDの完全性定理が使われる。ここではtdの真理値モデルに関する健全性定理が示され、この完全性定理と組み合わされることが定理が証明される。

"It is known that , for any expression satisfying the method of verification through substitution of the values 1 and 0 for variables, we can obtain an equiform thesis TD"

Section 3: Incomplete systemの場合

Hilbert(1922)のpositive logicとそれに同値であるFrege(1922)の体系がPTD(Positive Theory of Deduction)として扱われる。この章の特徴は論理体系の証明能力が弱い分、自然演繹の定理が公理的体系でも(developmentが)定理になるということの証明に意味論が使われず、構文論的に証明されていることである。このためにpositive logicの章を論文に含めたのかもしれない。

PTD1:  p\to(q\to r)

PTD2:  (p\to (q\to r))\to (  (p\to q)\to (p\to r)  )

定理3 PTDでの任意の定理に対し、その定理はptdで証明可能である。

証明例としてPTD1とPTD2が自然演繹で証明されている。これより従う。

定理4 ptdの任意の定理に対し、その定理のdevelopmentはPTDで証明可能である。

ptdにおける証明の長さに関する帰納法。あらかじめ証明に用いるPTDでの定理が I_k, II_k, III_kとして最初の部分で証明されている。推論規則ごとに場合分けし、 I_k, II_k, III_kを用いていく。

ptdの後でRule I-III + IVa, つまり含意断片と否定の導入規則の体系がitdとして扱われる。これはKolmogoroff(1925)の体系と対応する。これは直観主義論理である。

ITD1:  p\to(q\to p)

ITD2:  (p\to (q\to r))\to (  (p\to q)\to (p\to r)  )

ITD3:  (p\to q)\to (  (p\to\neg q)\to \neg p  )

定理5 ITDでの任意の定理に対し、その定理はitdで証明可能である。

定理6 itdの任意の定理に対し、その定理のdevelopmentはITDで証明可能である。

証明方針はptdの場合と同様。ITDPTDを含んでいるので、否定についてだけ示せば十分。

Section 4: 二階論理の場合

二階論理の場合の証明能力の同値性の証明は証明方針はsec2と同様であるが、完全性を示すのが難しい。Henkin(1950)がヘンキンモデルを用いて完全性定理を示した。実際に第三章までしか同値性に関する定理は述べられていない。この章では自然演繹体系の定義の後に、証明の具体例を提示しただけで終わる。"The needed proofs are analogous to those of the theorems 1 and 2"とopen problemであることが述べられる。ただしこの章では公理論的体系の公理は述べられていない。

Section5: 一階述語論理の場合

ここではPrincipia MathematicaとHilbertが参照されている。この章でも公理論的体系の公理は述べられていない。自然演繹の定義の後、証明の例を述べて終わる。

推論規則はどのように選ぶのか?

論文内では含意と否定と一階と二階の全称量化の論理結合子しか扱われていないが、これらだけに限定されないことは次のように説明されている。

The rules of the composite systems can be applied to different logical or mathematical systems. In such cases, it can happen that new rules may be required. For instance, it we want to build the composite system of the theory of deduction having besides "C" and "N" the new constant term of conjunction (logical product), it is sufficient to give three new rules. The first would permit us to subjoin to a domain a conjunction composed of propositions equiform with some propositions valid in that domain, and the others would allow to subjoin a proposition equiform with the first and a proposition equiform with the second member of a valid conjunction.

この説明での連言の規則は(導入規則や除去規則と呼ばれないこと以外は)Gentzenのものと一致する。これは公理的論理体系から得られた規則であると推測できる。

例えばHilbert&Ackermann(1959)ではFormula (12)  X\land Y\to X, Formula (13)  X\land Y\to Y, formula (18)  X\to(Y\to X\land Y)である。 連言に限らず一般に、推論規則の発見の仕方としては、公理論的体系の公理あるいは定理の前件を自然演繹規則の前提とし、後件を結論とすることで得られる。

どのような論理結合子(あるいはその推論規則)が許容されるべきか、あるいは選択されるべきかについてこの論文から何か言えるだろうか?

この論文の目的が証明能力の同等性を示すことだということを考慮に入れるならば、この論文からは特別なヤスコフスキの論理学的・哲学的な立場は読み取ることができない。他の公理系を参照して、その公理系と証明能力において同等となるような推論規則が選択されている。ただしこの論文での様々な体系を分け隔てなく提示するスタイルはWolenski(1989)の次のような説明とよく合致している (p. 191)。

In general (except for Leśniewski) opinions in the sphere of the philosophy of logic and mathematics were treated in the Warsaw School as 'private' problems, which did not, or at least should not, have any influence upon logical research, except, of cource, for the heuristic issues. But all philosophically motivated logical construction (e.g. the theory of truth and many-valued logics) was treated primarily as logical and as such it had to meet formal, and not philosophical, criteria.

ヤスコフスキの論理結合子や推論規則の扱いは、論理学的な結果を追求していくという目的のためには非常にバランスの取れたものであった。しかし、ゲンツェンのように論理結合子や推論規則に対するアイデアを提示しなかったことで、自然演繹の整備とともにヤスコフスキの論文の内容は古くなり、読まれることがなくなってしまった。

参考文献

Jaśkowski, On the Rules of Suppositions in Formal Logic, Studia Logica 1, pp. 5–32, 1934.

Gentzen, Untersuchungen über das logische Schließen I, Mathematische Zeitschrift 39 (2), pp. 176-210, 1934.

Wolenski, Logic and philosophy in the Lvov-Warsaw school, Kluwer academic publishers, 1989.

Hilbert and Ackermann, Grundzüge der theoretischen Logik, Springer, 1959.

Orłowska, On the Jaśkowski's method of suppositions, Studia Logica, 34 (2), pp. 187-200, 1975.

Hazen and Pelletier, Gentzen and Jaśkowski Natural Deduction: Fundamentally Similar but Importantly Different, Studia Logica, 102 (6), pp. 1103-1142, 2014.

Clouston, Fitch-Style Modal Lambda Calculi, Foundations of Software Science and Computation Structures (FoSSaCS) , pp.258-275, 2018.