Sequenzenkalkül

Der Sequenzenkalkü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.

Table of contents

1 Aussagenlogischer Sequenzenkalkül 1.1 Schlussregeln 2 prädikatenlogischer Sequenzenkalkül 2.2 Schlussregeln 3 prädikatenlogischer Sequenzenkalkül mit Gleichheit

Aussagenlogischer Sequenzenkalkül

Eine aussagenlogische Sequenz ist ein Ausdruck der Form ,wobei endliche Mengen von aussagenlogischen Formeln sind. Man bezeichnet mit Antezedens und mit Sukzedens. Eine Sequenz heisst 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.

• 
  
  
• 
  
  

• 
  
  

prädikatenlogischer Sequenzenkalkül

Eine prädikatenlogische Sequenz ist ein Ausdruck der Form , wobei endliche Mengen von geschlossenen prädikatenlogischen Formeln sind. Man bezeichnet mit Antezedenz und mit Sukzedenz. Eine Sequenz heisst gültig, wenn jedes Modell von , das zu auch Modell mindestens einer Formel aus ist. 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.

• 
  
  
• 
  
  

• 
  
  

• , darf nicht in oder vorkommen
  
  

• , darf nicht in oder vorkommen

prädikatenlogischer Sequenzenkalkül mit Gleichheit