Questa dissertazione cerca di fornire un trattamento unificato delle costanti proposizionali in logica modale. I linguaggi arricchiti con costanti vengono usati almeno a partire dalla metà del secolo scorso, ma ancora non è stato fatto uno studio sistematico. Il principale contributo del mio lavoro consiste nello sviluppo di un approccio semantico basato su strutture con insiemi di interpretazioni possibili per le costanti proposizionali, chiamati restrizioni specifiche; tali strutture sono confrontate con quelle in cui ogni costante ha una interpretazione fissa, solitamente utilizzate nella letteratura. Viene mostrato che la presenza di restrizioni specifiche permette di definire la nozione di strict range di una formula (traducibile come "varietà stretta di modelli"), che risulta essere importante per questioni di teoria dei modelli. Inoltre, l'approccio semantico qui introdotto viene usato per formulare sistemi di logica del tempo il cui linguaggio include operatori primitivi di contingenza; per tali sistemi si dimostrano risultati di caratterizzazione in riferimento a diverse classi di strutture temporali. Infine, la tesi propone una generalizzazione dello studio dei linguaggi modali arricchiti passando da linguaggi con costanti proposizionali a linguaggi con quantificatori proposizionali e di questi ultimi viene studiata la teoria della dimostrazione con sistemi di deduzione naturale etichettata.

This dissertation aims at providing a unified treatment of propositional constants in modal logic. Languages enriched with constants have been used at least from the Fifties, but a systematic study of them is still not available.The main contribution consists in the development of a semantic approach based on structures with sets of possible interpretations for propositional constants, called specific restrictions; such structures are compared with those in which every constant has a fixed interpretation, usually adopted in the literature. We show that the presence of specific restrictions allows one to define the notion of strict range of a formula, that turns out to be important for model-theoretic purposes. Furthermore, we use the semantic approach here introduced to develop systems of temporal logic whose language includes primitive operators of contingency, showing that propositional constants are useful to obtain characterization results with reference to different classes of temporal frames. Finally, we move from languages with propositional constants to languages with propositional quantifiers (the latter being intended as a generalization of the former) and analyse their proof theory in natural deduction calculi.