formalizzazione

formalizzazione

formalizzazione in generale, il termine designa il processo per il quale proprietà, relazioni e legami tra gli elementi di un problema, di un gioco, di una teoria ecc. sono espressi in forma matematica attraverso l’utilizzo di appropriati simboli e formule che li rappresentano. Così, a livello elementare, il problema di determinare due numeri naturali consecutivi il cui prodotto sia 552 può essere formalizzato mediante l’equazione n(n + 1) = 552 la cui risoluzione fornisce come risposta i numeri 23 e 24. Oppure, in geometria, un problema di ricerca delle intersezioni tra una retta e una circonferenza può essere risolto considerando le loro equazioni in un sistema di riferimento cartesiano, e lo si formalizza allora impostando il sistema costituito da tali equazioni. In queste accezioni si parla di formalizzazione di un problema.

In logica, il significato generale del termine è il medesimo, ma indica più propriamente il processo di costruzione di → sistemi formali i cui assiomi e regole di inferenza costituiscano una esplicita e rigorosa formulazione di tutte le ipotesi e procedure di prova usualmente applicate nella corrispondente teoria intuitiva. La formalizzazione va in questo senso distinta dal processo di assiomatizzazione: mentre questo precisa l’insieme delle nozioni e principi su cui si argomenta in una data teoria, la prima costituisce una ulteriore precisazione dei principi secondo cui si ragiona in una teoria, cioè delle procedure dimostrative ammesse.

Preannunciato dalla enucleazione dell’aspetto puramente matematico-strutturale della geometria, quale emerge dalle indagini di B. Riemann e F. Klein, il processo di formalizzazione ha trovato momenti storicamente assai significativi nell’opera di G. Frege e D. Hilbert. Sulla base di una nuova interpretazione del concetto di analiticità, per cui viene definita analitica una verità per la cui derivazione si richiedono solo definizioni esplicite e le leggi generali logiche, Frege giunse al rifiuto del linguaggio comune e alla costruzione di linguaggi le cui regole di inferenza fossero stabilite in modo preciso ed esplicito. Questa esplicitazione venne poi portata a completo sviluppo con la → metamatematica di Hilbert, in cui la trattazione matematica della stessa nozione di dimostrazione è strettamente connessa alla considerazione dei problemi che la costruzione di sistemi formali fa sorgere. Questi concernono la richiesta che all’interno della teoria sia dimostrabile ogni espressione che è la trascrizione formale di un enunciato vero della corrispondente teoria intuitiva, e che non sia possibile dimostrare una contraddizione. La possibilità che i sistemi formali soddisfino queste due proprietà ha subito profonde limitazioni in seguito ai risultati (1931) di K. Gödel (→ Gödel, teorema di).