aritmetizzazione
aritmetizzazione procedimento di associazione biunivoca di un numero naturale a ogni simbolo fondamentale, formula ben formata o successione di formule di una teoria formale. In tal modo, una dimostrazione nella teoria risulta identificata da un numero naturale e ogni discorso attorno alla teoria diviene un discorso attorno a proprietà di numeri. L’idea di un procedimento di riduzione a numeri e a calcolo di ogni asserzione logica o schema dimostrativo risale a G.W. Leibniz (di cui è noto il «Calculemus!» come criterio per dirimere controversie tra filosofi); tuttavia il processo di aritmetizzazione trova compimento solo nel xx secolo, attraverso l’opera di K. Gödel (→ Gödel, teorema di) ed è per questo anche detto gödelizzazione. Il procedimento di aritmetizzazione si basa sul teorema della unicità della fattorizzazione di un numero (→ aritmetica, teorema fondamentale dell’), secondo cui la scomposizione di un numero naturale in fattori primi è univoca, a meno dell’ordine dei fattori: ciò consente di assegnare a ogni simbolo, formula o sequenza di formule un numero avente una particolare scomposizione e risalire così dalla teoria formale all’aritmetica in modo biunivoco e, quindi, non ambiguo (→ Gödel, numero di).