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

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?

• Of course; just take the set of all truths (in the language of arithmetic) as your set of axioms. – Carl Mummert Jan 22 '14 at 1:24
• @CarlMummert How about just a finite number of truths? – Dan Christensen Jan 22 '14 at 1:28
• Any finite set can be listed by an effective procedure – Carl Mummert Jan 22 '14 at 1:29
• By the incompleteness theorem, no effectively enumerable set of true axioms can prove all true statements in the language of arithmetic – Carl Mummert Jan 22 '14 at 1:33
• As someone who wrote a proof assistant, I'd expect you to know that axioms are theorems. – Asaf Karagila Jan 22 '14 at 1:41

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.)

• While the last corollary is true, PA is not finitely axiomatizable, did you mean "truths" rather than theorems? – Asaf Karagila Jan 22 '14 at 1:46
• @Asaf: thanks, I did mean that. – Carl Mummert Jan 22 '14 at 1:47

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.