Logische Theorien
Wir definieren zunächst, was eine Theorie ist. Gegeben sind zunächst die logischen Zeichen $\wedge$, welches für das logische "und" steht, $\vee$, welches für das logische "oder" steht, $\rightarrow$, welches für logische Implikation steht, $\bot$, welches für die immer falsche Aussage, das Falsum, steht, $\forall$, der Allquantor, $\exists$, der Existenzquantor.
Außerdem gegeben seien unendlich viele $n$-stellige Relationssymbole $R_0^n, R_1^n, R_2^n, \ldots$, wobei $n\in\mathbb{N}_1$; unendlich viele $n$-stellige Funktionssymbole $f_0^n, f_1^n, f_2^n, \ldots$, wobei $n\in\mathbb{N}_0$; und unendlich viele Variablensymbole $x_0, x_1, x_2, \ldots$.
Wir arbeiten nun mit dem Alphabet das all diese Symbole enthält, also einem unendlichen Alphabet, in diesem Fall. Nun wollen wir die Sprache der korrekt geformten Aussagen der Logik 1. Stufe definieren. Zunächst definieren wir die Sprache $\operatorname{Ter}$ der Terme:
- Alle Variablensymbole sind Terme: für alle $i$ ist $x_i \in \operatorname{Ter}$.
- Sind $t_1, \ldots, t_k\in\operatorname{Ter}$, so ist für alle $i$ auch $f_i^k(t_1,\ldots,t_k)\in\operatorname{Ter}$, das heißt, man darf einem Funktionssymbol so viele Terme übergeben, wie es Stellen hat.
Nun können wir die Sprache $\operatorname{For}$ der Formeln definieren:
- Es ist $\bot\in\operatorname{For}$: Die immer-falsche Aussage ist eine Formel.
- Sind $t_1,\ldots,t_k\in\operatorname{Ter}$, so ist für alle $i$ auch $R_i^k(t_1,\ldots,t_k)\in\operatorname{For}$, das heißt, man darf einem Relationssymbol so viele Terme übergeben, wie es Stellen hat.
- Sind $A, B\in\operatorname{For}$, so sind auch $A\wedge B, A\vee B, A\rightarrow B\in\operatorname{For}$.
- Ist $A\in\operatorname{For}$, so sind für alle $i$ auch $\forall_{x_i} A, \exists_{x_i} A\in\operatorname{For}$.
Dies war eine sehr technische Definition, die zwar immer funktioniert, aber nicht sehr praktisch zu benutzen ist. In den meisten Fällen schreiben wir nicht $f_i^n$ und $R_i^n$, sondern haben andere, konkretere Funktions- und Relationssymbole. Beispielsweise ist $+$ ein zweistelliges Funktionssymbol, das man zusätzlich üblicherweise als Infix notiert, und $\le$ ist ein zweistelliges Relationssymbol, das man ebenfalls als Infix notiert. Solange klar ist, wie man alles in die formale Schreibweise überführt, sind solche Kurzschreibweisen aber kein Problem, und werden in der Regel ohne größeren Kommentar übernommen.
Ein Spezialfall sind nullstellige Funktionssymbole, die wir ja definiert haben. Diese bezeichnet man auch als Konstanten. Beispielsweise ist die $0$ in vielen Theorien eine solche Konstante.
Freie Variablen und geschlossene Aussagen
Wir sagen, dass Quantoren deren Variablen "binden". Eine Variable heißt "frei", solange sie nicht gebunden wird. Man kann dies rekursiv definieren durch die Funktion $\operatorname{FV} : (\operatorname{Ter}\cup\operatorname{For})\rightarrow \{x_0,\ldots\}$
- $\operatorname{FV}(x_i) := \{x_i\}$
- $\operatorname{FV}(f_i^k(t_1,\ldots,t_k)) := \bigcup\limits_j=1^k\operatorname{FV}(t_j) = \operatorname{FV}(t_1) \cup \ldots \cup \operatorname{FV}(t_k)$.
