«الترجمة التفسيرية» (interpretation) هي تحديد معنى الرموز في «اللغة الشكلية». تُعرّف العديد من اللغات الشكلية المستخدمة في الرياضيات والمنطق وعلم الحاسوب النظري بـ «مصطلحات نحوية» فقط، وبالتالي ليس لها أي معنى حتى تُفسر بطريقة محددة. تسمى الدراسة العامة لتفسيرات اللغات الشكلية باسم «الدلالات الشكلية».
المنطق الشكلي الأكثر شيوعًا هو «منطق القضايا» و«منطق المسندات» و«منطق الموجهات» النظير لهما، وهناك طرق قياسية لتقديم ترجمة تفسيرية لكل منها. في هذه السياقات، الترجمة التفسيرية هي عبارة عن دالة توفر امتدادًا لرموز وسلاسل الرموز لإحداى «لغات الهدف». على سبيل المثال، يمكن أن تستقبل دالة الترجمة التفسيرية «الدالة الخبرية» تي T (كرمز لـ «الطول») وتعين الامتداد {إيه a} (كرمز لـ «ابراهام لنكون»). لاحظ أن وظيفة الترجمة التفسيرية الخاصة بنا هو تعيين الامتداد {إيه a} للثابت غير المنطقي تي T، ولا تدعي ما إذا كان تي T يرمز للطول أو إيه a لابراهام لنكولن. ولا علاقة للترجمة التفسيرية المنطقية بالـ «روابط المنطقية» مثل «و and» و«أو or» و« ليس not». على الرغم من أننا قد نستخدم هذه الرموز للدلالة على أشياء أو مفاهيم معينة، إلا أن هذا لا يُحدد بواسطة دالة الترجمة التفسيرية.
غالبًا (ولكن ليس دائمًا) ما توفر الترجمة التفسيرية طريقة لتحديد «القيم الحقيقة» للجمل في اللغة. إذا كان الترجمة التفسيرية تحدد قيمة صحيحة إلى جملة أو نظرية، تُسمى الترجمة التفسيرية في هذه الحالة نموذج تلك الجملة أو النظرية.
اللغات الشكلية
تتكون اللغة الشكلية من مجموعة لا حصر لها من الجمل (تسمى كلمات أو صيغ) مبنية من مجموعة ثابتة من الحروف أو الرموز. تُسمى القائمة التي تُؤخذ منها هذه الحروف بـ «الحروف الأبجدية» التي تُعرف اللغة بواسطتها. للتمييز بين سلاسل الرموز الموجودة في اللغة الشكلية وبين سلاسل الرموز الاعتباطية، تسمى الأولى في بعض الأحيان بـ «الصيغة المُشكلة جيدًا» (دبليو إف إف). تكمن الميزة الأساسية للغة الشكلية في إمكانية تحديد مصطلحاتها النحوية دون الرجوع للترجمة التفسيرية. على سبيل المثال، يمكننا تحديد ما كانت (بّي P أو كيو Q) صيغة مشكلة جيدًا حتى دون معرفة ما إذا كانت صحيحة أم خاطئة.