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 bounded 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.

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.

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 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$)
4. $\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}})$.
5. $\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 bounded 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.

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 bounded 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.