2 Comments

  1. Buongiorno, chiedo un veloce chiarimento riguardante la slide 29/30 del blocco sulla semantica, dove si prova che se un frame è transitivo allora vale l’assioma “boxp entails boxboxp”.
    Non mi è chiara la conclusione che il mondo k porti a boxp dal fatto che j e k portano a p. Sarebbe chiaro se il frame fosse anche riflessivo, e cioè che k si riflettesse su se stesso. Così, avendo transitività e riflessività avremmo un preordine, che infatti è il frame adeguato, come si dice nella slide 18/30, per il sistema s4, caratterizzato per l’appunto dall’assioma “boxp entails boxboxp”. Mancando la transitività però mi riesce difficile capire quel passaggio.
    Grazie!

    Reply

    1. L’idea è questa. Supponiamo i\models \square\phi. Dobbiamo dimostrare i \models \square\square \phi. Supponiamo che <i,j>\in E è sufficiente dimostrare che j\models \square \phi. Se k è un punto arbitrario tale che <j,k>\in E allora <i,k>\in E per transitività. Ora, per ipotesi i\models\square\phi. Dunque k \models \phi. Ma poiché k era uno stato arbitrario in relazione con j otteniamo che j\models \square \phi, come desiderato.

      Reply

Comments