What does Bellantoni-Cook say about Cook-Reckov?

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!

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".

• Thank you. I assume same applies to FO(LFP) in descriptive complexity referenced in the PS above? Apr 9 '20 at 21:20
• It's exactly the same thing. Apr 9 '20 at 21:21
• word thank you. Apr 9 '20 at 21:22