Question: My basic question is: "Do longer tautologies take longer to prove?" But obviously this is underdetermined. If you are allowed an inference rule "Tautological Implication" then any tautology has a 1 line proof. 

But let's say we're working in natural deduction, is it true that longer tautologies (tautologies with more letters and connectives in them) take more proof steps?

But this is still not quite a good enough question, since we can add superfluous steps to a proof and still prove the result. So the question is:

In Natural Deduction, is the shortest proof of a tautology related to its length? Or perhaps: does a shorter tautology always admit a shorter proof?

And how robust is this result across different sets of connectives/inference rules?

Answer: 
This question is one of the main topics studied in [proof complexity](http://en.wikipedia.org/wiki/Proof_complexity). The measure you are talking about is called the number of *steps* in the proof or proof-length.

The size of a tautology is related to the number of steps of its shortest proof, but this does not mean that the number of steps is a monotone function of size of tautology. As mentioned by others, the length of a long tautology can be very short. Coming up with arbitrary long tautologies having proofs with constant (i.e. independent from the size of tautology) number of steps is not difficult. 

On the other hand, the task of coming up with tautologies with large number of steps is not obvious and is open for many propositional proof systems. Note that it follows from the (constructive) proof of completeness theorem that every tautology of size $s$ has a proof of height $O(s)$ with $O(2^s)$ steps and size $O(s2^s)$.

We have some very weak lowerbounds for maximum number of steps needed for a tautology of size $s$ and the question that this upperbound is tight is wide open for sequent calculus and also for natural deduction which are essentially equivalent to Hilbert style proof systems. The bound is tight if we remove cut rule from sequent calculus, i.e. there are tautologies which require exponential number of steps.

You can find out more about the relation between different measure studied in proof complexity and the relation between different propositional proof systems by checking surveys/books on the topic.

For first order logic, note that the first order logic is undecidable, i.e. given a formula there is no algorithm to check if it is a valid formula. Any computable upperbound on the proof size would give an algorithm for deciding first order logic, check all possible proofs up to that size. (Note that an upper bound on proof length in natural deduction/sequent calculus will give an upper bound on the size because of normalization/cut elimination). Since there is no such algorithm, there cannot be any computable upperbound.
Suppose that $\phi$ is any sentence of the form $\lnot (\psi \land \lnot \psi)$. Then there is a pattern for a very short proof of $\phi$ that works for any formula $\psi$. I can't format it here, but the idea is to obtain $\bot$ from $\psi \land \lnot \psi$ in a fixed number of steps, and then apply the rule for proof by contradiction to get $\phi$. The original contradiction will take three steps in natural deduction: two are conjunction elimination and the third derives $\bot$. So the entire proof pattern has four steps in natural deduction regardless of $\psi$. If you tweak the setup for natural deduction the number of steps may go up to five or six, but it will be constant in any case. 

I'm not sure whether there is any system where longer tautologies always take longer proofs and where length is measured in proof steps. Certainly it would have to have modified versions of the rules relating to $\bot$. 

One way to change the question is to change the way you measure the length of a proof. If the size of the proof is the total symbol count then there is clearly a sense in which longer facts require longer proofs.