5.3 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$ - קבוצה של עולמות אפשריים
$@ \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
-
נתון
v(@, □( Α -> Β)) = Τולכן לכלw \in Wכך ש@Rw(w, A-> B) = T$כלומר, בעולם
@,Aהכרחי -
נתון
v(w, □A) = Tולכן לכלw \in Wכך ש@Rw:(w, B) = T$כלומר, בעולם
@, בהכרחBשקרי
מ1 ו2 נובע:
v(@, □B) = T
בסתירה להנחה.
יחסי נגישות
הנגישות של העולמות במודלי קריפקה מתחלקת לכמה סוגי יחסים:
- רפלקסיביים - כל עולם יכול לגשת לעצמו.
\forall w \in W,\ wRw
כלומר, אם \Box Α, אז A אמיתי בעולם הממשי.
-
טרנזיטיביים - אם
w1יכול לראות אתw2וw2יכול לראות אתw3אזיw1יכול לראות אתw3<20>w1, w2, w3∈W ,(w1Rw2 ∧ w2Rw3) \to w1Rw3$$
כלומר, אם \Box A, אז A אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.
- סימטריים - אם
w1יכול לראות אתw2אזw2יכול לראות אתw1.
\forall w1,w2 \in W, w1Rw2 \to w2Rw1
כלומר, כל העולמות נגישים האחד לשני
- סדרתיים - כל עולם יכול לגשת לפחות לעולם אחד נוסף כך ש-
\forall w \in W,\exists v\to W\ so\ that\ wRv
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות רפלקסיבי מתקיים: Μ ⊨ Τ
(כאן הייתה הוכחה, והתעצלתי)
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סדרתי מתקיים: Μ ⊨ D
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות טרנזיטיבי מתקיים M ⊨ S4
(האקסיומה, לא המערכת).
!!! is-info "הגדרה"
בכל מודל קריפקה M בו יחס הנגישות סימטרי מתקיים M ⊨ B
$$Β:\ Α \to \Box \Diamond Α$$
!!! is-info "הגדרה" בכל מודל קריפקה M בו יחס הנגישות יהיה סימטרי וטרנזיטיבי מתקיים
$$Μ \models \Diamond Α \to \Box \Diamond Α$$
מסגרת
ומה לגבי מודל שיש בו עולם יחיד, שבו A=T? האם □Α \to Α?
!!! is-info "הגדרה" מסגרת C היא קבוצה של מודלי קריפקה שחולקים את אותם עולמות אפשריים ואותו יחס נגישות.
לעיתים נסמן:
$C = <W,R>$
משפטי השלמות של קריפקה
I.F.F1
\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 כך שΜ ⊭ Α.
!!! is-info "הגדרה"
בהינתן קבוצת פסוקים Δ -
$$□Δ = {B\ |\ \Box B \in Δ}$$
עובדות:
- לכל
Γ, Σעקבית-מקסימלית
□Δ != Ø
- לכל
Δ,Σעקבית כך ש
\neg \Box B \in Δ
□Δυ[\neg Β]\ is\ Σ-consistent
-
אם ורק אם ↩︎