Understanding and finding proofs is a central part of mathematics. But what is a proof, actually? Can the concept of a proof be formalised? Can we program a computer so that the computer can verify proofs and even search for proofs? What are the usual axioms of mathematics that we are allowed to use in proofs?
To formalise the notion of a proof we need logic; more specifically, we will work with so-called first-order logic. Logic is in many respects the most important logic, both in mathematics and in computer science. It strikes a good balance between expressiveness on the one hand and good mathematical properties on the other hand. For example, first-order logic is expressive enough to formulate the axioms of axiomatic set theory, e.g., Zermelo–Fraenkel set theory (ZFC; Chapter 4) or Bernays-Gödel set theory. Practically all of mathematics can be formalised in this way. What is even more important is that first-order logic has a very rich model theory; here we have to refer to model theory courses. In computer science, firstorder logic may be viewed as the most important database query language. Various restrictions and extensions of first-order logic might be relevant in applications, but
logic remains the central point of departure.
- Teacher: Chafiâa Ayhar