diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index 980d3a7..a595dc6 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -64,9 +64,9 @@ module PropositionalKripke (PV : Set) where ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ) ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩ ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ) - ⟦ andi p₁ p₂ ⟧ = {!!} - ⟦ ande₁ p ⟧ = {!!} - ⟦ ande₂ p ⟧ = {!!} + ⟦ andi p₁ p₂ ⟧ wΓ = ⟨ (⟦ p₁ ⟧ wΓ) , (⟦ p₂ ⟧ wΓ) ⟩ + ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ + ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ @@ -91,10 +91,10 @@ module PropositionalKripke (PV : Set) where ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F ⊢→⊩ᶠ {Var x} h = h ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF)) - ⊢→⊩ᶠ {F ∧∧ G} h = {!!} + ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩ ⊩ᶠ→⊢ {Var x} h = h ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) - ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = {!!} + ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG) -- Finally, we can deduce completeness of the Kripke model completeness : {F : Form} → [] ⊫ F → [] ⊢ F @@ -124,10 +124,10 @@ module PropositionalKripke (PV : Set) where ⊢→⊩ᶠ {Var x} h = h ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF)) - ⊢→⊩ᶠ {F ∧∧ G} h = ? + ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩ ⊩ᶠ→⊢ {Var x} h = neu⁰ h ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) - ⊩ᶠ→⊢ {F ∧∧ G} h = {!!} + ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG) module OtherProofs where diff --git a/PropositionalKripkeGeneral.agda b/PropositionalKripkeGeneral.agda index 3796b1e..d13dac5 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) @@ -24,8 +24,11 @@ module PropositionalKripkeGeneral (PV : Set) where _⊢*_ : Con → Form → Prop zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G + ande₁ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ F + ande₂ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ G 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) record NormalizationFrame : Set₁ where field @@ -58,8 +61,11 @@ 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)) ⟩ + 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) @@ -77,8 +83,11 @@ module PropositionalKripkeGeneral (PV : Set) where _⊢*_ = _⊢*_ ; zero = zero zero∈ ; app = app ; + ande₁ = ande₁; + ande₂ = ande₂ ; neu⁰ = neu⁰ ; - lam = lam + lam = lam; + andi = andi } BiggestNN : NormalAndNeutral @@ -88,8 +97,11 @@ module PropositionalKripkeGeneral (PV : Set) where _⊢*_ = _⊢_ ; zero = zero zero∈ ; app = app ; + ande₁ = ande₁ ; + ande₂ = ande₂ ; neu⁰ = λ x → x ; - lam = lam + lam = lam ; + andi = andi } PO⊢⁺ = [ order {Con} _⊢⁺_ refl⊢⁺ tran⊢⁺ ]ᵒᵖ diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda index 3dbff9c..2be69cf 100644 --- a/PropositionalLogic.agda +++ b/PropositionalLogic.agda @@ -109,9 +109,12 @@ module PropositionalLogic (PV : Set) where data _⊢⁰_ : Con → Form → Prop where zero : A ∈ Γ → Γ ⊢⁰ A app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B + ande₁ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ A + ande₂ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ B data _⊢*_ : Con → Form → Prop where neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B) + andi : Γ ⊢* A → Γ ⊢* B → Γ ⊢* (A ∧∧ B) infix 5 _⊢⁰_ infix 5 _⊢*_ @@ -120,16 +123,22 @@ module PropositionalLogic (PV : Set) where ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F ⊢⁰→⊢ (zero h) = zero h ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x) + ⊢⁰→⊢ (ande₁ h) = ande₁ (⊢⁰→⊢ h) + ⊢⁰→⊢ (ande₂ h) = ande₂ (⊢⁰→⊢ h) ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x ⊢*→⊢ (lam h) = lam (⊢*→⊢ h) + ⊢*→⊢ (andi h₁ h₂) = andi (⊢*→⊢ h₁) (⊢*→⊢ h₂) -- We can add hypotheses to a proof addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A addhyp⊢* : Γ ∈* Γ' → Γ ⊢* A → Γ' ⊢* A addhyp⊢⁰ s (zero x) = zero (mon∈∈* x s) addhyp⊢⁰ s (app h h₁) = app (addhyp⊢⁰ s h) (addhyp⊢* s h₁) + addhyp⊢⁰ s (ande₁ h) = ande₁ (addhyp⊢⁰ s h) + addhyp⊢⁰ s (ande₂ h) = ande₂ (addhyp⊢⁰ s h) 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₂) -- Extension of ⊢⁰ to contexts -- i.e. there is a neutral proof for any element @@ -163,9 +172,12 @@ module PropositionalLogic (PV : Set) where halftran⊢⁰⁺⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F 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⊢⁰⁺⁰ {Γ' = 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') + halftran⊢⁰⁺⁰ h⁺ (ande₁ h) = ande₁ (halftran⊢⁰⁺⁰ h⁺ h) + halftran⊢⁰⁺⁰ h⁺ (ande₂ h) = ande₂ (halftran⊢⁰⁺⁰ h⁺ h) -- The relation is transitive tran⊢⁰⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰⁺ Γ'' → Γ ⊢⁰⁺ Γ''