הועלה לאתר:  
מספר עמודים: 25
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

לוגיקה - סיכום נקודות

סיכום מאת: ניר אדר

מושגי יסוד סמנטיים

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

על מנת להראות שנוסחה אינה אמת לוגית יש להראות מבנה והשמה שאינם מספקים אותה.

טענות

  1. plot:\[\exists {v_1}\forall {v_2}R\left( {{v_1},{v_2}} \right) \to \forall {v_2}\exists {v_1}R\left( {{v_1},{v_2}} \right)\] אמת לוגית.
  2. plot:\[\forall {v_1}\exists {v_2}R\left( {{v_1},{v_2}} \right) \to \exists {v_2}\forall {v_1}R\left( {{v_1},{v_2}} \right)\] לא אמת לוגית.

הגדרות

  • נאמר שנוסחה plot:\[\alpha \] היא סתירה אם לכל מבנה plot:\[M\] עבור המילון של plot:\[\alpha \] ולכל השמה plot:\[z\] ב-plot:\[M\] מתקיים כי plot:\[M\mathop {\not  \vDash }\limits_z \alpha \].
  • נוסחה plot:\[\alpha \] היא ספיקה אם קיים מבנה plot:\[M\] וקיימת השמה plot:\[z\] כך ש-plot:\[M\mathop  \vDash \limits_z \alpha \].
  • נאמר ש-plot:\[M \vDash \alpha \] אם לכל השמה plot:\[z\] ב-plot:\[M\], מתקיים plot:\[M\mathop  \vDash \limits_z \alpha \].
  • נאמר ש-plot:\[M\not  \vDash \alpha \] אם קיימת השמה plot:\[z\] ב-plot:\[M\], עבורה plot:\[M\mathop {\not  \vDash }\limits_z \alpha \].
  • נסמן plot:\[ \vDash \alpha \] אם plot:\[\alpha \] הוא אמת לוגית.
  • נאמר ש-plot:\[M\mathop  \vDash \limits_z \Sigma \] עבור קבוצת נוסחאות plot:\[\Sigma \], אם לכל plot:\[\alpha  \in \Sigma \], plot:\[M\mathop  \vDash \limits_z \alpha \].
  • נאמר שנוסחה plot:\[\alpha \] גוררת לוגית נוסחה plot:\[\beta \] ונסמן plot:\[\alpha  \vDash \beta \] אם לכל מבנה plot:\[M\] והשמה plot:\[z\], אם plot:\[M\mathop  \vDash \limits_z \alpha \] אז גם plot:\[M\mathop  \vDash \limits_z \beta \].
  • נאמר ש-plot:\[\Sigma  \vDash \alpha \] אם לכל מבנה plot:\[M\] והשמה plot:\[z\], אם plot:\[M\mathop  \vDash \limits_z \Sigma \] אז plot:\[M\mathop  \vDash \limits_z \alpha \].

דוגמא

נראה כי plot:\[\exists {v_1}\alpha  \equiv \neg \forall {v_1}\neg \alpha \].

יהי plot:\[M\] מבנה ו-plot:\[z\] השמה: plot:\[ \Leftrightarrow M\mathop  \vDash \limits_z \exists {v_1}\alpha \]קיים plot:\[d \in {D^M}\] כך ש-plot:\[M\mathop  \vDash \limits_{z\left[ {{v_1} \leftarrow d} \right]} \alpha \] plot:\[\mathop  \Leftrightarrow \limits_{T{T_\neg }} \] קיים plot:\[d \in {D^M}\] כך ש-plot:\[M\mathop {\not  \vDash }\limits_{z\left[ {{v_1} \leftarrow d} \right]} \neg \alpha \]plot:\[ \Leftrightarrow \]לא לכל plot:\[d \in {D^M}\] מתקיים plot:\[M\mathop  \vDash \limits_z \neg \forall {v_1}\neg \alpha \mathop  \Leftrightarrow \limits_{T{T_\neg }} M\mathop {\not  \vDash }\limits_z \forall {v_1}\neg \alpha  \Leftrightarrow {\rm M}\mathop  \vDash \limits_{z\left( {{v_1} \leftarrow d} \right)} \neg d\].

הצבות

בהינתן פונקצית הצבה:        שמות העצםplot:\[ \to \]משתניםplot:\[s:\], נגדיר את plot:\[sub\left( {\varphi ,s} \right)\] עבור נוסחה plot:\[\varphi \].

נגדיר עבור שם עצם plot:\[t\] את plot:\[sub\left( {t,s} \right)\]:

בסיס:     plot:\[t\] משתנהplot:\[ \Leftarrow \]plot:\[sub\left( {{v_i},s} \right) = s\left( {{v_i}} \right)\].             plot:\[t\] קבועplot:\[ \Leftarrow \]plot:\[sub\left( {c,s} \right) = c\].

סגור:     סימן פונקציה plot:\[ \Leftarrow F\]plot:\[sub\left( {F\left( {{t_1},...,{t_n}} \right),s} \right) = F\left( {sub\left( {{t_1},s} \right),...,sub\left( {{t_n},s} \right)} \right)\].

נגדיר עבור נוסחה plot:\[\varphi \] את plot:\[sub\left( {\varphi ,s} \right)\]:

בסיס:     נוסחה אטומית: plot:\[sub\left( {R\left( {{t_1},...,{t_n}} \right),s} \right) = R\left( {sub\left( {{t_1},s} \right),...,sub\left( {{t_n},s} \right)} \right)\].

סגור:     קשרים: נציג לכל צד בנפרד: דוגמא: plot:\[sub\left( {\alpha  \to \beta ,s} \right) = sub\left( {\alpha ,s} \right) \to sub\left( {\beta ,s} \right)\].

כמתים:

  • plot:\[sub\left( {\forall {v_i}\alpha ,s} \right) = \forall {v_i}sub\left( {\alpha ,s'} \right)\], כאשר plot:\[s'\] מוגדרת כך: לכל plot:\[i \ne j\] plot:\[s'\left( {{v_j}} \right) = s\left( {{v_j}} \right)\]. plot:\[s'\left( {{v_i}} \right) = {v_i}\], כלומר, את המשתה הקשור לא משנים.
  • עבור plot:\[s'\] כנ"ל, plot:\[sub\left( {\exists {v_i}\alpha ,s} \right) = \exists {v_i}sub\left( {\alpha ,s'} \right)\].

תגיות המסמך:

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

תיקון

מציעה להחליף את
(a¬)
ב
a¬
שכן (a¬) אינו פסוק
מאת: משה ב

סמנטיקה
שיתוף:
| עוד