RMの建設的分析

システムRMは、アンダーソンとベルナップの学派によって発展された論理の中で、最もよく理解されている（そして私たちの意見では、最も重要な）システムです。本論文では、建設的な観点からRMを調査します。例えば、私たちは、スギハラ行列に対するRMの完全性の新しい証明を示します（最初にマイヤーによって示されたもの）。ここでは、p.r.手続きが提示されており、RM言語の文Aにこれを適用すると、RMにおけるそれの証明またはスギハラ行列S Zにおけるそれの反証価値が得られます。この作業で扱われる2つのトピックは特に注目に値します。a) γの適用可能性。これはマイヤーとダンの有名な定理です。1 アンダーソンとベルナップは、「マイヤー・ダンの議論は…Bの証明の存在を保証しますが、Bの証明がAとĀ ∨ Bの証明と何らかの妥当な方法で関連することが保証されるわけではありません。」と強調しています。§2ではRMの場合にそのような保証を提供します。実際、AとĀ ∨ Bの証明からBの証明を得る直接的な方法をここで示します。 b) RMとその完全な反意帰納片の関係。RMは（Sobocińskiの3値論理を参照；4を見よ）保守的な拡張であることが知られています。アンダーソンとベルナップは、RM全体が三値からかけ離れているため、この事実が彼らにとって明らかな驚きであったと認めています。とはいえ、本論文ではこの「驚くべき」事実は非常に自然に現れます（III.3を参照）。実際、私たちは、がRMの「ハードコア」であることを示します。なぜなら、RMの完全性の証明が根本的にSobociński行列に対する完全性に基づいており、またRMのために開発するジェンツェン型計算がに対する類似の（しかしはるかに単純な）計算の直接的な拡張であるからです。この作業におけるの重要性のために、私たちは最初のセクションをその建設的な調査に捧げます。最後に、上記のジェンツェン型計算はカット消去と標準形技術を許容することに注意します。（そのような計算は、分配なしのRMに対してのみこれまで発見されてきました。）