In order to give some illustrative examples of the many techniques and problems involved in working in these subsystems, we will sketch some results related to Lebesgue spaces (every open covering has a Lebesgue number) and Atsuji spaces (every continuous function defined on them is uniformly continuous) within subsystems of second order arithmetic. The most interesting result is ``every Atsuji space is Lebesgue''. It is known that it is provable in ACA₀, however we do not know yet if it is equivalent to ACA₀. As improvement of such known result, we prove that the known proof needs ACA₀, and we conjecture that the statement is actually equivalent to ACA₀.

Another example is from Combinatorics: it is related to the Free Set Theorem and Ramsey's Theorem and uses techniques from computability theory. This example shows how some theorems of ordinary mathematics may not fit in one of the subsystems mentioned above.

We will also comment on a couple of interesting results: the first one is related to Set Theory. While Cantor's proof that every countable closed set is a set of uniqueness makes essential use of ATR₀, the result itself can be proved in ACA by different means (result due to J. Humphreys).

Leon Horsten

We consider a language containing partial predicates for subjective knowability and truth. For this language, inductive hierarchy rules are proposed which build up the extension and anti-extension of these partial predicates in stages. The logical interaction between the extension of the truth predicate and the anti-extension of the knowability predicate is investigated.

Marcus Kracht

The emergence of attribute value formalisms in linguistic theory has provoked a debate about the nature of representations. The painfully explicit notation of GPSG and HPSG, for example, was criticized by transformationalists as not psychologically adequate. In their view, these notations conflate inherently descriptive with computational content. However, it is not clear at the outset where to draw the boundary between these two notions. In order to decide this issue, one needs a neutral platform where these two positions can be nego- tiated. We shall argue that logic and model theory is such a plat- form. This talk will present a tour d'horizon of the logical theory of syntactic (and phonological) structures. In particular, we shall present a definition of naturalness for features that will allow us to distinguish between features which are in some sense essential and those which are only virtual ("ghost features") and which seem to be proxy for something else that is not yet understood. Using this dichotomy, the nature of certain representations can actually be better motivated.

Kai-Uwe Kühnberger

Theories of truth are a highly discussed topic in philosophy. In the last twenty-five years several different frameworks were developed in order to provide a modeling of classical paradoxes in natural language. In a wider context these frameworks can be used to model circular phenomena in general. Whereas, most of these frameworks are well-examined concerning their empirical properties (for example concerning their properties of modeling Liar-like sentences) less attention was paid to questions concerning complexity issues of these frameworks.

In this talk we will examine aspects of the latter issue. First, we will consider results of generalized fixed point accounts that originated from the classical work of Saul Kripke. We will see that in such theories truth predicates are essentially inductively defined. Second, we will consider Gupta-Belnap's revision theory of truth. According to a result of Antonelli and Kremer it can be shown that the complexity of validity of the semantical systems S^* and S^# is Pi¹₂. Third, we shall examine the modeling of truth in a situation theoretic account, using Peter Aczel's theory of non-well-founded sets. Using the theory of hypersets instead of classical ZFC enables us to model circular propositions in a situation theoretic framework. In particular the coalgebraic features of this representation is of special interest in this context.

All these frameworks will be informally discussed with a stress of the mathematical techniques used in such theories. Furthermore, we will mention a number of open problems. Examples are the following ones.

What are necessary and sufficient conditions for the existence of fixed points in generalized versions of Kripke's framework? Is there a coalgebraic representation of revision theories? What are the properties of a second-order version of revision theories? What can be said about the complexity of coalgebraic theories?

Mario Piazza

In this talk, we tackle the philosophical problem of the applicability of mathematics, also known as the problem of "the unreasonable effectiveness of mathematics": how can facts about mathematical structures be relevant to the empirical world? For instance, how do topological concepts such as that of boundary apply to the ordinary world around us? Why, generally speaking, observations of the natural world seem to fit so well into logical structures? (Are logical entities the sine qua non of mental activity?) It may be argued that mathematics is essential to physics, i.e. it has a causal counterpart, because we select for study only those features of the natural world that can be framed into mathematical form. Mathematics is effective since it is generative. Several examples are provided in order to explain this phenomenon.

At a first stage it will be explained what are the main metatheoretical aspects of Structuralist Theory of Science. It will be illustrated which technical tools within the Structuralists' program are developed which make possible a lot of applications to empirical sciences. One of the main applications are reconstructions of empirical theories within a semantic approach founded on informal set theory. These techniques will be illustrated with Quantum Theories which deliver a couple of examples.

Finally it should be discussed how some well-known methods of empirical science can be explicated within structuralism. In the centre of these considerations are methods which describe some changing of theories. Special types of changing can be represented as intertheoretical relations. In this metatheoretical frame it will be argued that "Analogy" could be comprehended as such an intertheoretical relation.

Hans-Jörg Tiede

In a series of articles, Lambek laid out a program advocating a proof theoretical approach to grammar. Current interest in proof theoretical grammars stems from their applicability to natural language syntax and semantics, their relation to linear logic, and studies of their formal properties - which often combine proof theoretic and recursion theoretic arguments. This talk will focus on formal properties of proof theoretical grammars - in particular formal language theoretic and complexity theoretic aspects. Recent work on the formal properties of grammar formalisms has paid considerable attention to the "strong generative capacity," i.e. the structures or derivation trees assigned to the generated strings. We will discuss what could take the role of structures or derivation trees in the proof theoretical framework and the relationship of these structures to the derivation trees of context-free grammars.

In a range of contexts, one comes across processes resembling inference, but where input propositions are not in general included among outputs, and the operation is not in any way reversible. Examples arise in contexts of conditional obligations, goals, ideals, preferences, actions, and beliefs. Our purpose is to develop a theory of such input/output operations. Four are singled out: simple-minded, basic (making intelligent use of disjunctive inputs), simple-minded reusable (in which outputs may be recycled as inputs), and basic reusable. They are defined semantically and characterised by derivation rules, as well as in terms of relabeling procedures and modal operators. Their behaviour is studied on both semantic and syntactic levels.

In this talk we discuss:

• the four basic input-output relations we have singled out;
• two consistency constraints which can be imposed on the input-output relations;
• the application of input-output logic with constraints to normative reasoning (including a comparison with modal deontic logic with its contrary-to-duty paradoxes);
• the application of input-output logic to beliefs-obligations-intention-desires (boid) agents to analyse the interaction between agents' components.

NOTE: This presentation reports on joint work with David Makinson, Unesco, Paris