>Leggo che, dato un sistema formale, una proposizione " ben fatta" può
>essere vera, falsa, o indecidibile ( ovvero non si può decidere, nel
>sistema, se sia vera o falsa )
No. In un sistema formale abbiamo proposizioni dimostrabili, refutabili o
indecidibili. Una proposizione e' vera o falsa non nel sistema formale in
se', ma in riferimento a un modello del sistema.
>Prima questione che non capisco: quando una proposizione è ben fatta
>rispetto ad un dato sistema formale?
Quando ne rispetta le regole sintattiche.
>E' ovvio che la proposizione " il
>mare domani sarà mosso " è indecidibile rispetto all'aritmetica,
No. Non e' indecibile: non fa nemmeno parte dell'aritmetica, perche'
l'aritmetica non parla di mare.
>Potrei anche dire che ogni affermazione indecidibile sia estranea
>al sistema, in qanto, appunto, il sistema non può dire nulla
>sualla falsità o verità di essa.
Completamente fuori strada. Le proposizioni indecidibili sono interne al
sitema, ma semplicemente irraggiungibili da un percorso di deduzione.
>Tutte le indecidibili sarebbero dunque equivalenti a " il mare domani sarà
>mosso"
No.
>Risolto il problema di quando una proposizione sia ben fatta, pongo
>laS econda questione: come può essere strutturata una dimostrazione
>che una proposizione è indecidibile rispetto ad un sistema dato?
>Esiste uno schema dimostrativo comune?
Ci possono essere metodi semantici, o, meglio ancora, sintattici. In una
dimostrazione semantica di indecidibilita', l'indimostrabilita' di una
proposizione A e della sua negazione ~A si fa ricorrendo alla conoscenza
di due modelli rispettivamente incompatibili con A e ~A e viceversa. Ad
esempio, nella teoria elementare dei gruppi, la proposizione
A = (per ogni x)(per ogni y) xy=yx
e la sua negazione sono indecidibili, perche' A e' vera in un modello di
gruppo abeliano (come potrebbe essere Z) ma falsa in un gruppo non abeliano
(come S_3), e ~A viceversa.
Invece in un metodo sintattico si prescinde dalla conoscenza di modelli: un
esempio banale puo' essere una teoria S del primo ordine con numerali 0,
s(0)=1, s(s(0))=2, ...., un solo predicato unario P, e per assiomi
specifici solo
P(0)
(per ogni x)( P(x) --> P(s(s(x))) )
In S, ne' P(1) ne' ~P(1) (ad esempio) sono dimostrabili: infatti si
puo' dimostrare per induzione sul numero di connettivi di un teorema
che in tutte le occorrenze di P(n) n e' un numerale pari. Ciao
> Leggo che, dato un sistema formale, una proposizione " ben fatta" può
> essere vera, falsa, o indecidibile ( ovvero non si può decidere, nel
> sistema, se sia vera o falsa )
Sbagliato. In un sistema formale una proposizione può essere
dimostrabile, refutabile o indecidibile.
È dimostrabile se ammette una dimostrazione nel sistema formale,
refutabile se la sua negazione è dimostrabile. Se né la proposizione
né la sua negazione sono dimostrabili, la proposizione è indecidibile.
Il concetto di "vero" e "falso" si usano con i modelli. In un dato
modello del sistema formale ogni proposizione è vera o falsa.
Risulta che una proposizione è dimostrabile se e solo se è vera
in /ogni/ modello del sistema formale; refutabile se è falsa in
ogni modello; indecidibile se è vera in almeno un modello e falsa
in almeno un altro modello.
> Prima questione che non capisco: quando una proposizione è ben fatta
> rispetto ad un dato sistema formale? E' ovvio che la proposizione " il
> mare domani sarà mosso " è indecidibile rispetto all'aritmetica, ma
> ciò non sembra interessante. Potrei anche dire che ogni affermazione
> indecidibile sia estranea al sistema, in qanto, appunto, il sistema
> non può dire nulla sualla falsità o verità di essa. Tutte le
> indecidibili sarebbero dunque equivalenti a " il mare domani sarà
> mosso"
Un sistema formale usa un linguaggio formale. Le proposizioni "ben
fatte" sono quelle che rispettano le regole sintattiche del sistema.
> Risolto il problema di quando una proposizione sia ben fatta, pongo
> laS econda questione: come può essere strutturata una dimostrazione
> che una proposizione è indecidibile rispetto ad un sistema dato?
Un metodo te l'ho già detto. Per esempio è stato usato con successo
per dimostrare l'indecidibilità dell'ipotesi del continuo nella teoria
degli insiemi ZF. Un altro metodo consiste nell'analisi delle
dimostrazioni; il teorema di Gödel-Rosser (nell'aritmetica esistono
proposizioni indecidibili) si dimostra infatti costruendo una
proposizione che è impossibile dimostrare o refutare.
> Esiste uno schema dimostrativo comune?
No. Una delle tante conseguenze del teorema di Gödel-Rosser è che
in un sistema formale "sufficientemente potente" non esiste alcun
procedimento meccanico che dica se una proposizione è dimostrabile,
refutabile o indecidibile. "Meccanico" nel senso che possa essere
eseguito, almeno in linea di principio, da una macchina.
Ciao
Enrico
> No. In un sistema formale abbiamo proposizioni dimostrabili, refutabili o
> indecidibili. Una proposizione e' vera o falsa non nel sistema formale in
> se', ma in riferimento a un modello del sistema.
Che differenza c'e' tra vero e dimostrabile ?
Nel senso :
come fai a sapere che in un modello M di S una proposizione P e'
vera, se non la *dimostri* tale ?
Per esempio l' aritmetica e' un modello del sistema formale di
Peano, giusto ? E pero' le proposizioni dell' aritmetica vanno
dimostrate, per sapere se sono o non sono vere.
Sicuro? Si dimostra dai primi quattro postulati?
Nel modello di geometria non euclidea dove vengono chiamate "rette" i
cerchi massimi su una superficie sferica, non esistono rette parallele
(a meno di definire banalmente "parallele" anche due rette coincidenti -
ma comunque nessuna parallela passa per un punto esterno). Se quello che
dici e' vero, questo modello dovrebbe *violare* uno dei primi quattro
postulati. Quale?
--
TRu-TS
Buon vento e cieli sereni
È ben noto che i cinque postulati euclidei (più le nozioni comuni)
non caratterizzano affatto la retta come la pensiamo noi, cioè aperta.
La non esistenza di un triangolo con due angoli retti richiede qualcosa
di più.
L'asserzione di Paolo è corretta se intendiamo con "i primi quattro
postulati euclidei" gli assiomi di Hilbert, escluso quello delle
parallele.
Ciao
Enrico
>Paolo ha scritto:
>> ... se partiamo dai postulati della
>> geometria euclidea togliendo quello delle parallele, cioč:"Data
>> una retta r e un punto p che non giace su r, per p passa una ed
>> una sola parallela.", otteniamo un teorema:"Data una retta r ed
>> un punto p esterno ad essa, per p passa almeno una parallela".
>
>Sicuro? Si dimostra dai primi quattro postulati?
Mi sembra che l'OP voglia intendere che *non* si dimostra dai primi quattro
postulati.
>Nel modello di geometria non euclidea dove vengono chiamate "rette" i
>cerchi massimi su una superficie sferica, non esistono rette parallele
>(a meno di definire banalmente "parallele" anche due rette coincidenti -
>ma comunque nessuna parallela passa per un punto esterno). Se quello che
>dici e' vero, questo modello dovrebbe *violare* uno dei primi quattro
>postulati.
Comunque questo non e' un buon esempio, in quanto il modello della
geometria sferica viola l'assioma di prolungabilita' infinita di un
segmento di retta. Magari un modello di geometria iperbolica e' meglio.
Ciao
Il teorema dell'esistenza di almeno una parallela lo si ricava
proprio dai quattro postulati.
Allora ? T' ho messo in crisi ? :D
> Leggo che, dato un sistema formale, una proposizione " ben fatta" può
> essere vera, falsa, o indecidibile ( ovvero non si può decidere, nel
> sistema, se sia vera o falsa )
Orrore!! Stai facendo una gran confusione.
Può essere:
* vera in ogni modello
* falsa in ogni modello
* vera in alcuni modelli e falsa in altri modelli
Oppure:
* dimostrabile dagli assiomi del sistema
* con negazione dimostrabile dagli assiomi del sistema
* non dimostrabile nè lei nè la negazione dagli assiomi del sistema
(altrimenti detta indecidibile)
Esempio:
Assiomi
1) A->B
2) B->C
* A->C è dimostrabile dagli assiomi e vera in ogni modello
* non(A->B) ha negazione dimostrabile ed è falsa in ogni modello
* C->A è indecidibile, vera in alcuni modelli, falsa in altri
> Prima questione che non capisco: quando una proposizione è ben fatta
> rispetto ad un dato sistema formale?
Non è una proposizione ad essere ben fatta, è una stringa di simboli.
Ecco la definizione formale:
* logica proposizionale:
http://it.wikipedia.org/wiki/Logica_proposizionale#Formule_ben_formate
*logica predicativa:
http://it.wikipedia.org/wiki/Linguaggio_del_primo_ordine#Formule_ben_formate
> On 16 Set, 07:15, radicale 003 <radicale....@gmail.com> wrote:
> > On 15 Set, 20:45, El Filibustero <spall...@gmail.com> wrote:
> >
>
> Allora ? T' ho messo in crisi ? :D
Non credo che ci sia crisi.
Ti posso esprimere un enunciato E, ben fatto, che non è dimostrabile
all'interno di un dato sistema formale, ma che sia vero.
La dimostrazione di verità è raggiunta agendo fuori dal sistema formale dato.
Ho appena letto un caso mlto bello ( il sistema MIU descritto a pag 132 de "
Goedel, Escher e Bach ,..... )
L' ho gia' chiesto a El F. ma siccome non risponde (avra'
le sue buone ragioni) ci riprovo con te :
Che differenza c'e' tra vero e dimostrabile ?
Ma nel senso :
come fai a sapere che in un modello M di S una proposizione P e'
vera, se non la *dimostri* tale ?
Per esempio l' aritmetica e' un modello del sistema formale di
Peano, giusto ? E pero' le proposizioni dell' aritmetica vanno
dimostrate, per sapere se sono o non sono vere.
Giusto ?
> Non credo che ci sia crisi.
Vallo a dire alle opposizioni.
>Ti posso esprimere un enunciato E, ben fatto, che non è
>dimostrabile all'interno di un dato sistema formale, ma
>che sia vero.
Ok
>La dimostrazione di verità è raggiunta agendo fuori dal
>sistema formale dato.
Ma sempre una dimostrazione e'.
Comunque :
come si fa a fare una dimostrazione "agendo fuori dal
sistema formale" ?
Ho sempre avuto una certa difficolta' a capire questo
punto.
..> L'asserzione di Paolo è corretta se intendiamo con "i primi quattro
> postulati euclidei" gli assiomi di Hilbert, escluso quello delle
> parallele.
Mi pare anche che sia stato anche un povero cristo ( Sacchiri ? ) che tentò
tutta la vita di dedurre il fatto delle parallele dai primi 4 postulati.
Ovviamente ( col senno del poi ) non ci riuscì. Tanto che sconsigliò al
figlio ( anche lui matematico <) di lasciar perdere l'avventura, in quanto
si sarebbe amareggiato la vita.
E' interessante il fatto che, in questo tentativo, costruì una serie di
teoremi basati sulla non validità dell'assioma delle parallele validi in
geometrie non eucldee.
Interessante è anche il fatto ( dal punto di vista psicologico e non
matematico )che costui alla fine, per non dichiarare il fallimento, affermo'
che i suoi teoremi derivanti dalla negazione delle parallele, "ripugnavano
alla ragione"
........
> come si fa a fare una dimostrazione "agendo fuori dal
> sistema formale" ?
>
> Ho sempre avuto una certa difficolta' a capire questo
> punto.
>
Prova a leggerti la pagina che ti ho detto.
Comunque, di mio, posso pensare ad una cosa del genere
Prendi il sistema formale di Peano.
In esso è ben fatta l'affermazione:
" esistono infinite coppie di numeri P1, P2 la cui differenza P2-P1 sia 140"
Infatti il sistema di Peano tratta numeri interi, e l'affermazione riguarda i
numeri interi.
Ora, immagina che l'_unico_ modo per dimostrare che quest'affermazione sia
vera passi attraverso i numeri complessi.
Si avrebbe un'affermazione vera ma non derivabile ( dimostrabile ) dal sistema.
> > Interessante è anche il fatto ( dal punto di vista psicologico e non
> > matematico )che costui alla fine, per non dichiarare il fallimento,
affermo'
> > che i suoi teoremi derivanti dalla negazione delle parallele, "ripugnavano
> > alla ragione"
>
> "ripugna alla natura della linea retta"
>
EHI..E' un aneddoto così noto?? Pensavo di aver pescato per caso la cosa nei
meandri dei pettegolezzi "colti"
Ciao
> Enrico Gregorio <greg...@math.unipd.it> ha scritto:
>
> > > Interessante č anche il fatto ( dal punto di vista psicologico e non
> > > matematico )che costui alla fine, per non dichiarare il fallimento,
> affermo'
> > > che i suoi teoremi derivanti dalla negazione delle parallele,
> > > "ripugnavano
> > > alla ragione"
> >
> > "ripugna alla natura della linea retta"
> >
>
> EHI..E' un aneddoto cosě noto?? Pensavo di aver pescato per caso la cosa nei
> meandri dei pettegolezzi "colti"
Be', ho letto e discusso parecchio sull'argomento. :)
Ciao
Enrico
> > Può essere:
> > * vera in ogni modello
> > * falsa in ogni modello
> > * vera in alcuni modelli e falsa in altri modelli
> > Oppure:
> > * dimostrabile dagli assiomi del sistema
> > * con negazione dimostrabile dagli assiomi del sistema
> > * non dimostrabile nè lei nè la negazione dagli assiomi del sistema
> > (altrimenti detta indecidibile)
>
> L' ho gia' chiesto a El F. ma siccome non risponde (avra'
> le sue buone ragioni) ci riprovo con te :
>
> Che differenza c'e' tra vero e dimostrabile ?
Una differenza abbastanza grande visto che la verità è un concetto
semantico mentre la dimostrabilità è un concetto sintattico che
prescinde dal significato che può essere dato alle formule.
> Ma nel senso :
> come fai a sapere che in un modello M di S una proposizione P e'
> vera, se non la *dimostri* tale ?
>
> Per esempio l' aritmetica e' un modello del sistema formale di
> Peano, giusto ? E pero' le proposizioni dell' aritmetica vanno
> dimostrate, per sapere se sono o non sono vere.
Dipende da che cosa intendi per "dimostrazione".
1) Se stai parlando della "dimostrazione formale" nel sistema S
(quella consistente nel derivare fbf in sequenza in base a regole
meccaniche partendo dalle fbf che rappresentano gli assiomi) allora
non è difficile trovare esempi di situazioni in cui tu puoi conoscere
la verità di un enunciato senza eseguire la "dimostrazione formale"
della sua fbf (ti invito a pensarci su e produrre tu stesso degli
esempi).
2) Se per "dimostrazione" intendi un generico "argomento
convincente" (secondo gli standard dei matematici) che porta a
concludere la verità di qualcosa allora il discorso si sposta sul
filosofico spinto, e si potrebbe citare il sorprendente caso di
Ramanujan che riusciva a "vedere" con la sua intuizione delle verità
matematiche sofisticate senza ricorrere a "dimostrazioni".
> si potrebbe citare il sorprendente caso di
> Ramanujan che riusciva a "vedere" con la sua intuizione delle verità
> matematiche sofisticate senza ricorrere a "dimostrazioni".
Questa almeno è la versione di Hofstadter, wikipedia invece dice che
si tratta di una credenza errata e secondo alcuni lui semplicemente
svolgeva dimostrazioni a parte senza scriverle sul quaderno per
risparmiare carta.
Mioddio che bellezza.. e allo stesso tempo.. che tristezza! :)
> Una differenza abbastanza grande visto che la verità è un concetto
> semantico mentre la dimostrabilità è un concetto sintattico che
> prescinde dal significato che può essere dato alle formule.
Si ma questo mi e' chiaro.
Posso avere la tua attenzione un attimino ?
Tu, per sapere se una affermazione F in un modello M che
ha SF come modello formale e' VERA, devi pur sempre ricorrere ad una
dimostrazione.
Quindi ricapitolando :
in un modello M ogni affermazione sappiamo che deve essere o
vera o falsa. Bene.
Ma per sapere QUALE dei due valori (v,f) prende effettivamente,
dobbiamo ricorrere ad una dimostrazione.
Allora,
supponiamo che quell' affermazione F sia indecidibile in un
certo sistema formale SF che ha M come UNO dei
suoi modelli.
Siccome e' indecidibile, non esiste nessuna dimostrazione
formale in SF tale da poter dire che e' vera in ogni M di
SF.
Supponiamo pero' di sapere che e' Vera in un certo M di
SF.
Allora per quanto detto sopra l' abbiamo dimostrato.
Ma questa dimostrazione NON PUO' essere una di quelle
fattibili in SF. (altrimenti sarebbe decidibile)
Dunque : qual' ' la NATURA di questa dimostrazione ?
Ci troviamo di fronte a due alternative possibili, mi sembra :
data una F di SF avente M come modello.
1)
Sia F indecidibile in SF. Allora non sappiamo dire, in ogni
M di SF, se e' V o F. Sappiamo solo che e' V, oppure F.
2) OPPURE :
disponiamo di una dimostrazione di natura non precisata
che non si sa che cacchio e' che ci dice che F e' vera
in M (o falsa)
FORSE : abbiamo una dimostrazione fatta in un SF
piu' GRANDE, piu' potente del precedente o che cacchio
ne so io.
Capito ?
> FORSE : abbiamo una dimostrazione fatta in un SF
> piu' GRANDE, piu' potente del precedente o che cacchio
> ne so io.
Ma a pensarci bene quest' ultima non e' possibile,
perche' se esistesse un SF(+) piu' POTENTE di SF
tale che F in SF(+) sia decidibile, allora F deve
essere vera in *ogni* modello M di SF(+)
Ma allora, siccome ogni M di SF e' ANCHE M di
SF(+), arriveremmo all' assurdo che F e' vera
in ogni M di SF(+), mentre puo' essere vera in
certi modelli M e falsa in altri in SF.
Cioe' esiste almeno un M in cui F e' vera E falsa.
Percio' rimane solo la prima alternativa :
di una F indecidibile NON possiamo sapere
se e' vera o falsa, qualsiasi sia l' SF che andiamo
a prendere.
> Prendi il sistema formale di Peano.
> In esso è ben fatta l'affermazione:
> " esistono infinite coppie di numeri P1, P2 la cui differenza P2-P1 sia 140"
> Infatti il sistema di Peano tratta numeri interi, e l'affermazione riguarda i
> numeri interi.
> Ora, immagina che l'_unico_ modo per dimostrare che quest'affermazione sia
> vera passi attraverso i numeri complessi.
> Si avrebbe un'affermazione vera ma non derivabile ( dimostrabile ) dal sistema.
E no, perche' se
F = " esistono infinite coppie di numeri P1, P2 la cui differenza P2-
P1 sia 140"
non e' decidibile in SF = Peano, allora esistono modelli di SF(Peano)
in cui
e' vera e altri in cui e' falsa.
Ma se mi dimostri che e' vera passando attraverso i complessi,
dovrebbe essere vera in TUTTI i modelli che hanno SF(Peano).
Come si spiega questo fatto ?
> Dunque : qual' ' la NATURA di questa dimostrazione ?
>
> Ci troviamo di fronte a due alternative possibili, mi sembra :
> data una F di SF avente M come modello.
> 1)
> Sia F indecidibile in SF. Allora non sappiamo dire, in ogni
> M di SF, se e' V o F. Sappiamo solo che e' V, oppure F.
>
> 2) OPPURE :
> disponiamo di una dimostrazione di natura non precisata
> che non si sa che cacchio e' che ci dice che F e' vera
> in M (o falsa)
>
> FORSE : abbiamo una dimostrazione fatta in un SF
> piu' GRANDE, piu' potente del precedente o che cacchio
> ne so io.
Ma pressochè *tutte* le dimostrazioni matematiche con cui si ha a che
fare NON sono fatte in un sistema formale (non sono derivazioni
formali di fbf, sono cose decisamente meno formali e più umanamente
comprensibili) quindi non è chiaro quale sia il tuo problema nel
concepire una dimostrazione che non è fatta in nessun sistema formale
visto che lo sono praticamente tutte. Forse non ti è chiaro che cosa
sia invece una "dimostrazione formale".
Neanche se prendi il sistema che ha F come assioma?
> Ma pressochè *tutte* le dimostrazioni matematiche con cui si ha a che
> fare NON sono fatte in un sistema formale (non sono derivazioni
> formali di fbf, sono cose decisamente meno formali e più umanamente
> comprensibili)
Dannazione. :D
... Scusa non ti irritare, ma non m' hai capito :D
Saro' io.
Si,
ma debbono pur essere comunque traducibili in una dimostrazione
formale, senno' ti ci PULISCI IL CULO. Chiaro ?
E QUINDI ... Ce risemo :
qual' e' la LORO NATURA ????
Cioe' Lord ... La domanda e' semplice :
Come stracazzo fai a sapere che in un certo modello una
affermazione e' VERA ?
> > Ma pressochè *tutte* le dimostrazioni matematiche con cui si ha a che
> > fare NON sono fatte in un sistema formale (non sono derivazioni
> > formali di fbf, sono cose decisamente meno formali e più umanamente
> > comprensibili)
>
> Dannazione. :D
> ... Scusa non ti irritare, ma non m' hai capito :D
> Saro' io.
>
> Si,
> ma debbono pur essere comunque traducibili in una dimostrazione
> formale, senno' ti ci PULISCI IL CULO. Chiaro ?
Le dimostrazioni formali sono una creazione del '900, prima di allora
la matematica progrediva lo stesso senza porsi il problema di una tale
totale formalizzabilità (anche perchè non esisteva neanche il concetto
di "sistema formale"), non per questo Gauss e Riemann pensavano che le
loro dimostrazioni fossero buone solo come carta igienica.
> E QUINDI ... Ce risemo :
> qual' e' la LORO NATURA ????
>
> Cioe' Lord ... La domanda e' semplice :
> Come stracazzo fai a sapere che in un certo modello una
> affermazione e' VERA ?
Di solito lo sai o perchè lo intuisci in modo evidente oppure sei a
conoscenza di un argomento rigoroso e convincente a sostegno della
verità di quella cosa (cioè una dimostrazione NON formale).
> Le dimostrazioni formali sono una creazione del '900, prima di allora
> la matematica progrediva lo stesso senza porsi il problema di una tale
> totale formalizzabilità (anche perchè non esisteva neanche il concetto
> di "sistema formale"), non per questo Gauss e Riemann pensavano che le
> loro dimostrazioni fossero buone solo come carta igienica.
> Di solito lo sai o perchè lo intuisci in modo evidente oppure sei a
> conoscenza di un argomento rigoroso e convincente a sostegno della
> verità di quella cosa (cioè una dimostrazione NON formale).
Non *percepisci* ( in modo informale :D ) che c'e' qualcosa che non
va in tutto cio' ? No eh ?
Mah.
Non penso di essere l'unico a non percepirlo.
> La domanda e' semplice :
> Come stracazzo fai a sapere che in un certo modello una
> affermazione e' VERA ?
Cosa c'e' di meglio che far rispondere al creatore stesso della teoria
dei modelli, Alfred Tarski:
"Qualunque cosa possa ottenersi dalla costruzione di una definizione
adeguata del concetto di verita per un linguaggio scientifico, una
cosa e certa: la definizione NON porta con se un criterio pratico
per decidere se una particolare proposizione di tale linguaggio sia
vera o falsa (e invero questo NON E affatto IL SUO SCOPO). Si
consideri per esempio la seguente proposizione nel linguaggio della
geometria elementare: le tre bisettrici di un triangolo passano per
uno stesso punto. Se ci interessa sapere se questa proposizio e vera
e ci rifacciamo alla definizione di verita per scoprirlo, siamo
destinati ad avere una DELUSIONE. Lunica informazione che ricaviamo
e che la proposizione e vera se le tre bisettrici di un triangolo
si incontrano sempre in un punto, e falsa in caso contrario; solo un
indagine di natura geometrica ci permettera di decidere come stanno
le cose in realta.
[ ... ] Non e compito della logica o della teoria della verita
scoprire
se una proposizione e vera o falsa."
Alfred Tarski, Le scienze Ottobre 1972
.
Giovanni