Export (Logik) - Exportation (logic)

Transformationsregeln
Aussagenrechnung
Schlussfolgerungsregeln
Einführung  / Beseitigung von Implikationen ( Modus Ponens ) Bibedingte Einführung  / Elimination Konjunktionseinführung  / -beseitigung Disjunktionseinführung  / -beseitigung Disjunktiver  / hypothetischer Syllogismus Konstruktives  / destruktives Dilemma Absorption  / modus tollens  / modus ponendo tollens Verneinungseinleitung
Regeln für den Austausch
Assoziativität Kommutativität Verteilung Doppelte Negation De Morgans Gesetze Umsetzung Materielle Auswirkungen Ausfuhr Tautologie
Prädikatenlogik
Schlussfolgerungsregeln
Universelle Generalisierung  / Instanziierung Existenzielle Generalisierung  / Instanziierung
v T e

Export ist eine gültige Ersetzungsregel in der Aussagenlogik . Die Regel erlaubt es, bedingte Aussagen mit konjunktiven Antezedenten durch Aussagen mit bedingten Konsequenzen zu ersetzen und umgekehrt in logischen Beweisen . Es gilt die Regel:

${\displaystyle ((P\land Q)\to R)\Linksrightarrow (P\to (Q\to R))}$

Wobei " " ein metalogisches Symbol ist, das "in einem Beweis mit ersetzt werden kann." ${\displaystyle \Leftrightarrow}$

Formale Notation

Die Ausfuhr Regel kann in geschrieben werden sequent Schreibweise:

${\displaystyle ((P\land Q)\to R)\dashv \vdash (P\to (Q\to R))}$

wo ist eine metalogische Symbolbedeutung, die ein syntaktisches Äquivalent von in einem logischen System ist ; ${\displaystyle \dashv \vdash}$${\displaystyle (P\to (Q\to R))}$${\displaystyle ((P\land Q)\to R)}$

oder in Regelform :

${\displaystyle {\frac {(P\land Q)\to R}{P\to (Q\to R)}}}$, ${\displaystyle {\frac {P\to (Q\to R)}{(P\land Q)\to R}}.}$

wobei die Regel lautet, dass überall dort, wo eine Instanz von " " in einer Beweiszeile erscheint, sie durch " " ersetzt werden kann und umgekehrt; ${\displaystyle (P\land Q)\to R}$${\displaystyle P\to (Q\to R)}$

oder als Aussage einer wahrheitsfunktionalen Tautologie oder eines Satzes der Aussagenlogik:

${\displaystyle ((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))}$

wobei , , und Sätze sind, die in einem logischen System ausgedrückt werden . ${\displaystyle P}$${\displaystyle Q}$${\displaystyle R}$

Natürliche Sprache

Wahrheitswerte

Wenn P→Q wahr ist, kann es jederzeit durch P→(P∧Q) ersetzt werden.
Ein möglicher Fall für P→Q ist, dass P wahr ist und Q wahr ist; also gilt auch P∧Q und P→(P∧Q) ist wahr.
Ein anderer möglicher Fall setzt P als falsch und Q als wahr. Somit ist P∧Q falsch und P→(P∧Q) ist falsch; false→false ist wahr.
Der letzte Fall tritt ein, wenn sowohl P als auch Q falsch sind. Somit ist P∧Q falsch und P→(P∧Q) ist wahr.

Beispiel

Es regnet und die Sonne scheint, bedeutet, dass es einen Regenbogen gibt.
Wenn es also regnet, dann scheint die Sonne impliziert, dass es einen Regenbogen gibt.

Wenn mein Auto eingeschaltet ist und ich den Gang auf D schalte, fährt das Auto los. Wenn mein Auto an ist und ich den Gang auf D geschaltet habe, muss das Auto losfahren.

Nachweisen

Der folgende Beweis verwendet Material Implikation , doppelte Negation , De Morgans Gesetze , die Negation der bedingten Aussage, die Assoziativeigenschaft der Konjunktion, die Negation einer anderen bedingten Aussage und wiederum doppelte Negation, um das Ergebnis abzuleiten.

Vorschlag	Ableitung
${\displaystyle P\rightarrow (Q\rightarrow R)}$	Gegeben
${\displaystyle \neg P\lor (Q\rightarrow R)}$	Materielle Auswirkungen
${\displaystyle \neg P\lor (\neg Q\lor R)}$	Materielle Auswirkungen
${\displaystyle (\neg P\lor\neg Q)\lor R}$	Assoziativität
${\displaystyle \neg (P\land Q)\lor R}$	De Morgans Gesetz
${\displaystyle (P\land Q)\rightarrow R}$	Materielle Auswirkungen

Bezug zu Funktionen

Der Export ist mit Currying über die Curry-Howard-Korrespondenz verbunden .

Verweise