Produrre assiomi evidenti
Ciao a tutti.
In un testo di Lolli è riportata l'analisi di un testo del 1951 di Kurt Gödel.
Cito:
Non riesco a capire cosa si intenda con "produzione di assiomi". Cosa vuol dire? In che modo si costruisce una regola che produce assiomi?
So che dagli assiomi, tramite regole di inferenza, si raggiungono altre proposizioni; ma tali proposizioni sono teoremi, non assiomi.
Se gli assiomi sono "evidenti", cosa vuol dire che ci sia una regola in grado di produrli?
Spero che qualcuno possa chiarirmi le idee a riguardo
In un testo di Lolli è riportata l'analisi di un testo del 1951 di Kurt Gödel.
Cito:
La seconda alternativa, che esistano problemi assolutamente insolubili,
è stata ricavata dalla ipotesi o eventualità che per la matematica propria
soggettiva esista una macchina che produce tutti i suoi assiomi evidenti.
Non riesco a capire cosa si intenda con "produzione di assiomi". Cosa vuol dire? In che modo si costruisce una regola che produce assiomi?
So che dagli assiomi, tramite regole di inferenza, si raggiungono altre proposizioni; ma tali proposizioni sono teoremi, non assiomi.
Se gli assiomi sono "evidenti", cosa vuol dire che ci sia una regola in grado di produrli?
Spero che qualcuno possa chiarirmi le idee a riguardo
Risposte
Ciao.
Potresti, per favore, scrivere cosa c'è prima della parte che hai citato e dirmi anche di cosa si sta parlando più precisamente? Così non riesco ad inquadrare il contesto e non me la sento di provare a risponderti.
Potresti, per favore, scrivere cosa c'è prima della parte che hai citato e dirmi anche di cosa si sta parlando più precisamente? Così non riesco ad inquadrare il contesto e non me la sento di provare a risponderti.
Salve xunil1987,
sicuramente si riferisce a questo scritto (pg. 12)
Se mietitore lo confermasse però sarebbe meglio!
Cordiali saluti
"xunil1987":
Ciao.
Potresti, per favore, scrivere cosa c'è prima della parte che hai citato e dirmi anche di cosa si sta parlando più precisamente? Così non riesco ad inquadrare il contesto e non me la sento di provare a risponderti.
sicuramente si riferisce a questo scritto (pg. 12)
Se mietitore lo confermasse però sarebbe meglio!
Cordiali saluti
Ciao garnak,
hai sicuramente ragione. La citazione di mietitore è proprio testuale. Avevo intuito che si trattasse di filosofia della matematica.
Credo che con produzione di assiomi ci si riferisca qui alla possibilità di definire una macchina (di Turing?) che sia in grado di produrre in sequenza una lista di assiomi che siano giudicati evidenti secondo una definizione sintattica.
Ma si tratta di filosofia avanzata e con tante insidie. Non ci scommetterei sulla mia ipotesi.
hai sicuramente ragione. La citazione di mietitore è proprio testuale. Avevo intuito che si trattasse di filosofia della matematica.
Credo che con produzione di assiomi ci si riferisca qui alla possibilità di definire una macchina (di Turing?) che sia in grado di produrre in sequenza una lista di assiomi che siano giudicati evidenti secondo una definizione sintattica.
Ma si tratta di filosofia avanzata e con tante insidie. Non ci scommetterei sulla mia ipotesi.
Chiedo scusa per il ritardo con cui rispondo.
Il riferimento è proprio quello che avete rintracciato.
Ciò che mi chiedo è: se gli assiomi sono evidenti, come possono essere "prodotti" a partire da altro?
Cosa intendi per "evidenti secondo una definizione sintattica"?
Il riferimento è proprio quello che avete rintracciato.
Ciò che mi chiedo è: se gli assiomi sono evidenti, come possono essere "prodotti" a partire da altro?
Cosa intendi per "evidenti secondo una definizione sintattica"?
Ciao.
Dicendo "definizione sintattica", cercavo di dare un'idea del fatto che, prima di usare una macchina, occorre avere in mano una definizione formale di assioma evidente.
Un qualunque modello di calcolo è costituito da regole costruttive con cui manipolare i simboli di una data stringa e dare eventualmente una risposta positiva o negativa su una certa domanda che ci si pone.
Per esempio, data una certa stringa di simboli su un alfabeto del primo ordine, dire se questa è oppure no una formula ben formata, un assioma della teoria del primo ordine, un teorema, etc.
Oppure, dato un certo alfabeto e determinate regole di costruzione delle formule (o degli assiomi), scrivere in sequenza tutte le possibili formule (assiomi).
Per fare questo, è necessario prima stabilire una definizione formale degli oggetti che stiamo studiando. Una fbf è una stringa dell'alfabeto tale che ... un'assioma è una fbf tale che, un teorema è una fbf tale che ... eccetera.
Ora, devo ammettere che non ho letto integralmente e con molta attenzione il tuo riferimento, ma non mi sembra che ci sia questa definizione formale per il concetto di assioma evidente. E questo mi lascia immaginare che si stia facendo una dissertazione naive della faccenda. Ad ogni modo mi va di aggiungere che Lolli è sempre stato molto difficile da leggere
Spero che voglia intervenire qualcuno più esperto di me per chiarire definitivamente la faccenda.
Saluti.
p.s. è possibile che per assiomi evidenti si stiano intendendo le tautologie?
Dicendo "definizione sintattica", cercavo di dare un'idea del fatto che, prima di usare una macchina, occorre avere in mano una definizione formale di assioma evidente.
Un qualunque modello di calcolo è costituito da regole costruttive con cui manipolare i simboli di una data stringa e dare eventualmente una risposta positiva o negativa su una certa domanda che ci si pone.
Per esempio, data una certa stringa di simboli su un alfabeto del primo ordine, dire se questa è oppure no una formula ben formata, un assioma della teoria del primo ordine, un teorema, etc.
Oppure, dato un certo alfabeto e determinate regole di costruzione delle formule (o degli assiomi), scrivere in sequenza tutte le possibili formule (assiomi).
Per fare questo, è necessario prima stabilire una definizione formale degli oggetti che stiamo studiando. Una fbf è una stringa dell'alfabeto tale che ... un'assioma è una fbf tale che, un teorema è una fbf tale che ... eccetera.
Ora, devo ammettere che non ho letto integralmente e con molta attenzione il tuo riferimento, ma non mi sembra che ci sia questa definizione formale per il concetto di assioma evidente. E questo mi lascia immaginare che si stia facendo una dissertazione naive della faccenda. Ad ogni modo mi va di aggiungere che Lolli è sempre stato molto difficile da leggere
Spero che voglia intervenire qualcuno più esperto di me per chiarire definitivamente la faccenda.
Saluti.
p.s. è possibile che per assiomi evidenti si stiano intendendo le tautologie?
Ti cito:
Cerco di fare un mini-ragionamento. Per avere un sistema formale (o macchina di Turing equivalente) dobbiamo avere un linguaggio (di simboli primitivi, termini e formule ben formate), degli assiomi e delle regole di deduzione.
Io so che le regole di deduzione si "applicano" agli assiomi per ottenere dei teoremi.
Ma di "regole" per produrre teoremi non ho esperienza. O meglio, possono esserci regole per creare delle formule ben formate del sistema (che poi possono essere analizzate per sapere se sono teoremi o meno). Per esempio, per la logica di I ordine,
\(\displaystyle A \rightarrow @ \)
non sarà una formula ben formata se il simbolo @ non è previsto nel linguaggio della logica di I ordine.
Ma come faccio a sapere se una formula ben formata è un assioma o meno? Per un po' ho pensato che per "assiomi" intendesse dire "teoremi", ma la caratterizzazione di "evidenti" mi pare escludere questa possibilità.
Oppure, dato un certo alfabeto e determinate regole di costruzione delle formule (o degli assiomi), scrivere in sequenza tutte le possibili formule (assiomi).
Cerco di fare un mini-ragionamento. Per avere un sistema formale (o macchina di Turing equivalente) dobbiamo avere un linguaggio (di simboli primitivi, termini e formule ben formate), degli assiomi e delle regole di deduzione.
Io so che le regole di deduzione si "applicano" agli assiomi per ottenere dei teoremi.
Ma di "regole" per produrre teoremi non ho esperienza. O meglio, possono esserci regole per creare delle formule ben formate del sistema (che poi possono essere analizzate per sapere se sono teoremi o meno). Per esempio, per la logica di I ordine,
\(\displaystyle A \rightarrow @ \)
non sarà una formula ben formata se il simbolo @ non è previsto nel linguaggio della logica di I ordine.
Ma come faccio a sapere se una formula ben formata è un assioma o meno? Per un po' ho pensato che per "assiomi" intendesse dire "teoremi", ma la caratterizzazione di "evidenti" mi pare escludere questa possibilità.
Come hai detto tu stesso, quando definisci un sistema formale $T$ stai anche scegliendo qual è il sottoinsieme delle fbf che sono assiomi. Questa scelta puoi farla in modo che esista una macchina di Turing che, presa una qualunque fbf $\varphi$ della teoria $T$, essa stabilisca in un numero finito di transizioni se $\varphi$ sia un assioma oppure no. Se tale macchina esiste, allora l'insieme degli assiomi è detto decidibile. Una teoria siffatta, per esempio, è la teoria di Zermelo-Fraenkel i cui assiomi sono le tautologie e quelle formule che trovi scritte su un libro di fondamenti che tratta $ZF$.
In tal caso, è possibile definire anche una macchina di Turing che produca (senza fermarsi!) la lista di tutti gli assiomi di $ZF$. Anzi, se non sbaglio per questa teoria si riesce a dimostrare che esiste una macchina di Turing che produce la lista di tutti i teoremi di $ZF$. Per questo motivo, l'insieme dei teoremi viene detto semi-decidibile o ricorsivamente enumerabile.
È in questo senso che si intende il verbo "produrre". Non è che una macchina con i suoi calcoli produce nuovi assiomi, semplicemente ne scrive la lista.
Ci sono altre teorie, invece, in cui l'insieme degli assiomi non è decidibile. Un esempio che mi viene in mente è la teoria che sceglie come assiomi l'insieme di tutti i teoremi dell'aritmetica di Peano.
Il punto (b) in effetti non è ragionevole, proprio perché non è detto che esista una Turing in grado di decidere in tempo finito se una formula non è derivabile da tutte le altre.
Dunque la domanda che ti ponevi tu all'inizio di questo thread ora me la pongo anche io.
Cosa si intende per assiomi evidenti? Dovrebbe, secondo me, essere data una definizione formale per poter poi definire un modello di calcolo che li produca.
In tal caso, è possibile definire anche una macchina di Turing che produca (senza fermarsi!) la lista di tutti gli assiomi di $ZF$. Anzi, se non sbaglio per questa teoria si riesce a dimostrare che esiste una macchina di Turing che produce la lista di tutti i teoremi di $ZF$. Per questo motivo, l'insieme dei teoremi viene detto semi-decidibile o ricorsivamente enumerabile.
È in questo senso che si intende il verbo "produrre". Non è che una macchina con i suoi calcoli produce nuovi assiomi, semplicemente ne scrive la lista.
Ci sono altre teorie, invece, in cui l'insieme degli assiomi non è decidibile. Un esempio che mi viene in mente è la teoria che sceglie come assiomi l'insieme di tutti i teoremi dell'aritmetica di Peano.
Il punto (b) in effetti non è ragionevole, proprio perché non è detto che esista una Turing in grado di decidere in tempo finito se una formula non è derivabile da tutte le altre.
Dunque la domanda che ti ponevi tu all'inizio di questo thread ora me la pongo anche io.
Cosa si intende per assiomi evidenti? Dovrebbe, secondo me, essere data una definizione formale per poter poi definire un modello di calcolo che li produca.
Grazie mille Mi prendo un po' di tempo per pensarci e andare alla ricerca di libri che ne parlino. Sono sicuro di aver letto qualcosa del genere in Franzén (Gödel's Theorem), quindi appena possibile andrò a cercare lì e ti farò sapere se ho trovato informazioni utili.
Se qualcuno ha chiarificazioni a riguardo gliene sarei più che grato
Mi prendo un po' di tempo per pensarci e andare alla ricerca di libri che ne parlino. Sono sicuro di aver letto qualcosa del genere in Franzén (Gödel's Theorem), quindi appena possibile andrò a cercare lì e ti farò sapere se ho trovato informazioni utili.Se qualcuno ha chiarificazioni a riguardo gliene sarei più che grato
Così a naso mi sento di concordare con xunil1987, ovvero che s'intenda semplicemente che l'insieme degli "assiomi della matematica" è ricorsivo.
Se un insieme è ricorsivamente enumerabile, allora esiste un algoritmo in grado di generare tutte le stringhe che appartengono all'insieme. Cioè c'è una procedura meccanica che, seguendo alcune regole, ne scrive una lista.
L'insieme dei teoremi di un sistema formale è ricorsivamente enumerabile.
Nel caso della logica del primo ordine, si può scegliere un insieme di assiomi decidibile. Quindi una macchina di Turing può decidere se una formula sia un assioma della teoria in questione oppure no.
Parafraso quello che dice Gödel:
Nel caso della matematica soggettiva (formata da tutte le verità matematiche umanamente dimostrabili), non sarebbe possibile escludere l'esistenza di una regola finita in grado di produrne tutti gli [infiniti] assiomi evidenti.
Quindi, secondo quanto stiamo dicendo, potrebbe esistere un algoritmo in grado di enumerare uno dopo l'altro tutti gli assiomi che l'uomo usa nei vari sistemi formali. Giusto?
Eppure, c'è ancora qualcosa che mi sfugge.
Ipotizziamo di avere un insieme di assiomi finito. In che modo un algoritmo riesce a trovare tutti i suoi assiomi? Come fa a distinguere tra gli assiomi e i teoremi?
Un'enumerazione dell'insieme dei numeri naturali funziona scrivendo prima le stringhe di una sola cifra, poi quelle di due cifre, e così via, ordinandole (magari) in ordine crescente. Quindi:
\(\displaystyle 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 ... \)
In questo modo ogni membro dell'insieme apparirà nella lista (ipotizzando di andare avanti all'infinito).
Ma per gli assiomi una procedura del genere come si svolge? Come faccio a sapere quali sono i membri dell'insieme e quali no?
Conosco i numeri naturali, e posso stabilire una regola per enumerarli tutti a partire dalle prime 10 cifre combinate tra loro. Ma per gli assiomi come funziona?
Sono confuso.
L'insieme dei teoremi di un sistema formale è ricorsivamente enumerabile.
Nel caso della logica del primo ordine, si può scegliere un insieme di assiomi decidibile. Quindi una macchina di Turing può decidere se una formula sia un assioma della teoria in questione oppure no.
Parafraso quello che dice Gödel:
Nel caso della matematica soggettiva (formata da tutte le verità matematiche umanamente dimostrabili), non sarebbe possibile escludere l'esistenza di una regola finita in grado di produrne tutti gli [infiniti] assiomi evidenti.
Quindi, secondo quanto stiamo dicendo, potrebbe esistere un algoritmo in grado di enumerare uno dopo l'altro tutti gli assiomi che l'uomo usa nei vari sistemi formali. Giusto?
Eppure, c'è ancora qualcosa che mi sfugge.
Ipotizziamo di avere un insieme di assiomi finito. In che modo un algoritmo riesce a trovare tutti i suoi assiomi? Come fa a distinguere tra gli assiomi e i teoremi?
Un'enumerazione dell'insieme dei numeri naturali funziona scrivendo prima le stringhe di una sola cifra, poi quelle di due cifre, e così via, ordinandole (magari) in ordine crescente. Quindi:
\(\displaystyle 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 ... \)
In questo modo ogni membro dell'insieme apparirà nella lista (ipotizzando di andare avanti all'infinito).
Ma per gli assiomi una procedura del genere come si svolge? Come faccio a sapere quali sono i membri dell'insieme e quali no?
Conosco i numeri naturali, e posso stabilire una regola per enumerarli tutti a partire dalle prime 10 cifre combinate tra loro. Ma per gli assiomi come funziona?
Sono confuso.
"mietitore":
L'insieme dei teoremi di un sistema formale è ricorsivamente enumerabile.
Questo non è sempre vero. Per ottenere ciò che dici, in genere, è necessario che gli assiomi del sistema formino un insieme ricorsivo enumerabile e che le regole d'inferenza siano calcolabili.
"mietitore":
Nel caso della logica del primo ordine, si può scegliere un insieme di assiomi decidibile. Quindi una macchina di Turing può decidere se una formula sia un assioma della teoria in questione oppure no.
Giusto un piccolo appunto. Fino ad ora tutti i modelli di calcolo proposti si sono rivelati simulabili da una macchina di Turing. Da ciò è seguita quella che oggi si definisce "Tesi di Turing" secondo cui le macchine che portano il suo nome non saranno mai superabili in potenza espressiva. Se mai ci si dovesse sbagliare e si scoprisse una macchina ideale più potente della Turing, chiaramente la definizione di decidibilità andrà riferita a questo nuovo modello.
"mietitore":
Quindi, secondo quanto stiamo dicendo, potrebbe esistere un algoritmo in grado di enumerare uno dopo l'altro tutti gli assiomi che l'uomo usa nei vari sistemi formali. Giusto?
No. Perché abbiamo sempre parlato di un singolo sistema formale alla volta e abbiamo discusso della sua decidibilità a prescindere dagli altri.
"mietitore":
Conosco i numeri naturali, e posso stabilire una regola per enumerarli tutti a partire dalle prime 10 cifre combinate tra loro. Ma per gli assiomi come funziona?
Per gli assiomi di solito si usa la tecnica della Gödelizzazione. Che consiste, guarda caso, nell'individuare una codifica delle formule di una teoria in numeri naturali. Tutto questo in modo che una macchina ideale possa scorrere l'elenco dei numeri naturali ed operare decodificandovi la formula associata, stabilendo inoltre se essa sia oppure no un assioma.
Per i teoremi funziona più o meno allo stesso modo. Si codifica la sequenza di formule in un numero naturale, facendo in modo che la macchina possa operare sul numero decodificandone la sequenza e riconoscendone una dimostrazione , così che in caso positivo possa classificare come teorema l'ultima formula di suddetta sequenza.
Per qualche ulteriore dettaglio sul mondo della calcolabilità ti consiglio i seguenti testi.
Martin Davis - Computability, complexity and languages;
Michael Sipser - Introduction to the theory of computation.
"mietitore":
Sono confuso.
Ti capisco
"xunil1987":
Giusto un piccolo appunto. Fino ad ora tutti i modelli di calcolo proposti si sono rivelati simulabili da una macchina di Turing. Da ciò è seguita quella che oggi si definisce "Tesi di Turing" secondo cui le macchine che portano il suo nome non saranno mai superabili in potenza espressiva. Se mai ci si dovesse sbagliare e si scoprisse una macchina ideale più potente della Turing, chiaramente la definizione di decidibilità andrà riferita a questo nuovo modello.
Un altro piccolo appunto
Modelli più potenti della macchina di Turing esistono, un esempio concreto sono le famiglie non uniformi di circuiti. La mdT è però il più potente sistema di calcolo realizzabile fisicamente (le famiglie non uniformi di circuiti non lo sono perché ad ogni dimensione dell'input bisognerebbe associare un circuito differente con la possibilità che non esista una mdT in grado di generare il circuito adatto per ogni dimensione dell'input).
Ma perché, la mdT è realizzabile fisicamente?
Non conosco queste famiglie di circuiti non uniformi. Mi stai dunque dicendo che la Tesi di Turing è falsa? Interessante!
Non conosco queste famiglie di circuiti non uniformi. Mi stai dunque dicendo che la Tesi di Turing è falsa? Interessante!
"xunil1987":
Ma perché, la mdT è realizzabile fisicamente?
Non conosco queste famiglie di circuiti non uniformi. Mi stai dunque dicendo che la Tesi di Turing è falsa? Interessante!
Sì, la mdt è realizzabile fisicamente (beh, nastro infinito a parte, ma possiamo pensare di aggiungere pezzi di nastro ogni volta che finiamo quelli a disposizione). Il computer con il quale ti scrivo è programmabile con linguaggi di programmazione che hanno certamente la stessa espressività della macchina di Turing.
"xunil1987":
Non conosco queste famiglie di circuiti non uniformi. Mi stai dunque dicendo che la Tesi di Turing è falsa? Interessante!
No! La tesi di Church-Turing dice che la classe delle funzioni "intuitivamente calcolabili" coincide con la classe delle funzioni calcolabili da una mdT. Questo non vuol dire che non possano esistere modelli astratti più potenti della mdT (ed infatti esistono, io te ne ho fatto un esempio, un altro potrebbe essere quello di una mdT che ha un oracolo in grado di decidere se una mdT termina su tutti gli input o meno... ma ce ne sono milioni!), semplicemente che modelli realistici, che possono essere implementati fisicamente, saranno al più equivalenti alla mdT. E finora questa tesi si è dimostrata vera.
Adesso è tutto più chiaro. È una differenza sottilissima. Grazie per la precisazione.
[OT]
un piccolo spunto Fisico: http://web.eecs.umich.edu/~taustin/EECS ... Limits.pdf sulla realizzazione od approssimazione di una macchina di Turing
[/OT]
"Deckard":
Modelli più potenti della macchina di Turing esistono, un esempio concreto sono le famiglie non uniformi di circuiti. La mdT è però il più potente sistema di calcolo realizzabile fisicamente
un piccolo spunto Fisico: http://web.eecs.umich.edu/~taustin/EECS ... Limits.pdf sulla realizzazione od approssimazione di una macchina di Turing
[/OT]
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo