# How to prove that finding math proofs is $\text{NP}$-hard?

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?

• It's ​ " $1^n$ instead of just $n$ " ​ so the problem will be in NP. ​ ​ ​ ​ – user12859 Apr 27 '17 at 4:28
• @RickyDemer I got it. $1^n$ means the length of the proof which is $n$ in unary instead of in binary. Thanks. – hengxin Apr 27 '17 at 4:45
• Have you tried reducing from SAT? I imagine it should be possible by mostly using the first-order logic underpinnings of ZF. – Pontus Apr 27 '17 at 6:18
• @Pontus I am trying 3SAT. No substantial progress yet. – hengxin Apr 27 '17 at 8:01
• 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. – Pontus Apr 27 '17 at 8:12

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.

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