L'introduction d'un nouveau concept scientifique permet souvent de donner de nouvelles réponses à des questions anciennes qui n'avaient jusqu'alors reçu que des réponses imparfaites. Cet exposé présente quelques questions qui ont trouvé de nouvelles réponses depuis que nous comprenons mieux la notion d'algorithme : qu'est-ce qu'un aéroport ?, qu'est-ce qu'une cellule, qu'est-ce qu'une loi physique ?, ... La prise de conscience du caractère algorithmique de ces objets scientifiques nous amène à considérer de nouveaux langages pour les décrire. Cette révolution, dans le langage dans lequel la science s'écrit, peut-être comparée à la révolution qui s'est produite, au début du XVIIe siècle, quand le langage mathématique a commencé à être utilisé pour décrire des phénomènes physiques.[-]

Goedel's theorem on the completeness of propositional and first-order logic allows one to choose between a plurality of 'equivalent' methods to evaluate the validity of arguments: for example, natural deduction in a syntactic approach, and truth tables, refutation trees, model theory in a semantic approach. However, there is a practical asymmetry between the two approaches when it comes to making actual evaluations. For example, to show that an argument is invalid, it is easier to show a semantic counterexample than to provide a proof, whereas the opposite is true when it comes to showing that it is valid. When one moves to the terrain of natural language to study ordinary argumentation, the distance between syntax and semantics further increases, because of the role played by pragmatics.
There are three basic ways to add pragmatics to logic. One can keep syntax and semantics unchanged (thus maintaining symmetry as much as possible) and add pragmatics to extend formal logic in such a way that it could satisfactorily apply to natural languages. On the other hand, one can integrate pragmatics into syntactics (by extending admissible derivation rules and schemes) and into semantics (by generalizing the notion of possible world or by including context parameters in the semantic analysis of propositions). Finally, a third way grounds semantics directly on pragmatics, abandoning the idea that one can analyze the relationship between language, thought and the world regardless of human interactions.
Three open questions then come to the forefront. From a logical point of view, the question is whether one can recover a symmetry between syntax and semantics after the pragmatic turn. Or are we forced out of Goedel's completeness paradise? From an argumentation theory perspective, the question is no longer that about the relationship between formal and informal approaches, but about how syntax, semantics, and pragmatics relate to each other. From a comparative perspective that takes into account results in linguistics and philosophy of language, how should we understand the relationship between logic and argumentation theory? Does the former explain how language can speak about the world through the senses of the words, and the latter explain how language is the result of human interactions and is therefore governed by the need to coordinate and facilitate interactions? Or do they have the same objectives?[-]

In this programmatic talk, we will sketch both a conceptual and formal framework for reasoning about the notion of algorithm. This framework will arise from the analysis we will make of the relationships existing between the notion of algorithm and other similar (but still different) notions, like that of computation and that of program. We will first show that the Turing-Church thesis concerning effective computability is not sufficient to capture the notion of algorithm, as it identifies programs which are intensionally different. We will then show the limits of the existing models of computation in capturing some basic construction processes that we are willing to call algorithmic. In order to solve this problem, we propose a formalisation of the notion of model of computation on the base of which we claim that the notion of algorithm could eventually be analyzed. This approach centered around the dynamics of program execution, reconciles the more mechanical view of computation (such as formalized by Turing machines and automata) with the logical view - as it in particular stems from a generalization of Jean-Yves Girard's Geometry of Interaction programme.[-]

Let A be a commutative ring. Does it have a maximal ideal? Classically, Zorn's lemma would allow us to concoct such an ideal. Constructively, no such ideal needs to exist. However, even though no maximal ideal might exist in the standard domain of discourse, a maximal ideal always exists *somewhere*. This is because every ring is countable *somewhere*, and *everywhere*, countable rings have maximal ideals. Concrete computational consequences follow from this phantomic variant of existence.
The talk will introduce the modal operators 'somewhere' and 'everywhere', referring to the multiverse of parametrized mathematics, the multitude of computational forcing extensions. Just like the well-known double negation operator, they are (mostly) trivial from a classical point of view. Their purpose is to (a) put established results in constructive algebra and constructive combinatorics into perspective, (b) construct an origin story for certain inductive definitions and (c) form a unified framework for certain techniques for extracting programs from classical proofs.
Our proposal is inspired by the study of the set-theoretic multiverse, but focuses less on exploring the range of set/topos-theoretic possibility and more on concrete applications in constructive mathematics. As guiding examples, we will examine algebraic closures of fields, Noetherian conditions on rings and the foundations of well-quasi orders such as Dickson's Lemma.
(joint work with Alexander Oldenziel)[-]