Beispiel für Spezifikation

Signatur:

• Sorten: P, G
• Funktion: boolean I(P, G)

Axiome:

• ∀x∈P : ∃_≥2y∈G : I(x, y)
• ∀y∈G : ∃_≥2x∈P : I(x, y)
• ∀x, y∈P : x≠y⇒∃₌₁z∈G : I(x, z)∧I(y, z)
• ∀y, z∈G : y≠z⇒∃₌₁x∈P : I(x, y)∧I(x, z)

Ü: gibt es Modelle mit | P| = 2, 3, 4,… ?

Ü: sind die Axiome unabhängig?

Ü: übersetze ∃_≥2,∃₌₁ in ∃(= ∃_≥1)