Main | Awards | Registration | Accommodation | Social Program | Map of Helsinki |

Conference Timetable | Contributed Papers | Committees | Mailing List | Sponsors | ASL |

Bell Labs, Lisle, USA.

E-mail: benedikt@research.bell-labs.com

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.

E-mail: stevo@math.jussieu.fr

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' *c _{0}*-theorem or Rosenthal's

Oxford University (Computing Laboratory), Oxford, UK

E-mail: Alexandru.Baltag@comlab.ox.ac.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.

E-mail: becker@math.sc.edu

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.

E-mail: zoe@logique.jussieu.fr

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 **F**_{p}),
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 **F**_{p},
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 **Q**_{p}
and the asymptotic theory of the
valued fields **F**_{p}((*t*))
(formal power series over **F**_{p})
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 **˜F**_{p},
s_{p}), where **˜F**_{p} denotes the algebraic closure of
**F**_{p},
s_{p} is an additional unary function predicate, interpreted as
the Frobenius map *x |-> x ^{p}*
(Recall that in any field of positive
characteristic

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
\Sigma_{2}^{0}-complete.

**Matthew Foreman**, *Has the CH been settled?*

University of California, Irvine, USA.

E-mail: mforeman@math.uci.edu

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, *AD ^{L(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.

E-mail: girard@iml.univ-mrs.fr

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.

E-mail: grohe@inf.ed.ac.uk

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.

E-mail: ptj@dpmms.cam.ac.uk

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.

E-mail: kojman@math.bgu.ac.il

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.

E-mail: mcl@math.umd.edu

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.

E-mail: lmaksi@math.nsc.ru

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.

E-mail: pml@math.su.se

**Dag Normann**,
*The continuous functionals in the perspective of domain theory*

University of Oslo, Oslo, Norway.

E-mail: dnormann@math.uio.no

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.

E-mail: g.priest@unimelb.edu.au

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.

E-mail: pudlak@math.cas.cz

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.

E-mail: rathjen@math.ohio-state.edu

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 \Sigma_{1} Skolem hull and condensation arguments.

**Saharon Shelah**, *Good frames, for what are they good?*

The Hebrew University, Jerusalem, Israel.

E-mail: shelah@math.huji.ac.il

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

**References**

[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.

[4] Saharon Shelah. Classification theory for nonelementary classes, i. the number of
uncountable models of *\psi \in l _{\omega 1,\omega}*. part b.

[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.

E-mail: shore@math.cornell.edu

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.

**Tuna Altinel**, *Simple groups of finite Morley rank*

Universite Claude Bernard Lyon-1, Villeurbanne, France.

E-mail: altinel@igd.univ-lyon1.fr

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 ^{*}*-

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

**Tapani Hyttinen**, *Random logarithm: An example of a homogeneous class of structures*

University of Helsinki, Helsinki, Finland.

E-mail: tapani.hyttinen@helsinki.fi

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.

E-mail: newelski@math.uni.wroc.pl

ABSTRACT:
Assume *M* is a sufficiently saturated and homogeneous model (a
monster model). We define on *M* some canonical equivalence
relations:

*E _{S}* is the intersection of all 0-definalbe equivalence relations on

So *E _{L}* refines

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 *Gal _{L}(M) = Aut(M)/Autf_{L}(M)*, where

There are still some questions on Lascar strong types motivated by the
classification of Borel equivalence relations, since *E _{L}* 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.

E-mail: pong@math.csudh.edu

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.

**Arthur W. Apter**, *Indestructibility and Strong Compactness*

Baruch College of CUNY, New York, USA.

E-mail: awabb@cunyvm.cuny.edu

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.

E-mail: jackson@unt.edu

ABSTRACT: We use the existence of cubical markers for equivalence
relations generated by actions of **Z**^{n}
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.

E-mail: heike@logic.univie.ac.at

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.

E-mail: stanley@math.sjsu.edu

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.

**Klaus Ambos-Spies**, *Generators of the computably enumerable degrees*

University of Heidelberg, Heidelberg, Germany

E-mail: ambos@math.uni-heidelberg.de

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.

E-mail: kud@math.nsc.ru

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 *rank _{tr}(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.*

**References**

[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.

E-mail: cpollett@yahoo.com

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.

E-mail: j.v.tucker@swansea.ac.uk

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].

**References**

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.

**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.

E-mail: palmgren@math.uu.se

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.

E-mail: jeff@maths.man.ac.uk

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 |