C[omp]ute

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