ترجمه استاندارد

در منطق موجهات، **ترجمه ا****ستاندارد** راهی برای تبدیل فرمولهای منطق موجهات به فرمولهای منطق مرتبه اول است که معنای فرمولهای مرتبه اول را به خود می‌گیرد. ترجمه استاندارد، به طور استقرایی روی ساختار فرمولها تعریف می‌شود. به طور خلاصه، فرمولهای اتمی بروی محمولهای تک-متغیره نگاشت شده و اشیایِ زبان، جهانهای دسترس پذیر هستند. رابط‌های منطقی از منطق گزاره‌ها، دست نخورده باقی مانده و عملگرهای وجهی، بسته به معناشناسی شان به فرمولهای مرتبه اول تبدیل می‌شوند.

## تعریف
ترجمه استاندارد به شرح زیر تعریف می‌شود:
* 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 درست باشد. توجه داشته باشید که اگر هیچ چنین جهان در دسترس پذیری موجود نباشد هم این فرمول همچنان درست خواهد بود. در صورتی که R(x,y) به هیچ جهانی دسترسی نداشته باشد،  نادرست است اما کل فرمول بطور پوچ درست است: یک استلزام، وقتی که مقدمه اش هم غلط باشد، درست است.

## ترجمه استاندارد و عمق وجهی
عمق وجهی یک فرمول نیز در ترجمه اش به منطق مرتبه اول آشکار می‌شود. وقتی عمق وجهی فرمول *k *باشد، فرمول مرتبه اول معادلش شامل «زنجیر»ی ز *k* انتقال از جهان آغازین  x است. جهانها به هم «زنجیر شده‌اند» بدان معنی که هرکدام از این جهانها با رفتن از جهانی دسترس پذیر به جهان دسترس پذیری دیگر، ملاقات می‌شوند. به طور غیررسمی، تعداد انتقالات در «طولانی‌ترین زنجیر» از انتقالات، عمق وجهی آن فرمول است.

عمق وجهی فرمول مورد استفاده در مثال بالا، دو است. فرمول مرتبه اول، نشان می‌دهد که انتقالات از x به y و از y به z برای ارزیابی فرمول لازم است. این عدد، همچنین عمق وجهی فرمول است، چرا که هر عملگر وجهی، عمق وجهی را یکی افزایش می‌دهد.

## منابع

* *Modal Logic: A Semantic Perspective*, Patrick Blackburn and Johan van Benthem

رده:منطق محمولات
رده:منطق موجهات