# Questions tagged [proof-complexity]

Proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements.

21
questions

1
vote

2
answers

82
views

### Hardness of a Hybrid problem combining knapsack and scheduling

I am trying to prove whether the following problem is NP-hard or not:
Items with a certain length arrive in a fixed sequence and must be assigned to one of two containers which are constrained in ...

5
votes

2
answers

580
views

### MIP*=RE theorem and its impact on logic and proof theory

In the monumental paper MIP*=RE five authors, Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, and Henry Yuen, managed to show that two complexity classes: RE and MIP* do in fact coincide. ...

0
votes

0
answers

82
views

### 1-degree SOS proof refutes Linear Programming

I am trying to understand Sums-of-Squares proof systems.
A degree $d$ Sums-of-Squares refutation for a set of polynomial equations $P = \{p_1(x) = 0, ..., p_m(x) = 0\}$ is defined as
$\sum_{i=1}^m g_i(...

9
votes

4
answers

2k
views

### Computational complexity theoretic incompleteness: is that a thing?

Has anyone done research in an area that I have not heard of but that I want to call "Computational complexity theoretic incompleteness", which would mean not absolute incompleteness in the ...

3
votes

1
answer

77
views

### Does extended Frege p-simulate circuit Frege with substitutions?

Consider propositional logic.
Frege systems are textbook-style proof systems, with a finite set of logically sound axioms and rules. However you can generalise each axiom/rule with substitutions, ...

3
votes

1
answer

1k
views

### When do you get to the point of writing proofs that need to be so complicated that verifying the details becomes a great burden on others?

Keyword here is need, many people thought I meant this intentionally rather than as an inevitability. I recently reread the article on Fukaya's work at Quanta and looked into the situation a bit more ...

3
votes

0
answers

59
views

### Explicit tautologies requiring lots/few uses of modus ponens in minimal proofs

I am interested in minimal length proofs of tautologies in propositional logic. For concreteness, let's fix a particular Frege system $F$ (i.e., sound and complete set of axioms and deduction rules ...

5
votes

3
answers

599
views

### Zero-knowledge proof for $P \ne NP$?

In computational complexity, $P \ne NP$ is a widely believed conjecture. Suppose that someone discovered a proof for it. He wants to publish a proof that he correctly proved the conjecture. I am aware ...

3
votes

0
answers

128
views

### Lengths of proofs and quasilinear time

Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care ...

10
votes

1
answer

813
views

### Is there good reference for proof complexity?

I am asking if there are some good or standard references for proof complexity theory? I didn't find references when I search in internet. Thanks!

12
votes

2
answers

2k
views

### Connections between Complexity Theory & Set Theory

Inspired by Joshua Grochow and Iddo Tzameret's answers in a post on http://cstheory.stackexchange.com , I would like to get more references on possible connections between complexity theory and set ...

10
votes

2
answers

592
views

### Bounded Arithmetic vs Complexity Theory

In this post, when I talk about bounded arithmetic theories,
I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^...

7
votes

1
answer

237
views

### Oracle queries asked in parallel

Definition: Assume that $\phi(q)$ is of the form $\exists y \leq 2^{p(n)} \varphi(q,y)$, where $p$ is a polynomial and $n = |q|$ (i.e. $n$ is the length of the binary representation of $q$). Then a ...

5
votes

0
answers

259
views

### Is there a program for theory of incompleteness in NP?

Motivated by Suresh's post, Techniques for showing that problem is in hardness limbo, it seems that there might be an underlying theory that explains why some of these problems can not be complete for ...

4
votes

1
answer

134
views

### Results where complexity bounds implies finite number of test cases

We have all been there, when a formula works for the first 30 parameters,
but it is not sufficient for a proof. My question is where one can actually just check a finite number of cases, to conclude ...

16
votes

3
answers

1k
views

### Finite versions of Godel' s incompleteness

Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...

3
votes

2
answers

574
views

### Measure of progress towards a proof

Can one define some measure of progress towards a proof of a statement? I'm not sure if it's even possible for general first order logic statements so let's restrict ourselves to propositional ...

4
votes

1
answer

713
views

### Proof system with same complexity as "informal mathematics"?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal ...

4
votes

1
answer

619
views

### Proof systems and their hierarchy

Why ZFC is placed in top of the proof system hierarchy? How it can p-simulate other systems?

3
votes

0
answers

252
views

### Oracle separating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)

Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?
Such an oracle ...

73
votes

31
answers

9k
views

### Can infinity shorten proofs a lot?

I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...