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
``` 

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 ,(w1​Rw2​ ∧ w2​Rw3​) -> w1​Rw3​

כלומר, אם `□Α`, אז A אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.


- **סימטריים** - אם `w1` יכול לראות את `w2` אז `w2` יכול לראות את `w1`.

		∀w1​,w2​∈W,w1​Rw2​⟹w2​Rw1​
	כלומר, כל העולמות נגישים האחד לשני

- **סדרתיים** - כל עולם יכול לגשת לפחות לעולם אחד נוסף (s.t[^1]).

		∀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.F[^2]

		⊨(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 ∈ Δ}

עובדות:

1. לכל Γ, Σ עקבית-מקסימלית 
		□Δ != Ø

2. לכל Δ,

Σ עקבית כך ש

	~□B ∈ Δ
	
	□Δυ[~Β] is Σ-consistent


[^1]: כך ש
[^2]: אם ורק אם