منطق قابلية التفسير

لغة ILM توسع لغة المنطق الافتراضي الكلاسيكي بإضافة عامل الوضع الأحادي${\displaystyle \Box }$والمؤثر النمطي الثنائي${\displaystyle \triangleright }$(كالعادة،${\displaystyle \Diamond p}$يُعرَّف بأنه${\displaystyle \neg \Box \neg p}$التفسير الحسابي لـ${\displaystyle \Box p}$يكون "${\displaystyle p}$يمكن إثبات ذلك في حساب بيانو (PA)".${\displaystyle p\triangleright q}$يُفهم على أنه "${\displaystyle PA+q}$يمكن تفسيره في${\displaystyle PA+p}$"

مخططات البديهيات :

1. جميع التكرارات الكلاسيكية
2. ${\displaystyle \Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)}$
3. ${\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p}$
4. ${\displaystyle \Box (p\rightarrow q)\rightarrow (p\triangleright q)}$
5. ${\displaystyle (p\triangleright q)\rightarrow (\Diamond p\rightarrow \Diamond q)}$
6. ${\displaystyle (p\triangleright q)\wedge (q\triangleright r)\rightarrow (p\triangleright r)}$
7. ${\displaystyle (p\triangleright r)\wedge (q\triangleright r)\rightarrow ((p\vee q)\triangleright r)}$
8. ${\displaystyle \Diamond p\triangleright p}$
9. ${\displaystyle (p\triangleright q)\rightarrow ((p\wedge \Box r)\triangleright (q\wedge \Box r))}$

قواعد الاستدلال :

1. "من${\displaystyle p}$و${\displaystyle p\rightarrow q}$ختامًا${\displaystyle q}$"
2. "من${\displaystyle p}$ختامًا${\displaystyle \Box p}$"

تم إثبات اكتمال ILM فيما يتعلق بتفسيره الحسابي بشكل مستقل من قبل أليساندرو بيراردوتشي وفلاديمير شافروكوف.

لغة TOL توسع لغة المنطق الافتراضي الكلاسيكي بإضافة عامل الوضع${\displaystyle \Diamond }$والتي يُسمح لها بأخذ أي سلسلة غير فارغة من الوسائط. التفسير الحسابي لـ${\displaystyle \Diamond (p_{1},\ldots ,p_{n})}$يكون "${\displaystyle (PA+p_{1},\ldots ,PA+p_{n})}$"هو تسلسل متسامح من النظريات".

البديهيات (مع${\displaystyle p,q}$يرمز إلى أي صيغة، ${\displaystyle {\vec {r}},{\vec {s}}}$لأي سلسلة من الصيغ، و${\displaystyle \Diamond ()}$(يُشار إليه بـ ⊤):

1. جميع التكرارات الكلاسيكية
2. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r}},q,{\vec {s}})}$
3. ${\displaystyle \Diamond (p)\rightarrow \Diamond (p\wedge \neg \Diamond (p))}$
4. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},{\vec {s}})}$
5. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p,p,{\vec {s}})}$
6. ${\displaystyle \Diamond (p,\Diamond ({\vec {r}}))\rightarrow \Diamond (p\wedge \Diamond ({\vec {r}}))}$
7. ${\displaystyle \Diamond ({\vec {r}},\Diamond ({\vec {s}}))\rightarrow \Diamond ({\vec {r}},{\vec {s}})}$

قواعد الاستدلال:

1. "من${\displaystyle p}$و${\displaystyle p\rightarrow q}$ختامًا${\displaystyle q}$"
2. "من${\displaystyle \neg p}$ختامًا${\displaystyle \neg \Diamond (p)}$"

أثبت جيورجي جاباريدزه اكتمال نظرية التكافؤ فيما يتعلق بتفسيرها الحسابي .