The *learning objectives* specify the knowledge and skills
you should acquire in order to pass the course. In the official course description you can find a concise
description of the learning objectives for this course; below we
present a more detailed and informative version.

After successfully completing the course, the student:

- can formalise first-order properties with formulas of predicate logic;
- can list the axioms and rules of an equational formal system for reasoning about the equivalence of abstract propositions and first-order predicates;
- can list the axioms and rules of a natural deduction style formal system for reasoning about the equivalence of abstract propositions and first-order predicates;
- can prove first-order properties in a fixed formal system (calculational style, natural deduction style);
- can use the calculational style of reasoning (replacing equals by equals, strengthening/weaking) to prove that two formulas are equivalent and to prove that a formula is a tautology;
- can prove that a first-order formula of predicate logic is a tautology using a natural-deduction style formal system;
- can reproduce the formal definitions of predicates and operations on sets (set comprehension, subset, intersection, union, complement, set difference, empty set, power set, Cartesian product);
- can reproduce the formal definitions pertaining to relations (equivalence relation, equivalence class, composition of relations);
- can reproduce the formal definitions pertaining to mappings (image and source, injection, surjection, bijection, inverse mapping, composition of mappings);
- can prove simple first-order properties about sets, relations and functions using calculational style reasoning, or natural deduction style reasoning, or a combination thereof;
- can refute the validity of a first-order property about sets, relations and functions with a counterexample;
- can reproduce the formal definitions pertaining to partial orderings (linear partial ordering, minimal and maximal elements, minimum and maximum, least upper bound, greatest lower bound).
- can recognize the logical reasoning steps in a mathematical proof in natural language;
- can synthesize simple mathematical proofs in natural language;
- has a systematic approach (in particular, can systematically draw conclusions according to a predefined collection of axioms and inference rules);
- can prove properties with induction.