# 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. Aug 29, 2015 at 21:17
• That's not a stupid question. You should remove that self-deprecating statement from your question. Aug 29, 2015 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? Aug 29, 2015 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. Aug 29, 2015 at 21:21
• It seems you are taking effective = recursive, while OP seems to be saying effective = recursively enumerable Aug 29, 2015 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. Aug 29, 2015 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. Aug 29, 2015 at 22:06