Dealing with infinities in predicate calculus

Question

I'd like to develop a program capable of verifying basic expressions in predicate calculus. When working in finite domains, one can exhaustively check the validity of universal/existential quantifiers. The trouble is, infinite collections show up all the time in math. This means it is impossible to use the exhaustive approach mentioned earlier. To get over this hurdle I've thought of a few possible solutions: mathematical induction, and/or showing the predicate is derivable from a set of axioms/already proven statements. Ideally, I'd like to be able to create expressions like "let $x$ be an arbitrary integer" and then use what is known about the integers to prove stuff. How I'd go about doing this is still not clear. How are infinite domains tamed in predicate calculus?