<p>One can be more precise than &quot;non-elementary&quot; and say that HOQBF is <strong>TOWER-complete</strong> — morally, TOWER is the complexity class just beyond elementary. This fact is explicitly stated and proved in <a href="https://drops.dagstuhl.de/opus/volltexte/2022/16831/" rel="nofollow noreferrer">the MFCS'22 paper <em>Higher-Order Quantified Boolean Satisfiability</em> by  Chistikov, Haase, Hadizadeh &amp; Mansutti</a>.</p>
<p>In fact, while TOWER-completeness is a semi-recent notion, <a href="https://arxiv.org/abs/1312.5686" rel="nofollow noreferrer">introduced by Schmitz less than a decade ago</a>, older proofs of non-elementary lower bounds for various problems tend to be implicitly readable as actually proving TOWER-hardness. Chistikov et al. make some historical remarks that converge with yours (I've taken the liberty of expanding the numerical references e.g. [30] into more informative ones):</p>
<blockquote>
<p>Statman […] shows that checking whether two λ-terms of the calculus reduce to the same normal form is non-elementary recursive (in fact, it shows that the problem is TOWER-complete).</p>
<p>[…]</p>
<p>According to [<em>The typed λ-calculus is not elementary recursive</em>, Statman 1979], TOWER-completeness of the satisfiability problem of Ω was announced
by Meyer in [<em>The inherent computational complexity of theories of ordered sets</em>, Theorem 1(7)] as part of a forthcoming paper coauthored with Fischer. To
the best of our knowledge, the latter paper was never published. To resolve this issue, in [<em>A simple proof of a theorem of Statman</em>]
Mairson gives a revision of [Statman 1979] that provides a standalone proof of the TOWER-hardness of
Ω and a simplification to the aforementioned Church encoding.</p>
</blockquote>

CC BY-SA 4.0
2022-11-05T02:49:44.547Z
great to see that there is finally a good reference for this result, just under 50 years later!
Noam Zeilberger
CC BY-SA 4.0
2022-11-04T14:51:28.703Z
2022-11-04T14:51:28.703Z
Lê Thành Dũng 'Tito' Nguyễn
<p>$\newcommand\iddots{⋰}$In <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048" rel="nofollow">"A simple proof of a theorem of Statman"</a> (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda calculus is not elementary recursive, i.e., cannot be done in time $O(2^{\iddots^{2^n}})$ for any finite tower of exponentials.  It's a nice proof, that works by showing how to encode arbitrary formulas of what Mairson calls "higher-order type theory" as simply typed terms, such that a formula is valid iff the corresponding term evaluates to the <a href="https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans" rel="nofollow">Church boolean</a> $true = \lambda x.\lambda y.x$.  The phrase "higher-order type theory" sounds ambiguous to me, so for the purpose of this post I will just call these <em>higher-order quantified boolean formulas</em> (HOQBF) &mdash; please let me know if there is a more standard terminology.</p>

<p>HOQBF can be seen as a generalization of <a href="https://en.wikipedia.org/wiki/QBF#Overview" rel="nofollow">QBF</a>, where quantifiers can range not just over the set of booleans $\mathbb{B} = \{ \mathbf{true}, \mathbf{false} \}$, but over sets of booleans $P(\mathbb{B})$, sets of sets of booleans $P(P(\mathbb{B}))$, and so on.  In other words, the language of formulas is
$$
F ::= \forall x^k.F \mid \exists x^k.F  \mid F\wedge F \mid F \vee F \mid \neg F \mid x^k \in y^{k+1}
$$
where the $k$ are natural numbers, and where variables $x^k$ are interpreted as ranging over $P^k(\mathbb{B})$.  (Again, is there a standard name for such formulas?)</p>

<p>Mairson cites</p>

<ul>
<li>A. R. Meyer. The inherent computational complexity of theories of ordered sets. Proceedings of the International Congress of Mathematicians, 1974.</li>
</ul>

<p>for the result that deciding formulas of HOQBF requires nonelementary time.  I checked <a href="http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TM-054.pdf" rel="nofollow">that paper</a>, and unless I'm overlooking something it doesn't contain a direct proof of this result.  I'm not 100% sure it contains a statement of it either...what looks most relevant is the theorem on page 4, which cites a list of results that various decision problems are nonelementary, including "7. The theory of pure finite types [M. Fischer and Meyer, FM75]".  Naturally, the bibliography includes the line </p>

<blockquote>
  <p>[FM75] Fischer, M.J. and A.R. Meyer, (1975), in preparation.</p>
</blockquote>

<p>and I can't find <a href="https://www.google.fr/search?q=fischer+meyer+&quot;pure+finite+types&quot;" rel="nofollow">much evidence</a> that such a paper ever surfaced.</p>

<p>I do believe the claim that deciding HOQBF requires nonelementary time, and moreover Mairson's paper also gives a separate encoding of Turing machines in simply typed lambda calculus, which computes the result of running the machine for any tower of exponential steps &mdash; so I suppose it might be possible to complete the circle and try to reduce the problem of deciding $\beta\eta$-equality of simply typed lambda terms back to HOQBF. Still, it would be nice to know if there is a classical reference for this result.</p>

<p><strong>Question:</strong> Is there a reference for the result that deciding HOQBF requires nonelementary time? (<em>Side question</em>: Is there a standard name for HOQBF?)</p>

<hr>

<p><strong>Update (June 17):</strong> So I finally went ahead and looked at <a href="https://deepblue.lib.umich.edu/bitstream/handle/2027.42/23535/0000494.pdf?sequence=1&amp;isAllowed=y" rel="nofollow">Statman's original paper</a>, and it seems that Mairson got his citation from there!  Statman begins by defining these formulas, which he calls "$\Omega$-sentences", then states the result that deciding whether they are true is non-elementary. This is listed as "Proposition 1 (Fischer and Meyer, Statman)", stated without proof, but with a citation to the Meyer survey paper (<a href="http://www.mathunion.org/ICM/ICM1974.2/Main/icm1974.2.0477.0482.ocr.pdf" rel="nofollow">conference version</a>) and the specific item "7" of the theorem I had in mind (which cites the [FM75] paper I have been unable to locate). Since Meyer is actually listed as the handling editor for Statman's paper, I'm beginning to suspect that there may not exist a more canonical reference for this...</p>

CC BY-SA 3.0
2016-06-03T10:51:25.257Z
Have you asked Harry?
Neel Krishnaswami
CC BY-SA 3.0
2016-06-03T13:05:06.330Z
Isn't it kind of straight forward that it is not elementary or am I missing something? It seems easy to show that the problem is k-Exp-hard for all k: with a level k existential quantiser we can guess the computation and expressing that it is a valid accepting computation is not different from SAT.
Kaveh
CC BY-SA 3.0
2016-06-03T14:03:57.100Z
@NeelKrishnaswami No, but that's worth a shot!
Noam Zeilberger
CC BY-SA 3.0
2016-06-03T14:08:18.920Z
@Kaveh As I said, I believe the claim, but I'm interested in original references -- even a paper that just goes through the work of setting up the decision problem for HOQBF (and giving it a name!).
Noam Zeilberger
CC BY-SA 3.0
2016-06-03T14:11:29.950Z
...and actually, a modern textbook account would be great as well.
Noam Zeilberger
CC BY-SA 3.0
2016-06-03T19:08:59.753Z
@NeelKrishnaswami Got a quick response! Alas, though, he does not have any more information about the source.
Noam Zeilberger
CC BY-SA 3.0
2016-06-07T18:21:45.837Z
[HO](https://en.wikipedia.org/wiki/HO_(complexity)), [HO on zoo](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:H#ho), the reference seems to be [doi:10.1016/j.tcs.2006.01.009](https://dx.doi.org/10.1016%2Fj.tcs.2006.01.009)
Kaveh
CC BY-SA 3.0
2016-06-07T19:12:46.563Z
HO seems to be related to what I'm asking about, but not quite the same thing.  [HT06] is a result in [descriptive complexity theory](https://en.wikipedia.org/wiki/Descriptive_complexity_theory): they show that the class of languages which can be expressed by (i.e., represented as the collection of finite models of) formulas in higher-order logic is precisely the class ELEMENTARY.  My question is about something different -- the complexity of the decision procedure for higher-order quantified boolean formulas -- although it's quite possibly related.
Noam Zeilberger
CC BY-SA 3.0
2016-06-08T15:20:23.090Z
I stumbled on HO while looking for something else and taught it is relevant since satisfiability contains evaluation (consider an HO formula with no free variable), if evaluation is hard for elementary satisfiability is also. I think there is an easy translation between HO formulas and higher order boolean formulas similar to O(1) depth QBF and SO.
Kaveh
<cc.complexity-theory><reference-request><type-theory><descriptive-complexity>
reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary
Noam Zeilberger
# reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary

(Asked by: username_0 on 2016-06-03)

$\newcommand\iddots{⋰}$In ["A simple proof of a theorem of Statman"](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048) (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda calculus is not elementary recursive, i.e., cannot be done in time $O(2^{\iddots^{2^n}})$ for any finite tower of exponentials. It's a nice proof, that works by showing how to encode arbitrary formulas of what Mairson calls "higher-order type theory" as simply typed terms, such that a formula is valid iff the corresponding term evaluates to the [Church boolean](https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans) $true = \lambda x.\lambda y.x$. The phrase "higher-order type theory" sounds ambiguous to me, so for the purpose of this post I will just call these *higher-order quantified boolean formulas* (HOQBF) — please let me know if there is a more standard terminology.

HOQBF can be seen as a generalization of [QBF](https://en.wikipedia.org/wiki/QBF#Overview), where quantifiers can range not just over the set of booleans $\mathbb{B} = \{ \mathbf{true}, \mathbf{false} \}$, but over sets of booleans $P(\mathbb{B})$, sets of sets of booleans $P(P(\mathbb{B}))$, and so on. In other words, the language of formulas is
$$
F ::= \forall x^k.F \mid \exists x^k.F \mid F\wedge F \mid F \vee F \mid \neg F \mid x^k \in y^{k+1}
$$
where the $k$ are natural numbers, and where variables $x^k$ are interpreted as ranging over $P^k(\mathbb{B})$. (Again, is there a standard name for such formulas?)

Mairson cites

* A. R. Meyer. The inherent computational complexity of theories of ordered sets. Proceedings of the International Congress of Mathematicians, 1974.

for the result that deciding formulas of HOQBF requires nonelementary time. I checked [that paper](http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TM-054.pdf), and unless I'm overlooking something it doesn't contain a direct proof of this result. I'm not 100% sure it contains a statement of it either...what looks most relevant is the theorem on page 4, which cites a list of results that various decision problems are nonelementary, including "7. The theory of pure finite types [M. Fischer and Meyer, FM75]". Naturally, the bibliography includes the line

> [FM75] Fischer, M.J. and A.R. Meyer, (1975), in preparation.

and I can't find [much evidence](https://www.google.fr/search?q=fischer+meyer+) that such a paper ever surfaced.

I do believe the claim that deciding HOQBF requires nonelementary time, and moreover Mairson's paper also gives a separate encoding of Turing machines in simply typed lambda calculus, which computes the result of running the machine for any tower of exponential steps — so I suppose it might be possible to complete the circle and try to reduce the problem of deciding $\beta\eta$-equality of simply typed lambda terms back to HOQBF. Still, it would be nice to know if there is a classical reference for this result.

**Question:** Is there a reference for the result that deciding HOQBF requires nonelementary time? (*Side question*: Is there a standard name for HOQBF?)

---

**Update (June 17):** So I finally went ahead and looked at [Statman's original paper](https://deepblue.lib.umich.edu/bitstream/handle/2027.42/23535/0000494.pdf?sequence=1&isAllowed=y), and it seems that Mairson got his citation from there! Statman begins by defining these formulas, which he calls "$\Omega$-sentences", then states the result that deciding whether they are true is non-elementary. This is listed as "Proposition 1 (Fischer and Meyer, Statman)", stated without proof, but with a citation to the Meyer survey paper ([conference version](http://www.mathunion.org/ICM/ICM1974.2/Main/icm1974.2.0477.0482.ocr.pdf)) and the specific item "7" of the theorem I had in mind (which cites the [FM75] paper I have been unable to locate). Since Meyer is actually listed as the handling editor for Statman's paper, I'm beginning to suspect that there may not exist a more canonical reference for this...

**Tags:** cc.complexity-theory, reference-request, type-theory, descriptive-complexity
> **Comments:**
> **username_1**: Have you asked Harry?  
> **username_2**: Isn't it kind of straight forward that it is not elementary or am I missing something? It seems easy to show that the problem is k-Exp-hard for all k: with a level k existential quantiser we can guess the computation and expressing that it is a valid accepting computation is not different from SAT.  
> **username_0**: @NeelKrishnaswami No, but that's worth a shot!  
> **username_0**: @Kaveh As I said, I believe the claim, but I'm interested in original references -- even a paper that just goes through the work of setting up the decision problem for HOQBF (and giving it a name!).  
> **username_0**: ...and actually, a modern textbook account would be great as well.  
> **username_0**: @NeelKrishnaswami Got a quick response! Alas, though, he does not have any more information about the source.  
> **username_2**: [HO](https://en.wikipedia.org/wiki/HO_(complexity)), [HO on zoo](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:H#ho), the reference seems to be [doi:10.1016/j.tcs.2006.01.009](https://dx.doi.org/10.1016%2Fj.tcs.2006.01.009)  
> **username_0**: HO seems to be related to what I'm asking about, but not quite the same thing.  [HT06] is a result in [descriptive complexity theory](https://en.wikipedia.org/wiki/Descriptive_complexity_theory): they show that the class of languages which can be expressed by (i.e., represented as the collection of finite models of) formulas in higher-order logic is precisely the class ELEMENTARY.  My question is about something different -- the complexity of the decision procedure for higher-order quantified boolean formulas -- although it's quite possibly related.  
> **username_2**: I stumbled on HO while looking for something else and taught it is relevant since satisfiability contains evaluation (consider an HO formula with no free variable), if evaluation is hard for elementary satisfiability is also. I think there is an easy translation between HO formulas and higher order boolean formulas similar to O(1) depth QBF and SO.  

---

## 1 answers

### Answer by username_3 on 2022-11-04. Score: 3 | Accepted answer

One can be more precise than "non-elementary" and say that HOQBF is **TOWER-complete** — morally, TOWER is the complexity class just beyond elementary. This fact is explicitly stated and proved in [the MFCS'22 paper *Higher-Order Quantified Boolean Satisfiability* by Chistikov, Haase, Hadizadeh & Mansutti](https://drops.dagstuhl.de/opus/volltexte/2022/16831/).

In fact, while TOWER-completeness is a semi-recent notion, [introduced by Schmitz less than a decade ago](https://arxiv.org/abs/1312.5686), older proofs of non-elementary lower bounds for various problems tend to be implicitly readable as actually proving TOWER-hardness. Chistikov et al. make some historical remarks that converge with yours (I've taken the liberty of expanding the numerical references e.g. [30] into more informative ones):

> Statman […] shows that checking whether two λ-terms of the calculus reduce to the same normal form is non-elementary recursive (in fact, it shows that the problem is TOWER-complete).
>
> […]
>
> According to [*The typed λ-calculus is not elementary recursive*, Statman 1979], TOWER-completeness of the satisfiability problem of Ω was announced
> by Meyer in [*The inherent computational complexity of theories of ordered sets*, Theorem 1(7)] as part of a forthcoming paper coauthored with Fischer. To
> the best of our knowledge, the latter paper was never published. To resolve this issue, in [*A simple proof of a theorem of Statman*]
> Mairson gives a revision of [Statman 1979] that provides a standalone proof of the TOWER-hardness of
> Ω and a simplification to the aforementioned Church encoding.

> **Comments:**
> **username_0**: great to see that there is finally a good reference for this result, just under 50 years later!  

---

