Logica intuizionista: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m →Logica intuizionistica come calcolo formale e logico: fix wlink a disambigua |
|||
Riga 12:
==Logica intuizionistica come calcolo formale e logico==
Da un punto di vista pratico, c'è un buon motivo per usare la logica intuizionista. Nella [[Programmazione (informatica)|programmazione]], infatti, delle mere asserzioni di [[esistenza]] sono poco interessanti. Un programma per [[computer]] è compilato per fornire una risposta, non per affermare che ne esiste (o non ne esiste) una. Sarebbe infatti strano che un sistema fornisse una dimostrazione per ∃''x''P(''x'') ma non potesse provare P(''b'') per qualsiasi ''b'' che non sia una variabile libera.
Una formalizzazione rigorosa della logica intuizionista richiede una [[teoria dei modelli]] ed una teoria della dimostrazione adeguate. La [[sintassi]] delle formule intuizioniste è simile alla [[logica proposizionale]] (o del primo ordine). Naturalmente molte [[tautologia|tautologie]] della logica classica non possono più esser dimostrate nell'intuizionismo; non solo il principio del terzo escluso, ma anche la [[legge di Peirce]] ed uno dei [[teoremi di De Morgan]].
| |||