We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter. One could separate the parameterized complexity classes FPT and W[2] by showing that there is no proof system (for CNF formulae) that admits proofs of size f(k)n^{O(1)} where f is a computable function and n denotes the size of the propositional formula. We provide a first step and show that tree-like resolution does not admit such proofs. We obtain this result as a corollary to a meta-theorem, the main result of this paper.

The meta-theorem extends Riis' Complexity Gap Theorem for tree-like resolution. Riis' result establishes a dichotomy between polynomial
and exponential size tree-like resolution proofs for propositional formulae that uniformly encode a first-order principle over a universe
of size n: (1) either there are tree-like resolution proofs of size polynomial in n, or (2) the proofs have size at least 2^{\epsilon n} for some constant \epsilon; the second case prevails exactly when the first-order principle has no finite but some infinite model.

We show that the parameterized setting allows a refined classification, splitting the second case into two subcases: (2a) there are tree-like resolution proofs of size at most \beta^k n^\alpha for some constants \alpha,\beta; or (2b) every tree-like resolution proof has size at least n^{k^\gamma} for some constant \gamma in (0,1]; the latter case prevails exactly if for every infinite model, a certain associated hypergraph has no finite dominating set. We provide examples of first-order principles for all three cases.