[Proof Complexity] new preprint

Moritz Müller moritz at cs.upc.edu
Fri Jul 26 11:36:06 CEST 2019

Dear all

there is a new preprint available from my homepage:


I appreciate all kinds of comments. Please find title and abstract below.



Title: Typical forcings, NP search problems and an extension of a 
theorem of Riis

Abstract: We study total (type 2) NP search problems associated to 
finitary combinatorial principles. Complexity theory compares such 
problems with respect to (polynomial time) many-one or Turing 
reductions. From a logical perspective such problems are graded 
according to the bounded arithmetic theories that prove their totality. 
The logical analogue of a reduction is to prove the totality of one 
problem from the totality of another. The link between the two 
perspectives is tight for what we call universal variants of relativized 
bounded arithmetics. We strengthen a theorem of Buss and Johnson that 
infers relative bounded depth Frege proofs of totality from Turing 

We define typical forcings encompassing many informal forcing arguments 
in bounded arithmetic and give general conditions for such forcings to 
produce models of the universal variant of relativized T^1_2. As an 
application we derive a strong form of Riis' finitization theorem. We 
extend it by exhibiting a simple model-theoretic property that implies 
independence from the universal variant of relativized T^1_2 plus the 
weak pigeonhole principle. More generally, we show that the universal 
variant of relativized T^1_2 does not prove (the totality of the total 
NP search problem associated to) a strong finitary combinatorial 
principle from a weak one. Being weak or strong are simple 
model-theoretic properties based on the behaviour of the principles with 
respect to finite structures that are only partially defined.

More information about the Proof-Complexity mailing list