So here I am studying the Ackerman interpretation (via Kaye-Wong) to try and suss what the fragment of arithmetic associated with KF (Mac Lane minus Foundation and Infinity, with separation restricted to stratified $\Delta_0$ formulae) is like when you add categorical products. Then the idea (read: ADD) hits: is there a suitable arithmetic interpretation of the theory of $\mathbf{Set_{Fin}}$ in the signature $\{\circ\}$ that will let me duck the translation of elaborate statements about ordered pairs?
I'm not sure if I can hope for something as strong as the Ackerman interpretation's property of having an inverse, but I am hoping for at least the following from an interpretation $i$: if $Th(\mathbf{Set_{Fin}})\cup\{\phi\}$ and $Th(\mathbf{Set_{Fin}})\cup\{\neg\phi\}$ are both satisfiable, $PA\cup\{i(\phi)\}$ and $PA\cup\{i(\neg\phi)\}$ are both satisfiable.
For clarification, I'm not hoping for you fine folks to know of the right kind of interpretation; more just hoping for something reasonably Googlable on intepretations that have the above property. What is a name for what I'm hoping for here? What should I watch out for if I'm hoping for this property? Have any capable authors written about my hopes and dreams in this area? I've been toying with the notion that since the Ackerman interpretation seems construable as an equivalence between preorder categories, maybe I can weaken that by asking $i$ to be, say, right adjoint; but that's probably just me being cute again.