# Does the foundations of Arithmetic need to be effective?

I was reading about Godel's incompleteness theorem which is true for any formal theory that satisfies certain properties. One of these properties is the following: "The theory is assumed to be effective, which means that the set of axioms must be recursively enumerable.". I have also been told that Godel's incompleteness theorem hold for any axiomatic system large enough to be capable of expressing elementary arithmetic. (Is this because we assume the theory to have a signature that specifies the non-logical symbols in the language of such theory, such as '0' or '+'? )

But, clearly, if our assumption is false, such that our theory is not effective, Godel's theorem would not apply. Then, can't we create an axiomatic system which defines Arithmetic but is not effective? If so, it could be complete and consistent at the same time, right?. Why do we assume that the theory is effective? Why is that so important? In this case, being effective equivalent to having a finite list of axioms?

• Do you mean the representation theorem ? It is essential for Gödel's results. – Peter Aug 29 '15 at 21:17
• That's not a stupid question. You should remove that self-deprecating statement from your question. – Asaf Karagila Aug 29 '15 at 21:20

## 1 Answer

The thing is that being effective means that there is an algorithm that you can run on your very own computer, which if given sufficient time and resources, will recognize a statement provable from the effective theory.

In other words, a theory is effective, if there is a "reasonable" proof verification method to it. Meaning that there is a "simple" algorithm to verify whether a statement is provable from our foundational theory.

This might not be important if we had access to oracles, or to some higher being that could have given us immediate answers that would otherwise require an infinite time of computation, but we don't have such access (at the time of writing the answer). So "potential" computer verification is all we can do.

• I see. So if our theory is not effective, we wouldn't be able to check if a proof is correct, is that right? – Victor Chavauty Aug 29 '15 at 21:21
• Yes, we won't have an algorithm to check if the proofs are correct. Because we won't have a[n algorithmic] way of knowing what is an axiom and what is not an axiom. – Asaf Karagila Aug 29 '15 at 21:21
• It seems you are taking effective = recursive, while OP seems to be saying effective = recursively enumerable – UserB1234 Aug 29 '15 at 21:22
• @Danul: If $T$ is recursively enumerable, then there is a recursive theory $T'$ such that $T$ and $T'$ prove exactly the same statements. – Asaf Karagila Aug 29 '15 at 21:23
• @Danul: I should have been more accurate, perhaps, I meant "a set of axioms", which is sometimes called a "theory" without requiring it is closed under deductions. – Asaf Karagila Aug 29 '15 at 22:06