Proving infinity vs Axiom of infinity I am not much of a set theorist, I deal primarely with algebra in my interest and what I study so this is toward set theorists. I am curious as to why cannot infinity be properly proven to exist? I know this is the issue which makes it be an axiom in ZFC set theory but I'd like to know in a more rigorous sense why it is not possible to prove it in any meaningful sense, it is intuitively relatively simple I feel but I'd like the formal one.
A link or description here would be in an equivalence class of acceptance ;-P
 A: The phrase "infinity cannot be properly proven to exist" begs the question: what axioms are we allowed to use to 'properly prove' something? Some sets of axioms, of course, can prove that an infinite set exists - e.g., ZFC :P. Others can't - e.g., ZFC minus the axiom of infinity (this is a good exercise - checking that the set $V_\omega$ of hereditarily finite sets is a model of all the ZFC axioms except Infinity). (We can also find reasonable-sounding sets of axioms which do prove the existence of an infinite set, but don't obviously sound like they do; so you have to be careful here. For example, Quine's New Foundations NF - see my and Zhen Lin's comments below.)
The axioms of ZFC are formulated to build the universe of sets starting from the smallest possible ingredient - the emptyset, $\emptyset$. In one interpretation, the axioms come in three flavors: 


*

*"Contextual" axioms, Foundation and Extensionality. These don't help us build new sets, they tell us what sort of object a set is.

*"Toolbox" axioms - Union, Pairing, Powerset, Separation, Replacement, and Choice. These are axioms which - more or less - tell us how to build new sets from old sets. (The "more or less" applies to Powerset and Choice, which don't really tell you how to build the new set, but whatever.) I ought to catch a transfinite amount of flack for grouping all these axioms together, but for this question I think this is the right grouping to uses.

*And then you have the "Jack-in-the-box" axioms - that just give you a set ex nihilo, that you otherwise couldn't build using the toolbox. In ZFC, there's only one - Infinity. But we often consider other similar axioms - we call them "strong axioms of infinity," or large cardinals.
The reason Infinity has to be a jack-in-the-box is that, if we start with the emptyset, then all our toolbox axioms just keep spitting out finite sets. So we have a "gap" between the finite and the infinite. 
A: If you're talking about things like ZF, then you're working in that context and that context is not everything.  The class of all hereditarily finite sets is a model of ZF without the axiom of infinity.  Therefore ZF without the axiom of infinity is consistent with every set being finite.
A: We prove that Vω is a model of ZF - infinity, that only proves that ZF-infinity is consistent. To prove that in ZF-Infinity we can't prove the consistency of the existence of an Infinite set, suppose it is consistent with ZF-Infinity (I'll call I=Infinity and X=exists infinite set). Then Con(ZF-I)-->Con((ZF-I)+X). Suppose (ZF-I)+X is consistent. Then there is a model K of it, there we can construct Vω, so we proved Con(ZF-I), therefore (ZF-I)+X proves Con((ZF-I)+X) which is impossible due to Godels Incompleteness theorem. 
