General operators binding variables in the interpreted modal calculus $\mathcal{MC}^{\nu}$

Bressan, Aldo ; Zanardo, Alberto

Atti della Accademia nazionale dei Lincei. Rendiconti della Classe di scienze fisiche, matematiche e naturali, Série 8, Tome 70 (1981) no. 4, pp. 191-197

Résumé

Si considera il calcolo modale interpretato $\mathcal{MC}^{\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 $\mathcal{MC}^{\nu}$ operatori vincolanti variabili, di tipo generale. Per teorie basate sul calcolo logico risultante $\mathcal{MC}^{\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 in [12].