The course treats derivations and proofs as mathematical objects, and study these from a formal, syntactic point of view, unlike model theory that can be said to be the semantic theory of the corresponding phenomena. Among the many proof formalisms that have been constructed, studied, and implemented we focus on two central classes of systems: natural deduction and sequent calculus. The most fundamental theorems, whose proofs are implemented in detail are cut elimination and normalisation for propositional logic and predicate logic, but also for stronger systems, such as formalised arithmetic. Philosophical and linguistic aspects of proof theory, as its connection with semantics and anti-realism, will also be addressed.
Det är institutionen för filosofi, lingvistik och vetenskapsteori som ger kursen. Länk till institutionens sidor.