vault backup: 2024-12-05 13:17:37

This commit is contained in:
2024-12-05 13:17:37 +02:00
parent 565ca9aa3c
commit c724922a49
4 changed files with 185 additions and 123 deletions

View File

@@ -0,0 +1,176 @@
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
```
1. נתון `v(@, □( Α -> Β)) = Τ` ולכן לכל `w∈ W` כך ש `@Rw`
`v(w, A-> B) = T`
כלומר, בעולם @, A הכרחי
2. נתון `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.t[^1]).
∀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.F[^2]
⊨(K)A Ι.f.f ⊢(K)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
המשפטים האלו הם מה שהפכו את קריפקה לקריפקה, והם נאותים ושלמים.
[^1]: כך ש
[^2]: אם ורק אם