Is this possibility ruled out by Godel's Incompleteness Theorem?

Question

From Wikipedia:

"The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system."

Question: Does this (or any other known theorem) rule out the possibility of a consistent system of axioms whose theorems cannot be listed by an effective procedure, but can be used to prove any truth about the natural numbers?

Answer 1

Here are several facts. For simplicity, although it is not essential, assume all theories are in the language of arithmetic.

• If you take the set of all arithmetical true statements as a set of axioms, of course this proves all arithmetical true statements. This set of axioms is not effectively enumerable.

• One statement of the first incompleteness theorem is: No consistent set of axioms which is effectively enumerable can prove all arithmetical truths.

• If a set of axioms is effectively enumerable, so is its set of theorems. For this reason, we usually talk about "effectively axiomatizable" theories, which are theories generated by some effectively enumerable set of axioms.

• If a set of axioms is effectively enumerable, there is a (maybe different) set of axioms that is decidable and which proves the same set of theorems.

Corollaries:

• No effectively enumerable set of true sentences can prove all arithmetical truths. (Every set of true sentences must be consistent.)

• No finite set of true sentences can prove all arithmetic truths. (Every finite set of axioms is effectively enumerable.)

Answer 2

axioms [that] can be used to prove any truth about the natural numbers

Even if the axioms are not required to be listable by a computer, as long as the derivations from the axioms are required to be algorithmically verifiable certificates of finite length, then any subset of arithmetic truths from which all of them can be derived will be as complicated (by any measure of complexity that is meaningful in this context) as a listing all arithmetic truths.