Aussagenrechnung - Propositional calculus

Die Aussagenrechnung ist ein Zweig der Logik . Es wird auch als Propositionslogik , Aussagenlogik , Aussagenkalküls , sentential Logik , oder manchmal auch der nullten Ordnung Logik . Es befasst sich mit Aussagen (die wahr oder falsch sein können) und Beziehungen zwischen Aussagen, einschließlich der Konstruktion von darauf basierenden Argumenten. Zusammengesetzte Aussagen werden gebildet, indem Aussagen durch logische Verknüpfungen verbunden werden . Sätze, die keine logischen Verknüpfungen enthalten, heißen atomare Sätze.

Im Gegensatz zur Logik erster Ordnung befasst sich die Aussagenlogik nicht mit nicht-logischen Objekten, Prädikaten über sie oder Quantoren . Die gesamte Maschinerie der Aussagenlogik ist jedoch in der Logik erster Ordnung und in der Logik höherer Ordnung enthalten. In diesem Sinne ist die Aussagenlogik die Grundlage der Logik erster und höherer Ordnung.

Erläuterung

Logische Verknüpfungen finden sich in natürlichen Sprachen. Im Englischen zum Beispiel sind einige Beispiele "and" ( Konjunktion ), "or" ( Disjunktion ), "not" ( Negation ) und "if" (aber nur, wenn sie verwendet werden, um Materialbedingung zu bezeichnen ).

Das Folgende ist ein Beispiel für eine sehr einfache Inferenz im Rahmen der Aussagenlogik:

Prämisse 1: Wenn es regnet, ist es bewölkt.
Prämisse 2: Es regnet.
Fazit: Es ist bewölkt.

Sowohl Prämissen als auch die Konklusion sind Aussagen. Die Prämissen werden als selbstverständlich vorausgesetzt, und mit der Anwendung von modus ponens (einer Inferenzregel ) folgt die Schlussfolgerung.

Da sich die Aussagenlogik nicht mit der Struktur von Aussagen über den Punkt hinaus befasst, an dem sie nicht mehr durch logische Verknüpfungen zerlegt werden können, kann diese Schlussfolgerung neu formuliert werden, indem diese atomaren Aussagen durch Aussagebuchstaben ersetzt werden , die als Variablen interpretiert werden, die Aussagen repräsentieren:

Prämisse 1:
Prämisse 2:
Abschluss:

Dasselbe lässt sich kurz und bündig wie folgt formulieren:

Wenn P als "Es regnet" und Q als "Es regnet" interpretiert wird, können die obigen symbolischen Ausdrücke genau dem ursprünglichen Ausdruck in natürlicher Sprache entsprechen. Nicht nur das, sondern sie werden auch mit jeder anderen Folgerung dieser Form übereinstimmen , die auf der gleichen Grundlage wie diese Folgerung gültig ist.

Propositionslogik kann durch ein untersucht werden formales System , in dem Formeln einer formalen Sprache kann interpretiert darstellen Sätze . Ein System von Axiomen und Inferenzregeln erlaubt die Ableitung bestimmter Formeln. Diese abgeleiteten Formeln werden Theoreme genannt und können als wahre Aussagen interpretiert werden. Eine konstruierte Folge solcher Formeln wird als Ableitung oder Beweis bezeichnet und die letzte Formel der Folge ist der Satz. Die Herleitung kann als Beweis des Satzes interpretiert werden, der durch den Satz repräsentiert wird.

Wenn ein formales System verwendet wird, um formale Logik darzustellen, werden nur Anweisungsbuchstaben (normalerweise lateinische Großbuchstaben wie , und ) direkt dargestellt. Die Sätze der natürlichen Sprache, die bei ihrer Interpretation entstehen, liegen außerhalb des Anwendungsbereichs des Systems, und die Beziehung zwischen dem formalen System und seiner Interpretation liegt ebenfalls außerhalb des formalen Systems selbst.

In der klassischen wahrheitsfunktionalen Aussagenlogik werden Formeln so interpretiert, dass sie genau einen von zwei möglichen Wahrheitswerten haben , den Wahrheitswert von wahr oder den Wahrheitswert von falsch . Das Prinzip der Bivalenz und das Gesetz der ausgeschlossenen Mitte werden gewahrt. Als solche definierte wahrheitsfunktionale Aussagenlogik und dazu isomorphe Systeme gelten als Logik nullter Ordnung . Es sind jedoch auch alternative Aussagenlogiken möglich. Weitere Informationen finden sich andere logische Kalküle unten.

Geschichte

Obwohl Propositionslogik (die mit Aussagenlogik austauschbar ist) war von früheren Philosophen angedeutet worden ist , wurde sie in eine formale Logik (entwickelt stoische Logik ) durch Chrysippus im 3. Jahrhundert vor Christus und von seinem Nachfolger erweitert Stoiker . Die Logik konzentrierte sich auf Aussagen . Diese Weiterentwicklung unterschied sich von der traditionellen syllogistischen Logik , die sich auf Begriffe konzentrierte . Die meisten Originalschriften gingen jedoch verloren und die von den Stoikern entwickelte Aussagenlogik wurde später in der Antike nicht mehr verstanden. Folglich wurde das System im 12. Jahrhundert von Peter Abaelard im Wesentlichen neu erfunden .

Die Aussagenlogik wurde schließlich mit der symbolischen Logik verfeinert . Der Mathematiker Gottfried Leibniz aus dem 17./18. Jahrhundert gilt als Begründer der symbolischen Logik für seine Arbeit mit dem Calculus ratiocinator . Obwohl sein Werk das erste seiner Art war, war es der größeren logischen Gemeinschaft unbekannt. Folglich wurden viele der von Leibniz erzielten Fortschritte von Logikern wie George Boole und Augustus De Morgan nachgebildet – völlig unabhängig von Leibniz.

So wie die Aussagenlogik als eine Weiterentwicklung der früheren syllogistischen Logik angesehen werden kann, kann auch die Prädikatenlogik von Gottlob Frege als eine Weiterentwicklung der früheren Aussagenlogik betrachtet werden. Ein Autor beschreibt die Prädikatenlogik als eine Kombination „der charakteristischen Merkmale der syllogistischen Logik und der Aussagenlogik“. Folglich leitete die Prädikatenlogik eine neue Ära in der Geschichte der Logik ein; jedoch wurden nach Frege noch Fortschritte in der Aussagenlogik gemacht, einschließlich natürlicher Deduktion , Wahrheitsbäume und Wahrheitstabellen . Die natürliche Deduktion wurde von Gerhard Gentzen und Jan ukasiewicz erfunden . Wahrheitsbäume wurden von Evert Willem Beth erfunden . Die Erfindung von Wahrheitstafeln ist jedoch von ungewisser Zuschreibung.

In den Werken von Frege und Bertrand Russell finden sich Ideen, die für die Erfindung von Wahrheitstafeln einflussreich sind. Die eigentliche Tabellenstruktur (als Tabelle formatiert) selbst wird im Allgemeinen entweder Ludwig Wittgenstein oder Emil Post (oder beiden unabhängig) zugeschrieben. Außer Frege und Russell zählen Philo, Boole, Charles Sanders Peirce und Ernst Schröder zu anderen, denen Ideen zugeschrieben werden, die Wahrheitstabellen vorausgehen . Andere, denen die tabellarische Struktur zugeschrieben wird, sind Jan ukasiewicz , Alfred North Whitehead , William Stanley Jevons , John Venn und Clarence Irving Lewis . Letztendlich sind einige, wie John Shosky, zu dem Schluss gekommen, dass "Es ist alles andere als klar, dass einer Person der Titel 'Erfinder' von Wahrheitstafeln verliehen werden sollte.".

Terminologie

Allgemein ausgedrückt ist ein Kalkül ein formales System , das aus einer Reihe von syntaktischen Ausdrücken ( wohlgeformten Formeln ), einer bestimmten Teilmenge dieser Ausdrücke (Axiome) sowie einer Reihe formaler Regeln besteht, die eine bestimmte binäre Beziehung definieren , die als logische Äquivalenz interpretiert werden , auf dem Raum der Ausdrücke.

Wenn das formale System ein logisches System sein soll , sollen die Ausdrücke als Aussagen interpretiert werden, und die Regeln, die als Inferenzregeln bekannt sind , sollen typischerweise wahrheitserhaltend sein. In dieser Einstellung können die Regeln, die Axiome enthalten können, dann verwendet werden, um Formeln abzuleiten, die wahre Aussagen repräsentieren – aus gegebenen Formeln, die wahre Aussagen repräsentieren.

Die Menge der Axiome kann leer, eine nichtleere endliche Menge oder eine abzählbar unendliche Menge sein (siehe Axiomenschema ). Eine formale Grammatik definiert rekursiv die Ausdrücke und wohlgeformten Formeln der Sprache . Zusätzlich kann eine Semantik angegeben werden, die Wahrheit und Bewertungen (oder Interpretationen ) definiert.

Die Sprache eines Aussagenkalküls besteht aus

  1. eine Reihe von primitiven Symbolen, die verschiedentlich als atomare Formeln , Platzhalter , Satzbuchstaben oder Variablen bezeichnet werden , und
  2. eine Reihe von Operatorsymbolen, die unterschiedlich als logische Operatoren oder logische Verknüpfungen interpretiert werden .

Eine wohlgeformte Formel ist jede atomare Formel oder jede Formel, die aus atomaren Formeln mit Hilfe von Operatorsymbolen nach den Regeln der Grammatik aufgebaut werden kann.

Mathematiker unterscheiden manchmal zwischen propositionalen Konstanten, propositionalen Variablen und Schemata. Aussagenkonstanten stellen eine bestimmte Aussage dar, während Aussagenvariablen über die Menge aller atomaren Aussagen reichen. Schemata reichen jedoch über alle Aussagen. Es ist üblich, propositionale Konstanten durch A , B und C darzustellen , propositionale Variablen durch P , Q und R , und schematische Buchstaben sind oft griechische Buchstaben, meistens φ , ψ und χ .

Grundlegendes Konzept

Im Folgenden wird ein Standard-Aussagenkalkül skizziert. Es gibt viele verschiedene Formulierungen, die alle mehr oder weniger gleichwertig sind, sich aber in den Details unterscheiden:

  1. ihre Sprache (dh die besondere Sammlung von primitiven Symbolen und Operatorsymbolen),
  2. die Menge von Axiomen oder ausgezeichneten Formeln, und
  3. der Satz von Inferenzregeln.

Jede gegebene Aussage kann mit einem Buchstaben dargestellt werden, der als 'Aussagenkonstante' bezeichnet wird, analog zur Darstellung einer Zahl durch einen Buchstaben in der Mathematik (zB a = 5 ). Alle Aussagen erfordern genau einen von zwei Wahrheitswerten: wahr oder falsch. Sei beispielsweise P der Satz, dass es draußen regnet. Dies ist wahr ( P ), wenn es draußen regnet, andernfalls falsch ( ¬ P ).

  • Dann definieren wir wahrheitsfunktionale Operatoren, beginnend mit der Negation. ¬ P stellt die Negation von P dar , die man sich als Verleugnung von P vorstellen kann . Im obigen Beispiel drückt ¬ P aus, dass es draußen nicht regnet, oder durch eine üblichere Lesart: "Es ist nicht der Fall, dass es draußen regnet." Wenn P wahr ist, ist ¬ P falsch; und wenn P falsch ist, ist ¬ P wahr. Folglich hat ¬ ¬ P immer den gleichen Wahrheitswert wie P .
  • Konjunktion ist ein wahrheitsfunktionales Konnektor, das einen Satz aus zwei einfacheren Sätzen bildet, zum Beispiel P und Q . Die Konjunktion von P und Q wird PQ geschrieben und drückt aus, dass beide wahr sind. Wir lesen PQ als „ P und Q “. Für zwei beliebige Aussagen gibt es vier mögliche Zuweisungen von Wahrheitswerten:
    1. P ist wahr und Q ist wahr
    2. P ist wahr und Q ist falsch
    3. P ist falsch und Q ist wahr
    4. P ist falsch und Q ist falsch
Die Konjunktion von P und Q ist im Fall 1 wahr und ansonsten falsch. Wo P die Aussage ist, dass es draußen regnet und Q die Aussage ist, dass eine Kaltfront über Kansas ist, gilt PQ , wenn es draußen regnet und es eine Kaltfront über Kansas gibt. Wenn es draußen nicht regnet, ist P ∧ Q falsch; und wenn es keine Kaltfront über Kansas gibt, dann ist auch PQ falsch.
  • Die Disjunktion ähnelt der Konjunktion insofern, als sie einen Satz aus zwei einfacheren Sätzen bildet. Wir schreiben es PQ , und es wird " P oder Q " gelesen . Es drückt aus, dass entweder P oder Q wahr ist. Somit gilt in den oben aufgeführten Fällen die Disjunktion von P mit Q in allen Fällen – außer Fall 4. Mit dem obigen Beispiel drückt die Disjunktion aus, dass es entweder draußen regnet oder über Kansas eine Kaltfront herrscht. (Beachten Sie, dass diese Verwendung der Disjunktion der Verwendung des englischen Wortes „or“ ähneln soll. Es ähnelt jedoch am meisten dem englischen einschließlich „or“, das verwendet werden kann, um die Wahrheit von mindestens einem von zwei Aussagen auszudrücken. Es ist nicht wie das englische exklusive "oder", das die Wahrheit von genau einem von zwei Aussagen ausdrückt. Mit anderen Worten, das exklusive "oder" ist falsch, wenn sowohl P als auch Q wahr sind (Fall 1). Ein Beispiel für das exklusive oder ist: Sie können einen Bagel oder ein Gebäck haben, aber nicht beides. Oft wird in natürlicher Sprache der Zusatz „aber nicht beides" weggelassen – aber nicht beides" In der Mathematik ist „oder" jedoch immer einschließend oder; wenn exklusiv oder gemeint ist, wird es angegeben, möglicherweise durch "xor".)
  • Materialbedingt verbindet auch zwei einfachere Aussagen, und wir schreiben PQ , was gelesen wird "wenn P, dann Q ". Der Satz links vom Pfeil heißt Antezedens, der Satz rechts vom Pfeil heißt Konsequenz. (Es gibt keine solche Bezeichnung für Konjunktion oder Disjunktion, da es sich um kommutative Operationen handelt.) Es drückt aus, dass Q immer dann wahr ist, wenn P wahr ist. Somit ist PQ in jedem der obigen Fälle wahr, außer im Fall 2, weil dies der einzige Fall ist, in dem P wahr ist, aber Q nicht. Im Beispiel, wenn P dann Q ausdrückt, dass es eine Kaltfront über Kansas gibt, wenn es draußen regnet. Die materielle Bedingung wird oft mit der physikalischen Kausalität verwechselt. Das materielle Konditional jedoch verbindet nur zwei Sätze durch ihre Wahrheitswerte – was nicht das Verhältnis von Ursache und Wirkung ist. In der Literatur ist umstritten, ob die materielle Implikation eine logische Kausalität darstellt.
  • Biconditional verbindet zwei einfachere Propositionen, und wir schreiben PQ , das heißt " P genau dann, wenn Q ". Es drückt aus, dass P und Q denselben Wahrheitswert haben, und zwar in den Fällen 1 und 4. ' P ist genau dann wahr, wenn Q ' wahr ist, andernfalls ist es falsch.

Es ist sehr hilfreich, sich die Wahrheitstabellen für diese verschiedenen Operatoren sowie die Methode der analytischen Tableaus anzusehen .

Schließung im laufenden Betrieb

Aussagenlogik ist unter wahrheitsfunktionalen Verknüpfungen abgeschlossen. Das heißt, für jeden Satz φ ist ¬ φ auch ein Satz. Ebenso für alle Sätze , & phgr; und ψ , & phiv;ψ ist ein Satz, und in ähnlicher Weise für die Disjunktion, bedingte und biconditional. Dies impliziert, dass zum Beispiel φψ ein Satz ist und daher mit einem anderen Satz verbunden werden kann. Um dies darzustellen, müssen wir Klammern verwenden, um anzugeben, welcher Satz mit welchem ​​verbunden ist. Zum Beispiel PQR ist keine wohlgeformte Formel, weil wir nicht wissen , ob wir Unzusammengehöriges PQ mit R oder wenn wir Unzusammengehöriges P mit QR . Somit müssen wir entweder schreiben ( PQ ) ∧ R ersterem zu repräsentieren, oder P ∧ ( QR ) die letzteren darzustellen. Durch die Auswertung der Wahrheitsbedingungen sehen wir, dass beide Ausdrücke die gleichen Wahrheitsbedingungen haben (in den gleichen Fällen wahr sein werden), und darüber hinaus, dass jeder Satz, der durch beliebige Konjunktionen gebildet wird, unabhängig von der Position der Klammern die gleichen Wahrheitsbedingungen hat. Dies bedeutet, dass die Konjunktion assoziativ ist, man sollte jedoch nicht davon ausgehen, dass Klammern niemals einen Zweck erfüllen. Zum Beispiel hat der Satz P ( QR ) nicht die gleichen Wahrheitsbedingungen von ( PQ ) R , so dass es sich um unterschiedliche Sätze handelt, die sich nur durch die Klammern unterscheiden. Dies kann durch die oben erwähnte Wahrheitstabellenmethode überprüft werden.

Anmerkung: Für eine beliebige Anzahl von Aussagenkonstanten können wir eine endliche Anzahl von Fällen bilden, die ihre möglichen Wahrheitswerte auflisten. Eine einfache Möglichkeit, dies zu erzeugen, sind Wahrheitstabellen, in die man P , Q , ..., Z für eine beliebige Liste von k Aussagenkonstanten schreibt , dh jede Liste von Aussagenkonstanten mit k Einträgen. Unter diese Liste schreibt man 2 k Zeilen, und unter P füllt man die erste Hälfte der Zeilen mit wahr (oder T) und die zweite Hälfte mit falsch (oder F). Unterhalb von Q füllt man ein Viertel der Zeilen mit T, dann ein Viertel mit F, dann ein Viertel mit T und das letzte Viertel mit F. Die nächste Spalte wechselt für jedes Achtel der Zeilen zwischen wahr und falsch, dann Sechzehntel usw., bis die letzte Aussagekonstante für jede Zeile zwischen T und F variiert. Dies ergibt eine vollständige Liste der Fälle oder Wahrheitswertzuweisungen, die für diese Aussagenkonstanten möglich sind.

Streit

Der Aussagenkalkül definiert dann ein Argument als eine Liste von Aussagen. Ein gültiges Argument ist eine Liste von Aussagen, von denen die letzte aus dem Rest folgt oder von ihm impliziert wird. Alle anderen Argumente sind ungültig. Das einfachste gültige Argument ist modus ponens , ein Beispiel dafür ist die folgende Liste von Propositionen:

Dies ist eine Liste von drei Sätzen, jede Zeile ist ein Satz und der letzte folgt aus dem Rest. Die ersten beiden Zeilen heißen Prämissen und die letzte Zeile die Konklusion. Wir sagen, dass jede Aussage C aus jeder Menge von Aussagen folgt , wenn C immer dann wahr sein muss, wenn jedes Mitglied der Menge wahr ist. Im obigen Argument gilt für jedes P und Q , wenn PQ und P wahr sind, notwendigerweise Q wahr. Beachten Sie, dass wir , wenn P wahr ist, die Fälle 3 und 4 (aus der Wahrheitstabelle) nicht berücksichtigen können. Wenn PQ wahr ist, können wir Fall 2 nicht betrachten. Es bleibt nur Fall 1, in dem auch Q wahr ist. Somit ist Q durch die Prämissen impliziert.

Dies verallgemeinert schematisch. Wo also φ und ψ beliebige Aussagen sein können,

Andere Argumentformen sind praktisch, aber nicht notwendig. Bei einer vollständigen Menge von Axiomen (siehe unten für eine solche Menge) reicht modus ponens aus, um alle anderen Argumentformen in der Aussagenlogik zu beweisen, sie können also als Ableitungen betrachtet werden. Beachten Sie, dass dies nicht für die Erweiterung der Aussagenlogik auf andere Logiken wie die Logik erster Ordnung gilt . Die Logik erster Ordnung erfordert mindestens eine zusätzliche Inferenzregel, um Vollständigkeit zu erhalten .

Die Bedeutung von Argumenten in der formalen Logik besteht darin, dass man aus etablierten Wahrheiten neue Wahrheiten gewinnen kann. Im ersten obigen Beispiel ist die Wahrheit von Q unter den gegebenen beiden Prämissen noch nicht bekannt oder angegeben. Nach dem Argument wird Q abgeleitet. Auf diese Weise definieren wir ein Deduktionssystem als eine Menge aller Aussagen, die aus einer anderen Menge von Aussagen abgeleitet werden können. Zum Beispiel kann die Reihe von Sätzen gegeben , können wir einen Abzug System definieren Γ , die die Menge aller Sätze, die aus folgen A . Wiederholung wird immer vorausgesetzt, also . Auch aus dem ersten Element von A , dem letzten Element sowie dem Modus ponens ist R eine Konsequenz und so . Da wir jedoch keine ausreichend vollständigen Axiome aufgenommen haben, kann nichts anderes abgeleitet werden. Obwohl also die meisten in der Aussagenlogik untersuchten Deduktionssysteme in der Lage sind, zu deduzieren , ist dieses zu schwach, um einen solchen Satz zu beweisen.

Generische Beschreibung eines Aussagenkalküls

Ein Aussagenkalkül ist ein formales System , wobei:

  • Die Alpha-Menge ist eine abzählbar unendliche Menge von Elementen, die als Propositionssymbole oder Propositionsvariablen bezeichnet werden . Syntaktisch gesehen sind dies die grundlegendsten Elemente der formalen Sprache , die auch als atomare Formeln oder terminale Elemente bezeichnet werden . In den folgenden Beispielen sind die Elemente von typischerweise die Buchstaben p , q , r usw.
  • Das Omega - Set Ω ist eine endliche Menge von Elementen genannt Operator Symbole oder logische Verknüpfungen . Die Menge Ω ist aufgeteilt in getrennte Sub - Sätze wie folgt:

    In dieser Partition ist die Menge von Operatorsymbolen der Stelligkeit j .

    In den bekannteren Aussagenkalkülen wird Ω typischerweise wie folgt partitioniert:

    Eine häufig übernommene Konvention behandelt die konstanten logischen Werte als Operatoren der Stelligkeit Null, also:

    Einige Autoren verwenden die Tilde (~) oder N anstelle von ¬ ; und einige verwenden v statt sowie das kaufmännische Und (&), das vorangestellte K oder statt . Die Notation variiert noch stärker für den Satz logischer Werte, wobei Symbole wie {false, true}, {F, T} oder {0, 1} alle in verschiedenen Kontexten anstelle von gesehen werden .
  • Die Zeta-Menge ist eine endliche Menge von Transformationsregeln , die als Inferenzregeln bezeichnet werden, wenn sie logische Anwendungen erwerben.
  • Die Iota-Menge ist eine abzählbare Menge von Anfangspunkten , die Axiome genannt werden, wenn sie logische Interpretationen erhalten.

Die Sprache von , auch bekannt als Formelmenge , wohlgeformte Formeln , wird induktiv durch die folgenden Regeln definiert:

  1. Basis: Jedes Element des Alpha-Sets ist eine Formel von .
  2. Wenn Formeln sind und in ist , dann ist eine Formel.
  3. Geschlossen: Nichts anderes ist eine Formel von .

Die wiederholte Anwendung dieser Regeln erlaubt die Konstruktion komplexer Formeln. Zum Beispiel:

  • Nach Regel 1 ist p eine Formel.
  • Nach Regel 2 ist eine Formel.
  • Nach Regel 1 ist q eine Formel.
  • Nach Regel 2 ist eine Formel.

Beispiel 1. Einfaches Axiomensystem

Seien , wobei , , , wie folgt definiert:

  • Die Alpha-Menge ist eine abzählbar unendliche Menge von Symbolen, zum Beispiel:
  • Von den drei Konnektoren für Konjunktion, Disjunktion und Implikation ( , und ) kann einer als primitiv aufgefasst werden, und die anderen beiden können in Begriffen davon und Negation ( ¬ ) definiert werden. Alle logischen Verknüpfungen können im Sinne eines einzigen hinreichenden Operators definiert werden . Das Bikonditional ( ) kann natürlich in Bezug auf Konjunktion und Implikation definiert werden , wobei definiert als .
    Die Annahme von Negation und Implikation als die beiden primitiven Operationen eines Aussagenkalküls ist gleichbedeutend damit, die Omega-Mengen- Partition wie folgt zu haben:
  • Ein von Jan Łukasiewicz vorgeschlagenes Axiomensystem , das als Aussagenkalkül-Teil eines Hilbert-Systems verwendet wird , formuliert einen Aussagenkalkül in dieser Sprache wie folgt. Die Axiome sind alle Substitutionsinstanzen von:
  • Die Inferenzregel ist modus ponens (dh aus p und , infer q ). Dann ist definiert als , und ist definiert als . Dieses System wird in der formalen Beweisdatenbank Metamath set.mm verwendet.

Beispiel 2. Natürliches Deduktionssystem

Seien , wobei , , , wie folgt definiert:

  • Die Alpha-Menge ist eine abzählbar unendliche Menge von Symbolen, zum Beispiel:
  • Die Omega-Set- Partitionen wie folgt:

Im folgenden Beispiel eines Aussagenkalküls sollen die Transformationsregeln als Inferenzregeln eines sogenannten natürlichen Deduktionssystems interpretiert werden . Das hier vorgestellte spezielle System hat keine Anfangspunkte, was bedeutet, dass seine Interpretation für logische Anwendungen seine Theoreme aus einer leeren Axiomenmenge ableitet .

  • Die Menge der Anfangspunkte ist leer, d. h. .
  • Der Satz von Transformationsregeln, , wird wie folgt beschrieben:

Unser Aussagenkalkül hat elf Inferenzregeln. Diese Regeln ermöglichen es uns, andere wahre Formeln abzuleiten, wenn eine Menge von Formeln gegeben ist, von denen angenommen wird, dass sie wahr sind. Die ersten zehn besagen einfach, dass wir bestimmte wohlgeformte Formeln von anderen wohlgeformten Formeln ableiten können. Die letzte Regel verwendet jedoch hypothetische Argumentation in dem Sinne, dass wir in der Prämisse der Regel vorübergehend eine (unbewiesene) Hypothese als Teil der Menge der abgeleiteten Formeln annehmen, um zu sehen, ob wir eine bestimmte andere Formel ableiten können. Da die ersten zehn Regeln dies nicht tun, werden sie normalerweise als nicht-hypothetische Regeln und die letzte als hypothetische Regel beschrieben.

Bei der Beschreibung der Transformationsregeln können wir ein metasprachliches Symbol einführen . Es ist im Grunde eine bequeme Abkürzung, um "das folgern" zu sagen. Das Format ist , wobei Γ eine (möglicherweise leere) Menge von Formeln ist, die Prämissen genannt werden, und ψ eine Formel namens Konklusion. Die Transformationsregel besagt, dass, wenn jeder Satz in Γ ein Satz ist (oder denselben Wahrheitswert wie die Axiome hat), auch ψ ein Satz ist. Beachten Sie, dass wir unter Berücksichtigung der folgenden Regel Konjunktionseinführung wissen, wann immer Γ mehr als eine Formel hat, wir sie immer sicher mit Hilfe von Konjunktionen in eine Formel reduzieren können. Kurz gesagt können wir von diesem Zeitpunkt an Γ als eine Formel anstelle einer Menge darstellen. Eine weitere Auslassung aus Bequemlichkeitsgründen ist, wenn Γ eine leere Menge ist, in welchem ​​Fall Γ möglicherweise nicht erscheint.

Verneinungseinleitung
Aus und folgern .
Das heißt, .
Negation Elimination
Von , folgern .
Das heißt, .
Eliminierung der Doppelnegation
Aus , entnehmen Sie S .
Das heißt, .
Konjunktionseinführung
Aus p und q folgern .
Das heißt, .
Konjunktionsbeseitigung
Aus , entnehmen Sie S .
Von , folge q .
Das heißt, und .
Einführung in die Disjunktion
Aus p folgern .
Aus q folgern .
Das heißt, und .
Disjunktionsbeseitigung
Von und und leite r ab .
Das heißt, .
Biconditional Einführung
Aus und folgern .
Das heißt, .
Bibedingte Elimination
Von , folgern .
Von , folgern .
Das heißt, und .
Modus ponens (bedingte Eliminierung)
Aus p und folge q .
Das heißt, .
Bedingter Beweis (bedingte Einführung)
Aus [das Akzeptieren von p erlaubt einen Beweis von q ], folgern Sie .
Das heißt, .

Grundlegende und abgeleitete Argumentationsformen

Name Sequenz Beschreibung
Modus Ponens Wenn p dann q ; p ; daher q
Modus Tollens Wenn p dann q ; nicht q ; daher nicht p
Hypothetischer Syllogismus Wenn p dann q ; wenn q dann r ; also, wenn p dann r
Disjunktiver Syllogismus Entweder p oder q oder beides; nicht p ; daher q
Konstruktives Dilemma Wenn p dann q ; und wenn r dann s ; aber p oder r ; also q oder s
Zerstörerisches Dilemma Wenn p dann q ; und wenn r dann s ; aber nicht q oder nicht s ; also nicht p oder nicht r
Bidirektionales Dilemma Wenn p dann q ; und wenn r dann s ; aber p oder nicht s ; also q oder nicht r
Vereinfachung p und q sind wahr; daher ist p wahr
Verbindung p und q sind getrennt wahr; daher sind sie gemeinsam wahr
Zusatz p ist wahr; daher ist die Disjunktion ( p oder q ) wahr
Komposition Wenn p dann q ; und wenn p dann r ; also wenn p wahr ist, dann sind q und r wahr
Satz von De Morgan (1) Die Negation von ( p und q ) ist äquiv. zu (nicht p oder nicht q )
Satz von De Morgan (2) Die Negation von ( p oder q ) ist äquiv. zu (nicht p und nicht q )
Kommutierung (1) ( p oder q ) ist äquiv. zu ( q oder p )
Kommutierung (2) ( p und q ) ist äquiv. zu ( q und p )
Kommutierung (3) ( p ist äquivalent zu q ) ist äquivalent. zu ( q ist gleich p )
Verein (1) p oder ( q oder r ) ist äquivalent. zu ( p oder q ) oder r
Verein (2) p und ( q und r ) ist äquiv. zu ( p und q ) und r
Verteilung (1) p und ( q oder r ) ist äquivalent. zu ( p und q ) oder ( p und r )
Verteilung (2) p oder ( q und r ) ist äquivalent. zu ( p oder q ) und ( p oder r )
Doppelte Negation und p ist äquivalent zur Negation von not p
Umsetzung Wenn p dann ist q äquiv. zu wenn nicht q dann nicht p
Wesentliche Auswirkungen Wenn p dann ist q äquiv. nicht p oder q
Materialäquivalenz (1) ( p iff q ) ist äquiv. zu (wenn p wahr ist, dann ist q wahr) und (wenn q wahr ist, ist p wahr)
Materialäquivalenz (2) ( p iff q ) ist äquiv. entweder ( p und q sind wahr) oder (sowohl p als auch q sind falsch)
Materialäquivalenz (3) ( p iff q ) ist gleichbedeutend mit, beides ( p oder nicht q ist wahr) und (nicht p oder q ist wahr)
Ausfuhr aus (wenn p und q wahr sind, dann ist r wahr) können wir beweisen (wenn q wahr ist, dann ist r wahr, wenn p wahr ist)
Einfuhr Wenn p dann (wenn q dann r ) ist äquivalent zu wenn p und q dann r
Tautologie (1) p ist wahr ist äquiv. to p ist wahr oder p ist wahr
Tautologie (2) p ist wahr ist äquiv. zu p ist wahr und p ist wahr
Tertium non datur (Gesetz der ausgeschlossenen Mitte) p oder nicht p ist wahr
Gesetz der Widerspruchsfreiheit p und nicht p falsch ist, ist eine wahre Aussage

Beweise in der Aussagenlogik

Eine der Hauptanwendungen eines Aussagenkalküls, wenn er für logische Anwendungen interpretiert wird, besteht darin, Beziehungen logischer Äquivalenz zwischen Aussagenformeln zu bestimmen. Diese Zusammenhänge werden mit Hilfe der verfügbaren Transformationsregeln ermittelt, deren Folgen Ableitungen oder Beweise genannt werden .

In der folgenden Diskussion wird ein Beweis als Folge nummerierter Zeilen präsentiert, wobei jede Zeile aus einer einzelnen Formel besteht, gefolgt von einem Grund oder einer Begründung für die Einführung dieser Formel. Jede Prämisse des Arguments, dh eine als Hypothese des Arguments eingeführte Annahme, wird am Anfang der Sequenz aufgeführt und anstelle anderer Begründungen als "Prämisse" gekennzeichnet. Die Schlussfolgerung ist in der letzten Zeile aufgeführt. Ein Beweis ist vollständig, wenn jede Zeile durch die richtige Anwendung einer Transformationsregel aus der vorherigen folgt. (Für einen kontrastierenden Ansatz siehe Beweisbäume ).

Beispiel für einen Beweis im natürlichen Deduktionssystem

  • Zu zeigen, dass AA .
  • Ein möglicher Beweis dafür (der zwar gültig ist, aber zufällig mehr Schritte enthält als nötig) kann wie folgt arrangiert werden:
Beispiel für einen Beweis
Nummer Formel Grund
1 Prämisse
2 Aus ( 1 ) durch Disjunktionseinleitung
3 Aus ( 1 ) und ( 2 ) durch Konjunktionseinleitung
4 Aus ( 3 ) durch Konjunktionsbeseitigung
5 Zusammenfassung von ( 1 ) bis ( 4 )
6 Aus ( 5 ) durch bedingten Beweis

Interpretieren Sie als " A angenommen , A abgeleitet ". Lesen Sie, wie „Unter der Annahme nichts, daraus schließen , dass A bedeutet , A “, oder „Es ist eine Tautologie , dass A bedeutet , A “, oder „Es ist immer wahr , dass A bedeutet , A “.

Beispiel für einen Beweis in einem klassischen Aussagensystem

Wir beweisen nun den gleichen Satz in dem oben beschriebenen axiomatischen System von Jan Łukasiewicz , das ein Beispiel für ein klassisches Aussagenkalkülsystem oder ein deduktives System nach Hilbert-Art für Aussagenkalkül ist.

Die Axiome sind:

(A1)
(A2)
(A3)

Und der Beweis ist wie folgt:

  1.       (Beispiel von (A1))
  2.       (Beispiel von (A2))
  3.       (aus (1) und (2) von modus ponens )
  4.       (Beispiel von (A1))
  5.       (aus (4) und (3) von modus ponens)

Korrektheit und Vollständigkeit der Regeln

Die entscheidenden Eigenschaften dieses Regelwerks sind, dass es solide und vollständig ist . Informell bedeutet dies, dass die Regeln korrekt sind und keine anderen Regeln erforderlich sind. Diese Ansprüche können wie folgt formaler formuliert werden. Beachten Sie, dass die Beweise für die Richtigkeit und Vollständigkeit der Aussagenlogik selbst keine Beweise in der Aussagenlogik sind; Dies sind Theoreme in ZFC, die als Metatheorie verwendet werden , um Eigenschaften der Aussagenlogik zu beweisen.

Wir definieren eine Wahrheitszuweisung als eine Funktion , die propositionale Variablen auf wahr oder falsch abbildet . Informell kann eine solche Wahrheitszuordnung als Beschreibung eines möglichen Sachverhalts (oder einer möglichen Welt ) verstanden werden, bei dem bestimmte Aussagen wahr sind und andere nicht. Die Semantik von Formeln kann dann formalisiert werden, indem definiert wird, für welchen "Sachstand" sie als wahr gelten, was durch die folgende Definition geschieht.

Wir definieren, wann eine solche Wahrheitszuordnung A eine bestimmte wohlgeformte Formel mit den folgenden Regeln erfüllt :

  • A erfüllt die Aussagenvariable P genau dann, wenn A ( P ) = wahr
  • A erfüllt ¬ φ genau dann, wenn A nicht φ
  • A erfüllt ( φψ ) genau dann, wenn A sowohl φ als auch ψ . erfüllt
  • A erfüllt ( φψ ) genau dann, wenn A mindestens entweder φ oder ψ . erfüllt
  • A erfüllt ( φψ ) genau dann, wenn A nicht erfüllt φ aber nicht ψ
  • A erfüllt ( φψ ) genau dann, wenn A sowohl φ als auch ψ erfüllt oder keines von beiden erfüllt

Mit dieser Definition können wir nun formalisieren, was es bedeutet, dass eine Formel φ durch eine bestimmte Menge S von Formeln impliziert wird . Informell gilt dies, wenn in allen möglichen Welten mit der Formelmenge S auch die Formel φ gilt. Dies führt zu folgender formalen Definition: Wir sagen, dass eine Menge S wohlgeformter Formeln semantisch eine bestimmte wohlgeformte Formel φ impliziert (oder impliziert ), wenn alle Wahrheitszuweisungen, die alle Formeln in S erfüllen, auch φ erfüllen .

Schließlich definieren wir die syntaktische Folgerung so, dass φ genau dann von S syntaktisch zur Folge hat, wenn wir sie mit den oben vorgestellten Inferenzregeln in endlich vielen Schritten ableiten können. Dies ermöglicht es uns, genau zu formulieren, was es bedeutet, dass der Satz von Inferenzregeln solide und vollständig ist:

Korrektheits: Wenn der Satz von wohlgeformten Formeln S syntaktisch bringt die wohlgeformte Formel φ dann S semantisch bringt φ .

Vollständigkeits: Wenn der Satz von wohlgeformten Formeln S semantisch beinhaltet die wohlgeformte Formel φ dann S syntaktisch Entails φ .

Für das obige Regelwerk ist dies tatsächlich der Fall.

Skizze eines Dichtheitsnachweises

(Für die meisten logischen Systeme ist dies die vergleichsweise "einfache" Beweisrichtung)

Notationskonventionen: Sei G eine Variable, die sich über Sätze von Sätzen erstreckt. Lassen Sie A, B und C über Sätze reichen. Für „ G folgt syntaktisch A “ schreiben wir „ G beweist A “. Für „ G semantisch bringt ein “ wir „schreiben G impliziert A “.

Wir wollen zeigen: ( A )( G ) (wenn G A beweist , dann folgt aus G A ).

Wir bemerken, dass " G beweist A " eine induktive Definition hat, und das gibt uns die unmittelbaren Ressourcen, um Behauptungen der Form "Wenn G beweist A , dann ..." zu demonstrieren . Unser Beweis verläuft also per Induktion.

  1. Basis. Zeigen Sie : Wenn ein Mitglied ist G , dann G impliziert A .
  2. Basis. Zeigen Sie : Wenn A ein Axiom ist, dann G impliziert A .
  3. Induktionsschritt (Induktion über n , die Länge des Beweises):
    1. Nehmen Sie für beliebiges G und A an, dass, wenn G A in n oder weniger Schritten beweist , G impliziert A .
    2. Zeigen Sie für jede mögliche Anwendung einer Inferenzregel in Schritt n + 1 , die zu einem neuen Satz B führt, dass G B impliziert .

Beachten Sie, dass Basisschritt II für natürliche Deduktionssysteme weggelassen werden kann, da sie keine Axiome haben. Wenn Schritt II verwendet wird, muss gezeigt werden, dass jedes der Axiome eine (semantische) logische Wahrheit ist .

Die Basisschritte zeigen, dass die einfachsten beweisbaren Sätze aus G auch von G für jedes G impliziert werden . (Der Beweis ist einfach, da die semantische Tatsache, dass eine Menge eines ihrer Mitglieder impliziert, ebenfalls trivial ist.) Der induktive Schritt wird systematisch alle weiteren Sätze abdecken, die beweisbar sein könnten – indem wir jeden Fall betrachten, in dem wir zu einer logischen Schlussfolgerung kommen könnten mit einer Inferenzregel – und zeigt, dass ein neuer Satz, wenn er beweisbar ist, auch logisch impliziert ist. (Zum Beispiel könnten wir eine Regel haben, die uns sagt, dass wir aus " A " " A oder B " ableiten können . In III.a nehmen wir an, dass, wenn A beweisbar ist, es impliziert ist. Wir wissen auch, dass, wenn A beweisbar ist, dann " A oder B " ist beweisbar. Wir müssen zeigen, dass dann auch " A oder B " impliziert ist. Wir tun dies unter Berufung auf die semantische Definition und die soeben gemachte Annahme. A ist aus G beweisbar , nehmen wir an. Es ist also auch durch G impliziert . Also macht jede semantische Bewertung, die alles G wahr macht, A wahr. Aber jede Bewertung, die A wahr macht, macht " A oder B " wahr, durch die definierte Semantik für "oder". Also jede Bewertung, die alles G wahr macht macht " A oder B " wahr. Also ist " A oder B " impliziert.) Im Allgemeinen besteht der Induktionsschritt aus einer langen, aber einfachen Einzelfallanalyse aller Schlußregeln, die zeigt, dass jede die Semantik "beibehält". Implikation.

Nach der Definition der Beweisbarkeit gibt es keine anderen beweisbaren Sätze, als dass sie ein Mitglied von G , ein Axiom sind oder einer Regel folgen; Wenn also all dies semantisch impliziert ist, ist der Deduktionskalkül stichhaltig.

Skizze des Vollständigkeitsnachweises

(Dies ist normalerweise die viel schwierigere Beweisrichtung.)

Wir verwenden die gleichen Notationskonventionen wie oben.

Wir wollen zeigen: Wenn aus G A folgt , dann beweist G A . Wir gehen durch Kontraposition : Wir zeigen stattdessen , dass , wenn G nicht nicht beweisen A dann G ist nicht impliziert A . Wenn wir zeigen, dass es ein Modell gibt, in dem A nicht gilt, obwohl G wahr ist, dann impliziert G offensichtlich nicht A . Die Idee ist, ein solches Modell aus unserer Annahme zu bauen, dass G nicht A beweist .

  1. G beweist A nicht . (Annahme)
  2. Wenn G nicht beweisen A , dann können wir eine (unendliche) konstruieren Maximal Set , G * , die eine Obermenge ist G und die auch nicht beweisen , A .
    1. Ordnen Sie alle Sätze in der Sprache (mit dem Ordnungstyp ω) an (z. B. die kürzesten zuerst und die gleich langen in erweiterter alphabetischer Reihenfolge) und nummerieren Sie sie ( E 1 , E 2 , ...)
    2. Definiere eine Reihe G n von Mengen ( G 0 , G 1 , ...) induktiv:
      1. Wenn A beweist , dann
      2. Wenn sie nicht beweisen , A , dann
    3. Definiere G als Vereinigung aller G n . (Das heißt, G ist die Menge aller Sätze, die in jedem G n vorkommen .)
    4. Das lässt sich leicht zeigen
      1. G enthält (ist eine Obermenge von) G (nach (bi));
      2. G beweist A nicht (weil der Beweis nur endlich viele Sätze enthalten würde und wenn der letzte von ihnen in einem G n eingeführt wird, würde G n A entgegen der Definition von G n beweisen); und
      3. G * ist ein MaximalSatz in Bezug auf A : Sollte mehr Sätzewas hinzugefügt wurde G * , würde es beweisen , A . (Denn wenn es möglich wäre, weitere Sätze hinzuzufügen, hätten sie hinzugefügt werden sollen, als sie während der Konstruktion des G n angetroffen wurden, wiederum per Definition)
  3. Wenn G eine maximale Menge bezüglich A ist , dann ist sie wahrheitsähnlich . Das bedeutet, dass es C genau dann enthält, wenn es kein ¬C enthält ; Wenn es C enthält und "If C then B " enthält, dann enthält es auch B ; und so weiter. Um dies zu zeigen, muss man zeigen, dass das axiomatische System stark genug ist für Folgendes:
    • Für alle Formeln C und D , wenn es sowohl beweist C und ¬C , dann erweist es sich D . Daraus folgt, dass eine Maximalmenge bezüglich A nicht sowohl C als auch ¬C beweisen kann , da sie sonst A beweisen würde .
    • Wenn für alle Formeln C und D sowohl CD als auch ¬CD beweist, dann beweist es D . Dies wird zusammen mit dem Deduktionssatz verwendet , um zu zeigen, dass für jede Formel entweder sie oder ihre Negation in G ∗ ist : Sei B eine Formel, die nicht in G ∗ ist ; dann beweist G mit der Addition von B A . Aus dem Deduktionssatz folgt also, dass G BA beweist . Aber nehmen wir an ¬B waren auch nicht in G * , dann mit der gleichen Logik G * auch beweist ¬BA ; aber dann beweist G A , das wir bereits als falsch gezeigt haben.
    • Für alle Formeln C und D gilt , wenn sie C und D beweist, dann beweist sie CD .
    • Für alle Formeln C und D gilt , wenn C und ¬D bewiesen sind , dann beweist es ¬( CD ).
    • Für alle Formeln C und D gilt: Wenn ¬C beweist , dann beweist es CD .
    Wenn zusätzliche logische Operationen (wie Konjunktion und/oder Disjunktion) ebenfalls Teil des Vokabulars sind, dann gibt es zusätzliche Anforderungen an das axiomatische System (zB dass, wenn es C und D beweist , es auch ihre Konjunktion beweisen würde).
  4. Wenn G wahrheitsähnlich ist, gibt es eine G -kanonische Bewertung der Sprache: eine, die jeden Satz in G wahr und alles außerhalb von G falsch macht, während sie dennoch den Gesetzen der semantischen Zusammensetzung in der Sprache gehorcht. Beachten Sie, dass die Voraussetzung, dass es wahrheitsähnlich ist, erforderlich ist, um zu garantieren, dass die Gesetze der semantischen Zusammensetzung in der Sprache durch diese Wahrheitszuweisung erfüllt werden.
  5. Eine G -kanonische Bewertung macht unsere ursprüngliche Menge G alle wahr und A falsch.
  6. Wenn es eine Bewertung gibt, bei der G wahr und A falsch ist, dann impliziert G (semantisch) nicht A .

Somit ist jedes System, das modus ponens als Inferenzregel hat und die folgenden Sätze (einschließlich ihrer Ersetzungen) beweist, vollständig:

  • p → (¬p → q)
  • (p → q) → ((¬p → q) → q)
  • p → (q → (p → q))
  • p → (¬q → ¬(p → q))
  • ¬p → (p → q)
  • p → p
  • p → (q → p)
  • (p → (q → r)) → ((p → q) → (p → r))

Die ersten fünf werden verwendet, um die fünf Bedingungen in Stufe III oben zu erfüllen, und die letzten drei zum Beweis des Deduktionssatzes.

Beispiel

Als Beispiel kann gezeigt werden, dass wie jede andere Tautologie die drei zuvor beschriebenen Axiome des klassischen Aussagenkalkülsystems in jedem System bewiesen werden können, das das Obige erfüllt, nämlich das Modus ponens als Inferenzregel hat und das Obige beweist acht Theoreme (einschließlich ihrer Ersetzungen). Von den acht Sätzen sind die letzten beiden zwei der drei Axiome; auch das dritte Axiom, , kann bewiesen werden, wie wir nun zeigen.

Für den Beweis können wir den hypothetischen Syllogismussatz (in der für dieses axiomatische System relevanten Form) verwenden, da er sich nur auf die beiden Axiome stützt, die bereits in der obigen Menge von acht Sätzen enthalten sind. Der Beweis lautet dann wie folgt:

  1.       (Instanz des 7. Satzes)
  2.       (Instanz des 7. Satzes)
  3.       (aus (1) und (2) von modus ponens)
  4.       (Beispiel des hypothetischen Syllogismussatzes)
  5.       (Instanz des 5. Satzes)
  6.       (aus (5) und (4) von modus ponens)
  7.       (Instanz des 2. Satzes)
  8.       (Instanz des 7. Satzes)
  9.       (aus (7) und (8) von modus ponens)
  10.       (Instanz des 8. Satzes)
  11.       (aus (9) und (10) von modus ponens)
  12.       (aus (3) und (11) von modus ponens)
  13.       (Instanz des 8. Satzes)
  14.       (von (12) und (13) von modus ponens)
  15.       (aus (6) und (14) von modus ponens)

Vollständigkeitsprüfung für das klassische Aussagensystem

Wir verifizieren nun, dass das zuvor beschriebene klassische Aussagenkalkül-System tatsächlich die oben genannten erforderlichen acht Sätze beweisen kann. Wir verwenden mehrere hier bewiesene Lemmata :

(DN1) - Doppelnegation (eine Richtung)
(DN2) - Doppelnegation (andere Richtung)
(HS1) - eine Form des hypothetischen Syllogismus
(HS2) - eine andere Form des hypothetischen Syllogismus
(TR1) - Umsetzung
(TR2) - eine andere Form der Umsetzung.
(L1)
(L3)

Wir verwenden auch die Methode des hypothetischen Syllogismus-Metatheorems als Kurzform für mehrere Beweisschritte.

  • p → (¬p → q) - Beweis:
    1.       (Beispiel von (A1))
    2.       (Instanz von (TR1))
    3.       (aus (1) und (2) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
    4.       (Beispiel von (DN1))
    5.       (Instanz von (HS1))
    6.       (aus (4) und (5) mit modus ponens)
    7.       (aus (3) und (6) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
  • (p → q) → ((¬p → q) → q) - Beweis:
    1.       (Instanz von (HS1))
    2.       (Instanz von (L3))
    3.       (Instanz von (HS1))
    4.       (aus (2) und (3) nach modus ponens)
    5.       (aus (1) und (4) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
    6.       (Instanz von (TR2))
    7.       (Instanz von (HS2))
    8.       (aus (6) und (7) mit modus ponens)
    9.       (aus (5) und (8) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
  • p → (q → (p → q)) - Beweis:
    1.       (Beispiel von (A1))
    2.       (Beispiel von (A1))
    3.       (aus (1) und (2) mit modus ponens)
  • p → (¬q → ¬(p → q)) - Beweis:
    1.       (Instanz von (L1))
    2.       (Instanz von (TR1))
    3.       (aus (1) und (2) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
  • ¬p → (p → q) - Beweis:
    1.       (Beispiel von (A1))
    2.       (Beispiel von (A3))
    3.       (aus (1) und (2) unter Verwendung des hypothetischen Syllogismus-Metatheorems)
  • p → p - Beweis im obigen Beweisbeispiel
  • p → (q → p) - Axiom (A1)
  • (p → (q → r)) → ((p → q) → (p → r)) - Axiom (A2)

Noch eine Gliederung für einen Vollständigkeitsnachweis

Wenn eine Formel eine Tautologie ist , dann gibt es dafür eine Wahrheitstabelle , die zeigt, dass jede Bewertung den Wert wahr für die Formel ergibt. Betrachten Sie eine solche Bewertung. Zeigen Sie durch mathematische Induktion über die Länge der Teilformeln, dass die Wahrheit oder Falschheit der Teilformel aus der Wahrheit oder Falschheit (je nach Bewertung) jeder Aussagevariablen in der Teilformel folgt. Kombinieren Sie dann die Zeilen der Wahrheitstabelle jeweils zu zweit, indem Sie "( P ist wahr impliziert S ) impliziert (( P ist falsch impliziert S ) impliziert S )". Wiederholen Sie dies, bis alle Abhängigkeiten von Aussagenvariablen beseitigt sind. Das Ergebnis ist, dass wir die gegebene Tautologie bewiesen haben. Da jede Tautologie beweisbar ist, ist die Logik vollständig.

Interpretation eines wahrheitsfunktionalen Aussagenkalküls

Eine Interpretation einer wahrheitsfunktionalen Aussagenlogik ist eine Zuordnung zu jedem propositionaler Symbol von der einen oder der anderen (aber nicht beide) der Wahrheitswerte Wahrheit ( T ) und Falschen ( F ) und eine Zuordnung zu den Binde - Symbole von der ihre üblichen wahrheitsfunktionalen Bedeutungen. Eine Interpretation eines wahrheitsfunktionalen Aussagenkalküls kann auch in Form von Wahrheitstabellen ausgedrückt werden .

Für verschiedene Aussagensymbole gibt es verschiedene mögliche Interpretationen. Für ein bestimmtes Symbol gibt es beispielsweise mögliche Interpretationen:

  1. wird T zugewiesen , oder
  2. ist F zugeordnet .

Für das Paar , gibt es mögliche Interpretationen:

  1. beide sind mit T belegt ,
  2. beide sind mit F belegt ,
  3. wird T zugewiesen und wird F zugewiesen , oder
  4. wird F zugewiesen und wird T zugewiesen .

Da hat , das heißt, abzählbar viele Voraussetzungssymbole gibt es , und daher unzählbar viele verschiedene mögliche Interpretationen .

Interpretation eines Satzes der wahrheitsfunktionalen Aussagenlogik

Wenn φ und ψ sind Formeln von und ist eine Interpretation dann gelten die folgenden Definitionen:

  • Ein Satz der Aussagenlogik ist unter einer Interpretation wahr, wenn diesem Satz der Wahrheitswert T zugewiesen wird. Wenn ein Satz unter einer Interpretation wahr ist , dann wird diese Interpretation als Modell dieses Satzes bezeichnet.
  • φ ist unter einer Interpretation falsch, wenn φ unter nicht wahr ist .
  • Ein Satz der Aussagenlogik ist logisch gültig, wenn er unter jeder Interpretation wahr ist.
    φ bedeutet, dass φ logisch gültig ist.
  • Ein Satz ψ der Aussagenlogik ist eine semantische Konsequenz eines Satzes φ, wenn es keine Interpretation gibt, unter der φ wahr und ψ falsch ist.
  • Ein Satz der Aussagenlogik ist konsistent, wenn er unter mindestens einer Interpretation wahr ist. Es ist inkonsistent, wenn es nicht konsistent ist.

Einige Konsequenzen dieser Definitionen:

  • Für jede gegebene Interpretation ist eine gegebene Formel entweder wahr oder falsch.
  • Keine Formel ist bei derselben Interpretation sowohl wahr als auch falsch.
  • φ ist für eine gegebene Interpretation falsch, wenn für diese Interpretation wahr ist; und φ unter einer Interpretation wahr ist, wenn unter dieser Interpretation falsch ist.
  • Wenn φ und beide unter einer gegebenen Interpretation wahr sind, dann ist ψ unter dieser Interpretation wahr.
  • Wenn und , dann .
  • ist wahr unter genau dann, wenn φ unter nicht wahr ist .
  • ist wahr unter genau dann, wenn entweder φ unter nicht wahr ist oder ψ unter wahr ist .
  • Ein Satz ψ der Aussagenlogik ist eine semantische Folge eines Satzes φ iff ist logisch gültig , das heißt, iff .

Alternativrechnung

Es ist möglich, eine andere Version der Aussagenkalküle zu definieren, die den Großteil der Syntax der logischen Operatoren mit Hilfe von Axiomen definiert und die nur eine Inferenzregel verwendet.

Axiome

Seien φ , χ und ψ für wohlgeformte Formeln. (Die wohlgeformten Formeln selbst würden keine griechischen Buchstaben enthalten, sondern nur römische Großbuchstaben, Verknüpfungsoperatoren und Klammern.) Dann lauten die Axiome wie folgt:

Axiome
Name Axiom-Schema Beschreibung
DANN-1 Hypothese hinzufügen χ , Implikationseinleitung
DANN-2 Verteile Hypothese über Implikation
UND 1 Konjunktion eliminieren
UND 2  
UND-3 Konjunktion einführen
ODER-1 Disjunktion einführen
ODER-2  
ODER-3 Disjunktion beseitigen
NICHT-1 Verneinung einführen
NICHT-2 Negation beseitigen
NICHT-3 Ausgeschlossene mittlere, klassische Logik
IFF-1 Äquivalenz eliminieren
IFF-2  
IFF-3 Äquivalenz einführen
  • Axiom THEN-2 kann als eine "Verteilungseigenschaft der Implikation in Bezug auf die Implikation" angesehen werden.
  • Axiome AND-1 und AND-2 entsprechen der "Konjunktionsbeseitigung". Die Beziehung zwischen AND-1 und AND-2 spiegelt die Kommutativität des Konjunktionsoperators wider.
  • Axiom AND-3 entspricht "Konjunktionseinführung".
  • Die Axiome OR-1 und OR-2 entsprechen der "Disjunktionseinführung". Die Beziehung zwischen OR-1 und OR-2 spiegelt die Kommutativität des Disjunktionsoperators wider.
  • Axiom NOT-1 entspricht "reductio ad absurdum".
  • Axiom NOT-2 sagt, dass "alles aus einem Widerspruch abgeleitet werden kann".
  • Axiom NOT-3 heißt " tertium non-datur " ( lateinisch : "ein Drittel ist nicht gegeben") und spiegelt die semantische Bewertung von aussagenden Formeln wider: Eine Formel kann einen Wahrheitswert von entweder wahr oder falsch haben. Es gibt keinen dritten Wahrheitswert, zumindest nicht in der klassischen Logik. Intuitionistische Logiker akzeptieren das Axiom NOT-3 nicht .

Inferenzregel

Die Inferenzregel ist modus ponens :

.

Meta-Inferenzregel

Lassen Sie eine Demonstration durch eine Sequenz repräsentiert werden, mit Hypothesen links vom Drehkreuz und der Schlussfolgerung rechts vom Drehkreuz. Dann lässt sich der Deduktionssatz wie folgt formulieren:

Wenn die Sequenz
demonstriert wurde, dann ist es auch möglich, die Sequenz zu demonstrieren
.

Dieser Deduktionssatz (DT) ist selbst nicht mit Aussagenkalkül formuliert: er ist kein Satz der Aussagenkalküle, sondern ein Satz über die Aussagenkalküle. In diesem Sinne ist es ein Meta-Theorem , vergleichbar mit Theoremen über die Richtigkeit oder Vollständigkeit der Aussagenkalküle.

Andererseits ist DT so nützlich, um den syntaktischen Beweisprozess zu vereinfachen, dass sie als eine weitere Inferenzregel betrachtet und verwendet werden kann, die den Modus Ponens begleitet. In diesem Sinne entspricht DT der natürlichen bedingten Beweisinferenzregel, die Teil der ersten in diesem Artikel vorgestellten Version der Aussagenkalküle ist.

Es gilt auch die Umkehrung von DT:

Wenn die Sequenz
demonstriert wurde, dann ist es auch möglich, die Sequenz zu demonstrieren

Tatsächlich ist die Gültigkeit der Umkehrung von DT im Vergleich zu der von DT fast trivial:

Wenn
dann
1:
2:
und aus (1) und (2) lässt sich ableiten
3:
mittels Modus Ponens, QED

Die Umkehrung von DT hat starke Implikationen: Sie kann verwendet werden, um ein Axiom in eine Inferenzregel umzuwandeln. Zum Beispiel das Axiom AND-1,

lässt sich mit der Umkehrung des Deduktionssatzes in die Inferenzregel umwandeln

Das ist die Konjunktionsbeseitigung , eine der zehn Inferenzregeln, die in der ersten Version (in diesem Artikel) des Aussagenkalküls verwendet werden.

Beispiel für einen Beweis

Das Folgende ist ein Beispiel für eine (syntaktische) Demonstration, die nur die Axiome THEN-1 und THEN-2 beinhaltet :

Beweisen Sie: (Reflexivität der Implikation).

Nachweisen:

  1. Axiom DANN-2 mit
  2. Axiom DANN-1 mit
  3. Aus (1) und (2) nach modus ponens.
  4. Axiom DANN-1 mit
  5. Aus (3) und (4) nach modus ponens.

Äquivalenz zur Gleichungslogik

Der obige alternative Kalkül ist ein Beispiel für ein Deduktionssystem nach Hilbert-Art . Im Fall von Aussagensystemen sind die Axiome Terme, die mit logischen Verknüpfungen aufgebaut sind, und die einzige Inferenzregel ist der Modus Ponens. Gleichungslogik, wie sie in der High-School-Algebra standardmäßig informell verwendet wird, ist eine andere Art von Kalkül als Hilbert-Systeme. Seine Theoreme sind Gleichungen und seine Inferenzregeln drücken die Eigenschaften der Gleichheit aus, nämlich dass es sich um eine Kongruenz von Termen handelt, die eine Substitution zulässt.

Die oben beschriebene klassische Aussagenrechnung entspricht der Booleschen Algebra , während die intuitionistische Aussagenrechnung der Heyting-Algebra entspricht . Die Äquivalenz wird durch Translation der Sätze der jeweiligen Systeme in jede Richtung gezeigt. Sätze der klassischen oder intuitionistischen Aussagenkalküle werden als Gleichungen der Booleschen bzw. Heyting-Algebra übersetzt. Umgekehrt werden Theoreme der Booleschen oder Heyting-Algebra als Theoreme des klassischen bzw. intuitionistischen Kalküls übersetzt, was eine Standardabkürzung ist. Im Fall der Booleschen Algebra kann man auch mit übersetzt werden , aber diese Übersetzung ist intuitiv falsch.

Sowohl in der Booleschen Algebra als auch in der Heyting-Algebra kann Ungleichheit anstelle von Gleichheit verwendet werden. Die Gleichheit lässt sich als Paar von Ungleichungen und ausdrücken . Umgekehrt lässt sich die Ungleichung als Gleichheit oder als ausdrücken . Die Bedeutung der Ungleichheit für Hilbert-style - Systeme ist , dass sie den Abzug oder die des letzteren entspricht entailment Symbol . Eine Verpflichtung

wird in der Ungleichungsversion des algebraischen Rahmens übersetzt als

Umgekehrt wird die algebraische Ungleichung als Folgerung übersetzt

.

Der Unterschied zwischen Implikation und Ungleichheit oder entailment oder ist , daß der erstere auf die interne Logik ist , während die letztere extern ist. Interne Implikation zwischen zwei Begriffen ist ein anderer Begriff der gleichen Art. Entailment als externe Implikation zwischen zwei Begriffen drückt eine Metawahrheit außerhalb der Sprache der Logik aus und wird als Teil der Metasprache betrachtet . Selbst wenn die zu untersuchende Logik intuitionistisch ist, wird das Entstehen klassischerweise als zweiwertig verstanden: entweder die linke Seite beinhaltet die rechte Seite oder ist kleiner oder gleich der rechten Seite oder nicht.

Ähnliche, aber komplexere Übersetzungen in und aus der algebraischen Logik sind für natürliche Deduktionssysteme wie oben beschrieben und für die Folgerechnung möglich . Die Folgerungen der letzteren können als zweiwertig interpretiert werden, aber eine aufschlussreichere Interpretation ist als eine Menge, deren Elemente als abstrakte Beweise verstanden werden können, die als Morphismen einer Kategorie organisiert sind . In dieser Interpretation entspricht die Schnittregel des Sequenzkalküls der Komposition in der Kategorie. Boolesche und Heyting-Algebren treten in dieses Bild als spezielle Kategorien ein, die höchstens einen Morphismus pro homset haben, dh einen Beweis pro Folgerung, entsprechend der Idee, dass es nur auf die Existenz von Beweisen ankommt: Jeder Beweis reicht aus, und es macht keinen Sinn, sie zu unterscheiden .

Grafische Berechnungen

Es ist möglich, die Definition einer formalen Sprache aus einer Menge endlicher Folgen über eine endliche Basis zu verallgemeinern, um viele andere Mengen mathematischer Strukturen einzuschließen, solange sie mit endlichen Mitteln aus endlichen Materialien aufgebaut sind. Darüber hinaus eignen sich viele dieser Familien formaler Strukturen besonders gut für die Verwendung in der Logik.

Zum Beispiel gibt es viele Familien von Graphen , die den formalen Sprachen so nahe kommen, dass das Konzept eines Kalküls ganz einfach und natürlich auf sie ausgedehnt werden kann. Viele Arten von Graphen entstehen als Parse-Graphen bei der syntaktischen Analyse der entsprechenden Familien von Textstrukturen. Die Erfordernisse der praktischen Berechnung formaler Sprachen erfordern häufig, dass Textstrings in Zeigerstrukturdarstellungen von Parsegraphen umgewandelt werden, einfach um zu überprüfen, ob Strings wohlgeformte Formeln sind oder nicht. Wenn dies einmal getan ist, ergeben sich viele Vorteile aus der Entwicklung des grafischen Analogons des Kalküls auf Strings. Die Abbildung von Strings auf Parse-Graphen wird als Parsing bezeichnet und die inverse Abbildung von Parse-Graphen auf Strings wird durch eine Operation erreicht, die als Durchqueren des Graphen bezeichnet wird.

Andere logische Berechnungen

Die Aussagenrechnung ist die einfachste Art von Logikkalkül, die derzeit verwendet wird. Es kann auf verschiedene Weise erweitert werden. (Die aristotelische „syllogistische“ Kalkül , die in der modernen Logik weitgehend verdrängt wird, ist in mancher Hinsicht einfacher – aber in anderer Hinsicht komplexer – als die Aussagenkalkül.) Der unmittelbarste Weg, einen komplexeren logischen Kalkül zu entwickeln, besteht darin, Regeln einzuführen, die empfindlich auf feinkörnigere Details der verwendeten Sätze.

Logik erster Ordnung (auch bekannt als Prädikatenlogik erster Ordnung) ergibt sich, wenn die "atomaren Sätze" der Aussagenlogik in Begriffe , Variablen , Prädikate und Quantoren zerlegt werden , wobei alle die Regeln der Aussagenlogik mit einigen neuen eingeführt werden. (Aus "Alle Hunde sind Säugetiere" können wir beispielsweise ableiten "Wenn Rover ein Hund ist, dann ist Rover ein Säugetier".) Mit den Werkzeugen der Logik erster Ordnung ist es möglich, eine Reihe von Theorien zu formulieren, entweder mit expliziten Axiomen oder durch Inferenzregeln, die selbst als logische Kalküle behandelt werden können. Arithmetik ist die bekannteste davon; andere schließen Mengenlehre und Mererologie ein . Logik zweiter Ordnung und andere Logiken höherer Ordnung sind formale Erweiterungen der Logik erster Ordnung. Daher ist es sinnvoll, die Aussagenlogik als " Logik nullter Ordnung" zu bezeichnen , wenn man sie mit diesen Logiken vergleicht.

Die Modallogik bietet auch eine Vielzahl von Schlussfolgerungen, die in der Aussagenrechnung nicht erfasst werden können. Zum Beispiel können wir aus "Notwendigerweise p " folgern, dass p . Aus p können wir ableiten "Es ist möglich, dass p ". Die Übersetzung zwischen Modallogik und algebraischer Logik betrifft die klassische und intuitionistische Logik, jedoch mit der Einführung eines unären Operators für Boolesche oder Heyting-Algebren, der sich von den Booleschen Operationen unterscheidet, der die Möglichkeitsmodalität interpretiert, und im Fall der Heyting-Algebra einen zweiten Operator, der die Notwendigkeit interpretiert (Für die Boolesche Algebra ist dies überflüssig, da die Notwendigkeit das De-Morgan-Dual der Möglichkeit ist). Der erste Operator behält 0 und Disjunktion bei, während der zweite 1 und Konjunktion beibehält.

Vielwertige Logiken erlauben es Sätzen, andere Werte als true und false zu haben . (Zum Beispiel sind keiner und beide Standard-"Zusatzwerte"; "Kontinuumslogik" erlaubt es jedem Satz, einen von unendlich vielen "Wahrheitsgraden" zwischen wahr und falsch zu haben .) Diese Logiken erfordern oft Rechenvorrichtungen, die sich von den Aussagen deutlich unterscheiden Infinitesimalrechnung. Wenn die Werte eine Boolesche Algebra bilden (die mehr als zwei oder sogar unendlich viele Werte haben kann), reduziert sich die vielwertige Logik auf die klassische Logik; Vielwertige Logiken sind daher nur dann von eigenständigem Interesse, wenn die Werte eine nicht boolesche Algebra bilden.

Löser

Das Finden von Lösungen für aussagenlogische Formeln ist ein NP-vollständiges Problem. Es gibt jedoch praktische Verfahren (zB DPLL-Algorithmus , 1962; Chaff-Algorithmus , 2001), die für viele nützliche Fälle sehr schnell sind. Neuere Arbeiten haben die SAT-Löseralgorithmen so erweitert , dass sie mit Aussagen arbeiten, die arithmetische Ausdrücke enthalten ; das sind die SMT-Löser .

Siehe auch

Höhere logische Ebenen

verwandte Themen

Verweise

Weiterlesen

  • Brown, Frank Markham (2003), Boolean Reasoning: The Logic of Boolean Equations , 1. Auflage, Kluwer Academic Publishers, Norwell, MA. 2. Auflage, Dover Publications, Mineola, NY.
  • Chang, CC und Keisler, HJ (1973), Modelltheorie , Nordholland, Amsterdam, Niederlande.
  • Kohavi, Zvi (1978), Switching and Finite Automata Theory , 1. Auflage, McGraw-Hill, 1970. 2. Auflage, McGraw-Hill, 1978.
  • Korfhage, Robert R. (1974), Diskrete Computerstrukturen , Academic Press, New York, NY.
  • Lambek, J. und Scott, PJ (1986), Einführung in die kategoriale Logik höherer Ordnung , Cambridge University Press, Cambridge, UK.
  • Mendelson, Elliot (1964), Einführung in die mathematische Logik , D. Van Nostrand Company.

Verwandte Werke

Externe Links