Modal and Superintuitionistic based on new system

[SnO2WMaN]

Rewrite modal logic based on #44

Depends

• system #44
• refactor(Modal): Refactor Modal Logical Connectives #46
• Superintuitionistic based on new system #50

[iehality]

FrameClassの定義に照らし合わせると，（というより，一般にはこういう定義だと思う）Wは型の中に含めてしまったほうが良いと思うが，どうだろう？

structure Frame (α : Type*) where
  World : Type*
  nonempty : Nonempty World
  Rel : World → World → Prop

[iehality]

この方法を採用する場合，αは単なるマーカーなので以下のようにしたほうがいいかもしれない

structure Frame where
  World : Type*
  nonempty : Nonempty World
  Rel : World → World → Prop

set_option linter.unusedVariables false in
abbrev FrameOn (α : Type*) := Frame

[SnO2WMaN]

この定義で少し試してみたが，Formula.Kripke.SatisfiesのSemanticsへのインスタンス化で上手く型を合わせることが出来ず失敗してしまった（wの型がMに依存するためだろうか？）．勘違いかもしれないので試してみてほしい．

[iehality]

Mはwから推論されるので，instance (M : Model α) : Semantics (Formula α) M.frame.Worldを示せばよいと思う（依存積instance : Semantics (Formula α) ((M : Model α) × M.frame.World)で定義してもよいが，型推論がうまく行かないことがある）．Modal/Standard/Kripke/Semantics.leanの冒頭部分だけを書き直してみたが，問題ないと思う．

import Logic.Logic.System
import Logic.Modal.Standard.Formula

universe u

namespace LO.Modal.Standard

namespace Kripke

-- variable (W α : Type*) [Inhabited W]

structure Frame where
  World : Type*
  nonempty : Nonempty World
  Rel : World → World → Prop

structure FiniteFrame extends Frame where
  finite : Finite World

set_option linter.unusedVariables false in
abbrev Frame' (α : Type*) := Frame

set_option linter.unusedVariables false in
abbrev FiniteFrame' (α : Type*) := FiniteFrame

instance (F : Frame) : Nonempty F.World := F.nonempty

abbrev Frame.Rel' {F : Frame} (w w' : F.World) : Prop := F.Rel w w'

scoped infix:45 " ≺ " => Frame.Rel'

-- Vorspiel とかに移動したほうがいいかも
def RelItr {α : Type*} (R : α → α → Prop) : ℕ → α → α → Prop
  | 0 => (· = ·)
  | n + 1 => fun x y ↦ ∃ z, R x z ∧ RelItr R n z y

@[simp] lemma relItr_zero {α : Type*} (R : α → α → Prop) (x y : α) : RelItr R 0 x y ↔ x = y := iff_of_eq rfl

@[simp] lemma relItr_succ {α : Type*} (R : α → α → Prop) (x y : α) :
    RelItr R (n + 1) x y ↔ ∃ z, R x z ∧ RelItr R n z y := iff_of_eq rfl

protected abbrev Frame.RelItr (n : ℕ) {F : Frame} (w w' : F.World) : Prop := RelItr (· ≺ ·) n w w'

scoped notation w:45 " ≺^[" n "] " w':46 => Frame.RelItr n w w'

def Multiframe (F : Frame) (n : ℕ) : Frame where
  World := F.World
  nonempty := F.nonempty
  Rel := (· ≺^[n] ·)

notation:max F "^[" n "]" => Multiframe F n

abbrev Valuation (W α) := W → α → Prop

structure Model (α) where
  frame : Frame
  valuation : Valuation frame.World α

abbrev FrameClass := Set Frame

abbrev FiniteFrameClass := Set FiniteFrame

set_option linter.unusedVariables false in
abbrev FrameClass' (α : Type*) := FrameClass

set_option linter.unusedVariables false in
abbrev FiniteFrameClass' (α : Type*) := FiniteFrameClass

def FrameClass.toFinite (𝔽 : FrameClass) : FiniteFrameClass := {F | F.toFrame ∈ 𝔽}

postfix:max "ꟳ" => FrameClass.toFinite
instance : Coe FrameClass FiniteFrameClass := ⟨λ 𝔽 ↦ 𝔽ꟳ⟩

instance : Coe (FrameClass' α) (FiniteFrameClass' α) := ⟨λ 𝔽 ↦ 𝔽ꟳ⟩

abbrev FrameClass.Nonempty (𝔽 : FrameClass) : Prop := Set.Nonempty 𝔽

abbrev FiniteFrameClass.Nonempty (𝔽 : FiniteFrameClass) := Set.Nonempty 𝔽

abbrev FrameProperty (α : Type u) := Frame' α → Prop

abbrev FiniteFrameProperty (α : Type u) := FiniteFrame' α → Prop

abbrev Model.World (M : Model α) := M.frame.World

end Kripke

variable {W α : Type*} [Inhabited W]

open Standard.Kripke

def Formula.Kripke.Satisfies (M : Kripke.Model α) (w : M.frame.World) : Formula α → Prop
  | atom a  => M.valuation w a
  | falsum  => False
  | and p q => (Satisfies M w p) ∧ (Satisfies M w q)
  | or p q  => (Satisfies M w p) ∨ (Satisfies M w q)
  | imp p q => ¬(Satisfies M w p) ∨ (Satisfies M w q)
  | box p   => ∀ w', w ≺ w' → (Satisfies M w' p)

instance (M : Model α) : Semantics (Formula α) M.World := ⟨fun w ↦ Formula.Kripke.Satisfies M w⟩

open Formula.Kripke

namespace Formula.Kripke.Satisfies

lemma iff_models {M : Model α} {w : M.World} : w ⊧ f ↔ Formula.Kripke.Satisfies M w f := iff_of_eq rfl

instance (M : Model α) : Semantics.Tarski M.World where
  realize_top := by simp [iff_models, Satisfies]
  realize_bot := by simp [iff_models, Satisfies]
  realize_not := by simp [iff_models, Satisfies]
  realize_and := by simp [iff_models, Satisfies]
  realize_or := by simp [iff_models, Satisfies]
  realize_imp := by simp [iff_models, Satisfies, imp_iff_not_or]

variable {M : Model α} {w : M.World} {p q : Formula α}

@[simp] lemma atom_def : w ⊧ atom a ↔ M.valuation w a := by simp [iff_models, Satisfies];

@[simp] lemma box_def : w ⊧ (□p : Formula α) ↔ ∀ w', w ≺ w' → w' ⊧ p := by simp [iff_models, Satisfies];

@[simp] lemma dia_def : w ⊧ (◇p : Formula α) ↔ ∃ w', w ≺ w' ∧ w' ⊧ p := by simp [iff_models, Satisfies];

@[simp]
lemma multibox_def : (w ⊧ (□^[n]p : Formula α)) ↔ (∀ v, w ≺^[n] v → v ⊧ p) := by
  induction n generalizing w with
  | zero => simp;
  | succ n ih =>
    constructor;
    . intro h w' hww';
      simp at h;
      obtain ⟨v, hwv, hvw'⟩ := hww';
      exact (ih.mp $ h _ hwv) w' hvw';
    . simp;
      intro h w' hww';
      apply ih.mpr;
      intro v hwv;
      exact h v w' hww' hwv;

ただ□pの型推論がうまくいかないところが気になる．集合の場合は□'' sなどの表記にするのはどうだろう．

[SnO2WMaN]

全体的にこの方針で書き換えたのだが，Modelが非明示的なので⊧などの表記が使えずSatisfiesで直接書かざるケースが多々あり，やや冗長な気もする．

[iehality]

おそらく多くの場合はノーテーションを若干変えればSatisfiesを使用しなくて済むと思う．例えば，Modal/Standard/Kripke/Semantics.leanではCanonicalFrame Lを最初に定義してしまって，MCT Lについての定理を(CanonicalFrame L).Worldに置き換えて示せばよい．このような言い換えが難しい場合は，フレームf := {World := W, Rel := R}の自明な全単射W ≃ f.Worldを用いてworldにアクセスすればよい．

_.Worldといちいち書くのは面倒なのでinstance : CoeSort Frame Type* where coe := Frame.Worldを定義するといいと思う．

[iehality]

もしくはWを外に出した型クラスと中に含めた型と両方定義する方法もある．FirstOrderではこの方法を採用している（StructureとStruc）．一階論理では特定のモデル（算術の標準モデルなど）に関してなにかを述べることがよくあるのでこの定義は便利だが，様相論理では過剰な気がする．

[SnO2WMaN]

様相論理の書き換えが完了した．残りは直観主義論理の完全性のみ．

[SnO2WMaN]

@iehality

まもなくこのPRでやるべき全ての書き換えが終わるのだが（残りの補題は2つ）， #44 のブランチを最新のmasterに追従してほしい（LICENSEの追加の差分などが入ってしまう：GitHub上で最新に更新することが出来るはず）のとLogic.mainのModalの部分のコメントアウトを外してほしい．（Conflictしているため）

[SnO2WMaN]

全ての書き換えが終わりました．

[SnO2WMaN]

このPR自体がもうかなり大きいためドキュメントについては別PRで出そうと思う．

[SnO2WMaN]

とりあえず修正した．GeachConfluencyの命名規則は一旦保留で．