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

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

ausgedrückt.