From: "andrew cooke" <andrew@...>
Date: Mon, 5 Jun 2006 12:43:36 -0400 (CLT)
For example, Kolmogorov's embedding of classical propositional logic/proofs into intuitionistic propositional logic/proofs is exactly the the typed CPS transform [...] The Kolmogorov translation is a mapping K on logical formulas to logical formulas, such that a formula f is provable in the classical setting iff K(f) is provable in the intuitionistic setting. Other such translations were given by Goedel and Gentzen (and all are so called double negation translations, because they introduce double negations for every atom or subformula) http://lambda-the-ultimate.org/node/1532 What a neat idea! http://www.ltn.lv/~podnieks/mlog/ml3.htm#s35 And Google turned up this, which looks interesting but which also has a crazy look about it somehow (haven't read it yet) - http://users.viawest.net/~keirsey/mathitself.html Andrew