  The paper is the second of two and shows that (assuming large cardinals) set
theory is a tractable (and we dare to say tame) first order theory when
formalized in a first order signature with natural predicate symbols for the
basic definable concepts of second and third order arithmetic, and appealing to
the model-theoretic notions of model completeness and model companionship.
  Specifically we use the general framework linking generic absoluteness
results to model companionship introduced in the first paper to show that
strong forms of Woodin's axiom $(*)$ entail that any theory $T$ extending
$\mathsf{ZFC}$ by suitable large cardinal axioms has a model companion $T^*$
with respect to certain signatures $\tau$ containing symbols for
$\Delta_0$-relations and functions, constant symbols for $\omega$ and
$\omega_1$, a predicate symbol for the nonstationary ideal on $\omega_1$,
symbols for certain lightface definable universally Baire sets.
  Moreover $T^*$ is axiomatized by the $\Pi_2$-sentences $\psi$ for $\tau$ such
that $T$ proves that $$
L(\mathsf{UB})\models(\mathbb{P}_\max\Vdash\psi^{H_{\omega_2}}), $$ where
$L(\mathsf{UB})$ denotes the smallest transitive model containing the
universally Baire sets.
  Key to our results is the recent breakthrough of Asper\`o and Schindler
establishing that a strong form of Woodin's axiom $(*)$ follows from
$\mathsf{MM}^{++}$.
