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


1. נתון $v(@, □( Α -> Β)) = Τ$ ולכן לכל $w \in W$ כך ש $@Rw$
	
	$$v(w, A-> B) = T$$
	כלומר, בעולם $@$, $A$ הכרחי

2. נתון  $v(w, □A) = T$ ולכן לכל $w \in W$ כך ש  $@Rw$:
	
	$$v(w, B) = T$$
	
	כלומר, בעולם $@$, בהכרח $B$ שקרי


מ1 ו2 נובע:


$$
v(@, □B) = T
$$

**בסתירה להנחה**.

## יחסי נגישות 

הנגישות של העולמות במודלי קריפקה מתחלקת לכמה סוגי יחסים:

- **רפלקסיביים** - כל עולם יכול לגשת לעצמו.

$$\forall w \in W,\ wRw$$

כלומר, אם $\Box Α$, אז $A$ אמיתי בעולם הממשי.


- **טרנזיטיביים** - אם  $w1$ יכול לראות את $w2$ ו$w2$ יכול לראות את $w3$  אזי $w1$  יכול לראות את $w3$ 

	$$∀w1​, w2​, w3​∈W ,(w1​Rw2​ ∧ w2​Rw3​) \to w1​Rw3​$$

כלומר, אם $\Box A$, אז $A$ אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.


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

$$\forall w1​,w2 \in W, w1​Rw2 ​\to w2​Rw1$$

כלומר, כל העולמות נגישים האחד לשני

- **סדרתיים** - כל עולם יכול לגשת לפחות לעולם אחד נוסף כך ש-

$$\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`
	
	`Β: Α-> □◇Α`


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


[^2]: אם ורק אם