5.1 KiB
title: מודלי קריפקה
סול קריפקה היה מגדולי הלוגיקנים בכל הזמנים. תרומתו הגדולה, אולי הגדולה ביותר, הגיעה בגיל 15. מה הוא אומר?
!!! is-info "" רע לובש ז'קט. האם אפשרי עבורו לפשוט אותו? כן. רע פושט את הז'קט. האם עכשיו אפשרי עבורו לפשוט את הז'קט? לא; קריפקה אומר שאפשרות הוא מושג יחסי.
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.
!!! is-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
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות רפלקסיבי מתקיים: Μ ⊨ Τ
(כאן הייתה הוכחה, והתעצלתי)
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סדרתי מתקיים: Μ ⊨ D
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות טרנזיטיבי מתקיים M ⊨ S4 (האקסיומה, לא המערכת).
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סימטרי מתקיים M ⊨ B
`Β: Α-> □◇Α`
!!! is-info "הגדרה" בכל מודל קריפקה M בו יחס הנגישות יהיה סימטרי וטרנזיטיבי מתקיים
`Μ ⊨ ◇Α -> □◇Α`
מסגרת
ומה לגבי מודל שיש בו עולם יחיד, שבו A=T? האם
□Α -> Α
?
!!! is-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 כך ש
Μ ⊭ Α
!!! is-info "הגדרה" בהינתן קבוצת פסוקים Δ -
□Δ = {B | □B ∈ Δ}
עובדות:
-
לכל Γ, Σ עקבית-מקסימלית □Δ != Ø
-
לכל Δ,
Σ עקבית כך ש
~□B ∈ Δ
□Δυ[~Β] is Σ-consistent