Erfüllbarkeitsreduktion

Einfache Sprache

Def. Erfüllbarkeitsreduktion

Seien $\mathcal S, \mathcal S'$ Signaturen so, dass $\mathcal S\subseteq \mathcal S'$. Eine $\mathcal S$-Formel $\varphi$ ist erfüllbarkeitsreduzierbar zu einer $\mathcal S'$-Formel $\varphi'$, geschrieben $\varphi\leq_\mathcal S \varphi'$, wenn folgendes gilt:

1. Für alle $\mathcal S$-Strukturen $\mathcal A$ existiert eine $\mathcal S'$-Erweiterung $\mathcal A'$ von $\mathcal A$ so, dass für jede A-Belegung $\beta$ gilt $$\mathcal A,\beta\models \varphi\implies\mathcal A',\beta\models\varphi'\;.$$
2. Für alle $\mathcal S'$-Strukturen $\mathcal A'$ und $A'$-Belegungen $\beta$ gilt, dass für die $\mathcal S$-Erfüllbarkeitsreduktion $\mathcal A$ auf $\mathcal A'$ $$\mathcal A',\beta\models \varphi'\implies\mathcal A,\beta\models\varphi\;.$$