Kripke.agda

module Kripke where

open import Prelude
open import Data.Bool
open import Data.Empty
open import Data.Sum
open import Data.Nat

-- ───────────────────────────────────────────────
-- 1. SYNTAX OF INTUITIONISTIC PROPOSITIONAL LOGIC
-- ───────────────────────────────────────────────

Var : 𝒰
Var = ℕ

data Formula : 𝒰 where
  atom : Var → Formula
  _⇒i_ : Formula → Formula → Formula
  _∨i_ : Formula → Formula → Formula
  _∧i_ : Formula → Formula → Formula
  ⊥i   : Formula

¬i_  : Formula → Formula
¬i A = A ⇒i ⊥i

-- ───────────────────────────────────
-- 2. PROOF SYSTEM (natural deduction)
-- ───────────────────────────────────

-- Contexts are lists of formulas
data Ctx : 𝒰 where
  ∅   : Ctx
  _,_ : Ctx → Formula → Ctx

-- Membership
data _∈i_ : Formula → Ctx → 𝒰 where
  here  : ∀ {Γ A}   → A ∈i (Γ , A)
  there : ∀ {Γ A B} → A ∈i Γ → A ∈i (Γ , B)

data _⊢_ : Ctx → Formula → 𝒰 where
  ax   : ∀ {Γ A}     → A ∈i Γ
                     → Γ ⊢ A
  ⇒I   : ∀ {Γ A B}   → (Γ , A) ⊢ B
                     → Γ ⊢ (A ⇒i B)
  ⇒E   : ∀ {Γ A B}   → Γ ⊢ (A ⇒i B) → Γ ⊢ A
                     → Γ ⊢ B
  ∧I   : ∀ {Γ A B}   → Γ ⊢ A → Γ ⊢ B
                     → Γ ⊢ (A ∧i B)
  ∧E₁  : ∀ {Γ A B}   → Γ ⊢ (A ∧i B)
                     → Γ ⊢ A
  ∧E₂  : ∀ {Γ A B}   → Γ ⊢ (A ∧i B)
                     → Γ ⊢ B
  ∨I₁  : ∀ {Γ A B}   → Γ ⊢ A
                     → Γ ⊢ (A ∨i B)
  ∨I₂  : ∀ {Γ A B}   → Γ ⊢ B
                     → Γ ⊢ (A ∨i B)
  ∨E   : ∀ {Γ A B C} → Γ ⊢ (A ∨i B) → (Γ , A) ⊢ C → (Γ , B) ⊢ C
                     → Γ ⊢ C
  ⊥E   : ∀ {Γ A}     → Γ ⊢ ⊥i
                     → Γ ⊢ A
                     
-- ────────────────────────────────────
-- 3. KRIPKE MODEL AND FORCING RELATION
-- ────────────────────────────────────

record KripkeModel : 𝒰₁ where
  field
    World  : 𝒰
    _≤_    : World → World → 𝒰
    refl≤  : ∀ {w}     → w ≤ w
    trans≤ : ∀ {u v w} → u ≤ v → v ≤ w → u ≤ w
    val    : World → Var → 𝒰
    mono   : ∀ {w v p} → w ≤ v → val w p → val v p

module Forcing (M : KripkeModel) where
  open KripkeModel M

  _⊩_ : World → Formula → 𝒰
  w ⊩ atom p   = val w p
  w ⊩ ⊥i       = ⊥
  w ⊩ (A ⇒i B) = ∀ {v} → w ≤ v → v ⊩ A → v ⊩ B
  w ⊩ (A ∧i B) = (w ⊩ A) × (w ⊩ B)
  w ⊩ (A ∨i B) = (w ⊩ A) ⊎ (w ⊩ B)

  ⊩⇒ : ∀ {A B w} → w ⊩ (A ⇒i B) → w ⊩ A → w ⊩ B
  ⊩⇒ hab = hab refl≤

  -- Monotonicity of forcing
  mono⊩ : ∀ {w v} (A : Formula) → w ≤ v → w ⊩ A → v ⊩ A
  mono⊩ (atom p) w≤v  wA      = mono w≤v wA
  mono⊩ ⊥i       w≤v  ()
  mono⊩ (A ⇒i B) w≤v  wAB v≤u = wAB (trans≤ w≤v v≤u)
  mono⊩ (A ∧i B) w≤v (a , b)  = mono⊩ A w≤v a , mono⊩ B w≤v b
  mono⊩ (A ∨i B) w≤v (inl a)  = inl (mono⊩ A w≤v a)
  mono⊩ (A ∨i B) w≤v (inr b)  = inr (mono⊩ B w≤v b)

  -- Semantic environment
  Env : World → Ctx → 𝒰
  Env w ∅       = ⊤
  Env w (Γ , A) = Env w Γ × w ⊩ A

  -- Lookup in environment
  lookup : ∀ {Γ A w} → A ∈i Γ → Env w Γ → w ⊩ A
  lookup  here     (_ , a) = a
  lookup (there x) (γ , _) = lookup x γ

  -- Environments are monotone
  monoEnv : ∀ {w v} (Γ : Ctx) → w ≤ v → Env w Γ → Env v Γ
  monoEnv ∅       _   _       = tt
  monoEnv (Γ , A) w≤v (γ , a) = monoEnv Γ w≤v γ , mono⊩ A w≤v a

-- ────────────
-- 4. SOUNDNESS
-- ────────────

  -- The main theorem: every derivation is semantically valid
  soundness : ∀ {Γ A} → Γ ⊢ A
            → ∀ {w} → Env w Γ → w ⊩ A
  soundness     (ax x)             γ = lookup x γ
  soundness {Γ} (⇒I d)             γ = λ w≤v a → soundness d (monoEnv Γ w≤v γ , a)
  soundness     (⇒E {A} {B} d₁ d₂) γ = ⊩⇒ {A = A} {B = B} (soundness d₁ γ) (soundness d₂ γ)
  soundness     (∧I d₁ d₂)         γ = soundness d₁ γ , soundness d₂ γ
  soundness     (∧E₁ d)            γ = soundness d γ .fst
  soundness     (∧E₂ d)            γ = soundness d γ .snd
  soundness     (∨I₁ d)            γ = inl (soundness d γ)
  soundness     (∨I₂ d)            γ = inr (soundness d γ)
  soundness     (∨E d d₁ d₂)       γ with soundness d γ
  ... | inl a                        = soundness d₁ (γ , a)
  ... | inr b                        = soundness d₂ (γ , b)
  soundness     (⊥E d)             γ = absurd (soundness d γ)

  -- If a formula is provable from the empty context, it is forced everywhere
  soundness∅ : ∀ {A} → ∅ ⊢ A → ∀ {w} → w ⊩ A
  soundness∅ d = soundness d tt

-- ───────────────────────────────────
-- 4. COUNTERMODELS AND UNDERIVABILITY
-- ───────────────────────────────────

A B : Formula
A = atom 0
B = atom 1

-- Two worlds: bottom (false) and top (true)
-- Ordering: false ≤ false, false ≤ true, true ≤ true

data TwoWorld : 𝒰 where
  bottom top : TwoWorld

data _≼_ : TwoWorld → TwoWorld → 𝒰 where
  b≼  : ∀ {w} → bottom ≼ w
  t≼t :         top    ≼ top

-- Atomic valuation:
-- A and B are forced only at top
twoVal : TwoWorld → Var → 𝒰
twoVal top    _ = ⊤
twoVal bottom _ = ⊥

-- Monotonicity: bottom forces nothing, so vacuous; top forces everything already at top
twoMono : ∀ {w v p} → w ≼ v → twoVal w p → twoVal v p
twoMono b≼  hp = absurd hp
twoMono t≼t hp = hp

counterModel : KripkeModel
counterModel .KripkeModel.World              = TwoWorld
counterModel .KripkeModel._≤_                = _≼_
counterModel .KripkeModel.refl≤ {w = bottom} = b≼
counterModel .KripkeModel.refl≤ {w = top}    = t≼t
counterModel .KripkeModel.trans≤ b≼  q       = b≼
counterModel .KripkeModel.trans≤ t≼t t≼t     = t≼t
counterModel .KripkeModel.val                = twoVal
counterModel .KripkeModel.mono {p}           = twoMono {p = p}

module _ where
  open Forcing counterModel

  no-lem : ¬ (∅ ⊢ (A ∨i (¬i A)))
  no-lem d =
    [ id , (λ f → f {v = top} b≼ tt) ]ᵤ (soundness∅ d {w = bottom})

  -- Step 1: bottom forces A ⇒ B
  bottom⊩A⇒B : bottom ⊩ (A ⇒i B)
  bottom⊩A⇒B {v = top} b≼v vA = tt

  -- Step 2: bottom does not force ¬ A ∨ B
  bottom⊮¬A∨B : ¬ (bottom ⊩ ((¬i A) ∨i B))
  bottom⊮¬A∨B (inl ¬A) = ¬A b≼ tt   -- ¬A means A→⊥ for all extensions;
                                  -- but top ⊩ A, so we get ⊥
  bottom⊮¬A∨B (inr B)  = B          -- bottom ⊩ B means twoVal bottom true = ⊥

  -- Step 3
  not-provable : ¬ (∅ ⊢ ((A ⇒i B) ⇒i ((¬i A) ∨i B)))
  not-provable d = bottom⊮¬A∨B (soundness∅ d b≼ bottom⊩A⇒B)

data ThreeWorld : 𝒰 where
  bottom left right : ThreeWorld

data _≼3_ : ThreeWorld → ThreeWorld → 𝒰 where
  b≼3  : ∀ {w} → bottom ≼3 w
  l≼3l :         left   ≼3 left
  r≼3r :         right  ≼3 right

refl≼3 : ∀ {w} → w ≼3 w
refl≼3 {w = bottom} = b≼3
refl≼3 {w = left}   = l≼3l
refl≼3 {w = right}  = r≼3r

trans≼3 : ∀ {u v w} → u ≼3 v → v ≼3 w → u ≼3 w
trans≼3 b≼3  q = b≼3
trans≼3 l≼3l q = q
trans≼3 r≼3r q = q

-- Atomic valuation:
--   A (false) forced only at left
--   B (true)  forced only at right
threeVal : ThreeWorld → Var → 𝒰
threeVal left  0 = ⊤
threeVal right 1 = ⊤
threeVal _     _ = ⊥

threeMono : ∀ {w v p} → w ≼3 v → threeVal w p → threeVal v p
threeMono b≼3  hp = absurd hp
threeMono l≼3l hp = hp
threeMono r≼3r hp = hp

counterModel3 : KripkeModel
counterModel3 .KripkeModel.World  = ThreeWorld
counterModel3 .KripkeModel._≤_    = _≼3_
counterModel3 .KripkeModel.refl≤  = refl≼3
counterModel3 .KripkeModel.trans≤ = trans≼3
counterModel3 .KripkeModel.val    = threeVal
counterModel3 .KripkeModel.mono   = threeMono

module _ where
  open Forcing counterModel3

  bottom⊩¬[A∧B] : bottom ⊩ (¬i (A ∧i B))
  bottom⊩¬[A∧B] {v = bottom} b≼3 (va , vb) = va
  bottom⊩¬[A∧B] {v = left}   b≼3 (va , vb) = vb
  bottom⊩¬[A∧B] {v = right}  b≼3 (va , vb) = va

  bottom⊮¬A∨¬B : ¬ (bottom ⊩ ((¬i A) ∨i (¬i B)))
  bottom⊮¬A∨¬B (inl na) = na {v = left} b≼3 tt
  bottom⊮¬A∨¬B (inr nb) = nb {v = right} b≼3 tt

  not-provable3 : ¬ (∅ ⊢ ((¬i (A ∧i B)) ⇒i ((¬i A) ∨i (¬i B))))
  not-provable3 d = bottom⊮¬A∨¬B (soundness∅ d b≼3 bottom⊩¬[A∧B])