If we replace first-order logic by second-order logic in the original definition of Gödel’s inner model L, we obtain the inner model of hereditarily ordinal definable sets [33]. In this paper...