תכונות של מערכת הוכחה

  1. הנחת המבוקש ("מה שרוצים להוכיח הוא אחת ההנחות"): אם plot:\[\alpha  \in X\] אז plot:\[X \vdash \alpha \].
  2. לכל 2 קבוצות פסוקים plot:\[{\Sigma _1},{\Sigma _2}\], אם plot:\[{\Sigma _1} \subseteq {\Sigma _2}\] אז לכל פסוק plot:\[\alpha \], אם plot:\[{\Sigma _1} \vdash \alpha \] אזי plot:\[{\Sigma _2} \vdash \alpha \].

    זוהי מונוטוניות מערכת ההוכחה: plot:\[Ded\left( {{\Sigma _1}} \right) \subseteq Ded\left(
      {{\Sigma _2}} \right) \Leftarrow {\Sigma _1} \subseteq {\Sigma _2}\].

    מסקנה: אם plot:\[ \vdash \alpha \] אזי לכל קבוצה plot:\[\Sigma \] מתקיים plot:\[\Sigma  \vdash \alpha \].
  3. טענות עזר: לכל שתי קבוצות פסוקים plot:\[{\Sigma _1},{\Sigma _2}\], אם לכל plot:\[\alpha  \in {\Sigma _1}\] מתקיים plot:\[{\Sigma _2} \vdash \alpha \] אזי לכל פסוק plot:\[\beta \] אם plot:\[{\Sigma _1} \vdash \beta \] אזי plot:\[{\Sigma _2} \vdash \beta \]. אם plot:\[{\Sigma _1} \subseteq Ded\left( {{\Sigma _2}} \right)\] אז plot:\[Ded\left( {{\Sigma _1}} \right)
      \subseteq Ded\left( {{\Sigma _2}} \right)\].

  1. אם plot:\[\Sigma  \vdash \left( {\alpha  \to \left( {\beta  \to
      \gamma } \right)} \right)\] וגם plot:\[\Sigma  \vdash \left( {\alpha  \to \beta } \right)\] אזי plot:\[\Sigma  \vdash \left( {\alpha  \to \gamma } \right)\].
  2. לכל פונקצית הצבה plot:\[s\]: plot:\[s:\left\{ {{p_i}|i \in \mathbb{N}} \right\} \to WFF\] מתקיים כי אם plot:\[\Sigma  \vdash \alpha \] אז plot:\[sub\left( {\Sigma ,s} \right) = \left\{ {sub\left(
      {\gamma ,s} \right)|\gamma  \in \Sigma } \right\} \vdash sub\left( {\alpha
      ,s} \right)\].
  3. משפט הדדוקציה: לכל קבוצת פסוקים plot:\[\Sigma \] ולכל זוג פסוקים plot:\[\alpha ,\beta \] מתקיים כי plot:\[\Sigma  \cup \left\{ \alpha  \right\} \vdash \beta 
      \Leftrightarrow \Sigma  \vdash \left( {\alpha  \to \beta } \right)\].

שימושים למשפט הדדוקציה

  1. נראה כי לכל פסוק plot:\[\alpha \], מתקיים plot:\[ \vdash \left( {\alpha  \to \alpha } \right)\]: על פי משפט הדדוקציה מספיק שנוכיח כי    plot:\[\left\{ \alpha  \right\} \vdash \alpha \]. סדרת ההוכחה: (הנחה)        plot:\[1)\,\,\alpha \].
  2. נראה plot:\[\left\{ \alpha  \right\}
      \vdash \left( {\left( {\alpha  \to F} \right) \to F} \right)\]. ע"פ משפט הדדוקציה מספיק שנוכיח כי plot:\[\left\{ {\alpha ,\alpha  \to F} \right\} \vdash F\]. סדרת ההוכחה:

1) plot:\[\alpha \] (הנחה)

2) plot:\[\alpha  \to F\] (הנחה)

3) F                                         (MP 1, 2)

  1. נראה:plot:\[\left\{ {\alpha  \to \beta } \right\} \vdash \left\{
      {\beta  \to F} \right\} \to \left\{ {\alpha  \to F} \right\}\]. על פי הדדוקציה מספיק שנוכיח כי plot:\[\left\{ {\alpha  \to \beta ,\beta  \to F,\alpha }
      \right\} \vdash F\]. סדרת ההוכחה:

1) plot:\[\alpha \] (הנחה)

2) plot:\[\alpha  \to \beta \] (הנחה)

3) plot:\[\beta \]                                   (MP 1, 2)

4) plot:\[\beta  \to F\]                    (הנחה)

5) F                                         (MP 3, 4)

תגיות המסמך:

מאת: bentz

תיקון

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

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

סמנטיקה

שיתוף:
| עוד