add axiom of infinity to stateless inference system

this breaks the soundness by translation proof. to fix it will probably
mean switching over to the psholSemantics based on polySetTheory, since
that's where INFINITY_AX_correct lives and I haven't proved a version
for modelSetTheory.
prove stateful soundness of INFINITY_AX

by tedious translation into the stateless syntax.

Also, switch to using psholSemanticsTheory as the specification for
holSemanticsTheory. So, is_model M assumptions are creeping into the
theorem statements, i.e. the assumption that the unspecified set theory
sitting at the top is OK.

Later theories (e.g. hol_verification) not yet updated.