6
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ It's ​ " $1^n$ instead of just $n$ " ​ so the problem will be in NP. ​ ​ ​ ​ $\endgroup$ – user12859 Apr 27 '17 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 Apr 27 '17 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 Apr 27 '17 at 6:18
  • $\begingroup$ @Pontus I am trying 3SAT. No substantial progress yet. $\endgroup$ – hengxin Apr 27 '17 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 Apr 27 '17 at 8:12
4
$\begingroup$

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.

$\endgroup$
  • 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 Jun 20 '18 at 11:01
  • $\begingroup$ @Arno True, thank you for bringing that up. $\endgroup$ – cody Jun 20 '18 at 14:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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