Das Kefk Network Wiki befindet sich im Testbetrieb.

Sequenzenkalkül

Aus Kefk.

(Weitergeleitet von Gentzenkalkül)
Wechseln zu: Navigation, Suche

Der Sequenzenkalkül (manchmal auch Gentzenkalkül) ist ein von Gerhard Gentzen entwickelter, primär für metalogische Zwecke konzipierter logischer Kalkül. In einem weiteren Sinne kann er als ein System des natürlichen Schließens verstanden werden. Für den Sequenzenkalkül gilt der Vollständigkeitssatz.

Inhaltsverzeichnis

Aussagenlogischer Sequenzenkalkül

Eine aussagenlogische Sequenz ist ein Ausdruck der Form \Gamma \Rightarrow \Delta, wobei Γ,Δ endliche Mengen von aussagenlogischen Formeln sind. Man bezeichnet Γ mit Antezedens und Δ mit Sukzedens. Eine Sequenz \Gamma \Rightarrow \Delta heißt gültig, wenn jedes Modell von Γ auch Modell mindestens einer Formel aus Δ ist. Gibt es eine Belegung, unter der alle Formeln in Γ wahr werden, aber alle Formeln in Δ falsch werden, so falsifiziert eine derartige Belegung die Sequenz.

Schlussregeln

Die Sequenzen der ersten Zeile heißen Prämissen, die der zweiten Zeile Konklusion.

  • \left( \neg \Rightarrow \right)\qquad\frac{\Gamma \Rightarrow \Delta, F}{\Gamma, \neg F \Rightarrow \Delta}\qquad\qquad\qquad \left( \Rightarrow \neg \right)\qquad\frac{\Gamma, F\Rightarrow \Delta}{\Gamma\Rightarrow \Delta, \neg F}
  • \left(\vee\Rightarrow\right)\qquad\frac{\Gamma,F\Rightarrow\Delta\qquad\Gamma,G\Rightarrow\Delta}{\Gamma,F\vee G\Rightarrow\Delta}\quad\left(\Rightarrow\vee\right)\qquad\frac{\Gamma\Rightarrow\Delta,F,G}{\Gamma\Rightarrow\Delta,F \vee G}
  • \left(\wedge\Rightarrow\right)\qquad\frac{\Gamma, F, G\Rightarrow\Delta}{\Gamma, F\wedge G\Rightarrow \Delta}\qquad\qquad\quad\left(\Rightarrow\wedge\right)\qquad\frac{\Gamma\Rightarrow\Delta, F\qquad\Gamma\Rightarrow\Delta, G}{\Gamma\Rightarrow\Delta, F \wedge G}

Prädikatenlogischer Sequenzenkalkül

Eine prädikatenlogische Sequenz ist ein Ausdruck der Form \Gamma \Rightarrow \Delta, wobei Γ,Δ endliche Mengen von geschlossenen prädikatenlogischen Formeln sind. Man bezeichnet Γ mit Antezedens und Δ mit Sukzedens. Eine Sequenz \Gamma \Rightarrow \Delta heißt gültig, wenn jedes Modell von Γ auch Modell mindestens einer Formel aus Δ ist, d.h. wenn \bigwedge\Gamma\models\bigvee\Delta. Gibt es eine Struktur, unter der alle Formeln in Γ wahr werden, aber alle Formeln in Δ falsch werden, so falsifiziert eine derartige Struktur die Sequenz.

Schlussregeln

Die Sequenzen der ersten Zeile heißen Prämissen, die der zweiten Zeile Konklusion.

  • \left( \neg \Rightarrow \right)\qquad\frac{\Gamma \Rightarrow \Delta, F}{\Gamma, \neg F \Rightarrow \Delta}\qquad\qquad\qquad \left( \Rightarrow \neg \right)\qquad\frac{\Gamma, F\Rightarrow \Delta}{\Gamma\Rightarrow \Delta, \neg F}
  • \left(\vee\Rightarrow\right)\qquad\frac{\Gamma,F\Rightarrow\Delta\qquad\Gamma,G\Rightarrow\Delta}{\Gamma,F\vee G\Rightarrow\Delta}\quad\left(\Rightarrow\vee\right)\qquad\frac{\Gamma\Rightarrow\Delta,F,G}{\Gamma\Rightarrow\Delta,F \vee G}
  • \left(\wedge\Rightarrow\right)\qquad\frac{\Gamma, F, G\Rightarrow\Delta}{\Gamma, F\wedge G\Rightarrow \Delta}\qquad\qquad\quad\left(\Rightarrow\wedge\right)\qquad\frac{\Gamma\Rightarrow\Delta, F\qquad\Gamma\Rightarrow\Delta, G}{\Gamma\Rightarrow\Delta, F \wedge G}
  • \left(\exists\Rightarrow\right)\qquad\frac{\Gamma,F\left[x/a\right]\Rightarrow\Delta}{\Gamma,\exists xF\Rightarrow\Delta}, a darf nicht in Γ, Δ oder F[x] vorkommen.
  • \left(\Rightarrow\forall \right)\qquad\frac{\Gamma\Rightarrow\Delta, F\left[x/a\right]}{\Gamma\Rightarrow\Delta,\forall xF}, a darf nicht in Γ, Δ oder F[x] vorkommen.

Prädikatenlogischer Sequenzenkalkül mit Gleichheit

  • \left( = \right) \qquad \frac{\Gamma,t = t \Rightarrow \Delta}{\Gamma \Rightarrow \Delta}


Im Sequenzenkalkül gültige Regeln

Folgende Regeln sind im Sequenzenkalkül gültig

Mischung:

  • \left(mix \right) \qquad\frac{\Gamma\Rightarrow M\qquad \Delta\Rightarrow\ B}{\Gamma, \Delta - M \Rightarrow\ B}

Δ − M bezeichnet die Formelfolge, die entsteht, wenn man in Δ jedes vorkommende M streicht.

Schnittregel:

  • \left(cut \right) \qquad\frac{\Gamma\Rightarrow A\qquad A, \Delta\Rightarrow\ B}{\Gamma, \Delta \Rightarrow\ B}

Für die Beweisidee siehe Gentzenscher Hauptsatz

Weblinks

Wikipedia
 Dieses Dokument entstammt in seiner ersten oder einer späteren Version der deutschsprachigen Wikipedia. Es ist dort zu finden unter dem Stichwort Sequenzenkalk%C3%BCl, die Liste der bisherigen Autoren befindet sich in der Versionsliste; die Originalfassung kann dort auch bearbeitet werden. Alle Texte der Wikipedia und ihre Derivate stehen unter der GNU-Lizenz für freie Dokumentation.
Von „http://www.kefk.org/wiki/Sequenzenkalk%C3%BCl“
Persönliche Werkzeuge
Andere Sprachen