We provide and interpret a new measure independent characterization of the Gödel speed-up phenomenon. In particular, we prove a theorem that demonstrates the indifference of the concept of a measure independent Gödel speed-up to an apparent weakening of its definition that is obtained by requiring only those measures appearing in some fixed Blum complexity measure to participate in the speed-up, and by deleting the “for all r” condition from the definition so as to relax the required amount of speed-up. We (...) interpret our results as correlating the relative difficulty of mechanically recognizing theories with the relative power and the relative abstractness of the theories. We conclude by providing two open problems concerning possible similarities and relationships between the Blum speedability and Gödel speed-up phenomena. MSC: 03D15, 03F20. (shrink)

In this paper we investigate the following two questions: Q1: Do there exist optimal proof systems for a given language L? Q2: Do there exist complete problems for a given promise class equation image?For concrete languages L and concrete promise classes equation image , these questions have been intensively studied during the last years, and a number of characterizations have been obtained. Here we provide new characterizations for Q1 and Q2 that apply to almost all promise classes equation image and (...) languages L, thus creating a unifying framework for the study of these practically relevant questions. While questions Q1 and Q2 are left open by our results, we show that they receive affirmative answers when a small amount of advice is available in the underlying machine model. For promise classes with promise condition in equation imageequation image, the advice can be replaced by a tally equation image-oracle. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim. (shrink)

We prove that the Nisan-Wigderson generators based on computationally hard functions and suitable matrices are hard for propositional proof systems that admit feasible interpolation. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi . Previously this was known only for the treelike systems G*i. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

Cook and Reckhow [5] pointed out that $\mathcal {N}\mathcal {P} \neq co\mathcal {N}\mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time (...) generators) without a reference to proof complexity notions as follows:•There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $\mathcal {N}\mathcal {P}$ sets.We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from [18] is a good candidate for g. We define a new hardness property of generators, the $\bigvee $ -hardness, and show that one specific gadget generator is the $\bigvee $ -hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite $\mathcal {N}\mathcal {P}$ sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite $\mathcal {N}\mathcal {P}$ sets. (shrink)

In the early nineteenth century, a series of articles by Laplace and Poisson discussed the importance of ‘directness’ in mathematical methodology. In this thesis, we argue that their conception of a ‘direct’ proof is similar to the more widely contemplated notion of a ‘pure’ proof. More rigorous definitions of mathematical purity were proposed in recent publications by Arana and Detlefsen, as well as by Kahle and Pulcini: we compare Laplace and Poisson’s writings with these modern definitions of purity and show (...) how the modern definitions fail to grasp some more nuanced aspects. (shrink)

In [20] Krajíček and Pudlák discovered connections between problems in computational complexity and the lengths of first-order proofs of finite consistency statements. Later Pudlák [25] studied more statements that connect provability with computational complexity and conjectured that they are true. All these conjectures are at least as strong as $\mathsf {P}\neq \mathsf {NP}$ [23–25].One of the problems concerning these conjectures is to find out how tightly they are connected with statements about computational complexity classes. Results of this kind had been (...) proved in [20, 22].In this paper, we generalize and strengthen these results. Another question that we address concerns the dependence between these conjectures. We construct two oracles that enable us to answer questions about relativized separations asked in [19, 25] (i.e., for the pairs of conjectures mentioned in the questions, we construct oracles such that one conjecture from the pair is true in the relativized world and the other is false and vice versa). We also show several new connections between the studied conjectures. In particular, we show that the relation between the finite reflection principle and proof systems for existentially quantified Boolean formulas is similar to the one for finite consistency statements and proof systems for non-quantified propositional tautologies. (shrink)

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK . We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.