Prädikatenlogische Formel

Einfache Sprache

$\mathcal S$-Formel liefern bei Auswertung einen Booleschen Wert, im Gegensatz zu $\mathcal S$-Termen, die einen Wert des Universums liefern.

Def. Prädikatenlogischen Formel

Sei $\mathcal S$ eine Signatur. Die Menge der $\mathcal S$-Formeln bzw. Formeln der Logik erster Stufe $\mathbf F_\textrm{PL}$ ist induktiv definiert.

Basiselemente: Teil von $\mathbf F_\mathrm{PL}$ sind

• die einknotigen Bäume beschriftet mit den Booleschen Werte $\top$ und $\bot$,
• für zwei $\mathcal S$-Terme $t_0$ und $t_1$ der Baum mit der Wurzel $\doteq$ und den Teilbäumen $t_0$ und $t_1$ (geschrieben $t_0\doteq t_1$) und
• für jedes Relationssymbol $R\in\mathcal R$ mit der Stelligkeit $n = \Sigma(R)$ und $\mathcal S$-Terme $t_0,\ldots,t_{n-1}$, ist auch der Baum mit der Wurzel $R$ und $n$ Teilbäumen $t_0,\ldots,t_{n-1}$ (geschrieben $R(t_0,\ldots,t_{n-1}$).

Induktive Regel: Teil von $\mathbf F_\mathrm{PL}$ sind

• für einen $n$-stelligen Junktor $C$ und $\mathcal S$-Formeln $\varphi_0,\ldots,\varphi_{n-1}$ der Baum mit der Wurzel $C$ und Teilbäumen $\varphi_0,\ldots,\varphi_{n-1}$ (geschrieben $C(\varphi_0,\ldots,\varphi_{n-1})$) und
• für einen Variable (Elementvariable) $x_i\in\mathbf V_\mathrm{PL}$, eine $\mathcal S$-Formel $\varphi$ und einen Quantor $Q\in\{\forall,\exists\}$ der Baum mit der Wurzel $Qx_i$ und dem Teilbaum $\varphi$ (geschrieben $Qx_i\varphi$).