unicode_fol_kit.rel_countermodel

unicode_fol_kit.rel_countermodel(formula, max_worlds=2)[source]

Return (model, world) where formula fails at a normal world, or None.

EXHAUSTIVE search over every simplified Routley–Meyer interpretation with |W| ≤ max_worlds worlds and exactly ONE normal world "w0": every involution for *, every R ⊆ (W∖N) × W × W, and every valuation of the formula’s atoms. The returned countermodel is verified with rel_satisfies() before it is returned (the search’s failure check is that call), so a non-None result definitively refutes validity in B.

One normal world is WLOG for countermodel existence: if φ fails at a normal world w0 of any interpretation, demote every other normal world w to non-normal and add the triples R(w, x, x) for all x — the demoted →-clause with those triples coincides with the normal-world clause, the other clauses never mention N, so every truth value is preserved and w0 (relabelled first) still refutes φ. The search enumerates ALL R, so it covers that transformed interpretation.

The space is EXPONENTIAL: about inv(n) · 2^((n-1)·n²) · 2^(n·a) interpretations for n worlds and a atoms. max_worlds=2 with ≤ 3 atoms is ~2·16·64 ≈ 2000 models (well under a second); max_worlds=3 with 3 atoms is already ≈ 5·10⁸ — keep the bound tiny.

Parameters:
Return type:

Tuple[RelevantModel, str] | None