Intuitionistin mielestä mahdollinen ristiriitaa hyödyntävä todistus vaikkapa Goldbachin konjektuurin negaatiolle ("on olemassa 2 suurempi parillinen kokonaisluku, jota ei voida ilmaista kahden alkuluvun summana") ei vielä tarkoittaisi, että while-silmukka, joka testaa kokonaislukuja järjestyksessä ko. pysähtymisehdolla välttämättä ikinä pysähtyisi.

Klassinen logiikka voidaan upottaa intuitionistiseen logiikkaan esimerkiksi Kolmogorovin kaksoisnegaatiomuunnoksella k(a) = ¬¬a, k(b → c) = ¬¬(k(b) → k(c)) (a on jokin peruspropositio). Brouwer-Heyting-Kolmogorov-tulkinnassa intuitionistinen väite ¬x tarkoittaa (x → ⊥) eli että kaikista x:n todistuksista voidaan konstruoida mahdoton olio. Toisin sanoen klassinen peruspropositio tulkitaan intuitionistisesti niin, että olisi ristiriitaista, että ko. väitteestä seuraisi ristiriita jne.

(Vaughan-Williams - Tallis Fantasia)

lisäys:

Periaate oli tässä postauksessa tärkein, mutta valitsin tuon esimerkin (Goldbach) huonosti, sillä se on aritmeettisessä hierarkiassa niin heikko väite, että sille tuo klassinen todistus ilmeisesti riittää Turingin koneen, joka generoi tuon luvun, konstruointiin, kuten Gödel osoitti Dialectica-tulkinnassaan. Nimittäin Π₂⁰ kaavoille vielä pätee tuo, mutta ei enää Π₃⁰, sillä niillä pystyy spesifioimaan pysähtymistesterin.

lisälukemista konstruktiiviseen logiikkaan liittyen:

Lectures on the Curry-Howard Isomorphism-kirja (suppeampi PDF-versio löytyy netistä) 
Andrzej Filinskin diplomityö: Declarative Continuations and Categorical Duality (.ps-tiedosto) 
Coq
Paul Taylor: Real Analysis in Abstract Stone Duality
CPS-translaatio (Kolmogorov-upotus)