2012 seminar talk: Refutation complexity of relativized spectra

Talk held by Moritz Müller (KGRC) at the KGRC seminar on 2012-03-22.

Abstract

How difficult is it to prove that a given first-order sentence does not have a finite model of a given size? This can be understood in two natural, roughly equivalent ways. First, as a question for how strong a fragment of arithmetic needs to be to prove the statement. Second, as a question concerning proof lengths in certain propositional calculi. The talk gives a short introduction to proof complexity and presents some exponential lower bounds for the $R(k)$ systems. This is joint work with Albert Atserias and Sergi Oliva.