[Agda] Double Negation as Monad

[Peter Hancock]

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?

Roughly. However, the double negation translation works (there
are three isotopes, by Gentzen, Godel and someone else) only 
works for *logic*, or a system where the atomic formulas are
decidable. (Or maybe just satisfy ~~X -> X.)   You can regard
the translation as a definition of what classical reasoners mean
by disjunction or existential quantification. 

So it is OK for first and second order logic, and some 
subsystems.  It is OK for formal first order arithmetic,
because the atomic formulas are decidable.  In fact the
provable formulas coincide for a wide class of formulas.
(all "pi^0_2" formulas: a theorem of Friedman). 

But it is not 
not OK for a corresponding theory of countably branching
well-founded trees.  The strength is still the same between
the classical and constructive systems, but the
reason is not a mere ~~ translation.

Mathematics is a bit more than logic, and it is not always
clear how "domain specific" axioms of classical mathematics
should be interpreted.  An example is the classical axiom of
choice.

> 
> module DoubleNegationIsMonad where
> 

I'd just like to mention that 
A |-> (A -> R) -> R 
is a monad for any R (needn't be empty.)

Also
A |-> (A -> R) -> A
for which Peirce's law is an algebra, is a monad for any R.
This was noticed by Escardo and Oliva
http://www.cs.bham.ac.uk/%7Emhe/papers/selection-escardo-oliva.pdf
You may find many things of interest in that paper!


I hope that makes some sense.

Hank