<p>No Time Hierarchy theorem is known for <span class="math-container">$\mathsf{BPTIME}$</span>, however, consider the following simple modification of the definition:</p>
<blockquote>
<p>A language is in <span class="math-container">$\mathsf{ProvableBPTIME}[f(n)]$</span> if there is a randomized Turing-machine <span class="math-container">$T$</span> that decides membership with error <span class="math-container">$\le \frac 13$</span> in time <span class="math-container">$f(n)$</span> [so far usual definition of <span class="math-container">$\mathsf{BPTIME}$</span>] and it can be proved that <span class="math-container">$T$</span> accepts every <span class="math-container">$x$</span> with probability <span class="math-container">$\ge \frac 23$</span> or with probability <span class="math-container">$\le \frac 13$</span> [so there is a proof that <span class="math-container">$T$</span> satisfies the <span class="math-container">$\mathsf{BP}$</span> condition].</p>
</blockquote>
<p>Note that this definition is completely different from that of <span class="math-container">$\mathsf{PromiseBPTIME}$</span>.</p>
<p>For <span class="math-container">$\mathsf{ProvableBPTIME}$</span> there is a Time Hierarchy: On input <span class="math-container">$(T,\Psi,x)$</span>, reject if <span class="math-container">$\Psi$</span> is not a proof that <span class="math-container">$T$</span> satisfies the <span class="math-container">$\mathsf{BP}$</span> condition, otherwise simulate <span class="math-container">$T$</span> on input <span class="math-container">$(T,\Psi,x)$</span> (until our running time permits), then negate the answer. Using standard tricks, hierarchy results can be established also about <span class="math-container">$\mathsf{RTIME}$</span> and similar classes.</p>
<p>This method almost gives a Time Hierarchy theorem for <span class="math-container">$\mathsf{BPTIME}$</span> as well, the only issue is that if there is a <span class="math-container">$T$</span> that satisfies the <span class="math-container">$\mathsf{BP}$</span> condition but this cannot be proved. (Think about fast primality tests using the Generalized Riemann Hypothesis.) In fact, I find the situation quite plausible that there are some fast algorithms whose correctness cannot be proved. If this is the case, it would be quite hard to diagonalize against them with an algorithm that must provably satisfy the <span class="math-container">$\mathsf{BP}$</span> condition.</p>
<p>So my questions would be:<br />
1, Has <span class="math-container">$\mathsf{ProvableBPTIME}$</span> been defined before?<br />
2, Are there known hierarchy theorems using some kind of provability?<br />
3, Is there a way to take care somehow of the unprovably correct algorithms?</p>
<p>Related questions: <a href="https://cstheory.stackexchange.com/questions/6748/hierarchy-for-bpp-vs-derandomization">Hierarchy for BPP vs derandomization</a>, <a href="https://cstheory.stackexchange.com/questions/4458/is-there-a-quantum-equivalent-of-the-time-hierarchy-theorem">Is there a Quantum equivalent of the Time hierarchy theorem ?</a>,<br />
<a href="https://cs.stackexchange.com/questions/132936/does-promisebptime-have-a-time-hierarchy-theorem">https://cs.stackexchange.com/questions/132936/does-promisebptime-have-a-time-hierarchy-theorem</a></p>
<p><em>Update 2020/12/24:</em> Joshua pointed out that in <a href="https://doi.org/10.1137/1.9781611970395.ch6" rel="nofollow noreferrer">Chapter 6 of Hartmanis: Feasible Computations and Provable Complexity Properties</a> a similar definition was considered but only for the provability of the time/space bound <span class="math-container">$f(n)$</span> of deterministic classes. I would instead define <span class="math-container">$\mathsf{ProvableDTIME}[f(n)]$</span> as deterministic algorithms whose correctness can be proven. (Again think about primality tests using the GRH.) Then we can ask the following.</p>
<blockquote>
<p><span class="math-container">$\mathsf{DTIME}[f(n)]\neq\mathsf{ProvableDTIME}[f(n)]$</span> for some time-constructible function <span class="math-container">$f(n)$</span>?
Could <span class="math-container">$\mathsf{P}$</span> and <span class="math-container">$\mathsf{ProvableP}$</span> differ?</p>
</blockquote>

CC BY-SA 4.0
2020-12-23T21:34:52.127Z
In your definition you write: *"and it can be proved that"*.  But then you should also specify the logic fragment in which this proof is done.
Gamow
CC BY-SA 4.0
2020-12-23T22:01:47.790Z
Yes, but I didn't want to go into these details.
domotorp
CC BY-SA 4.0
2020-12-24T01:49:01.123Z
I don't remember if Hartmanis defined it for BPTIME in particular, but his monograph nicely lays out the kind of theory you're asking about, I think. See eg https://cstheory.stackexchange.com/a/36088/129
Joshua Grochow
CC BY-SA 4.0
2020-12-24T06:29:02.510Z
@Joshua Indeed the proof of his Theorem 6.3 is practically the same as the one sketched above! But he only studies provable time and space bounds for deterministic Turing machines, denoted $\mathsf{F-TIME}$ and $\mathsf{F-SPACE}$. He proves $\mathsf{F-TIME}[f(n)]\ne \mathsf{TIME}[f(n)]$ for some recursive $f(n)$, exploiting that $f(n)$ is not time-constructible.
domotorp
<cc.complexity-theory><randomness><time-hierarchy>
Provable BPP Hierarchy
domotorp
# Provable BPP Hierarchy

(Asked by: username_0 on 2020-12-23)

No Time Hierarchy theorem is known for $\mathsf{BPTIME}$, however, consider the following simple modification of the definition:

> A language is in $\mathsf{ProvableBPTIME}[f(n)]$ if there is a randomized Turing-machine $T$ that decides membership with error $\le \frac 13$ in time $f(n)$ [so far usual definition of $\mathsf{BPTIME}$] and it can be proved that $T$ accepts every $x$ with probability $\ge \frac 23$ or with probability $\le \frac 13$ [so there is a proof that $T$ satisfies the $\mathsf{BP}$ condition].

Note that this definition is completely different from that of $\mathsf{PromiseBPTIME}$.

For $\mathsf{ProvableBPTIME}$ there is a Time Hierarchy: On input $(T,\Psi,x)$, reject if $\Psi$ is not a proof that $T$ satisfies the $\mathsf{BP}$ condition, otherwise simulate $T$ on input $(T,\Psi,x)$ (until our running time permits), then negate the answer. Using standard tricks, hierarchy results can be established also about $\mathsf{RTIME}$ and similar classes.

This method almost gives a Time Hierarchy theorem for $\mathsf{BPTIME}$ as well, the only issue is that if there is a $T$ that satisfies the $\mathsf{BP}$ condition but this cannot be proved. (Think about fast primality tests using the Generalized Riemann Hypothesis.) In fact, I find the situation quite plausible that there are some fast algorithms whose correctness cannot be proved. If this is the case, it would be quite hard to diagonalize against them with an algorithm that must provably satisfy the $\mathsf{BP}$ condition.

So my questions would be:  
1, Has $\mathsf{ProvableBPTIME}$ been defined before?  
2, Are there known hierarchy theorems using some kind of provability?  
3, Is there a way to take care somehow of the unprovably correct algorithms?

Related questions: [Hierarchy for BPP vs derandomization](https://cstheory.stackexchange.com/questions/6748/hierarchy-for-bpp-vs-derandomization), [Is there a Quantum equivalent of the Time hierarchy theorem ?](https://cstheory.stackexchange.com/questions/4458/is-there-a-quantum-equivalent-of-the-time-hierarchy-theorem),  
<https://cs.stackexchange.com/questions/132936/does-promisebptime-have-a-time-hierarchy-theorem>

*Update 2020/12/24:* Joshua pointed out that in [Chapter 6 of Hartmanis: Feasible Computations and Provable Complexity Properties](https://doi.org/10.1137/1.9781611970395.ch6) a similar definition was considered but only for the provability of the time/space bound $f(n)$ of deterministic classes. I would instead define $\mathsf{ProvableDTIME}[f(n)]$ as deterministic algorithms whose correctness can be proven. (Again think about primality tests using the GRH.) Then we can ask the following.

> $\mathsf{DTIME}[f(n)]\neq\mathsf{ProvableDTIME}[f(n)]$ for some time-constructible function $f(n)$?
> Could $\mathsf{P}$ and $\mathsf{ProvableP}$ differ?

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

> **Comments:**
> **username_1**: In your definition you write: *"and it can be proved that"*.  But then you should also specify the logic fragment in which this proof is done.  
> **username_0**: Yes, but I didn't want to go into these details.  
> **username_2**: I don't remember if Hartmanis defined it for BPTIME in particular, but his monograph nicely lays out the kind of theory you're asking about, I think. See eg https://cstheory.stackexchange.com/a/36088/129  
> **username_0**: @Joshua Indeed the proof of his Theorem 6.3 is practically the same as the one sketched above! But he only studies provable time and space bounds for deterministic Turing machines, denoted $\mathsf{F-TIME}$ and $\mathsf{F-SPACE}$. He proves $\mathsf{F-TIME}[f(n)]\ne \mathsf{TIME}[f(n)]$ for some recursive $f(n)$, exploiting that $f(n)$ is not time-constructible.  

---

## 0 answers

