מודלי קריפקה

סול קריפקה היה מגדולי הלוגיקנים בכל הזמנים. תרומתו הגדולה, אולי הגדולה ביותר, הגיעה בגיל 15. מה הוא אומר?

רע לובש ז'קט. האם אפשרי עבורו לפשוט אותו? כן. רע פושט את הז'קט. האם עכשיו אפשרי עבורו לפשוט את הז'קט? לא; קריפקה אומר שאפשרות הוא מושג יחסי.

P = Wearing a jacket
Q - Taking of the jacket

Situaion 1: Wearing the jacket
P = T
Q = F

◇Q = T

Situation 2: 
P = F
Q = T

◇Q = F

כלומר, מצב 2 נגיש (accessible) ממצב 1, אבל לא כל הדברים ממצב 1 נגישים ממצב 2.

הגדרה

מודל קריפקה הוא רביעיה סדורה:

\(Μ = <W, @, v, R>\)

(הוספנו \(R\)) כאשר:

\(W\) - קבוצה של עולמות אפשריים

\(@ \in W\) - העולם הממשי

\(R\) - יחס נגישות (בינארי) בין עולמות אפשריים:

\(WRw\)

משמע \(W\) נגיש ל \(w\)

\(V\) - פונקציית הערכה.

\(v(w,P)\) - הערך של P בעולם \(w\).

\(v(W, \not A)\), \(v(W, A \to B)\) - כמו במודלי קארנפ

\(v(w, \Box A) = T\) אם לכל \(w \in W\) כך ש \(wRw\): \(v(w,A) = T\)

\(v(w,\Diamond A) = T\) אם יש \(w \in W\) כך ש \(wRw\): \(v(w,A) = T\)

לכל מודל קריפקה \(M\): \(M \models \Box (A \to B) \to (\Box A \to \Box B)\) (אקסיומה K) כלומר,

\(v(@,K) = T\)

הוכחה:

נניח בשלילה שיש מודל \(M\) כך ש \(Μ \nvDash Κ\)

כלומר, \(v(@,K) = F\)

לכן,

\[ v(@, □(Α -> Β)) = Τ v(@, □Α -> □Β) = F \]

1. נתון \(v(@, □( Α -> Β)) = Τ\) ולכן לכל \(w \in W\) כך ש \(@Rw\)

   \(\(v(w, A-> B) = T\)\) כלומר, בעולם \(@\), \(A\) הכרחי

2. נתון \(v(w, □A) = T\) ולכן לכל \(w \in W\) כך ש \(@Rw\):

   \[v(w, B) = T\]

   כלומר, בעולם \(@\), בהכרח \(B\) שקרי

מ1 ו2 נובע:

\[ v(@, □B) = T \]

בסתירה להנחה.

יחסי נגישות

הנגישות של העולמות במודלי קריפקה מתחלקת לכמה סוגי יחסים:

• רפלקסיביים - כל עולם יכול לגשת לעצמו.

\[\forall w \in W,\ wRw\]

כלומר, אם \(\Box Α\), אז \(A\) אמיתי בעולם הממשי.

• טרנזיטיביים - אם \(w1\) יכול לראות את \(w2\) ו\(w2\) יכול לראות את \(w3\) אזי \(w1\) יכול לראות את \(w3\)

  \[∀w1​, w2​, w3​∈W ,(w1​Rw2​ ∧ w2​Rw3​) \to w1​Rw3​\]

כלומר, אם \(\Box A\), אז \(A\) אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.

• סימטריים - אם \(w1\) יכול לראות את \(w2\) אז \(w2\) יכול לראות את \(w1\).

\[\forall w1​,w2 \in W, w1​Rw2 ​\to w2​Rw1\]

כלומר, כל העולמות נגישים האחד לשני

• סדרתיים - כל עולם יכול לגשת לפחות לעולם אחד נוסף כך ש-

\[\forall w \in W,\exists v\to W\ so\ that\ wRv\]

הגדרה

בכל מודל קריפקה M בו יחס הנגישות רפלקסיבי מתקיים: \(\(Μ ⊨ Τ\)\)

(כאן הייתה הוכחה, והתעצלתי)

הגדרה

בכל מודל קריפקה M בו יחס הנגישות סדרתי מתקיים: \(\(Μ ⊨ D\)\)

הגדרה

בכל מודל קריפקה M בו יחס הנגישות טרנזיטיבי מתקיים \(M ⊨ S4\)

(האקסיומה, לא המערכת).

הגדרה

בכל מודל קריפקה M בו יחס הנגישות סימטרי מתקיים \(M ⊨ B\)

\[Β:\ Α \to \Box \Diamond Α\]

הגדרה

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

\[Μ \models \Diamond Α \to \Box \Diamond Α\]

מסגרת

ומה לגבי מודל שיש בו עולם יחיד, שבו \(A=T\)? האם \(□Α \to Α\)?

הגדרה

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

לעיתים נסמן:

\(C = <W,R>\)

משפטי השלמות של קריפקה

I.F.F¹

\[ \begin{align} ⊨(K)A\ Ι.f.f\ ⊢(K)A \\ ⊨(ref)A\ Ι.f.f\ ⊢(T)A \\ ⊨(serial)A\ Ι.f.f\ ⊢(D)A \\ ⊨(ref + trans)A\ Ι.f.f\ ⊢(S4)A \\ ⊨(Sym)A\ Ι.f.f\ ⊢(b)A \\ ⊨(equiv)A\ Ι.f.f\ ⊢(S5)A \\ \end{align} \]

המשפטים האלו הם מה שהפכו את קריפקה לקריפקה, והם נאותים ושלמים. הם מראים שאם יש לי הוכחה במסגרות מודלים מסוימות (סדרתיות, סימטריות וכו'), הרי שלא תהיה דוגמה נגדית, ולהיפך - אם אין דוגמה נגדית, יש הוכחה.

הוכחת הנאותות

משפט הנאותות - אם \(⊢(Σ)A\), אזי אין מודל במסגרות הרלוונטיות \(M\) כך ש\(Μ ⊭ Α\).

הגדרה

בהינתן קבוצת פסוקים \(Δ\) -

\[□Δ = {B\ |\ \Box B \in Δ}\]

עובדות:

1. לכל \(Γ, Σ\) עקבית-מקסימלית

\[□Δ != Ø\]

1. לכל \(Δ,Σ\) עקבית כך ש

\[ \neg \Box B \in Δ \]

\[□Δυ[\neg Β]\ is\ Σ-consistent\]

---

1. אם ורק אם ↩