 Theoremhood

Theoremhood is formal derivability with no undischarged assumptions. A logical formula is a theorem of a calculus exactly when it has an assumption-free formal proof.