On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity

We show that the asymptotic complexity of uniformly generated (expressible in First-Order (FO) logic) propositional tautologies for the Nullstellensatz proof system (NS) as well as for Polynomial Calculus, (PC) has four distinct types of asymptotic behavior over fields of finite characteristic. More precisely, based on some highly non-trivial work by Krajicek, we show that for each prime p there exists a function l(n) ∈ Ω(log(n)) for NS and l(n) ∈ Ω(log(log(n)) for PC, such that the propositional translation of any FO formula (that fails in all finite models), has degree proof complexity over fields of characteristic p, that behave in 4 distinct ways: (i) The degree complexity is bound by a constant. (ii) The degree complexity is at least l(n) for all values of n. (iii) The degree complexity is bound by a constant on an infinite set S, and is at least l(n) on the complement N \ S. Furthermore, membership n ∈ S is for some k ∈ N determined uniquely by the value of n mo...

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Søren Riis
• Keywords: Computer Science, Degree Complexity, Degree Proof Complexity, FO Formula, LICS 2008