Si considera il calcolo modale interpretato $ℳ{𝒞}^{\nu }$, che è basato su un sistema di tipi con infiniti livelli, contiene descrizioni, ed è dotato di una semantica di tipo generale - v. [2], o [3], o [4], o [5]. In modo semplice e naturale si introducono in $ℳ{𝒞}^{\nu }$ operatori vincolanti variabili, di tipo generale. Per teorie basate sul calcolo logico risultante $ℳ{𝒞}^{\nu }$ vale un teorema di completezza, che si dimostra in modo immediato sulla base dell'estensione del teorema parziale di completezza stabilito in [11], fatta...