◀ ▲ ▶Branches / Logic / Definition: Proofs and Theorems in a Logical Calculus
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.
Mentioned in:
Chapters: 1
Definitions: 2
Thank you to the contributors under CC BY-SA 4.0! 
- Github:
-
References
Bibliography
- Hoffmann, Dirk W.: "Grenzen der Mathematik - Eine Reise durch die Kerngebiete der mathematischen Logik", Spektrum Akademischer Verlag, 2011
- Beierle, C.; Kern-Isberner, G.: "Methoden wissensbasierter Systeme", Vieweg, 2000
