Dissertations / Theses on the topic 'Axiom of choice'

We will discuss the 9th axiom of Zermelo-Fraenkel set theory with choice, which is often abbreviated ZFC, since it includes the axiom of choice (AC). AC is a controversial axiom that is mathematically equivalent to many well known theorems and has an interesting history in set theory. This thesis is a combination of discussion of the history of the axiom and the reasoning behind why the axiom is controversial. This entails several proofs of theorems that establish the fact that AC is equivalent to such theorems and notions as Tychonoff's Theorem, Zorn's Lemma, the Well-Ordering Theorem, and many more.

The Nielsen-Schreier theorem states that subgroups of free groups are free. As all of its proofs use the Axiom of Choice, it is natural to ask whether the theorem is equivalent to the Axiom of Choice. Other questions arise in this context, such as whether the same is true for free abelian groups, and whether free groups have a notion of dimension in the absence of Choice. In chapters 1 and 2 we define basic concepts and introduce Fraenkel-Mostowski models. In chapter 3 the notion of dimension in free groups is investigated. We prove, without using the full Axiom of Choice, that all bases of a free group have the same cardinality. In contrast, a closely related statement is shown to be equivalent to the Axiom of Choice. Schreier graphs are used to prove the Nielsen-Schreier theorem in chapter 4. For later reference, we also classify Schreier graphs of (normal) subgroups of free groups. Chapter 5 starts with an analysis of the use of the Axiom of Choice in the proof of the Nielsen-Schreier theorem. Then we introduce representative functions - a tool for constructing choice functions from bases. They are used to deduce the finite Axiom of Choice from Nielsen-Schreier, and to prove the equivalence of a strong form of Nielsen-Schreier and the Axiom of Choice. Using Fraenkel-Mostowski models, we show that Nielsen-Schreier cannot be deduced from the Boolean Prime Ideal Theorem. Chapter 6 explores properties of free abelian groups that are similar to those considered in chapter 5. However, the commutative setting requires new ideas and different proofs. Using representative functions, we deduce the Axiom of Choice for pairs from the abelian version of the Nielsen-Schreier theorem. This implication is shown to be strict by proving that it doesn't follow from the Boolean Prime Ideal Theorem. We end with a section on potential applications to vector spaces.

A topological space X, is shown to be compact if and only if every net in X has a cluster point. If s is a net in a product Q 2A X, where each Xis a compact topological space, then, for every subset B of A, such that the restriction of s to B has a cluster point in the partial product Q 2B X, it is found that the restriction of s to B [ fg – extending B by one element 2 A n B – has a cluster point in its respective partial product Q 2B[fg X, as well. By invoking Zorn’s lemma, the whole of s can be shown to have a cluster point. It follows that the product of any family of compact topological spaces is compact with respect to the product topology. This is Tychono’s theorem. The aim of this text is to set forth a self contained presentation of this proof. Extra attention is given to highlight the deep dependency on the axiom of choice.

In this essay we give an elementary introduction to topology so that we can prove Tychonoff’s theorem, and also its equivalence with the axiom of choice.
Denna uppsats tillhandahåller en grundläggande introduktion till topologi för att sedan bevisa Tychonoff’s theorem, samt dess ekvivalens med urvalsaxiomet.

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.

Submitted by Viviane Lima da Cunha (viviane@biblioteca.ufpb.br) on 2015-10-19T12:44:14Z No. of bitstreams: 1 arquivototal.pdf: 685310 bytes, checksum: c2f1ca276071e748c54644c3a47977f8 (MD5)
Approved for entry into archive by Maria Suzana Diniz (msuzanad@hotmail.com) on 2015-10-19T12:44:52Z (GMT) No. of bitstreams: 1 arquivototal.pdf: 685310 bytes, checksum: c2f1ca276071e748c54644c3a47977f8 (MD5)
Made available in DSpace on 2015-10-19T12:44:52Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 685310 bytes, checksum: c2f1ca276071e748c54644c3a47977f8 (MD5) Previous issue date: 2014-08-27
Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES
The main objective of this work is showing the importance of systems axiomatic in mathematics. We will study some classic axioms, their equivalence and we will see some applications of them.
Este trabalho tem como objetivo fazer uma abordagem sobre a importância de sistemas axiomáticos na Matemática. Estudaremos alguns axiomas clássicos, suas equivalências e veremos algumas aplicações dos mesmos.

This thesis concerns two-point sets, which are subsets of the real plane which intersect every line in exactly two points. The existence of two-point sets was first shown in 1914 by Mazukiewicz, and since this time, the properties of these objects have been of great intrigue to mathematicians working in both topology and set theory. Arguably, the most famous problem about two-point sets is concerned with their so-called "descriptive complexity"; it remains open, and it appears to be deep. An informal interpretation of the problem, which traces back at least to Erdos, is: The term "two-point" set can be defined in a way that it is easily understood by someone with only a limited amount of mathemat- ical training. Even so, how hard is it to construct a two-point set? Can one give an effective algorithm which describes precisely how to do so? More formally, Erdos wanted to know if there exists a two-point set which is a Borel subset of the plane. An essential tool in showing the existence of a two-point set is the Axiom of Choice, an axiom which is taken to be one of the basic truths of mathematics.

On travaille dans ZF, théorie des ensembles sans Axiome du Choix. En considérant des formes plus faibles de l'Axiome du choix, comme l'axiome de Hahn-Banach HB : "Toute forme linéaire sur un sous-espace vectoriel d'un espace vectoriel E, majorée par une forme sous-linéaire p se prolonge en une forme linéaire sur E majorée par p'', ou encore l'axiome de Tychonov T2 : "Un produit de compacts séparés est compact'', on étudie l'existence d'états dans les groupes ordonnés avec unité d'ordre. On poursuit l'étude en établissant des liens entre idéaux à gauche et états sur les C*-algèbres
We work in ZF, set theory without Axiom of Choice. Using weak forms of Axiom of Choice, for example Hahn-Banach axiom HB : "Every linear form on a vector subspaceof a vector space E, increased by a sublinear form p can be extended to a linear form on E increased by p", or Tychonov axiom T2 : "Every product of compact Haussdorf is compact, we study the existence of states on ordered groups with order unit. We continue giving links between left ideals and states on C*-algebras

AGUIAR, Francisco Fagner Portela. Um background na teoria dos conjuntos. 2015. 50 f. Dissertação (Mestrado em Matemática em Rede Nacional) – Centro de Ciências, Universidade Federal do Ceará, Fortaleza, 2015.
Submitted by Erivan Almeida (eneiro@bol.com.br) on 2015-11-13T15:41:09Z No. of bitstreams: 1 2015_dis_ffpaguiar.pdf: 1566390 bytes, checksum: 114ad96172cfa622234e88e05d73ffff (MD5)
Approved for entry into archive by Rocilda Sales(rocilda@ufc.br) on 2015-11-18T13:38:59Z (GMT) No. of bitstreams: 1 2015_dis_ffpaguiar.pdf: 1566390 bytes, checksum: 114ad96172cfa622234e88e05d73ffff (MD5)
Made available in DSpace on 2015-11-18T13:38:59Z (GMT). No. of bitstreams: 1 2015_dis_ffpaguiar.pdf: 1566390 bytes, checksum: 114ad96172cfa622234e88e05d73ffff (MD5) Previous issue date: 2015
The set theory sometimes left out in some high schools, is in a key element for understanding the functions in particular. Failure to address this issue or its superficial approach leaves the student a difficult gap to be filled in later studies. Incidentally, the left gap may hinder student performance in higher education. If this is so, is the main objective of this work to a reinterpretation of the main topics linked to the high school set theory, while making a bridge between these and other equally important points dealing with sets in a more academic language. Will be covered from the properties and theorems related to finite sets up its generalization to infinite sets, culminating in the Cantor-Schroeder-Bernstein theorem, the Axiom of Choice and Zorn’s Lemma. To this end, there were literature searches in various sources.
A teoria de conjuntos por vezes deixada de lado em algumas escolas de ensino médio, constitui-se em um elemento primordial para o entendimento das funções, em especial. A não abordagem, ou a sua abordagem superficial, deixa no estudante uma lacuna difícil de ser suprida em estudos posteriores. Aliás, a lacuna deixada pode dificultar o desempenho do estudante no ensino superior. Diante desta constatação, é objetivo principal desta dissertação fazer uma leitura dos principais tópicos ligados à Teoria de Conjuntos do ensino médio, ao mesmo tempo em que faz uma ponte entre estes e outros pontos não menos importantes, tratando conjuntos em uma linguagem mais acadêmica. Serão abordados desde as propriedades e teoremas relacionados a conjuntos finitos, até a sua generalização para conjuntos infinitos, culminando com o teorema de Cantor-Schroeder-Bernstein, o Axioma da Escolha, e o Lema de Zorn. Para tantos, realizaram-se pesquisas bibliográficas em fontes variadas.

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

Les préférences révélées lient choix, préférences et bien-être lorsque les choix apparaissent cohérents. Le premier chapitre s’intéresse à la force des hypothèses nécessaire pour obtenir des indications précises sur le bien-être quand les choix sont incohérents. Il utilise les données d’expériences en laboratoire et sur le terrain pour évaluer le pouvoir prédictif de deux approches utilisant peu d’hypothèses. Ces approches ont un pouvoir prédictif élevé pour une majorité d’individus, elles fournissent donc des indications précises sur le bien-être. Le pouvoir prédictif de ces approches est fortement corrélé à deux propriétés des préférences révélées. Le deuxième chapitre introduit une méthode pour obtenir l’ensemble des meilleures alternatives d’un individu, en cohérence avec théorie des préférences révélées, mais en contradiction avec les pratiques expérimentales. Les individus sont incités à choisir plusieurs alternatives à l’aide d’un petit paiement additionnel, mais sont rémunérés à la in par une seule, tirée au hasard. Les conditions pour que les meilleures alternatives soient partiellement ou complètement identifiées sont données. Le troisième chapitre applique cette méthode dans une expérience. Les meilleures alternatives sont complètement identifiées pour 18% des sujets et partiellement pour 40%. Les préférences complètes, réflexives et transitives rationalisent 40% des choix observés dans l’expérience. Permettre que les choix dépendant de l’ensemble de choix, tout en conservant les préférences classiques, rationalise 96% des choix observés. Enfin, on observe une quantité significative d’indifférence, bien supérieure à ce qui est obtenu traditionnellement
Revealed preferences link choices, preferences, and welfare when choices appear consistent. The first chapter assesses how much structure is necessary to impose on a model to provide precise welfare guidance based on inconsistent choices. We use data sets from the lab and field to evaluate the predictive power of two conservative “model-free” approaches of behavioral welfare analysis. We find that for most individuals, these approaches have high predictive power, which means there is little ambiguity about what should be selected from each choice set. We show that the predictive power of these approaches correlates highly with two properties of revealed preferences. The second chapter introduces a method for eliciting the set of best alternatives of decision makers, in line with the theory on revealed preferences, but at odds with the current practice. We allow decision makers to choose several alternatives, provide an incentive for each alternative chosen, and then randomly select one for payment. We derive the conditions under which we partially or fully identify the set of best alternatives. The third chapter applies the method in an experiment. We fully identify the set of best alternatives for 18% of subjects and partially identify it for another 40%. We show that complete, reflexive, and transitive preferences rationalize 40% of observed choices in the experiment. Going beyond, we show that allowing for menu-dependent choices while keeping classical preferences rationalize 96% of observed choices. Besides, eliciting sets allows us to conclude that indifference is significant in the experiment, and underestimate by the classical method

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

Cette thèse s'intéresse au contenu calculatoire des preuves classiques, et plus spécifiquement aux preuves avec effets de bord et à la réalisabilité classique de Krivine. Le manuscrit est divisé en trois parties, dont la première consiste en une introduction étendue des concepts utilisés par la suite. La seconde partie porte sur l’interprétation calculatoire de l’axiome du choix dépendant en logique classique. Ce travail s'inscrit dans la continuité du système dPAω d'Hugo Herbelin, qui permet d’adapter la preuve constructive de l’axiome du choix en théorie des types de Martin-Löf pour en faire une preuve constructive de l’axiome du choix dépendant dans un cadre compatible avec la logique classique. L'objectif principal de cette partie est de démontrer la propriété de normalisation pour dPAω, sur laquelle repose la cohérence du système. La difficulté d'une telle preuve est liée à la présence simultanée de types dépendants (pour la partie constructive du choix), d'opérateurs de contrôle (pour la logique classique), d'objets co-inductifs (pour "encoder" les fonctions de type N → A par des streams (a₀,a₁,...)) et d'évaluation paresseuse avec partage (pour ces objets co-inductifs). Ces difficultés sont étudiées séparément dans un premier temps. En particulier, on montre la normalisation du call-by-need classique (présenté comme une extension du λµµ̃-calcul avec des environnements partagé), en utilisant notamment des techniques de réalisabilité à la Krivine. On développe ensuite un calcul des séquents classique avec types dépendants, définie comme une adaptation du λµµ̃-calcul, dont la correction est prouvée à l'aide d'une traduction CPS tenant compte des dépendances. Enfin, une variante en calcul des séquents du système dPAω est introduite, combinant les deux points précédents, dont la normalisation est finalement prouvée à l'aide de techniques de réalisabilité. La dernière partie, d'avantage orientée vers la sémantique, porte sur l’étude de la dualité entre l’appel par nom (call-by-name) et l’appel par valeur (call-by-value) dans un cadre purement algébrique inspiré par les travaux autour de la réalisabilité classique (et notamment les algèbres de réalisabilité de Krivine). Ce travail se base sur une notion d'algèbres implicatives développée par Alexandre Miquel, une structure algébrique très simple généralisant à la fois les algèbres de Boole complètes et les algèbres de réalisabilité de Krivine, de manière à exprimer dans un même cadre la théorie du forcing (au sens de Cohen) et la théorie de la réalisabilité classique (au sens de Krivine). Le principal défaut de cette structure est qu’elle est très orientée vers le λ-calcul, et ne permet d’interpréter fidèlement que les langages en appel par nom. Pour remédier à cette situation, on introduit deux variantes des algèbres implicatives les algèbres disjonctives, centrées sur le “par” de la logique linéaire (mais dans un cadre non linéaire) et naturellement adaptées aux langages en appel par nom, et les algèbres conjonctives, centrées sur le “tenseur” de la logique linéaire et adaptées aux langages en appel par valeur. On prouve en particulier que les algèbres disjonctives ne sont que des cas particuliers d'algèbres implicatives et que l'on peut obtenir une algèbre conjonctive à partir d'une algèbre disjonctive (par renversement de l’ordre sous-jacent). De plus, on montre comment interpréter dans ces cadres les fragments du système L de Guillaume Munch-Maccagnoni en appel par valeur (dans les algèbres conjonctives) et en appel par nom (dans les algèbres disjonctives)
This thesis focuses on the computational content of classical proofs, and specifically on proofs with side-effects and Krivine classical realizability. The manuscript is divided in three parts, the first of which consists of a detailed introduction to the concepts used in the sequel.The second part deals with the computational content of the axiom of dependent choice in classical logic. This works is in the continuity of the system dPAω developed Hugo Herbelin. This calculus allows us to adapt the constructive proof of the axiom of choice in Martin-Löf's type theory in order to turn it into a constructive proof of the axiom of dependent choice in a setting compatible with classical logic. The principal goal of this part is to prove the property of normalization for dPAω, on which relies the consistency of the system. Such a proof is hard to obtain, due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of co-inductive objects (in order to "encode" functions of type N → A as streams (a₀,a₁,...)) and of lazy evaluation with sharing (for this co-inductive objects). These difficulties are first studied separately. In particular, we prove the normalization of classical call-by-need (presented as an extension of the λµ̃µ-calculus with shared environments) by means of realizability techniques. Next, we develop a classical sequent calculus with dependent types, defined again as an adaptation of the λµ̃µ-calculus, whose soundness is proved thanks to a CPS translation which takes the dependencies into account. Last, a sequent-calculus variant of dPAω is introduced, combining the two previous systems. Its normalization is finally proved using realizability techniques. The last part, more oriented towards semantics, studies the duality between the call-by-name and the call-by-value evaluation strategies in a purely algebraic setting, inspired from several works around classical realizability (and in particular Krivine realizability algebras). This work relies on the notion of implicative algebras developed by Alexandre Miquel, a very simple algebraic structure generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such a way that it allows us to express in a same setting the theory of forcing (in the sense of Cohen) and the theory of classical realizability (in the sense of Krivine). The main default of these structures is that they are deeply oriented towards the λ-calculus, and that they only allows to faithfully interpret languages in call-by-name. To remediate the situation, we introduce two variants of implicative algebras: disjunctive algebras, centered on the "par" connective of linear logic (but in a non-linear framework) and naturally adapted to languages in call-by-name; and conjunctives algebras, centered on the "tensor" connective of linear logic and adapted to languages in call-by-value. Amongst other things, we prove that disjunctive algebras are particular cases of implicative algebras and that conjunctive algebras can be obtained from disjunctive algebras (by reversing the underlying order). Moreover, we show how to interpret in these frameworks the fragments of Guillaume Munch-Maccagnoni's system L corresponding to a call-by-value calculus (within conjunctive algebras) and to a call-by-name calculus (within disjunctive algebras)

Cette thèse comporte cinq chapitres et a deux objectifs principaux qui sont l'étude de l'axiome de quasi transitivité des préférences dans la théorie du choix individuel, et l'extension de la définition traditionnelle du choix rationnel aux cas de préférences dépendant des ensembles de choix. Chapitre 1. Rappel de notions sur les relations binaires, mise en exergue du principe de dualité, analyse de l'axiome de totalité, analyse des concepts d'indifférence et d'in comparabilité, rappel sur la modélisation standard des préférences dans la théorie du choix individuel. Chapitre 2. Analyse des relations binaires avec indifférence non transitive (relations de ferrers, relations d'intervalles quasiordres), représentation continue de ces relations. Chapitre 3. Analyse de l'axiome de quasi-transitivité par, d'une part l'analyse de la procédure de la pompe à monnaie et d'autre part, la confrontation de cet axiome avec la définition du choix rationnel dans la théorie des fonctions de choix. Chapitre 4. Selon le chapitre précédent, l'axiome d'acyclicité des préférences est respecté par les agents rationnels se pose alors le problème de la représentation et de l'interprétation de ces types de préférences chapitre 5. Partie empirique qui teste (sur données individuelles de consommations, INSEE, budgets des familles, 1979, 1984, 1989) principalement le modèle que nous avons construit dans le chapitre précédent.

Cette thèse s’intéresse à quelques aspects de la formalisation des mathématiques, et plus spécialement des mathématiques classiques, dans le calcul des constructions inductives (CCI), le système logique implanté dans le logiciel d’aide à la démonstration Coq. Trois principaux travaux ont été réalisés. La première partie fait état d’un travail de formalisation d’algèbre, topologie et théorie des faisceaux en vue de la définition des schémas affines, ainsi que de la spécification du lemme d’Horace. La deuxième partie s’intéresse aux types quotients, on montre qu’il ne peut y avoir dans le CCI de notion catégorique de type quotient qui soit aussi expressive que les ensembles quotients en mathématiques classiques. Enfin, on montre en troisième partie l’incohérence dans le CCI de l’ajout simultané de l’axiome du choix et du tiers exclu sous forme propositionnelle
This thesis is about some aspects of the formalization of mathematics, and more especially of classical mathematics, in the calculus of inductive constructions (CIC), the logical system of the proof assistant Coq. In the first part we formalize algebria, topology and sheaves theory and we finish by definition of affine schemes. We also give a specification of the Horace’s lemma. The second part is about quotient types, we show that there cannot be in the CCI a categoric notion of quotient type as expressive as quotients in classical mathematics. Finally one shows in the third part the axiom of choice with values in prop is contradictory with the excluded middle in prop

Ce travail est devoué à la Réalisabilité de Krivine, se focalisant sur les aspects calculatoires des réalisateurs des formules. Chaque formule a un jeu associé. Chaque preuve fournit un therme capable d'implémenter une stratégie gagnante pour le jeux associé à la formule qu'elle démontre. Une preuve est, par adéquation, un combinateur capable de prendre des stratégies gagnantes pour les hypothèses et les combiner pour rendre une stratégie gagnante pour la conclusion. Y-sont abordés: A. Le problème de l'espécification, consistant a décrire en termes calculatoires les réalisateurs d'une formule donée. Des nombreaux examples y-sont traités. B. On étudie une preuve en tant que combinateur de stratégies gagnantes: On pose une implication $A\to B$ où $A$ et $B$ sont des formules $\Sigma^0_2$. Soit $C$ la forma normale prenexe de $A\to B$. On étudie une preuve de $A, C\to B$ en tant que combinateur de stratégies gagnantes. En faisant ce travail, certaines techniques sont développées pour tracer l'éxécution d'un processus, dont notamment la "méthode des fils".

Thesis (Ph. D.)--Florida State University, 2009.
Advisor: Russell M. Dancy, Florida State University, College of Arts and Sciences, Dept. of Philosophy. Title and description from dissertation home page (viewed Aug. 6, 2009). Document formatted into pages; contains viii, 148 pages. Includes bibliographical references.

In dieser Arbeit möchte ich dem Wesen des Auswahlaxioms auf den Grund gehen und verstehen, inwieweit es problematisch sein könnte, es zu benutzen, aber auch wie nützlich es ist, dieses mächtige Instrument als Mathematiker zu besitzen.

Dissertação de Mestrado em Matemática apresentada à Faculdade de Ciências e Tecnologia
A análise real é familiaríssima e desconhecidíssima. A familiaridade vem-lhe da física e do cálculo e da geometria e das finanças, e muita intuição que outorga números a espaço e tempo e investimento, o mais das vezes abstraindo as funções reais de fenómenos discretos; vem-lhe a estranheza de respeitar a um conjunto \mathbb{R}, encafuado numa axiomática e rico em propriedades indecidíveis. Na verdade, não há princípios bem-conhecidos que eliminem as patologias da análise e deem uma descrição completa de \mathbb{R} e dos seus subconjuntos; o usual é haver escâmbios, onde uma barbaridade contrapesa um bom expediente (como o paradoxo de Banach-Tarski e o Lema de Zorn em \mathbb{R}), e dúvidas nas condições topológicas dos conjuntos, e questões sobre o tamanho do continuum (a prevalência da propriedade de Baire, da mensurabilidade à Lebesgue, etc, depende da axiomática adotada; e as cardinalidades de subconjuntos de \mathbb{R} variam entre o universo binário da Hipótese do Contínuo e a presença de conjuntos de Dedekind cujas cardinalidades são tão diversas como o continuum; e mesmo admitindo que \mathbb{R} é bem-ordenado, o continuum pode ser igual a qualquer um dos cardinais \aleph_n, com n \qeq 1, e a Hipótese do Contínuo pode ser falsa). Estudaremos alguns axiomas que regularizam a análise real e a topologia de \mathbb{R} com um mínimo de abnormidades colaterais: o Axioma da Determinabilidade, o Axioma das Escolhas Numeráveis e a omni-mensurabilidade à Lebesgue. Também veremos algumas relações entre esses postulados e propriedades dos ordinais numeráveis.
Real analysis is strange and familiar. The familiarity comes to it from physics and calculus and geometry and finance, and much intuiting of figures from space and time and investment, most of the time abstracting real-valued functions from discrete phenomena; the strangeness comes from being concerned with a set \mathbb{R}, ensconced in an axiomatic theory and having virtually undecidable predicates. There are in fact no easy principles which can be counted on to do away with the problems of real analysis and give a full description of \mathbb{R} and its subsets; one must usually rely on trade-offs wherein an axiom is shown to have a barbarous corollary (as Zorn's Lemma is to the Banach-Tarski paradox), and the understanding of one point raises other questions about topology in \mathbb{R} and the size of the continuum (the prevalence of the Baire property, Lebesgue measurability, etc, depends on the adopted theory; and the cardinalities contained in \mathbb{R} can vary between the binary dictum of the Continuum Hypothesis and Dedekind sets that assume continuum-many different sizes; and even allowing \mathbb{R} to be well-ordered, the continuum can be assumed to equal any of the alephs \aleph_n, for n \geq 1). We shall expound on axioms which give a cleaner account of real analysis (and topology and set-theoretic properties of \mathbb{R}) without producing too many abnormalities: the Axiom of Determinacy, the Axiom of Countable Choice and the full Lebesgue measurability. We shall also broach some relations between these postulates and the numerable ordinals.