4.8 KiB
title: מודלי קריפקה
סול קריפקה היה מגדולי הלוגיקנים בכל הזמנים. תרומתו הגדולה, אולי הגדולה ביותר, הגיעה בגיל 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.
!!! info "הגדרה" מודל קריפקה הוא רביעיה סדורה:
`Μ = <W, @, v, R>`
(הוספנו `R`) כאשר:
W - קבוצה של עולמות אפשריים
@ ∈ W - העולם הממשי
R - יחס נגישות (בינארי) בין עולמות אפשריים:
wRw
משמע W נגיש ל W
V - פונקציית הערכה.
v(w,P) - הערך של P בעולם W.
v(W, ~A), v(W, A-> B) - כמו במודלי קארנפ
v(w,□A) = T אם לכל w ∈ W כך ש wRw: v(w,A) = T
v(w,◇A) = T אם יש w ∈ W כך ש wRw: v(w,A) = T
לכל מודל קריפקה M:
M ⊨ □ (A -> B) -> (□A -> □B) (אקסיומה K)
כלומר,
v(@,K) = T
הוכחה:
נניח בשלילה שיש מודל M כך ש Μ ⊭ Κ
כלומר,
v(@,K) = F
לכן,
v(@, □(Α -> Β)) = Τ
v(@, □Α -> □Β) = F
-
נתון
v(@, □( Α -> Β)) = Τולכן לכלw∈ Wכך ש@Rwv(w, A-> B) = Tכלומר, בעולם @, A הכרחי -
נתון
v(w, □A) = Tולכן לכלw∈ Wכך ש@Rw:v(w, B) = Tכלומר, בעולם @, בהכרח B שקרי
מ1 ו2 נובע:
v(@, □B) = T
בסתירה להנחה.
יחסי נגישות
הנגישות של העולמות במודלי קריפקה מתחלקת לכמה סוגי יחסים:
-
רפלקסיביים - כל עולם יכול לגשת לעצמו.
∀w∈W,wRw
כלומר, אם □Α, אז A אמיתי בעולם הממשי.
-
טרנזיטיביים - אם
w1יכול לראות אתw2וw2יכול לראות אתw3אזיw1יכול לראות אתw3∀w1, w2, w3∈W ,(w1Rw2 ∧ w2Rw3) -> w1Rw3
כלומר, אם □Α, אז A אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.
-
סימטריים - אם
w1יכול לראות אתw2אזw2יכול לראות אתw1.∀w1,w2∈W,w1Rw2⟹w2Rw1כלומר, כל העולמות נגישים האחד לשני
-
סדרתיים - כל עולם יכול לגשת לפחות לעולם אחד נוסף (s.t1 ).
∀w∈W,∃v∈W s.t. wRv
!!! info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות רפלקסיבי מתקיים: Μ ⊨ Τ
(כאן הייתה הוכחה, והתעצלתי)
!!! info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סדרתי מתקיים: Μ ⊨ D
!!! info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות טרנזיטיבי מתקיים M ⊨ S4 (האקסיומה, לא המערכת).
!!! info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סימטרי מתקיים M ⊨ B
`Β: Α-> □◇Α`
!!! info "הגדרה" בכל מודל קריפקה M בו יחס הנגישות יהיה סימטרי וטרנזיטיבי מתקיים
`Μ ⊨ ◇Α -> □◇Α`
מסגרת
ומה לגבי מודל שיש בו עולם יחיד, שבו A=T? האם
□Α -> Α
?
!!! info "הגדרה" מסגרת C היא קבוצה של מודלי קריפקה שחולקים את אותם עולמות אפשריים ואותו יחס נגישות.
לעיתים נסמן:
C = <W,R>
משפטי השלמות של קריפקה
I.F.F2
⊨(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
המשפטים האלו הם מה שהפכו את קריפקה לקריפקה, והם נאותים ושלמים. הם מראים שאם יש לי הוכחה במסגרות מודלים מסוימות (סדרתיות, סימטריות וכו'), הרי שלא תהיה דוגמה נגדית, ולהיפך - אם אין דוגמה נגדית, יש הוכחה.
הוכחת הנאותות
משפט הנאותות - אם
⊢(Σ)A
אזי אין מודל במסגרות הרלוונטיות M כך ש
Μ ⊭ Α