Todos

README.md

@@ -1,10 +1,2 @@
-# Mambo
+# mambo
 
-This was my weekend turned a bit more project from Christmas, really fun thinking thingy, would be interesting to show the relation to other similar systems as LTL and CTL.
-
-## Resources used
-- https://vcvpaiva.github.io/includes/pubs/2011-Basic_Constructive_Modality.pdf
-- https://arxiv.org/html/2408.16428v1
-- https://www.sciencedirect.com/science/article/pii/S157106611000037X
-- https://builds.openlogicproject.org/courses/boxes-and-diamonds/bd-screen.pdf
-- https://www.cambridge.org/us/universitypress/subjects/computer-science/programming-languages-and-applied-logic/logic-computer-science-modelling-and-reasoning-about-systems-2nd-edition?format=PB&isbn=9780521543101

mambo.agda

@@ -1,14 +1,10 @@
 {-# OPTIONS --no-import-sorts #-}
 open import Agda.Primitive renaming (Set to Type)
 open import Agda.Builtin.Nat
+open import Agda.Builtin.List
 
 data Bottom : Type where
 
-infixl 10 _,_
-data Stack (A : Type) : Type where
-  ∙ : Stack A
-  _,_ : Stack A → A → Stack A
-
 ¬ : Type → Type
 ¬ A = A → Bottom
 
@@ -30,21 +26,14 @@ 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
-  ∼_ : (p : Formula) → Formula
-  □_ : (p : Formula) → Formula
-  _∧_ : (p q : Formula) → Formula
-  _∨_ : (p q : Formula) → Formula
-  _⇒_ : (p q : Formula) → Formula
+  ∼_ : Formula → Formula
+  □_ : Formula → Formula
+  _∧_ : Formula → Formula → Formula
+  _∨_ : Formula → Formula → Formula
+  _⇒_ : Formula → Formula → Formula
 
 infixr 4 _⇒_
 infix 19 _∧_
@@ -62,14 +51,14 @@ X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)
 ◇ p = ∼ (□ (∼ p))
 
 infix 9 _∈_
-data _∈_ {A : Type} : A → Stack A → Type where
-  zero : (x : A) (xs : Stack A) → x ∈ (xs , x)
-  succ : {y : A} (x : A) (xs : Stack A) → (x ∈ xs) → (x ∈ (xs , y))
+data _∈_ {A : Type} : A → List A → Type where
+  zero : (x : A) (xs : List A) → x ∈ (x ∷ xs)
+  succ : {y : A} (x : A) (xs : List A) → (x ∈ xs) → (x ∈ (y ∷ xs))
 
 record M (W : Type) : Type₁ where
   field
     R : Rel W W
-    L : W → Stack Nat
+    L : W → List Nat
 
 infix 2 _,_⊩_
 _,_⊩_ : {W : Type} (Model : M W) (x : W) (p : Formula) → Type 
@@ -90,38 +79,36 @@ data R : Nat → Nat → Type where
 ExampleModel : M Nat
 ExampleModel .M.R = R
 
-ExampleModel .M.L 0 = ∙ , 0
-ExampleModel .M.L 1 = ∙ , 2 , 1
-ExampleModel .M.L 2 = ∙ , 2 , 0
-ExampleModel .M.L _ = ∙
+ExampleModel .M.L 0 = 0 ∷ []
+ExampleModel .M.L 1 = 1 ∷ 2 ∷ []
+ExampleModel .M.L 2 = 0 ∷ 2 ∷ []
+ExampleModel .M.L _ = []
 
 
 KSem : ExampleModel , 0 ⊩ □ (atom 1 ⇒ atom 2) ⇒ (□ atom 1 ⇒ □ atom 2)
-KSem x x₁ y zeroone = succ 2 (∙ , 2) (zero 2 ∙)
-KSem x x₁ y zerotwo = succ 2 (∙ , 2) (zero 2 ∙)
+KSem x x₁ y zeroone = succ 2 (2 ∷ []) (zero 2 [])
+KSem x x₁ y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
 
 ExampleSem : ExampleModel , 0 ⊩ □ (atom 2)
-ExampleSem y zeroone = succ 2 (∙ , 2) (zero 2 ∙)
-ExampleSem y zerotwo = succ 2 (∙ , 2) (zero 2 ∙)
+ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 [])
+ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
 
 Example2Sem : ExampleModel , 0 ⊩ ◇ (atom 1)
-Example2Sem = pair 1 (λ _ → zero 1 (∙ , 2))
+Example2Sem = pair 1 (λ _ → zero 1 (2 ∷ []))
 
 Context : Type
-Context = Stack Formula
+Context = List Formula
 
 variable
-  Γ Δ Γ' Δ' : Context
+  Γ Δ : Context
 
+infixl 10 _,_
+pattern _,_ Γ X = X ∷ Γ
 
-infix 9 _++_
-_++_ : {A : Type} → Stack A → Stack A → Stack A
-xs ++ ∙ = xs
-xs ++ ys , y = (xs ++ ys) , y
-
-infix 8 _⊆_
-_⊆_ : {A : Type} → (Γ Γ' : Stack A) → Type
-_⊆_ {A} Γ Γ' = ∀ {X} → X ∈ Γ → X ∈ Γ'
+infix 10 _++_
+_++_ : {A : Type} → List A → List A → List A
+[] ++ ys = ys
+(xs , x) ++ ys = xs ++ (x ∷ ys)
 
 infixr 2 _/_⊢_
 data _/_⊢_ (Δ Γ : Context) : Formula → Type where
@@ -136,174 +123,35 @@ data _/_⊢_ (Δ Γ : Context) : Formula → Type where
   ⇒ᵢ : Δ / Γ , X ⊢ Y → Δ / Γ ⊢ X ⇒ Y
   ¬ᵢ : Δ / Γ , X ⊢ ⊥ → Δ / Γ ⊢ ∼ X
   ¬ₑ : Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ X → Δ / Γ ⊢ ⊥
-  ⊥ₑ : Δ / Γ ⊢ ⊥ → Δ / Γ ⊢ X
-  □ᵢ : ∙ / Δ ⊢ X → Δ / Γ ⊢ □ X
+  □ᵢ : [] / Δ ⊢ X → Δ / Γ ⊢ □ X
   □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y
   -- TODO: Maybe make it KT45
 
-inSwap : {A : Type} {X Y Z : A} (Γ Γ' : Stack A) → Z ∈ (Γ , X , Y ++ Γ') → Z ∈ (Γ , Y , X ++ Γ')
-inSwap Γ ∙ (zero x xs) = succ x (Γ , x) (zero x Γ)
-inSwap Γ ∙ (succ x xs (zero x₁ xs₁)) = zero x (Γ , _)
-inSwap Γ ∙ (succ x xs (succ x₁ xs₁ x₂)) = succ x (Γ , _) (succ x Γ x₂)
-inSwap Γ (Γ' , x₁) (zero x xs) = zero x₁ (Γ , _ , _ ++ Γ')
-inSwap Γ (Γ' , x₁) (succ x xs x₂) = succ x (Γ , _ , _ ++ Γ') (inSwap Γ Γ' x₂)
-
-exchange : (Γ' : Context) → Δ / (Γ , A , B) ++ Γ'  ⊢ C → Δ / (Γ , B , A) ++ Γ' ⊢ C
-exchange Γ' (var x) = var (inSwap _ Γ' x)
-exchange Γ' (mp x x₁) = mp (exchange Γ' x) (exchange Γ' x₁)
-exchange Γ' (∧ᵢ x x₁) = ∧ᵢ (exchange Γ' x) (exchange Γ' x₁)
-exchange Γ' (∧ₑ₁ x) = ∧ₑ₁ (exchange Γ' x)
-exchange Γ' (∧ₑ₂ x) = ∧ₑ₂ (exchange Γ' x)
-exchange Γ' (∨ᵢ₁ x) = ∨ᵢ₁ (exchange Γ' x)
-exchange Γ' (∨ᵢ₂ x) = ∨ᵢ₂ (exchange Γ' x)
-exchange Γ' (∨ₑ x x₁ x₂) = ∨ₑ (exchange Γ' x) (exchange (Γ' , _) x₁) (exchange (Γ' , _) x₂)
-exchange Γ' (⇒ᵢ x) = ⇒ᵢ (exchange (Γ' , _) x)
-exchange Γ' (¬ᵢ x) = ¬ᵢ (exchange (Γ' , _) x)
-exchange Γ' (¬ₑ x x₁) = ¬ₑ (exchange Γ' x) (exchange Γ' x₁)
-exchange Γ' (⊥ₑ x) = ⊥ₑ (exchange Γ' x)
-exchange Γ' (□ᵢ x) = □ᵢ x
-exchange Γ' (□ₑ x x₁) = □ₑ (exchange Γ' x) (exchange Γ' x₁)
-
-exchange-modal : (Δ' : Context) →  Δ , A , B  ++ Δ' / Γ ⊢ C → Δ , B , A ++ Δ' / Γ ⊢ C
-exchange-modal Δ' (var x) = var x
-exchange-modal Δ' (mp x x₁) = mp (exchange-modal Δ' x) (exchange-modal Δ' x₁)
-exchange-modal Δ' (∧ᵢ x x₁) = ∧ᵢ (exchange-modal Δ' x) (exchange-modal Δ' x₁)
-exchange-modal Δ' (∧ₑ₁ x) = ∧ₑ₁ (exchange-modal Δ' x)
-exchange-modal Δ' (∧ₑ₂ x) = ∧ₑ₂ (exchange-modal Δ' x)
-exchange-modal Δ' (∨ᵢ₁ x) = ∨ᵢ₁ (exchange-modal Δ' x)
-exchange-modal Δ' (∨ᵢ₂ x) = ∨ᵢ₂ (exchange-modal Δ' x)
-exchange-modal Δ' (∨ₑ x x₁ x₂) = ∨ₑ (exchange-modal Δ' x) (exchange-modal Δ' x₁) (exchange-modal Δ' x₂)
-exchange-modal Δ' (⇒ᵢ x) = ⇒ᵢ (exchange-modal Δ' x)
-exchange-modal Δ' (¬ᵢ x) = ¬ᵢ (exchange-modal Δ' x)
-exchange-modal Δ' (¬ₑ x x₁) = ¬ₑ (exchange-modal Δ' x) (exchange-modal Δ' x₁)
-exchange-modal Δ' (⊥ₑ x) = ⊥ₑ (exchange-modal Δ' x)
-exchange-modal Δ' (□ᵢ x) = □ᵢ (exchange Δ' x)
-exchange-modal Δ' (□ₑ x x₁) = □ₑ (exchange-modal Δ' x) (exchange-modal (Δ' , _) x₁)
-
-inBoth : {A : Type} {Γ Γ' : Stack A} {X : A} → Γ ⊆ Γ' → (Γ , X) ⊆ (Γ' , X)
-inBoth {A} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ'
-inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂)
-
-weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A
-weak (var x) x₁ = var (x₁ x)
-weak (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
-weak (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
-weak (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
-weak (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
-weak (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
-weak (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
-weak (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
-weak (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
-weak (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
-weak (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
-weak (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
-weak (□ᵢ x) x₁ = □ᵢ x
-weak (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
-
-weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A
-weak-modal (var x) x₁ = var x
-weak-modal (mp x x₂) x₁ = mp (weak-modal x x₁) (weak-modal x₂ x₁)
-weak-modal (∧ᵢ x x₂) x₁ = ∧ᵢ (weak-modal x x₁) (weak-modal x₂ x₁)
-weak-modal (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak-modal x x₁)
-weak-modal (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak-modal x x₁)
-weak-modal (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak-modal x x₁)
-weak-modal (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak-modal x x₁)
-weak-modal (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak-modal x x₁) (weak-modal x₂ x₁) (weak-modal x₃ x₁)
-weak-modal (⇒ᵢ x) x₁ = ⇒ᵢ (weak-modal x x₁)
-weak-modal (¬ᵢ x) x₁ = ¬ᵢ (weak-modal x x₁)
-weak-modal (¬ₑ x x₂) x₁ = ¬ₑ (weak-modal x x₁) (weak-modal x₂ x₁)
-weak-modal (⊥ₑ x) x₁ = ⊥ₑ (weak-modal x x₁)
-weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁)
-weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁))
-
-cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / (Γ , A) ++ Γ' ⊢ B → Δ / Γ ++ Γ' ⊢ B
-cut ∙ x (var x₁) = mp (⇒ᵢ (var x₁)) x
-cut (Γ' , x₂) x (var (zero x₁ xs)) = var (zero x₂ (_ ++ Γ'))
-cut (Γ' , x₂) x (var (succ _ xs x₃)) = weak (cut Γ' x (var x₃)) λ {X} → succ X (_ ++ Γ')
-cut Γ' x (mp x₁ x₂) = mp (cut Γ' x x₁) (cut Γ' x x₂)
-cut Γ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut Γ' x x₁) (cut Γ' x x₂)
-cut Γ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut Γ' x x₁)
-cut Γ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut Γ' x x₁)
-cut Γ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut Γ' x x₁)
-cut Γ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut Γ' x x₁)
-cut Γ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut Γ' x x₁) (cut (Γ' , _) x x₂) (cut (Γ' , _ ) x x₃)
-cut Γ' x (⇒ᵢ x₁) = ⇒ᵢ (cut (Γ' , _) x x₁)
-cut Γ' x (¬ᵢ x₁) = ¬ᵢ (cut (Γ' , _) x x₁)
-cut Γ' x (¬ₑ x₁ x₂) = ¬ₑ (cut Γ' x x₁) (cut Γ' x x₂)
-cut Γ' x (⊥ₑ x₁) = ⊥ₑ (cut Γ' x x₁)
-cut Γ' x (□ᵢ x₁) = □ᵢ x₁
-cut Γ' x (□ₑ x₁ x₂) = □ₑ (cut Γ' x x₁) (cut Γ' (weak-modal x (λ {X = X₁} → succ X₁ _)) x₂)
-
-cut-modal : (Δ' : Context) → ∙ / Δ ⊢ A → (Δ , A) ++ Δ' / Γ ⊢ B → Δ ++ Δ' / Γ ⊢ B
-cut-modal Δ' x (var x₁) = var x₁
-cut-modal Δ' x (mp x₁ x₂) = mp (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
-cut-modal Δ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
-cut-modal Δ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut-modal Δ' x x₁)
-cut-modal Δ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut-modal Δ' x x₁)
-cut-modal Δ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut-modal Δ' x x₁)
-cut-modal Δ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut-modal Δ' x x₁)
-cut-modal Δ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂) (cut-modal Δ' x x₃)
-cut-modal Δ' x (⇒ᵢ x₁) = ⇒ᵢ (cut-modal Δ' x x₁)
-cut-modal Δ' x (¬ᵢ x₁) = ¬ᵢ (cut-modal Δ' x x₁)
-cut-modal Δ' x (¬ₑ x₁ x₂) = ¬ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
-cut-modal Δ' x (⊥ₑ x₁) = ⊥ₑ (cut-modal Δ' x x₁)
-cut-modal Δ' x (□ᵢ x₁) = □ᵢ (cut Δ' x x₁)
-cut-modal Δ' x (□ₑ x₁ x₂) = □ₑ (cut-modal Δ' x x₁) (cut-modal (Δ' , _) x x₂)
-
-KSym : ∙ / ∙ ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
-KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) (∙ , (□ (X ⇒ Y)))))
-                      (□ₑ (var (succ (□(X ⇒ Y)) (∙ , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) ∙)))
+KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
+KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))
+                      (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) [])))
                       (□ᵢ (mp
-                        (var (zero (X ⇒ Y) (∙ , X)))
-                        (var (succ X (∙ , X) (zero X ∙))))))))
+                        (var (zero (X ⇒ Y) ([] , X)))
+                        (var (succ X ([] , X) (zero X []))))))))
 
-MTSym : ∙ / ∙ ⊢ (A ⇒ B) ⇒ ∼ B ⇒ ∼ A
-MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) (∙ , (A ⇒ B) , (∼ B)) (zero (∼ B) (∙ , (A ⇒ B))))) (mp (var (succ (A ⇒ B) (∙ , (A ⇒ B) , (∼ B)) (succ (A ⇒ B) (∙ , (A ⇒ B)) (zero (A ⇒ B) ∙)))) (var (zero A (∙ , (A ⇒ B) , (∼ B))))))))
+MTSym : [] / [] ⊢ (A ⇒ B) ⇒ ∼ B ⇒ ∼ A
+MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) ([] , (A ⇒ B) , (∼ B)) (zero (∼ B) ([] , (A ⇒ B))))) (mp (var (succ (A ⇒ B) ([] , (A ⇒ B) , (∼ B)) (succ (A ⇒ B) ([] , (A ⇒ B)) (zero (A ⇒ B) [])))) (var (zero A ([] , (A ⇒ B) , (∼ B))))))))
 
-DedSym : Δ / Γ ⊢ A ⇒ B → Δ / Γ , A ⊢ B
-DedSym {Δ} {Γ} {A} {B} (var x) = mp (var (succ (A ⇒ B) Γ x)) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (mp x x₁) = mp (mp (weak x λ {X = X₁} → succ X₁ Γ) (weak x₁ (λ {X = X₁} → succ X₁ Γ))) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (∧ₑ₁ x) = mp (weak (∧ₑ₁ x) (λ {X} → succ X Γ)) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = mp (weak (∧ₑ₂ x) (λ {X = X₁} → succ X₁ Γ)) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (∨ₑ x x₁ x₂) = mp (weak (∨ₑ x x₁ x₂) λ {X = X₁} → succ X₁ Γ) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (⇒ᵢ x) = x
-DedSym {Δ} {Γ} {A} {B} (⊥ₑ x) = weak (⊥ₑ x) λ {X} → succ X Γ
-DedSym {Δ} {Γ} {A} {B} (□ₑ x x₁) = mp (weak (□ₑ x x₁) (λ {X = X₁} → succ X₁ Γ)) (var (zero A Γ))
+ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X)
+ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))
 
-DedSymInv : Δ / Γ , A ⊢ B → Δ / Γ ⊢ A ⇒ B
-DedSymInv {Δ} {Γ} {A} {B} x = ⇒ᵢ x
+ExampleSyn2 : [] / [] ⊢ □(A ∧ B) ⇒ (□ A ∧ □ B)
+ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₁ (var (zero (A ∧ B) []))))) (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₂ (var (zero (A ∧ B) []))))))
 
-ExampleSyn : ∙ / ∙ ⊢ □ X ⇒ □ (Y ⇒ X)
-ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) ∙)) (□ᵢ (⇒ᵢ (var (succ X (∙ , X) (zero X ∙))))))
+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)))))))
 
-ExampleSyn2 : ∙ / ∙ ⊢ □(A ∧ B) ⇒ (□ A ∧ □ B)
-ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) ∙)) (□ᵢ (∧ₑ₁ (var (zero (A ∧ B) ∙))))) (□ₑ (var (zero (□ (A ∧ B)) ∙)) (□ᵢ (∧ₑ₂ (var (zero (A ∧ B) ∙))))))
+ExampleSyn4 : [] / [] ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
+ExampleSyn4 {A} {B} = {!!}
 
-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)))))))
+Soundness : {W : Type} → (p : Formula) → [] / [] ⊢ p → (∀ (m : M W) (x : W) → m , x ⊩ p)
+Soundness p x m w = {!!}
 
-ExampleSyn4 : ∙ / ∙ ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
-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)))))))))))))
 
-ExampleSyn5 : ∙ / ∙ ⊢ □ ( A ⇒ B ) ⇒ ( □ A ⇒ □ B )
-ExampleSyn5 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ A) (∙ , (□ (A ⇒ B))))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙))) (□ᵢ (mp (var (zero (A ⇒ B) (∙ , A))) (var (succ A (∙ , A) (zero A ∙))))))))
-
-ExampleSyn6 : ∙ / ∙ ⊢ (◇ A) ⇔ (∼ □ ∼ A)
-ExampleSyn6 {A} = ∧ᵢ (⇒ᵢ (var (zero (∼ (□ (∼ A))) ∙))) (⇒ᵢ (var (zero (◇ A) ∙)))
-
-ExampleSyn7 : ∙ / ∙ ⊢ □ A ⇒ (◇ (A ⇒ B) ⇒ ◇ B)
-ExampleSyn7 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (succ (□ A) (∙ , (□ A)) (zero (□ A) ∙))) (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ A) , (◇ (A ⇒ B))))) (¬ₑ (var (succ (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A) , (◇ (A ⇒ B)))
-                                                                                                                                                   (zero (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) (∙ , A , (∼ B)) (zero (∼ B) (∙ , A)))) (mp (var (zero (A ⇒ B) (∙ , A , (∼ B)))) (var (succ A (∙ , A , (∼ B)) (succ A (∙ , A) (zero A ∙)))))))))))))
-
-ExampleSyn8 : ∙ / ∙ ⊢ □ ∼ A ⇒ □ (A ⇒ B)
-ExampleSyn8 {A} {B} = ⇒ᵢ (□ₑ (var (zero (□ (∼ A)) ∙)) (□ᵢ (⇒ᵢ (⊥ₑ (¬ₑ (var (succ (∼ A) (∙ , (∼ A)) (zero (∼ A) ∙))) (var (zero A (∙ , (∼ A)))))))))
-
-ExampleSyn9 : ∙ / ∙ ⊢ (□ A) ∨ (□ B) ⇒ □ (A ∨ B)
-ExampleSyn9 {A} {B} = ⇒ᵢ (∨ₑ (var (zero ((□ A) ∨ (□ B)) ∙)) (□ₑ (var (zero (□ A) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₁ (var (zero A ∙))))) (□ₑ (var (zero (□ B) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₂ (var (zero B ∙))))))
-
-ExampleSyn10 : ∙ / ∙ ⊢ ◇ A ⇒ ◇ (A ∨ B)
-ExampleSyn10 {A} {B} = ⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ (A ∨ B))) (∙ , (◇ A)))) (¬ₑ (var (succ ( ◇ A) (∙ , (◇ A)) (zero (∼ (□ (∼ A))) ∙))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ (A ∨ B)) (∙ , (∼ (A ∨ B))) (zero (∼ (A ∨ B)) ∙))) (∨ᵢ₁ (var (zero A (∙ , (∼ (A ∨ B))))))))))))
-
-ExampleSyn11 : ∙ / ∙ ⊢ ◇ A ⇒ □ B ⇒ □ ( A ⇒ B )
-ExampleSyn11 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ B) (∙ , (◇ A)))) (□ᵢ (⇒ᵢ (var (succ B (∙ , B) (zero B ∙)))))))
+Completeness : {W : Type} → (p : Formula) → (∀ (m : M W) (x : W) → m , x ⊩ p) → [] / [] ⊢ p
+Completeness p x = {!!}