Formula di Barcan

In logica modale, la formula di Barcan e l'inverso della formula di Barcan definiscono una relazione tra quantificatori e operatori modali.

Formula di Barcan

La formula di Barcan può essere formalizzata come segue:

$\forall x\Box A\rightarrow \Box \forall xA$

In altri termini, la traduzione in lingua Italiana è la seguente "'Per ogni x, è necessario A', implica, 'È necessario che per ogni x, A'".

In tutti i mondi accessibili da un generico mondo W, se la formula A è vera per ogni x del dominio di W, allora la formula A è vera per ciascun elemento del dominio di tutti i mondi accessibili da W. In altre parole, questa formula vincola a definire, nelle interpretazioni, domini uguali per tutti i mondi considerati.

È un assioma solo nel sistema formale S5.

Questa formula fu proposta da Ruth Barcan Marcus.

Inverso della formula di Barcan

L'inverso della formula di Barcan può essere formalizzato come segue:

$\Box \forall xA\rightarrow \forall x\Box A$

Questa formula afferma quanto segue: se è vero A per ogni x del dominio di ogni mondo, allora A è vera per ogni x del generico mondo W in tutti i mondi visibili da W. Rispetto alla formula di Barcan, questa è meno vincolante perché non richiede l'uguaglianza dei domini ma solo la condizione che se un generico mondo Wi vede un generico mondo Wj, il dominio di Wi sia incluso in quello di Wj.

È un assioma nei sistemi formali T, S4, S5

Relazione con la semantica di Kripke

La formule di Barcan affermano una equivalenza fra necessità (possibilità) de dicto e necessità (possibilità) de re.

Considerato un generico sistema formale in cui sia ammessa la semantica di Kripke, è dimostrato che la formula di Barcan e il suo inverso non sono più assiomi, in quanto non è più garantito il fatto che se un generico mondo Wi vede un generico mondo Wj, il dominio del primo sia incluso in quello del secondo.

Per evitare di associare lo stesso insieme di esistenti, D, a ogni modello, cioè a ogni mondo possibile, Kripke nel 1963 stabilì che le condizioni di verità degli enunciati quantificati devono essere modificate in modo da non presupporre la verità di tale tesi, dichiarando in modo esplicito per ogni mondo possibile, quale sia l'insieme degli individui in esso esistenti: per ogni elemento del mondo attuale viene specificato un dominio di quantificazione non vuoto.

Teorema

Considerato un generico sistema formale in cui sia imposta la relazione di simmetria tra i mondi (ad esempio S5), è dimostrato che in tale sistema formale la formula di Barcan è un assioma, come anche il suo inverso. Questo perché se un generico mondo Wi vede Wj, allora, per definizione di simmetria, Wj vede Wi. Quindi i domini sono uguali.

Voci correlate

• Ruth Barcan Marcus

Collegamenti esterni

• Barcan both ways Archiviato il 25 settembre 2006 in Internet Archive. by Melvin Fitting
• Contingent Objects and the Barcan Formula by Hayaki Reina