I hesitate to say this, because it sounds harsh, but your comment is a heap of confusion. You're using words like "first order", "second order", "axiom system",

I hesitate to say this, because it sounds harsh, but your comment is a heap of confusion. You're using words like "first order", "second order", "axiom system", "true statements", "refuted", with confused understanding of what they mean. They all have clear technical meanings. If you're interested in this stuff and can stomach mathematical rigor, I highly recommend Enderton's _A Mathematical Introduction to Logic_ for mathematical logic in general, and Smullyan's own _Goedel's Incompleteness Theorems_ for this topic. Now, to back my harsh words a little. An axiomatic system, in the context of Goedel's theorems, is a bunch of axioms with some inference rules. Axioms are statements that are automatically taken as proved, while inference rules allow one to infer more proved statements from some already proved statements. Given an axiomatic system, you can define a proof of statement X to be a sequence of statements that starts with axioms and always goes through inference rules until it reaches X. All of the above is purely syntactic, meaning it has to do with rules that govern how symbols are written on the paper, and there's no need for any interpretation of what the symbols mean. You could have an axiomatic system where statements would be Tarot cards, axioms some particular cards, and inference rules would govern which card you can place next to ones you already have. It'd be a silly axiomatic system, but it would be one, and you wouldn't need to know anything about what the cards "mean". Similarly, you can write down an axiomatic system with statements that use symbols like "0", "1", "+", "x" "forall", without caring what it means for a statement to be true or false. Any axiomatic system really comes with a _logic_ in the background: the logic specifies what kinds of statements you're allowed to write down. The most important and frequently used kind is first-order logic, which lets you use constant symbols like "0", "1", function symbols like "+" (again, as purely abstract marks-on-paper without caring what their meaning is), equality sign "=", variables like "x", "y" etc., and crucially quantifiers "for all" and "exists" that let you say things like "for all x, something-that-depends-on-x". Second-order logic, in addition, also lets you quantify over sets or functions. In first-order logic, you can only have a few fixed symbols like + and write some statements about them, but in second-order logic you can express statements about any possible function, like, say, "for every function F on two variables, F(x,y) = F(y,x)". This kind of statement is invalid in first-order logic, for some good reasons. Not "true" or "false", just impossible to write down in the first place. This is why when you say "The Incompleteness Theorem shows that no first order axiomatic system is powerful enough to encapsulate all true statements in the second order Peano axioms", this is nonsense, because a first-order axiomatic system cannot prove statements in a second-order system, in general. They come from different logics. Second-order systems contain statements that first-order systems can't express at all, much less prove. Now, independently of defining an axiomatic system, we can also define a meaning - "semantics" - for any statement in a particular logic. For example, we can decide, with good reason, that the symbol "0" actually stands for the number 0, the symbol "+" stands for the operation of addition, and so on. The statement "2+2=5" will then not be just a string of five meaningless marks on paper, it will also have a meaning and a truth value (which is false, in this case). We can decide what it means for the more complex statements like "for all x ..." to be true - appropriately enough, it means that if you try to substitute any number for x inside the "...", you'll always get a true statement. Now every statement in our logic is either true or false, although for many of them it's difficult to know which is the case. Going back to axiomatic systems, we remember that they have axioms and inference rules. Typically, some of the axioms and all of the inference rules are called "logical" and are independent of the particular math structure we're trying to investigate (natural numbers, in this case). The logical axioms and inference rules say things like "x=x" and "if you proved "for all x, ...", you can also count as proved any version of ... in which you substituted something for x". We regard them as intuitively, tautologically true. The other, remaining non-logical axioms say things like "a+0=a" and "every number except 0 has a predecessor". They could be for example the Peano axioms for natural numbers. Godel's Completeness Theorem has absolutely nothing to do with his Incompleteness Theorem, and the "completeness" it talks about is very different from the "incompleteness" the other theorem talks about. Goedel's Completeness Theorem really says something important about the usual bunch of logical axioms and inference rules, the one that form the backbone of pretty much every first-order axiomatic system we study. It says that they're strong enough to prove anything that must always be true in any semantics. For example (trivial example), no matter how we define what the symbol '0' means, it will always be true that "for any x, if x=0, then 0=x". All tautologies like that are better be provable with logical axioms alone, and Goedel's Completeness Theorem ensures that they are. The fact that we have a Goedel's Completeness Theorem is really what allows us to confidently use first-order logic as a conceptual basis for all mathematics. It tells us that axiomatic systems for first-order logic are complete in the sense of "strong enough to prove all tautologies". But it has nothing to do with the Incompleteness Theorems, which are about "complete" in the sense of "strong enough to prove every sentence or its negation". So your second paragraph "In fact, his Completeness Theorem proves the opposite of what you claim" is nonsense, too. It's true that you can make up a trivial example of a complete system just by declaring all true statements to be axioms. But that fact has nothing to do with Goedel's Completeness Theorem. The reason that trivial example is inadequate is that, as you mention, it's not manageable - you can't determine what's an axiom and what isn't. Finally, your third paragraph is also wrong. To refute means to prove the negation of. If X cannot be refuted, that means you can't prove not-X. From this it only follows that you can prove X if you have a complete axiomatic system. Since normally, in fact, you don't (by virtue of Goedel's incompleteness theorems), it doesn't follow at all. Now what's true and may be confusing you is that there are certain simple kinds of statements for which this is true, because they're very simple. You can prove that e.g. the Peano Axioms are powerful enough to prove any true statement, or refute any false statement, of a particular simple kind. But not in any statement in general - that'd contradict the Goedel's incompleteness theorems.