Journal of Symbolic Logic · 1994 · 43 citations · 7 references
ComputingComputer ScienceMathematicsAlgorithmsCombinatoricsTheory Of ComputationArithmetic FunctionsComputability TheoryComputational ComplexityRecursion TheoryKönig's TheoremPolynomial-time AlgorithmsRecursive Functions
Abstract We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.
7