 As an example of the applications of normalization theorems, the fact that normal derivations have the subformula property has implications for the decision problems. In propositional logic, there are only finitely many subformulas of the (finitely many) initial premises and conclusion, so a normal derivation can contain occurrences only of finitely many formulas. This (with a bit more work) implies that there is a finite upper bound on the size of possible normal derivations of a given conclusion from given premisses, so the propositional logic is (in principle!) decidable by an exhaustive search of possible derivations (Gentzen 1934 proves the decidability of Intuitionistic propositional logic in essentially this way, appealing to his Hauptsatz for the sequent calculus rather than normalization for natural deduction.) Turning to First Order logic, normal derivations have only a looser subformula property: for every free variable, the instance \(F(a)\) substituting that free variable for the quantified variable counts as a subformula of \(\forall xF(x)\) and \(\exists xF(x)\). First order logic is, of course, undecidable: what this shows is that no upper bound can be computed for the number of distinct instances of a quantification that need to occur in \(\forall\)-I or \(\exists\)-E subproofs in the proof of a valid formula of a given length.