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.
> 
> does a shorter tautology always admit a shorter proof?
> 
> 
> 

it seems like there should be a tautology whose statement is longer than fermats last theorem but whose shortest proof is shorter