Стандартный перевод

В модальной логике стандартный перевод — это логический перевод , который преобразует формулы модальной логики в формулы логики первого порядка , которые отражают смысл модальных формул. Стандартный перевод определяется индуктивно по структуре формулы. Короче говоря, атомарные формулы отображаются на унарные предикаты , а объекты языка первого порядка — это доступные миры . Логические связки из логики высказываний остаются нетронутыми, а модальные операторы преобразуются в формулы первого порядка в соответствии с их семантикой .

Определение

Стандартный перевод определяется следующим образом:

• $ST_{x}(p)\equiv P(x)$, где $p$ формула атомная ; P(x) истинно, когда $p$ держится в мире $x$.
• $ST_{x}(\top )\equiv \top$
• $ST_{x}(\bot )\equiv \bot$
• $ST_{x}(\neg \varphi )\equiv \neg ST_{x}(\varphi )$
• $ST_{x}(\varphi \wedge \psi )\equiv ST_{x}(\varphi )\wedge ST_{x}(\psi )$
• $ST_{x}(\varphi \vee \psi )\equiv ST_{x}(\varphi )\vee ST_{x}(\psi )$
• $ST_{x}(\varphi \rightarrow \psi )\equiv ST_{x}(\varphi )\rightarrow ST_{x}(\psi )$
• $ST_{x}(\Diamond _{m}\varphi )\equiv \exists y(R_{m}(x,y)\wedge ST_{y}(\varphi ))$
• $ST_{x}(\Box _{m}\varphi )\equiv \forall y(R_{m}(x,y)\rightarrow ST_{y}(\varphi ))$

В приведенном выше $x$ это мир, из которого вычисляется формула. Изначально свободная переменная $x$ используется, и всякий раз, когда модальный оператор необходимо перевести, вводится новая переменная , указывающая, что оставшуюся часть формулы необходимо вычислить из этого мира. Здесь индекс $m$ относится к отношению доступности , которое следует использовать: обычно $\Box$ и $\Diamond$ ссылаться на отношение $R$ модели Крипке , но может существовать более одного отношения доступности ( мультимодальная логика ), и в этом случае используются индексы. Например, $\Box _{a}$ и $\Diamond _{a}$ обратитесь к отношению доступности $R_{a}$ и $\Box _{b}$ и $\Diamond _{b}$ к $R_{b}$ в модели. Альтернативно, его также можно поместить внутри модального символа.

Пример

Например, когда стандартный перевод применяется к $\Box \Box p$, мы расширяем внешнюю рамку, чтобы получить

$\forall y(R(x,y)\rightarrow ST_{y}(\Box p))$

это означает, что мы теперь переехали из $x$ в доступный мир $y$ и теперь мы оцениваем оставшуюся часть формулы, $\Box p$, в каждом из этих доступных миров.

Весь стандартный перевод этого примера становится

$\forall y(R(x,y)\rightarrow (\forall z(R(y,z)\rightarrow P(z))))$

который точно отражает семантику двух блоков в модальной логике. Формула $\Box \Box p$ держится $x$ когда для всех доступных миров $y$ от $x$ и для всех доступных миров $z$ от $y$, предикат $P$ верно для $z$. Обратите внимание, что формула верна и тогда, когда таких доступных миров не существует. В случае $x$ тогда у него нет доступных миров $R(x,y)$ ложно, но вся формула в целом истинна : ​​импликация также истинна, когда антецедент ложен.

Стандартный перевод и модальная глубина

Модальная глубина формулы также становится очевидной при переводе в логику первого порядка. Когда модальная глубина формулы равна k , то логическая формула первого порядка содержит «цепочку» из k переходов из начального мира. $x$. Миры «сцеплены» в том смысле, что эти миры посещаются путем перехода от доступного к доступному миру. Неформально количество переходов в «самой длинной цепочке» переходов в формуле первого порядка представляет собой модальную глубину формулы.

Модальная глубина формулы, использованной в приведенном выше примере, равна двум. Формула первого порядка указывает на то, что переходы от $x$ к $y$ и из $y$ к $z$ необходимы для проверки правильности формулы. Это также модальная глубина формулы, поскольку каждый модальный оператор увеличивает модальную глубину на единицу.

Ссылки

• Патрик Блэкберн и Йохан ван Бентем (1988), Модальная логика: семантическая перспектива .