Set theory that proves that if its consistient, is only proves true things about arithmetic Is there a computable ω-consistent set theory $Q = ZFC + T$ (for some set of statements $T$), such that for every statement $s$ in the language of arithmetic, $Q$ proves $Con(Q) \implies (\mathbb N \models s \iff Q \vdash (\mathbb N \models s))$?
One candidate for $Q$ is $Q := ZFC + (Con(Q) \implies T(p,<x,y,z,
\dots>):Q \vdash (\mathbb N \models p(x,y,z,\dots))\text{ satisfies the Tarski recursive definition of truth})$, (this can be done via quining). I do not know if its ω-consistent though (or even consistient).
 A: The answer is no (unless I'm missing something).
Take $s$ to be $Con(Q)$. Then ZFC proves $Con(Q)\iff\mathbb{N}\models s$, trivially. But then $Q$ proves $$Con(Q)\implies (Con(Q)\iff Q\vdash Con(Q)).$$ Since ZFC proves the second incompleteness theorem, however, this means $Q\vdash\neg Con(Q)$. But this can't happen if $Q$ is $\omega$-consistent.
In more detail: the second incompleteness theorem in this context essentially says $Q\vdash Con(Q)\implies\neg Con(Q)$. So $Q$ proves $Con(Q)\implies\neg Con(Q)$, which itself is just $\neg Con(Q)$. Note that we only used one direction of your property here: in fact, you can replace what you wrote with the seemingly weaker requirement "for each $s$, $Q$ proves $Con(Q)\implies(Q\vdash(\mathbb{N}\models s)\implies \mathbb{N}\models s)$" and this argument shows that the answer is still negative.

Note that I'm being a bit cavalier when I write "$Con(Q)$." There are really two versions of this sentence running around, the one in set theory and the one in arithmetic. The point is that ZFC proves $Con(Q)_{sets}\iff\mathbb{N}\models Con(Q)_{arith}$, and so we actually are free to conflate them in this way.
