On Fri 15 May 2020 05:19:01 AM GMT, Ruben Astudillo wrote:
On 13-05-20 09:15, Olaf Klinke wrote:
Excersise: Prove that intuitionistically, it is absurd to deny the law of excluded middle:
Not (Not (Either a (Not a)))
This fact is indeed truly wondrous. I encourage everyone to ponder it thoroughly. It has been worked into a classical logic fairy tale: http://blog.ezyang.com/2013/04/a-classical-logic-fairy-tale/ (sorry for http) And more in this little Oleg jewel: https://web.archive.org/web/20180901035449/http://okmij.org/ftp/Computation/...
given you seem knowledgeable I want to corroborate with you. I've seen claimed on the web that the CPS transform *is* the double negation [1] [2]. I don't think that true, it is almost true in my view. I'll [...]
Yes, you are right, and your analysis of the situation is correct. Using (_ → R) → R for some fixed statement R instead of ¬¬_ = ((_ → ⊥) → ⊥) is what's called "the R-Friedman translation applied to the double negation translation". It is what powers "Friedman's trick", a marvelous technique for extracting constructive content from classical proofs [1]. People say that you cannot escape the continuation monad. But sometimes, you can. Dickson's lemma nicely illustrates this insight. It states that for any infinite list xs ∷ [Nat], there is an index i such that xs !! i ≤ xs !! (i + 1). This lemma has a trivial classical proof (just pick the minimum of the list xs), but this classical proof is not effective: There is no algorithm for computing the minimum of an infinite list. Using the continuation monad, we can extract the constructive content of this classical proof. See here: https://github.com/iblech/talk-constructive-mathematics/blob/master/law-of-e... Cheers, Ingo [1] Say you want to constructively prove A → B. You already have a classical proof of A → B, and you managed [2] to turn this proof into a constructive proof of ((A → R) → R) → ((B → R) → R), for any as of yet undecided statement R. Now specialize to R ≔ B. Hence we have a constructive proof of ((A → B) → B) → ((B → B) → B). Combining this with the constructive tautologies A → ((A → B) → B) and ((B → B) → B) ↔ B, we obtain a constructive proof of A → B. [2] A metatheorem states that if some statement A is classically provable then its double negation translation and furthermore the R-Friedman translation of the double negation translation are constructively provable. (Incidentally, this metatheorem has a constructive proof.) But "translation" here means more than just replacing A by ¬¬A (respectively ((A → R) → R)). It means introducing a double negation in front of every equality, disjunction and existential quantification. For instance, the ¬¬-translation of ∀x. ∃y. f(x,y) = g(x,y) is ∀x. ¬¬∃y. ¬¬(f(x,y) = g(x,y)). In some circumstances, the double negation translation of a complex statement A is constructively equivalent to ¬¬A, that is, in some circumstances the many nested double negations can be pulled to the front. This is for instance the case for so-called "geometric formulas", statements in which the logical symbols "→" and "∀" don't occur.