Sémantická definice definitních formulí

• Postačující podmínky pro definitní formule A:

  • 1. komponenty TRUE-ohodnocení A jsou z adom(A).
  • 2. je-li A´ y (y), pak je-li pro nějaké y

• (y0) TRUE, pak yadom().

  • 3. je-li A´ y (y), pak je-li pro nějaké y0

• (y0)  FALSE, pak y0 adom().

• Pz.: 2. a 3. platí pro jakékoli přípustné hodnoty volných proměnných v (mimo y).

• Pz.: vysvětlení podmínky 3.

• y (y)  y (y)

•  je-li pro nějaké y0 (y0)  TRUE, pak podle 2. platí y0  adom().