Provability Logic: □ and ⋄ modalities

provability_logic.lean

import tactic

-- https://math.berkeley.edu/~buehler/The%20Logic%20of%20Provability.pdf

variables {p q : Prop}

axiom box : Prop → Prop
prefix `□`:95 := box -- \B

@[simp] def dia (p : Prop) := ¬□¬p
prefix `⋄`:95 := dia -- \dia

axiom K : □(p → q) → □p → □q
axiom L : □(□p → p) → □p
axiom necessity : p → □p

lemma impl_box (h : p → q) : □p → □q := K (necessity h)

#check λ h, K (impl_box and.intro h)

lemma and_box_iff : □(p ∧ q) ↔ □p ∧ □q :=
begin
  split,
  { intro h,
    split,
    exact impl_box and.elim_left h,
    exact impl_box and.elim_right h },
  { rintro ⟨hp, hq⟩,
    exact K (impl_box and.intro hp) hq }
end

#print and_box_iff

lemma impl_dia (h : p → q) : ⋄p → ⋄q := λ hp, hp ∘ impl_box (mt h)

lemma K4 : □p → □□p := K (necessity necessity)

-- (1)
lemma S4 : ¬(∀ p, □p → p) := λ h, h false (L (necessity (h false)))

-- (2)
example (h₁ : □p → p) (h₂ : □(□p → p)) : p := h₁ (L h₂)
example (h : □(□false → false)) : □false := L h

example (h : ⋄p) : ⋄(p ∧ □¬p) :=
begin
  intro _, clear a,
  apply h,
  apply L,
  apply necessity,
  intros h' _, clear a,
  exact h h'
end

example (h : ⋄true) : ¬□⋄true :=
begin
  intro _, clear a,
  apply h,
  apply L,
  apply necessity,
  intros h' _, clear a,
  exact h h'
end

-- (4)
example : ¬⋄p :=
begin
  intro h,
  apply h,
  apply L,
  apply necessity,
  intros h' _, clear a,
  exact h h'
end

example : ¬¬□false :=
begin
  intro h,
  apply h,
  apply L,
  exact necessity h
end

-- (5)
example : ¬□⋄true := sorry

-- (6)
example (h : □p → p) : p :=
begin
  apply h,
  apply L,
  exact necessity h
end

-- (7)
#check necessity false.elim

example : □false → □⋄true := λ h, K (necessity false.elim) h

example : □false ↔ □⋄true :=
begin
  split; intro h,
  { apply K,
    apply necessity false.elim,
    exact h },
  { sorry }
end

#check function.const _

def hook (p q : Prop) := □(p → q)
infix `≺`:53 := hook -- \prec
 
example : □p ↔ (p → p) ≺ p :=
begin
  split; intro h,
  { refine K _ h,
    exact necessity (function.const _) },
  { refine K h _,
    exact necessity id }
end