Intensional and higher-order modal logic