Logica Matematica 6r2s65

Logica matematica La logica matematica è il settore della matematica che studia i sistemi formali dal punto di vista del modo di codificare i concetti intuitivi della dimostrazione e di computazione come parte dei fondamenti della matematica.

re a un programma compilatore perché la trascriva come una sequenza di istruzioni per il computer), sia i suoi atteggiamenti semantici (costruire specifici modelli o interi insiemi di stringhe, nella teoria dei modelli).

Alcune pubblicazioni determinanti sono state la Essa si occupa delle parti della logica che possono essere Begriffsschrift (Notazione dei concetti) di Gottlob Frege modellate matematicamente. e i Principia Mathematica di Bertrand Russell. Altri termini utilizzati spesso nel ato sono logica simbolica (termine contrapposto a logica filosofica) e metamatematica, termine che ora si applica più specificamente a taluni aspetti della teoria della dimostrazione.

1

2 Argomenti della logica matematica Tra le aree principali della logica matematica vi sono la teoria dei modelli, la teoria della dimostrazione e la teoria della ricorsione. A queste talora viene aggiunta anche la Teoria degli insiemi. Molte sono le sovrapposizioni con l'informatica teorica, fin dai lavori dei pionieri di questa disciplina, come Alan Turing e Alonzo Church, che erano matematici e logici.

Storia

Logica matematica è il nome assegnato da Giuseppe Peano a quella che era nota anche come logica simbolica o anche formale. In buona sostanza è ancora la logica di Aristotele, ma viene scritta nei termini dell'algebra astratta e della combinatoria. Lo studio della semantica dei linguaggi di programmaDei tentativi di trattare le operazioni delle logica for- zione è derivato dalla teoria dei modelli, come è accaduto male con modalità simboliche o algebriche furono effet- alla verifica dei programmi, in particolare alla verifica dei tuati da alcuni dei matematici con più spiccate attitudi- modelli. ni filosofiche, come Gottfried Leibniz e Johann Heinrich L'isomorfismo di Curry-Howard tra dimostrazioni e proLambert; i loro sforzi, però, rimasero quasi sconosciu- grammi si collega alla teoria della dimostrazione; per queti e isolati. Furono George Boole e il suo continuatore, ste questioni sono significative anche la logica intuizioniAugustus De Morgan, che, intorno alla metà del XIX se- sta e la logica lineare. Calcoli come il lambda calcolo e colo, proposero, per il trattamento della logica, alcune la logica combinatoria oggi sono studiati principalmente modalità matematiche sistematiche (naturalmente di na- come linguaggi di programmazione idealizzati. tura non-quantitativa). In tal modo la dottrina tradizionale, aristotelica, della logica, veniva riformata e comple- Nel senso speculare inoltre l'informatica contribuisce altata; in questo modo, si sviluppava anche uno strumen- la logica sviluppando strumenti per la verifica automatito adeguato per l'indagine dei concetti fondamentali del- ca delle dimostrazioni e anche per la individuazione della matematica. Lo sviluppo di questa “nuova” logica ha le dimostrazioni: tra questi i dimostratori automatici dei condotto ad affrontare problemi che sono sfociati in con- teoremi e gli strumenti della programmazione logica. troversie fondazionali ampiamente dibattute fra il 1900 e il 1925 e che sarebbe fuorviante considerare ricomposte; in ogni caso, la filosofia della matematica ha rice- 3 Teoremi significativi vuto una profonda chiarificazione dalle acquisizioni della logica matematica. • Teorema di semidecidibilità Mentre lo sviluppo tradizionale della logica classica (vedi elenco degli articoli di logica) pone forte enfasi sulla forma delle argomentazioni, l'atteggiamento della logica matematica dei nostri giorni potrebbe essere riassunto con la frase studio combinatorio del contenuto. Questa espressione copre sia i suoi atteggiamenti sintattici (ad es. individuare in un linguaggio formale una stringa da invia-

• Teorema di completezza (forte) • Teorema di completezza (debole) • Teorema di Löwenheim-Skolem (debole). • Teorema di compattezza (semantico) 1

2

7 • Teorema di compattezza (sintattico) • Lemma di Zorn • Lemma di König

4

Alcuni risultati fondamentali • Le dimostrazioni computative della validità universale delle formule della logica del primo ordine possono essere sottoposte alla verifica algoritmica della loro validità. Con una espressione tecnica si dice che il linguaggio delle dimostrazioni è ricorsivo primitivo. Essenzialmente questo equivale al teorema di completezza di Gödel; esso però in genere viene formulato per chiarire che esso non ha nulla a che fare con gli algoritmi. • Il linguaggio delle formule valide della logica del primo ordine non è decidibile, bensì semidecidibile, questo implica che esiste un algoritmo in grado di valutare la validità di una formula. Nel caso in cui la formula sia valida l'algoritmo è in grado di terminare restituendo come prova la dimostrazione della sua validità, in caso contrario, se la formula non è valida, l'algoritmo non è in grado di accorgersene e continua a eseguire calcoli (si dice che diverge), senza mai fornire una risposta. Per questo il linguaggio delle formule si dice ricorsivamente enumerabile.

• Elliott Mendelson, Introduzione alla Logica Matematica, Bollati Boringhieri, 1972. • Dario Palladino: Corso di Logica. Introduzione elementare al calcolo dei predicati, Carocci, 2002. • Dario Palladino: Logica e teorie formalizzate. Completezza, incompletezza, indecidibilità, Carocci, 2004. • Anne Sjerp Troelstra, H. Schwichtenberg: Basic Proof Theory (2nd ed.). Cambridge University Press, 2000. • Achille C. Varzi, John Nolt, Dennis Rohatyn: Logica (2 ed.). McGraw-Hill, 2007.

6 Voci correlate • Assioma (matematica) • Base di Herbrand • Calcolo dei sequenti • Elenco (logica formale) • Logica • Logica della computabilità • Logica della dimostrabilità • Logica della interpretabilità

• Il linguaggio di tutte le formule universalmente valide della logica del secondo ordine non è neppure ricorsivamente enumerabile. Questa è una conseguenza del teorema di incompletezza di Gödel, quindi un eventuale algoritmo che prende in input una formula potrebbe divergere anche nel caso in cui la formula sia valida.

• Logica intuizionista

• Eliminazione dei tagli nel calcolo dei sequenti.

• Semantica dei giochi

• L'indipendenza logica dell'ipotesi del continuo dimostrata da Paul Cohen nel 1963.

COLLEGAMENTI ESTERNI

• Logica dei predicati • Logica modale • Logica dinamica • Model checking

• Teorema di deduzione

7 Collegamenti esterni 5

Bibliografia • Andrea Asperti, Agata Ciabattoni: Logica a Informatica (2 ed.). McGraw-Hill, 2005.

• (EN) Mathematical logic around the world • (EN) Polyvalued logic • Breve storia della logica

• George Boolos, Richard Jeffrey: Computability and Logic (3rd ed.). Cambridge University Press, 1989.

• Logica matematica in Tesauro del Nuovo soggettario, BNCF, marzo 2013.

• Diego Filotto: Dalla grammatica alla logica. Armando Editore, 2005.

• (EN) Computability logic Recente orientamento nella logica matematica, che si propone di spostarla dalla teoria della verità verso la teoria della computabilità.

• Vincenzo Manca, Logica Matematica, Bollati Boringhieri, 2000.

3

8

Fonti per testo e immagini; autori; licenze

8.1

Testo

• Logica matematica Fonte: http://it.wikipedia.org/wiki/Logica%20matematica?oldid=71153174 Contributori: Alfio, Frieda, Robbot, Alberto da Calvairate, Hellis, Kyakan, 4v4l0n42, Ares, MM, Xelloss, BMF81, Felyx, Chobot, CruccoBot, SashatoBot, Nicolaennio, Dedee, Thijs!bot, F l a n k e r, Giovannigobbin, Drow, JAnDbot, Baroc, Gierre, Giacomo.lucchese, Snow Blizzard, Tirinto, GJo, TXiKiBoT, VolkovBot, Robertobra, Ripepette, Al-Nablusi, Abbot, Popop, Rl89, AlnoktaBOT, Wisbot, Megalexandros, Ontoraul, Phantomas, OKBot, Roberto Mura, Hxhbot, Alexbot, Ticket 2010081310004741, MarcoRosa, Demart81, MystBot, FrescoBot, Yamibolo, Maksim-bot, Xqbot, Vanalon, RCantoroBot, D'ohBot, GrouchoBot, Movses-bot, EmanueleMinotto, Christihan, MerlIwBot, Altrevolte, AlessioMela, Botcrux, Legobot, AngeLix88, Addbot e Anonimo: 27

8.2

Immagini

• File:Math.svg Fonte: http://.wikimedia.org/wikipedia/commons/e/eb/Math.svg Licenza: Public domain Contributori: Opera propria Artista originale: Johannes Rössel (talk)

8.3

Licenza dell'opera

• Creative Commons Attribution-Share Alike 3.0