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?