Logica matematica: differenze tra le versioni

Contenuto cancellato Contenuto aggiunto
Diablo (discussione | contributi)
Riga 23:
Ma Goedel, nel 1931 con il suo famoso teorema di incompletezza, spezza questo sogno: ogni sistema sufficientemente ricco da contenere l' aritmentica non può essere esplorato completamente partendo da pochi assiomi e regole finitistiche. Ci sarà sempre qualche verità che sfugge a questo tipo di analisi.
 
Nonostante questa grande storia sulla ricerca dei fondamenti, il resto della matematica è stata solo sfiorata da questi metodi. Se apriamo un testo di analisi non troviamo assiomi e derivazioni formali, ma prove abbastanzadimostrazioni discorsive e sicuremente convincenti, ma stilizzate nei passaggi principali e con i passaggi formali lasciati come esercizio al lettore.
 
L' invenzione e la diffusione del computer, macchina logica per eccellenza, sta cambiando la situazione. Da un lato l' informatica utilizza i metodi della logica, questa volta come disciplina applicata, sia per la costruzione dell' hardware che per lo studio delle caratteristitiche e della progettazione del software, dall' altro il sogno formalista trova nei dimostratori automatici di teoremi e nei più semplici "proof assistants" quel complemento alla natura umana, ben attenta alla sostanza e sommersa dai dettagli, indispensabile per portarne a termine il programma.