日々の流転

λ. SLACS 2006

に参加。 しかし、みんな頭いいしちゃんと研究してるよなぁ。 いつものように凹んできた。

以下色々書くが、これらは講演内容をまとめたわけではなく、私の単なるメモであり、偏っており間違いを含む可能性も高いのでご注意を。まあ、真に受ける人はいないと思うが。

λ. A subsystem of sequent calculus isomorphic to natural deduction

発表者

中澤巧爾 (京都大学)

概要

シーケント計算のカット除去と自然演繹の正規化との関連について。

自然演繹とシーケント計算はしっかり対応しているものだと思い込んでいたけど、そうでもないのだな。それが一番驚きだった。 NJ_g は β と π (permutative conversion) を持つ自然演繹の体系。シーケント計算のカットには principal cut (p-cut) とそれ以外 (n-cut) があり、p-cutのみを持つ体系が LJ_p 。

• LJ_p ≅ NJ_g
• LJ ≅ NJ_g + ?(explicit substitution)

興味深い話だっただけに、あまり覚えていないのが残念。

• β-protocol ≅ β-reduction
• π-protocol ≅ π-reduction
• n-cut elim ≅ propagation of explicit subst

λ. Kleese's slash interpretationの統一的記述について

発表者

小島健介 (京都大学)

概要

Kleene's slash interpretationは直観主義論理におけるdisjunctionとexistenceの性質を調べるために導入された解釈の一つである。その定式化は対象となる体系ごとに別々に行われていたが、これを統一的に記述することができないかを一階の体系に限定して考察する。

slash interpretation は Kleene がDisjunctionやExistenceの直観主義論理での振る舞いを調べるために、Disjunction and Existence Under Implication in Elementary Intuitionistic Formalisms. Journal of Symbolic Logic, Vol. 27, No. 1 (Mar., 1962), pp. 11-18 で導入したもの(らしい)。

直観主義命題論理(IPL) の slash interpretation では、二項関係 Γ | A を次のように定義。

• Γ | p ⇔ Γ ⊢ p
• Γ | A∧B ⇔ Γ | A and Γ | B
• Γ | A∨B ⇔ (Γ ⊢ A and Γ | A) or (Γ ⊢ B and Γ | B)
• Γ | A→B ⇔ if (Γ ⊢ A and Γ | A) then Γ | B
• Γ | ¬A ⇔ if (Γ ⊢ A and Γ | A) then Γ ⊢ ⊥

これを使うことで、健全性と disjunction property について言うことが出来る(具体的なstatementは忘れた)。

一階述語論理に拡張するには以下のようにする。

• Γ | ∀x.A[x] ⇔ ∀t. Γ | A[t]
• Γ | ∃x.A[x] ⇔ ∃t. Γ ⊢ A[t] and Γ | A[t]

これを使うことで「If - ⊢ A then - | A」が言える。

HA(Heyting Arithmetics)に拡張するには以下のようにする。

• Γ | s=t ⇔ Γ ⊢ s=t
• Γ | ∀x.A[x] ⇔ ∀n∈ω. Γ | A[n]
• Γ | ∃x.A[x] ⇔ ∃n∈ω. Γ ⊢ A[n] and Γ | A[n]

この場合には「If A is closed and - ⊢ A then - | A.」が言える。ただし、- ⊢ A であっても一般には - | A とは限らないので注意(e.g. x=0∨x≠0)。

一般化の方針として、普通のモデルと slash を混ぜてみることを考えた。 first-order structure A と 二項関係 ⊢ が与えられたときに、ρ | A を以下のように定義。

• ρ | P ⇔ ρ ⊨ P and P : atomic
• …
• ρ | ∀x.A[x] ⇔ ∀a∈|A|. ρ(x := a) | A[a]
• ρ | ∃x.A[x] ⇔ ∀a∈|A|. ρ(x := a) ⊢ A and ρ(x := a) | A[a]

これを使って健全性のための十分条件を与える(具体的なstatementは忘れた)。

既存の slash interpretation との対応。

• FOLのslashにはterm model のようなものを考えることで対応
• HAのslashとは閉じた論理式について一致

まとめ

• 普通のstructureを考えてtruthをslashのように定義してみた
• 適切な条件を満たすと健全性が成り立つ
• 定義した枠内でslashの定式化を試みた
  • 一階述語論理では成功
  • 算術では完全には一致しない

質疑応答で「q-realizability interpretation を使わないのは何故か?」というツッコミを龍田先生から言われていた。 それから、休憩時間中の雑談で「帰納的定義」に対して q-realizability interpretation を与える話が出ていた。私は realizability の話は全然知らないけど、気になるなぁ。

λ. The upper part of the lattice NExt(KTB)

発表者

宮崎裕 (北海道大学)

概要

We will describe the structure of the upper part of the lattice of normal modal logics containing KTB, and discuss some related problems.

normal-extension

tra_n = □ⁿ p → □ⁿ⁺¹ p

このクラスの cardinality は 非可算個

量子論理のlatticeであるortholatticeをKTBに埋め込める(?)。それから、KTBやNExt(KTB) についての研究は意外と行われていない、というのもこの研究を始めた理由。

λ. お昼

佐々木克巳先生とご一緒した。TRATTORIA Alioli というところで、ポルチーニ茸のクリームスパゲティ。おいしかった。

λ. A Hybridization of Irreflexive Modal Logics

発表者

佐野勝彦 (京都大学)

概要

Unlike ordinary modal language, hybrid language makes it possible to refer to states (possible worlds) in formulas. This is achieved by a class of formulas called nominals. This talk discusses hybrid language with a sub-modality (called the irreflexive modality) associated with the intersection of the accessibility relation R and the inequality. First, we provide the Hilbert-style axiomatizations (with and without the Gabbay-style rule) for logics of our language, and prove the Kripke completeness. Second, with respect to the frame expressive power, we compare the effect of the irreflexive modality with that of nominals. Finally, we establish the Goldblatt-Thomason-style characterization for our language.

Hybrid Logic については存在すら知らなかったが、結構面白そう。

• Hybrid Logics' Home Page
• Stanford Encyclopedia of Philosophy - Hybrid Logic

非反射的な様相論理をハイブリッド化したらどうなるか?

Modest ◆ gives MORE expressive power to HLs!

Two topological interpretation of ◇:

• ◇ as closure: w ∈ V(◇φ) ⇔ w ∈ ~(V(φ))
• ◇ as derivative: w ∈ V(◇φ) ⇔ w ∈ ~(V(φ)＼w)

<R∩S)i ⇔ <R>i ∧ <S>i

Ultrafilter Extension

λ. 様相定数loopを含む様相論理について

発表者

鈴木徹 (東京工業大学)

ここで言う様相定数はp,q,rといった変数と、⊥,Tといった定数の中間のイメージ。モデルの付値には依存しないが、モデルの形状に依存する。ここで導入するloopはxRxである可能世界xでのみ真になるような様相定数。 loopを導入した体系に関する基本的な性質色々 (配布資料があったので、後でゆっくり読む)。 「■」を加えてもこのloopは表現できない。何故なら、以下の二つを区別できないため。

質疑応答では、このモデルの作り方だとK4(違ったかも?)とかには使えないといった話があった。

【追記】 2006年度 MLG 数理論理学研究集会(第40回)の発表資料。<URL:http://matu.cc.kyushu-u.ac.jp/mlg/pdf/TouluSuzuki.pdf>

λ. 知識論理による匿名性検証のための関数部分知識モデル

発表者

川本裕輔 (東京大学)

知識論理(modal logic of knowledge?)とマルチエージェントシステムを用いた匿名性検証の話。

Fagin, R., J. Y. Halpern, Y. Moses, and M. Y. Vardi (1995). Reasoning about Knowledge. Cambridge, Mass.: MIT Press.

Halpern, J. Y., and O'Neill, K. Anonymity and information hiding in multiagent systems. In Proc. of the 16th IEEE Computer Security Foundations Workshop (2003), pp. 75–88. <URL:http://citeseer.ist.psu.edu/halpern03anonymity.html> で知識論理による匿名性の定式化が行われている(?)。

λ. CM: TLCA 2007

International Conference on Typed Lambda Calculi and Applications.

Important dates:

Dec 22

Title and abstract due

Jan 2

Deadline for submission

Mar 25

Notification of acceptance-rejection

λ. Some classes of relevant modal logics

発表者

関隆宏 (九州大学)

概要

メタ完全な適切論理は構文論的な面から2種類に分類できることが知られている。適切様相論理に対してこのような分類が可能であるか、あるいは別の側面から分類できるかどうかについて考えていく。

Relevant logic (適切論理)は、古典論理のパラドックスを除くために考えられた。

1. paradox of relevance: A→(B→A), A→(B→B)
2. paradox of consistency: (A∧¬A)→B, A→(B∨¬B)

命題適切論理の一つの特徴は「A→B が定理ならばA,Bが共通の命題変数を含む」という点。適切論理にも色々なものがある(最も基本的なのがB)。様相論理は通常古典論理の上で議論されるが、非古典論理上の様相論理が最近(?)注目されてる。ここでは適切論理をベースとした様相論理。

A logic is metacomplete if exactly the sentences true on a certain perferred interpretation of that logic in its metalogic are theorems. メタ完全な適切論理は Reductio 「A ⇒ ~(A→~A)」を認めるかどうかで二つに分類できる(M1-logic, M2-logic)。

適切論理に基づく様相論理で最も基本的なものが B.C_□◇ 。これはnormalではないがregularな様相論理。T-axioms「□A→A」「A→◇A」を認めるか否かで二つに分類できる(ように見える)。Reductioによる分類とあわせて四つに分類。

Metavaluations に関する Slaney's method 。

• The primeness is often called the disjunction property
• Two kind of the primeness
  1. Intuitionistic primeness (IP): if ⊢A∨B, then ⊢A ∨ ⊢B.
  2. Modal primeness (MP): if ⊢□A∨□B, then ⊢A ∨ ⊢B

λ. 帰り

寝不足でしんどいので懇親会には出ずに帰ることに。 明日は PPL Summer School もあるしね。