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:

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

Chapters: 1
Definitions: 2

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




  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