L'objet de cette thèse est d'obtenir une description des plongements élémentaires (au sens de la logique du premier ordre) dans un groupe hyperbolique sans torsion. Le résultat principal décrit ces plongements en terme d'une structure définie par Sela dans sa solution au problème de Tarski: la structure de tour hyperbolique. Ainsi, si H est plongé élementairement dans un groupe hyperbolique sans torsion G, on peut obtenir G en amalgamant successivement des groupes de surfaces à bord à un produit libre de H avec des groupes libres et des groupes de surfaces sans bord. Ceci permet en corollaire de montrer qu'un sous-groupe plongé élémentairement dans un groupe libre de type fini est un facteur libre. Les techniques utilisées pour obtenir cette description sont essentiellement géométriques: actions sur des arbres réels ou simpliciaux, existence de décompositions JSJ. On s'appuie également sur des résultats d'existence d'ensembles de factorisation qui affirment que pour certains groupes A de type fini, étant donné un groupe hyperbolique sans torsion G, il existe un ensemble fini de quotients de A tel que tout morphisme non injectif de A vers G se factorise par l'un de ces quotients après précomposition par un automorphisme de A. On expose une preuve de ces résultats, y compris une version complète et détaillée du shortening argument de Rips et Sela. Le shortening argument montre, grâce à l'analyse de Rips des actions sur des arbres réels, que si une suite d'action d'un groupe A sur des espaces hyperboliques converge vers un A-arbre réel d'un certain type, alors une infinité de ces actions peuvent être raccourcies.

Ce mémoire a pour objectif principal l'analyse du concept de métalangage tel qu'il s'est développé en logique mathématique. L'introduction et la conclusion mises à part, chaque chapitre porte sur un auteur -logicien, mathématicien ou philosophe ayant contribué de manière significative à l'évolution de ce concept. Ces auteurs sont, en ordre de présentation, Gottlob Frege, Bertrand Russell, Ludwig Wittgenstein, David Hilbert, Kurt Godel et Alfed Tarski. Puisque la notion de métalangage s'est développée avec la formalisation progressive de la logique, une attention particulière est accordée à l'émergence des systèmes formels et à leur présentation. Trois périodes se dessinent dans la genèse de cette notion. Une première, que j'appelle « pré-météthéorique », où l'intervention d'une théorie externe au langage formel est rejetée catégoriquement, mais où certaines notions métathéoriques sont implicitement tracées. Une seconde, dite « hilbertienne », qui marque l'entrée en jeu de la métamathématique et qui consacre le métalangage dans l'étude des mathématiques, quoiqu'avec des moyens limités. Et une troisième, dite « tarskienne », où la notion moderne de métalangage est exposée. Par ailleurs, j'effectue une analyse détaillée de la preuve que Godel donne de son second théorème d'incomplétude où je prétends qu'il commet une erreur conceptuelle entre langage et métalangage. Enfin, en conclusion, j'explore une conception fondationnelle de la logique compatible avec l'étude métathéorique. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Métalangage, Logique, Philosophie, Métamathématique, Godel, Tarski.

L'objet de cette thèse est la formalisation et l'automatisation du raisonnement géométrique au sein de l'assistant de preuve Coq.<br />Dans une première partie, nous réalisons un tour d'horizon des principales axiomatiques de la géométrie puis nous présentons une formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie.<br />Dans la seconde partie, nous présentons l'implantation en Coq d'une procédure de décision pour la géométrie affine plane : la méthode des aires de Chou, Gao et Zhang. Cette méthode produit des preuves courtes et lisibles.<br />Dans la troisième partie, nous nous intéressons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof. GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq.<br />Enfin, nous proposons un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.

Nous associons à tout polydisque compact B [appartenant à] Rn une algèbre CB de fonctions réelles de classe C∞ définies au voisinage de B. La collection des algèbres CB est supposée stable par certaines opérations, dont la composition et la dérivation partielle. Nous supposons de plus que, lorsque B est centrée à l'origine, l'algèbre des germes à l'origine des éléments de CB est quasianalytique (c'est à dire qu'elle ne contient pas de germe plat). A l'aide de ces fonctions, nous définissons des ensembles C-semi- analytiques et C-sous-analytiques comme on le fait traditionnellement en géométrie analytique réelle. Notre résultat principal est un théorème du type Tarski-Seidenberg pour ces ensembles. Son énoncé dit essentiellement que les ensembles sous-C-analytiques peuvent être définis par des égalités et des inégalités satisfaites par des termes obtenus en composant des fonctionsdes algèbres C_B , les fonctions x → x1/n , et la fonction x → 1/x. Sa preuve se fait en exprimant les solutions de sytèmes d'équations quasianalytiques au moyen d'un théorème de préparation issu de la théorie des modèles

Nous associons à tout polydisque compact B [appartenant à] Rn une algèbre CB de fonctions réelles de classe C∞ définies au voisinage de B. La collection des algèbres CB est supposée stable par certaines opérations, dont la composition et la dérivation partielle. Nous supposons de plus que, lorsque B est centrée à l’origine, l’algèbre des germes à l’origine des éléments de CB est quasianalytique (c’est à dire qu’elle ne contient pas de germe plat). A l’aide de ces fonctions, nous définissons des ensembles C-semi- analytiques et C-sous-analytiques comme on le fait traditionnellement en géométrie analytique réelle. Notre résultat principal est un théorème du type Tarski-Seidenberg pour ces ensembles. Son énoncé dit essentiellement que les ensembles sous-C-analytiques peuvent être définis par des égalités et des inégalités satisfaites par des termes obtenus en composant des fonctionsdes algèbres C_B , les fonctions x → x1/n , et la fonction x → 1/x. Sa preuve se fait en exprimant les solutions de sytèmes d’équations quasianalytiques au moyen d’un théorème de préparation issu de la théorie des modèles / We associate to every compact polydisk B [belonging to ] Rn an algebra CB of real functions defined in a neighborhood of B. The collection of these algebras is supposed to be closed under several operations, such as composition and partial derivatives. Moreover, if the center of B is the origin, we assume that the algebra of germs at the origin of elements of CB is quasianalytic (it does not contain any flat germ). We define with these functions the collection of C-semianalytic and C-subanalytic sets according to the classical process in real analytic geometry. Our main result is an analogue of Tarski-Seidenberg's usual result for these sets. It says that the sub-C-subanalytic sets may be described by means of equalities and inequalities by terms obtained by composition of elements of the algebras CB, the functions x->^{1/n} and the function x->1/x. It is proved via a model theoretic preparation theorem

Inhalt der Dissertation ist der Einfluß, den die von Alfred Tarski formulierte mathematische Logik auf die Entstehung der drei Computerkonzepte des Konrad Zuse hatte.

Les crises financières et les problèmes se formaient mais les indicateurs ne sont pas précis pour permettre une intervention réglementaire. La thèse propose un modèle dynamique pour le système bancaire avec une banque centrale afin de calculer un indicateur de faillite en fonction de la probabilité qu'une banque soit en faillite et les pertes rencontrées dans le réseau financier, une méthodologie qui peut améliorer la mesure, le suivi et la gestion du risque systémique.La thèse propose également des mécanismes de compensation : 1- avec un modèle considérant l'ancienneté du passif et avec un type d'actif liquide dont la vente excessive conduit à un impact sur le marché, 2 - avec un modèle considérant les participations croisées entres les banques dont les engagements interbancaires sont de différentes séniorités et avec un type d'actif liquide dont la vente excessive conduit à un impact sur le marché. / Financial crisis pose important theoretical problems on creating reliable indicator of stability of financial systems on which basis the regulators could intervene. The thesis proposes a dynamic model of banking system were the central bank can calculate an indicator of potential defaults taking into consideration the probability for a bank to default and the losses encountered in the financial network, a methodology that can improve the measurement, monitoring, and the management of the systemic risk. The thesis also suggests a clearing mechanisms : 1- in a model with seniority of liabilities and one type of liquid asset whose fire sale has a market impact, 2 - in a model with crossholdings among the banks whose interbank liabilities may be senior and junior and with one liquid asset whose firing sale has a market impact.

Normalformen drücken semantische Eigenschaften einer Logik durch syntaktische Restriktionen aus. Sie ermöglichen es Algorithmen, Grenzen der Ausdrucksstärke einer Logik auszunutzen. Ein Beispiel ist die Lokalität der Logik erster Stufe (FO), die impliziert, dass Graph-Eigenschaften wie Erreichbarkeit oder Zusammenhang nicht FO-definierbar sind. Gaifman-Normalformen drücken die Bedeutung einer FO-Formel als Boolesche Kombination lokaler Eigenschaften aus. Sie haben eine wichtige Rolle in Model-Checking Algorithmen für Klassen dünn besetzter Graphen, deren Laufzeit durch die Größe der auszuwertenden Formel parametrisiert ist. Es ist jedoch bekannt, dass Gaifman-Normalformen im Allgemeinen nur mit nicht-elementarem Aufwand konstruiert werden können. Dies führt zu einer enormen Parameterabhängigkeit der genannten Algorithmen. Ähnliche nicht-elementare untere Schranken sind auch für Feferman-Vaught-Zerlegungen und für die Erhaltungssätze von Lyndon, Łoś und Tarski bekannt. Diese Arbeit untersucht die Komplexität der genannten Normalformen auf Klassen von Strukturen beschränkten Grades, für welche die nicht-elementaren unteren Schranken nicht gelten. Für diese Einschränkung werden Algorithmen mit elementarer Laufzeit für die Konstruktion von Gaifman-Normalformen, Feferman-Vaught-Zerlegungen, und für die Erhaltungssätze von Lyndon, Łoś und Tarski entwickelt, die in den ersten beiden Fällen worst-case optimal sind. Wichtig hierfür sind Hanf-Normalformen. Es wird gezeigt, dass eine Erweiterung von FO durch unäre Zählquantoren genau dann Hanf-Normalformen erlaubt, wenn alle Zählquantoren ultimativ periodisch sind, und wie Hanf-Normalformen in diesen Fällen in elementarer und worst-case optimaler Zeit konstruiert werden können. Dies führt zu Model-Checking Algorithmen für solche Erweiterungen von FO sowie zu Verallgemeinerungen der Algorithmen für Feferman-Vaught-Zerlegungen und die Erhaltungssätze von Lyndon, Łoś und Tarski. / Normal forms express semantic properties of logics by means of syntactical restrictions. They allow algorithms to benefit from restrictions of the expressive power of a logic. An example is the locality of first-order logic (FO), which implies that properties like reachability or connectivity cannot be defined in FO. Gaifman's local normal form expresses the satisfaction conditions of an FO-formula by a Boolean combination of local statements. Gaifman normal form serves as a first step in fixed-parameter model-checking algorithms, parameterised by the size of the formula, on sparse graph classes. However, it is known that in general, there are non-elementary lower bounds for the costs involved in transforming a formula into Gaifman normal form. This leads to an enormous parameter-dependency of the aforementioned algorithms. Similar non-elementary lower bounds also hold for Feferman-Vaught decompositions and for the preservation theorems by Lyndon, Łoś, and Tarski. This thesis investigates the complexity of these normal forms when restricting attention to classes of structures of bounded degree, for which the non-elementary lower bounds are known to fail. Under this restriction, the thesis provides algorithms with elementary and even worst-case optimal running time for the construction of Gaifman normal form and Feferman-Vaught decompositions. For the preservation theorems, algorithmic versions with elementary running time and non-matching lower bounds are provided. Crucial for these results is the notion of Hanf normal form. It is shown that an extension of FO by unary counting quantifiers allows Hanf normal forms if, and only if, all quantifiers are ultimately periodic, and furthermore, how Hanf normal form can be computed in elementary and worst-case optimal time in these cases. This leads to model-checking algorithms for such extensions of FO and also allows generalisations of the constructions for Feferman-Vaught decompositions and preservation theorems.

Le but de cette thèse est d'étudier la somme et le zéro dans deux principaux cadres : les isomorphismes de types et la normalisation de lambda-termes. Les isomorphismes de type avaient déjà été étudiés dans le cadre du lambda-calcul simplement typé avec paires surjectives mais sans somme. Pour aborder le cas avec somme et zéro, j'ai commencé par restreindre l'étude au cas des isomorphismes linéaires, dans le cadre de la logique linéaire, ce qui a conduit à une caractérisation remarquablement simple de ces isomorphismes, obtenue grâce à une méthode syntaxique sur les réseaux de preuve. Le cadre plus général de la logique intuitionniste correspond au problème ouvert de la caractérisation des isomorphismes dans les catégories bi-cartésiennes fermées. J'ai pu apporter une contribution à cette étude en montrant qu'il n'y a pas d'axiomatisation finie de ces isomorphismes. Pour cela, j'ai tiré partie de travaux en théorie des nombres portant sur un problème énoncé par Alfred Tarski et connu sous le nom du « problème des égalités du lycée ». Pendant tout ce travail sur les isomorphismes de types, s'est posé le problème de trouver une forme canonique pour représenter les lambda-termes, que ce soit dans le but de nier l'existence d'un isomorphisme par une étude de cas sur la forme du terme, ou pour vérifier leur existence dans le cas des fonctions très complexes que j'étais amené à manipuler. Cette réflexion a abouti à poser une définition « extensionnelle » de forme normale pour le lambda-calcul avec somme et zéro, obtenue par des méthodes catégoriques grâce aux relations logiques de Grothendieck, apportant ainsi une nouvelle avancée dans l'étude de la question réputée difficile de la normalisation de ce lambda-calcul. Enfin je montrerai comment il est possible d'obtenir une version « intentionnelle » de ce résultat en utilisant la normalisation par évaluation. J'ai pu ainsi donner une adaptation de la technique d' évaluation partielle dirigée par les types pour qu'elle produise un résultat dans cette forme normale, ce qui en réduit considérablement la taille et diminue aussi beaucoup le temps de normalisation dans le cas des isomorphismes de types considérés auparavant.

To αντικείμενο μελέτης της εργασίας αυτής είναι κατά μείζονα λόγο το θεώρημα Tarski-Seidenberg. Στο πρώτο κεφάλαιο μελετάμε το κίνητρο που ώθησε τον Tarski σε αυτή την έρευνα, εξιστορούμε την πορεία της ιδέας του από την ανακάλυψη μέχρι τη δημοσίευση και έπειτα προσπαθούμε να σκιαγραφήσουμε ευκρινώς τη συνολική επίδραση του θεωρήματος στα μαθηματικά και όχι μόνο. Για την ακρίβεια, αναφερόμαστε στην πληρότητα της Ευκλείδειας γεωμετρίας ως συνέπεια του θεωρήματος, στη συμβολή του θεωρήματος στην ανάπτυξη της ημιαλγεβρικής γεωμετρίας. Στο δεύτερο κεφάλαιο αποδικνύεται το εν λόγω θεώρημα, δηλαδή ότι η πρωτοβάθμια θεωρία των πραγματικώς κλειστών σωμάτων είναι πλήρης, με χρήση των θεωρημάτων Sturm και Sylvester. Στο τρίτο κεφάλαιο παρουσιάζεται μία διδακτική έρευνα με φοιτητές του τμήματος με σκοπό τη διάγνωση πιθανών γνωστικών κενών των φοιτητών σε θέματα της θεωρίας πολυωνύμων με πραγματικούς συντελεστές. / To study object of this work is a fortiori the Tarski-Seidenberg theorem. In the first chapter we study Tarski's motivation in this research, we recount the progress of the idea from ​​the discovery until the publication, and then we try to outline clearly the overall effect of the theorem in mathematics and beyond. In fact, we refer to the completeness of Euclidean geometry as a consequence of the theorem, in its contribution to the development of semialgebraic geometry. In the second chapter we prove the Tarski-Seidenberg theorem, namely that the first order theory of real closed fields is actually complete, using the Sturm and Sylvester theorems. In the third chapter we present a teaching research on students of the Department in purpose to diagnose potential knowledge gaps of the students concerning the theory of polynomials with real coefficients.