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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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