Mjau

mambo.agda

@@ -26,14 +26,21 @@ data _∪_ (A B : Type) : Type where
   inl : A → A ∪ B
   inr : B → A ∪ B
 
+orₑ : {A B C : Type} → A ∪ B → (A → C) → (B → C) → C
+orₑ (inl x) f g = f x
+orₑ (inr x) f g = g x
+
+absurd : {A : Type} → Bottom → A
+absurd ()
+
 data Formula : Type where
   ⊥ : Formula
   atom : Nat → Formula
-  ∼_ : Formula → Formula
-  □_ : Formula → Formula
-  _∧_ : Formula → Formula → Formula
-  _∨_ : Formula → Formula → Formula
-  _⇒_ : Formula → Formula → Formula
+  ∼_ : (p : Formula) → Formula
+  □_ : (p : Formula) → Formula
+  _∧_ : (p q : Formula) → Formula
+  _∨_ : (p q : Formula) → Formula
+  _⇒_ : (p q : Formula) → Formula
 
 infixr 4 _⇒_
 infix 19 _∧_
@@ -100,16 +107,19 @@ Context : Type
 Context = List Formula
 
 variable
-  Γ Δ : Context
+  Γ Δ Γ' Δ' : Context
 
 infixl 10 _,_
 pattern _,_ Γ X = X ∷ Γ
 
-infix 10 _++_
+infix 9 _++_
 _++_ : {A : Type} → List A → List A → List A
 [] ++ ys = ys
 (xs , x) ++ ys = xs ++ (x ∷ ys)
 
+_⊆_ : {A : Type} → (Γ Γ' : List A) → Type
+_⊆_ {A} Γ Γ' = ∀ {X} → X ∈ Γ → X ∈ Γ'
+
 infixr 2 _/_⊢_
 data _/_⊢_ (Δ Γ : Context) : Formula → Type where
   var : X ∈ Γ → Δ / Γ ⊢ X
@@ -147,10 +157,5 @@ ExampleSyn3 : [] / [] ⊢ (□ A ∧ □ B) ⇒ □(A ∧ B)
 ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B)) []))) (□ₑ (∧ₑ₂ (var (zero ((□ A) ∧ (□ B)) []))) (□ᵢ (∧ᵢ (var (succ A ([] , A) (zero A []))) (var (zero B ([] , A)))))))
 
 ExampleSyn4 : [] / [] ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
-ExampleSyn4 {A} {B} = {!!}
-
-Soundness : {W : Type} → (p : Formula) → [] / [] ⊢ p → (∀ (m : M W) (x : W) → m , x ⊩ p)
-Soundness p x m w = {!!}
-
-Completeness : {W : Type} → (p : Formula) → (∀ (m : M W) (x : W) → m , x ⊩ p) → [] / [] ⊢ p
-Completeness p x = {!!}
+ExampleSyn4 {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ B)) ([] , (□ (A ⇒ B)) , (◇ A)))) (□ₑ (var (succ (□ (A ⇒ B)) ([] , (□ (A ⇒ B)) , (◇ A)) (succ (□ (A ⇒ B)) ([] , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) [])))) (¬ₑ (var (succ (∼ (□ (∼ A))) ([] , (□ (A ⇒ B)) , (◇ A))
+                                                                                                                                                                                                                      (zero (∼ (□ (∼ A))) ([] , (□ (A ⇒ B)))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ ( ∼ B) ([] , (∼ B) , (A ⇒ B)) (succ (∼ B) ([] , (∼ B)) (zero (∼ B) [])))) (mp (var (succ (A ⇒ B) ([] , (∼ B) , (A ⇒ B)) (zero (A ⇒ B) ([] , (∼ B))))) (var (zero A ([] , (∼ B) , (A ⇒ B)))))))))))))