I'm trying to understand what 'effectively generated' theory means. Wikipedia says that it means that its set of theorems form a 'recursively enumerable' set, which I found equally confusing.
As an example how would one prove that Peano Arithmetic is effectively generated?
On
Usually one would appeal to a general theorem:
Let $T$ be a theory. If the axioms of $T$ form a decidable set (that is, the theory is recursively axiomatized), then the set of theorems of $T$ is recursively enumerable.
Since it ought to be easy to see that the set of axioms of PA is decidable, the result follows.
The theorem above is easy enough to prove once you have decided on a definition for "recursively enumerable". Unfortunately there are several possible definitions of that, which are equivalent but not obviously so -- but a major part of learning recursion theory is to familiarize oneself deeply with the fact that they're equivalent.
For this purpose it will be convenient to use the definition that a set is r.e. if it is the range of a partial computable function. Namely, here is pseudocode for a partial computable function whose range is the theorems of $T$:
It's a bit easier to think about recursive, rather than recursively enumerable, axiom sets (at least at first). A set of sentences $S$ is recursive iff, informally, we have an algorithm to tell what sentences are in $S$ and what sentences are not in $S$. This is a desirable property for a theory to have: we shouldn't, for example, be uncertain as to whether a given sentence is actually an axiom of PA!
A theory $T$ is recursively axiomatizable if it has some axiomatization which is recursive - remember that a given theory can be axiomatized in many different ways in general, and some axiomatizations might be pointlessly complicated (there's no rule that we can't have redundant axioms, for example).
(It's worth noting that the recursively axiomatizable theories are exactly the recursively enumerably axiomatizable theories, even though the latter seems a priori a broader class; this is due to Craig.)
In the specific case of PA, we have a standard axiomatization, consisting of (i) the ordered semiring axioms (of which there are only finitely many) and (ii) the induction scheme (which has infinitely many instances). To decide whether a given sentence $\varphi$ is an axiom of PA, we must check:
Is $\varphi$ one of the ordered semiring axioms? Since there are only finitely many of those, this is something we can just do.
If not, is $\varphi$ an instance of the induction scheme? Since there are infinitely many instances, we can't just check them one by one. Instead, we check whether $\varphi$ has a specific form: is there some formula $\psi(x_0,x_1,...,x_n)$ such that $\varphi$ literally is the sentence $$Ind_\psi:\quad\forall x_1,...,x_n(\psi(0,x_1,...,x_n)\wedge\forall y(\psi(y,x_1,...,x_n)\rightarrow\psi(y+1,x_1,...,x_n))\implies\forall y(\psi(y,x_1,...,x_n)))?$$ The point here is that (i) there are only finitely many possible $\psi$s we need to check (namely, the formulas shorter than $\varphi$) and (ii) the map $\psi\mapsto Ind_\psi$ is recursive. So this is in fact something we can do: check, for each $\psi$ shorter than $\varphi$, whether $\varphi$ is the sentence $Ind_\psi$.
The above procedure is completely algorithmic: it gives us a way to tell whether a sentence is one of the PA axioms. Now this obviously isn't a formal proof, but rather a "proof by Church's thesis;" however it isn't hard to turn it completely formal (if deeply tedious).