Introduction to Logic and Model Theory

Organizers: Dr. Radu Mardare and Prof. Kim G. Larsen
Type - PhD course
Scheduled for - 2011: 24 Nov, 28 Nov, 1 Dec, 8 Dec, 9 Dec, 12 Dec - from 9:00 AM to 12:00 each day
Language: English
ECTS: 2

Participants:
Aalborg, Denmark - Department of Computer Science, Department of Mathematics, Aalborg University.
Copenhagen, Denmark (video-conference) - Technical University of Denmark, IT University of Copenhagen, Aalborg University-Copenhagen.
Aarhus, Denmark (video-conference) - Aarhus University.
Beijing, China (video conference) - The State Key Laboratory, Beijing, China.
Shanghai, China (video conference) - East China Normal University, Shanghai, China.

Course materials:
Overview and Bibliography
Lecture 0
Lecture 1
Lecture 2
Lecture 3
Lecture 4
Lecture 5
Lecture 6
Exercises-Exam

Motivation: In the past decades significant research in Computer Science and Applied Mathematics adopted logical methods and techniques, such as model checking, satisfiability checking, theorem proving and various logical specifications and analysis methods. These opened new perspectives in science while solving challenging problems in emergent fields like dynamic and hybrid systems, engeneering, economics, systems biology, ecology, etc. These logical methods and tools rely on the revolutionary results of the last century in the field of Foundations of Mathematics and Computation, Mathematical Logic and Model Theory due to scientists such as Georg Cantor, Gottlob Frege, Bertrand Russell, Kurt Gödel, Alan Turing, Alonzo Church to name but a few. These results have impacted first of all the way we think of Mathematics and mathematical structures in general by emphasizing the limits of mathematical reasoning and made possible Computer Science as a science.

Description: This course is mainly addressed to postgraduate students in Computer Science and Mathematics with the aim of introducing the basic concepts, results and tools from Mathematical Logic and Model Theory. The course will approach most of the hot problems in these fields, from the paradoxes of Set Theory to Gödel's theorems, while the main focus will be on Classical First and Second Order Logics and on Modal Logics. We will formally define various metamathematical concepts such as syntax, semantics, truth, provability, completeness and complete axiomatizations, compactness, decidability, quantification etc. With some of these concepts the students are already familiar from more specific courses. The role of this course is to present these concepts in a general framework and to clarify the spectrum of their use and applicability.

Formally, the course will cover the following topics:

I. An introduction to Classical Logic and Model Theory
I.1. Formal Theories
I.2. Propositional Logic (PL)
I.2.1 Syntax and Semantics, truth tables
I.2.2 Conjunctive and disjunctive normal forms
I.2.3 Proof theories for PL
I.2.4. Completeness and compactness
I.3. First Order Logic (FOL)
I.3.1. Syntax and Semantics
I.3.2. Axiomatization
I.3.3. Completeness and Compactness
I.3.4. Lowenheim-Skolem Theorems
I.3.5. Henkin’s constants and the relation to PL
I.4. Monadic Second Order Logic and finite state machines

II. Modal Logic and its Model Theory
II.1. Kripke structures and transition systems
II.2. Bisimulations and zig-zag morphisms
II.3. The standard translation into FOL and SOL
II.4. Model constructions
II.5. Bisimulation and invariance
II.6. Classical truth-preserving constructions
II.7. Axiomatizations and Weak Completeness
II.7.1. Axiomatic systems
II.7.2. Finite model property
II.7.3. Canonical models
II.7.4. The filtration method

III. Multimodal Logics for Transition Systems
III.1. Hennessy-Milner Logic
III.2. Dynamic Logic
III.3. Epistemic Logics
III.4. Probabilistic and Markovian Logics
III.5. Temporal and probabilistic/stochastic temporal logics

 

Prerequisites: Not strictly necessary but useful is the familiarity with the basic concepts of Set Theory and Algebra.