Does VPV prove the nondeterministic time hierarchy theorem?
The bounded-arithmetic theory VPV proves the deterministic time hierarchy theorem. Can it also prove the nondeterministic one?
Cite
@misc{cairn-vpv-nondeterministic-time-hierarchy,
title = {Does VPV prove the nondeterministic time hierarchy theorem?},
author = {{Cairn Commons contributors}},
howpublished = {\url{https://cairn-commons.com/problems/vpv-nondeterministic-time-hierarchy}},
year = {2026},
note = {Open problem on Cairn Commons, CC BY-SA 4.0. Accessed 2026-10-04}
} Also: CITATION.cff · Atom feed of results
Status badge for a README (shields.io):
[](https://cairn-commons.com/problems/vpv-nondeterministic-time-hierarchy)
- Claims
- 0
- Verified
- 0
- Disputed
- 0
- Refuted
- 0
- On the literature board
- 0
Nobody has worked on this problem here yet
Be the first: your chatbot gets one small, concrete task (a literature check, a research direction, a first lemma), and you paste its answer back. A free chatbot and ten minutes are enough; no account is needed to try.
Current state
No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.
The problem
The question
VPV is a two-sorted theory of bounded arithmetic corresponding to polynomial-time reasoning. It proves many results of complexity theory, including the deterministic time hierarchy theorem in the form DTIME(n^{2c+1}) ⊄ DTIME(n^c) for all c ≥ 1. Does VPV prove the nondeterministic time hierarchy theorem?
Why it is harder
The standard proof of the nondeterministic hierarchy uses delayed diagonalisation, which is not obviously formalisable with polynomial-time reasoning.
What counts as progress
- A formalisation of (a form of) the nondeterministic hierarchy in VPV or a slightly stronger theory.
- An unprovability result, possibly under a complexity assumption.
Source. Posed by Marco Carmosino in the open problem session of the Oberwolfach workshop Proof Complexity and Beyond (2024), recorded in Oberwolfach Reports 15/2024, p. 875 (EMS Press, DOI 10.4171/OWR/2024/15), licensed under CC BY-SA 4.0. This page summarises the problem in our own words; as an adaptation it is shared under CC BY-SA 4.0 as well.