Schlussfolgerungsregel - Rule of inference

In der Philosophie der Logik ist eine Inferenzregel , Inferenzregel oder Transformationsregel eine logische Form, die aus einer Funktion besteht, die Prämissen nimmt, ihre Syntax analysiert und eine Schlussfolgerung (oder Schlussfolgerungen ) zurückgibt . Zum Beispiel nimmt die modus ponens genannte Inferenzregel zwei Prämissen, eine in der Form "Wenn p, dann q" und eine andere in der Form "p", und gibt die Schlussfolgerung "q" zurück. Die Regel gilt in Bezug auf die Semantik der klassischen Logik (wie auch die Semantik vieler anderer nichtklassischer Logiken ) in dem Sinne, dass, wenn die Prämissen (unter einer Interpretation) wahr sind, die Schlussfolgerung auch wahr ist.

Typischerweise bewahrt eine Inferenzregel die Wahrheit, eine semantische Eigenschaft. In der vielwertigen Logik behält es eine allgemeine Bezeichnung bei. Aber die Wirkung einer Inferenzregel ist rein syntaktisch und braucht keine semantische Eigenschaft zu bewahren: Jede Funktion von Formelmengen bis zu Formeln zählt als Inferenzregel. Normalerweise sind nur rekursive Regeln wichtig; dh Regeln, so dass es ein wirksames Verfahren gibt, um zu bestimmen, ob eine gegebene Formel die Konklusion einer gegebenen Menge von Formeln gemäß der Regel ist. Ein Beispiel für eine in diesem Sinne nicht wirksame Regel ist die unendliche ω-Regel .

Beliebte Schlußregeln in der Aussagenlogik sind der Modus Ponens , der Modus tollens und die Kontraposition . Die Prädikatenlogik erster Ordnung verwendet Inferenzregeln, um mit logischen Quantoren umzugehen .

Standardform

In der formalen Logik (und vielen verwandten Bereichen) werden Schlußregeln normalerweise in der folgenden Standardform angegeben:

  Prämisse#1
  Prämisse#2
        ...
  Prämisse#n   
  Fazit

Dieser Ausdruck besagt, dass immer dann, wenn im Laufe einer logischen Ableitung die gegebenen Prämissen erhalten wurden, die angegebene Schlussfolgerung ebenfalls als selbstverständlich angesehen werden kann. Die genaue formale Sprache, mit der sowohl Prämissen als auch Schlussfolgerungen beschrieben werden, hängt vom tatsächlichen Kontext der Ableitungen ab. In einem einfachen Fall kann man logische Formeln verwenden, wie in:

Dies ist die Modus-Ponens- Regel der Aussagenlogik . Inferenzregeln werden oft als Schemata formuliert, die Metavariablen verwenden . In der obigen Regel (Schema) können die Metavariablen A und B zu jedem Element des Universums (oder manchmal, gemäß Konvention, einer eingeschränkten Teilmenge wie Propositionen ) instanziiert werden , um einen unendlichen Satz von Inferenzregeln zu bilden .

Ein Beweissystem besteht aus einer Reihe von Regeln, die zu Beweisen verkettet sind, auch Ableitungen genannt . Jede Ableitung hat nur eine abschließende Schlussfolgerung, nämlich die bewiesene oder abgeleitete Aussage. Bleiben Prämissen in der Ableitung unbefriedigt, so ist die Ableitung ein Beweis für eine hypothetische Aussage: " Wenn die Prämissen gelten, dann gilt die Konklusion."

Beispiel: Hilbert-Systeme für zwei Aussagenlogiken

In einem Hilbert-System sind die Prämissen und Schlussfolgerungen der Inferenzregeln einfach Formeln einer Sprache, die normalerweise Metavariablen verwenden. Aus Gründen der grafischen Kompaktheit der Darstellung und um die Unterscheidung zwischen Axiomen und Inferenzregeln hervorzuheben, verwendet dieser Abschnitt die sequentielle Notation ( ) anstelle einer vertikalen Darstellung von Regeln. In dieser Schreibweise

wird geschrieben als .

Die formale Sprache der klassischen Aussagenlogik kann nur durch Negation (¬), Implikation (→) und Aussagesymbole ausgedrückt werden. Eine bekannte Axiomatisierung, bestehend aus drei Axiomenschemata und einer Inferenzregel ( modus ponens ), lautet:

(CA1) ⊢ A → (BA)
(CA2) ⊢ (A → (BC)) → ((AB) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(MP) A, ABB

Es mag überflüssig erscheinen, in diesem Fall zwei Inferenzbegriffe zu haben, und →. In der klassischen Aussagenlogik fallen sie tatsächlich zusammen; der Deduktionssatz besagt, dass AB genau dann gilt, wenn ⊢ AB . Es gibt jedoch auch hier einen hervorzuhebenden Unterschied: Die erste Notation beschreibt eine Deduktion , also eine Aktivität des Übergehens von Sätzen zu Sätzen, während AB einfach eine Formel mit einem logischen Konnektor ist , in diesem Fall Implikation. Ohne eine Inferenzregel (wie in diesem Fall modus ponens ) gibt es keine Deduktion oder Inferenz. Dieser Punkt wird in Lewis Carrolls Dialog „ What the Tortoise Said to Achilles “ illustriert , sowie in späteren Versuchen von Bertrand Russell und Peter Winch , das in dem Dialog eingeführte Paradox aufzulösen.

Für einige nichtklassische Logiken gilt der Deduktionssatz nicht. Zum Beispiel kann die dreiwertige Logik von Łukasiewicz axiomatisiert werden als:

(CA1) ⊢ A → (BA)
(LA2) ⊢ (AB) → ((BC) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(LA4) ⊢ ((A → ¬A) → A) → A
(MP) A, ABB

Diese Folge unterscheidet sich von der klassischen Logik durch die Änderung von Axiom 2 und die Hinzufügung von Axiom 4. Der klassische Deduktionssatz gilt für diese Logik nicht, jedoch eine modifizierte Form, nämlich AB genau dann, wenn ⊢ A → ( AB ).

Zulässigkeit und Ableitbarkeit

In einem Regelwerk könnte eine Inferenzregel in dem Sinne redundant sein, dass sie zulässig oder ableitbar ist . Eine ableitbare Regel ist eine Regel, deren Schlussfolgerung aus ihren Prämissen unter Verwendung der anderen Regeln abgeleitet werden kann. Eine zulässige Regel ist eine Regel, deren Konklusion immer dann gilt, wenn die Prämissen gelten. Alle ableitbaren Regeln sind zulässig. Um den Unterschied zu verstehen, betrachten Sie die folgenden Regeln zur Definition der natürlichen Zahlen (das Urteil bestätigt die Tatsache, dass es sich um eine natürliche Zahl handelt):

Die erste Regel besagt, dass 0 eine natürliche Zahl ist, und die zweite besagt, dass s( n ) eine natürliche Zahl ist, falls n es ist. In diesem Beweissystem lässt sich folgende Regel ableiten, die zeigt, dass der zweite Nachfolger einer natürlichen Zahl auch eine natürliche Zahl ist:

Seine Ableitung ist die Zusammensetzung von zwei Verwendungen der oben genannten Nachfolgeregel. Die folgende Regel zur Behauptung der Existenz eines Vorgängers für eine beliebige Zahl ungleich Null ist lediglich zulässig:

Dies ist eine wahre Tatsache der natürlichen Zahlen, wie durch Induktion bewiesen werden kann . (Um zu beweisen, dass diese Regel zulässig ist, nehmen Sie eine Ableitung der Prämisse an und leiten Sie daraus eine Ableitung von ab .) Sie ist jedoch nicht ableitbar, da sie von der Struktur der Ableitung der Prämisse abhängt. Aus diesem Grund ist die Ableitbarkeit unter Hinzufügungen zum Beweissystem stabil, die Zulässigkeit jedoch nicht. Um den Unterschied zu sehen, nehmen wir an, dass dem Beweissystem die folgende Unsinnsregel hinzugefügt wurde:

In diesem neuen System ist die Doppelnachfolgerregel noch ableitbar. Die Regel zum Auffinden des Vorgängers ist jedoch nicht mehr zulässig, da keine Ableitung möglich ist . Die Brüchigkeit der Zulässigkeit ergibt sich aus der Art des Beweises: Da der Beweis auf die Struktur der Ableitungen der Prämissen einleiten kann, fügen Systemerweiterungen diesem Beweis neue Fälle hinzu, die möglicherweise nicht mehr gelten.

Zulässige Regeln kann man sich als Theoreme eines Beweissystems vorstellen. Zum Beispiel ist in einem nachfolgenden Kalkül, in dem die Schnitteliminierung gilt, die Schnittregel zulässig.

Siehe auch

Verweise