Sequenzenkalkül (Aussagenlogik)

Ein Kalkül zum Ableiten gültiger Sequenzen.

Axiom: Eine Sequenz (Logik) $Φ \Rightarrow Δ$ ist ein Axiom, wenn $Φ \cap Δ \neq \emptyset$ (d.h. eine Formel kommt links und rechts vor).
Regeln: Es gibt für jeden Junktor ( $\neg, \land, \lor, \to$ ) jeweils eine Regel für das Auftreten auf der linken Seite ( $\dots \Rightarrow$ ) und auf der rechten Seite ( $\Rightarrow \dots$ ).
- Beispiel ( $\land$ links): $\frac{Φ, ψ, φ \Rightarrow Δ}{Φ, ψ \land φ \Rightarrow Δ}$
- Beispiel ( $\land$ rechts): $\frac{Φ \Rightarrow Δ, ψ Φ \Rightarrow Δ, φ}{Φ \Rightarrow Δ, ψ \land φ}$

\begin{aligned} (\neg \Rightarrow) & \frac{Φ \Rightarrow Δ, ψ}{Φ, \neg ψ \Rightarrow Δ} & (\Rightarrow \neg) & \frac{Φ, ψ \Rightarrow Δ}{Φ \Rightarrow Δ, \neg ψ} \\ (\land \Rightarrow) & \frac{Φ, ψ, φ \Rightarrow Δ}{Φ, ψ \land φ \Rightarrow Δ} & (\Rightarrow \land) & \frac{Φ \Rightarrow Δ, ψ Φ \Rightarrow Δ, φ}{Φ \Rightarrow Δ, ψ \land φ} \\ (\lor \Rightarrow) & \frac{Φ, φ \Rightarrow Δ Φ, ψ \Rightarrow Δ}{Φ, φ \lor ψ \Rightarrow Δ} & (\Rightarrow \lor) & \frac{Φ \Rightarrow Δ, φ, ψ}{Φ \Rightarrow Δ, φ \lor ψ} \\ (\to \Rightarrow) & \frac{Φ \Rightarrow Δ, φ Φ, ψ \Rightarrow Δ}{Φ, φ \to ψ \Rightarrow Δ} & (\Rightarrow \to) & \frac{Φ, φ \Rightarrow Δ, ψ}{Φ \Rightarrow Δ, φ \to ψ} \end{aligned}