Main Awards Registration Accommodation Social Program Map of Helsinki
Conference Timetable Contributed Papers Committees Mailing List Sponsors ASL

Speakers and Titles

Tutorial speakers

Michael Benedikt, Model Theory and Complexity Theory
Bell Labs, Lisle, USA.

ABSTRACT: This tutorial concentrates on links between traditional (infinitary) model theory and complexity theory. We begin with an overview of the `classical' connection between complexity theory and finite model theory, giving quickly the basic results of descriptive complexity theory. /We then discuss several ways of generalizing this to take account a fixed infinite background structure. We will start by giving the basics of complexity theory parameterized by a model (algebraic complexity over an arbitrary structure). We then cover results characterizing first-order theories of models via the complexity of query problems (embedded finite model theory). Finally, time permitting, we will look at abstractions of descriptive complexity theory to take into account a background structure.

Stevo Todorcevic, Set-Theoretic Methods in Ramsey Theory
C.N.R.S. - UMR 7056, Paris, France.

ABSTRACT: We shall start with an overview of some of the basic pigeon-hole principles of Ramsey theory such as the Halpern-Lauchli or the Hales-Jewett theorems. We shall present then a general method for getting the higher-dimensional analogues of these principles. We shall finish with some applications to the Banach space theory such as Gowers' c0-theorem or Rosenthal's l1-theorem.'

Plenary Speakers

Alexandru Baltag, Doing Things to Models: Trans-Structural Dynamic Logics
Oxford University (Computing Laboratory), Oxford, UK

ABSTRACT: The title is not referring to sub-structural logics, which bear no relation or similarity to my subject. The word "trans-structural" refers to the fact that the semantics of such logics transcends the current structure on which they are defined, their current "model": these logics contain propositional connectives, modalities or quantifiers whose semantics refers to other models than the one on which they are defined. These logical operators can be interpreted dynamically, as talking about "ways to transform/change/update the current model". Such operators provide ways to capture inherent properties of the model in an indirect manner, by referring to properties of the model's possible modifications. These logics can be thus seen as a "dynamification" of model-theoretic semantics, in which the dynamic (relational, Kripke-style) possible-world semantics is applied to the level of models, instead of the level of states in a single model.

I give examples of such operators, all from very recent literature (as the subject is rather new): the "entailment (or implication) along a model-theoretic relation" (due to Barwise/van Benthem), the "bisimulation quantifiers" (due to G. d'Agostino and M. Hollenberg), the modal logic of "relativisation" (or "public announcement", due to J. Gerbrandy and J. Plaza, and formalised as a trans-structural modality by L. Moss and myself) and, more generally, the "epistemic-action" modalities (introduced by myself and L. Moss to model communication in multi-agent systems). I point to the relations between some of these notions and non-standard versions of the standard logical results of interpolation, preservation and definability. I discuss peculiarities of these logics, e.g. their essential lack of "strong compositionality" (in spite of their "weak" compositionality: the meaning of a formula in a model cannot be defined in terms of the meanings of its subformulas in the SAME model), I mention some completeness, decidability and undecidability results for some of these logics, I discuss their relations with other logics and I give a list of open problems.

Howard S. Becker, Generalized model theory and Polish group actions
University of South Carolina, Columbia, USA.

ABSTRACT: Most of the model theory of the language L\omega1,\omega and countable structures can be rephrased in group action terminology, with respect to the logic action by the group of permutations of the integers. We generalize these results to other actions by other Polish groups.

Zoé Chatzidakis, Asymptotic theories of fields
CNRS -University of Paris 7, Paris Cedex 05, France.

ABSTRACT: Families of fields (maybe with additional structure) are often defined in terms of prime numbers. The simplest example is the family of all fields with p elements (denoted Fp), as p ranges over the set of all prime numbers. James Ax studied in 1968 the asymptotic theory of these fields, i.e., the set of sentences in the language of rings which hold in all but finitely many of the fields Fp, gave an axiomatisation of this theory and showed that it was decidable. The famous results of Ax and Kochen (1965, 1966) show that the asymptotic theory of the valued fields of p-adic numbers Qp and the asymptotic theory of the valued fields Fp((t)) (formal power series over Fp) coincide; Ax's result then implies that this theory is decidable .

In the past few years, other asymptotic theories were investigated, usually yielding decidability results. Maybe the most striking example is the asymptotic theory of the fields ˜Fp, sp), where ˜Fp denotes the algebraic closure of Fp, sp is an additional unary function predicate, interpreted as the Frobenius map x |-> xp (Recall that in any field of positive characteristic p, the Frobenius map defines an injective, not necessarily surjective, homomorphism). Hrushovski showed that this asymptotic theory is decidable and model complete (and in fact coincides with the model companion of the theory of fields with a distinguished automorphism). This result was announced independently by Macintyre.

In this talk, I will survey the classical results, and list a few recent examples of asymptotic theories of fields with decidable theories. I will conclude with an example of an asymptotic theory, whose existential part is \Sigma20-complete.

Matthew Foreman, Has the CH been settled?
University of California, Irvine, USA.

ABSTRACT: A collection of generalized large cardinal axioms are presented that provide a reasonably complete picture of the set theoretic universe, deciding the CH, the existence of Suslin trees, Kurepa trees, ADL(R) and many other problems. Most of the results have been known for a long time, but new results are presented and the old results are put in context.

Jean-Yves Girard, From operator algebras to logic
IML, UPR 9016, Marseille, France.

ABSTRACT: We discuss the interpretation of logical laws by means of operators acting on Hilbert space. The case of the finite matricial factor is of special interest.

Martin Grohe, The Succinctness of Monadic Logics on Finite Trees
Humboldt-University of Berlin, Berlin, Germany.

ABSTRACT: A central topic in finite model theory has always been the expressive power of logics on finite relational structures. However, in some situations of practical interest we have to compare logics of the same expressive power. In particular, there is great interest in a variety of logics on finite trees that all characterise precisely the regular tree languages and thus have the same expressive power as monadic second-order logic.

Succinctness is a natural refined measure for the strength of a logic. For a class F of functions on the natural numbers, we call a logic L F-succinct in a logic L' if for every L-formula A there is an equivalent L'-formula A' and a function f \in F such that size(A') <= f(size(A)).

In this talk I will present recent results on the succinctness of first-order logic, monadic second-order logic, and a number of fixed-point logics on finite words and trees.

(This is joint work with Nicole Schweikardt.)

Peter T. Johnstone, A survey of realizability toposes
DPMM, Cambridge, United Kingdom.

ABSTRACT: The notion of realizability topos has been around for over tewnty years now: numerous variants of the basic construction of a topos from a Schönfinkel algebra (or PCA) have been studied, and many different examples of Schönfinkel algebras have been considered. However, until recently (with the notable exception of John Longley's Ph.D. thesis) there has been relatively little work on how these different examples fit together: we do not have a well- understood 2-category of realizability toposes in the same way that we have a well-understood 2-category of Grothendieck toposes. I believe that the time is now ripe for the development of such an understanding: in this talk I shall attempt to give some indications of what we already know, and what we might hope to learn, about morphisms between realizability toposes.

Simo Knuuttila, On the history of modality as alternativeness
University of Helsinki, Helsinki, Finland.
E-mail: sknuutti@Teologi.Helsinki.FI

ABSTRACT: There are four modal paradigms in ancient philosophy: the `statistical' or `temporal frequency' interpretation of modality, the model of possibility as a potency, the model of antecedent necessities and possibilities with respect to a certain moment of time (diachronic modalities) and the model of possibility as non-contradictoriness. None of these conceptions, which were well known to early medieval thinkers through the works of Boethius, was associated with the idea of modality as involving reference to simultaneous alternatives. This new paradigm was included in Augustine´s theological conception of God as acting by choice between alternative histories and similarly in some Arabic theological theories. Ancient habits of thinking continued to play an important role in scholasticism, and the theoretical significance of the new conception was not fully realized before the works of John Duns Scotus and other early fourteenth century thinkers, such as William Ockham and John Buridan.

Many scholars have recently remarked that the notions of necessity and possibility were treated in fourteenth century modal logic and modal theory in a way which is analogous to the contemporary possible worlds semantics. I shall discuss the principles of the new fourteenth-century modal logic and how this differed from thirteenth century interpretations of Aristotle´s modal syllogistic. Second, I shall deal with John Buridan´s discussion of Aristotle´s indirect proofs and with some other fourteenth century thinkers´ theories of counterfactual reasoning based on the new theory of modality as alternativeness. These authors contrasted their approaches to counterfactual reasoning with those of Averroes and Thomas Aquinas which did not operate with the idea of alternative domains but instead with abstract essentialist modalities. I conclude with remarks on this controversy.

Menachem Kojman, On the role of infinite cardinals
Ben Gurion University, Beer Sheva, Israel.

ABSTRACT: The talk will address the role infinite cardinals and infinite cardinal arithmetic have in mathematics and survey several recent results from topology, combinatorics and geometry in which infinite cardinals play a role, to demonstrate various aspects of the topic.

Michael C. Laskowski, Applications of descriptive set theory to uncountable model theory
University of Maryland, College Parkmd, USA.

ABSTRACT: Fix a complete theory T in a countable language. All of Shelah's stability-theoretic technology for analyzing the UNCOUNTABLE models of T can be described in terms of which COUNTABLE configurations of elements embed into models of T. Recent work has highlighted the utility of examining the descriptive set-theoretic complexity of these notions, either in general or in specific instances. This talk will survey the role played by such methods in computing the uncountable spectrum of such a theory (which was joint work with Hart and Hrushovski) and discuss recent work with Shelah on the Main Gap for aleph-one saturated models, which also employs descriptive set-theoretic technology.

Larisa Maksimova, Decidable properties of logical calculi and of varieties of algebras
Siberian Branch of Russian Academy of Sciences, Novosobirsk, Russia.

ABSTRACT: We give an overview of decidable and strongly decidable properties over the propositional modal logics K, GL, S4, S5 and Grz, and also over the intuitionistic logic Int and the positive logic Pos. A property P is said to be decidable over a calculus L if there is an algorithm which, for any finite set Ax of additional axiom schemes, decides if the calculus L+Ax possesses the property P; P is said to be strongly decidable over L if there is an algorithm which, for any finite set Rul of additional axiom schemes and rules of inference, decides if the calculus L+Rul has the property P.

We consider a number of important properties of logical calculi: consistency, tabularity, pretabularity, local tabularity, various forms of interpolation and of the Beth property. For instance, consistency is decidable over K and strongly decidable over S4 and Int; tabularity and pretabularity are decidable over S4, Int and Pos; interpolation is decidable over S4 and Pos and strongly decidable over S5, Grz and Int; the projective Beth property is decidable over Int, Pos and Grz, etc. Some complexity bounds are found.

In addition, we state that tabularity and many variants of amalgamation and of surjectivity of epimorphisms are base-decidable in varieties of closure algebras, of Heyting algebras and of relatively pseudocomplemented lattices.

Per Martin-Löf, Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic?
University of Stockholm, Stockholm, Sweden.

Dag Normann, The continuous functionals in the perspective of domain theory
University of Oslo, Oslo, Norway.

ABSTRACT: In the 70'ies and early 80'ies the continuous functionals were primarily studied as a hierarchy of total functionals, and the prime notion of computability was based on Kleene's S1 - S9. Domain theory originated from Scott and Ershov. Scott's original motivation was to construct a typed hierarchy of partial continuous functionals with a Platek-inspired notion of computability. The domain-theoretical approach leads to an equivalent hierarchy of hereditarily total functionals, but to alternative notions of computability. One advantage of the domain-theoretical approach is that we may use domain-representations of the reals or other spaces, and then consider additional base types. This has e.g. been used for the semantics of typed languages for exact real-valued computations. We will discuss some advances that have been made over the recent years on the continuous functionals of higher types over the natural and real numbers and corresponding notions of computability.

Graham Priest, Inconsistent arithmetics and inconsistent computation
University of Melbourne, Melbourne, Australia.

ABSTRACT: The structure of inconsistent arithmetics is well known. (See Priest (2000).) Some of these arithmetics are axiomatisable, but can prove their own ``Gödel sentences''. This fact, in turn, can be used as an argument to the effect that such an arithmetic is the true arithmetic. (See Priest (1987), ch. 3.) Shapiro (2002), points out that the inconsistencies of such an arithmetic must occur ``even in its most elementary'' part - essentially the computational part - and argues that this is unacceptable. This paper examines Shapiro's arguments. It argues that the problems arise only if one marries an inconsistent arithmetic with a consistent theory of computation. If one marries an inconsistent arithmetic with an inconsistent theory of computation (which the arithmetic itself shows us how to construct), the problems Shapiro envisages do not arise.

G. Priest (1987), In Contradiction, Dordrecht: Kluwer Academic Publishers.

G. Priest (2000), Inconsistent Models of Arithmetic II; the General Case, Journal of Symbolic Logic 65, 1519-29.

S. Shapiro (2002), Inconsistency and Incompleteness, Mind 111, 817-832.

Pavel Pudlák, Consistency and games
Academy of Sciences, Praha, Czech Republic.

ABSTRACT: The statement that a weak formal system is consistent should be equivalent to a simple combinatorial principle. I will report on some results about this problem. The formal systems that we studied are proof systems for propositional calculus and subtheories of Bounded Arithmetic. We found formal statements about strategies for playing several finite games simultaneously which are closely related to the consistency of these systems. We found also interesting computational problems about such strategies.

Michael Rathjen, Realizability, Forcing, and Independence Results for Constructive Theories
University of Leeds and Ohio State University, Columbus, USA.

ABSTRACT: An important techniques for achieving independence and consistency results for intuitionistic theories is realizability. While there exist detailed accounts of realizability interpretations for arithmetic and analysis, a synopsis of different notions of realizability for the more general frameworks of type theory and set theory has rarely been undertaken.

In this talk I shall survey several notions of realizability for constructive type and set theories such as Kleene realizability, formulae-as-types interpretation based on E-recursive functions, and realizability in Kripke-Platek set theory. These realizability interpretations are then employed to obtain independence and equiconsistency results.

The most famous method for showing independence of statements from axiom systems in the classical context is Cohen's method of forcing or the closely related technique of Boolean-valued models. Forcing has been developed for intuitionistic set theories as as well, in particular for intuitionistic Zermelo-Fraenkel set theory, IZF. In this context, forcing models are closely related to Heyting-valued models as well as sheaf models. However, to obtain specific independence results, I shall focuss on particular forcing constructions (due to Lubarsky), where the underlying partial order is a class and one utilizes techniques from classical set-theoretic forcing as well as techniques that are germane to the classical constructible hierarchy L such as \Sigma1 Skolem hull and condensation arguments.

Saharon Shelah, Good frames, for what are they good?
The Hebrew University, Jerusalem, Israel.

ABSTRACT: The aim of the lecture is to show how we can get good frames starting from an abstract elementary class which is categorical in a large enough cardinal (but in ZFC!). We think this will lead to reasonable understanding of the categoricity spectrum in large enough cardinals. But probably the reader needs more background. An abstract elementary class is e.g the class of models of a first order theory omitting some types with the usual notion of an elementary submodel. A good frame s is a mini version of a superstable first order theory; we have an abstract elementary class \Kappa, a fixed cardinal \lambda in which \Kappa has amalgamation, a set of basic types over models in \lambda and for them a notion of non-forking for such types. The restriction to one cardinal makes a difference. Now [5], [1], and [2] did the parallel of [3], [4] (+ justification of "good frames are like superstable first order theory"). Essentially, assuming enough instances of weak GCH, when an abstract elementary class \Kappa is categorical in \lambda , \lambda+ (and has a model in \lambda++) we get a good frame and assuming not too many models in the \lambda+n we arrive at a parallel to excellent classes. A consequence is: If \Kappa is categorical in a large enough cardinal then it is categorical in every large enough cardinal, when \Kappa is: (a) an abstract elementary class with amalgamation or (b) (Mod(T),\prec),T\subseteq{\Bbb L}\kappa , \omega, \kappa measurable.


[1] Saharon Shelah. Categoricity in abstract elementary classes: going up inductive step. Preprint math.LO/0011215.

[2] Saharon Shelah. Toward classification theory of good \lambda frames and abstract elementary classes.

[3] Saharon Shelah. Classification theory for nonelementary classes, i. the number of uncountable models of \psi \in l\omega 1,\omega. part a. Israel Journal of Mathematics, 46:212--240, 1983.

[4] Saharon Shelah. Classification theory for nonelementary classes, i. the number of uncountable models of \psi \in l\omega 1,\omega. part b. Israel Journal of Mathematics, 46:241--273, 1983.

[5] Saharon Shelah. Categoricity of an abstract elementary class in two successive cardinals. Israel Journal of Mathematics, 126:29--128, 2001. math.LO/9805146.

Richard A. Shore, The boundary between decidability and undecidability in degree structures
Cornell University, Ithaca NY, USA.

ABSTRACT: Very early reserach suggested and sought decidability results for many degree structures. Although the lowest levels (in quantifier complexity) were shown decidable, most structures turned out to be highly undecidable. Finding the precise diving line between decidability and undecidability provides a setting for formulating the extent of our knowledge of, and control over, the notion of relative computability in different settings. Older results typically showed the two quantifier level decidable and the third undecidable. We examine the situation for the r.e. degrees, the degrees below 0' and the structure of all the Turing degrees when the language is expanded to include join and infimum or (for all the degrees) the Turing jump. The border now typically moves to between the first and second quantifier level with new theorems and needed for both types of results and new problems and questions coming to light.

Special Sessions

Model Theory

Tuna Altinel, Simple groups of finite Morley rank
Universite Claude Bernard Lyon-1, Villeurbanne, France.

ABSTRACT: The Cherlin-Zil'ber conjecture states that an infinite simple group of finite Morley rank is a linear algebraic group over an algebraically closed field. Various approaches to this conjecture have been developed over the years from both model theoretic and group theoretic sides.

On the group theory side, the presence of a well-developed Sylow 2-theory and various finiteness conditions permitted the use of finite group theoretic ideas, and it has been possible to adapt techniques from the classification of the finite simple groups. The context where these techniques have been the most efficient has been the context of simple K*-groups. The notion of K*-group, a group of finite Morley rank all of whose infinite definable simple and proper sections are algebraic groups over algebraically closed fields, was introduced to set firm grounds for an analogue of the revisionist approach to the classification of the finite simple groups, and has made it possible to carry out a systematic analysis of various classes of simple groups of finite Morley rank. As a result, the algebraicity conjecture has been verified for the simple K*-groups that have infinite 2-subgroups of bounded exponent.

A weakness of the notion of K*-group is the strength of its definition. In order to arrive at a classification statement free of an inductive hypothesis one needs to verify that the Cherlin-Zil'ber conjecture holds for all the simple K*-groups of finite Morley rank. In my talk, I will discuss a broader inductive notion which is most relevant in the context of simple groups that have infinite 2-subgroups of bounded exponent. Indeed, if this approach succeeds then the Cherlin-Zil'ber conjecture will be verified for all simple groups of finite Morley rank that have infinite 2-subgroups of bounded exponent. As important as this potential success are the new ideas and techniques which have been introduced to tackle various technical difficulties in the new context and bring closer the model theoretic and group theoretic sides in the area. Part of my talk will be devoted to exposing these new methods.

Tapani Hyttinen, Random logarithm: An example of a homogeneous class of structures
University of Helsinki, Helsinki, Finland.

ABSTRACT: We give an example of a non-elementary class of structures, which is homogeneous for non-trivial reasons and which arises from classical mathematics. In addition, a model theoretic classification of the class is given.

Ludomir Newelski, Lascar strong types and topology
Wroclaw University, Wroclaw, Poland.

ABSTRACT: Assume M is a sufficiently saturated and homogeneous model (a monster model). We define on M some canonical equivalence relations:
ES is the intersection of all 0-definalbe equivalence relations on M with finitely many classes;
EKP is the finest 0-type-definable equivalence relation on M with bounded (that is, <= 2|T|) number of classes;
EL is the finest equivalence relation on M invariant under Aut(M) (as a subset of M x M) and with bounded number of classes.

So EL refines EKP and EKP refines ES. The classes of ES are called (Shelah) strong types, the classes of EKP Kim-Pillay strong types and the classes of EL Lascar strong types. In stable theories all these relations and strong type notions coincide. In simple theories EKP equals EL, while it is open if they equal also ES there. There are only a few examples where EL and EKP differ (the first was found by Ziegler).

In 2002 I answered most questions from [1] on the structure of Lascar strong types, particularly referring to their type-definability and to the structure of the Lascar group GalL(M) = Aut(M)/AutfL(M), where AutfL(M) is the poinwise stabilizer in Aut(M) of M/EL. I obtained also some general results on elimination of hyperimaginaries and on invariant equivalence relations, extending some ideas on genericity from stable theories to arbitrary ones (see also my contributed talk join with M.Petrykowski).

There are still some questions on Lascar strong types motivated by the classification of Borel equivalence relations, since EL regarded on the level of types is Borel.

The main new tool in the proofs is the notion of an open analysis of a compact space with respect to its covering by a family of subsets. This yields a new way of proving some finiteness results in model theory (not referring to the compactness theorem) and generalizes the Cantor-Bendixson analysis and the Baire category theorem. Everything here is elementary and does not require any knowledge of advanced model theory.

[1] E.Casanovas, D.Lascar, A.Pillay, M.Ziegler, Galois groups of first order theories, J.Math.Logic 1(2001), 305-319.

[2] L.Newelski, The diameter of a Lascar strong type, Fund.Math. 176(2003), 157-170.

Wai Yan Pong, The Differential Order
California State University, Carson, USA.

ABSTRACT: Differential Order is a model theoretic rank that generalizes the concept of the order of a differential polynomial. We will discuss its application in differential algebra and its relation with other ranks. This is a joint work with Matthias Aschenbrenner.

Set Theory

Arthur W. Apter, Indestructibility and Strong Compactness
Baruch College of CUNY, New York, USA.

ABSTRACT: I will discuss forcing indestructibility for non-supercompact strongly compact cardinals, emphasizing the construction of a model in which the first two strongly compact cardinals aren't supercompact yet satisfy significant indestructibility properties. I will also mention the problems that seem to be inherent in trying to extend both this result and results of a similar nature.

Steve Jackson, Some applications of cubical markers
University of North Texas, Denton, USA.

ABSTRACT: We use the existence of cubical markers for equivalence relations generated by actions of Zn to obtain new results and new proofs for these equivalence relations and others.

Heike Mildenberger, New canonization theorems and dense free subsets in \aleph\omega.
University of Vienna, Vienna, Austria.

ABSTRACT: In the talk I will sketch the forcing construction, starting from \omega compact cardinals, of a model of ZFC where every structure with countable signature and domain \aleph\omega has a free subset which hits every infinite cardinal interval. Combinatorics in ZFC shows that a denser distribution of members of free subsets cannot be obtained.

Maurice C. Stanley, Outer models and genericity
San Jose State University, Tracy, USA.

ABSTRACT: If V is a standard transitive model of ZFC, say that a transitive W\supseteq V is an outer model of V if W contains the same ordinals as V and if (W,V) satisfies ZFC in a language with a predicate symbol for V. Why is forcing the only known method for constructing outer models? How strong is generic absoluteness? We approach these questions by characterizing those outer models of a given model that are set generic and those that are class generic in each of two senses.

Recursion Theory and Arithmetic

Klaus Ambos-Spies, Generators of the computably enumerable degrees
University of Heidelberg, Heidelberg, Germany

ABSTRACT: We will survey some older results and present some new results on generators of the computably enumerable (c. e.) degrees. We will focus on the role played by the meet operator in the process of generating (subclasses of the) c.e. degrees under join and meet. In particular we will address the question whether every set of degrees which generates the c. e. degrees under join and meet will generate the nonzero c. e. degrees under join. We have raised this questions in a paper of 1985 where we had shown that every generator of the c. e. degrees intersects all nonzero initial segments. Our main results are that every generator of the c. e. degrees also generates the high c. e. degrees under join (joint work with D. Ding and P. A. Fejer) but that there is a generator of the c. e. degrees which does not generate the nonzero c. e. degrees under join (joint work with S. Lempp and T. A. Slaman).

Oleg V. Kudinov, Computable listings and autodimensions of rings and fields
Siberian Division of RAS, Novosibirsk, Russia.

ABSTRACT: There are several methods to code computable families of computably enumerable sets or computable graphs in computable integral domains - one of them was proposed by author in 1997 to prove the following

Theorem: There exists a computable integral domain with exactly two nonequivalent computable presentations.

Since for fields the similar problem is still open, it would be natural to describe the index sets of the classes of computably categorical (autostable) fields and fields of infinite autodimension. The reasonable conjecture states that the index set of the first class is \Pi^1_1-complete.

The next result deals with fields of algebraic numbers.

Theorem: The index set of autostable fields of algebraic numbers of zero characteristic is \Pi^0_4-complete.

The general case is very hard since we need a lot of autostable fields F with infinite ranktr(F). However, for the class of integral domains the description of correspondig index set is closely related to the following result.

Theorem: The index set of autostable graphs is \Pi^1_1-complete.

It is worth to note that index sets of the classes of fields are defined via classical computable enumeration of the class of semicomputable commutative rings. We can not define them via suitable computable enumeration of computable fields as the following result states.

Theorem: There does not exist a computable listing of all the class of computable fields of zero characteristic up to isomorphism.


[K1] M. Kummer: Some applications of computable one-one numberings, Arch. Math. Logic, 30 (1990), 219--230.

[A2] M. Kummer, S. Wehner, Xiao-Ding Yi: Discrete families of recursive functions and index sets, Algebra and Logic, 33 (1994), 85--94.

Chris Pollett, Weak Arithmetics and Unrelativised Independence Results
San Jose State University, San Jose, USA.

ABSTRACT: In this talk I will survey some techniques which can be used to show unrelativized independence results for questions like NP vs coNP, the collapse of the polynomial hierarchy, or Hilbert's Tenth Problem in weak systems of arithmetic. I will also present some new results concerning the limits of formalizing padding arguments in commonly studied weak arithmetics.

John V. Tucker, Specification and computation on topological algebras
University of Wales Swansea, Swansea, United Kingdom.

ABSTRACT: We consider computability theory for infinite data, such as real numbers, signals and wave forms, streams, spatial objects, and functions. Usually, such data is collected into topological spaces and so we consider models of computation for functions and sets on topological spaces.

The many models fall into two types. First, there are concrete models of computation which depend on building a representation of the space of data, usually from the natural numbers, and defining computability on the space in terms of computability on the representation. This is the standard approach of Computable Analysis starting in the 1950s; it is used in current work based on Pour El and Richards´ computation structures, Klaus Weihrauch´s TTE, Stoltenberg-Hansen, Tucker and Edalat´s domain representations, and Spreen´s effective topology.

Secondly, there are abstract models that define computability independently of all representations. The spaces are given algebraic structure (e.g., that of a Banach space) and programs and machines are based on the structure. Thus, computation is abstract in precisely the way algebra is abstract: computation is invariant under isomorphism. This is the approach of many generalisations of recursion theory starting in the 1950s; it is used in some current work by S Smale and his collaborators (on rings and fields) and J I Zucker and J V Tucker (on many sorted universal algebras).

The lecture will discuss some current results and problems, especially on the equivalence of the concrete and abstract models. Recent results of Tucker and Zucker show that equivalence requires programmable approximations of partial multivalued functions on topological algebras.

We will also mention applications to
(i) specifying and programming in the growing practical field of exact real number computation, and
(ii) long standing problems to do with machines and the analogue-digital interface.

Some background can be found in Stoltenberg-Hansen and Tucker[1995, 1999], and Tucker and Zucker[2000].


V Stoltenberg-Hansen and J V Tucker, Effective algebras, in S Abramsky, D Gabbay and T Maibaum (eds.) Handbook of Logic in Computer Science. Volume IV, Oxford University Press, 1995, pp.357-526.

V Stoltenberg-Hansen and J V Tucker, Computable rings and fields, in E Griffor (ed.), Handbook of Computability Theory, Elsevier, 1999, pp.363-447.

J V Tucker and J I Zucker, Computable functions and semicomputable sets on many sorted algebras, in S. Abramsky, D. Gabbay and T Maibaum (eds.) Handbook of Logic for Computer Science Volume V, Oxford University Press, 2000, pp. 317-523.

Proof Theory and Non-classical Logic

Ralph Matthes, Inductive Constructions for Classical Natural Deduction

ABSTRACT: Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. We present an approach based on reducibility candidates that involve non-strictly positive inductive definitions.

It also covers the extension of the logic by least and greatest fixed-points of monotone operators, which appears to be a new result.

An informal realizability interpretation yields an embedding of Parigot's second-order lambda-mu-calculus into second-order lambda-calculus (published at TLCA 2001). We discuss how this could be extended to disjunctions.

Finally, the relation to Parigot's strictly-positive inductive definition of his set of reducibility candidates is explained.

Erik Palmgren, Problems of predicativity in constructive topology
Uppsala University, Uppsala, Sweden.

ABSTRACT: The theory of locales provides a framework for constructive general topology, albeit in impredicative settings such as toposes or higher order logics. It has been recognised that much of the theory can be carried out in constructive type theory or set theory, predicatively, without using full separation principles. The main idea of this theory, formal topology, is to generate the open cover relation inductively. It appeared in the doctoral thesis of Per Martin-Löf 1970, and has been investigated by Sambin, Aczel, Coquand and their associates. Formal topology avoids some known artificialities of the definition of continuous function present in the metric theory advocated by Bishop. Lacking the separation principle the distinction of small versus large type (set versus class) enters in unexpected and unwellcome places. For instance neither the points of a formal topological space, nor the continuous functions between such spaces, need to form a set. We survey results of G. Curi and Aczel and present some new methods of proving smallness, which use topological properties as well as predicative type-theoretic principles: a general dependent choice principle and type universe operators. An important problem is to find a predicatively well-defined category with sufficiently good closure properties for carrying out standard constructions of algebraic and differential topology.

Jeff Paris, Uncertain reasoning
Manchester University, Manchester, United Kingdom.

ABSTRACT: In the real world we can rarely enjoy the luxury of drawing definitive conclusions from our knowledge. Indeed even our knowledge itself is usually tainted with some degree of uncertainty. Nevertheless the real world demands action, we usually do not have the option of saying that we cannot decide and will therefore simply refuse to do anything.

This has led to logics, or patterns of reasoning, with such knowledge that allow rules of proof which go beyond simple `truth preservation' and take instead their justification from considerations of `rationality'. I shall describe one such approach along with some of its surprising, and for the most part, welcome, consequences.

Tarmo Uustalu, Type-based termination of recursive definitions
Institute of Cybernetics, Tallinn, Estonia.
E-mail: (removed)

ABSTRACT: We describe an approach to supplementing a type assignment system with inductive and coinductive constructors where the recursors and corecursors compute almost as general recursion operators, but their typing rules ensure that the system stays strongly normalizing and is sound with respect to the expected initial algebra, final coalgebra semantics. This way of directly supporting sophisticated structured (co)recursive definitions is radically different from that of syntactic guardedness conditions. The simplest instance appeared in the systems of N. P. Mendler's LICS'87 / APAL'91 paper, but the underlying principle, once explicated, gives the approach a much wider scope.

Besides considering (co)inductive types in a simply typed system, we discuss (co)inductive constructors of higher kinds and a setting of dependent typing.
University of Helsinki Dept. of Mathematics Helsinki City Tourist Office