Conner and Spencer used ultrafilters to construct homomorphisms between fundamental groups that could not be induced by continuous functions between the underlying spaces. We use methods from Shelah and Pawlikowski to prove that Conner and Spencer could not have constructed these homomorphisms with a weak version of the Axiom of Choice. This led us to define and examine a class of pathological objects that cannot be constructed without a strong version of the Axiom of Choice, which we call the class of inscrutable objects. Objects that do not need a strong version of the Axiom of Choice are scrutable. We show that the scrutable homomorphisms from the fundamental group of a Peano continuum are exactly the homomorphisms induced by a continuous function.We suspect that any proposed theorem whose proof does not use a strong Axiom of Choice cannot have an inscrutable counterexample.

Cette thèse étudie deux modèles de réalisabilité pour la logique classique construits sur la sémantique des jeux HO, interprétant la logique, l'arithmétique et l'analyse classiques directement par des programmes manipulant un espace de stockage d'ordre supérieur.La non-innocence en jeux HO autorise les références d'ordre supérieur, et le non parenthésage révèle la CPS des jeux HO et fournit une catégorie de continuations dans laquelle interpréter le lambda-mu calcul de Parigot. Deux modèles de réalisabilité sont construits sur cette interprétation calculatoire directe des preuves classiques.Le premier repose sur l'orthogonalité, comme celui de Krivine, mais il est simplement typé et au premier ordre. En l'absence de codage de l'absurdité au second ordre, une mu-variable libre dans les réaliseurs permet l'extraction. Nous définissons un bar-récurseur et prouvons qu'il réalise l'axiome du choix dépendant, utilisant deux conséquences de la structure de CPO du modèle de jeux: toute fonction sur les entiers (même non calculable) existe dans le modèle, et toute fonctionnelle sur des séquences est Scott-continue. La bar-récursion est habituellement utilisée pour réaliser intuitionnistiquement le « double negation shift » et en déduire la traduction négative de l'axiome du choix. Ici, nous réalisons directement l'axiome du choix dans un cadre classique.Le second, très spécifique au modèle de jeux, repose sur des conditions de gain: des ensembles de positions d'un jeu munis de propriétés de cohérence. Un réaliseur est alors une stratégie dont les positions sont toutes gagnantes. / This thesis investigates two realizability models for classical logic built on HO game semantics. The main motivation is to have a direct computational interpretation of classical logic, arithmetic and analysis with programs manipulating a higher-order store.Relaxing the innocence condition in HO games provides higher-order references, and dropping the well-bracketing of strategies reveals the CPS of HO games and gives a category of continuations in which we can interpret Parigot's lambda-mu calculus. This permits a direct computational interpretation of classical proofs from which we build two realizability models.The first model is orthogonality-based, as the one of Krivine. However, it is simply-typed and first-order. This means that we do not use a second-order coding of falsity, and extraction is handled by considering realizers with a free mu-variable. We provide a bar-recursor in this model and prove that it realizes the axiom of dependent choice, relying on two consequences of the CPO structure of the games model: every function on natural numbers (possibly non computable) exists in the model, and every functional on sequences is Scott-continuous. Usually, bar-recursion is used to intuitionistically realize the double negation shift and consequently the negative translation of the axiom of choice. Here, we directly realize the axiom of choice in a classical setting.The second model relies on winning conditions and is very specific to the games model. A winning condition is a set of positions in a game which satisfies some coherence properties, and a realizer of a formula is then a strategy which positions are all winning.

Dans cette thèse nous étudions les sémantiques ludothéoriques, conçues comme les altérnatives à la sémantique traditionelle de Tarski, qui metent en marche le princip Meaning is in use et l’idée des jeux de language de second Wittgenstein: le sens des constantes logiques est donné par les règles qui en fixent l’usage et qui apparaissent dans les interactions social que sont les jeux de langage. Deux traditions ludotheorique sont présentées: Game Theoretical Semantics (GTS), proposé par Hintikka et Sandu en 1968 et Dialogical logic, proposé initialement par Paul Lorenzen et Kuno Lorenz en 1955 et developé à partir de 1993 par Shahid Rahman et ses collègues. En 1989 Hintikka et Sandu ont arrivé à l’idée des jeux avec des informations imparfaits qui les a emmené à Independence Friendly Logique (IF logic), logique du premiere ordre qui dépasse en expressivité la logique classique. Deux chapitres de cette thèse sont consacrés à l’axiom de choix et au traitement de l’anaphore, deux sujets choisis par Hintikka pour démontrer la fécondité de la logique IF et de GTS. Le but de cette thèse et de montrer que’il est possible de rendre compte aussi bien et à moindre frais dans le cadre dialogique. Plus précisément, la logique IF est comparée avec la théorie constructive des types dans la forme dialogique pour conclure à la supériorité de cette dernière qui a le même pouvoir explicatif qu’IF sans sacrifier pour autant la dimension inférentielle de la logique. / This thesis studies game-theoretically oriented semantics which provide an alternative to traditional Tarski-style semantics, implementing Wittgenstein’s idea of the meaning as use. Two different game theoretical traditions are presented: Game Theoretical Semantics (GTS), developed by Jaako Hintikka and Gabriel Sandu, and Dialogical logic, first introduced by Paul Lorenzen and Kuno Lorenz and further developed by Shahid Rahman and his associates. In 1989 Hintikka and Sandu came up with games with imperfect information. Those games yielded Independence friendly first-order logic (IF logic), exceeding the expressive power of classical first-order logic. It is expressive enough to enable formulating linearly, and at the first-order level, sentences containing branching quantification. Because of this characteristic, Hintikka claims that IF logic is most suitable for at least two main purposes: to be the logic of the first-order fragment of natural language; and to be the medium for the foundation of mathematics. This thesis aims to explore the above uses of IF logic. The properties of IF logic are discussed, as well as the advantages of this approach such as the possibility of taking account of (in)dependency relations among variables; GTS-account of two different notions of scope of quantifiers; the “outside–in” direction in approaching the meaning, which turns out to be advantageous over the traditional “inside-out” approach; the usefulness of game-theoretic reasoning in mathematics; the expressiveness of IF language, which allows formulating branching quantifiers on the first-order level, as well as defining the truth predicate in the language itself. We defend Hintikka’s stance on the first-order character of IF logic against some criticisms of this point. The weak points are also discussed: first and foremost, the lack of a full axiomatization for IF logic and second, the problem of signalling, a problematic phenomenon related to the possibility of imperfect information in a game. We turn to another game-theoretically oriented semantics, that of Dialogical Logic linked with Constructive Type Theory, in which dependency relations can be accounted for, but without using more means than constructive logic and the dialogical approach to meaning have to offer. This framework is used first to analyse and confront Hintikka’s take on the axiom of choice, and second to analyse the GTS account of anaphora.

This thesis presents the strong and weak forms of the Banach-Tarski paradox based on the Hausdorff paradox. It provides modernized proofs of the paradoxes and necessary properties of equidecomposable and paradoxical sets. The historical significance of the paradox for measure theory is covered, along with its incorrect attribution to Banach and Tarski. Finally, the necessity of the axiom of choice is discussed and contrasted with other axiomatic and topological assumptions that enable the paradoxes. / Den här uppsatsen presenterar den starka och svaga formen av Banach-Tarskis paradox baserade på Hausdorffs paradox. Den tillhandahåller moderniserade bevis av paradoxerna och nödvändiga egenskaper av likuppdelningsbara och paradoxala mängder. Den historiska betydelsen av paradoxen på måtteori tas upp samt dess felaktiga tillskrivning till Banach och Tarski. Till sist diskuteras behovet av urvalsaxiomet som ställs i kontrast mot andra axiomatiska och topologiska antaganden som möjliggör paradoxerna.