[Agda] Double Negation as Monad

[Thorsten Altenkirch]

On 29 Oct 2009, at 17:22, Vag Vagoff wrote:

> If constructive mathematics is equivalent to classic one without  
> double
> negation elimination law (from wich law of Excluded Middle is  
> derivable)
> then constructive mathematics is strictly as  powerful as classic  
> because
> simple algorithm may be created which converts classic proofs to
> constructive ones automatically using proof continuations and double
> negation monad (but converted proof will be surrounded by double  
> negation).
>
> Is this correct?


Yes, but this works only for Arithmetic but not for Set Theory,  
because classical Mathematicians have this strange belief in the so  
called classical axiom of choice.

Here by axiom of choice I mean, given A:Set, R : A->A->Set we have

	(forall x:A,exists y:B,R x y) -> exists f : A->B,forall x:A,R x (f x)

there is no problem proving this in Agda (interpreting forall by pi- 
types and exists by sigma) but once you apply the double negation  
translation you obtain something equivalent to:

	forall x:A,not (forall y:B, not R x y) -> not (forall f : A-> B, not  
forall x:A,R x (f x))

but this is not provable in Agda. To see this consider A=TM  
(Turingmachine configurations), B=Bool and

	R m true   =  if m will terminate
	R m false  = if m will not terminate

You can prove forall x:A,not (forall y:B, not R x y) which just says  
that you cannot have that a TM doesn't terminate and doesn't not  
terminate. However, the conclusion says that it is impossible that  
there is no function deciding the Halting problem. But indeed, there  
is no function deciding the Halting problem, even though you cannot  
prove this in Agda (you'd need to assume that all functions are  
computable, this is called Church's thesis).

Cheers,
Thorsten

>
>
>
> module DoubleNegationIsMonad where
>
> -- libraries --
>
> data ⊥ : Set where
> infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡- 
> refl : a ≡ a
> infixr 90 _∘_ ; _∘_ : ∀ {A B C : Set} → (B → C) → (A →  
> B) → (A → C) ; f
> ∘ g = λ x → f (g x)
> ¬_ : (P : Set) → Set ; ¬ P = P → ⊥
> ¬¬ = λ (p : Set) → ¬ ¬ p
>
> -- helpers --
>
> ¬¬-intro : ∀ {P} → P → ¬¬ P
> ¬¬-intro p = λ f → f p
>
> →¬¬-intro : ∀ {P Q} → (P → Q) → (P → ¬¬ Q)
> →¬¬-intro = _∘_ ¬¬-intro
>
> ¬¬¬→¬  : ∀ {P} → ¬ ¬ ¬ P → ¬ P
> ¬¬¬→¬ {P} nnnp = λ p → (¬¬-intro (¬¬-intro p)) nnnp
>
> ¬¬¬¬→¬¬  : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
> ¬¬¬¬→¬¬ = ¬¬¬→¬
>
> swap : ∀ {P Q} → (P → ¬ Q) → (Q → ¬ P)
> swap pq qp p = (pq p) qp
>
> swap&intro : ∀ {P Q} → (P → Q) → ¬  Q → ¬  P
> swap&intro = swap ∘ →¬¬-intro
>
> lift : ∀ {P Q} → (P → Q) → ¬¬ P → ¬¬ Q
> lift = swap&intro ∘ swap&intro
>
> -- monad --
>
> return : ∀ {P} → P → ¬¬ P
> return = ¬¬-intro
>
> infixl 10 _>>=_
> _>>=_ : ∀ {P Q} → ¬¬ P → (P → ¬¬ Q)  → ¬¬ Q
> ma >>= f = ¬¬¬¬→¬¬ (lift f ma)
>
> join : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
> join = ¬¬¬¬→¬¬
>
> -- monad laws --
>
> left-identity : ∀ {A B} → (a : A) → (f : A → ¬¬ B) →  
> return a >>= f ≡ f a
> left-identity a f = ≡-refl
>
> right-identity : ∀ {A} → (a : ¬¬ A) → a >>= return ≡ a
> right-identity a = ≡-refl
>
> associativity : ∀ {A B C} → (a : ¬¬ A) → (b : A → ¬¬ B)  
> → (c : B → ¬¬ C)
> → (a >>= b) >>= c ≡ a >>= (λ x → b x >>= c)
> associativity a b c = ≡-refl
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091029/86be14c9/attachment.html