Logica della computabilità: differenze tra le versioni

Versione delle 09:23, 20 set 2023

Versione attuale delle 15:22, 16 ott 2024

(Una versione intermedia di un altro utente non mostrate)

Riga 1:

La '''logica della computabilità''' ('''Computability logic''' o '''CoL''') è un programma di ricerca e un [[modello matematico]] per riqualificare la logica come una teoria formale sistematica della computabilità, in contrapposizione alla logica classica che può essere vista come una teoria formale della verità. È stato presentata per la prima volta e così nominata da [[Giorgi Japaridze]] nel 2003<ref> G. Japaridze, ''[https://www.sciencedirect.com/science/article/pii/S016800720300023X Introduction to computability logic]''. Annals of Pure and Applied Logic 123 (2003), pages 1–99.</ref>.

Se si confronta la CoL con la [[logica classica]] si potrebbe dire che, mentre nella seconda le formule rappresentano enunciati veri o falsi, nella CoL rappresentano [[Problema computazionale|problemi computazionali]]. Nella logica classica, la validità di una formula è intesa come "la formula è sempre vera", ossia indipendentemente dall'interpretazione delle sue sottoformule primitive (variabili extralogiche, cioè enunciati atomici). In modo simile, nella CoL validità significa essere sempre computabile. Più in generale, la logica classica ci dice quando la verità di un certo enunciato segue sempre dalla verità di un dato insieme di altri enunciati. Allo stesso modo, la CoL ci dice quando la computabilità di un certo problema ''A'' segue sempre dalla computabilità di altri problemi dati ''B₁, ...,B_n''. Inoltre, la CoL fornisce un metodo uniforme per realizzare effettivamente una soluzione ([[algoritmo]]) di tale problema ''A'' da qualsiasi soluzione nota di ''B₁, ..., B_n''.

La logica della computabilità interpreta i problemi computazionali nel loro senso più generale - interattivo. Questi, infatti, sono formalizzati come giochi giocati da una macchina contro il suo ambiente, e la computabilità significa l'esistenza di una macchina che vince il gioco contro qualsiasi possibile comportamento dell'ambiente. Definendo il significato di queste macchine-giocatori, la CoL fornisce una generalizzazione della [[Tesi di Church-Turing]] al livello della computazione interattiva, che è anche il tipo usuale di computazione dei computer reali (con diversi input e output). Il classico concetto di verità risulta così essere un caso speciale con interattività di grado zero della computabilità. Questo rende la logica classica un frammento particolare della CoL. Essendo un'estensione conservativa della logica

Riga 11:

==Linguaggio==

[[File:Operators of computability logic.png|thumb|Operatori della logica della computabilità]]Il linguaggio completo della CoL è un'estensione del linguaggio della [[logica del primo ordine]]. Il suo vocabolario logico ha diversi tipi di congiunzioni, disgiunzioni, quantificatori, implicazioni, negazioni e cosiddetti ''operatori di ricorrenza''. Questa collezione comprende tutti i connettivi e quantificatori della logica classica. Il linguaggio ha anche due tipi diversi di atomi non logici: ''elementari'' e ''generali''. Gli atomi elementari, che non sono altro che le proposizioni atomiche della logica classica, rappresentano problemi elementari, ovvero giochi senza movimenti che vengono automaticamente vinti dalla macchina quando veri e perduti quando sono falsi, in modo assegnato [[A priori e a posteriori|a priori]]. D'altra parte, gli atomi generali possono essere interpretati come qualsiasi gioco, elementare o non elementare. Sia semanticamente che sintatticamente, la logica classica non è altro che il frammento della CoL ottenuto non permettendo atomi generali nel suo linguaggio così come proibendo tutti gli operatori (costanti logiche del linguaggio) diversi da ¬, ∧, ∨, →, ∀, ∃.

Japaridze ha ripetutamente sottolineato che il linguaggio del CoL è ''in fieri'' e potrebbe subire ulteriori estensioni. A causa dell'espressività di questo linguaggio, i singoli progressi e ricerche nel settore della CoL, come la costruzione di assiomatizzazioni o di teorie applicate basate su di essa, sono di solito limitati solo ad uno o a un altro frammento proprio del linguaggio.

Riga 46:

*G. Japaridze, ''[https://web.archive.org/web/20150628201840/http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.jsl%2F1174668394 The logic of interactive Turing reduction]''. Journal of Symbolic Logic 72 (2007), pages 243-276. [https://arxiv.org/pdf/cs/0512100v4.pdf Prepublication]

*G. Japaridze, ''{{Collegamento interrotto|1=[https://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6TYB-4NSWYVP-1&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_version=1&_urlVersion=0&_userid=10&md5=3a7cf451f14038839aba1d27bd89393f The intuitionistic fragment of computability logic at the propositional level] |data=settembre 2019 |bot=InternetArchiveBot }}''. Annals of Pure and Applied Logic 147 (2007), pages 187-227.

*G. Japaridze, ''[https://archive.todayis/20130415174625/http://logcom.oxfordjournals.org/cgi/content/abstract/exn019 Cirquent calculus deepened]''. Journal of Logic and Computation 18 (2008), No.6, pp.&nbsp;983–1028.

*G. Japaridze, ''{{collegamento interrotto|1=[http://clx.doi.org/10.1016/j.ic.2008.10.001 Sequential operators in computability logic] |data=ottobre 2017 |bot=InternetArchiveBot }}''. Information and Computation 206 (2008), No.12, pp.&nbsp;1443–1475. [https://arxiv.org/pdf/0712.1345v2.pdf Prepublication]

*G. Japaridze, ''{{Collegamento interrotto|1=[http://www.springerlink.com/content/04t6780731373n13/ Many concepts and two logics of algorithmic reduction] |data=febbraio 2020 |bot=InternetArchiveBot }}''. Studia Logica 91 (2009), No.1, pp.&nbsp;1–24. [https://arxiv.org/pdf/0706.0103v4.pdf Prepublication]

*G. Japaridze, ''[https://archive.todayis/20130203153059/http://www.springerlink.com/content/m022011617448676/?p=a62bebfc0dec4164a3a3ba90fefb86aa&pi=10 In the beginning was game semantics]''. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp.&nbsp;249–350. [https://arxiv.org/pdf/cs/0507045v3.pdf Prepublication]

*G. Japaridze, ''[https://web.archive.org/web/20150629001449/http://projecteuclid.org/DPubS?verb=Display&version=1.0&service=UI&handle=euclid.jsl%2F1268917495&page=record Towards applied theories based on computability logic]''. Journal of Symbolic Logic 75 (2010), pp.&nbsp;565–601.

*G. Japaridze, ''[https://www.sciencedirect.com/science/article/pii/S0304397510006754 Toggling operators in computability logic]''. Theoretical Computer Science 412 (2011), pp.&nbsp; 971-1004. [https://arxiv.org/pdf/0904.3469v2.pdf Prepublication]