  A different attempt at providing a way around Gödel’s second theorem for Hilbert’s Program was proposed by Detlefsen  (1986;  2001;  1979).  Detlefsen presents several lines of defense, one of which is similar to the one just described: arguing that a version of the \(\omega\)-rule is finitarily acceptable, although not capable of formalization (however, see  Ignjatovic 1994).  Detlefsen’s other argument against the common interpretation of Gödel’s second theorem focuses on the notion of formalization: That the particular formalization of “\(T\) is consistent” by Gödel’s formula \(Con_T\) is not provable does not imply that there couldn’t be other formulas, which are provable in \(T\), and which have as much right to be called “formalizations of the consistency of \(T\).” These rely on different formalizations of the provability predicate \(Pr_T\) than the standard ones. It is known that formalized consistency statements are unprovable whenever the provability predicate obeys certain general derivability conditions. Detlefsen argues that these conditions are not necessary for a predicate to count as a genuine provability predicate, and indeed there are provability predicates which violate the provability conditions and which give rise to consistency formulas which are provable in their corresponding theories. These, however, depend on non-standard conceptions of provability which would likely not have been accepted by Hilbert (see also  Resnik 1974,  Auerbach 1992  and  Steiner 1991).