Loading article…
論理学および論理哲学、特に演繹的推論において、推論規則、推論規則、または変換規則は、前提を受け取り、その構文を分析し、結論（または複数の結論） を返す関数で構成される論理形式です。
たとえば、モダス・ポネンスと呼ばれる推論規則は、2 つの前提 (1 つは「p ならば q」という形式、もう 1 つは「p」という形式) を取り、結論「q」を返します。この規則は、前提が (ある解釈の下で) 真であれば結論も真であるという意味で、古典論理の意味論(および他の多くの非古典論理の意味論)に関して有効です。
通常、推論規則は真理、つまり意味的性質を保持する。多値論理では、一般的な指定を保持する。しかし、推論規則の作用は純粋に統語論的であり、意味的性質を保持する必要はない。つまり、一連の式から一連の式へのあらゆる関数は推論規則として数えられる。通常、再帰的な規則だけが重要である。つまり、規則によれば、任意の式が一連の式の結論であるかどうかを判断するための有効な手順がある規則である。この意味で有効でない規則の例は、無限ω規則である。[1]
命題論理における一般的な推論規則には、modus ponens、modus tollens、およびcontrapositionが含まれます。一階述語論理では、推論規則を使用して論理量指定子を扱います。
標準フォーム
形式論理（および多くの関連分野）では、推論規則は通常、次の標準形式で与えられます。
前提#1
前提#2
...
前提#n
結論
この表現は、何らかの論理的導出の過程で与えられた前提が得られた場合はいつでも、指定された結論も当然とみなすことができる、ということを示しています。前提と結論の両方を記述するために使用される正確な形式言語は、導出の実際のコンテキストによって異なります。単純なケースでは、次のような論理式を使用できます。
これは命題論理のモダスポネンス規則である。推論規則はメタ変数を用いたスキーマとして定式化されることが多い。[2]上記の規則（スキーマ）では、メタ変数AとBを宇宙の任意の要素（または慣例により命題などの制限されたサブセット）にインスタンス化して、無限の推論規則の集合を形成することができる。
証明システムは、証明を形成するために連結された一連の規則から構成され、これは導出とも呼ばれます。導出には、証明または導出されたステートメントである最終的な結論が 1 つだけあります。導出で前提が満たされない場合、その導出は「前提が成り立つ場合、結論が成り立つ」という 仮説的なステートメントの証明になります。
例: 2つの命題論理に対するヒルベルトシステム
ヒルベルト体系では、推論規則の前提と結論は、通常はメタ変数を使用する言語の単なる式です。図式的な表現を簡潔にし、公理と推論規則の違いを強調するために、このセクションでは規則の垂直な表現の代わりに シーケント表記法 ( ) を使用します。この表記法では、
と書きます。
古典的な命題論理の形式言語は、否定 (¬)、含意 (→)、命題記号のみを使用して表現できます。3 つの公理スキーマと 1 つの推論規則 ( modus ponens )で構成されるよく知られた公理化は次のとおりです。
(CA1) ⊢ A → ( B → A )
(CA2) ⊢ ( A → ( B → C )) → (( A → B ) → ( A → C ))
(CA3) ⊢ (¬ A → ¬ B ) → ( B → A )
(MP) A , A → B ⊢ B
この場合、⊢と→という2つの推論の概念があるのは冗長に思えるかもしれない。古典的な命題論理では、これらは実際に一致している。演繹定理は、 A ⊢ Bである場合に限り、⊢ A → Bであると述べている。しかし、この場合でも強調する価値のある区別がある。最初の表記は演繹、つまり文から文へ移る動作を記述するのに対し、A → Bは、この場合、単に論理接続子、含意で作られた式である。推論規則（この場合のmodus ponensなど）がなければ、演繹も推論もない。この点は、ルイス・キャロルの「アキレスに亀が言ったこと」という対話[3]や、その後のバートランド・ラッセルとピーター・ウィンチによる対話で紹介されているパラドックスを解決しようとした試みで示されている。
いくつかの非古典的論理では演繹定理は成立しない。例えば、Łukasiewiczの3値論理は次のように公理化できる。[4]
(CA1) ⊢ A → ( B → A )
(LA2) ⊢ ( A → B ) → (( B → C ) → ( A → C ))
(CA3) ⊢ (¬ A → ¬ B ) → ( B → A )
(LA4) ⊢ (( A → ¬ A ) → A ) → A
(MP) A , A → B ⊢ B
このシーケンスは、公理2の変更と公理4の追加によって古典論理と異なります。古典的な演繹定理はこの論理には当てはまりませんが、修正された形式、つまりA ⊢ Bである場合に限り、⊢ A → ( A → B ) が成立します。[5]
許容性と推論可能性
一連の規則では、推論規則は許容可能または導出可能であるという意味で冗長である可能性があります。導出可能な規則とは、その結論が他の規則を使用してその前提から導出できる規則です。許容可能な規則とは、前提が成り立つときは常に結論が成り立つ規則です。導出可能な規則はすべて許容可能です。違いを理解するには、自然数を定義する次の一連の規則を検討してください(判決では、 が自然数である という事実を主張しています)。
最初の規則は0が自然数であることを述べ、2 番目の規則はnが自然数であればs( n )も自然数であると述べています。この証明システムでは、自然数の 2 番目の数も自然数であることを示す次の規則を導出できます。
その導出は、上記の後続ルールの 2 つの使用を組み合わせたものです。任意の非ゼロ数に対して先行数の存在を主張する次のルールは、単に許容されるだけです。
これは自然数の真の事実であり、帰納法によって証明できます。(この規則が許容可能であることを証明するには、前提の導出を仮定し、それに基づいて帰納法を行って の導出を生成します。) ただし、これは前提の導出の構造に依存するため、導出可能ではありません。このため、導出可能性は証明システムへの追加に対して安定していますが、許容可能性は安定していません。違いを確認するために、次のナンセンスな規則が証明システムに追加されたと仮定します。
この新しいシステムでは、二重後続ルールは依然として導出可能です。しかし、 を導出する方法がないため、先行ルールを見つけるルールはもはや許容されません。許容性の脆弱性は、証明方法に起因します。証明は前提の導出の構造に基づいて帰納的に行うことができるため、システムの拡張によってこの証明に新しいケースが追加され、それがもはや成立しなくなる可能性があります。
許容される規則は、証明システムの定理として考えることができます。たとえば、カット除去が成り立つシーケント計算では、カット規則は許容されます。
参照
参考文献
- ^ Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). 計算可能性と論理。ケンブリッジ: ケンブリッジ大学出版局。p. 364。ISBN 978-0-521-87752-7。
- ^ ジョン・C・レイノルズ (2009) [1998]. プログラミング言語の理論. ケンブリッジ大学出版局. p. 12. ISBN 978-0-521-10697-9。
- ^ Kosta Dosen (1996)。「論理的帰結：スタイルの転換」。Maria Luisa Dalla Chiara、Kees Doets、Daniele Mundici、Johan van Benthem (編)。論理と科学的方法：第 10 回国際論理、方法論、科学哲学会議第 1 巻、フィレンツェ、1995 年 8 月。Springer。p. 290。ISBN 978-0-7923-4383-7。プレプリント（ページ番号が異なる）
- ^ Bergmann, Merrie (2008).多値論理とファジー論理入門: 意味論、代数、導出システムケンブリッジ大学出版局。p. 100。ISBN 978-0-521-88128-9。
- ^ Bergmann, Merrie (2008).多値論理とファジー論理入門: 意味論、代数、導出システムケンブリッジ大学出版局。p. 114。ISBN 978-0-521-88128-9。