Why is finite-ness so important in proofs? Oftentimes I notice that in proof-writing, something that both my professors and textbook-writers stress is that such-and-such procedure must terminate. Other times, if we want to verify a property is true for some set, they will mention that there are only finitely many elements to check, which apparently makes our job easier. My question is why it is that finiteness is nicer than non-finiteness. I get that in an infinite set, we will never be able to finish checking "everything", but why does that matter? It's not like we're describing a process that a person will have to go through and actually do. I would imagine that it's a logic thing, but I haven't studied enough logic to understand it.
 A: The more explicit the proof, the clearer image we have of the objects involved in it.
For example, if you want to prove that a function $T\colon X\to Y$ extends to a function from some larger $X'$ with certain properties, having a complete description of the extension is better than having used an abstract theorem to prove the existence of the extension.
Finite sets are great this way, because of their finiteness they are easy to deal with by recursion: when you remove an element of a finite set, it becomes strictly smaller. Not so for infinite sets in general.
Proofs are also finite, which makes sense, since proofs are something we want to think of as objects we could possibly write on a piece of paper. When we have to make finitely many steps, even if we are using somehow abstract logical rules, we can still think of them as being somewhat descriptive.
For example, suppose that $X_1,\dots,X_n$ are non-empty sets. Then there is a function $f$ such that $f(i)\in X_i$. The easy way to prove this is to repeat the existential instantiation rule: $X_1$ is not empty, i.e. $\exists x(x\in X_1)$, so we can add a new symbol $x_1$ and declare $x_1\in X_1$. Rinse and repeat until $x_n$ is given, and define $f(i)=x_i$.
If the family of sets is infinite we can no longer do this. In that case we need to use the axiom of choice we simply asserts the existence of $f$. But we have no idea what this $f$ might be. And while the existential instantiation is somehow abstract and mysterious, we can at least grasp it conceptually as an iterative process, compared to the use of the axiom of choice which just instantly creates this function.
A: Well, this is a rather vague question, but here is a very nice (and useful) property of finite sets. 

Let $E$ be a finite set and let $f:E \to E$ be a function. Then  the
  following conditions are equivalent:
  
  
*
  
*$f$ is injective,
  
*$f$ is surjective,
  
*$f$ is bijective.
  

