# Godel's incompleteness theorem: Question about effective axiomatization

I am studying Godel incompleteness theorems and I am struggling with the definition of effective axiomatization.

From Wikipedia:

A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is recursively enumerable. This means that there is a computer program that, in principle, could enumerate all the theorems of the system without listing any statements that are not theorems. Examples of effectively generated theories include Peano arithmetic and Zermelo–Fraenkel set theory (ZFC).1

The theory known as true arithmetic consists of all true statements about the standard integers in the language of Peano arithmetic. This theory is consistent and complete, and contains a sufficient amount of arithmetic. However, it does not have a recursively enumerable set of axioms and thus does not satisfy the hypotheses of the incompleteness theorems.

I have some intuitive idea of what effective axiomatization means... We need it to be able to recognize valid theorems and proofs, we need to check which axioms are part of that.

But I don't understand the definition of effective axiomatization. Probably because it refers to computer programs. Isn't that weird? How come we can't have a mathematical definition instead?

UPDATE: I realize even if I get the definition, I am lacking some intuition behind it, I would appreciate seeing some example of an algorithm that is axiomatizing a theory. E.g., for Peano arithmetic or ZFC.

• Computer programs are perfectly mathematical. If you prefer you can rephrase the definition in terms of Turing machines: en.wikipedia.org/wiki/Turing_machine Commented Jul 16 at 22:00
• Or primitive recursive functions. Commented Jul 16 at 22:02
• Note (re: @NaïmFavier's comment) that the following are equivalent for a theory $T$: $T$ is recursively enumerably axiomatizable; $T$ is recursively axiomatizable; $T$ is primitive recursively axiomatizable. (We can go even lower FWIW.) This is known as Craig's trick and is a consequence of the fact that Kleene's $T$-predicate is itself primitive recursive. Commented Jul 16 at 22:04
• @TerezaTizkova Godel worked at the level of primitive recursive (p.r.) functions, so his version would have been (something like) "If $T$ is a theory whose set of Godel numbers has primitive recursive characteristic function, then [stuff]." To see that (say) ZFC is p.r. in this sense, just think about how difficult it is to tell whether a sentence $\varphi$ is a ZFC axiom (not theorem): we first check finitely many special cases (Powerset/Extensionality/Foundation/Choice/Union/Pairing/Infinity), and then - if $\varphi$ isn't any of those - we check whether $\varphi$ fits the pattern (cont'd) Commented Jul 16 at 22:07
• of Separation or of Replacement. In each case, we don't have to search through arbitrary instances of the relevant scheme, only those generated by a formula of length less than that of $\varphi$, so this is p.r. See also this old answer of mine. (Throughout this and the previous comment, I've conflated the sentence $\varphi$ with its Godel number for convenience. That said, if we set up computability in terms of arbitrary strings or similar, this "translation" isn't needed.) Commented Jul 16 at 22:08