Concezione assiomatica, dimostrazioni formali e meccanizzabilità della matematica

Secondo la concezione assiomatica della matematica, fare matematica significa principalmente dimostrare teoremi, ovvero produrre dimostrazioni in un sistema formale a partire da determinati assiomi. Per Hilbert, la formalizzazione della matematica aveva come scopo principale fornire una fondazione sicura alla matematica. La concezione assiomatica è stata messa in crisi dai teoremi di Gödel, che mostrano come lo scopo che Hilbert assegnava alla formalizzazione della matematica non possa essere raggiunto. Molti sostenitori della concezione assiomatica ritengono però che ciò non debba significare l’abbandono di tale concezione e affermano che altri risultati della logica matematica, come l’isomorfismo di Curry-Howard, forniscono ragioni sufficienti al mantenimento di tale concezione della matematica. Scopo di questo articolo è valutare tale affermazione.