unicode_fol_kit.satisfies_so

unicode_fol_kit.satisfies_so(formula, structure, assignment=None, pred_binding=None)[source]

Return whether structure satisfies formula (second-order Tarski).

assignment maps object-variable names to individuals (as in semantics.tarski.satisfies()); pred_binding maps a bound predicate-variable name to its current relation (a set of argument tuples). Both default to empty and are threaded immutably.

Recursion:

  • Atom A(t1..tk): if A is currently bound (A in pred_binding), it is true iff the tuple of evaluated term values is in pred_binding[A] (an arity-0 bound A is true iff () in pred_binding[A]). Otherwise satisfaction falls back to the structure exactly as semantics.tarski.satisfies() does — including = as identity and ≠ as non-identity.

  • Not/And/Or/Xor/Implies/Iff: the classical truth tables.

  • Quantifier / SortedQuantifier (object-level): range over the domain (or the named sort), threading the same pred_binding.

  • SecondOrderQuantifier ∀P/k φ / ∃P/k φ: range P over every relation R ⊆ domain ** k (the powerset of all k-tuples). ∀ holds iff φ holds for all such R; ∃ iff for some. See the module docstring for the 2 ** (n ** k) complexity.

Raises:

  • ValueError – on a Łukasiewicz node (use the fuzzy evaluator), an unknown quantifier type / node type, or when a ∀P / ∃P would enumerate more than MAX_RELATIONS relations (a clear error instead of a hang — see the module docstring for the 2 ** (n ** k) cost).

  • NotImplementedError – on a lambda or modal node — these are out of scope for second-order predicate semantics (lambda: beta-reduce and lambda-eliminate first).

Parameters:
Return type:

bool