Qual è la differenza tra questi due tipi di prove?
Pur impiegando il metodo di induzione per dimostrare, derivare la stringa (formula) " F n → F n + 1 " è diverso dal mostrare che se F n è vero, allora anche F n + 1 ?
Mostrando intendo che usiamo l'espressione F n o la sua conseguenza per derivare F n + 1 . Mi sembra che entrambi alla fine significhino la stessa cosa, ma non ne sono sicuro. C'è qualche differenza meta-matematica o dimostrazione teorica? (Tuttavia, mi sembra che nel derivare la stringa (formula) " F n → F n + 1 " stiamo operando a un meta livello). Se si può dimostrare che quest'ultima è valida, è sempre possibile "derivare" la formula " F n → F n + 1 "?
Risposte
Se ti riferisci alle pagine 259-262 dell'articolo di Turing , la prova che la formula CF n è dimostrabile, per ogni n , è per induzione.
È una dimostrazione di meta-teoria, perché riguarda le formule e la loro derivabilità ("provabilità") nel sistema formale.
La prova è una prova standard per induzione :
(i) Caso base: CF 0 è dimostrabile.
(ii) Fase di induzione: la formula CF n → CF n + 1 è dimostrabile, per ogni n .
Quindi, per induzione, concludiamo che CF n è dimostrabile, per ogni n .
Ora, il problema è: qual è il significato esatto di "formula CF n è dimostrabile "?
È derivabile nel calcolo dei predicati .
Vedere pagina 259:
[...] per mostrare che il problema Hilbert Entscheidungs (il problema richiede un algoritmo che consideri, come input, un'affermazione e risponde "Sì" o "No" a seconda che l'affermazione sia universalmente valida ) non può avere soluzione.
Propongo quindi di mostrare che non può esistere un processo generale per determinare se una data formula A del calcolo funzionale K [vedi Grundzüge der Theoryetischen Logik (1928) , Cap.3 ] di David Hilbert e Wilhelm Ackermann non ci può essere macchina che, alimentato con qualsivoglia una di queste formule, finirà dire se A è dimostrabile.
In corrispondenza di ciascuna macchina di calcolo M costruiamo una formula Un (M) e mostriamo che, se esiste un metodo generale per determinare se Un (M) è dimostrabili, allora esiste un metodo generale per determinare se M stampa mai 0 .
Quindi, cercando di essere più "formale", il risultato a cui ti riferisci equivale (vedi simbolo "tornello" ):
⊢ K CF n , per ogni n ,
dove ⊢ K CF n significa:
"c'è una derivazione della formula CF n nel calcolo funzionale K ".
Nota aggiuntiva : come detto sopra, l'induzione viene eseguita nella meta-teoria, perché si applica alle formule .
Abbiamo una sequenza infinita di formule: {CF 0 , CF 1 , ..., CF n , ...} e consideriamo la proprietà P (n) : = "la formula CF n è dimostrabile (nel calcolo funzionale K )" .
Dimostriamo che CF 0 è dimostrabile, cioè vale P (0) , e dimostriamo che: "se CF n è dimostrabile, allora anche CF n + 1 è dimostrabile, per n qualunque".
Quindi, applicando l' induzione matematica , concludiamo che P (n) vale per ogni n , cioè che:
" CF n è dimostrabile, per ogni n .
Turing scrive " CF n → CF n + 1 è dimostrabile" invece di "se CF n è dimostrabile, allora anche CF n + 1 è dimostrabile".
Non c'è differenza; in simboli, da ⊢ K CF n e ⊢ K CF n → CF n + 1 , per Modus ponens abbiamo ⊢ K CF n + 1 .
Una rappresentazione quasi formale dell'induzione matematica può essere fornita come segue:
Lo stadio che argomentiamo da una k arbitraria al suo successore, sebbene dia l'impressione di uno schema logico, è essenzialmente aritmetico (confronta questo caso con il paradosso dei sorites, per esempio). Intendiamoci, se fosse logico, le sue conseguenze sarebbero molto più ampie di una rivendicazione del logicismo.