標準翻訳

様相論理において、標準変換とは、様相論理の式を、様相式の意味を捉える一階論理の式に変換する論理変換である。標準変換は、式の構造に基づいて帰納的に定義される。つまり、原子式は単項述語にマッピングされ、一階言語のオブジェクトはアクセス可能な世界である。命題論理の論理接続詞はそのまま残り、様相演算子は意味論に従って一階論理式に変換される。

標準的な翻訳は次のように定義されます。

• ${\displaystyle ST_{x}(p)\equiv P(x)}$ここで は原子式であり、が世界で成り立つ場合、P(x) は真です。${\displaystyle p}$${\displaystyle p}$${\displaystyle x}$
• ${\displaystyle ST_{x}(\top )\equiv \top }$
• ${\displaystyle ST_{x}(\bot )\equiv \bot }$
• ${\displaystyle ST_{x}(\neg \varphi )\equiv \neg ST_{x}(\varphi )}$
• ${\displaystyle ST_{x}(\varphi \wedge \psi )\equiv ST_{x}(\varphi )\wedge ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\varphi \vee \psi )\equiv ST_{x}(\varphi )\vee ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\varphi \rightarrow \psi )\equiv ST_{x}(\varphi )\rightarrow ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\Diamond _{m}\varphi )\equiv \exists y(R_{m}(x,y)\wedge ST_{y}(\varphi ))}$
• ${\displaystyle ST_{x}(\Box _{m}\varphi )\equiv \forall y(R_{m}(x,y)\rightarrow ST_{y}(\varphi ))}$

上記で、は式が評価される世界です。最初は自由変数が使用され、様相演算子を変換する必要があるときはいつでも、式の残りをその世界から評価する必要があることを示す新しい変数が導入されます。ここで、下付き文字は、使用する必要があるアクセシビリティ関係を参照します。通常、と はKripke モデルの関係を参照しますが、アクセシビリティ関係が複数存在する場合 (マルチモーダル ロジック)、下付き文字が使用されます。たとえば、と は、モデル内のアクセシビリティ関係およびおよびを参照します。あるいは、 を様相記号内に置くこともできます。 ${\displaystyle x}$ ${\displaystyle x}$${\displaystyle m}$${\displaystyle \Box}$${\displaystyle \Diamond }$${\displaystyle R}$${\displaystyle \Box _{a}}$${\displaystyle \Diamond _{a}}$${\displaystyle R_{a}}$${\displaystyle \Box_{b}}$${\displaystyle \Diamond _{b}}$${\displaystyle R_{b}}$

例えば、 に標準変換を適用すると、外側のボックスを展開して次の式を得ます。 ${\displaystyle \Box \Box p}$

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

つまり、 からアクセス可能な世界に移動したので、それぞれのアクセス可能な世界で 式の残りの部分 を評価することになります。${\displaystyle x}$${\displaystyle y}$${\displaystyle \Box p}$

この例の標準的な翻訳は、

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

これは、様相論理における 2 つのボックスの意味を正確に表しています。からのすべてのアクセス可能な世界に対してが成り立ち、からのすべてのアクセス可能な世界に対して が成り立つ場合、述語 がに対して真となります。 式は、そのようなアクセス可能な世界が存在しない場合にも真となることに注意してください。 にアクセス可能な世界がない場合は は偽ですが、式全体は空虚に真です。つまり、前提が偽である場合にも含意は真です。 ${\displaystyle \Box \Box p}$${\displaystyle x}$${\displaystyle y}$${\displaystyle x}$${\displaystyle z}$${\displaystyle y}$${\displaystyle P}$${\displaystyle z}$${\displaystyle x}$${\displaystyle R(x,y)}$

式の様相の深さは、一階論理への変換でも明らかになります。式の様相の深さがkの場合、一階論理式には、開始世界からのk 個の遷移の「連鎖」が含まれます。世界は、アクセス可能な世界からアクセス可能な世界へと移動することによってこれらの世界が訪問されるという意味で「連鎖」されています。非公式には、一階論理式における遷移の「最長連鎖」の遷移数が、式の様相の深さです。 ${\displaystyle x}$

上記の例で使用されている式のモーダル深度は 2 です。 一次式は、式の有効性を検証するために、から への遷移と から への遷移が必要であることを示しています。 これは式のモーダル深度でもあり、各モーダル演算子によってモーダル深度が 1 ずつ増加します。 ${\displaystyle x}$${\displaystyle y}$${\displaystyle y}$${\displaystyle z}$

• Patrick Blackburn とJohan van Benthem (1988)、「様相論理：意味論的観点」。