vault backup: 2025-01-16 14:17:53
This commit is contained in:
@@ -128,61 +128,60 @@ $$\forall w \in W,\exists v\to W\ so\ that\ wRv$$
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **רפלקסיבי** מתקיים: $Μ ⊨ Τ$
|
||||
בכל מודל קריפקה M בו יחס הנגישות **רפלקסיבי** מתקיים: $$Μ ⊨ Τ$$
|
||||
|
||||
|
||||
(כאן הייתה הוכחה, והתעצלתי)
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **סדרתי** מתקיים: `Μ ⊨ D`
|
||||
בכל מודל קריפקה M בו יחס הנגישות **סדרתי** מתקיים: $$Μ ⊨ D$$
|
||||
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **טרנזיטיבי** מתקיים `M ⊨ S4` (האקסיומה, לא המערכת).
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **סימטרי** מתקיים `M ⊨ B`
|
||||
בכל מודל קריפקה M בו יחס הנגישות **טרנזיטיבי** מתקיים $M ⊨ S4$
|
||||
|
||||
`Β: Α-> □◇Α`
|
||||
(האקסיומה, לא המערכת).
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות **סימטרי** מתקיים $M ⊨ B$
|
||||
|
||||
$$Β:\ Α \to \Box \Diamond Α$$
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בכל מודל קריפקה M בו יחס הנגישות יהיה **סימטרי** ו**טרנזיטיבי** מתקיים
|
||||
|
||||
`Μ ⊨ ◇Α -> □◇Α`
|
||||
$$Μ \models \Diamond Α \to \Box \Diamond Α$$
|
||||
|
||||
|
||||
## מסגרת
|
||||
|
||||
ומה לגבי מודל שיש בו עולם יחיד, שבו A=T? האם
|
||||
`□Α -> Α`
|
||||
?
|
||||
ומה לגבי מודל שיש בו עולם יחיד, שבו $A=T$? האם $□Α \to Α$?
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
מסגרת C היא קבוצה של מודלי קריפקה שחולקים את אותם עולמות אפשריים ואותו יחס נגישות.
|
||||
|
||||
|
||||
לעיתים נסמן:
|
||||
|
||||
C = <W,R>
|
||||
$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
|
||||
$$
|
||||
\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}
|
||||
$$
|
||||
|
||||
|
||||
המשפטים האלו הם מה שהפכו את קריפקה לקריפקה, והם נאותים ושלמים. הם מראים שאם יש לי הוכחה במסגרות מודלים מסוימות (סדרתיות, סימטריות וכו'), הרי שלא תהיה דוגמה נגדית, ולהיפך - **אם אין דוגמה נגדית, יש הוכחה**.
|
||||
@@ -192,32 +191,27 @@ I.F.F[^2]
|
||||
### הוכחת הנאותות
|
||||
|
||||
**משפט הנאותות** -
|
||||
אם
|
||||
|
||||
⊢(Σ)A
|
||||
|
||||
אזי אין מודל במסגרות הרלוונטיות M כך ש
|
||||
|
||||
Μ ⊭ Α
|
||||
אם $⊢(Σ)A$, אזי אין מודל במסגרות הרלוונטיות $M$ כך ש$Μ ⊭ Α$.
|
||||
|
||||
|
||||
!!! is-info "הגדרה"
|
||||
בהינתן קבוצת פסוקים Δ -
|
||||
בהינתן קבוצת פסוקים $Δ$ -
|
||||
|
||||
□Δ = {B | □B ∈ Δ}
|
||||
$$□Δ = {B\ |\ \Box B \in Δ}$$
|
||||
|
||||
עובדות:
|
||||
|
||||
1. לכל Γ, Σ עקבית-מקסימלית
|
||||
□Δ != Ø
|
||||
1. לכל $Γ, Σ$ עקבית-מקסימלית
|
||||
|
||||
2. לכל Δ,
|
||||
$$□Δ != Ø$$
|
||||
|
||||
Σ עקבית כך ש
|
||||
2. לכל $Δ,Σ$ עקבית כך ש
|
||||
|
||||
~□B ∈ Δ
|
||||
|
||||
□Δυ[~Β] is Σ-consistent
|
||||
$$
|
||||
\neg \Box B \in Δ
|
||||
$$
|
||||
|
||||
|
||||
$$□Δυ[\neg Β]\ is\ Σ-consistent$$
|
||||
|
||||
[^2]: אם ורק אם
|
||||
Reference in New Issue
Block a user