Deduktionssatz

Ein Metatheorem, das syntaktische Beweisbarkeit mit Implikation verknüpft: Wenn eine Formel B aus der Annahme A (ggf. zusammen mit weiteren Annahmen) beweisbar ist, dann ist die Implikation A → B im umgebenden formalen System beweisbar, unter systemspezifischen Bedingungen bzgl. der Entlastung von Annahmen.