Representing Imperfect Information of Procedures with Hyper Models - Logic and Its Applications - page 226

we first show that if ˆ is necessarily truethenitistrue, and if it is true then it is possibly
true.

Lemma 1. Fo r all the pointed simple hyper model M ,s , any ˆ the following two hold:

1. M,s ˆ implies M,s 0 ˆ

2. M ,s 0 ˆ implies M ,s ♦ ˆ

Therefore M ,s ˆ implies M ,s ♦ ˆ .

Proof. We prove the two claims simultaneously by induction on the structure of ˆ.
ˆ = p or ˆ = ˆ 1 ∧ ˆ 2 : trivial. For ˆ = ¬ ˈ :Suppose M ,s ¬ ˈ then according

to the semantics, M ,s ♦ ˈ thus by IH (2nd claim), we have M ,s 0 ˈ namely

M ,s 0 ¬ ˈ . Similar for the second claim. For ˆ = Kˈ :Suppose M ,s Kˈ

then M ,s ˈ thus according to the semantics M ,s 0 Kˈ . Similarly, suppose

M ,s 0 Kˈ then M ,s ˈ ,thus M ,s ♦ Kˈ according to the semantics.

Ss a

For ˆ = a ˆ :Suppose M ,s a ˈ then there exists T ↆ → ∃ T and

T ˈ . According to the definition of hyper models, there is a t ∈ T such that

a
→

a
→ s t and M ,t ˈ .ByIHwehavethereisa t such that s t and M ,t 0 ˈ

thus M ,s 0 a ˈ. Now for the second claim, suppose M ,s 0 a ˈ then there is

a
→ a t 0 such that s t 0 and M ,t 0 0 ˈ .ByIH, M ,t 0 ♦ ˈ . In order to show that

a
→ ∀ T implies that there is a t

M ,s ♦ a ˈ , we prove that for all T ↆ S : s ∈ T

♦ ˈ .Suppose not, then there exists a T 0 such that s a

such that M ,t → ∀ T 0 and for all

a
→ ∀ T 0 , by the definition of hyper models we have for

t ∈ T 0 : M ,t ♦ ˈ .Since s

a
→

a
→

all t : s t implies t ∈ T 0 .Since s t 0 , t 0 ∈ T 0 thus M ,t 0 ♦ ˈ , contradiction.

a
→ ∀ T implies there is a t such that Therefore for all T ↆ S : s M ,t ♦ ˈ , namely,

M ,s ♦ a ˈ .

Theorem 1. The following S5 axiom schemas are valid: DIST : K ( ˆ → ˈ ) → ( Kˆ→
Kˈ ) , T : Kˆ→ ˆ,

4 : Kˆ→ KKˆ, 5 : ¬Kˆ→ K¬Kˆ

Proof. For DIST :
M

,s K ( ˆ → ˈ ) → ( Kˆ → Kˈ )

⃒⃐ M ,s 0 K ( ˆ → ˈ ) implies M ,s 0 ( Kˆ → Kˈ )

⃒⃐ M ,s ˆ → ˈ implies

( M ,s ˆ implies M ,s ˈ )

⃒⃐ ( M ,s ♦ ˆ implies M ,s ˈ ) implies

( M ,s ˆ implies M ,s ˈ )

Now suppose ( M ,s ♦ ˆ implies M ,s ˈ ) and M ,s ˆ .Since M ,s ˆ

then by Theorem 1, we have M ,s ♦ ˆ .Thus M ,s ˈ .

For T :

M,s Kˆ→ ˆ
⃒⃐ M ,s 0 Kˆ implies M ,s 0 ˆ

⃒⃐ M ,s ˆ implies M ,s 0 ˆ

From Theorem 1, it is clear that M ,s Kˆ → ˆ .