2.9 Soundness Lemma & Proof

有一個模型M= 是faithful to branch b= df. 存在有一個function,f, f是一個從所有自然數的集合到Wm(世界W的模型m)的函數，而如果A,i 出現在b上，那麼f(i)就會使A為真，而且對任何A,i而言，如果irj是空的滿足又出現在b上，那麼f(i)Rf(j) (f(i)和f(j)有R的關係)，而且是對於任何 i,j而言都成立。

現在，模型M是一個模態的模型，而且b是一真植樹上的branch；如果M是faithful to b，若且為若存在有一個mapping叫做function f，f是一個從自然數集合映射到世界W的函數。所以，對任何在這棵樹上的節點A,i，A,i是出現在b上的，那麼function f 就會使得A為真，寫成f(i) in M。

如果irj在b上，那麼在M之中，f(i)和f(j)有R的關係。

預備定理(Lemma)

讓b是樹上的分枝，而M=< W , R , v>
M是faithful to b，而且這棵樹是已經完成的，那麼我們可以從樹上至少找到一個分枝b'，M也會faithful to b'。

預備定理的證明(Proof)

Case1

1.M會使得分枝b上的A&B,i在f(i)為真，那麼，f(i)就會使A&B為真。

2.假如句子在樹上的是 ~◇A,i，我們可以寫成 □~A,i，所以，M是faithful to b，那麼M就會使 ~◇A在f(i)為真，寫成 ~◇A,i，

3.因此，M也會使 □~A在f(i)為真，寫成 □~A,i。

4.如果 □A,i在b上，而M是faithful to b，□A就是在f(i)為真的。

5.接著，對於任何 i和 j，像irj 這類的關係出現在b上，則 f(i)Rf(j)是成立的，模型M就是faithful to branch b的。

6.最後，◇A,i 是在branch b 上，根據樹枝規則，我們可以獲得一個irj而且A,j出現在枝上，M就會使W和它的可能世界有一個f(i)的函數，並使得A在W的可能世界為真，寫成 ◇A,i以及f(i)Rw。
7.現在有一個f'，將 j帶入，寫成f'(j)，將 i 帶入，寫成f'(i)，在f'(i)和f'(j)之間存在一個關係R，寫成 f'(i)Rf'(j)，而M也會是faithful to branch b，所以也是faithful to 這個 extended的 branch的，也就是faithful to f'(i)Rf'(j)的。


健全性證明(Proof)
1. Σ ⊨ A 不成立
2.存在有一個模型裡的一個世界，這個世界會使得  Σ U {~A}
3. M是faithful to這個branch b的，
4. 如果M是faithful to branch b，那麼M就會faithful to 延伸的branch b1，以及延伸的branch b2，以及延伸的任何branch bi。
5.讓一棵樹T是任何完成的樹，我們可以從這個樹上找到一枝branch bk，而且bk是開放的枝子
6.所以，任何完成的樹會出現Σ U {~A}，而且M是faithful to Σ U {~A}的
7.這是一棵開放的樹T
8. Σ ⊦ A 不成立




note: 如果bk是封閉的，那麼A,i在這枝branch上也會出現~A,i，那麼f(i)就是 ⊨ A 而且f(i)會使得⊨~A成立，這是矛盾的。