Herleitbarkeit (Sequenzenkalkül)

Eine Formel $\psi$ heißt aus einer Menge $\mathrm{\Phi }$ herleitbar ($\mathrm{\Phi }{⊢}_S\psi$), wenn es eine endliche Teilmenge ${\mathrm{\Phi }}^{\prime }\subseteq \mathrm{\Phi }$ gibt, sodass die Sequenz (Logik) ${\mathrm{\Phi }}^{\prime }\Rightarrow \{\psi \}$ im Sequenzenkalkül beweisbar ist (d.h. es existiert ein Ableitungsbaum (Logik) mit nur positiven Blättern).