logischer Ausdruck, der aus einem gegebenen logischen Axiomensystem mit Hilfe formaler Ableitungsregeln erzeugt werden kann (siehe auch logische Ableitbarkeit). Anstatt „herleitbare Formel” sagt man auch häufig „ableitbarer Ausdruck”.