I was wondering what happens if we extend ZFC by the assumption that $U$ is a model of ZFC that is 'standard' relative to every definable higher-order theory that is categorical. Specifically:
Let ZFC* be ZFC plus a new constant symbol $U$ and the axiom that $U$ is a model of ZFC and what I shall call the HOL-standardness axiom schema:
For every ZFC-definable higher-order theory $S$, ZFC* has the axiom ( If $S$ has an essentially unique model $M$ (under full semantics), then there is some set $N$ in $U$ such that $N$ is an essentially unique model of $S$ relative to $U$ and $N$ relative to $U$ is isomorphic to $M$. ).
In particular, ZFC* proves that $U$ is an ω-model of ZFC, since second-order PA is categorical (under full semantics), and that $U$ has essentially the same reals as the 'true universe', since the second-order axiomatization of the reals is categorical.
Furthermore, ZFC* proves that $U$ has essentially the same model as the 'true universe' for every explicit computable higher-order theory $S$ (i.e. its theorems are enumerated by an explicitly given program, using a fixed encoding of non-logical symbols and their signatures by natural numbers) that is categorical. But I doubt that it proves 'standardness' of $U$ that every (internal) computable higher-order theory that is categorical, because perhaps such a theory may not be definable over ZFC...
Presumably, ZFC* proves much more, but is it consistent to begin with, and what is its consistency strength? Furthermore, does the provision for higher-order theories make it strictly stronger than if we merely make it 'standard' relative to categorical second-order theories? Note also that I do not require $U$ to be a transitive model of ZFC, but I don't know whether it would make a difference.
For reference, by higher-order logic (HOL) I mean many-sorted first-order logic with base types $U,bool$, where $U$ is the domain of individuals, and the function type $(A→B)$ for every types $A,B$ (just like in simple type theory), and one sort for each type. Full semantics for HOL means that a model specifies a collection for the domain $U$, and all the other types are interpreted according to the function types built from $U$ in the meta-system, and also specifies the interpretation of each function/predicate-symbol (respecting its signature). And we say that a model of a higher-order theory $S$ is essentially unique if every model of $S$ is isomorphic to it (there is a bijection between their domains respecting their interpretations).
By "ZFC-definable higher-order theory $S$" I mean that there is a property $Q$ over ZFC such that ZFC proves that there is a unique higher-order theory $S$ that satisfies $Q$. So by "$S$ has an essentially unique model $M$" I mean "The higher-order theory that satisfies $Q$ has an essentially unique model $M$" and by "$N$ is an essentially unique model of $S$ relative to $U$" I mean "$N$ is an essentially unique model of the higher-order theory in $U$ that satisfies $Q$ in $U$".
And by "$N$ relative to $U$ is isomorphic to $M$" I mean that there is a bijection $i$ from sorts in $M$ to sorts in $N$ according to $U$, and a bijection $j$ from objects in $M$ to objects in $N$ according to $U$, that respect the interpretations of $M$ and $N$ relative to $U$, i.e.:
For every object $x$ of sort $A$ in $M$, $j(x)$ is an object of sort $i(A)$ in $N$ according to $U$.
$M ⊨ P(x[1..k])$ iff $U ⊨ ( N ⊨ P(j(x[1..k])) )$ for every predicate-symbol $P$ of $S$ and objects $x[1..k]$ in $M$ (of the appropriate sorts).
$M ⊨ f(x[1..k])) = y$ iff $U ⊨ ( N ⊨ f(j(x[1..k]))=j(y) )$ for every function-symbol $f$ of $S$ and objects $x[1..k],y$ in $M$ (of the appropriate sorts).