Logic with finite symbols What obstructions do you run into if you're trying to develop first order logic when you only have finitely many constant, relation, and function symbols?
Are there any cases where you actually need infinite symbols? It just seems like you'd be able to do almost everything if you just have finite, but a "large enough" number of symbols. Though I suppose there might be some axiom schemas that you can't express.
What I'm looking for is a theorem of classical logic where you can't prove it with finite symbols, even in some limited case like "if you have at least $f(n)$ symbols, then you can prove this for $n$ (formulas, -length proofs, etc.)," or infinite axiom schemas that require an infinite number of symbols, or other problems that I haven't thought of.
 A: The overwhelming  majority of mathematical theories are framed in a language that has only finitely many symbols, with the exception that infinitely many variable symbols are allowed.  The arguably most important theory, ZF, has a single binary predicate symbol. 
We can sneak around the infinitude of variable symbols by starting with the variable symbol $x$, and constructing others by appending an arbitrary number of occurrences of a new symbol $|$.
For some theoretical purposes, such as proving the Upward Lowenheim-Skolem Theorem, or for Skolemization,  it is useful to consider languages with infinitely many constant symbols, and even function symbols. And for constructing "rich" non-standard models of analysis, it is useful to have constant symbols, function symbols, and predicate symbols, for all reals, all functions on $\mathbb{R}^n$, and all relations. So certainly I would not want to restrict attention to "small" languages, but for most mathematical purposes one can.   
A: Finitely many constant, relation and function symbols is what we usually have in any concrete application of first-order logic.
The only thing we usually say we have an infinite supply of is variable names. But that's just for convenience -- it can be avoided if we want, by calling the variables $x, x', x'', x''', \ldots$. Then we only need two symbols x and ' for variables, and we can then do logic with a finite alphabet.
