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: 
The size of proofs is almost totally unrelated to the size of the statements they prove (in the worst case).

**Lower Bound: constant size**

The size of the smallest proof for statements of size N is constant. Just make your statements of the form "True or S". (Unless you count the input statement as part of the size, in which case it is linear.)

**Upper Bound: incomputable size**

The size of the largest proof proving a statement of size less than N grows so fast it is not computable from N.

*Proof*

Consider the size of a proof that a Turing Machine does not halt within S steps. Some turing machines run forever but can't be proven to run forever. Suppose you have such a machine M. Proving M doesn't halt before S steps must take more steps as S grows. Otherwise we have a proof for all S and have contradicted ourselves.

Lets call that number-of-steps to proof-size function G. I am going to make one assumption, which is that there is a computable function G' such that G(G'(X)) >= X.

Suppose you have some computable function F you claim is an asymptotic upper bound on proof sizes given the statement size. Then I just generate a sequence of statements where the Nth statement is "M does not halt within G'(N\*F(N)) steps". The statements are all provable (worst case: simulate M in the proof; that's why I assumed G' is computable) and grow in size logarithmically. But the proof sizes grow asymptotically faster than F, which is exponentially faster than F with respect to the statement sizes. So F is not actually an asymptotic upper bound.

Therefore no computable function is an asymptotic upper bound on proof size given the statement size, which means the upper bound is incomputable.
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.