vault backup: 2025-01-16 13:17:53
This commit is contained in:
@@ -30,66 +30,71 @@ Q = T
|
||||
!!! is-info "הגדרה"
|
||||
**מודל קריפקה** הוא רביעיה סדורה:
|
||||
|
||||
Μ = <W, @, v, R>
|
||||
|
||||
(הוספנו `R`) כאשר:
|
||||
$Μ = <W, @, v, R>$
|
||||
|
||||
W - קבוצה של עולמות אפשריים
|
||||
(הוספנו $R$) כאשר:
|
||||
|
||||
@ ∈ W - העולם הממשי
|
||||
$W$ - קבוצה של עולמות אפשריים
|
||||
|
||||
R - יחס נגישות (בינארי) בין עולמות אפשריים:
|
||||
$@ \in W$ - העולם הממשי
|
||||
|
||||
wRw
|
||||
$R$ - יחס נגישות (בינארי) בין עולמות אפשריים:
|
||||
|
||||
משמע W נגיש ל W
|
||||
$WRw$
|
||||
|
||||
משמע $W$ נגיש ל $w$
|
||||
|
||||
V - פונקציית הערכה.
|
||||
$V$ - פונקציית הערכה.
|
||||
|
||||
v(w,P) - הערך של P בעולם W.
|
||||
$v(w,P)$ - הערך של P בעולם $w$.
|
||||
|
||||
v(W, ~A), v(W, A-> B) - כמו במודלי קארנפ
|
||||
$v(W, \not A)$, $v(W, A \to B)$ - כמו במודלי קארנפ
|
||||
|
||||
v(w,□A) = T אם לכל w ∈ W כך ש wRw: v(w,A) = T
|
||||
$v(w, \Box A) = T$ אם לכל $w \in W$ כך ש $wRw$: $v(w,A) = T$
|
||||
|
||||
v(w,◇A) = T אם יש w ∈ W כך ש wRw: v(w,A) = T
|
||||
$v(w,\Diamond A) = T$ אם יש $w \in W$ כך ש $wRw$: $v(w,A) = T$
|
||||
|
||||
|
||||
לכל מודל קריפקה M:
|
||||
`M ⊨ □ (A -> B) -> (□A -> □B)` (אקסיומה K)
|
||||
לכל מודל קריפקה $M$:
|
||||
$M \models \Box (A \to B) \to (\Box A \to \Box B)$ (אקסיומה K)
|
||||
כלומר,
|
||||
|
||||
`v(@,K) = T`
|
||||
$v(@,K) = T$
|
||||
|
||||
הוכחה:
|
||||
|
||||
נניח בשלילה שיש מודל M כך ש `Μ ⊭ Κ`
|
||||
נניח בשלילה שיש מודל $M$ כך ש $Μ \nvDash Κ$
|
||||
|
||||
כלומר,
|
||||
`v(@,K) = F`
|
||||
$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`:
|
||||
1. נתון $v(@, □( Α -> Β)) = Τ$ ולכן לכל $w \in W$ כך ש $@Rw$
|
||||
|
||||
`v(w, B) = T`
|
||||
$$v(w, A-> B) = T$$
|
||||
כלומר, בעולם $@$, $A$ הכרחי
|
||||
|
||||
2. נתון $v(w, □A) = T$ ולכן לכל $w \in W$ כך ש $@Rw$:
|
||||
|
||||
כלומר, בעולם @, בהכרח B שקרי
|
||||
$$v(w, B) = T$$
|
||||
|
||||
כלומר, בעולם $@$, בהכרח $B$ שקרי
|
||||
|
||||
|
||||
מ1 ו2 נובע:
|
||||
|
||||
`v(@, □B) = T`
|
||||
|
||||
$$
|
||||
v(@, □B) = T
|
||||
$$
|
||||
|
||||
**בסתירה להנחה**.
|
||||
|
||||
## יחסי נגישות
|
||||
@@ -98,29 +103,32 @@ v(@, □Α -> □Β) = F
|
||||
|
||||
- **רפלקסיביים** - כל עולם יכול לגשת לעצמו.
|
||||
|
||||
∀w∈W,wRw
|
||||
כלומר, אם `□Α`, אז A אמיתי בעולם הממשי.
|
||||
$$\forall w \in W,\ wRw$$
|
||||
|
||||
כלומר, אם $\Box Α$, אז $A$ אמיתי בעולם הממשי.
|
||||
|
||||
|
||||
- **טרנזיטיביים** - אם `w1` יכול לראות את `w2` ו`w2` יכול לראות את `w3` אזי `w1` יכול לראות את `w3`
|
||||
- **טרנזיטיביים** - אם $w1$ יכול לראות את $w2$ ו$w2$ יכול לראות את $w3$ אזי $w1$ יכול לראות את $w3$
|
||||
|
||||
∀w1, w2, w3∈W ,(w1Rw2 ∧ w2Rw3) -> w1Rw3
|
||||
$$∀w1, w2, w3∈W ,(w1Rw2 ∧ w2Rw3) \to w1Rw3$$
|
||||
|
||||
כלומר, אם `□Α`, אז A אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.
|
||||
כלומר, אם $\Box A$, אז $A$ אמיתי בכל העולמות הנגישים, לרבות העולם הממשי.
|
||||
|
||||
|
||||
- **סימטריים** - אם `w1` יכול לראות את `w2` אז `w2` יכול לראות את `w1`.
|
||||
- **סימטריים** - אם $w1$ יכול לראות את $w2$ אז $w2$ יכול לראות את $w1$.
|
||||
|
||||
$$\forall w1,w2 \in W, w1Rw2 \to w2Rw1$$
|
||||
|
||||
כלומר, כל העולמות נגישים האחד לשני
|
||||
|
||||
- **סדרתיים** - כל עולם יכול לגשת לפחות לעולם אחד נוסף כך ש-
|
||||
|
||||
$$\forall w \in W,\exists v\to W\ so\ that\ wRv$$
|
||||
|
||||
∀w1,w2∈W,w1Rw2⟹w2Rw1
|
||||
כלומר, כל העולמות נגישים האחד לשני
|
||||
|
||||
- **סדרתיים** - כל עולם יכול לגשת לפחות לעולם אחד נוסף (s.t[^1]).
|
||||
|
||||
∀w∈W,∃v∈W s.t. wRv
|
||||
|
||||
---
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **רפלקסיבי** מתקיים: `Μ ⊨ Τ`
|
||||
בכל מודל קריפקה M בו יחס הנגישות **רפלקסיבי** מתקיים: $Μ ⊨ Τ$
|
||||
|
||||
|
||||
(כאן הייתה הוכחה, והתעצלתי)
|
||||
@@ -212,5 +220,4 @@ I.F.F[^2]
|
||||
□Δυ[~Β] is Σ-consistent
|
||||
|
||||
|
||||
[^1]: כך ש
|
||||
[^2]: אם ורק אם
|
||||
Reference in New Issue
Block a user