Gerçeklenebilirlik bir kolu olan matematiksel mantık , özellikle gösteri teorisi bir formülleri arasındaki mantıksal ilişkiyi tanımlar, mantıksal sistem ve programları hesaplama modeli . 40'lı yıllarda Kleene tarafından aritmetik Heyting (en) formüllerinin özyinelemeli fonksiyonların kümeleri (indeksi) tarafından yorumlanması olarak tanıtıldı . O zamandan beri diğer tüm mantıksal sistemlere genişletildi ve bugün Curry-Howard yazışmalarının bir genellemesi olarak görülüyor .
Bir formül ve bir program verildiğinde , " gerçekleştirdiği " özelliği belirtiriz ; Bu notasyonu anımsatır ait Cohen'in zorlayarak hangi gerçeklenebilirlik hediyeler biçimsel Analojilerle. Gerçekleştirilebilirlik, formüllerin program özellikleri olarak yorumlanmasına yol açar: örneğin totoloji , bir tür girdisi verildiğinde, bir tür sonucu oluşturan programlarla elde edilir .