unicode_fol_kit.int_countermodel

unicode_fol_kit.int_countermodel(formula, max_worlds=3, domain_elements=2, max_steps=300000)

Return (model, world) where formula fails intuitionistically, or None.

For a propositional formula this is a decision procedure: it searches every Kripke model up to max_worlds worlds (intuitionistic propositional logic has the finite-model property), so None proves validity. For a first-order formula (containing ∀/∃) it is a bounded search over increasing-domain Kripke models (the formula’s constants plus domain_elements fresh individuals, up to max_steps valuations): a returned model genuinely refutes validity, but None only means “no counter-model within the bounds” — first-order intuitionistic logic is undecidable.

Parameters:

• formula (Node)

• max_worlds (int)

• domain_elements (int)

• max_steps (int)

Return type:

Tuple[IntKripkeModel, int] | None