formalismo e costruttivismo

Rispondo a quel se fossi foco arderei lo mondo messo in musica da de Andrè in merito alle differenze tra formalismo e costruttivismo (noto anche come intuizionismo) in matematica.

A dire il vero si potrebbe parlarne e scriverne per ore. 

Semplificando molto, per i formalisti una dimostrazione è una catena di ragionamenti sintatticamente e semanticamente corretta. Si precisano gli assiomi della teoria e le regole di inferenza (usualmente l'ambiente di lavoro è la teoria ingenua degli insiemi mista a derivazioni in salsa logica del primo o secondo ordine) e si effettua una dimostrazione. E tra le regole consentite v'è il principio del terzo escluso, utilizzato nei ragionamenti per assurdo.

E poi pure un altro assioma non costruttivo, l'assioma della scelta, la cui vita tormentata nel corso della prima metà del novecento meriterebbe una digressione senza fine.

Ai costruttivisti non piace né il principio del terzo escluso con cui si effettuano le dimostrazioni per assurdo né l'assioma della scelta (si può chiudere un occhio sulla versione numerabile dell'assioma della scelta; ma anche questa è una lunga storia è andrà raccontata un'altra volta).

I costruttivisti attribuiscono un significato particolare a quella che è o dovrebbe essere una dimostrazione. In breve, dimostrare qualcosa significa esibire una costruzione concreta di quel qualcosa. Per i formalisti invece la dimostrazione può essere indiretta, oppure può solo consistere in una dimostrazione di esistenza.

E l'assioma della scelta perché sarebbe controverso? Perché non è "costruttivo". Tra le altre cose esso implica - ed è straordinario e controintuitivo - il principio del terzo escluso a cui è indirettamente legato anche il principio di non contraddizione (in logica classica il principio del terzo escluso afferma che per ogni enunciato T, o T è vero oppure è vera la sua negazione; esiste poi il principio di bivalenza: ogni enunciato T è determinatamente vero o falso).

L'assioma della scelta afferma - nella sua forma numerabile - che da una famiglia numerabile di insiemi è possibile estrarre un elemento preso da ciascuno degli insiemi. Qualcosa di assolutamente intuitivo. Però non è chiaro come estrarre un elemento da ogni insieme. Questo ha generato - e genera - controversie e paradigmi teorici di lavoro.

E le dimostrazioni per assurdo? Ve n'è una famosa, particolarmente semplice che forse potrà aiutare a capire la controversia.

C'era una volta, molti anni fa, la setta dei pitagorici. Essi credevano di poter esprimere ogni grandezza come rapporto tra numeri interi. 2/3 , oppure 1/4 e così via. Intero è bello. Sfortunatamente qualcuno osservò che proprio dal teorema di Pitagora segue che il rapporto tra la diagonale di una quadrato di lato unitario e il lato non può essere espresso come rapporto tra numeri interi.

E la dimostrazione è "per assurdo". Si nega la tesi e si arriva ad una contraddizione. E quindi, applicando il terzo escluso (e il principio di non contraddizione) si conclude che non si dà il caso che la tesi sia falsa.

Invece il costruttivista mostra come qualsiasi rapporto tra numeri interi sia necessariamente di un certo tipo (attraverso la fattorizzazione unica dei numeri interi; tale procedimento è un esempio di "costruzione") e non del tipo richiesto nel caso esistesse l'oggetto della discussione (il rapporto tra diagonale e lato). Ma fa anche di più: è in grado di esibire una costruzione che dice qualcosa di esplicito su tale rapporto (una successione che converge a quel rapporto; in questo semplice caso la radice quadrata di due).

Ora al formalista puro non frega alcunché di questo "esibizionismo costruttivo" anche perché nella maggioranza dei casi richiede un enorme quantità di lavoro che egli reputa inutile (e qui iniziano gli scambi di improperi).

Oggi il costruttivismo ha propri paradigmi e scuole di pensiero più o meno diversificate in base al significato che è possibile attribuire al predicato dimostrare. Ma la storia narra che  Luitzen Brouwer, uno dei primi costruttivisti, fu di fatto cacciato da David Hilbert, il dio dei formalisti. Poco importa, fondò poi la sua scuola, il cui paradigma teorico fu sistematizzato da Arend Heitying. 

Poi vennero altri e la rivoluzione fu completa. Erret Bishop ad esempio ricostrui pazientemente diverse parti dell'analisi matematica utilizzando il paradigma costruttivista (e l'assioma della scelta in versione numerabile).

Tuttavia nella sua versione storica, il costruttivismo è deludente: tutto quello che si può dimostrare costruttivamente lo si può dimostrare formalmente all'interno della logica classica. I teoremi del costruttivismo classico sono i teoremi formali della logica classica senza l'assioma del terzo escluso. 

Io sono un particolare esponente del costruttivismo, più debole del costruttivismo originario. Prediligo i risultati espliciti, ma tollero a volte i risultati non costruttivi (e per alcuni risultati non c'è davvero speranza, almeno utilizzando le teorie oggi a disposizione, di ottenere costruzioni esplicite).
Ad esempio io comprendo formalmente che se una successione è crescente ed è limitata allora dovrà convergere verso un limite; allo stesso modo una macchina che corre a velocità costante verso un ostacolo prima o poi lo colpirà. Però rifiuto di accettare l'argomentazione come definitiva. Perché voglio esplicitamente sapere qual è il limite della successione (equivalentemente quando la macchina colpirà l'ostacolo; il problema naturalmente è risolto se sono note velocità e distanza dall'ostacolo - ma questo cambierebbe i termini del problema rendendolo di fatto costruttivo). Avere una visione costruttiva della vita implica una certa visione del mondo. Problematica ma profonda. Difficile ma affascinante. E sì, la vita è più semplici quando non è costruttiva. Ma ci sono nato così. Chi si contenta, costruisce. E sia.