<p>No (assuming <span class="math-container">$f$</span> is computable).  By <span class="math-container">$ω$</span>-consistency, the <span class="math-container">$O(f(n))$</span> bound is correct, so some <span class="math-container">$c f(n)$</span> bound is correct, and we can add <span class="math-container">$c f(n)$</span> bound (which is <span class="math-container">$Π^0_1$</span>) as an axiom to a constructive theory.</p>

CC BY-SA 4.0
2018-09-29T14:59:45.657Z
2018-09-29T14:59:45.657Z
Dmytro Taranovsky
<p>Does there exist an algorithm, about which a non-constructive <span class="math-container">$\omega$</span>-consistent theory <span class="math-container">$A$</span> can prove that it has time complexity <span class="math-container">$O(f(n))$</span> where <span class="math-container">$n$</span> is some univariate function of the input, but there is no <span class="math-container">$\omega$</span>-consistent constructive theory which proves this bound, and there is a constructive <span class="math-container">$\omega$</span>-consistent theory <span class="math-container">$B$</span>, which proves that the algorithm terminates? If it is, is there such a case for a polynomial-time algorithm?</p>

<cc.complexity-theory><time-complexity>
Does a non-constructive proof of bounds of a computable asymptotic complexity, with impossible fix, exist?
Ilk
# Does a non-constructive proof of bounds of a computable asymptotic complexity, with impossible fix, exist?

(Asked by: username_0 on 2018-09-28)

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?

**Tags:** cc.complexity-theory, time-complexity

---

## 1 answers

### Answer by username_1 on 2018-09-29. Score: 5 | Accepted answer

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.


---

