It is not clear what you mean by "any recursively axiomatizable true theory with equality". For example, the theory of dense linear orderings without endpoints is a complete and decidable theory, and it has a finite list of axioms, so it is effectively axiomatizable.
If by "true theory" you mean a theory of arithmetic, then Presberger arithmetic is a more relevant example of a complete, decidable, effectively axiomatizable theory. It is the theory of $\mathbb{N}$ in the language with equality and addition, but without a multiplication. See [1].
If by "true theory with equality" you mean a true theory of arithmetic in the language with equality, addition, and multiplication, then the question you are asking is exactly Gödel's incompleteness theorem [2], and you can look up a proof in any logic textbook.
If you use a book that has a hypothesis of "the theory extends Robinson arithmetic" in the incompleteness theorem, you may find the following hint useful: if $T$ is a true theory in the language of Peano arithmetic then $T \cup Q$, where $Q$ is Robinson arithmetic, is also a true theory.
1: http://en.wikipedia.org/wiki/Presburger_arithmetic
2: http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems
Full semantics for higher-order logic is expressed at the meta-level: it says that we only consider models in which the higher-order variables range over all objects of the appropriate sort.
The error in the second paragraph of the post is that second-order logic with full semantics is not reducible to set-theory with first-order (Henkin) semantics in the way that paragraph claims. For example, every model of the second-order Peano axioms in full semantics satisfies the sentence Con(ZFC), but not every model of ZFC does. So the set of arithmetical logical consequences of the second-order Peano axioms in full semantics is a strictly larger set than the set of arithmetical consequences of the ZFC axioms.
There is no effective object theory whatsoever, in first-order (Henkin) semantics, that can achieve the restriction of full semantics. We have to make the restriction for full semantics at the metatheoretic level.
What is true is that, within each model of set theory, we have a "toy model" of full semantics: within a model $M$ of set theory, we can look at Henkin models for higher-order logic that appear to be full, from the viewpoint of $M$. We can use these "toy models" to understand how full semantics works. These "toy models" do help us understand just how strong second-order semantics are.
There is a vague analogy here with the fact that the intended model of ZFC consists of all sets, but no model in the usual first-order sense can contain all sets. So when we look at set models of ZFC, we get a sense of how the intended interpretation should work, but we don't actually see the intended interpretation. Similarly, if we try to formalize full semantics within a first-order set theory, we get a sense of how they work, but we can't capture their full strength.
The preceding paragraphs are written from what I view as the "classical" perspective on full semantics. Let me say, without taking a position, that there is another very tempting position for full semantics: that they are only defined relative to a given model of set theory. Thus, just as there are many models of set theory, there are many models of "full semantics". The benefit of this point of view is that it emphasizes more explicitly the assumptions about set existence that are presupposed by full semantics. But those who advocate the classical perspective might say that this other perspective misses the point, which is simply (from their POV) to require that the higher-order variables range over all objects of the appropriate sort.
Best Answer
Any FOL theory with computably enumerable axiom schemas is essentially equivalent (i.e. is bi-interpretable) with another FOL theory with finitely many axioms. You simply encode the (finitely many) rules that underlie the schemas. In some cases, such as finite axiomatization of NBG or ACA0, you can even do this with not much encoding. These clearly demonstrate that the infiniteness of an axiomatization is not at all set-theoretic in itself. Also, second-order logic is way over-hyped if you are concerned about foundations. Second-order theories are important when studying mathematical structures, but not really relevant to true foundations of mathematics.