Natürliche Deduktion und Sequenzenkalkül

Natürliche Deduktion und der Sequenzenkalkül sind die beiden formalen Systeme im Gentzen-Stil, die Beweise durch Einführungs- und Eliminierungsregeln für die logischen Konnektive darstellen und das grundlegende Gerüst der strukturellen Beweistheorie bilden.

Definition

Die natürliche Deduktion leitet Formeln aus Annahmen unter Verwendung von Einführungs- und Eliminierungsregeln ab, die informelles Denken widerspiegeln, während der Sequenzenkalkül Sequenzen manipuliert, d.h. Behauptungen, dass eine Liste von Formeln eine andere impliziert, durch Regeln, die auf der linken und rechten Seite einer Implikation wirken.

Scope

Dieses Thema behandelt die Regeln der natürlichen Deduktion mit ihren Einführungs- und Eliminierungspaaren, die Struktur des Sequenzenkalküls mit seinen Links- und Rechtsregeln sowie strukturellen Regeln, die Normalisierung für die natürliche Deduktion, die Beziehung zwischen den beiden Systemen und ihre intuitionistischen und klassischen Varianten.

Core questions

• Wie verleihen Einführungs- und Eliminierungsregeln den logischen Konnektiven Bedeutung?
• Was ist eine Sequenz und wie unterscheiden sich ihre Regeln von denen der natürlichen Deduktion?
• Wie vereinfacht die Normalisierung Beweise der natürlichen Deduktion?
• Wie hängen die klassischen und intuitionistischen Versionen dieser Kalküle zusammen?

Key theories

Einführungs- und Eliminierungsregeln

Jedes Konnektiv wird durch Regeln gesteuert, die es einführen, und Regeln, die es nutzen, und ihre Harmonie, dass die Eliminierung genau das wiederherstellt, was die Einführung einbringt, drückt die Bedeutung des Konnektivs aus.

Normalisierungstheorem

Prawitz zeigte, dass Beweise der natürlichen Deduktion auf eine normalisierte Form ohne Umwege reduziert werden können, bei der eine Einführung sofort durch eine Eliminierung rückgängig gemacht wird, das Analogon der Schnitteliminierung in der natürlichen Deduktion.

Korrespondenz der beiden Kalküle

Die natürliche Deduktion und der Sequenzenkalkül beweisen dieselben Theoreme und können ineinander übersetzt werden, wobei die linken Sequenzenregeln den Eliminierungsregeln der natürlichen Deduktion entsprechen.

Clinical relevance

Diese Kalküle sind die Standardformate für das strukturelle Studium von Beweisen: Die natürliche Deduktion liegt der Typentheorie und den Beweisassistenten durch die Korrespondenz von Beweisen als Programme zugrunde, während der Sequenzenkalkül mit seiner Subformeleigenschaft nach der Schnitteliminierung die Grundlage der automatisierten Beweissuche und analytischer Tableaus bildet.

History

Gentzen führte sowohl die natürliche Deduktion als auch den Sequenzenkalkül 1934 und 1935 ein. Er entwickelte den Sequenzenkalkül, um sein Schnitteliminierungstheorem zu erhalten, nachdem er die natürliche Deduktion als schwieriger zu analysieren empfunden hatte. Prawitz belebte die natürliche Deduktion 1965 mit einer gründlichen Normalisierungsstudie wieder, und die Systeme wurden zentral für die späteren Entwicklungen der Beweise als Programme.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

Was ist der Unterschied zwischen natürlicher Deduktion und dem Sequenzenkalkül?

Die natürliche Deduktion arbeitet mit Formeln unter einem Kontext von Annahmen und verwendet Eliminierungsregeln, was der informellen Beweisführung sehr nahekommt. Der Sequenzenkalkül arbeitet mit expliziten Implikationen und ersetzt Eliminierungsregeln durch linke Einführungsregeln, ein Format, das die Schnitteliminierung und die Subformeleigenschaft transparent macht.

Warum ist die Normalisierung wichtig?

Ein normaler Beweis enthält keine Umwege und besitzt die Subformeleigenschaft, sodass jede Formel darin eine Subformel der Konklusion oder der Prämissen ist. Dies schränkt die Form von Beweisen ein, liefert Konsistenzergebnisse und entspricht über die Korrespondenz von Beweisen als Programme der Auswertung eines Programms zu einem Wert.