Точно не знаю, но думаю да. Во-первых, если бы требовалась конечность системы аксиом, это не произвело бы такого эффекта (например, система аксиом Пеано 1-го порядка бесконечна, т.к. содержит схему индукции. Конечную систему аксиом арифметики, которая подпадает под теорему Геделя, придумал Робинсон позже), во-вторых, как я понимаю, его доказательство не стало бы проще от допущения конечности. Доказательство строилось на том, что вводилась кодировка высказываний и доказательств числами, показывалось, что в этой кодировке отношения типа "P - доказательство формулы φ" или "&psi получается из φ подстановкой выражения t вместо переменной x" становятся рекурсивными отношениями чисел, поэтому если система достаточно сильна, чтобы выражать рекурсивные функции, то можно построить формулу, которая говорит о себе, что у нее нет доказательства.

Одно допущение, которое было у Геделя и которое оказалось ненужным, это омега - непротиворечивость (если φ(0),&phi(1), ... -теоремы, то ∃n¬&phi(n) не теорема). Потом оказалось, что обычной непротиворечивости (если φ теорема то ¬φ не теорема) достаточно.