Gödel's Second Incompleteness theorem (G2) is one of the most famous results in mathematical logic. It asserts that no strong enough theory could prove its own consistency. Gödel's speedup theorem was the first result of the kind that established that one theory could prove the same sentences by a much shorter proofs than another theory. In this project I plan to investigate the question on limits of applicability of the second incompleteness theorem as well as the finer aspects of the speedup phenomenon. Recent results of Albert Visser and me opens the road to the development of category-theoretic forms of G2 that would be formulated in terms of internalization, which I plan to investigate. Also, I plan to study G2 for weak theories of syntax. I plan to investigate the speedups associated with conservation results for collection schemes, with conservative theories of truth definitions, and with various axiomatizations of the same classical decidable theories.