I would guess no, "$x$ is a von Neumann ordinal" is not positive, otherwise $\{x\mid x\text{ is a von Neumann ordinal and }\forall y∈x∀f:y\to y\;((∀z∈y∀w∈y\;f(z)=f(w)⇒z=w)⇒∀z∈y∃w∈y\;f(w)=z)\}$ would have define $ω$ in $GPK^+$ (where $f:y\to y$ is "$∀p∈f∃z∈y∃w∈y\;(p=\{\{z\},\{z,w\}\})$ and $∀z∈y∀w∈y∀u∈y\;((\{\{z\},\{z,w\}\}∈f∧\{\{z\},\{z,u\}\})⇒w=u)$")

@user103 I wrote one

@user103 Try to show that there is no single formula $φ(x)$ such that $φ(x)⇒x\notin ω$, now take $a\in {\frak A}\setminus\omega$, show that if $\operatorname{tp}(a)$ is isolated by $ψ(x)$ then $ψ(x)⇒x\notin\omega$, and reach a contradiction (and similarly for $\frak B$)

The last part is not accurate, you assumed that $\aleph_n$ is regular (I have made the same mistake, general poset may have singular cofinality)

Looking at your preprint I found their paper "The consistency of the axiom of universality for the ordering of cardinalities"

Thanks Asaf, do you know perhaps the name of the paper of Honsel and Forti?