New inner models from second order logics

We define a new inner model C2(omega) based on the fragment of second order logic in which second order variables range over countable subsets of the domain. We compare C2(omega) to the previously studied inner model C(aa). We argue that C2(omega) appears to be a much bigger inner model than C(aa), although this cannot be literally true in ZFC alone. However, we conjecture that it follows from large cardinal assumptions. For example, assuming large cardinals, C2(omega) contains, for every n, an inner model with n Woodin cardinals, while C(aa) contains, under the same assumption, no inner model with a Woodin cardinal. As to large cardinals in C2(omega), we show that, assuming a Woodin limit of Woodin cardinals, the cardinal omega_1 of V is Mahlo in C2(omega). A stronger result is proved for the combination C2(omega, aa) of C(aa) and C2(omega). We also show that the question whether HOD1, a variant of HOD, is the same as HOD cannot be decided on the basis of ZFC even if we add the assumption that there are supercompact cardinals.