The semantics of decision problems are always essentially independent of the
underlying representation. Thus the space of input data (under appropriate
indexing) is closed
under action of the symmetrical group $S_n$ (for a specific data-size)
and the input-output relation is closed under the action of $S_n$.
We show that symmetries of this nature (together with uniformity
constraints) have profound consequences in the context of Nullstellensatz
Proofs and Polynomial Calculus Proofs (Gr\"obner basis proofs).

Our main result states that for any co-NP (i.e. Universal Second Order)
sentence $\psi$ any non-constant degree lower bound on Nullstellensatz
proofs of $\psi_n$ immediately lifts to a
linear-degree lower bound.
This kind of ``gap'' theorem is new in this area of complexity theory.

The gap theorem is valid for Polynomial Calculus proofs as well,
and allows us immediately to solve a list of open problems concerning
degree lower bounds.
We get a linear degree (linear in the model size)
lower bounds for various matching principles. This solves an open
problem first posed in \cite{BIKPP}. The bounds
also improves the degree lower bounds of $\Omega(n^{\epsilon})$ achieved
in \cite{BIKPRS} as well as the degree lower bounds achieved
in \cite{BR}.

Another corollary to our main technical result
underlying the gap theorem is a {\it direct} linear degree lower bound on
proving primality. This improves recent work by \cite{Krajicek}.
We also
give a linear Polynomial Calculus degree lower bound on the onto-Pigeonhole
principle answering a question from \cite{Razborov1}.