diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index e17cb37..d251664 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -39,6 +39,7 @@ module PropositionalKripke (PV : Set) where w ⊩ᶠ Var x = w ⊩ x w ⊩ᶠ (fp ⇒ fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq w ⊩ᶠ (fp ∧∧ fq) = w ⊩ᶠ fp ∧ w ⊩ᶠ fq + w ⊩ᶠ ⊤⊤ = ⊤ _⊩ᶜ_ : Worlds → Con → Prop w ⊩ᶜ [] = ⊤ @@ -49,7 +50,8 @@ module PropositionalKripke (PV : Set) where mon⊩ᶠ {F = Var x} ww' wF = mon⊩ ww' wF mon⊩ᶠ {F = F ⇒ G} ww' wF w'w'' w''F = wF (tran≤ ww' w'w'') w''F mon⊩ᶠ {F = F ∧∧ G} ww' ⟨ wF , wG ⟩ = ⟨ mon⊩ᶠ {F = F} ww' wF , mon⊩ᶠ {F = G} ww' wG ⟩ - + mon⊩ᶠ {F = ⊤⊤} ww' wF = tt + mon⊩ᶜ : w ≤ w' → w ⊩ᶜ Γ → w' ⊩ᶜ Γ mon⊩ᶜ {Γ = []} ww' wΓ = wΓ mon⊩ᶜ {Γ = F ∷ Γ} ww' wΓ = ⟨ mon⊩ᶠ {F = F} ww' (proj₁ wΓ) , mon⊩ᶜ ww' (proj₂ wΓ) ⟩ @@ -67,3 +69,4 @@ module PropositionalKripke (PV : Set) where ⟦ andi p₁ p₂ ⟧ wΓ = ⟨ (⟦ p₁ ⟧ wΓ) , (⟦ p₂ ⟧ wΓ) ⟩ ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ + ⟦ true ⟧ wΓ = tt diff --git a/PropositionalKripkeGeneral.agda b/PropositionalKripkeGeneral.agda index d13dac5..9cf4716 100644 --- a/PropositionalKripkeGeneral.agda +++ b/PropositionalKripkeGeneral.agda @@ -4,7 +4,7 @@ module PropositionalKripkeGeneral (PV : Set) where open import ListUtil open import PropUtil - open import PropositionalLogic PV using (Form; Var; _⇒_; _∧∧_; Con) + open import PropositionalLogic PV using (Form; Var; _⇒_; _∧∧_; ⊤⊤; Con) open import PropositionalKripke PV using (Kripke) @@ -29,6 +29,7 @@ module PropositionalKripkeGeneral (PV : Set) where neu⁰ : {Γ : Con} → {x : PV} → Γ ⊢⁰ Var x → Γ ⊢* Var x lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G) andi : {Γ : Con} → {F G : Form} → Γ ⊢* F → Γ ⊢* G → Γ ⊢* (F ∧∧ G) + true : {Γ : Con} → Γ ⊢* ⊤⊤ record NormalizationFrame : Set₁ where field @@ -62,11 +63,12 @@ module PropositionalKripkeGeneral (PV : Set) where u {Var x} h = h u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) u {F ∧∧ G} h = ⟨ (u {F} (ande₁ h)) , (u {G} (ande₂ h)) ⟩ + u {⊤⊤} h = tt q {Var x} h = neu⁰ h q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero))) q {F ∧∧ G} ⟨ hF , hG ⟩ = andi (q {F} hF) (q {G} hG) - + q {⊤⊤} h = true @@ -87,7 +89,8 @@ module PropositionalKripkeGeneral (PV : Set) where ande₂ = ande₂ ; neu⁰ = neu⁰ ; lam = lam; - andi = andi + andi = andi; + true = true } BiggestNN : NormalAndNeutral @@ -101,7 +104,8 @@ module PropositionalKripkeGeneral (PV : Set) where ande₂ = ande₂ ; neu⁰ = λ x → x ; lam = lam ; - andi = andi + andi = andi ; + true = true } PO⊢⁺ = [ order {Con} _⊢⁺_ refl⊢⁺ tran⊢⁺ ]ᵒᵖ diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda index 2be69cf..4972b8d 100644 --- a/PropositionalLogic.agda +++ b/PropositionalLogic.agda @@ -9,6 +9,7 @@ module PropositionalLogic (PV : Set) where Var : PV → Form _⇒_ : Form → Form → Form _∧∧_ : Form → Form → Form + ⊤⊤ : Form infixr 10 _∧∧_ infixr 8 _⇒_ @@ -41,6 +42,7 @@ module PropositionalLogic (PV : Set) where andi : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧∧ B ande₁ : Γ ⊢ A ∧∧ B → Γ ⊢ A ande₂ : Γ ⊢ A ∧∧ B → Γ ⊢ B + true : Γ ⊢ ⊤⊤ infix 5 _⊢_ @@ -57,6 +59,7 @@ module PropositionalLogic (PV : Set) where addhyp⊢ s (andi h₁ h₂) = andi (addhyp⊢ s h₁) (addhyp⊢ s h₂) addhyp⊢ s (ande₁ h) = ande₁ (addhyp⊢ s h) addhyp⊢ s (ande₂ h) = ande₂ (addhyp⊢ s h) + addhyp⊢ s (true) = true -- Extension of ⊢ to contexts _⊢⁺_ : Con → Con → Prop @@ -93,6 +96,7 @@ module PropositionalLogic (PV : Set) where halftran⊢⁺ h⁺ (andi hf hg) = andi (halftran⊢⁺ h⁺ hf) (halftran⊢⁺ h⁺ hg) halftran⊢⁺ h⁺ (ande₁ hfg) = ande₁ (halftran⊢⁺ h⁺ hfg) halftran⊢⁺ h⁺ (ande₂ hfg) = ande₂ (halftran⊢⁺ h⁺ hfg) + halftran⊢⁺ h⁺ (true) = true -- The relation is transitive tran⊢⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁺ Γ' → Γ' ⊢⁺ Γ'' → Γ ⊢⁺ Γ'' @@ -115,6 +119,7 @@ module PropositionalLogic (PV : Set) where neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B) andi : Γ ⊢* A → Γ ⊢* B → Γ ⊢* (A ∧∧ B) + true : Γ ⊢* ⊤⊤ infix 5 _⊢⁰_ infix 5 _⊢*_ @@ -128,6 +133,7 @@ module PropositionalLogic (PV : Set) where ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x ⊢*→⊢ (lam h) = lam (⊢*→⊢ h) ⊢*→⊢ (andi h₁ h₂) = andi (⊢*→⊢ h₁) (⊢*→⊢ h₂) + ⊢*→⊢ true = true -- We can add hypotheses to a proof addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A @@ -139,6 +145,7 @@ module PropositionalLogic (PV : Set) where addhyp⊢* s (neu⁰ x) = neu⁰ (addhyp⊢⁰ s x) addhyp⊢* s (lam h) = lam (addhyp⊢* (both∈* s) h) addhyp⊢* s (andi h₁ h₂) = andi (addhyp⊢* s h₁) (addhyp⊢* s h₂) + addhyp⊢* s true = true -- Extension of ⊢⁰ to contexts -- i.e. there is a neutral proof for any element @@ -173,6 +180,7 @@ module PropositionalLogic (PV : Set) where halftran⊢⁰⁺* h⁺ (neu⁰ x) = neu⁰ (halftran⊢⁰⁺⁰ h⁺ x) halftran⊢⁰⁺* h⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero zero∈ , addhyp⊢⁰⁺ (right∈* refl∈*) h⁺ ⟩ h) halftran⊢⁰⁺* h⁺ (andi h₁ h₂) = andi (halftran⊢⁰⁺* h⁺ h₁) (halftran⊢⁰⁺* h⁺ h₂) + halftran⊢⁰⁺* h⁺ true = true halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺ halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero (next∈ h)) = halftran⊢⁰⁺⁰ (proj₂ h⁺) (zero h) halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h') @@ -195,6 +203,7 @@ module PropositionalLogic (PV : Set) where ⟦ Var x ⟧ᶠ ρ = ρ x ⟦ A ⇒ B ⟧ᶠ ρ = (⟦ A ⟧ᶠ ρ) → (⟦ B ⟧ᶠ ρ) ⟦ A ∧∧ B ⟧ᶠ ρ = (⟦ A ⟧ᶠ ρ) ∧ (⟦ B ⟧ᶠ ρ) + ⟦ ⊤⊤ ⟧ᶠ ρ = ⊤ ⟦_⟧ᶜ : Con → Env → Prop ⟦ [] ⟧ᶜ ρ = ⊤ @@ -208,6 +217,7 @@ module PropositionalLogic (PV : Set) where ⟦ andi hf hg ⟧ᵈ = λ p → ⟨ ⟦ hf ⟧ᵈ p , ⟦ hg ⟧ᵈ p ⟩ ⟦ ande₁ hfg ⟧ᵈ = λ p → proj₁ (⟦ hfg ⟧ᵈ p) ⟦ ande₂ hfg ⟧ᵈ = λ p → proj₂ (⟦ hfg ⟧ᵈ p) + ⟦ true ⟧ᵈ ρ = tt @@ -222,6 +232,7 @@ module PropositionalLogic (PV : Set) where ANDe₁ : ⊢sk ((A ∧∧ B) ⇒ A) ANDe₂ : ⊢sk ((A ∧∧ B) ⇒ B) app : ⊢sk (A ⇒ B) → ⊢sk A → ⊢sk B + true : ⊢sk ⊤⊤ data _⊢skC_ : Con → Form → Prop where zero : A ∈ Γ → Γ ⊢skC A @@ -231,6 +242,7 @@ module PropositionalLogic (PV : Set) where ANDe₁ : Γ ⊢skC ((A ∧∧ B) ⇒ A) ANDe₂ : Γ ⊢skC ((A ∧∧ B) ⇒ B) app : Γ ⊢skC (A ⇒ B) → Γ ⊢skC A → Γ ⊢skC B + true : Γ ⊢skC ⊤⊤ -- combinatory gives the same proofs as classic ⊢⇔⊢sk : ([] ⊢ A) ⇔ ⊢sk A @@ -242,6 +254,7 @@ module PropositionalLogic (PV : Set) where ⊢sk→⊢ ANDe₁ = lam (ande₁ (zero zero∈)) ⊢sk→⊢ ANDe₂ = lam (ande₂ (zero zero∈)) ⊢sk→⊢ (app x x₁) = app (⊢sk→⊢ x) (⊢sk→⊢ x₁) + ⊢sk→⊢ true = true skC→sk : [] ⊢skC A → ⊢sk A skC→sk SS = SS @@ -250,6 +263,7 @@ module PropositionalLogic (PV : Set) where skC→sk ANDe₁ = ANDe₁ skC→sk ANDe₂ = ANDe₂ skC→sk (app d e) = app (skC→sk d) (skC→sk e) + skC→sk true = true lam-sk : (A ∷ Γ) ⊢skC B → Γ ⊢skC (A ⇒ B) @@ -263,6 +277,7 @@ module PropositionalLogic (PV : Set) where lam-sk ANDe₁ = app KK (app (app SS (app KK ANDe₁)) lam-sk-zero) lam-sk ANDe₂ = app KK (app (app SS (app KK ANDe₂)) lam-sk-zero) lam-sk (app x₁ x₂) = app (app SS (lam-sk x₁)) (lam-sk x₂) + lam-sk true = app KK true ⊢→⊢skC : Γ ⊢ A → Γ ⊢skC A @@ -272,5 +287,6 @@ module PropositionalLogic (PV : Set) where ⊢→⊢skC (andi x y) = app (app ANDi (⊢→⊢skC x)) (⊢→⊢skC y) ⊢→⊢skC (ande₁ x) = app ANDe₁ (⊢→⊢skC x) ⊢→⊢skC (ande₂ x) = app ANDe₂ (⊢→⊢skC x) + ⊢→⊢skC (true) = true ⊢⇔⊢sk = ⟨ (λ x → skC→sk (⊢→⊢skC x)) , ⊢sk→⊢ ⟩