A Place Nearby


Modal Logic 2018

Lecture: HGX205, M 18:30-21
Section: HGW2403, F 18:30-20


Exercise 01

  1. Prove that \(\neg\Box(\Diamond\varphi\wedge\Diamond\neg\varphi)\) is equivalent to \(\Box\Diamond\varphi\rightarrow\Diamond\Box\varphi\). What you have assumed?
  2. Define strategy and winning strategy for modal evaluation games. Prove Key Lemma: \(M,s\vDash\varphi\) iff V has a winning strategy in \(G(M,s,\varphi)\). Prove that modal evaluation games are determined, i.e. either V or F has a winning strategy.

And all exercises for Chapter 2 (see page 23, open minds)

Exercise 02

  1. Let \(T\) with root \(r\) be the tree unraveling of some possible world model, and \(T’\) be the tree unraveling of \(T,r\). Show that \(T\) and \(T’\) are isomorphic.
  2. Prove that the union of a set of bisimulations between \(M\) and \(N\) is a bisimulation between the two models.
  3. We define the bisimulation contraction of a possible world model \(M\) to be the “quotient model”. Prove that the relation links every world \(x\) in \(M\) to the equivalent class \([x]\) is a bisimulation between the original model and its bisimulation contraction.

And exercises for Chapter 3 (see page 35, open minds): 1 (a) (b), 2.

Exercise 03

  1. Prove that modal formulas (under possible world semantics) have ‘Finite Depth Property’.

And exercises for Chapter 4 (see page 47, open minds): 1 – 3.

Exercise 04

    1. Prove the principle of Replacement by Provable Equivalents: if \(\vdash\alpha\leftrightarrow\beta\), then \(\vdash\varphi[\alpha]\leftrightarrow\varphi[\beta]\).
    2. Prove the following statements.
      • “For each formula \(\varphi\), \(\vdash\varphi\) is equivalent to \(\vDash\varphi\)” is equivalent to “for each formula \(\varphi\), \(\varphi\) being consistent is equivalent to \(\varphi\) being satisfiable”.
      • “For every set of formulas \(\Sigma\) and formula \(\varphi\), \(\Sigma\vdash\varphi\) is equivalent to \(\Sigma\vDash\varphi\)” is equivalent to “for every set of formulas \(\Sigma\), \(\Sigma\) being consistent is equivalent to \(\Sigma\) being satisfiable”.
    3. Prove that “for each formula \(\varphi\), \(\varphi\) being consistent is equivalent to \(\varphi\) being satisfiable” using the finite version of Henkin model.

And exercises for Chapter 5 (see page 60, open minds): 1 – 5.

Exercise 05

Exercises for Chapter 6 (see page 69, open minds): 1 – 3.

Exercise 06

  1. Show that “being equivalent to a modal formula” is not decidable for arbitrary first-order formulas.

Exercises for Chapter 7 (see page 88, open minds): 1 – 6. For exercise 2 (a) – (d), replace the existential modality E with the difference modality D. In the clause (b) of exercise 4, “completeness” should be “correctness”.

Exercise 07

  1. Show that there are infinitely many non-equivalent modalities under T.
  2. Show that GL + Id is inconsistent and Un proves GL.
  3. Give a complete proof of the fact: In S5, Every formula is equivalent to one of modal depth \(\leq 1\).

Exercises for Chapter 8 (see page 99, open minds): 1, 2, 4 – 6.

 Exercise 08

  1. Let \(\Sigma\) be a set of modal formulas closed under substitution. Show that \[(W,R,V),w\vDash\Sigma~\Leftrightarrow~ (W,R,V’),w\vDash\Sigma\] hold for any valuation \(V\) and \(V’\). Define a \(p\)-morphism between \((W,R),w\) and \((W’,R’),w’\) as a “functional bisimulation”, namely bisimulation regardless of valuation. Show that if there is a \(p\)-morphism between \((W,R),w\) and \((W’,R’),w’\), then for any valuation \(V\) and \(V’\), we have \[(W,R,V),w\vDash\Sigma~\Leftrightarrow~ (W’,R’,V’),w\vDash\Sigma.\]

Exercises for Chapter 9 (see page 99, open minds).

 Exercise the last

Exercises for Chapter 10 and 11 (see page 117 and 125, open minds).

The idea of a decentralized danmaku (弾幕) and subtitles service

Niconico and bilibili are the two leading streaming video sharing service provider who also feature overlaid comments called danmaku (弾幕).
Continue reading “The idea of a decentralized danmaku (弾幕) and subtitles service”


这是对知乎问题为什么能行可计算的就是图灵可计算的 的回答。

如果我没理解错的话,题主想要问的实际上就是丘奇-图灵论题(Church-Turing Thesis)为什么成立。丘奇-图灵论题简单地说就是:

一个自然数上的函数\(f:\mathbb{N}^n\to\mathbb{N}\)是能行可计算的(effectively computable),当且仅当它是图灵可计算的(Turing computable)。
Continue reading “为什么能行可计算的就是图灵可计算的(递归的)”


1620年11月11日,载着英格兰分离教派清教徒的五月花号终于决定停靠在现马赛诸塞州的鳕鱼角。这不是这片新大陆第一批英语殖民者,当然也不是最后一批。这些殖民者或因为坚持独特的宗教理想或为逃避政治迫害或存粹为了投机而选择离开了欧洲的成熟社会,以寻求各自心中的理想之国。得益于大西洋的阻隔,这群人可以摆脱部分历史束缚,相对自由地开始新的社会实验。十八世纪以来发源于欧洲的启蒙思想和理论在这里找到了理想的实验环境。 Continue reading “加密数字货币、信任与虚拟身份”


手机号码正在被越来越广泛地用作人们的身份证明。没有手机号码越来越难以在现代社会中生活。另一方面,手机号码是真正的不可再生资源。过长的手机号码会增加一系列成本(具体哪些成本、增加多少值得研究)。中国实行的是全世界最长的11位手机号码,容量为千亿,相对中国十亿级别的人口总数看似绰绰有余。但即使有如此冗余的号码容量在毫无管理的情况下也可能被浪费殆尽。 Continue reading “有必要立法保护人们的号码权”