La logique déconfinée

Link identifier archive #link-archive-thumb-soap-9509
La logique déconfinée
Venerdì 29 maggio 2020 alle ore 10:30, il prof. Jean-Yves Girard (CNRS, Directeur de recherche émeérite) terra un seminario di Logica e Informatica Teorica dal titolo: "La logique déconfinée"

Il seminario sarà tenuto in lingua francese.

Abstract:

Nul besoin de système pour raisonner, il suffit d’utiliser des tests. Jusqu’à une date récente, je pensais que cette approche d’usine achoppait sur des problèmes de finitude. Mais si l’on considère des tests suffisants (pas nécessaires donc), les batteries de tests peuvent rester finies. L’opposition traditionnelle entre Curry et Church se retrouve sous la forme usage/usine. L’usage (BHK) définit les signifiants logiques implicitement : le type comme comportement. L’usine (Herbrand) définit les signifiants logiques explicitement : le type comme critère de correction.

Ces deux approches sont reliées par un résultat d’adéquation, élimination des coupures si l’on veut : les tests suffisent à garantir l’usage. La trinité réaliste axiomatique syntaxe/sémantique/méta est ainsi remplacée par une trinité déréaliste usine/usage/adéquation.


Per partecipare al seminario bisognerà chiedere il link all’indirizzo email Link identifier #identifier__74634-1vitomichele.abrusci@uniroma3.it  o cliccare sul seguente link Link identifier #identifier__159577-2Teams Meeting

 
Link identifier #identifier__97179-1Link identifier #identifier__144607-2Link identifier #identifier__147418-3Link identifier #identifier__143030-4

This post is also available in: Link identifier #identifier__104295-5enEng