A page with our preliminary programme can be found here.
Speakers and their abstracts
Set Theory: Forcing methods at the successor of a singular cardinal
Topological and Constructive Aspects of Higher-Order Computation
Abstract: Categorical logic studies the interpretation of logical theories in categories and the interplay between formal theories and categories. As such, it is abstract algebraic logic extended to predicate logic and beyond.
Categorical semantics provides a wide variety of models for various formal languages and theories, including for intuitionistic first- and higher-order logic.
Moreover, the categorical framework provides a rich conceptual background for constructions and perspectives that are not (always so easily) obtainable in the more classical model theoretic setting.
This course gives a first introduction to central ideas and concepts in categorical logic. We shall focus primarily on first-order logic, including intuitionistic first-order logic and fragments of first-order logic. Prerequisites will be kept to a minimum, with an initial emphasis on from-the-ground-up explanations of the categorical interpretation of the logical constants, examples of interpretations is various categories, the familiar Tarski and Kripke semantics as special cases, the models-as-functors perspective, and the construction of universal models. On this basis, we will give pointers to and discuss further topics, such as higher-order logic, forcing semantics, duality between syntax and semantics, and type theories (depending on time and interest).
Prerequisites: (Modest) supplementary material will be posted in advance so that it can be assumed that the participants have some familiarity with basic notions of category theory such as category, functor, natural transformation, finite limits and colimits.
Truth & Paradox
Abstract: This is a course on 'surface reasoning' in natural language. The overall goal is to study logical systems which are based on natural language rather than (say) first-order logic. Most of the systems are complete and decidable, the class will see a lot of technical work in this direction. At the same time, the work is elementary. One needs to be comfortable with informal proofs, but only a small logic background is technically needed to follow the course.
Specific topics include: extended syllogistic logics; logics including verbs, relative clauses, and relative size quantifiers; the limits of syllogistic logics, monotonicity calculi; algorithms, complexity, and computer implementations.
The course will have a small amount of daily homework to help people learn. It also may involve some work with running computer programs which carry out proof search and model building in natural logics.
The topic of natural logic lends itself to philosophical reflections on the nature of semantics and is arguably something all formally-minded linguists and linguistically-minded logicians should know about. For people coming with a logic background, the course will offer many completeness theorems (as in modal logic), and connections to topics such as: fragments of first-order logic, some connections to combinatorics, and the typed lambda calculus.
Logic in Computer Science --- Control and Synthesis, from a Distributed Perspective
Abstract: Formal methods in computer science rely on a clear mathematical understanding of programs and their interactions. In synthesis, the goal is to construct a program that complies with some given logical specification. Synthesis of reactive programs addresses this question in the setting where programs interact with their environment. This problem was proposed in the sixties by A. Church as the solvability problem, and it can be also stated in terms of a game between program and environment. An alternative formulation is the theory of supervisory control, that asks to build a controller guaranteeing that a given program satisfies some requirements.
The course will start with an introduction to the areas of logic, automata and game theory that play a prominent role in synthesis. Then we will present some frameworks of distributed synthesis. The goal in distributed synthesis is to construct programs and controllers that consist of local entities that evolve by exchanging information. Distributed synthesis is a truly challenging area, where in some of the frameworks the decidability of the synthesis problem remains open. We will discuss the state-of-the-art and the challenges raised by the distributed setting.
Logic and Rationality
Peter Pagin and Dag Westerståhl
Abstract: The course gives an introduction to the main idea of the principle of semantic compositionality, some of its formal properties, some variants of the idea, and some interesting applications. The applications come from both logic and natural language semantics. The following classes are planned:
1. The general idea of compositionality. Historical background. Formal definitions. Stronger and weaker versions. Some standard arguments for and against compositionality.
2. Compositionality and context dependence. Extensionality and intensionality. Extra-linguistic context dependence. Linguistic context-dependence and general compositionality.
3. Applications 1: (a) Quotation: non-compositional but general compositional. (b) The problem of compositional accounts of the semantics of belief-sentences. (c) Compositionality solves Carnap's problem: Do the laws of classical propositional logic fix the meaning of the usual connectives?
4. Applications 2: Non-compositionality in logic: IF-logic versus Dependence logic.
5. Compositionality and the computational complexity of interpretation: Is compositional interpretation the most efficient kind of interpretation?
Sara L. Uckelman
Abstract: We start with basic material regarding Gentzen's sequent calculus for predicate logic: Cut elimination, Herbrand's theorem, interpolation.
Then we switch to classical results regarding the proof-theoretic analysis of first order Peano aritmetic (PA): provable and unprovable instances of transfinite induction.
In a next step we provide the standard classification of the provably recursive functions of PA.
These results will be put into the phase transition for Gödel incompleteness perspective: Phase transitions for Goodstein sequences and the Paris Harrington theorem.
We will end with a discussion of lower bounds for the lengths of finite proofs in PA of true and purely existential statements.
If time is left over we intend to cover extra material on phase transitions.