 A variant of second incompleteness theorem (Feferman 1960)   Let \(F\) be a consistent extension of PA, and let \(Ax_F (x)\) be a \(\Sigma^{0}_1\)-formula which weakly represents the axioms of \(F\), and \(\Cons(F)\) be a consistency statement constructed from \(Ax_F (x)\) and \(\Prov_{FOL}(x)\). Then \(\Cons(F)\) is not provable in \(F\). 