Насколько помню, к любой аксиоматической теории, включающей арифметику.
Я уточню: к любой аксиоматической теории, включающей арифметику, и имеющей перечислимое множество аксиом. То есть существует алгоритм (алгоритм - строгое математическое понятие) такой, что множеством его входных данных является

, а множество аксиом является множеством его выходных данных.
Это то, что я знаю твердо. Остается вопрос, что там с формальными системами, для которых такого алгоритма нет. Сам я этот вопрос не изучал, а слышал диаметрально противоположные мнения.
С одной стороны
Ну так, например, в формальных системах с неперечислимым множеством аксиом такого может и не быть. Сложность же увеличивается вместе с выразительностью и неизвестно, что быстрее.
А с другой стороны,
Есть мнение, что "теория с неперечислимым множеством аксиом" собственно теорией не является, ибо в такой "теории" нормальное доказательство чего бы то ни было невозможно.

Поскольку сам я в формальных системах с неперечеслимым множеством аксиом ни в зуб ногой, моего мнения не существует.