Ma i costruttivisti negano QUALSIASI dimostrazione per assurdo ?
radicale 001
Barone Barolo
> Oppure ?
Prima di tutto, quando si parla di matematica costruttiva non si intende
un particolare sistema logico, ma un programma di sviluppo della
matematica abbastanza generico, che si ripropone di ricostruire la
matematica su basi più concrete, più significative dal punto di vista
computazionale, più chiare sotto il profilo epistemologico. Quali
assiomi siano poi accettati da un certo costruttivista, dipende spesso
dai suoi gusti.
Di certo nessun costruttivista accetta la forma generale del terzo escluso
A or !A
o equivalentemente l'eliminazione della doppia negazione
!!A -> A
mentre chiaramente è accettata la regola opposta
A -> !!A
ed equivalentemente il terzo escluso debole
!A or !!A.
Anche se il terzo escluso non è accettato in generale, in una teoria
costruttiva possono esistere classi di formule per cui il terzo escluso
è dimostrabile. Per esempio nell'aritmetica di Heyting, si dimostra per
induzione che
\forall x,y. x = y or x != y
-- bb
radicale 001
wrote:
> Di certo nessun costruttivista accetta la forma generale del terzo escluso
> A or !A
Si,
ma il problema e' : * perche' * non l' accettano ?
E questo, inoltre, non implica la non accettazione delle
dimostrazioni per essurdo ?
-------------------------------------------------------------
Un' altra cosa che non c' entra nulla :
Sia A un insieme di assiomi di un certo SF.
Sia x una proposizione ben formata di quell' SF
x e' *indipendente* da A se e solo valgono ambedue
queste fatti :
1)
aggiungendo x ad A :
B = {A, x}, allora B e' coerente.
2)
aggiungendo non x ad A :
B = {A, non x}, allora B e' coerente.
Se sia 1 che 2 non sono vere, allora
A stesso e' incoerente. Fine.
Se e' vera una e l' altra falsa,
allora deve necessariamente esistere una
derivazione D di SF tale che A |- x oppure
A |- non x (a seconda dei casi) ?
superpollo
> On 5 Gen, 21:00, Barone Barolo <xelloss.metalliumDEM...@gmail.com>
> wrote:
>
>> Di certo nessun costruttivista accetta la forma generale del terzo escluso
>> A or !A
>
> Si,
> ma il problema e' : * perche' * non l' accettano ?
preciso che io personalmente non sono un talebano del costruttivismo, ma
"sento" dentro di me una predilezione per i processi costruttivi...
ti faccio un esempio che mi e' caro: R e' uno spazio vettoriale su Q
(nb: dimensione non finita), di conseguenza esiste una base
(dimostrazione non costruttiva); ora, nessuno e' mai stato in grado di
esibire o semplicemente descrivere tale base. a me 'sta cosa mi lascia
l'amaro in bocca, come dire: "la figa esiste, ma tu non la puoi nemmeno
vedere" ... sai che rosicata!
bye
--
Allora il mio amico disse, ma secondo te cosa è piu' grande,
1m oppure 0,1m^2 ?? ...Ancora ci stanno pensando........
radicale 001
> radicale 001 ha scritto:
>
> > On 5 Gen, 21:00, Barone Barolo <xelloss.metalliumDEM...@gmail.com>
> > wrote:
>
> >> Di certo nessun costruttivista accetta la forma generale del terzo escluso
> >> A or !A
>
> > Si,
> > ma il problema e' : * perche' * non l' accettano ?
>
> preciso che io personalmente non sono un talebano del costruttivismo, ma
> "sento" dentro di me una predilezione per i processi costruttivi...
>
> ti faccio un esempio che mi e' caro: R e' uno spazio vettoriale su Q
> (nb: dimensione non finita), di conseguenza esiste una base
> (dimostrazione non costruttiva); ora, nessuno e' mai stato in grado di
> esibire o semplicemente descrivere tale base. a me 'sta cosa mi lascia
> l'amaro in bocca, come dire: "la figa esiste, ma tu non la puoi nemmeno
> vedere" ... sai che rosicata!
Capisco ...
Ma dimostrare che esiste (e quindi e' coerente) e' il primo e
necessario
passo per tentare di costruirla.
D' altra parte, se la costruisci soltanto, come sai che e'
coerente ?
Ecco perche' dicevo che le dimostrazioni costruttive e di pura
esistenza
sono in realta' COMPLEMENTARI.
Ma sto parlando di cose che (per ora) intuisco appena, quindi ...
Barone Barolo
> Si,
> ma il problema e' : * perche' * non l' accettano ?
Se tagli a capocchia non ti rendi conto che la risposta l'ho già data.
"quando si parla di matematica costruttiva non si intende un particolare
sistema logico, ma un programma di sviluppo della matematica abbastanza
generico, che si ripropone di ricostruire la matematica su basi più
concrete, più significative dal punto di vista computazionale, più
chiare sotto il profilo epistemologico."
Esempio di computazionalità: in matematica costruttiva, se dimostri
l'esistenza di un oggetto con una determinata proprietà, allora puoi
anche esibirlo.
> E questo, inoltre, non implica la non accettazione delle
> dimostrazioni per essurdo ?
Per definizione. Le dimostrazioni per assurdo sono, per definizione,
quelle che utilizzano il terzo escluso o un principio equivalente.
Nota che molte dimostrazioni fanno uso di principi (es.
diagonalizzazione di Cantor) che pur essendo annoverati spesso spesso,
scorrettamente, tra le dimostrazioni per assurdo, rimangono costruttivi
perché non richiedono il terzo escluso.
> 1)
> aggiungendo x ad A :
> B = {A, x}, allora B e' coerente.
>
> 2)
> aggiungendo non x ad A :
> B = {A, non x}, allora B e' coerente.
>
> Se sia 1 che 2 non sono vere, allora
> A stesso e' incoerente. Fine.
>
> Se e' vera una e l' altra falsa,
> allora deve necessariamente esistere una
> derivazione D di SF tale che A |- x oppure
> A |- non x (a seconda dei casi) ?
In logica classica sì.
-- bb
radicale 001
wrote:
> Il 06/01/2011 01:27, radicale 001 ha scritto:
> > Si,
> > ma il problema e' : * perche' * non l' accettano ?
>
> Se tagli a capocchia non ti rendi conto che la risposta l'ho gi data.
Si, scusa.
Ma non e' che l' ho saltato, e' che .... Vedi sotto.
> "quando si parla di matematica costruttiva non si intende un particolare
> sistema logico, ma un programma di sviluppo della matematica abbastanza
> generico, che si ripropone di ricostruire la matematica su basi pi
> concrete, pi significative dal punto di vista computazionale, pi
> chiare sotto il profilo epistemologico."
> Esempio di computazionalit : in matematica costruttiva, se dimostri
> l'esistenza di un oggetto con una determinata propriet , allora puoi
> anche esibirlo.
Si,
ma quello che non mi entra in testa e' il motivo profondo per cui
i costruttivisti non accettano il terzo escluso, nel senso :
perche' accettarlo, secondo loro, porta a "problemi" ? Che
c'e' che non gli sconfinfera in quel principio ? Mi spiego ?
> > E questo, inoltre, non implica la non accettazione delle
> > dimostrazioni per essurdo ?
>
> Per definizione. Le dimostrazioni per assurdo sono, per definizione,
> quelle che utilizzano il terzo escluso o un principio equivalente.
> Nota che molte dimostrazioni fanno uso di principi (es.
> diagonalizzazione di Cantor) che pur essendo annoverati spesso spesso,
> scorrettamente, tra le dimostrazioni per assurdo, rimangono costruttivi
> perch non richiedono il terzo escluso.
Intendi la famosa dimostrazione della non - numerabilita' dei reali ?
Gia ! Se ci rifletto bene, e' vero ! E' una dimostrazione "negativa",
ma in realta' lui non dice : supponiamo di avere una lista numerabile
di tutti i reali. Ma lui dice : per ogni lista numerabile di reali, io
posso
costruirne una fatta di reali che non appartengono a quella lista, e
fa
vedere come costruirla. Notevole. Non ci avevo mai pensato.
... Dico bene ? O no ?
> > 1)
> > aggiungendo x ad A :
> > B = {A, x}, allora B e' coerente.
> > 2)
> > aggiungendo non x ad A :
> > B = {A, non x}, allora B e' coerente.
> > Se sia 1 che 2 non sono vere, allora
> > A stesso e' incoerente. Fine.
> > Se e' vera una e l' altra falsa,
> > allora deve necessariamente esistere una
> > derivazione D di SF tale che A |- x oppure
> > A |- non x (a seconda dei casi) ?
> In logica classica si .
Lo sospettavo. Dimmi qualcosa di piu'.
Per favore.
El Filibustero
>Nota che molte dimostrazioni fanno uso di principi (es.
>diagonalizzazione di Cantor) che pur essendo annoverati spesso spesso,
>scorrettamente, tra le dimostrazioni per assurdo, rimangono costruttivi
>perché non richiedono il terzo escluso.
Su questo argomento abbiamo gia' discusso e IMHO ti sbagli di grosso. La
dimostrazione con il metodo di diagonalizzazione di Cantor NON e'
costruttiva. Il tuo errore e' considerare esclusivamente la funzione
diagonale (vedi thread Che significa "dimostrazione finita?"):
>[d(f)](n) := 0 se [f(n)](n) = 1
> 1 se [f(n)](n) = 0
che e' banalmente ricorsiva e quindi costruttiva, dimenticandoti che essa
viene composta con una funzione *non* ricorsiva; la funzione composta
impiegata nella dimostrazione di Cantor non e' quindi ricorsiva. Ciao
Barone Barolo
> Si,
> i costruttivisti non accettano il terzo escluso, nel senso :
> perche' accettarlo, secondo loro, porta a "problemi" ? Che
> c'e' che non gli sconfinfera in quel principio ? Mi spiego ?
Immagino che ci si possa scrivere un libro, ma il succo l'abbiamo già detto.
Non è che i costruttivisti non credano che il terzo escluso sia un
principio VERO.
Piuttosto pensano che la matematica basata sulla logica classica non sia
una buona matematica perché si occupa di ciò che è vero, invece dovrebbe
preoccuparsi di ciò che è ottenibile in modo effettivo.
> Intendi la famosa dimostrazione della non - numerabilita' dei reali ?
> Gia ! Se ci rifletto bene, e' vero ! E' una dimostrazione "negativa",
> ma in realta' lui non dice : supponiamo di avere una lista numerabile
> di tutti i reali. Ma lui dice : per ogni lista numerabile di reali, io
> posso
> costruirne una fatta di reali che non appartengono a quella lista, e
> fa
> vedere come costruirla. Notevole. Non ci avevo mai pensato.
Più o meno.
> Lo sospettavo. Dimmi qualcosa di piu'.
> Per favore.
Non ho tempo di andare nel dettaglio, ma quello che ho scritto si
dimostra facilmente. Sospetto invece che in logica intuizionista la
stessa proprietà non valga, ma per dimostrarlo ci vuole un po' di
ragionamento in più.
-- bb
superpollo
...
> Non è che i costruttivisti non credano che il terzo escluso sia un
> principio VERO.
> Piuttosto pensano che la matematica basata sulla logica classica non sia
> una buona matematica perché si occupa di ciò che è vero, invece dovrebbe
> preoccuparsi di ciò che è ottenibile in modo effettivo.
quotone.
Barone Barolo
> Su questo argomento abbiamo gia' discusso e IMHO ti sbagli di grosso.
Non si pu� essere precisi senza esplicitare la logica in cui si lavora.
Quello che dico io � che il teorema di Cantor � dimostrabile nella
variante intuizionista di ZF.
Come ho scritto sopra, dire "costruttivo" non ha molto senso, un po'
come dire "moderato" o "riformista" in politica. Per� in moltissime
logiche considerate costruttive, puoi dimostrare una variante del
teorema di Cantor.
-- bb
radicale 001
> On Thu, 06 Jan 2011 11:53:54 +0100, Barone Barolo wrote:
> >Nota che molte dimostrazioni fanno uso di principi (es.
> >diagonalizzazione di Cantor) che pur essendo annoverati spesso spesso,
> >scorrettamente, tra le dimostrazioni per assurdo, rimangono costruttivi
> >perché non richiedono il terzo escluso.
>
> Su questo argomento abbiamo gia' discusso e IMHO ti sbagli di grosso. La
> dimostrazione con il metodo di diagonalizzazione di Cantor NON e'
> costruttiva.
Posso (nel mio piccolo) ?
Ma non e' nemmeno per assurdo !
Lui dice :
facciamo una qualunque lista numerabile L di reali.
Ebbene questa ne lascia fuori alcuni, e fa vedere quali.
Siccome vale per *ogni* lista, ne segue che non e' possibile
costruire una lista numerabile che contiene tutti i reali.
Chiedo :
Dove entra il principio del terzo escluso in questo
ragionamento ?
radicale 001
wrote:
> Immagino che ci si possa scrivere un libro, ma il succo l'abbiamo gi detto.
> Non che i costruttivisti non credano che il terzo escluso sia un
> principio VERO.
> Piuttosto pensano che la matematica basata sulla logica classica non sia
> una buona matematica perch si occupa di ci che vero, invece dovrebbe
> preoccuparsi di ci che ottenibile in modo effettivo.
Ma ... Anche dimostrare l' esistenza (o la non) e' ottenere
qualcosa ...
Come dicevo a Super P :
prima di costruire occorre sapere che l' ente esiste (dunque e' non
contraddittorio), e d' altra parte costruire un ente matematico non
basta, occorre mostrarne la coerenza interna.
Ecco che allora le due dimostrazioni (esistenza e costruzione)
sono complementari, collaborano.
> Non ho tempo di andare nel dettaglio, ma quello che ho scritto si
> dimostra facilmente. Sospetto invece che in logica intuizionista la
> stessa propriet non valga, ma per dimostrarlo ci vuole un po' di
> ragionamento in pi .
Ma :
se x e' indipendente, allora una D siffatta non puo' esistere.
Dunque, per "dimostrare" l' indipendenza, occorre necessariamente
uscire dall' SF. Ci vuole (per FORZA) una meta - dimostrazione.
Ma :
io posso ben dimostrare la (DI)pendenza della x in modo meta.
Ma da li a trovare la derivazione D di cui si diceva dianzi,
ce ne vuole. Non e' automatico
Dunque in questo caso noi avremmo dimostrato una esistenza
(in questo caso di una derivazione D) senza aver costruito la
derivazione D : sappiamo solo che esiste.
Ecco che il cerchio si chiude :
Destre e sinistre devono COLLABORARE :-)))
Barone Barolo
> dimostrazione con il metodo di diagonalizzazione di Cantor NON e'
> costruttiva. Il tuo errore e' considerare esclusivamente la funzione
> diagonale (vedi thread Che significa "dimostrazione finita?"):
>
>> [d(f)](n) := 0 se [f(n)](n) = 1
>> 1 se [f(n)](n) = 0
>
> che e' banalmente ricorsiva e quindi costruttiva, dimenticandoti che essa
> viene composta con una funzione *non* ricorsiva; la funzione composta
> impiegata nella dimostrazione di Cantor non e' quindi ricorsiva. Ciao
Comunque questi sono gli equivoci che si verificano quando si discutono
argomenti di logica con qualcuno che ha una (eccellente) formazione
matematica, che però non è una formazione da logico.
Tu dici che la dimostrazione non è costruttiva perché compone la
funzione diagonale con un'altra funzione (generica, ipotetica) non
ricorsiva. Ovvio, visto che ZF parla di funzioni generali: grazie tante!
Presumibilmente, quando parli di insiemi e di funzioni, hai in mente un
modello classico, in cui le funzioni ricorsive sono solo un piccolo
sottinsieme. Questa è la matematica classica, ma non è l'unica
matematica possibile. E' possibile pensare una matematica veramente
costruttiva in cui tutte le funzioni di cui puoi parlare sono ricorsive.
Quando dico che la dimostrazione di Cantor è costruttiva, intendo che è
il suo scheletro ad essere costruttivo: prendi una teoria degli insiemi
costruttiva, che parli esclusivamente di funzioni ricorsive, e la
dimostrazione di Cantor continua a valere.
-- bb
radicale.002
Allora ?
El Filibustero
>Tu dici che la dimostrazione non è costruttiva perché compone la
>funzione diagonale con un'altra funzione (generica, ipotetica) non
>ricorsiva. Ovvio, visto che ZF parla di funzioni generali: grazie tante!
E questo che c'entra? In ZF ci sono anche le funzioni ricorsive. Nessuno
vieta, quando si puo', di fare in ZF dimostrazioni costruttive. Per
esempio, si potrebbe dimostrare costruttivamente l'infinita' dei numeri
primi. Ma quando non si puo' (come nel caso della dimostrazione diagonale
di Cantor), c'e' poco da fare.
>Presumibilmente, quando parli di insiemi e di funzioni, hai in mente un
>modello classico, in cui le funzioni ricorsive sono solo un piccolo
>sottinsieme. Questa è la matematica classica, ma non è l'unica
>matematica possibile.
Bene: come ho sempre sostenuto, tu non parli di cio' che si intende
comunemente, usando la terminologia comune.
>E' possibile pensare una matematica veramente
>costruttiva in cui tutte le funzioni di cui puoi parlare sono ricorsive.
>
>Quando dico che la dimostrazione di Cantor è costruttiva, intendo che è
>il suo scheletro ad essere costruttivo: prendi una teoria degli insiemi
>costruttiva, che parli esclusivamente di funzioni ricorsive, e la
>dimostrazione di Cantor continua a valere.
Una teoria degli insiemi in cui non esistono funzioni non ricorsive?
veramente difficile da immaginare. Riferimenti? Ciao
superpollo
essendo una dimostrazione per assurdo, implicitamente utilizza il
principio del t.e.
bye
--
Allora con pazienza dissi loro, guardate che mezzo cavolo
e' pur sempre 5cavoletti e5cavoletti*1cavolo fanno 50cavoletti
che poi sarebbero sempre 5cavoli grandi.
E loro dicevano ; Ma che cavolo dici!!
radicale.002
Implicitamente come ? Io non lo vedo ...
Enrico Gregorio
> E questo che c'entra? In ZF ci sono anche le funzioni ricorsive. Nessuno
> vieta, quando si puo', di fare in ZF dimostrazioni costruttive. Per
> esempio, si potrebbe dimostrare costruttivamente l'infinita' dei numeri
> primi. Ma quando non si puo' (come nel caso della dimostrazione diagonale
> di Cantor), c'e' poco da fare.
La classica dimostrazione di Euclide /č/ costruttiva, anche se,
per ragioni a me ignote, viene spesso presentata come una
dimostrazione per assurdo.
Dati i numeri primi p_1, p_2, p_k (distinti o no), il minimo
divisore maggiore di 1 di N = p_1 p_2 ... p_k + 1 č un primo
diverso da quelli dati.
Ciao
Enrico
superpollo
sei d'accordo che e' per assurdo? si'?
radicale.002
> > Implicitamente come ? Io non lo vedo ...
>
> sei d'accordo che e' per assurdo? si'?
No (proprio perche' non "vedo" il ricorso al t.e.)
E anche Barone Barolo, che mi pare ci capisca qualcosina
piu' di me.
superpollo
> On 6 Gen, 21:25, superpollo <superpo...@tznvy.pbz> wrote:
>
>>> Implicitamente come ? Io non lo vedo ...
>> sei d'accordo che e' per assurdo? si'?
>
> No (proprio perche' non "vedo" il ricorso al t.e.)
ecco cosa hai detto tu:
> facciamo una qualunque lista numerabile L di reali.
questa appena fatta e' la negazione della tesi "i reali sono numerabili"
> Ebbene questa ne lascia fuori alcuni, e fa vedere quali.
questa appenda detta e' la contraddizione.
> E anche Barone Barolo, che mi pare ci capisca qualcosina
> piu' di me.
se non ho letto male, lui ha precisato che e' costruttiva *in ambito di
logica non classica*
bye
Barone Barolo
>> Tu dici che la dimostrazione non è costruttiva perché compone la
>> funzione diagonale con un'altra funzione (generica, ipotetica) non
>> ricorsiva. Ovvio, visto che ZF parla di funzioni generali: grazie tante!
>
> E questo che c'entra? In ZF ci sono anche le funzioni ricorsive. Nessuno
> vieta, quando si puo', di fare in ZF dimostrazioni costruttive.
Smettiamo di utilizzare questa parola ambigua, per cortesia? Ci sono
troppe logiche c.d. "costruttive" per essere precisi. Parliamo di logica
-intuizionista-, che è la logica che ottieni togliendo alla logica
classica la reductio ad absurdum e principi ad esso equivalenti come il
tertium non datur e la legge di Peirce. E parliamo della versione
intuizionista di ZF, cioè IZF, talvolta propagandata come "teoria degli
insiemi costruttiva".
Bene, il teorema di Cantor continua a valere.
> Bene: come ho sempre sostenuto, tu non parli di cio' che si intende
> comunemente, usando la terminologia comune.
Mi sa che sostieni male. Quale sarebbe esattamente la terminologia che
uso in modo sbagliato?
> Una teoria degli insiemi in cui non esistono funzioni non ricorsive?
> veramente difficile da immaginare. Riferimenti? Ciao
Preferisco parlare di teoria dei tipi. Rispetto alla teoria degli
insiemi perdi l'estensionalità, che d'altra parte è un concetto ben poco
costruttivo.
Trovi una discussione di una variante del teorema di Cantor nella teoria
dei tipi intuizionista di Martin-Loef a pag. 61 della tesi di dottorato
di Silvio Valentini
http://www.math.unipd.it/~silvio/papers/PhDThesis/TypeTheory.pdf
mentre qui puoi trovare una dimostrazione formalizzata nella logica del
theorem prover interattivo Coq (cioè il calcolo delle costruzioni)
http://muaddibspace.blogspot.com/2009/10/cantors-diagonalization-proof-in-coq.html
Ciao
-- bb
Barone Barolo
> > Ebbene questa ne lascia fuori alcuni, e fa vedere quali.
>
> questa appenda detta e' la contraddizione.
Il fraintendimento è questo: non ogni dimostrazione che raggiunga una
contraddizione richiede il terzo escluso.
Qualcuno qui conosce la deduzione naturale?
-- bb
radicale.002
> ecco cosa hai detto tu:
>> facciamo una qualunque lista numerabile L di reali.
Si
> questa appena fatta e' la negazione della tesi "i reali sono numerabili"
Ma nemmeno per sogno. Perche' ?
Tu puoi fare una qualunque lista numerabile di razionali.
Allora i razionali di per cio stesso sarebbero non numerabili ?
>> Ebbene questa ne lascia fuori alcuni, e fa vedere quali.
> questa appenda detta e' la contraddizione.
Ma la contraddizione con cosa, visto quello che ho scritto
sopra ?
superpollo
se ragioni in quel modo, la lista numerabile L e' "solo" *una* lista
numerabile di reali, e mi pare ovvio che qualche reale le sfugga, anche
se i reali fossero numerabili. in pratica non hai dimostrato niente.
nel suo teorema, cantor invece ipotizza esattamente di fare una lista
numerabile di *tutti* i reali (una biiezione N-->R, fonte g. prodi,
analisi matematica, pag. 82), e tale ipotesi conduce a una contraddizione.
bye
Barone Barolo
> nel suo teorema, cantor invece ipotizza esattamente di fare una lista
> numerabile di *tutti* i reali (una biiezione N-->R, fonte g. prodi,
> analisi matematica, pag. 82), e tale ipotesi conduce a una contraddizione.
Vogliamo schematizzare la dimostrazione di Cantor?
"Non esiste una funzione suriettiva da un insieme A in P(A)"
Dimostrazione
La tesi � nella forma !exists f.Q(f)
quindi assumiamo exists f.Q(f) e cerchiamo di derivare l'assurdo [*]
pi� concretamente, supponiamo (ipotesi H1) che esista f : A -> P(A)
suriettiva
allora costruiamo un sottinsieme di A (assioma di separazione, ammesso
in intuitionistic-ZF)
D = { x \in A | x \notin f(x) }
Per l'ipotesi H1, f � suriettiva quindi otteniamo (proposizione H2) che
esiste d \in A tale che f(d) = D.
Allora dimostriamo (proposizione H3) d \notin f(d) = D:
supponiamo [*] d \in D : per definizione di D, dev'essere d \notin f(d)
= D, ma avevamo supposto il contrario, il che � assurdo (qed per H3).
Tuttavia da H3, sempre pre la definizione di D, otteniamo (proposizione
H4) che d \in D. Ma H3 e H4 sono contraddittorie. Qed.
I passi comunemente (ma erroneamente) considerati "per assurdo" sono
quelli contrassegnati con [*] e sono nella forma
(!I) se A |- assurdo, allora |- !A
Le vere dimostrazioni per assurdo utilizzano invece il principio opposto
(RAA) se !A |- assurdo, allora |- A
la vedete la differenza tra (!I) e (RAA)? Be', anche se non la vedete,
provate a dimostrare il terzo escluso: se assumete (RAA) ci riuscite, se
assumete (!I) no...
Quindi il T. di Cantor __NON__ richiede il terzo escluso.
Ciao.
-- bb
radicale.002
> se ragioni in quel modo, la lista numerabile L e' "solo" *una* lista
> numerabile di reali, e mi pare ovvio che qualche reale le sfugga, anche
> se i reali fossero numerabili. in pratica non hai dimostrato niente.
Non e' solo *una* lista, ma *ogni* lista numerabile.
E' quello il bello ! Almeno, io ho capito cosi' ...
Per *ogni* lista numerabile di reali, io la acchiappo e ci caccio
fuori numeri che non stanno in quella lista.
Dunque :
*ogni* possibile immaginabile concepibile lista numerabile,
non acchiappa tutti i reali !
Allora mettiamole *tutte* insieme ! Una "sotto" l' altra.
Sappiamo che e' ancora numerabile, MA MANCO QUELLA
acchiappa tutti i reali.
Dunque, Cantor dimostra DIRETTAMENTE che una lista
del genere non si puo' fare. Da cui la tesi.
Ripeto : almeno io ho capito cosi' ... Poi ... Se ho sbagliato
chiedo umilmente perdono.
radicale.002
wrote:
> Quindi il T. di Cantor __NON__ richiede il terzo escluso.
Ti credo. Ciecamente. L' intuizione mi dice CHIARAMENTE
che e' come dici tu.
Ma non potresti riscrivere tutto in Italiano ? Ti prego ... Vorrei
tanto capirla anch' io.
Barone Barolo
> Ma non potresti riscrivere tutto in Italiano ? Ti prego ... Vorrei
> tanto capirla anch' io.
Allora lascia perdere i dettagli della dimostrazione di Cantor, c'è un
concetto più generale in ballo.
Si dice comunemente che la negazione di una negazione afferma: bene, per
gli intuizionisti non è così. A e !!A non dicono la stessa cosa: infatti
!!A è un concetto più debole di A. In logica intuizionista, dimostriamo
infatti
A -> !!A
ma non è possibile dimostrare
!!A -> A
Per quale ragione? Be', vediamo come si dimostrano.
***
Dimostrazione di A -> !!A
Supponiamo che A sia vero: dobbiamo dimostrare !!A.
Per dimostrare !!A, supponiamo che !A sia vero e dimostriamo l'assurdo:
il che è banale perché abbiamo assunto sia A sia !A. QED.
Il principio che ho utilizzato dice che, per dimostrare !B, qualunque
sia la formula B, posso assumere B e derivare l'assurdo. In simboli
(!I) se B |- assurdo, allora |- !B
Ovviamente nel nostro caso, abbiamo preso B = !A.
Questo principio (!I) è accettato da TUTTI gli intuizionisti.
***
Dimostrazione di !!A -> A
Per il terzo escluso, A or !A.
Nel primo caso, A è vero, quindi "a fortiori" anche !!A -> A è vero.
Nel secondo caso, !A è vero. Dovendo dimostrare !!A -> A, supponiamo !!A
e dimostriamo A. Ma a questo punto, abbiamo per ipotesi !A e !!A, che è
una contraddizione.
QED.
In questa dimostrazione si usa il terzo escluso. Non c'è verso di
dimostrare la tesi sostituendo al terzo escluso il principio (!I) della
dimostrazione precedente!
***
Per concludere, il teorema di Cantor si comporta come la prima di queste
due semplici dimostrazioni: utilizza il principio (!I) e non il terzo
escluso.
-- bb
radicale 001
wrote:
> Allora lascia perdere i dettagli della dimostrazione di Cantor, c' un
> concetto pi generale in ballo.
> Si dice comunemente che la negazione di una negazione afferma: bene, per
> gli intuizionisti non cos . A e !!A non dicono la stessa cosa: infatti
> !!A un concetto pi debole di A. In logica intuizionista, dimostriamo
> infatti
> A -> !!A
> ma non possibile dimostrare
> !!A -> A
> Per quale ragione? Be', vediamo come si dimostrano.
> ***
> Dimostrazione di A -> !!A
> Supponiamo che A sia vero: dobbiamo dimostrare !!A.
> Per dimostrare !!A, supponiamo che !A sia vero e dimostriamo l'assurdo:
> il che banale perch abbiamo assunto sia A sia !A. QED.
> Il principio che ho utilizzato dice che, per dimostrare !B, qualunque
> sia la formula B, posso assumere B e derivare l'assurdo. In simboli
> (!I) se B |- assurdo, allora |- !B
> Ovviamente nel nostro caso, abbiamo preso B = !A.
> Questo principio (!I) accettato da TUTTI gli intuizionisti.
Ho capito alla perfezione. Solo :
ma non e' un po' ... "Subdolo" questo principio ? Mi spiego :
(!I) se B |- assurdo, allora |- !B
Ora,
a - prescindere- (sottolineo) dal caso specifico A -> !!A,
puo' ben essere (correggimi se dico una cacchiata) che la
derivazione "B |- assurdo" sia possibile farla a sua volta solo
utilizzando il principio del terzo escluso ! Dunque non
bisognerebbe precisare :
"B |- assurdo", ok, ma a patto che nella |- non si utilizzi il t.e. ?
Non so se mi sono spiegato.
> ***
> Dimostrazione di !!A -> A
> Per il terzo escluso, A or !A.
> Nel primo caso, A vero, quindi "a fortiori" anche !!A -> A vero.
> Nel secondo caso, !A vero. Dovendo dimostrare !!A -> A, supponiamo !!A
> e dimostriamo A. Ma a questo punto, abbiamo per ipotesi !A e !!A, che
> una contraddizione.
> QED.
> In questa dimostrazione si usa il terzo escluso. Non c' verso di
> dimostrare la tesi sostituendo al terzo escluso il principio (!I) della
> dimostrazione precedente!
... E siccome di quel principio non si fidano, il resto vien da se.
Ho capito.
> ***
> Per concludere, il teorema di Cantor si comporta come la prima di queste
> due semplici dimostrazioni: utilizza il principio (!I) e non il terzo
> escluso.
A = "esiste una lista numerabile di tutti i reali"
Col metodo diagonale dimostro !A.
A |- A e !A , quindi ... !A ?
Non riesco a riportare la struttura A -> !!A alla dimostrazione di
Cantor !
radicale 001
> Non riesco a riportare la struttura A -> !!A alla dimostrazione di
> Cantor !
Ops ... Perdonami, dimenticavo :
grazie di cuore della CHIARISSIMA spiegazione.
LordBeotian
wrote:
> Si dice comunemente che la negazione di una negazione afferma: bene, per
> gli intuizionisti non cos . A e !!A non dicono la stessa cosa: infatti
> !!A un concetto pi debole di A. In logica intuizionista, dimostriamo
> infatti
>
> A -> !!A
>
> ma non possibile dimostrare
>
> !!A -> A
>
> Per quale ragione? Be', vediamo come si dimostrano.
Un attimo: lo vuoi dimostrare con quali assiomi?
superpollo
penso quelli della logica "debole" (intuizionista) no?
Barone Barolo
> Un attimo: lo vuoi dimostrare con quali assiomi?
Diciamo un sistema assiomatico alla Hilbert per logica classica o
intuizionista?
-- bb
superpollo
hai sbagliato e ti perdono. il fatto e' che tu fraintendi il
ragionamento cantoriano.
la questione e' semplice: sono andato a rileggere un po' di letteratura
originale (del 1874 e del 1891). ebbene in tutte le dimostrazioni di non
numerabilita', cantor assume l'esistenza di una corrispondenza
*biiettiva*, e non di una semplice corrispondenza *iniettiva* come fai tu.
superpollo
o per meglio dire: nella nota del 1891, cantor dimostra si' che per
*ogni* lista numerabile di sequenze binarie infinite e' possibile
generare una sequenza binaria che non viene elencata... ma precisa anche
che (in riferimanto alla nota del 1874) tale ragionamento si puo'
applicare alla non numerabilita' dei reali (in un dato intervallo), e
poiche' il riferimento e' chiaro e' ovvio che cantor parlava della lista
di *tutti* i reali.
preciso pero' che li ho letti in tedesco, e io il tedesco, nsomma...
pero' cito lolli che invece il tedesco lo capisce assai: "[nel 1874]
cantor parte per dimostrare l'esistenza della corrispondenza [biunivoca
N-->R] e poi la nonesistenza ne consegue per assurdo"
sottolineo: *per assurdo*
LordBeotian
wrote:
> > Un attimo: lo vuoi dimostrare con quali assiomi?
>
> Diciamo un sistema assiomatico alla Hilbert per logica classica o
> intuizionista?
Ma un sistema assiomatico per la logica classica potrebbe benissimo
avere il terzo escluso come assioma, o comunque gli assiomi si possono
scegliere il mille modi equivalenti che danno luogo a diverse
dimostrazioni per il terzo escluso.
Barone Barolo
>> Diciamo un sistema assiomatico alla Hilbert per logica classica o
>> intuizionista?
>
> Ma un sistema assiomatico per la logica classica potrebbe benissimo
> avere il terzo escluso come assioma, o comunque gli assiomi si possono
> scegliere il mille modi equivalenti che danno luogo a diverse
> dimostrazioni per il terzo escluso.
Schiacciamo reset per un secondo. Lasciamo perdere i sistemi alla
Hilbert perché non ne ricordo uno per la logica intuizionista. Prendiamo
la deduzione naturale, che per ogni connettivo logico presenta regole di
introduzione ed eliminazione.
Le regole che riguardano congiunzione disgiunzione ed implicazione sono
le stesse per logica classica e intuizionista:
(and I) se (Gamma |- A) e (Gamma |- B) allora (Gamma |- A and B)
(and E.1) se (Gamma |- A and B) allora (Gamma |- A)
(and E.2) se (Gamma |- A and B) allora (Gamma |- B)
(or I.1) se (Gamma |- A) allora (Gamma |- A or B)
(or I.2) se (Gamma |- B) allora (Gamma |- A or B)
(or E) se (Gamma |- A or B), (Gamma, A |- C) e (Gamma, B |- C),
allora (Gamma |- C)
(-> I) se (Gamma, A |- B) allora (Gamma |- A -> B)
(-> E) se (Gamma |- A -> B) e (Gamma |- A) allora (Gamma |- B)
(modus ponens)
Per quanto riguarda negazione e assurdo, la logica classica ammette le
seguenti regole di deduzione naturale:
(! I) se (Gamma, A |- assurdo) allora (Gamma |- !A)
(! E) se (Gamma |- A) e (Gamma |- !A) allora (Gamma |- assurdo)
(RAA) se (Gamma, !A |- assurdo) allora (Gamma |- A)
(assurdo E) se (Gamma |- assurdo) allora (Gamma |- A)
L'assurdo non ha regole di introduzione, anche se (! E) talvolta è
considerata (assurdo I). La regola di eliminazione dell'assurdo è anche
nota come "ex falso quodlibet". La regola (RAA) (reductio ad absurdum)
sfugge allo schema introduzione/eliminazione ma è necessaria per la
completezza del sistema.
La domanda è: quali di queste ultime quattro regole sono accettate dai
costruttivisti, e in particolare dagli intuizionisti?
-- bb
Barone Barolo
> (! I) se (Gamma, A |- assurdo) allora (Gamma |- !A)
> (! E) se (Gamma |- A) e (Gamma |- !A) allora (Gamma |- assurdo)
> (RAA) se (Gamma, !A |- assurdo) allora (Gamma |- A)
> (assurdo E) se (Gamma |- assurdo) allora (Gamma |- A)
>
> costruttivisti, e in particolare dagli intuizionisti?
Andiamo su, mi pare di parlare arabo :-(
Non � una domanda trabocchetto, voglio veramente capire come la pensate
voi, e confrontarlo con ci� che dicono i costruttivisti.
-- bb
superpollo
> Il 07/01/2011 14:20, Barone Barolo ha scritto:
>> (! I) se (Gamma, A |- assurdo) allora (Gamma |- !A)
>> (! E) se (Gamma |- A) e (Gamma |- !A) allora (Gamma |- assurdo)
>> (RAA) se (Gamma, !A |- assurdo) allora (Gamma |- A)
>> (assurdo E) se (Gamma |- assurdo) allora (Gamma |- A)
>>
>> costruttivisti, e in particolare dagli intuizionisti?
>
> Andiamo su, mi pare di parlare arabo :-(
> voi, e confrontarlo con ciň che dicono i costruttivisti.
preciso nuovamente che non sono un rigido costruttivista (ne so troppo
poco di logica per fare muro). la sola cosa e' che una dimostrazione che
mi illustra un *algoritmo* che costruisce eplicitamente un oggetto mi
soddisfa molto di piu' di una che (usando ad esempio RAA) afferma
l'esistenza di un oggetto.
bye
--
il mondo non sa neanche perchč mezzo*mezzo sia 1/4
1/4 di cosa ?? Almeno diteglielo di cosa ? di una terza cosa ??
Ma allora la terxa cosa farebbe 1*1 = 10. O no ??
superpollo
> Barone Barolo ha scritto:
>> Il 07/01/2011 14:20, Barone Barolo ha scritto:
>>> (! I) se (Gamma, A |- assurdo) allora (Gamma |- !A)
>>> (! E) se (Gamma |- A) e (Gamma |- !A) allora (Gamma |- assurdo)
>>> (RAA) se (Gamma, !A |- assurdo) allora (Gamma |- A)
>>> (assurdo E) se (Gamma |- assurdo) allora (Gamma |- A)
>>>
>>> La domanda č: quali di queste ultime quattro regole sono accettate dai
>>> costruttivisti, e in particolare dagli intuizionisti?
>>
>> Andiamo su, mi pare di parlare arabo :-(
>> Non č una domanda trabocchetto, voglio veramente capire come la
>> pensate voi, e confrontarlo con ciň che dicono i costruttivisti.
>
> preciso nuovamente che non sono un rigido costruttivista (ne so troppo
> poco di logica per fare muro). la sola cosa e' che una dimostrazione che
> mi illustra un *algoritmo* che costruisce eplicitamente un oggetto mi
> soddisfa molto di piu' di una che (usando ad esempio RAA) afferma
> l'esistenza di un oggetto.
e in generale sono molto perplesso di fronte a quelle dimostrazioni non
costruttive che aggiungono condizioni allucinanti... tipo: esiste un
numero n che soddisfa P, altrimenti si ha un assurdo, ma questo n
dev'essere maggiore del numero di elettroni che riempirebbero
compattamente l'universo conosciuto.
e' la solita storia della figa: "vai in quel villaggio valtour, e' pieno
di figa", solo che poi non conta quanta figa c'e' nel villaggio, conta
solo quanta ne tocchi proprio tu...
radicale 001
> ma non e' un po' ... "Subdolo" questo principio ? Mi spiego :
> (!I) se B |- assurdo, allora |- !B
> Ora,
> a - prescindere- (sottolineo) dal caso specifico A -> !!A,
> puo' ben essere (correggimi se dico una cacchiata) che la
> derivazione "B |- assurdo" sia possibile farla a sua volta solo
> utilizzando il principio del terzo escluso ! Dunque non
> bisognerebbe precisare :
> "B |- assurdo", ok, ma a patto che nella |- non si utilizzi il t.e. ?
> Non so se mi sono spiegato.
Non mi dici nulla ? Detto qualcosa che non va' ?
> Non riesco a riportare la struttura A -> !!A alla dimostrazione di
> Cantor !
E nemmeno qui ?
Barone Barolo
>> ma non e' un po' ... "Subdolo" questo principio ? Mi spiego :
>> (!I) se B |- assurdo, allora |- !B
>
>> Ora,
>> a - prescindere- (sottolineo) dal caso specifico A -> !!A,
>> puo' ben essere (correggimi se dico una cacchiata) che la
>> derivazione "B |- assurdo" sia possibile farla a sua volta solo
>> utilizzando il principio del terzo escluso !
Sě ma se il terzo escluso non ce l'hai, quella dimostrazione non la fai
e tanti saluti.
Una volta che hai fissato il tuo sistema deduttivo e la tua teoria, e il
terzo escluso non ne fa parte, non c'č nient'altro da specificare.
>> Non riesco a riportare la struttura A -> !!A alla dimostrazione di
>> Cantor !
La dimostrazione di Cantor č dello stesso tipo della dimostrazione di A
-> !!A nel senso che entrambe usano (!I), ma non usano il terzo escluso.
-- bb
Barone Barolo
>>> (! I) se (Gamma, A |- assurdo) allora (Gamma |- !A)
>>> (! E) se (Gamma |- A) e (Gamma |- !A) allora (Gamma |- assurdo)
>>> (RAA) se (Gamma, !A |- assurdo) allora (Gamma |- A)
>>> (assurdo E) se (Gamma |- assurdo) allora (Gamma |- A)
>
> poco di logica per fare muro). la sola cosa e' che una dimostrazione che
> mi illustra un *algoritmo* che costruisce eplicitamente un oggetto mi
> soddisfa molto di piu' di una che (usando ad esempio RAA) afferma
> l'esistenza di un oggetto.
Infatti (RAA) � rifiutato da tutti i costruttivisti.
Rimangono le altre tre regole: secondo voi sono costruttive o no?
-- bb
Winston Smith
> Immagino che ci si possa scrivere un libro, ma il succo l'abbiamo già detto.
> Non è che i costruttivisti non credano che il terzo escluso sia un
> principio VERO.
> Piuttosto pensano che la matematica basata sulla logica classica non sia
> una buona matematica perché si occupa di ciò che è vero, invece dovrebbe
> preoccuparsi di ciò che è ottenibile in modo effettivo.
Brouwer si starà rivoltando nella tomba :-)
Lui pensava davvero che il terzo escluso fosse un principio fallace.
Più precisamente, secondo lui una qualunque affermazione che non si era
in grado nè di dimostrare nè di refutare (tipo la congettura di Goldbach
per intenderci) era da considerarsi nè vera nè falsa.
Il modo convinto in cui propagandava le sue idee gli attirò l'ostilità
di gran parte dei suoi contemporanei (primo tra tutti Hilbert, e avere
contro Hilbert non era un problema da poco).
Fortunatamente i costruttivisti di oggi sono meno fondamentalisti: pochi
sostengono seriamente che la logica classica sia "sbagliata", e la
posizione prevalente è quella espressa sopra da Barone Barolo.
--
Saluti,
ws
Barone Barolo
> Brouwer si starà rivoltando nella tomba :-)
LOL.
Grazie per questi dettagli che non conoscevo :-)
-- bb
radicale 001
wrote:
> >> Ora,
> >> a - prescindere- (sottolineo) dal caso specifico A -> !!A,
> >> puo' ben essere (correggimi se dico una cacchiata) che la
> >> derivazione "B |- assurdo" sia possibile farla a sua volta solo
> >> utilizzando il principio del terzo escluso !
> Sì ma se il terzo escluso non ce l'hai, quella dimostrazione non la fai
> e tanti saluti.
> Una volta che hai fissato il tuo sistema deduttivo e la tua teoria, e il
> terzo escluso non ne fa parte, non c'è nient'altro da specificare.
Quindi appunto : il principio si, ma "al netto" del terzo escluso.
> >> Non riesco a riportare la struttura A -> !!A alla dimostrazione di
> >> Cantor !
> La dimostrazione di Cantor è dello stesso tipo della dimostrazione di A
> -> !!A nel senso che entrambe usano (!I), ma non usano il terzo escluso.
Si questo l' avevo capito. Ti chiedevo *come* riportare la
dimostrazione
di Cantor in quello schema. Non so se ...
Barone Barolo
>> La dimostrazione di Cantor è dello stesso tipo della dimostrazione di A
>> -> !!A nel senso che entrambe usano (!I), ma non usano il terzo escluso.
>
> Si questo l' avevo capito. Ti chiedevo *come* riportare la
> dimostrazione
> di Cantor in quello schema. Non so se ...
In che senso? Ho già reso esplicito l'utilizzo di (!I).
-- bb
radicale 001
wrote:
> Il 08/01/2011 01:22, radicale 001 ha scritto:
>
> >> -> !!A nel senso che entrambe usano (!I), ma non usano il terzo escluso.
>
> > Si questo l' avevo capito. Ti chiedevo *come* riportare la
> > dimostrazione
> > di Cantor in quello schema. Non so se ...
>
Si hai ragione scusa, sono io che non so spiegarmi ...
Volevo dire :
io conosco la dimostrazione di Cantor, diciamo, in "Italiano".
Mi potresti far vedere come si riporta, come si "traduce"
in modo da metterla esplicitamente nella forma A -> !!A ?
Barone Barolo
> Mi potresti far vedere come si riporta, come si "traduce"
> in modo da metterla esplicitamente nella forma A -> !!A ?
Perché dovresti fare una cosa del genere?
-- bb
radicale 001
wrote:
> Il 08/01/2011 01:41, radicale 001 ha scritto:
>
> > Mi potresti far vedere come si riporta, come si "traduce"
> > in modo da metterla esplicitamente nella forma A -> !!A ?
>
?!?
Come perche ? :-)
Tu m' hai detto che e' di quel tipo ! Allora mi sarebbe piaciuto
riuscire a metterla esplicitamente in quella forma.
Cioe' : che c'e' al posto di A ? Da dove esce il non non A ?
Barone Barolo
> ?!?
> Come perche ? :-)
>
> Tu m' hai detto che e' di quel tipo !
Certo, nel senso che tutte e due usano (! I) e nessuna delle due usa il
terzo escluso. Non ho mai detto che la dimostrazione di Cantor usa A -> !!A.
-- bb
radicale 001
wrote:
Ahhhh !!! Scusa ! Credevo che intendessi che proprio fosse stata
del tipo A -> !!A. Ecco perche' non ci riuscivo a riportarla in
quella forma :-))
radicale 001
> Oppure ?
Vedi titolo.
Per gentile spiegazione di barone barolo
superpollo
vorrei essere molto preciso:
(1) lo "spirito costruttivista" *diffida* (piu' che "rifiutare") del
principio del terzo escluso E ANCHE della doppia negazione (e *di
conseguenza* delle dimostrazioni per assurdo);
(2) ma suddetta riserva si applica *solo* al caso di *insiemi infiniti*;
nel caso finito non c'e' nessuna riserva alr riguardo.
bye
--
>>> Va bene, ma cosa serve ?
>> Converrai che chiesto da te è una osservazione quanto meno
>> bizzarra. ;-)
> Vuoi dire che io faccio cose che non servirebbero ??
Barone Barolo
> del principio del terzo escluso E ANCHE della doppia negazione
Hmm in quale forma?
-- bb
superpollo
> Il 08/01/2011 18:37, superpollo ha scritto:
>> del principio del terzo escluso E ANCHE della doppia negazione
>
> Hmm in quale forma?
!!A --> A
--
>>> Va bene, ma cosa serve ?
>> Converrai che chiesto da te � una osservazione quanto meno
Enrico Gregorio
> vorrei essere molto preciso:
>
> (1) lo "spirito costruttivista" *diffida* (piu' che "rifiutare") del
> principio del terzo escluso E ANCHE della doppia negazione (e *di
> conseguenza* delle dimostrazioni per assurdo);
Sbagliato. Nessun matematico, nemmeno gli intuizionisti più cattivi,
rifiuta le dimostrazioni per assurdo. Ci mancherebbe anche questa.
Una dimostrazione per assurdo è un ragionamento della forma
da "A -> (B e non B)" si deduce "non A"
Non c'è nulla qui che implichi l'uso del terzo escluso.
Ciao
Enrico
superpollo
> superpollo <super...@tznvy.pbz> scrive:
>
>> vorrei essere molto preciso:
>>
>> (1) lo "spirito costruttivista" *diffida* (piu' che "rifiutare") del
>> principio del terzo escluso E ANCHE della doppia negazione (e *di
>> conseguenza* delle dimostrazioni per assurdo);
>
> Sbagliato. Nessun matematico, nemmeno gli intuizionisti più cattivi,
> rifiuta le dimostrazioni per assurdo. Ci mancherebbe anche questa.
infatto ho specificato "diffida", non "rifiuta", almeno, questa e' la
mia personale posizione, che a mio avviso e' il contenuto concreto dello
spirito costruttivista: accetto (con riserva) una dimostrazione per
assurdo, che di solito e' non costruttiva; per alcuni la storia finisce
li'; per me no, la diostrazione e' provvisoria: io continuo a cercare un
algoritmo per costruire l'oggetto di cui e' stata dimostrata
l'esistenza; trovato l'algoritmo, sciolgo la riserva, in caso contrario
mantengo la riserva.
Barone Barolo
>>> del principio del terzo escluso E ANCHE della doppia negazione
>>
>> Hmm in quale forma?
>
> !!A --> A
Esatto. Comunque � equivalente al terzo escluso.
-- bb
Barone Barolo
> Sbagliato. Nessun matematico, nemmeno gli intuizionisti più cattivi,
> rifiuta le dimostrazioni per assurdo. Ci mancherebbe anche questa.
> Una dimostrazione per assurdo è un ragionamento della forma
>
> da "A -> (B e non B)" si deduce "non A"
>
> Non c'è nulla qui che implichi l'uso del terzo escluso.
Infatti. Sospettavo che l'equivoco fosse questo.
Nota che in teoria dei tipi "non A" è considerato un abbreviazione
sintattiva per "A -> assurdo", quindi quello di cui sopra non sarebbe
neanche un passo di deduzione...
-- bb
El Filibustero
>Brouwer si starà rivoltando nella tomba :-)
>Lui pensava davvero che il terzo escluso fosse un principio fallace.
>Più precisamente, secondo lui una qualunque affermazione che non si era
>in grado nè di dimostrare nè di refutare (tipo la congettura di Goldbach
>per intenderci) era da considerarsi nè vera nè falsa.
Ma chi ha *dimostrato* che la congettura di Goldbach e' indimostrabile e
irrefutabile? Nessuno. Potrebbe essere dimostrabile, magari con una
dimostrazione in PA, ineccepibile anche per l'intuizionista piu'
estremista. Non bisogna confondere "difficile da dimostrare o refutare per
un matematico" con "indecidibile". Ciao
Barone Barolo
> Ma chi ha *dimostrato* che la congettura di Goldbach e' indimostrabile e
> irrefutabile? Nessuno. Potrebbe essere dimostrabile, magari con una
> dimostrazione in PA, ineccepibile anche per l'intuizionista piu'
> estremista.
In HA, vuoi dire.
A parte questo, ti è chiara la conclusione a cui siamo giunti nel
thread, la condividi e, se no, su cosa non sei d'accordo?
Ciao
-- bb
El Filibustero
>> Ma chi ha *dimostrato* che la congettura di Goldbach e' indimostrabile e
>> irrefutabile? Nessuno. Potrebbe essere dimostrabile, magari con una
>> dimostrazione in PA, ineccepibile anche per l'intuizionista piu'
>> estremista.
>
>In HA, vuoi dire.
nel sistema che ti pare.
>A parte questo, ti è chiara la conclusione a cui siamo giunti nel
>thread
non ho seguito il thread. Ciao