A property of recursively enumerable sets containing “hardly deducible” formulas

There are considered recursively enumerable sets of formulas of the predicate calculus with the following property: for any sufficiently large $n$ there exists a formula in such a set, whose complexity of establishing of deducibility is maximal among all deducible formulas having the length $\leq n$. The article contains a low bound for some characteristic of density of such sets.