1st Semester 2021/22: What makes logics (un)decidable?

Instructors

Balder ten Cate

ECTS

6

Description

What makes first-order logic undecidable and what makes modal logic decidable? This question can of course be answered in different ways. In this course, we explore one line of research that aims to answer this (and that has also provided a basis for many effective algorithms for reasoning problems in different areas of computer science), namely the study of guarded fragments of first-order logic (and of second-order logic). The guarded fragment of first-order logic was first introduced 25 years ago by Andreka, van Benthem and Nemeti, and is still very much alive today: the study of various aspects of (extensions of) the guarded fragment is still an active area of research up to this day.

 

week 1: 

• we discuss some of the fundamental undecidable problems, including the primordial one, the halting problem, as well as infinite tiling problems. We prove the undecidability of first order logic by a reduction from such an undecidable tiling problem.

• we prove the decidability of modal logic, on the basis of its bisimulation invariance and the tree model property. We also review a powerful classic result by Rabin, according to which the monadic second order theory of infinite trees is decidable.

• We have a first look at the guarded fragment of first-order logic (GF), a large decidable fragment of first order logic that includes (the standard translation of) modal logic and that aims to provide an explanation of what it is about the syntax of modal formulas that is responsible for the decidability of modal logic.

 

Week 2:

• we prove the decidability of GF by showing that it has an analogue of the tree model property: every satisfiable guarded formula has a model of small treewidth. 

• We also explore one more recent extension of the GF called the guarded-negation fragment, which can be viewed as a common generalization of two important decidable fragments, namely GF and unions of conjunctive queries (UCQ), and which provides yet another take on what makes modal logic decidable.

 

Week 3:

• So far, we have only been concerned with fragments of first-order logic. In week 3 we consider guarded (as well as guarded-negation) fixed point logic. 

 

Week 4:

• Student presentations (literature review) on related and/or advanced topics. A list of suggestions will be provided. It will include: finite model theory of guarded logics; Craig interpolation; the connection between logics of trees and finite automata (which, most likely, we won’t have time to cover in depth in the lectures, but underlies many core results in the area); fixed point boundedness and the problem of deciding first-order definability of fixed point formulas; open world query answering in the presence of a backgrounds theory (aka ontology-mediated query answering); proof theory for guarded fragments.

 

Students are expected to pick a topic for their presentation at the end of the second week. Suggested reading will be provided by the teacher, and the teacher is available for office hours during the 2nd and 3rd week as the students prepare for their presentation.

Organisation

Tentative schedule:

- 6 lectures of 90min (3 in the first week; 2 in the second week, 1 in the 3rd week)

- plus student presentations (4th week -- topics decided in the beginning of the 2nd week)

 

Prerequisites

Familiarity with first-order logic, modal logic, standard translation, and bisimulations.

Assessment

Fail/pass based on class participation, homework exercises and presentations