<p>Cook-Reckhow propositional proof systems are nonunifrom.
E.g. the computational complexity counterpart to
the class of polynomial-size $\mathsf{Extended Frege}$ proofs is 
the nonuniform complexity class $\mathsf{P/poly}$.
We have to look at their uniform counterparts: 
E.g. the proof complexity counterpart for $\mathsf{P}$ are 
bounded arithmetic theories like
Cook's theory $\mathsf{PV}$ (standing for polynomial-time verifiable),
Buss's theory $\mathsf{S}^1_2$, ...</p>

<p>Cook and Urquhart used Cook's theory $\mathsf{PV}$ 
to define a theory of higher-types polynomial-time computable functions $\mathsf{PV}^\omega$ in the following paper:</p>

<ul>
<li>Stephen A. Cook and Alasdair Urquhart, "<a href="https://www.cs.toronto.edu/~sacook/homepage/cook_urquhart.ps">Functional interpretations of feasibly constructive arithmetic</a>", 1993. <a href="http://dx.doi.org/10.1016/0168-0072(93)90044-E">doi: 10.1016/0168-0072(93)90044-E</a></li>
</ul>

<p>There has been some follow up work which you can find by looking at <a href="https://scholar.google.com/scholar?cites=10240366969495405628">articles citing this paper</a>. </p>

<p>Implicit complexity theory that Martin mentions is also influenced by this work. Check out <a href="http://www.cs.unibo.it/~martini/">Simone Martini</a>'s <a href="http://www.cs.unibo.it/~martini/BISS/">survey slides</a> and <a href="http://www.cs.unibo.it/~dallago/">Ugo Dal Lago</a>'s <a href="http://www.cs.unibo.it/~dallago/ICCHC/esslli.pdf">survey article</a> to get a picture of what is implicit complexity theory and its history.</p>

CC BY-SA 3.0
2016-05-09T06:31:47.653Z
Thank you! The Cook-Urquhart paper is indeed the kind of work I was asking about. I also found the survey paper on implicit complexity enlightening, although I disagree with the (implied) characterization of machine-independent complexity as more fundamental than language-independent complexity, especially in light of the extended Church-Turing hypothesis, that -- efficient quantum computation algorithms aside -- still holds for the most interesting computational classes. If anything, the results show that both models are equivalent enough for the classical formulation to remain canonical.
pron
CC BY-SA 3.0
2016-05-08T17:16:15.820Z
2016-05-08T19:40:12.473Z
2016-05-08T19:40:12.473Z
Kaveh
<p>An important subfield of computational complexity is <a href="http://www.karlin.mff.cuni.cz/~krajicek/ecm.pdf" rel="nofollow">proof complexity</a>, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length polynomial to the formula being proven) for all tautologies could be constructed iff $coNP$ = $NP$. Other results deal with specific propositional calculus proof systems, showing that they all have superpolynomial proof lower-bounds. Is there any work relating type systems and type inference rules to the proof systems as defined in this theory? </p>

<p>In general, a cursory examination reveals that most discussions of type systems discuss computability (decidability/undecidability) with little discussion of finer complexity bounds (which may well exist in many finite models). Is there a reason why this is so (if indeed it is so)?</p>

CC BY-SA 3.0
2016-05-08T12:50:59.990Z
Not an expert on proof complexity, but the type systems that type theorists discuss tend to be much more expressive than the classes that complexity theorists are interested in. E.g.  the simply-typed λ-calculus with primitive recursion is probably the least expressive system type theory looks at, but every recursive function whose totality can be proved in first order logic (starting from the usual axioms for the elementary data types, eg Peano for natural numbers) can be expressed. The field of "implicit computational complexity"  seeks to combine type theory with complexity theory.
Martin Berger
<proof-complexity><type-systems><proof-theory>
Is there any work relating type systems and Cook-Reckhow proof systems?
pron
# Is there any work relating type systems and Cook-Reckhow proof systems?

(Asked by: username_0 on 2016-05-08)

An important subfield of computational complexity is [proof complexity](http://www.karlin.mff.cuni.cz/~krajicek/ecm.pdf), mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length polynomial to the formula being proven) for all tautologies could be constructed iff $coNP$ = $NP$. Other results deal with specific propositional calculus proof systems, showing that they all have superpolynomial proof lower-bounds. Is there any work relating type systems and type inference rules to the proof systems as defined in this theory?

In general, a cursory examination reveals that most discussions of type systems discuss computability (decidability/undecidability) with little discussion of finer complexity bounds (which may well exist in many finite models). Is there a reason why this is so (if indeed it is so)?

**Tags:** proof-complexity, type-systems, proof-theory
> **Comments:**
> **username_1**: Not an expert on proof complexity, but the type systems that type theorists discuss tend to be much more expressive than the classes that complexity theorists are interested in. E.g.  the simply-typed λ-calculus with primitive recursion is probably the least expressive system type theory looks at, but every recursive function whose totality can be proved in first order logic (starting from the usual axioms for the elementary data types, eg Peano for natural numbers) can be expressed. The field of "implicit computational complexity"  seeks to combine type theory with complexity theory.  

---

## 1 answers

### Answer by username_2 on 2016-05-08. Score: 6 | Accepted answer

Cook-Reckhow propositional proof systems are nonunifrom.
E.g. the computational complexity counterpart to
the class of polynomial-size $\mathsf{Extended Frege}$ proofs is
the nonuniform complexity class $\mathsf{P/poly}$.
We have to look at their uniform counterparts:
E.g. the proof complexity counterpart for $\mathsf{P}$ are
bounded arithmetic theories like
Cook's theory $\mathsf{PV}$ (standing for polynomial-time verifiable),
Buss's theory $\mathsf{S}^1\_2$, ...

Cook and Urquhart used Cook's theory $\mathsf{PV}$
to define a theory of higher-types polynomial-time computable functions $\mathsf{PV}^\omega$ in the following paper:

* Stephen A. Cook and Alasdair Urquhart, "[Functional interpretations of feasibly constructive arithmetic](https://www.cs.toronto.edu/~sacook/homepage/cook_urquhart.ps)", 1993. [doi: 10.1016/0168-0072(93)90044-E](http://dx.doi.org/10.1016/0168-0072(93)90044-E)

There has been some follow up work which you can find by looking at [articles citing this paper](https://scholar.google.com/scholar?cites=10240366969495405628).

Implicit complexity theory that Martin mentions is also influenced by this work. Check out [Simone Martini](http://www.cs.unibo.it/~martini/)'s [survey slides](http://www.cs.unibo.it/~martini/BISS/) and [Ugo Dal Lago](http://www.cs.unibo.it/~dallago/)'s [survey article](http://www.cs.unibo.it/~dallago/ICCHC/esslli.pdf) to get a picture of what is implicit complexity theory and its history.

> **Comments:**
> **username_0**: Thank you! The Cook-Urquhart paper is indeed the kind of work I was asking about. I also found the survey paper on implicit complexity enlightening, although I disagree with the (implied) characterization of machine-independent complexity as more fundamental than language-independent complexity, especially in light of the extended Church-Turing hypothesis, that -- efficient quantum computation algorithms aside -- still holds for the most interesting computational classes. If anything, the results show that both models are equivalent enough for the classical formulation to remain canonical.  

---

