3
$\begingroup$

Does there exist an algorithm, about which a non-constructive $\omega$-consistent theory $A$ can prove that it has time complexity $O(f(n))$ where $n$ is some univariate function of the input, but there is no $\omega$-consistent constructive theory which proves this bound, and there is a constructive $\omega$-consistent theory $B$, which proves that the algorithm terminates? If it is, is there such a case for a polynomial-time algorithm?

$\endgroup$
5
$\begingroup$

No (assuming $f$ is computable). By $ω$-consistency, the $O(f(n))$ bound is correct, so some $c f(n)$ bound is correct, and we can add $c f(n)$ bound (which is $Π^0_1$) as an axiom to a constructive theory.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.