Mjapp

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 []))))))