Modular counting in proof complexity
------------------------------------

Abstract: First-order formulas cannot count, meaning
that no sentence A(X), X a unary predicate, is true
in a finite structure (n,U) iff |U| is odd. More
generally, this remains true even with an extra
structure or with formulas replaced by constant-depth
circuits. One can write down a propositional tautology
expressing that a set cannot support a total pairing
and at the same time a pairing leaving one element
out. The proof complexity of these tautologies
is of great interest and relates propositional
calculus to the so called algebraic proof systems.
I shall discuss related Boolean complexity results
and connections to Nullstellensatz degree bounds.
Paper: http://www.math.cas.cz/~krajicek/ens.ps.gz