unicode_fol_kit.hybrid_is_valid

unicode_fol_kit.hybrid_is_valid(formula, frame='K', timeout=10000)[source]

Return True iff the hybrid-modal formula is valid over frame (via Z3).

Validity of H(@) over a frame class: true at EVERY world of EVERY Kripke model whose alethic relation satisfies the frame conditions, under EVERY nominal assignment. The check is the standard translation closed over the current world under the frame axioms:

frame_axioms  →  ∀w ST(formula)(w)

handed to the Z3 validity oracle. The nominal constants nom_i are left FREE in that implication — first-order validity quantifies free constants universally, which is exactly “for every nominal assignment” (each constant denotes exactly one domain element = one world, matching a nominal’s name-exactly-one-world semantics). frame is one of K / T / S4 / S5 and constrains the ALETHIC relation only.

Soundness/completeness: first-order validity is only semi-decidable in general, so is_valid may time out (returning False) on hard instances — but hybrid logic H(@) over K is DECIDABLE, and the ST images of H(@) formulas (two-variable-like, tiny) are well within Z3’s reach in practice; the frame-axiom variants used here (T/S4/S5) behave the same on these inputs. True is always a real proof; treat False as “not proven valid” (for these small hybrid instances: a genuine countermodel).

The ↓ binder (which makes hybrid validity undecidable) has no node type in this kit — deliberately out of scope.

Parameters:
Return type:

bool