What does it mean for a collection to be finite? On the one hand, we have our preschool notion that a collection is finite when can be counted with natural numbers in a way that terminates. On the other hand, there is a definition due to Dedekind that a set is finite if and only if it cannot be put in one-to-one correspondence with a proper subset. Intuitively these two notions should be equivalent, but can we prove it? I will argue that to avoid a circular argument, one direction requires more care than one would initially think. Further, the other direction is true only by virtue of the Axiom of Choice. To outline the proof of this fact, we will examine formal notions of definiabilty and the set-theoretic technique of forcing.