2
$\begingroup$

Let $\mathcal{L}'=\{+,\cdot,0,S,=,<,||,\#,R\}$ be the lanugage of bounded arithmetic with a $k$-ary relation $R$.

For every bounded sentence $\phi({\bf\bar{n}})$ in $\mathcal{L}'$ define propositional formula $\left <\phi({\bf\bar{n}})\right >$ inductivly as follows:

  1. $\left <\phi({\bf\bar{n}})\right >$ is the formula $\top$/$\bot$, if $\phi({\bf\bar{n}})$ is of the form $s({\bf\bar{n}})=t({\bf\bar{n}})$ and $\mathbb{N}\models s({\bf\bar{n}})=t({\bf\bar{n}})$/$\mathbb{N}\not\models s({\bf\bar{n}})=t({\bf\bar{n}})$.
  2. $\left <\phi({\bf\bar{n}})\right >$ is the formula $\top$/$\bot$, if $\phi({\bf\bar{n}})$ is of the form $s({\bf\bar{n}})<t({\bf\bar{n}})$ and $\mathbb{N}\models s({\bf\bar{n}})<t({\bf\bar{n}})$/$\mathbb{N}\not\models s({\bf\bar{n}})<t({\bf\bar{n}})$.
  3. $\left <\phi({\bf\bar{n}})\right >$ is the atomic formula $p_{n_1,...,n_k}$, if $\phi({\bf \bar{n}})$ is of the form $R(\bar{n_1},...,\bar{n_k})$.
  4. $\left <\phi({\bf\bar{n}})\right >$ is the formula $\left <\psi({\bf\bar{n}})\right > \circ \left <\eta({\bf\bar{n}})\right >$, if $\phi({\bf\bar{n}})$ is of the form $\psi({\bf\bar{n}}) \circ \eta({\bf\bar{n}})$ where $\circ \in \{\land,\lor, \to\}$.($\neg A := A\to \bot$)
  5. $\left <\phi({\bf \bar{n}})\right >$ is the formula $\bigwedge_{i=0}^{t({\bf \bar{n}})}\left <\psi(i,{\bf \bar{n}})\right >$, if $\phi({\bf\bar{n}})$ is of the form $\forall x<t({\bf \bar{n}}) \psi(x,{\bf \bar{n}})$.
  6. $\left <\phi({\bf \bar{n}})\right >$ is the formula $\bigvee_{i=0}^{t({\bf \bar{n}})}\left <\psi(i,{\bf \bar{n}})\right >$, if $\phi({\bf\bar{n}})$ is of the form $\exists x<t({\bf \bar{n}}) \psi(x,{\bf \bar{n}})$.

Let $[P=NP]_{(\bar{e},\bar{n})}$ be a $\Pi_1$ formula in the language of bounded arithmetic that says for every $x$, output of the Turing machine with code $\bar{e}$ on input $x$ after $|x|^{\bar{n}}+\bar{n}$ steps is $1$ iff $SAT(x)$ and $0$ otherwise.

Also, let $prove(x,y)$ be a bounded formula in the language of arithmetic which it says $x$ is the code of the Hilbert-style proof of propositional formula with code $y$.

Q. Fix $\bar{e}$ and $\bar{n}$. Is there any $\Sigma_0^b$ formula $\phi({\bf x})$ in $\mathcal{L}'$ such that for some bounded arithmetic like $\bf T^1_2$ and term $t({\bf x})$ in $\mathcal{L}'$, ${\bf T}^1_2\vdash [P=NP]_{(\bar{e},\bar{n})} \leftrightarrow \forall {\bf n} \exists y < t({\bf n}) prove(y,\ulcorner \left < \phi({\bf n})\right > \urcorner)$?

Thanks.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ The way it is written, e.g. the formula $x=x$ works for $\phi(x)$. Did you forget some conditions? $\endgroup$
    – Emil Jeřábek
    Jan 12, 2017 at 20:13
  • $\begingroup$ @EmilJeřábek: You are right. It should be $\leftrightarrow$ instead of $\to$. I edited my post. Thanks a lot $\endgroup$
    – Erfan Khaniki
    Jan 12, 2017 at 22:19
  • $\begingroup$ The right-hand side of the equivalence does not really make sense unless $\phi$ is $\Sigma^b_0$ (sharply bounded). If $\phi$ contains a non-sharply bounded quantifier, the length of $\langle\phi(n)\rangle$ is at least polynomial in $n$, hence exponential in the length of $n$. Thus, first, in a theory in which exponentiation is not total, $\langle\phi(n)\rangle$ is not even well-defined unless $n\in\mathit{Log}$, and even then it cannot have a Frege proof with code $t(n)$ (hence length $O(\log n)$) for any sufficiently large $n$, as the length of the proof is at least the length of the formula. $\endgroup$
    – Emil Jeřábek
    Jan 13, 2017 at 8:59
  • $\begingroup$ @EmilJeřábek: Actually I wanted to write my question in the language of arithmetic $\mathcal{L}_1=\{+,\cdot,S,0,=,<,R \}$. But I thought that language of bounded arithmetic is easier to work with and I forgot the fact that $\Delta_0$ formulas in $\mathcal{L}_1$ are $\Sigma_0^b$ formulas in $\mathcal{L}'$. I edited my post. Thanks. $\endgroup$
    – Erfan Khaniki
    Jan 13, 2017 at 14:26

0

Reset to default

Your Answer

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