| Andrew Cooke | Contents | Latest | RSS | Twitter | Previous | Next

C[omp]ute

Welcome to my blog, which was once a mailing list of the same name and is still generated by mail. Please reply via the "comment" links.

Always interested in offers/projects/new ideas. Eclectic experience in fields like: numerical computing; Python web; Java enterprise; functional languages; GPGPU; SQL databases; etc. Based in Santiago, Chile; telecommute worldwide. CV; email.

Personal Projects

Lepl parser for Python.

Colorless Green.

Photography around Santiago.

SVG experiment.

Professional Portfolio

Calibration of seismometers.

Data access via web services.

Cache rewrite.

Extending OpenSSH.

Last 100 entries

NYT Has More Details; Obvious Question; Advertising Low Cost Routes?; Similar Analysis Here; My Current Take On Surveillance Scandal; Last.fm is Hiring; How I Am 2; The back-wards compatibility fallacy; Wiggle The Mouse To Pass The Test; Python Enums on Crack, Part II; Multiple Monitors with Linux; What Is Happening In Turkey; A Simpler Enum; John Fogerty on IAmA; And You May Well Ask...; Progress on a Better Enum; I'm a MACHIIIIIIIIIIIIIIINE; Those little tab things on the side of jet engines; Re: Python's sad, unimaginative Enum; Some explanation; Printing binary trees sideways; About "Python's sad, unimaginative Enum"; Atoms in python; Some good feedback here; Frustration Understood; I agree with you #nt; What would be imaginative?; Re: Enum; this is fucking useless; Enum; Python's sad, unimaginative Enum; Possible Fix; Work, Exhaustion, Vacation; VirtualBox with Centos 6.3 to 6.4, client; Matasano - Programming Lessons Learned; PDF to HTML; Alternate Substitution; Why RSA Works; Trigger; Dreaming of Death; Example: Tracing; Using Coroutines In Protocol Simulations; Python 3.3 Only; Pure Python SHA1 and MD4 Implementations; Ubuntu on VirtualBox; Starting TOR as a service on OpenSuse 12.3; 1001 Albums; Using fail2ban on OpenSuse 12.3; PPPoE on OpenSuse 12.3; Good Article on Unified Physics; It's Police (Carabineros); Linux Software for Listening to and Exploring Music; Android is Pretty Bad; Lucky Number; 3D Printing for Casting; Cover Art for MPDroid; Who'd a thought the French were so bigoted?; PS Input Signal; Small Problem with Roksan K2 Amp; Roksan K2 Amp + ATC SCM7 Speakers; Do What Makes Sense; Re: Arguing About Tests, Still; Arguing About Tests, Still; Images; Good Article on NY Drummers; Related Bug Report; Getting Python 3.3 and Virtualenv Working in OpenSuse 12.3; How I Am; Awesome video about digital audio; The Difference Between Dimensional and Normalized Databases; The rise of the new Chinese bogeyman; Updated Syntax; Very First Steps to C-ORM; The Ideal User Interface For Music Exploration; Can The Republicans Be Saved?; Rate Limiting Calls to EchoNest; Mods to Cache; Comparing UYKFG and UYKFD/E/F; Someone Else is Concerned; EchoNest-based Playlist Generator for MPD; Example Voting Results; A Heavyweight Python Cache; Identifying Artists with EchoNest; Notes on Pregalex / Pregabalina / Lyrica; The Neil Cowley Trio; Drake - Make for Data; A Reliable Python Web Service; Useful Python Date/Time Library?; Need to Sleep, But this is Good; Command Line Set Difference; Little Details...; Linux Command Line Tricks; AutoTools Tutorial; Hangman Tactics; A Tor Proxy Embedded In A Web Page; Tree (Nested Dicts) in Python; Sleeping at Parties; I Know Someone Who Hurts Other People; Light and Tea; Description of the LCS35 Time Capsule Crypto-Puzzle; Re: I can relate to that ...

© 2006-2013 Andrew Cooke (site) / post authors (content).

Embedding Classical in Intuitionist Logic

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

Comment on this post