הצבות

הרעיון: נתון פסוק plot:\[\alpha \] ואנו מעוניינים להחליף כל פסוק אטומי ב-plot:\[\alpha \] בפסוק כלשהו.

בהינתן פונקצית הצבה plot:\[s:\left\{ {{p_i}|i \in \mathbb{N}}
 \right\} \to WFF\] נגדיר באינדוקציה את הפסוק plot:\[sub\left( {\alpha ,s} \right)\] שהוא הפסוק המתקבל מ-plot:\[\alpha \] על ידי החלפת כל מופע של plot:\[{p_i}\] ב-plot:\[s\left( {{p_i}} \right)\].

בסיס: plot:\[\alpha  = {p_i},sub\left( {\alpha ,s} \right) = s\left( {{p_i}} \right),
 & \alpha  = F,sub\left( {\alpha ,s} \right) = F, & \alpha  =
 T,sub\left( {\alpha ,s} \right) = T\].

סגור: עבור plot:\[ \circ  \in \left\{ { \wedge , \vee , \to } \right\}\], מתקיים plot:\[sub\left( {\left( {{\alpha
 _1} \circ {\alpha _2}} \right),s} \right) = \left( {sub\left( {{\alpha _1},s}
 \right) \circ sub\left( {{\alpha _2},s} \right)} \right)\].

כמו כן: plot:\[sub\left( {\neg \alpha ,s}
 \right) = \left( {\neg sub\left( {\alpha ,s} \right)} \right)\].

טענה: לכל פסוק plot:\[\alpha \], אם plot:\[{s_1}\] ו-plot:\[{s_2}\] פונקציות הצבה שמזדהות על כל הפסוקים האטומיים שמופיעים ב-plot:\[\alpha \], אזי plot:\[sub\left( {\alpha ,{s_1}} \right) = sub\left( {\alpha ,{s_2}} \right)\].

טענה: בהינתן פסוק plot:\[\alpha \], פונקצית הצבה plot:\[s\] והשמה plot:\[z\], נגדיר השמה חדשה plot:\[z'\]: plot:\[z'\left( {{p_i}} \right) =
 \bar z\left( {s\left( {{p_i}} \right)} \right)\]. מתקיים: plot:\[\bar z'\left( \alpha  \right) = \bar z\left( {sub\left( {\alpha ,s}
 \right)} \right)\].

טענה: אם plot:\[\alpha \] טאוטולוגיה אזי לכל הצבה plot:\[s\] מתקיים plot:\[sub\left( {\alpha ,s} \right)\] היא טאוטולוגיה (וכך גם לסתירה).

הוכחה: תהי plot:\[z\] השמה. נראה כי plot:\[z \vDash sub\left( {\alpha
 ,s} \right)\]. קיימת השמה plot:\[z'\] עבורה plot:\[\bar z'\left( \alpha  \right) = \bar z\left( {sub\left( {\alpha ,s}
 \right)} \right)\]. plot:\[\alpha \] טאוטולוגיה ולכן plot:\[\bar z'\left( \alpha  \right) = 1\] כלומר גם plot:\[\bar z\left( {sub\left( {\alpha
 ,s} \right)} \right) = 1\].

תגיות המסמך:

מאת: bentz

תיקון

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

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

סמנטיקה

שיתוף:
| עוד