1
$\begingroup$

In implicit complexity theory they construct natural programming languages that are complete for various complexity classes.

An example, while there are many others, is Bellantoni-Cook where they show that FP can be characterized by such a language (called system B).

What I'm wondering is what do successes such as Bellantoni-Cook in implicit complexity say about Cook-Reckov?

Cook-Reckov: There exists a polynomially bounded propositional proof system iff NP = coNP.

Are these languages not proof systems? Where the outputs are the propositional tautologies (or something like this).

Why does the successful construction of these languages not prove, by the Cook-Reckov theorem, that NP = coNP?

PS you could ask the same thing of descriptive complexity... why don't constructions like FO(LFP) (first-order logic with a least fixed point operator added to it, on ordered structures), by, again, the Cook-Reckov theorem, prove P=coNP? As P can be described as the problems expressible in FO(LFP) and it is a propositional proof system--how is this not the same thing as FO(LFP) is a polynomially bounded propositional proof system?

Thank you!

$\endgroup$
1
$\begingroup$

A polynomially bounded proof system is a function $M$ computable by an FP machine with the following properties:

  • For any $x$, the output $M(x)$ is a propositional tautology.
  • There exists a polynomial $p(n)$ such that for any propositional tautology $y$ there exists $x$ of size at most $p(|y|)$ such that $M(x) = y$.

Now suppose that you found a sophisticated way to describe all functions in FP, call it System R. This lets you come up with the following equivalent definition.

A polynomially bounded proof system is a function $M$ expressible in System R with the following properties:

  • For any $x$, the output $M(x)$ is a propositional tautology.
  • There exists a polynomial $p(n)$ such that for any propositional tautology $y$ there exists $x$ of size at most $p(|y|)$ such that $M(x) = y$.

As you can see, nothing has really been gained. We only changed "computable by an FP machine" with "expressible in System R".

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thank you. I assume same applies to FO(LFP) in descriptive complexity referenced in the PS above? $\endgroup$ – DeeDee Apr 9 at 21:20
  • $\begingroup$ It's exactly the same thing. $\endgroup$ – Yuval Filmus Apr 9 at 21:21
  • $\begingroup$ word thank you. $\endgroup$ – DeeDee Apr 9 at 21:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.