Allora, prima un disclaimer: non ho i titoli né le skill per dichiararmi un esperto di logica. Non sono un logico, né un matematico. Se questo per te non è un deterrente, leggi pure la risposta.
Diamoci delle definizioni
provvisorie molto naif, tanto per essere sicuri di parlare la stessa lingua.
Verità dimostrabili
Una teoria è un insieme (finito o infinito) di assiomi, i quali sono formule chiuse (ovvero senza variabili libere) date su un certo linguaggio.
Una dimostrazione in una teoria è una sequenza finita di formule in cui ognuna segue dalle precedenti o dagli assiomi della teoria, secondo regole d'inferenza fissate.
I teoremi di una teoria sono le formule dimostrabili nella teoria, ovvero tutte le formule di tutte le dimostrazioni.
Per dire che la formula $ ~\varphi $ è un teorema della teoria $ ~T $ (secondo regole d'inferenza fissate una volta per tutte, e sulle quali non ci interessa discutere) si usa la notazione $ ~T \vdash \varphi $, e si dice colloquialmente "$ ~T $ dimostra $ ~\varphi $".
Verità semantiche
Un modello di una teoria è un insieme che "interpreta" i simboli del linguaggio dando loro un significato, in modo che gli assiomi della teoria siano veri. Ad esempio, i naturali sono un modello della teoria di Peano sul linguaggio (0, succ). Si prende l'insieme $ ~\mathbb N $, si dà un'interpretazione al simbolo 0 (con poca fantasia, al simbolo 0 facciamo corrispondere il naturale 0), si dà un significato alla funzione successore, e si vede che gli assiomi sono verificati.
Se $ ~M $ è un insieme in cui viene data una certa interpretazione dei simboli di un certo linguaggio, e $ ~\varphi $ è una formula dello stesso linguaggio che è vera su $ ~M $, allora si scrive $ ~M\models \varphi $.
Quindi $ ~M $ è un modello della teoria $ ~T $ sse in esso sono veri tutti gli assiomi di $ ~T $, ed in tal caso si scrive più brevemente $ ~M\models T $, e si dice "$ ~M $ modella $ ~T $". Nota che una stessa teoria può avere molti modelli non isomorfi tra loro, nessun modello, etc.
Se una formula $ ~\varphi $ è verificata da tutti i modelli di una teoria $ ~T $, allora si scrive $ ~T\models \varphi $, e si dice "$ ~T $ verifica $ ~\varphi $".
Completezza
Che legame c'è tra verità dimostrata e verità semantica? Ovvero, che legame c'è tra i teoremi di una teoria e le formule verificate dalla teoria? A priori nessuna, ma in una particolare logica detta logica del prim'ordine (in cui cioè le variabili vengono interpretate solo come elementi del modello, e non come sottoinsiemi qualunque), vale il teorema di completezza di Gödel, secondo cui $ ~T\vdash \varphi \Longleftrightarrow T\models \varphi $ per ogni teoria ed ogni formula. Tra l'altro, la teoria di Peano come viene presentata di solito non è una teoria del prim'ordine, perché l'assioma d'induzione quantifica su sottoinsiemi e non su elementi singoli, ma non ci addentriamo in queste sottigliezze.
Meta-teorie
Come si "ragiona" su una teoria? Ovvero, come si deducono proprietà sui teoremi di una teoria? In sostanza, come si dimostra che $ ~T\vdash \varphi $? In generale ci si pone in una meta-teoria, che solitamente ed in qualche senso è una super-teoria. Ovvero un'altra teoria (data su un linguaggio tipicamente più complicato, ma non sempre, ed in una logica tipicamente più "potente", ma non sempre) in cui tutte le definizioni che ho dato sopra vengono "codificate" ed assiomatizzate, ed in cui effettivamente si riesce a dimostrare che una certa (altra) teoria dimostra una certa formula. Esistono casi emblematici in cui la teoria su cui vogliamo ragionare è così potente da poter essere usata essa stessa come meta-teoria. Questo è il caso della teoria di Peano (per la precisione, una delle tante teorie dell'aritmetica di Peano), in cui formule e dimostrazioni possono essere codificate da numeri interi, ed i predicati che esprimono la dimostrabilità di formule possono essere tradotti in uguaglianze e disuguaglianze tra espressioni aritmetiche. Fare costruzioni di questo tipo è prassi usuale quando si cerca di dimostrare cose come i teoremi d'incompletezza di Gödel, indecidibilità varie (vedi entscheidungsproblem), etc. In particolare, il secondo teorema d'incompletezza di Gödel ruota tutto attorno al fatto che una teoria sufficientemente potente può fungere da meta-teoria di sé stessa.
Matematica quotidiana
Tornando coi piedi per terra, cosa fanno quelle varie dispense di teoria dei gruppi, di aritmetica, di analisi, etc: dimostrano cose in una teoria, in una meta-teoria, wtf?!? La maggior parte di quelle dispense sono scritte da non logici, a cui importa poco o nulla dell'impianto formale low-level, e che vogliono soltanto enunciare fatti veri, fornendo motivazioni plausibili. Quello che dicono implicitamente (a volte
molto implicitamente) è: c'è questa teoria $ ~G $, per gli amici teoria dei gruppi, data sul linguaggio $ ~\{ +\} $, e che contiene gli assiomi $ ~\forall a,b,c,\ (a+b)+c=a+(b+c) $, etc etc. C'è poi una meta-teoria mooooolto mooooolto "meta", data sul linguaggio umano, che non assiomatizziamo (altrimenti dovremmo inventarci una meta-meta-teoria...) ma su cui tutti bene o male concordiamo, in quanto persone umane avvezze al pensiero matematico. Poi formuliamo ad esempio il piccolo teorema di Fermat come formula della meta-teoria, dando per scontata la sua (ovvia) riformulazione $ ~\varphi $ nel linguaggio $ ~\{ +\} $, e procediamo a dimostrarlo nella meta-teoria, "spiegando a parole" come farebbe $ ~G $ a dimostrare $ ~\varphi $. Questo quando le cose vanno bene. Perché quando vanno meno bene (ma non per questo male!), succede che, sempre nella meta-teoria, si considera un modello qualsiasi di $ ~G $ (esempio: "sia H un gruppo, bla bla") e si mostra che esso verifica $ ~\varphi $. In sostanza, si dimostra nella meta-teoria che $ ~G\models \varphi $ e non che $ ~G\vdash \varphi $, appellandosi implicitamente al teorema di completezza di Gödel nel caso di teorie del prim'ordine, e a
qualcos'altro negli altri casi. Fortunatamente, nel caso dell'aritmetica di Peano al second'ordine, il problema non si pone perché vi è un unico modello, a meno d'isomorfismi. Lì il vero problema sta a monte, nella non definibilità di un sistema dimostrativo completo, questione in cui non mi addentro.
Morale
Quindi direi che ora possiamo capire l'obiezione che facevo all'inizio: chiamiamo $ ~PA $ la teoria di Peano (al second'ordine, ma poco importa). Una dispensina, per giunta scritta in Italiano, ci dichiara laconicamente di voler dimostrare il teorema che citavi nel primo post. Perciò enuncia il fatto in linguaggio umano e lo dimostra in una meta-teoria $ MT $, facendo un discorso che richiama vagamente ed implicitamente l'induzione.
Ora, la cosa è ambigua! C'è un dubbio tra due interpretazioni alternative:
1) $ ~MT \vdash (PA \vdash \forall a,b,d, (a+b=a+d \implies b=d)) $,
2) $ ~MT \vdash \forall a,b,d, (PA \models (a+b=a+d \implies b=d)) $.
Nel primo caso l'induzione è usata dentro $ ~PA $, ed è quindi usata in modo essenziale ed "intrinseco", nonostante sia espressa in modo vago perché si tratta in realtà della spiegazione umana di come $ ~PA $ userebbe l'induzione per dimostrare il teorema.
Nel secondo caso l'induzione è usata dentro $ ~MT $, e può quindi essere sostituita con qualunque altro discorso, da una formalizzazione dell'induzione dentro $ ~PA $, giù giù fino ad un "è ovvio", come in effetti è. Infatti sta dicendo semplicemente che in ogni modello di $ ~PA $ (quindi in $ ~\mathbb N $, sostanzialmente) è vero che $ ~(0+0=0+0 \implies 0=0) $, è vero che $ ~(1+0=1+0 \implies 0=0) $, è vero che $ ~(0+1=0+0 \implies 1=0) $, etc etc.
Dunque, quando Tizio arriva e chiede "ma è davvero necessario usare l'induzione per dimostrare quel fatterello?", è evidente come la (colpevole?) trascuratezza della dispensa non solo abbia fatto inorridire me, sebbene non ne abbia potuto apprezzare che poche righe, ma abbia contribuito a confondere le idee a qualcuno, da cui il mio sproloquio auspicabilmente chiarificatore.
