Logic II for Mathematicians and Computer Scientists

RISC-Linz logo

Date and Time

Tuesday, 10:15 - 11:45, in room 416 of the TNF tower.

The lecture will start on 11.3.2002.

Important: If you want to participate in this course, please send an e-mail to the lecturer!

About the Lecture

Lecture notes are available in dvi format and postscript format.

Since communication skills become more and more important for mathematicians and computer scientists, it is a dedicated goal of the lecture to learn and practice oral presentations of difficult proofs in logic. Therefore, it is planned that a large portion of the material is presented by participants. Current Schedule.

Slides/papers prepared by other participants:

The objects studied in logics are formal theories. Meta-theory investigates such formal calculi from a combinatorial point of view. In model theory, the relation between the formal theory and its semantic is investigated. In this lecture, we discuss selected topics from these two main branches of logics.

Equational theories
We discuss unification, term rewriting rules and some useful theorems related to the Church-Rosser property.
Predicate calculus
(also called first order logic). We give proofs for Church's result of undecidability of predicate calculus, Gödel's completeness theorem and applications.
Formal number theory
Two famous negative results - Gödel's incompleteness theorem and the unsolvability of Hilbert's 10th problem - are obtained as immediate consequences of two positive results (which are closely related): any recursively enumerable set is arithmetic (Gödel) and any recursively enumerable set is diophantine (Matijasevic).
Lambda-Calculus
We discuss lambda calculus with respect to two main applications: as a foundation for functional programming, and as a language for higher order logic.
Constructive Logic
We give Goedels's negative translation of intuitionistic logics into classical logics.

Maintained by: Josef Schicho
Last Modification: June 20, 2003

[Up] [RISC-Linz] [University] [Search]