With these prerequisites, we can introduce the concepts of a formal proof and of a theorem in a logical calculus.

# Definition: Proofs and Theorems in a Logical Calculus

Let $(L,\mathcal A,\mathcal R)$ be logical calculus with $n$ axioms $\mathcal A:=\{a_1,\ldots, a_n\}$ and $r$ rules of inference $$\mathcal R:=\cases{f^{(1)}_1,\ldots,f^{(1)}_{m_{(1)}},\vdash f_1,\\ \vdots\\ f^{(r)}_1,\ldots,f^{(r)}_{m_{(r)}},\vdash f_r.}$$ A formal proof is a chain of strings $\phi_1, \phi_2,\ldots \phi_n\in L$ satisfying the following construction rules:

• $\phi_i$ is an axiom for some $i\in\{1,\ldots,n\}$, or
• there is a rule of inference such that $f^{(j)}_1,\ldots,f^{(j)}_{m_{(j)}},\vdash \phi_j$ for some $j\in\{1,\ldots,r\}.$

The last string $\phi_n$ is called a theorem.

Chapters: 1
Definitions: 2

Thank you to the contributors under CC BY-SA 4.0!

Github:

### References

#### Bibliography

1. Hoffmann, Dirk W.: "Grenzen der Mathematik - Eine Reise durch die Kerngebiete der mathematischen Logik", Spektrum Akademischer Verlag, 2011
2. Beierle, C.; Kern-Isberner, G.: "Methoden wissensbasierter Systeme", Vieweg, 2000