Date: Fri, 13 Jun 2003 12:13:49 +0100 (BST) From: Franco Raimondi To: Leo Sergio Liberti > Si`, infatti. Ci riuniamo 1-2 volte al mese e discutiamo argomenti di > matematica che ci piacciono. Adesso stiamo parlando di Goedel gia` da un > po'. I progressi (molto dubbi...) li vedi a First order logic (FOL) is complete (primo teorema di Godel). A parte come si dimostra il teorema, l'importante e' capire cosa e' un modello e cosa e' una dimostrazione. La completezza ti dice che: "vero in tutti i modelli" iff "si puo' ottenere partendo dagli assiomi i.e. e' un teorema i.e. e' dimostrabile" [FOL non e' decidable, ma questa e' un'altra storia. Decidable = esiste un metodo per dire se una cosa e' un teorema o meno.] ********* Teorema di _incompletezza_ di Godel: - axiomatic set theory ZFC and formal arithmetic PA _non_ sono assiomatizzabili con first ordel logic. Ti servono infiniti assiomi, oppure ti serve un linguaggio piu' complicato (che si puo' chiamare second order logic). Il problema e' introdurre l'induzione. In PA per "parlare" di induzione dici "se una proprieta' e' vera per 0 e, se e' vera per n allora e' vera anche per n+1, allora P e' vera sempre." In FOL non puoi quantificare su Proprieta', ma solo su variabili. \def\implies{\rightarrow} \forall P, [P(0) \land ( P(n) \implies P(n+1))] \implies [\forall x P(x)] _non_ e' una formula di FOL. Per uscirne, devi scrivere tante regole quante sono le proprieta' in FOL, ma allora la logica non e' finitely axiomatizable (hai infiniti assiomi, non e' quello che vuoi). Oppure consenti di quantificare sulle proprieta', e hai Second Order Logic (quello che tu chiami "first-order logic with proper axioms"). Il teorema di incompletezza dice: SOL non e' complete. Ovvero puoi trovare una roba che e' vera in tutti i modelli di SOL ma non puoi costruire una dimostrazione partendo dagli assiomi. Guarda un po' anche qui sotto Godel's theorems.(una roba a caso trovata ora): http://www.earlham.edu/~peters/courses/logsys/glossary.htm#g Bai, F