סמנטיקה לתחשיב היחסים - הגדרה פורמלית
הגדרת
מבנה: בהינתן מילון
:
מבנה עבור
הוא:
![plot:\[M =
\left\langle {{D^M},{R_1}^M,...,{R_m}^M,{F^M}_1,...,{F_k}^M,{C_1}^M...,{C_l}^M}
\right\rangle \]](/documentResources/171/plot_647.png)
כאשר
הוא התחום.
- לכל
אם
הוא סימן
יחס
-מקומי אזי
, כלומר
הוא יחס
-מקומי מעל
.
- לכל
אם
סימן
פונקציה
-מקומי אז
, כלומר
מתארת מה
ההערך של
עבור כל
-יה סדורה של
איברים מ-
.
- לכל
, מתקיים:
.
ראינו
כיצד בהינתן מבנה M מגדירים השמה
ב-
:
וראינו כיצד
להרחיב את
כך שתתאים ערך מהתחום לכל שם עצם.
בהינתן
נוסחה
מעל מילון
,
מבנה
והשמה
עבור
נסמן
את הטענה ש-
מסתפקת ב-
תחת
.
הגדרת
ערך האמת: נגדיר
באינדוקציה על מבנה
מתי
.
בסיס:
נוסחה אטומית:
עבור
שמות עצם,
.
כמו
כן כאשר
, עבור
שמות עצם,
.
סגור:
- קשרים:
מחשבים את ערך האמת בעזר טבלאות האמת. לכל נוסחה
, מבנה
והשמה
, מתקיים כי
או
אבל לא שניהם.
- כמתים:
נניח שלכל מבנה
והשמה
אנו יודעים
האם
. נרצה לדעת
האם
,
למבנה והשמה מסויימים. בהינתן השמה
, משתנה
ואיבר
, נגדיר השמה
מתוקנת
:
![plot:\[z\left[ {{v_i} \leftarrow d} \right]\left( {{v_j}} \right)
= \left\{ {\begin{array}{*{20}{c}}
{z\left( {{v_j}} \right)} \hfill & {i \ne j} \hfill
\\
d \hfill & {i = j} \hfill \\
\end{array} } \right.\]](/documentResources/171/plot_702.png)
נגדיר: לכל
מתקיים
.
קיים
עבורו
.
דוגמא: |
![plot:\[\begin{gathered}
\tau = \left\langle
{{R_{2,0}},{F_{2,0}},{F_{1,0}}} \right\rangle \hfill \\
M = \left\langle {\mathbb{N}, <
, + , + 2} \right\rangle \hfill \\
\end{gathered} \]](/documentResources/171/plot_707.png) |
|
האם
?
.
קיים
כך ש-![plot:\[M\mathop \vDash \limits_z \alpha \Leftrightarrow M\mathop \vDash
\limits_{\mathop {z\left[ {{v_1} \leftarrow d} \right]}\limits_{ \equiv z'} }
{R_{2,0}}\left( {{F_{1,0}}\left( {{v_1}} \right),{F_{2,0}}\left( {{v_1},{v_2}}
\right)} \right)\]](/documentResources/171/plot_716.png)
קיים
כך ש-![plot:\[\left( {\bar z'\left( {{F_{1,0}}\left( {{v_1}} \right)} \right),\bar
z'\left( {{F_{2,0}}\left( {{v_1},{v_2}} \right)} \right)} \right) \in
R_{2,0}^M\]](/documentResources/171/plot_719.png)
קיים
כך ש-![plot:\[\left( {F_{1,0}^M\left( {\bar z'\left( {{v_1}} \right)}
\right),F_{2,0}^M\left( {\bar z'\left( {{v_1}} \right),\bar z'\left( {{v_2}}
\right)} \right)} \right) \in R_{2,0}^M\]](/documentResources/171/plot_722.png)
קיים
כך ש-
.
קיים
כך ש-![plot:\[\left( {d + 2,d + 5} \right) \in < \]](/documentResources/171/plot_728.png)
ולכן
התשובה היא כן.
תיקון
מציעה להחליף את(a¬)
ב
a¬
שכן (a¬) אינו פסוק