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 &quot;computable by an FP machine&quot; with &quot;expressible in System R&quot;.