Newsgroup: it.cultura.filosofia
Titolo: Calcolo e pertinenza

Salve a tutti nuovamente,
visto che mi siete stati di grande aiuto nella precedente questione,
ci riprovo.
(Perdonatemi le imprecisioni e correggetemi quando volete)
Ho sentito che dovrebbero esistere algoritmi in grado di effettuare 
dimostrazioni nel linguaggio della logica predicativa del primo
ordine.
Se e' questo vero, il mio problema e' il seguente: poiché il calcolo
logico, che io sappia, fornisce solo schemi e regole che stabiliscono
se una data proposizione e' conseguenza logica di un'altra o meno , e
poiché credo che non ogni conseguenza logica sia equivalentemente
"utile" nel processo dimostrativo, esistono dei criteri per
"individuare" proposizioni "pertinenti" che permettano di concludere
la dimostrazione senza "generare" infinite proposizioni intermedie?
grazie
alef

Esiste un metodo, detto "del controesempio", e che si sviluppa nella 
innanzi tutto grazie per la risposta...
mi sapresti indicare anche qualche riferimento bibliografico, se ne
esistono, o eventualmente qualche esempio ?
ciao
alef
** Articolo inviato dal news server gratuito 
www.x-privat.org
 **

 la dimostrazione?
Credo di poter rispondere cosi':
Una proposizione e' davvero non pertinente solo se il suo contrario
non e' in contraddizione con la tesi. Ma dimostrare questo non e' piu'
semplice che dimostrare la tesi stessa. Quindi, in generale, la
risposta e' no. Cio' non toglie che si possano usare delle euristiche:
ad esempio, proposizioni troppo lunghe probabilmente non sono utili
(difficilmente in una dimostrazione mi serve affermare che per ogni X
esiste un Y tale che per ogni Z esiste un... e cosi' via per tre
pagine). Se pero' non ottengo risultati con questi metodi euristici
bisognera' riprendere in considerazione i rami abbandonati...
Spero di essere stato utile.
Ciao


** Free nntp server at 
www.x-privat.org
 **

Spero di essere stato utile.
certamente.
ciao
alef


 ha scritto nel messaggio
news:3ecba21a$1...@x-privat.org...


 i rami abbandonati delle serie di proposizioni consequenziali?
Esatto, e ricominciare ad esplorarli in un qualche ordine, scelto,
di nuovo, euristicamente.

 metodo anche i teoremi dell'aritmetica e dell'analisi, ecc. ?
Calma... salendo di formalismo, ci sono dei risultati di incompletezza
che affermano non solo che ci sono proposizioni indimostrabili,
ma anche proposizioni per le quali non e' possibile dimostrare se siano
dimostrabili o meno. Cercare non solo di dimostrare tutto, ma addirittura
di dimostrare tutto usando un solo metodo, e' battaglia persa in
partenza.

numerose partite giocate in passato.
Entro solo nel merito dell'esempio: non e' affatto cosi. Ogni pezzo
lasciato in presa induce lo scacchista avversario a valutare
attentamente se e' stato lasciato in presa per calcolo o per svista
(tanto piu' improbabile quanto piu' si sale in punti-capacita'). Ergo
la cattura va valutata, non puo' essere euristica ("mi butto") nel
modo che dici. C'e' sempre un setacciamento delle possibili
continuazioni di gioco a seguito della cattura (fin dove ovviamente e'
possibile arrivare). Non e' sufficiente - perche' aumentino le
probabilita' di vittoria - riuscire a "catturare i pezzi avversari
principali"; e' necessario aggiungere: "se l'avversario non puo'
impedirne la cattura" (scambio sbilanciato).
LG

 impedirne la cattura" (scambio sbilanciato).
Ma va la'... lo so anch'io che se giocassi semplicemente cercando di
prendere i pezzi avversari con gli scacchi farei ben poca strada,
ma l'esempio resta pertinente e anzi la tua osservazione mi permette
di portarlo piu' avanti.
I motivi per cui negli scacchi puo' venire scelta una euristica cosi'
grossolana come quella del mio esempio sono due:
1) Non sai giocare meglio di cosi'
2) Euristiche piu' raffinate richiederebbero troppo tempo per essere
applicate (e la tua bandierina sta per cadere, o qualcosa di simile)
Nella dimostrazione automatica dei teoremi si danno esattamente le
stesse situazioni, ed entrambe aprono il campo ad interessanti studi.
In particolare la seconda apre tutto il capitolo della complessita'
computazionale e giustifica il fatto che gli scacchi rimangono un
gioco "interessante" nonostante le partite giocabili siano finite e
(quindi) enumerabili, quanto quelle del tic-tac-toe.
Chissa' se in un remoto futuro i bambini si insegneranno l'un l'altro
come non perdere a scacchi, come oggi fanno col tic-tac-toe...

In quello che segue cerco di sintetizzare alcuni punti per verificare
se ho capito qualcosa. Non hanno l'interrogativo, ma e' come se ce
l'avessero. Per cui vi chiederei di indicarmi dove sono errati o non
sufficientemente chiari. 
La mia questione iniziale riguardava la possibilita' o meno di
dimostrare "automaticamente" una proposizione, usando il calcolo
logico |-. Cercando di chiarirmi il senso della domanda, ho capito
che:
con proposizione, posso intendere almeno:
1) una proposizione nel senso della logica enunciativa o della logica
predicativa, ossia una proposizione dell'algebra;
2) una proposizione dell'aritmetica, dell'analisi, ...;
3) una proposizione di un "metalinguaggio" delle proposizioni tipo 1)
(ad esempio il linguaggio utilizzato per esprimere l'equivalenza tra
|= e |-)
4) una proposizione di un metalinguaggio delle proposizioni tipo 2)
5) di qualunque tipo sia la proposizione che esamino, per essere
dimostrabile, deve (almeno) avere la forma "A->B". Deve avere cioe'
una forma "relazionale", nel senso che la sua (eventuale)
dimostrazione non comporta una verita' assoluta di A o B, ma una
"validita' relazionale"
6) Per quanto riguarda il calcolo logico, assumo di applicare sempre
lo stesso, qualunque sia il tipo di proposizione che sto considerando,
purché sia anche di tipo 5) (nel caso in cui cambiassi le regole del
calcolo, i cambiamenti varrebbero per tutti i tipi).
7) Ogni proposizione calcolabile e' una tautologia, ossia e' valida
(non, vera) a prescindere dalle sue possibili interpretazioni (lascio
da parte il fatto che non so formalizzare il concetto di
interpretazione...).
8) la proposizioni di tipo 1) sono tutte tautologie e ciascuna e'
calcolabile automaticamente (in un numero finito di passi)
9) alcune (non tutte) le proposizioni di tipo 2) sono calcolabili, e
per fare questo occorre definire un insieme di assiomi per
"caratterizzare" tale tipo di proposizioni. Tali specifici assiomi non
hanno la forma relazionale dei teoremi e pertanto non sono
"calcolabili" ne' logicamente validi.
10) alcune proposizioni di tipo 2) non sono calcolabili
Vi ringrazio per la pazienza,
alefalef0 wrote:



 calcolabile automaticamente (in un numero finito di passi)
Cosa cosa? Non mi sembra proprio; questa da dove ti e' uscita?

Cosa cosa? Non mi sembra proprio; questa da dove ti e' uscita?
Si', detta cosi' e' una vera fesseria.
per esempio 
A ^ -A 
e' una proposizione di tipo 1), _ben formata_, e non e' evidentemente
una tautologia, anzi e' una contraddizione!
Pero', dato un insieme P di proposizioni, l'insieme di tutte le sue 
conseguenze logiche sia C(P) (l'insieme C(P) mi pare venga anche
chiamato _teoria_di_P). Se C(P) e' completo, allora mi sembra che
_ogni sua proposizione e' calcolabile (in un numero finito di passi)_.
Per esempio l'algebra, non e' una teoria di questo tipo?
E le proposizioni dell'algebra (leggi di De Morgan,
commutativita',associativita', leggi dell'implicazione, ...) non sono
tautologie? 
Come mi e' stato fatto notare da Cosimo, una proposizione che e'
conseguenza logica di un'altra, forma con essa una tautologia.
Per esempio, P -> Q e' conseguenza logica di P <-> Q, ma P -> Q non e'
una tautologia. Tuttavia P<->Q -> P->Q e' una tautologia (mi pare sia
anche una delle leggi dell'implicazione).
Se questo e' vero, allora mi chiedo:
esiete un metodo automatico per generare tutte le tautologie di una
teoria? 
Se no, perche'? 
Se si, una volta generatele, esiste un criterio per stabilire quali
sono "significative"?
Ti ringrazio anche per avermi fatto notare che non e' sufficiente che
una proposizione sia calcolabile perche' sia una tautologia...
 
Per il punto 5) ci devo ripensare...
grazie ancora e ciao


 Se no, perche'? 
Conosci il teorema di Godel ? E' molto famoso, puoi trovarlo
facilmente con spiegazioni e commenti migliori di quelli che potrei
fornirti io, e credo possa rispondere a diverse tue domande.
Da un punto di vista piu' prettamente computazionale ti consiglio
invece di cercare una trattazione delle cosiddette "macchine di
Turing", che personalmente trovo piu' semplici da capire, mentre la
"tesi di Curch", che e' comunemente accettata anche se non dimostrata
e probabilmente non dimostrabile, stabilisce un'equivalenza tra i
risultati di Godel e quelli di Turing.
Aprire qui questi vasi di Pandora mi sembra fuori luogo...
Buon divertimento !!
Neo

Dopotutto è una forma della riduzione all'assurdo.
