After successful completion of the course, students are able to distinguish and to apply important concepts, techniques, and results of formal logic and computability theory. Moreover, students who pass the fianl exams should be able to understand and to explain connections between topics like incompleteness of arithmetical calculi, undecidabiltiy, formal provability and expressibility.

• advanced aspects of classical first order logic as specification tool
• proof systems for classical first order logic, including  soundness and completeness proofs 
• elements of model theory (Löwenheim-Skolem, compactness, expressibility)
• principles of automated theorem proving
• methods for handling identity  
• comparison of types of inference systems 
• elements of modal logic: Kripke semantics, temporal logics 
• elements of intuitionistic logic and constructive proofs
•  computational aspects of logic
• undecidabilty of first order logic and its consequences
• models of computation (Turing machines, lambda calculus)
• elementary recursion theory
• Church-Turing thesis
• incompleteness of arithmetic and its consequences 

• derivations in various different logical calculi
• applying formal concepts to standard problem sets
• mastering formal (mathematical) definitions
• analysis of proofs of central results
• mandatory exercises

ETCS Breakdown:

6 ETCS = 150 hours

• 38 hours:  lecture time (+ 6-8 hours repetitorium for students not having a firm previous knowledge in logic)
• 10 hours: exercise sessions (MANDATORY)
• 42 hours: 6  blocks of problems/exercises 
• 60 hours: examination (preparation time)

The course will start Wednesday,  October 2nd 2024, 11:00 (s.t.).

• solutions to 6 blocks of exercises - independent solutions expected
• mandatory attendance in 6 exercise classes
• written exam
• oral exam

NOTE: The participants are required to do 6 blocks of exercises. The solutions are to be uploaded in TUWEL and might have to be presented on the blackboard.

Mandatory exercise sessions:  11th October, 25th October, 8th November, 22 November, 6th December, 19th December 2024

The exercise part has to completed postively in order to be admitted for the exam.

(see lecture slides for additional literature)

Knowledge of classical propositional logic and of basic concepts of classical first order logic (logical consequence, interpretations and model structures, satisfiability versus validity), a firm understanding of the syntax/semantic distinction, some experience with formal specification, acquaintance with a range of different programming paradigms (imperative, functional, logical),  and automata theory (finite automata, pushdown automata, Turing machines)

NB: If you don't have a firm background in logic yet, you are asked to join special repetitorium classes, which are open to all participants.