Prädikatenlogik/Ableitbar/Definition
Ableitbar (Prädikatenlogik)
Ein Ausdruck heißt ableitbar im Prädikatenkalkül (oder eine syntaktische Tautologie), wenn er sich aus den Grundtautologien, also
- den aussagenlogischen syntaktischen Tautologien,
- den Gleichheitsaxiomen,
durch sukzessive Anwendung der Ableitungsregeln Modus ponens und der Existenzeinführung im Antezedens erhalten lässt. Die Ableitbarkeit wird durch
ausgedrückt.