Principio terzo escluso e proced. matematico alinguistico

[nato_pigro1]

Sto leggendo un libro che ad un certo punto pone la seguente questione:

Supponiamo che nel linguaggio matematico, cercando di trattare un'operazione matematica intuizionistica, si formuli, alla cieca, per una volta, la figura di un'applicazione di uno dei principi della logica classica. Tale figura accompagna un reale procedimento matematico alinguistico nel sistema matematico reale considerato?

L'autore si risponde che ciò non è possibile nel caso del principio del terzo escluso, per cui tale principio non può servire per la scoperta di nuove verità matematiche.

Cosa si intende qui per "procedimento matematico alinguistico"?
E perchè ciò non è possibile per il principio del terzo escluso?

[fields1]

"nato_pigro":Ma $\Phi$ deve dipendere sia da $h$ che da $f$?

Si', nel caso generale in cui uno voglia dimostrare (1) per $f$ arbitraria. Io per comodita' l'ho considerata fissata.

In pratica è $\Phi$ che mi rappresenta il punto di minimo, giusto?

In un certo senso si'. $\Phi$ rappresenta il contenuto costruttivo associato all'esistenza "ideale" del minimo, ne rappresenta una approssimazione parametrica ad $h$. Piu' la funzione controesempio $h$ e' sofisticata, piu' $\Phi(h)$ si avvicinera' al vero minimo. Il punto importante e' che $\Phi$ e' computabile (su argomenti computabili, ovviamente).

[nato_pigro1]

Ma $\Phi$ deve dipendere sia da $h$ che da $f$?

In pratica è $\Phi$ che mi rappresenta il punto di minimo, giusto?

[fields1]

"Sergio":
Temo, però, che per capirci davvero qualcosa bisognerebbe vedere come gli intuizionisti riformulano tanti teoremi, in particolare sulla continuità.

Possiamo anche prendere esempi piu' semplici. Consideriamo il teorema (in logica classica)

(1) $\exists x\in NN \forall y\in NN\ f(x)\leq f(y)$

dove $f: NN -> NN$.

E' ben noto che tale teorema non si puo' dimostrare in logica intuizionista, perche' in generale non si puo' costruire quell'$x$ in un numero finito di passi. (Provare per credere: qualcuno riesce a dimostrare (1) senza procere per assurdo o usare il terzo escluso?)

Che cosa fa allora un intuizionista? Di solito formula un teorema equivalente, dal punto di vista della logica classica, ma intuizionisticamente piu' debole. Una tecnica consolidata e' la No-Counterexample Interpretation di Kreisel. Ad esempio, si puo' dimostrare costruttivamente:

(2) $\forall h: NN-> NN \exists x\in NN\ f(x)\leq f(h(x))$

che e' equivalente (classicamente) a (1). In altri termini, si puo' costruire un funzionale $\Phi: (NN->NN)-> NN$ tale che

$\forall h: NN-> NN\ f(\Phi (h))\leq f(h(\Phi(h)))$

Vediamo il motivo del nome No-Counterexample Interpretation. Dimostrare (1) equivale a dimostrare che non esistono controesempi ad (1), ovvero funzioni $h:NN->NN$ tali che

$\forall x\in NN\ f(x)>f(h(x))$.

Il funzionale $\Phi$ prende allora un supposto controesempio $h$ ad (1) e fa vedere che effettivamente non e' un controesempio

[nato_pigro1]

Si, no, va bene. Quello ok.

Quindi "alinguistico" significa indipendente dal formalismo logico?

Il rifiuto del principio del terzo escludo nega la validità dell'inferenza $notnotP => P$, ma la giustificazione di questa posizione sta nel fatto che sarebbe una inferenza solo "linguistica" e non intuitiva?

[nato_pigro1]

si, lo so che parla dell'intuizionismo, il libro si intitola "lezioni sull'intuizionismo" ^^
volevo delucidazioni un po' più specifiche...