סמנטיקה לתחשיב היחסים - הגדרה פורמלית

הגדרת מבנה: בהינתן מילון plot:\[\tau \]: plot:\[\tau  = \left\langle
 {{R_1},...,{R_m},{F_1},...,{F_k},{C_1},...,{C_l}} \right\rangle \] מבנה עבור plot:\[\tau \] הוא:

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 \]

כאשר plot:\[{D^M}\] הוא התחום.

  • לכל plot:\[1 \leqslant i \leqslant m\] אם plot:\[{R_i}\] הוא סימן יחס plot:\[n\]-מקומי אזי plot:\[R_i^M \subseteq \underbrace {{D^M} \times ... \times
      {D^M}}_{n{\text{ times}}}\], כלומר plot:\[R_i^M\] הוא יחס plot:\[n\]-מקומי מעל plot:\[{D^M}\].
  • לכל plot:\[1 \leqslant i \leqslant k\] אם plot:\[{F_i}\] סימן פונקציה plot:\[n\]-מקומי אז plot:\[F_i^M:\underbrace {{D^M} \times ... \times
      {D^M}}_{n{\text{ times}}} \to {D^M}\], כלומר plot:\[F_i^M\] מתארת מה ההערך של plot:\[{F_i}\] עבור כל plot:\[n\]-יה סדורה של איברים מ-plot:\[{D^M}\].
  • לכל plot:\[1 \leqslant i \leqslant l\], מתקיים: plot:\[C_i^M \in {D^M}\].

ראינו כיצד בהינתן מבנה M מגדירים השמה plot:\[z\] ב-plot:\[M\]: plot:\[z:\left\{ {{v_i}|i \in
 \mathbb{N}} \right\} \to {D^M}\] וראינו כיצד להרחיב את plot:\[z\] כך שתתאים ערך מהתחום לכל שם עצם.

בהינתן נוסחה plot:\[\alpha \] מעל מילון plot:\[\tau \], מבנה plot:\[M\] והשמה plot:\[z\] עבור plot:\[M\] נסמן plot:\[M\mathop  \vDash \limits_z
 \alpha \] את הטענה ש-plot:\[\alpha \] מסתפקת ב-plot:\[M\] תחת plot:\[z\].

הגדרת ערך האמת: נגדיר באינדוקציה על מבנה plot:\[\alpha \] מתי plot:\[M\mathop  \vDash \limits_z \alpha \].

בסיס: plot:\[\alpha \] נוסחה אטומית: plot:\[\alpha  = \left( {{t_1}
 \approx {t_2}} \right)\] עבור plot:\[{t_1},{t_2}\] שמות עצם, plot:\[M\mathop  \vDash \limits_z \alpha  \Leftrightarrow \bar z\left( {{t_1}}
 \right) = \bar z\left( {{t_2}} \right)\].

כמו כן כאשר plot:\[\alpha  = R\left(
 {{t_1},...,{t_n}} \right)\], עבור plot:\[{t_1},...,{t_n}\] שמות עצם, plot:\[M\mathop  \vDash \limits_z \alpha  \Leftrightarrow \left( {\bar z\left(
 {{t_1}} \right),...,\bar z\left( {{t_n}} \right)} \right) \in {R^M}\].

סגור:

  1. קשרים: מחשבים את ערך האמת בעזר טבלאות האמת. לכל נוסחה plot:\[\alpha \], מבנה plot:\[M\] והשמה plot:\[z\], מתקיים כי plot:\[M\mathop  \vDash \limits_z \alpha \] או plot:\[M\mathop  \vDash \limits_z \neg \alpha \] אבל לא שניהם.
  2. כמתים: נניח שלכל מבנה plot:\[M'\] והשמה plot:\[z'\] אנו יודעים האם plot:\[M'\mathop  \vDash
      \limits_{z'} \alpha \]. נרצה לדעת האם plot:\[M\mathop  \vDash
      \limits_z \forall {v_i}\alpha \], plot:\[M\mathop  \vDash \limits_z \exists {v_i}\alpha \] למבנה והשמה מסויימים. בהינתן השמה plot:\[z\], משתנה plot:\[{v_i}\] ואיבר plot:\[d \in {D^M}\], נגדיר השמה מתוקנת plot:\[z\left[ {{v_i}
      \leftarrow d} \right]\] :

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.\]

נגדיר: לכל plot:\[d \in {D^M}\] מתקיים plot:\[M\mathop  \vDash \limits_z \forall {v_i}\alpha  \Leftrightarrow M\mathop 
 \vDash \limits_{z\left[ {{v_i} \leftarrow d} \right]} \alpha \].

קיים plot:\[d \in {D^M}\] עבורו plot:\[M\mathop  \vDash \limits_z \exists {v_i}\alpha 
 \Leftrightarrow M\mathop  \vDash \limits_{z\left[ {{v_i} \leftarrow d} \right]}
 \alpha \].

דוגמא:

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} \]

plot:\[{v_4}\]

plot:\[{v_3}\]

plot:\[{v_2}\]

plot:\[{v_1}\]

plot:\[z\]

80

6

5

2

האם plot:\[M\mathop  \vDash \limits_z \alpha \]? plot:\[\alpha  = \exists {v_1}{R_{2,0}}\left( {{F_{1,0}}\left( {{v_1}}
 \right),{F_{2,0}}\left( {{v_1},{v_2}} \right)} \right)\].

קיים plot:\[d \in {D^M}\] כך ש-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)\]

plot:\[ \Leftrightarrow \] קיים plot:\[d \in {D^M}\] כך ש-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\]

plot:\[ \Leftrightarrow \] קיים plot:\[d \in {D^M}\] כך ש-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\]

plot:\[ \Leftrightarrow \] קיים plot:\[d \in {D^M}\] כך ש-plot:\[\left( {F_{1,0}^M\left( d \right),F_{2,0}^M\left( {d,5} \right)} \right)
 \in R_{2,0}^M\].

plot:\[ \Leftrightarrow \] קיים plot:\[d \in {D^M}\] כך ש-plot:\[\left( {d + 2,d + 5} \right) \in  < \]

ולכן התשובה היא כן.

תגיות המסמך:

מאת: bentz

תיקון

מציעה להחליף את
(a¬)
ב

שכן (a¬) אינו פסוק
מאת: משה ב

סמנטיקה

שיתוף:
| עוד