Questions tagged [proof-complexity]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2
votes
0answers
104 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 ...
8
votes
1answer
462 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
2answers
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
2answers
501 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
1answer
169 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
0answers
249 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
1answer
117 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
3answers
945 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
2answers
539 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
1answer
644 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
1answer
535 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
0answers
237 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 ...
68
votes
31answers
8k 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 ...