Math 681 — Spring 2001 Logic


Instructor: Sergei Artemov
Time: TR 11:40–12:55
Room: MT 205

Propositional language, boolean semantics. Proof systems for propositional logic, completeness.

First order proof systems, soundness and consistency. Completeness theorem for first order proof systems. Compactness in logic and mathematics. Nonstandard models of arithmetic.

Computable functions, decidability and enumerability. Representing computable functions in first order arithmetic.

Goedel's first incompleteness theorem. Provability operator, consistency formula. Unprovability of consistency. Reflection principles, formal verification.

Axiomatic set theory as basis for mathematics. Second order logic and its incompleteness.

Constructive reasoning and intuitionistic logic. Possible worlds semantics, completeness. Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic. Operations on proofs, intuitionistic logic as logic of proofs. Explicit reflection and verification.