Trennungseinführung oder Hinzufügung sind eine einfache gültige Argument-Form, eine unmittelbare Schlussfolgerung und eine Regel der Schlussfolgerung der Satzlogik. Die Regel macht es möglich, Trennungen in logische Beweise einzuführen. Es ist die Schlussfolgerung dass, wenn P wahr ist, dann müssen P oder Q wahr sein.

:Socrates ist ein Mann.

:Therefore, entweder Sokrates ist ein Mann oder Schweine fliegen in der Bildung über den Englischen Kanal.

Die Regel kann als ausgedrückt werden:

:

wo die Regel dass darin besteht, wann auch immer Beispiele "" auf Linien eines Beweises erscheinen, "" kann auf einer nachfolgenden Linie gelegt werden.

Trennungseinführung ist in der parakonsequenten Logik umstritten, weil in der Kombination mit anderen Regeln der Logik es zu Explosion führt (d. h. alles nachweisbar wird). Sieh Umtausche in der Parakonsequenten Logik.

Formelle Notation

Die Trennungseinführungsregel kann in der folgenden Notation geschrieben werden:

:

wo ein metalogical Symbol ist, das bedeutet, dass das eine syntaktische Folge in einem logischen System ist;

und hat als eine mit der Wahrheit funktionelle Tautologie oder Lehrsatz der Satzlogik ausgedrückt::

wo und in einem formellen System ausgedrückte Vorschläge sind.