Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed
query: SELECT sid FROM sessions WHERE sid = '50am2o9mktf19h6d7pj4t1amr0' in /var/www/church/includes/database.mysql.inc on line 121 Gruppo di Logica e Geometria della Cognizione
Davide Barbarossa (Università Roma Tre/Université d'Aix-Marseille)
Quando:
20/07/2018 - 11:30
Dove:
Aula 311, Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1
Abstract
La teoria della realizzabilità classica è stata introdotta da J.-L. Krivine negli anni 2000 a seguito di una intuizione di T. Griffin, che ha tipato l'istruzione "callcc" in Scheme (simile alla istruzione "try-catch" in Java) con la regola dell'assurdo (nella forma di legge di Pierce). Questo ha portato a generalizzare la corrispondenza di Curry-Howard a tutta la logica classica, ed anche oltre: assiomatizzando la nozione di programma (lambda-termine) e di esecuzione (programma + pila di esecuzione), grazie alle "algebre di realizzabilità", si riesce ad associare programmi a dimostrazioni (classiche) che usino assiomi supplementari - come ad esempio quelli della teoria degli insiemi. Questi programmi, chiamati "realizzatori" della formula dimostrata, ne forniscono una "giustificazione" che è una semantica intermedia tra quella Tarskiana (vero/falso) e quella data dalle dimostrazioni. In questo incontro ci concentreremo sull'assioma dell'ultrafiltro ("esiste un ultrafiltro non triviale sull'algebra di Boole delle parti di N") nel quadro della aritmetica al secondo ordine.
Warning: Can't find file: 'watchdog' (errno: 2)
query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = '50am2o9mktf19h6d7pj4t1amr0' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/calendario/2018/07/20', '', '216.73.216.58', 1751937180) in /var/www/church/includes/database.mysql.inc on line 121
Warning: Can't find file: 'watchdog' (errno: 2)
query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: INSERT INTO sessions (sid, uid, cache, hostname, session, timestamp) VALUES ('50am2o9mktf19h6d7pj4t1amr0', 0, 0, '216.73.216.58', 'calendar_year|i:2018;calendar_mon|i:7;', 1751937180) in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/calendario/2018/07/20', '', '216.73.216.58', 1751937180) in /var/www/church/includes/database.mysql.inc on line 121