Introduction

The Goal of this Course

What is a mathematical proof? Within mathematics, there is no formal definition of what a proof should be. Informally speaking, a proof should be some “convincing argument”, why a particular statement is true or false. Why do we need proofs? Mathematics proceeds by starting from some given concepts (e.g. real numbers), then inventing new concepts based on the given ones (e.g. sequences of real numbers, arithmetical operations on sequences, limits of sequences) and explore the properties of the new concepts (e.g. limit of the sum or the product of two sequences). Intuition (and experience) leeds the mathematician in building up new mathematical areas. Intuition (and experiments) is also helpful in figuring out what facts might be true and which are not. But, due to the complexity of mathematical concepts, intuition is often not enough in order to gain certainty abouth truth or falsity. Moreover, one's own intuition often fails to convince someone else in case this person's intuition differs from one's own.
We will study the language of predicate logic as a language for formulating mathematical statements. Based on this language, we can study rules that tell us how to safely proceed from a known status to some new valid status. A proof of some statement S, in this view, is then just a sequence of statements starting from known facts ending in S, where each transition on the way from the known facts to the final statement S is justified by some rule. The rules used in this process are not arbitrary, in contrast, they should reflect the condensed experience of mankind in what is considered to be true. For instance, if we know that “A is true” and that “B is true whenever A is true”, then “B must necessarily be true”.
Of course, not everything can be proven. The first mathematical laws cannot be proven, because there are no earlier laws, from which to derive them. There must be some starting point, we call those laws axioms. Axioms should describe facts about the objects under consideration that are obviously true. For instance, consider the natural numbers, then the fact that “no natural number has 0 as its successor” is commonly accepted as an axiom for natural numbers. There is no rule how to choose appropriate axioms, rather, there are two extremes to be balanced:

It has been shown that first order predicate logic with set theory has sufficient expressive power to formulate in this theory all of mathematics. In most of this course, we will stay in this setting.

The Use of Theorema in this Course

Theorema contains computer–support for predicate logic, set theory, and tuple theory, i.e. it contains a concrete syntax for these elementary language constructs. We will study the language of predicate logic in its concrete appearance as in the Theorema system. Moreover, Theorema allows to organize mathematical knowledge by giving definitions, stating theorems, and collecting knowledge into structured theories. Theorema would even generate some of the proofs, which we will study in this course, completely automatically! The aim of this course is, however, not to train the students to operate Theorema such that it generates proofs automatically. After having attended this course, students should be capable of recognizing the structure of theorems and the structure of facts in the knowledge base and, by this, have a clear understanding of how to structure a proof. For obtaining this insight into structure, we might occasionally inspect Theorema–generated proofs.

Theorema Demo

Structure of the Course

({{Introduction}, {\(Syntax\ and\ Informal\ Semantics\ of\ Predicate\ Logic\)}, {Proof Rules for Predicate Logic}, {Case Studies}, {Solutions to Exercises}})

Literature

Literature Intimately Related to the Course

Literature on Mathematical Logic