Further reading in Applied Logic DV1

Lecture

1. Esterel and Synchronous Reactive Programming
2. Definability, decidability and undecidability. Undecidability proofs of the structure (N;+,.,0,1) can be found in section X.6 of found in
   • H.-D. Ebbinghaus, J. Flum, W. Thomas: Mathematical logic (Springer).
   An introductory book in Swedish which includes lambda-calculus as well:
   • Kent Petersson: Beräkningsbarhet för dataloger. Från lambda till P, Bokförlaget Aquila, 1988.

   For more advanced topics: C. Smorynski, Logical number theory (Springer) contains a proof of Julia Robinson theorem on the undecidability of (Q;+,.,0,1). Undecidable questions about expressions involving transcendental functions.

   Erwin Engeler Foundations of Mathematics Springer 1992 discusses various axiomatisations of number systems and geometry. Tarski's theorem is in section I.2 and example of a non-trivial geometry problem (an Euler problem) that can in principle be solved by a computer is in section I.3. Mathematica 4.0 contains an improvement of Tarski's decision method. For a good introduction see, Strzebonski, A. "Solving Algebraic Inequalities." Mathematica Journal 7, 525-541, 2000.

   The biographical memoir of Julia Robinson contains many mathematical details.

3. (Non-)constructive proof, typed lambda-calculus, The Curry-Howard isomorphism. Chapters 1 and 2 of the (free) book Programming in Martin-Löf's type theory contains much of the introductory material in chapter 1-4 of "Konstruktiv logik". See also the first two chapters of Constructive Mathematics
4. Exercise class.
5. Intuitionistic logic and its algorithmic interpretation.
13. An alternative proof of the completeness theorem is in van Dalen (1997), the so-called Henkin-proof, which has less constructive content.
14. Term rewriting: A course by Willem Klop can be found here. In chapter 1, it shown that braids can be regarded as confluent reduction systems.