This is Exercise 2.11 of the book "Computational Complexity: A Modern Approach" by Arora and Barak.

Mathematics can be axiomatized using for example the Zermelo-Frankel system, which has a finite description. Argue at a high level that the following language is $\text{NP}$-complete. (You don't need to know anything about ZF.)

$$\text{THEOREMS} = \{ \langle \varphi, 1^n \rangle: \text{math statement } \varphi \text{ has a proof of size at most } n \text{ in the ZF system}. \}$$

It is easy to show that $\text{THEOREM} \in \text{NP}$. However, how to prove it is $\text{NP}$-hard?

In addition, why is it $1^n$ instead of just $n$ in $\langle \varphi , 1^n \rangle$? Does this encoding scheme matter with the $\text{NP}$-hardness proof?

  • 1
    $\begingroup$ It's ​ " $1^n$ instead of just $n$ " ​ so the problem will be in NP. ​ ​ ​ ​ $\endgroup$
    – user12859
    Commented Apr 27, 2017 at 4:28
  • $\begingroup$ @RickyDemer I got it. $1^n$ means the length of the proof which is $n$ in unary instead of in binary. Thanks. $\endgroup$
    – hengxin
    Commented Apr 27, 2017 at 4:45
  • 3
    $\begingroup$ Have you tried reducing from SAT? I imagine it should be possible by mostly using the first-order logic underpinnings of ZF. $\endgroup$
    – Pontus
    Commented Apr 27, 2017 at 6:18
  • $\begingroup$ @Pontus I am trying 3SAT. No substantial progress yet. $\endgroup$
    – hengxin
    Commented Apr 27, 2017 at 8:01
  • $\begingroup$ An instance of SAT (or 3SAT) is essentially a formula of the form $\exists x_1, \ldots, x_m: \phi(x_1, \ldots, x_m)$ where $\phi$ is a formula in propositional logic. It shouldn't be hard to encode this in first-order logic, but I only know ZF superficially, so I may be missing something. $\endgroup$
    – Pontus
    Commented Apr 27, 2017 at 8:12

1 Answer 1


Define $\mathrm{Bool}$ to be the set of all subsets of $\{\varnothing\}$ (or some arbitrary set with 1 element). Then represent a propositional variable $x$ by some subset $x\in\mathrm{Bool}$, i.e. $x\subseteq\{\varnothing\}$.

Now there is an extremely straightforward translation $\rho$ of propositional formulae into such subsets:

  • $\rho(x)$ if $x$ is a variable is just some set (also called $x$) $\in\mathrm{Bool}$.
  • $\rho(\neg\phi)$ into the complement of $\rho(\phi)$ in $\mathrm{Bool}$.
  • $\rho(\psi\vee\phi)=\rho(\psi)\cup\rho(\phi)$
  • $\rho(\phi\wedge\psi)=\rho(\psi)\cap\rho(\phi)$

And you don't need any other connectives to get a polynomial sized translation of a propositional formula.

Then a formula $\phi$ is satisfiable iff $$ ZF\vdash\exists x_1\ldots x_n\in\mathrm{Bool},\ \rho(\phi) \neq \varnothing$$

I'll let you work out the details. One important thing, though, is to show that a proof will be proportional in length to $n$, where $n$ is the number of variables.

  • 2
    $\begingroup$ To nitpick: This only works if ZF actually is sound. This is of course rather tame assumption, but an important issue, see this question: cs.stackexchange.com/questions/93172/… $\endgroup$
    – Arno
    Commented Jun 20, 2018 at 11:01
  • $\begingroup$ @Arno True, thank you for bringing that up. $\endgroup$
    – cody
    Commented Jun 20, 2018 at 14:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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