The ultimate goal of the formal concepts we have introduced so far is to develop a formal system, in which it is possible to draw logical conclusions from assumptions. Humans can do so but our logical system should be capable to derive logical arguments more or less automatically, e.g. by an imaginary computer, which we will call in this section the **Proving Machine** (**PM**). We will summarize all concepts introduced so far and check, whether we have all components necessary to get our **PM** working.

- First of all, our
**PM**is given an alphabet of finitely many letters $\Sigma.$ We assume that it cconcatenate the letters to strings $s$. In principle, the**PM**can create infinitely many different strings $s$ out of the alphabet $\Sigma.$ We denote this infinite set $\Sigma^*.$ - Next, from all the infinitely many strings $s\in\Sigma^*,$ we choose only some strings and call this subset $L\subset \Sigma^*$ a language. You can think of $L$ as the set of all (finitely or infinitely many) words, which the
**PM**should ever be able to use. - To enable our
**PM**to decide, whether a given string $s \in\Sigma^*$ belongs to a language $L$, we have to restrict the language to some grammar. In other words, we restrict the language $L$ to be a formal language. The syntax can be compared to a computer program that enables the**PM**to accept only strings $s$ belonging to the language $L$ as its input. It should reject any other input. - Besides, we want the
**PM**to give us answers about a set $U$ of mathematical objects we want to study. We call $U$ the domain of discourse $U$ is completely independent of the language $L.$ However, we have chosen the alphabet $\Sigma$ and the syntax in a way that the resulting language $L$ is powerful enough to let the**PM**give us answers about $U.$ *"Giving us answers about $U$ in a formal language $L$"*means in fact that the**PM**should be able to prove statements formulated in $L$ about $U$. Ideally, given a statement $s\in L$ as input, the**PM**should return us "true", if the statement is true or "false" if the statement is false. Also, if the**PM**is not able to decide if a statement is true or false, it should return us "undefined". For this purpose, we have provided the**PM**with two other computer programs, one we denote by $I$ which interprets a given string $s$. Once $s$ is interpreted, the second program $[[]]_I$, called the "truth function" of interpretation gives us the answer, whether the interpreted string is true or false.

Are we done? You might say, in principle, yes, we are. We have constructed a **PM**, which can interpret any syntactically correct string $s\in L,$ which we might feed it with. We might even feed it with strings representing statements about all yet unproven conjectures stated about mathematical objects in the domain of our discourse $U$, and the **PM** will give us the awaited answers "true", "false" or "undefined". So are we are done with building our **PM**? Not quite.

Note that the interpretation $I$ and its truth function $[[]]_I$ must be very complex computer programs that somehow tell the **PM** how to "think logically." Thus, we only have shifted the problem to another level, creating black boxes - the functions $I$ and $[[]]_I$. Enabling the **PM** to give us all the awaited answers about $U$ means that we have to tell it **a priori** which answers are correct and which not.

Therefore, we will still need some tuning of the **PM** to get it working. Maybe we need even more components? These components are axioms, rules of inference, and the derivability property.

- Definition: Axioms
- Definition: Rules of Inference
- Definition: Logical Calculus
- Definition: Proofs and Theorems in a Logical Calculus

Chapters: 1