Logic in Stockholm 2017

NLS Summer School in Logic 2017

Logic Colloquium 2017

26th EACSL Annual Conference on Computer Science Logic CSL'2017

Preliminary programme

A page with our preliminary programme can be found here.

Speakers and their abstracts

Mirna Dzamonja
Set Theory: Forcing methods at the successor of a singular cardinal

Abstract: Forcing is a method in set theory that changes the properties of the ambient universe, for example the values of the power set function on some set or even a proper class of cardinals. This method is rather well developed when it comes to the successors of regular cardinals, but it is much more challenging to have a method that works at singular cardinals and their successors. In fact, it is known that such a method must necessarily involve the use of large cardinals. In joint work with co-workers James Cummings, Menachem Magidor and Charles Morgan and Saharon Shelah, we have been developing one such method, the details of which will be exposed in the course.

Martín Escardó
Topological and Constructive Aspects of Higher-Order Computation

Abstract: In higher-order computability we study computation with infinite objects, such as streams, real numbers, and higher types. Topology plays the role of mediating between the infinite nature of such objects with the finite nature of computers and algorithms. Of particular importance are the Kleene-Kreisel spaces modeling higher types, where topological notions such as continuity and compactness play a significant role in computability considerations. In these lectures we will introduce these and related concepts, their theory and some applications.

Henrik Forssell
Categorical Logic

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.

Volker Halbach
Truth & Paradox

Abstract: The course provides an introduction to the theory of the truth and the semantic paradoxes. The course does not presuppose any knowledge of logic beyond the basics of first-order predicate logic as it is taught in all introductory logic courses. At the beginning basic techniques such as Gödel's diagonal lemma will be proved in a simple theory of syntax without the detour through arithmetization and fundamental results such as Tarski's theorem on the undefinability of truth will be proved in this setting. Yablo's, Curry's, McGee's, and other paradoxes will be analyzed. It will be argued that many of these paradoxes can be reduced to a single source. To this end possible-worlds semantics for truth and other modal predicates will be employed, which allows to visualize the paradoxes in an informative and illuminating way. The machinery that is developed can also shed some light on the notions of self-reference and circularity that are not only central in the theory of paradoxes, but also in the analysis of Gödel's incompleteness theorems and related phenomena. Some popular axiomatic theories of truth will be presented and their main advantages and disadvantages will be discussed. Finally, if time permits, some applications of the theory of truth and the paradoxes, for instance, to the theory of logical consequence will be outlined.

Larry Moss
Natural Logic

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.

Anca Muscholl
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.

Eric Pacuit
Logic and Rationality

Abstract: to appear.

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
Medieval Logic

Abstract: to appear.

Andreas Weiermann
Proof Theory

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.