<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>On 29 Oct 2009, at 17:22, Vag Vagoff wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>If constructive mathematics is equivalent to classic one without double<br>negation elimination law (from wich law of Excluded Middle is derivable)<br>then constructive mathematics is strictly as powerful as classic because<br>simple algorithm may be created which converts classic proofs to<br>constructive ones automatically using proof continuations and double<br>negation monad (but converted proof will be surrounded by double negation).<br><br>Is this correct?</div></blockquote></div><div><br></div>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.<div><br></div><div>Here by axiom of choice I mean, given A:Set, R : A->A->Set we have</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>(forall x:A,exists y:B,R x y) -> exists f : A->B,forall x:A,R x (f x)</div><div><br></div><div>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:</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>forall x:A,not (forall y:B, not R x y) -> not (forall f : A-> B, not forall x:A,R x (f x))</div><div><br></div><div>but this is not provable in Agda. To see this consider A=TM (Turingmachine configurations), B=Bool and</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>R m true = if m will terminate</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>R m false = if m will not terminate</div><div><br></div><div>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).</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br><div><blockquote type="cite"><div><br><font class="Apple-style-span" color="#000000"><br></font><br>module DoubleNegationIsMonad where<br><br>-- libraries --<br><br>data ⊥ : Set where<br>infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a<br>infixr 90 _∘_ ; _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) ; f<br>∘ g = λ x → f (g x)<br>¬_ : (P : Set) → Set ; ¬ P = P → ⊥<br>¬¬ = λ (p : Set) → ¬ ¬ p<br><br>-- helpers --<br><br>¬¬-intro : ∀ {P} → P → ¬¬ P<br>¬¬-intro p = λ f → f p<br><br>→¬¬-intro : ∀ {P Q} → (P → Q) → (P → ¬¬ Q)<br>→¬¬-intro = _∘_ ¬¬-intro<br><br>¬¬¬→¬ : ∀ {P} → ¬ ¬ ¬ P → ¬ P<br>¬¬¬→¬ {P} nnnp = λ p → (¬¬-intro (¬¬-intro p)) nnnp<br><br>¬¬¬¬→¬¬ : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P<br>¬¬¬¬→¬¬ = ¬¬¬→¬<br><br>swap : ∀ {P Q} → (P → ¬ Q) → (Q → ¬ P)<br>swap pq qp p = (pq p) qp<br><br>swap&intro : ∀ {P Q} → (P → Q) → ¬ Q → ¬ P<br>swap&intro = swap ∘ →¬¬-intro<br><br>lift : ∀ {P Q} → (P → Q) → ¬¬ P → ¬¬ Q<br>lift = swap&intro ∘ swap&intro<br><br>-- monad --<br><br>return : ∀ {P} → P → ¬¬ P<br>return = ¬¬-intro<br><br>infixl 10 _>>=_<br>_>>=_ : ∀ {P Q} → ¬¬ P → (P → ¬¬ Q) → ¬¬ Q<br>ma >>= f = ¬¬¬¬→¬¬ (lift f ma)<br><br>join : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P<br>join = ¬¬¬¬→¬¬<br><br>-- monad laws --<br><br>left-identity : ∀ {A B} → (a : A) → (f : A → ¬¬ B) → return a >>= f ≡ f a<br>left-identity a f = ≡-refl<br><br>right-identity : ∀ {A} → (a : ¬¬ A) → a >>= return ≡ a<br>right-identity a = ≡-refl<br><br>associativity : ∀ {A B C} → (a : ¬¬ A) → (b : A → ¬¬ B) → (c : B → ¬¬ C)<br>→ (a >>= b) >>= c ≡ a >>= (λ x → b x >>= c)<br>associativity a b c = ≡-refl<br><br>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></blockquote></div><br></div></body><br/>
<p>
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.
</p>
</html>