Ein Ausdruck ${\displaystyle {}\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

${\displaystyle \vdash \alpha }$

ausgedrückt.