Here, we analyse some recent applications of set theory to topology and argue that set theory is not only the closed domain where mathematics is usually founded, but also a flexible framework where imperfect intuitions can be precisely formalized and technically elaborated before they possibly migrate toward other branches. This apparently new role is mostly reminiscent of the one played by other external fields like theoretical physics, and we think that it could contribute to revitalize the interest in set theory in the future.

§1. Introduction. Natural sets that can be enumerated by a computable function (the recursively enumerable or r.e. sets) always seem to be either actually computable (recursive) or of the same complexity (with respect to Turing computability) as the Halting Problem, the complete r.e. set K. The obvious question, first posed in Post [1944] and since then called Post's Problem is then just whether there are r.e. sets which are neither computable nor complete, i.e., neither recursive nor of the same Turing degree as K?

Let be the r.e. degrees, i.e., the r.e. sets modulo the equivalence relation of equicomputable with the partial order induced by Turing computability. This structure is a partial order (indeed, an uppersemilattice or usl)with least element 0, the degree (equivalence class) of the computable sets, and greatest element 1 or 0′, the degree of K. Post's problem then asks if there are any other elements of .

The (positive) solution of Post's problem by Friedberg [1957] and Muchnik [1956] was followed by various algebraic or order theoretic results that were interpreted as saying that the structure was in some way well behaved:

Theorem 1.1 (Embedding theorem; Muchnik [1958], Sacks [1963]). Every countable partial ordering or even uppersemilattice can be embedded into .

Theorem 1.2 (Sacks Splitting Theorem [1963b]). For every nonrecursive r.e. degreeathere are r.e. degreesb, c < asuch thatb ∨ c = a.

Theorem 1.3 (Sacks Density Theorem [1964]). For every pair of nonrecursive r.e. degreesa < bthere is an r.e. degreecsuch thata < c < b.

Introduction. Il est bien connu que la correspondance de Curry-Howard permet d'associer un programme, sous la forme d'un λ-terme, à toute preuve intuitionniste, formalisée dans le calcul des prédicats du second ordre (voir, par exemple [3]). Cette correspondance a été étendue, assez récemment, à la logique classique moyennant une extension convenable du λ-calcul (voir [1, 4, 5, 6]). Chaque théorème formalisé en logique du second ordre correspond donc à une spécification de programme.

Il se pose alors le problème, en général tout à fait non trivial, de trouver la spécification associée à un théorème donné; autrement dit, de déterminer le comportement opérationnel commun aux λ-termes associés aux diverses démonstrations formelles du théorème considéré.

Cette question est résolue ici pour le théorème de complétude de la logique classique.

La première étape consiste à formaliser convenablement ce théorème en logique du second ordre. Ce travail est fait complètement dans la section 1. Il a comme sous-produit, peut-être inattendu, de montrer que ce théorème est prouvable en logique intuitionniste du second ordre (section 2). Ceci, toutefois, à condition d'introduire une légère variante de la notion de modèle, en admettant un modèle supplémentaire trivial, où toute formule est satisfaite.

On notera, à ce sujet, que des preuves intuitionnistes du théorème de complétude de la logique intuitionniste, utilisant des variantes de la notion de modele de Kripke, ont été données par H. Friedman [7] et W. Veldman [8]. On remarquera également qu'un argument de G. Kreisel [2] montre que le théorème de complétude habituel de la logique intuitionniste n'a pas de preuve intuitionniste.

We introduce a new framework for classifying logics on finite structures and studying their expressive power. This framework is based on the concept of almost everywhere equivalence of logics, that is to say, two logics having the same expressive power on a class of asymptotic measure 1. More precisely, if L, L′ are two logics and μ is an asymptotic measure on finite structures, then L ≡a.e.L′ (μ) means that there is a class C of finite structures with μ(C) = 1 and such that L and L′ define the same queries on C. We carry out a systematic investigation of ≡a.e. with respect to the uniform measure and analyze the ≡a.e.-equivalence classes of several logics that have been studied extensively in finite model theory. Moreover, we explore connections with descriptive complexity theory and examine the status of certain classical results of model theory in the context of this new framework.