Todos

mambo.agda

@@ -122,7 +122,7 @@ data _/_⊢_ (Δ Γ : Context) : Formula → Type where
   ∨ₑ : Δ / Γ ⊢ X ∨ Y → Δ / Γ , X ⊢ Z → Δ / Γ , Y ⊢ Z → Δ / Γ ⊢ Z
   ⇒ᵢ : Δ / Γ , X ⊢ Y → Δ / Γ ⊢ X ⇒ Y
   ¬ᵢ : Δ / Γ , X ⊢ ⊥ → Δ / Γ ⊢ ∼ X
-  ¬ₑ : Δ / Γ ⊢ X → Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ ⊥
+  ¬ₑ : Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ X → Δ / Γ ⊢ ⊥
   □ᵢ : [] / Δ ⊢ X → Δ / Γ ⊢ □ X
   □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y
   -- TODO: Maybe make it KT45
@@ -134,6 +134,9 @@ KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))
                         (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))))))))
+
 ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X)
 ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))
 
@@ -142,3 +145,13 @@ ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (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)))))))
+
+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 = {!!}