Showing 1–19 of 19 results for author: Krajicek, J

On $NP \cap coNP$ proof complexity generators

Authors: Jan Krajicek

Abstract: Motivated by the theory of proof complexity generators we consider the following $Σ^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $π$ of a disjunction $\bigvee_i α_i$, no two $α_i$ having an atom in common, find $i$ such that $α_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$… ▽ More Motivated by the theory of proof complexity generators we consider the following $Σ^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $π$ of a disjunction $\bigvee_i α_i$, no two $α_i$ having an atom in common, find $i$ such that $α_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$ is not solvable in the student-teacher model with a p-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies $NP \neq coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds. △ Less

Submitted 25 June, 2025; originally announced June 2025.

MSC Class: O3F20; 03H15 ACM Class: F.1.2; F.4.1

A proof complexity conjecture and the Incompleteness theorem

Authors: Jan Krajicek

Abstract: Given a sound first-order p-time theory $T$ capable of formalizing syntax of first-order logic we define a p-time function $g_T$ that stretches all inputs by one bit and we use its properties to show that $T$ must be incomplete. We leave it as an open problem whether for some $T$ the range of $g_T$ intersects all infinite NP sets (i.e. whether it is a proof complexity generator hard for all proof… ▽ More Given a sound first-order p-time theory $T$ capable of formalizing syntax of first-order logic we define a p-time function $g_T$ that stretches all inputs by one bit and we use its properties to show that $T$ must be incomplete. We leave it as an open problem whether for some $T$ the range of $g_T$ intersects all infinite NP sets (i.e. whether it is a proof complexity generator hard for all proof systems). A propositional version of the construction shows that at least one of the following three statements is true: - there is no p-optimal propositional proof system (this is equivalent to the non-existence of a time-optimal propositional proof search algorithm), - $E \not\subseteq P/poly$, - there exists function $h$ that stretches all inputs by one bit, is computable in sub-exponential time and its range $Rng(h)$ intersects all infinite NP sets. △ Less

Submitted 15 September, 2023; v1 submitted 19 March, 2023; originally announced March 2023.

Comments: preliminary version March 2023, revised September 2023

MSC Class: 03F20; 03F40; 68Q15 ACM Class: F.1.3; F.4.1

Extended Nullstellensatz proof systems

Authors: Jan Krajicek

Abstract: For a finite set $\cal F$ of polynomials over fixed finite prime field of size $p$ containing all polynomials $x^2 - x$ a Nullstellensatz proof of the unsolvability of the system $$ f = 0\ ,\ \mbox{ all } f \in {\cal F} $$ in the field is a linear combination $\sum_{f \in {\cal F}} \ h_f \cdot f$ that equals to $1$ in the ring of polynomails. The measure of complexity of such a proof is its degr… ▽ More For a finite set $\cal F$ of polynomials over fixed finite prime field of size $p$ containing all polynomials $x^2 - x$ a Nullstellensatz proof of the unsolvability of the system $$ f = 0\ ,\ \mbox{ all } f \in {\cal F} $$ in the field is a linear combination $\sum_{f \in {\cal F}} \ h_f \cdot f$ that equals to $1$ in the ring of polynomails. The measure of complexity of such a proof is its degree: $\max_f deg(h_f f)$. We study the problem to establish degree lower bounds for some {\em extended} NS proof systems: these systems prove the unsolvability of $\cal F$ by proving the unsolvability of a bigger set ${\cal F}\cup {\cal E}$, where set $\cal E$ may use new variables $r$ and contains all polynomials $r^p - r$, and satisfies the following soundness condition: -- - Any $0,1$-assignment $\overline a$ to variables $\overline x$ can be appended by an assignment $\overline b$ to variables $\overline r$ such that for all $g \in {\cal E}$ it holds that $g(\overline a, \overline b) = 0$. We define a notion of pseudo-solutions of $\cal F$ and prove that the existence of pseudo-solutions with suitable parameters implies lower bounds for two extended NS proof systems ENS and UENS defined in Buss et al. (1996/97). Further we give a combinatorial example of $\cal F$ and candidate pseudo-solutions based on the pigeonhole principle. △ Less

Submitted 27 September, 2023; v1 submitted 25 January, 2023; originally announced January 2023.

Comments: Preliminary version January 2023

MSC Class: 03F20; 68Q15 ACM Class: F.1.1; F.4.1

Journal ref: Proc. of the AMS, Vol.152, Number 11, November 2024, pp.4881-4892

On the existence of strong proof complexity generators

Authors: Jan Krajicek

Abstract: Cook and Reckhow 1979 pointed out that NP is not closed under complementation iff there is no propositional proof system that admits polynomial size proofs of all tautologies. Theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus at a conjecture from K.2004 in foundations of the theory that there is a proof compl… ▽ More Cook and Reckhow 1979 pointed out that NP is not closed under complementation iff there is no propositional proof system that admits polynomial size proofs of all tautologies. Theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus at a conjecture from K.2004 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 exist a p-time function $g$ stretching each input by one bit such that its range intersects all infinite NP 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 K.2009 is a good candidate for $g$. We define a new hardness property of generators, the $\bigvee$-hardness, and shows that one specific gadget generator is the $\bigvee$-hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite NP sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite NP sets. △ Less

Submitted 9 November, 2023; v1 submitted 24 August, 2022; originally announced August 2022.

Comments: preliminary version August 2022, revised July 2023 and November 2023

MSC Class: 03F20; 68Q11 ACM Class: F.1.1; F.4.1

Journal ref: Bulletin of Symbolic Logic , Volume 30 , Issue 1 , March 2024 , pp. 20 - 40

Information in propositional proofs and algorithmic proof search

Authors: Jan Krajicek

Abstract: We study from the proof complexity perspective the (informal) proof search problem: Is there an optimal way to search for propositional proofs? We note that for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof system… ▽ More We study from the proof complexity perspective the (informal) proof search problem: Is there an optimal way to search for propositional proofs? We note that for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists. To characterize precisely the time proof search algorithms need for individual formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system $P$ we attach {\bf information-efficiency function} $i_P(τ)$ assigning to a tautology a natural number, and we show that: - $i_P(τ)$ characterizes time any $P$-proof search algorithm has to use on $τ$ and that for a fixed $P$ there is such an information-optimal algorithm, - a proof system is information-efficiency optimal iff it is p-optimal, - for non-automatizable systems $P$ there are formulas $τ$ with short proofs but having large information measure $i_P(τ)$. We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P(τ)$ where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search. △ Less

Submitted 5 September, 2021; v1 submitted 10 April, 2021; originally announced April 2021.

Comments: Preliminary version February 2021

Report number: ECCC (TR21-053) MSC Class: 03F20; 68Q11

Journal ref: J. of Symbolic Logic, vol.87, nb.2, (June 2022), pp.852-869

Small circuits and dual weak PHP in the universal theory of p-time algorithms

Authors: Jan Krajicek

Abstract: We prove, under a computational complexity hypothesis, that it is consistent with the true universal theory of p-time algorithms that a specific p-time function extending $n$ bits to $m \geq n^2$ bits violates the dual weak pigeonhole principle: every string $y$ of length $m$ equals the value of the function for some $x$ of length $n$. The function is the truth-table function assigning to a circui… ▽ More We prove, under a computational complexity hypothesis, that it is consistent with the true universal theory of p-time algorithms that a specific p-time function extending $n$ bits to $m \geq n^2$ bits violates the dual weak pigeonhole principle: every string $y$ of length $m$ equals the value of the function for some $x$ of length $n$. The function is the truth-table function assigning to a circuit the table of the function it computes and the hypothesis is that every language in P has circuits of a fixed polynomial size $n^d$. △ Less

Submitted 23 December, 2020; v1 submitted 24 April, 2020; originally announced April 2020.

Comments: Preprint April 2020, revision December 2020

MSC Class: 03F30; 68Q15 ACM Class: F.4.1

Journal ref: ACM Transactions on Computational Logic, 22, 2, Article 11 (May 2021)

A limitation on the KPT interpolation

Authors: Jan Krajíček

Abstract: We prove a limitation on a variant of the KPT theorem proposed for propositional proof systems by Pich and Santhanam (2020), for all proof systems that prove the disjointness of two NP sets that are hard to distinguish. We prove a limitation on a variant of the KPT theorem proposed for propositional proof systems by Pich and Santhanam (2020), for all proof systems that prove the disjointness of two NP sets that are hard to distinguish. △ Less

Submitted 11 August, 2020; v1 submitted 6 April, 2020; originally announced April 2020.

MSC Class: 03F20; 68Q15 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 3 (August 12, 2020) lmcs:6267

The Cook-Reckhow definition

Authors: Jan Krajicek

Abstract: The Cook-Reckhow 1979 paper defined the area of research we now call Proof Complexity. There were earlier papers which contributed to the subject as we understand it today, the most significant being Tseitin's 1968 paper, but none of them introduced general notions that would allow to make an explicit and universal link between lengths-of-proofs problems and computational complexity theory. In thi… ▽ More The Cook-Reckhow 1979 paper defined the area of research we now call Proof Complexity. There were earlier papers which contributed to the subject as we understand it today, the most significant being Tseitin's 1968 paper, but none of them introduced general notions that would allow to make an explicit and universal link between lengths-of-proofs problems and computational complexity theory. In this note we shall highlight three particular definitions from the paper: of proof systems, p-simulations and the pigeonhole principle formula, and discuss their role in defining the field. We will also mention some related developments and open problems. △ Less

Submitted 9 September, 2019; originally announced September 2019.

Journal ref: in: "Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook", ed.Bruce M.Kapron, Association for Computing Machinery Books, New York, NY, USA, 43, pp.83-94, May 2023

Consistency of circuit lower bounds with bounded theories

Authors: Jan Bydzovsky, Jan Krajicek, Igor C. Oliveira

Abstract: Proving that there are problems in $\mathsf{P}^\mathsf{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere circuit lower bounds is open even for pr… ▽ More Proving that there are problems in $\mathsf{P}^\mathsf{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere circuit lower bounds is open even for problems in $\mathsf{MAEXP}$. Giving the notorious difficulty of proving lower bounds that hold for all large input lengths, we ask the following question: Can we show that a large set of techniques cannot prove that $\mathsf{NP}$ is easy infinitely often? Motivated by this and related questions about the interaction between mathematical proofs and computations, we investigate circuit complexity from the perspective of logic. Among other results, we prove that for any parameter $k \geq 1$ it is consistent with theory $T$ that computational class ${\mathcal C} \not \subseteq \textit{i.o.}\mathrm{SIZE}(n^k)$, where $(T, \mathcal{C})$ is one of the pairs: $T = \mathsf{T}^1_2$ and ${\mathcal C} = \mathsf{P}^\mathsf{NP}$, $T = \mathsf{S}^1_2$ and ${\mathcal C} = \mathsf{NP}$, $T = \mathsf{PV}$ and ${\mathcal C} = \mathsf{P}$. In other words, these theories cannot establish infinitely often circuit upper bounds for the corresponding problems. This is of interest because the weaker theory $\mathsf{PV}$ already formalizes sophisticated arguments, such as a proof of the PCP Theorem. These consistency statements are unconditional and improve on earlier theorems of [KO17] and [BM18] on the consistency of lower bounds with $\mathsf{PV}$. △ Less

Submitted 16 June, 2020; v1 submitted 30 May, 2019; originally announced May 2019.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 2 (June 18, 2020) lmcs:5578

On monotone circuits with local oracles and clique lower bounds

Authors: Jan Krajicek, Igor C. Oliveira

Abstract: We investigate monotone circuits with local oracles [K., 2016], i.e., circuits containing additional inputs $y_i = y_i(\vec{x})$ that can perform unstructured computations on the input string $\vec{x}$. Let $μ\in [0,1]$ be the locality of the circuit, a parameter that bounds the combined strength of the oracle functions $y_i(\vec{x})$, and $U_{n,k}, V_{n,k} \subseteq \{0,1\}^m$ be the set of $k$-c… ▽ More We investigate monotone circuits with local oracles [K., 2016], i.e., circuits containing additional inputs $y_i = y_i(\vec{x})$ that can perform unstructured computations on the input string $\vec{x}$. Let $μ\in [0,1]$ be the locality of the circuit, a parameter that bounds the combined strength of the oracle functions $y_i(\vec{x})$, and $U_{n,k}, V_{n,k} \subseteq \{0,1\}^m$ be the set of $k$-cliques and the set of complete $(k-1)$-partite graphs, respectively (similarly to [Razborov, 1985]). Our results can be informally stated as follows. 1. For an appropriate extension of depth-$2$ monotone circuits with local oracles, we show that the size of the smallest circuits separating $U_{n,3}$ (triangles) and $V_{n,3}$ (complete bipartite graphs) undergoes two phase transitions according to $μ$. 2. For $5 \leq k(n) \leq n^{1/4}$, arbitrary depth, and $μ\leq 1/50$, we prove that the monotone circuit size complexity of separating the sets $U_{n,k}$ and $V_{n,k}$ is $n^{Θ(\sqrt{k})}$, under a certain restrictive assumption on the local oracle gates. The second result, which concerns monotone circuits with restricted oracles, extends and provides a matching upper bound for the exponential lower bounds on the monotone circuit size complexity of $k$-clique obtained by Alon and Boppana (1987). △ Less

Submitted 16 December, 2019; v1 submitted 20 April, 2017; originally announced April 2017.

Comments: Updated acknowledgements and funding information

MSC Class: F.1.1; F.2.2 ACM Class: F.1.1; F.2.2

Journal ref: Chicago Journal of Theoretical Computer Science, vol.2018, nb.1, (March 2018), pp.1-18

Randomized feasible interpolation and monotone circuits with a local oracle

Authors: Jan Krajicek

Abstract: We generalize the feasible interpolation theorem for semantic derivations from K.(1997) by allowing randomized protocols (protocols in the sense of K.(1997). We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that does correspond to communication protocols for the monotone Karchmer-Wigderson multi-function $KW^m[U,V]$ making errors. The new… ▽ More We generalize the feasible interpolation theorem for semantic derivations from K.(1997) by allowing randomized protocols (protocols in the sense of K.(1997). We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that does correspond to communication protocols for the monotone Karchmer-Wigderson multi-function $KW^m[U,V]$ making errors. The new randomized feasible interpolation thus shows that a short semantic derivation (from a certain class of derivations larger than in the original method) of the disjointness of $U, V$, $U$ closed upwards, yields a small randomized protocol for and hence a small monotone CLO separating the sets. To establish a lower bound for monotone CLOs separating two NP sets, one closed upwards, is an open problem. This research is motivated by the open problem to establish a lower bound for proof system $R(LIN)$ operating with clauses formed by linear Boolean functions over the 2-element field. The new randomized feasible interpolation applies to this proof system and also to the semantic versions of the cutting planes proof system CP (as randomized protocols efficiently simulate protocols with small real communication complexity of K.(1998)), to small width resolution over CP, R(CP), and to random resolution RR of Buss, Kolodziejczyk and Thapen (2014). △ Less

Submitted 26 June, 2018; v1 submitted 26 November, 2016; originally announced November 2016.

Comments: Preliminary version November 2016

MSC Class: 03F20; 68Q15 ACM Class: F.2.2

Journal ref: J. of Mathematical Logic, Vol.18., No. 2, 1850012 (2018)

Unprovability of circuit upper bounds in Cook's theory PV

Authors: Jan Krajicek, Igor C. Oliveira

Abstract: We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that $L \notin Size(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language. We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that $L \notin Size(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language. △ Less

Submitted 1 February, 2017; v1 submitted 1 May, 2016; originally announced May 2016.

MSC Class: 03F30; 68Q15 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 1 (February 3, 2017) lmcs:3119

A feasible interpolation for random resolution

Authors: Jan Krajicek

Abstract: Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply the general feasible interpolation theorem for semantic derivations of Krajicek (JSL, 1997) to random… ▽ More Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply the general feasible interpolation theorem for semantic derivations of Krajicek (JSL, 1997) to random resolution. As a consequence we get a lower bound for random resolution refutations of the clique-coloring formulas. △ Less

Submitted 1 February, 2017; v1 submitted 22 April, 2016; originally announced April 2016.

Comments: Preprint April 2016, revised September and October 2016

MSC Class: 03F20 (Primary); 68Q15 (Secondary) ACM Class: F.2.2

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 1 (February 3, 2017) lmcs:3120

Consistency of circuit evaluation, extended resolution and total NP search problems

Authors: Jan Krajicek

Abstract: We consider sets $Γ(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circuit with $n$ inputs is refutable in resolution R in $k$ steps. We show that every CNF shortly refutable in Extended R, ER, can be easily reduced to an instance of $Γ(0,s,k)$ (with $s,k$ depending on the size of the ER-refutation) and, in particular, that $Γ(0,s,k)$ when interpreted as a relativized NP sea… ▽ More We consider sets $Γ(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circuit with $n$ inputs is refutable in resolution R in $k$ steps. We show that every CNF shortly refutable in Extended R, ER, can be easily reduced to an instance of $Γ(0,s,k)$ (with $s,k$ depending on the size of the ER-refutation) and, in particular, that $Γ(0,s,k)$ when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory $V^1_1$. We use the ideas of implicit proofs to define from $Γ(0,s,k)$ a non-relativized NP search problem $iΓ$ and we show that it is complete among all such problems provably total in bounded arithmetic theory $V^1_2$. The reductions are definable in $S^1_2$. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them. △ Less

Submitted 10 September, 2015; originally announced September 2015.

Comments: Preliminary version 10.September 2015

MSC Class: 03F20 (Primary); 68Q15 (Secondary)

Journal ref: Forum of Mathematics, Sigma / Volume 4 / 2016, e15

Expansions of pseudofinite structures and circuit and proof complexity

Authors: Jan Krajicek

Abstract: I shall describe a general model-theoretic task to construct expansions of pseudofinite structures and discuss several examples of particular relevance to computational complexity. Then I will present one specific situation where finding a suitable expansion would imply that, assuming a one-way permutation exists, the computational class NP is not closed under complementation. I shall describe a general model-theoretic task to construct expansions of pseudofinite structures and discuss several examples of particular relevance to computational complexity. Then I will present one specific situation where finding a suitable expansion would imply that, assuming a one-way permutation exists, the computational class NP is not closed under complementation. △ Less

Submitted 1 May, 2015; originally announced May 2015.

Comments: Preliminary version May 2015

MSC Class: 03F20; 03C99; 68Q15

Journal ref: Tributes Ser. Vol.30, College Publications, London, (2016), pp.195-203

A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems

Authors: Jan Krajicek

Abstract: We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime $p$ (the so called $AC^0[p]$ Frege systems) to computational complexity lower bounds for search tasks involving search trees branching upon values of maps on the vector space of low degree polynomials over the finite filed with $p$ el… ▽ More We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime $p$ (the so called $AC^0[p]$ Frege systems) to computational complexity lower bounds for search tasks involving search trees branching upon values of maps on the vector space of low degree polynomials over the finite filed with $p$ elements. △ Less

Submitted 22 August, 2014; v1 submitted 11 November, 2013; originally announced November 2013.

Comments: the final version accepted to the Proc.AMS

MSC Class: 03F20; 68Q17

Journal ref: Proceedings of the AMS, 143(11), (2015), pp.4951-4965

On the computational complexity of finding hard tautologies

Authors: Jan Krajicek

Abstract: It is well-known (cf. K.-Pudlák 1989) that a polynomial time algorithm finding tautologies hard for a propositional proof system $P$ exists iff $P$ is not optimal. Such an algorithm takes $1^{(k)}$ and outputs a tautology $τ_k$ of size at least $k$ such that $P$ is not p-bounded on the set of all $τ_k$'s. We consider two more general search problems involving finding a hard formula, {\bf Cert} a… ▽ More It is well-known (cf. K.-Pudlák 1989) that a polynomial time algorithm finding tautologies hard for a propositional proof system $P$ exists iff $P$ is not optimal. Such an algorithm takes $1^{(k)}$ and outputs a tautology $τ_k$ of size at least $k$ such that $P$ is not p-bounded on the set of all $τ_k$'s. We consider two more general search problems involving finding a hard formula, {\bf Cert} and {\bf Find}, motivated by two hypothetical situations: that one can prove that $\np \neq co\np$ and that no optimal proof system exists. In {\bf Cert} one is asked to find a witness that a given non-deterministic circuit with $k$ inputs does not define $TAUT \cap \kk$. In {\bf Find}, given $1^{(k)}$ and a tautology $α$ of size at most $k^{c_0}$, one should output a size $k$ tautology $β$ that has no size $k^{c_1}$ $P$-proof from substitution instances of $α$. We shall prove, assuming the existence of an exponentially hard one-way permutation, that {\bf Cert} cannot be solved by a time $2^{O(k)}$ algorithm. Using a stronger hypothesis about the proof complexity of Nisan-Wigderson generator we show that both problems {\bf Cert} and {\bf Find} are actually only partially defined for infinitely many $k$ (i.e. there are inputs corresponding to $k$ for which the problem has no solution). The results are based on interpreting the Nisan-Wigderson generator as a proof system. △ Less

Submitted 18 July, 2013; v1 submitted 8 December, 2012; originally announced December 2012.

MSC Class: 03F20; 68Q15

Journal ref: Bulletin of the London Mathematical Society, 46(1), (2014), pp.111-125

A saturation property of structures obtained by forcing with a compact family of random variables

Authors: Jan Krajicek

Abstract: A method how to construct Boolean-valued models of some fragments of arithmetic was developed in Krajicek (2011), with the intended applications in bounded arithmetic and proof complexity. Such a model is formed by a family of random variables defined on a pseudo-finite sample space. We show that under a fairly natural condition on the family (called compactness in K.(2011)) the resulting structur… ▽ More A method how to construct Boolean-valued models of some fragments of arithmetic was developed in Krajicek (2011), with the intended applications in bounded arithmetic and proof complexity. Such a model is formed by a family of random variables defined on a pseudo-finite sample space. We show that under a fairly natural condition on the family (called compactness in K.(2011)) the resulting structure has a property that is naturally interpreted as saturation for existential types. We also give an example showing that this cannot be extended to universal types. △ Less

Submitted 10 August, 2012; v1 submitted 6 July, 2012; originally announced July 2012.

Comments: preprint February 2012

MSC Class: 03C90; 03C50; 03H99

Journal ref: Archive for Mathematical Logic, 52(1), pp.19-28, (2013)

Pseudo-finite hard instances for a student-teacher game with a Nisan-Wigderson generator

Authors: Jan Krajíček

Abstract: For an NP intersect coNP function g of the Nisan-Wigderson type and a string b outside its range we consider a two player game on a common input a to the function. One player, a computationally limited Student, tries to find a bit of g(a) that differs from the corresponding bit of b. He can query a computationally unlimited Teacher for the witnesses of the values of constantly many bits of g(a). T… ▽ More For an NP intersect coNP function g of the Nisan-Wigderson type and a string b outside its range we consider a two player game on a common input a to the function. One player, a computationally limited Student, tries to find a bit of g(a) that differs from the corresponding bit of b. He can query a computationally unlimited Teacher for the witnesses of the values of constantly many bits of g(a). The Student computes the queries from a and from Teacher's answers to his previous queries. It was proved by Krajicek (2011) that if g is based on a hard bit of a one-way permutation then no Student computed by a polynomial size circuit can succeed on all a. In this paper we give a lower bound on the number of inputs a any such Student must fail on. Using that we show that there is a pseudo-finite set of hard instances on which all uniform students must fail. The hard-core set is defined in a non-standard model of true arithmetic and has applications in a forcing construction relevant to proof complexity. △ Less

Submitted 10 August, 2012; v1 submitted 2 July, 2012; originally announced July 2012.

ACM Class: F.2.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (August 13, 2012) lmcs:788