Benutzer:Bocardodarapti/Arbeitsseite/Modallogik

Das Schema ${}K$ entspricht der Vorgängerregel

$\operatorname {Vorg} {\left(T\right)}\subseteq \operatorname {Vorg} {\left(\complement S\right)}\cup \operatorname {Vorg} {\left(S\cap T\right)}.$

Diese ist trivialerweise erfüllt, da aus ${}xRy$ mit ${}y\in T$ abhängig davon, ob ${}y$ zu ${}S$ gehört oder nicht, folgt, dass ${}x$ zu einer der Mengen rechts gehört.

${}\alpha \rightarrow \Diamond \alpha$ entspricht der Vorgängerbeziehung ${}T\subseteq \operatorname {Vorg} {\left(T\right)}$. Dies ist genau dann erfüllt, wenn die Menge reflexiv gerichtet ist, also jedes Element von sich selbst aus erreichbar ist.

${}\Diamond \Diamond \alpha \rightarrow \Diamond \alpha$ entspricht der Vorgängerbeziehung ${}\operatorname {Vorg} {\left(\operatorname {Vorg} {\left(T\right)}\right)}\subseteq \operatorname {Vorg} {\left(T\right)}$. Dies bedeutet, dass ein Vorvorgänger, also der Vorgänger eines Vorgängers, selbst ein Vorgänger sein muss. Dies bedeutet die Transitivität der Erreichbarkeitsrelation.

${}\alpha \rightarrow \neg \Diamond \neg \Diamond \alpha$ entspricht der Vorgängerbeziehung ${}T\subseteq \complement \operatorname {Vorg} {\left(\complement \operatorname {Vorg} {\left(T\right)}\right)}$. Dies bedeutet, dass jedes Element ${}x$ ein Nichtvorgänger eines Nichtvorgängers von ${}x$ sein muss. Wenn also ${}x$ ein Vorgänger eines Elementes ${}y$ ist, so muss dieses ein Vorgänger von ${}x$ sein. Dies bedeutet die Symmetrie der Erreichbarkeitsrelation.

${}\Box \alpha \rightarrow \Diamond \alpha$ bzw. ${}\neg \Diamond \alpha \rightarrow \Diamond \neg \alpha$ entspricht der Vorgängerbeziehung ${}\complement \operatorname {Vorg} {\left(T\right)}\subseteq \operatorname {Vorg} {\left(\complement T\right)}$. Dies bedeutet, dass ein Nichtvorgänger eines Elementes ${}x$ ein Vorgänger eines Elementes aus dem Komplement von ${}x$ sein muss. Dies bedeutet einfach, dass jedes ELement ${}x$ überhaupt irgendeinen Nachfolger (möglicherweise sich selbst) besitzt. Die Erreichbarkeitsrelations nennt man seriell (oder, im Sinne von ohne Endpunkt, definal oder linkstotal).

Wie lässt sich Nachfolger modallogisch erfassen? Euklidische Eigenschaft: aus ${}xRy$ und ${}xRz$ folgt ${}yRz$. ${}\operatorname {Nachf} {\left(T\right)}\subseteq \operatorname {Vorg} {\left(\operatorname {Nachf} {\left(T\right)}\right)}$. Modallogisch wohl ${}\Diamond p\wedge \Diamond q\rightarrow \Diamond (p\wedge \Diamond q)$. Heißt wiederum ${}\operatorname {Vorg} {\left(S\right)}\cap \operatorname {Vorg} {\left(T\right)}\subseteq \operatorname {Vorg} {\left(S\cap \operatorname {Vorg} {\left(T\right)}\right)}$.