Prädikatenlogik/Ableitbar/Definition

Ableitbar (Prädikatenlogik)

Ein Ausdruck ${}\alpha \in L^{S}$ heißt ableitbar im Prädikatenkalkül (oder eine syntaktische Tautologie), wenn er sich aus den Grundtautologien, also

• den aussagenlogischen syntaktischen Tautologien,
• den Gleichheitsaxiomen,
• der Existenzeinführung im Sukzedens,

durch sukzessive Anwendung der Ableitungsregeln Modus ponens und der Existenzeinführung im Antezedens erhalten lässt. Die Ableitbarkeit wird durch

$\vdash \alpha$

ausgedrückt.