Presentamos un sistema lógico-formal que aúna recursos expresivos de la teoría de tipos simple, de la lógica modal, y de la lógica híbrida básica, y lo dotamos de una semántica que puede caracterizarse  en su semántica por un doble ingrediente de parcialidad: los términos no-lógicos pueden carecer de denotación en ciertos estados o mundos posibles (la función de constantes y estados a entidades que les sirven de denotación es parcial) y por otra, la jerarquía de tipos no se construye con funciones totales sino con funciones parciales: para todo tipo funcional <a,b>, su dominio asociado es un subconjunto del conjunto de funciones parciales del dominio asociado al tipo a en el dominio asociado en el tipo b.

El cálculo que presentamos para esta lógica es de árboles semánticos, combinando adaptaciones de reglas ya existentes con otras originales (en particular para manejar los operadores @i característicos de la lógica híbrida). Tras la presentación de las reglas del cálculo desarrollamos la demostración de un teorema de corrección para el mismo.

Concluimos el trabajo con algunas observaciones concernientes a las capacidades expresivas del lenguaje respecto de la clase de modelos que lo interpreta, sobre las formas y dificultades que se encuentran a la hora de encarar el problema de la completud del cálculo y, muy sucintamente, sobre la adecuación del sistema para representar análisis de semántica formal tanto en la tradición de Richard Montague como en la de la denominada semántica de situaciones.