Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

<>Andrzej:

One might say that the intuitionists think that classical
first order logic is dubious :-) However, that is not the
right way to look at it: classical first order logic is a
subsystem of constructive first order logic (the subsystem
consisting of the negative statements, i.e., the statements
that are equivalent to formulas of the form "not A[]".)

I know. They have this triple negation law
           not not not P[] implies not P[]

For the propositional calculus it had been proved by {/L}kasiewicz in 1953. In the paper he claims that
the intuitionistic logic is _stronger_ that the classical one (he mentions that earlier he believed that is the other way around).
I do not cite his paper, I have only Polish translation. Maybe it would be easier for you to get the original paper and cite him.  

Jan {/L}ukasiewicz, On the intuitionistic theory of deduction. Indagationes Mathematicae. Koninklijke Nederlandse
Akademie van Wetenschappen, Proceedings, Series A, (1953), no. 2, p.113.