pingu/mambo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Todos

Browse Source
This commit is contained in:
pingu
2025-12-25 23:09:33 +01:00
parent 0e3754808e
commit 4ddf204ae8
1 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
mambo.agda
View File

@@ -145,3 +145,12 @@ ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) [])) (
ExampleSyn3 : [] / [] ⊢ (□ A ∧ □ B) ⇒ □(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))))))) 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 = {!!}