Syntaktische u. semantische Äq. von Termen

• für Gleichungssystem E über Σ

  Bsp. E = {P(Z, y) $\approx$ y, P(S(x), y) $\approx$ S(P(x, y))}.

• bereits definiert: syntaktische Äquivalenz: $\approx_{E}^{}$

  (←_E∪→_E)^*, alternative Schreibweise: E $\vdash$ s $\approx$ t

• Def. E $\models$ s $\approx$ t: für jedes Modell A von E gilt A $\models$ s $\approx$ t.

  Bsp: E $\models$ P(S(S(Z)), y) $\approx$ S(S(y)).

  Vorsicht: E $\not\models$P(x, y) $\approx$ P(y, x), dazu später mehr

• Def: semantische Äquivalenz: E $\models$ s $\approx$ t

• Satz (Birkhoff): E $\vdash$ s $\approx$ t$\iff$E $\models$ s $\approx$ t.      Anwend.:

  • syntaktische Beweise für Aussagen in (allen) Modellen
  • semantische Widerlegung von s↔_E^*t (ein Nicht-Mod.)