unicode_fol_kit.semantics.matrix

Finite-valued logical matrices: a generalisation of the K3 / LP three-valued layer.

A logical matrix is a finite set of truth values, a distinguished subset of designated values (those that count as assertible), and a truth table for each connective. Validity is “designated under every assignment”, satisfiability is “designated under some assignment”, and Γ ⊨ φ is “every assignment that designates all of Γ designates φ”. This module makes that schema first-class so any finite many-valued logic — not just the hard-wired {0, ½, 1} of unicode_fol_kit.semantics.manyvalued — can be evaluated and decided.

Three matrices ship built in:

  • K3_MATRIX — Kleene’s strong three-valued logic (designate {1});

  • LP_MATRIX — Priest’s Logic of Paradox (designate {½, 1});

  • FDE_MATRIX — the Belnap–Dunn four-valued logic FDE (first-degree entailment), values T/F/N (neither)/B (both), designate the true-containing values {T, B}. FDE is both paraconsistent (p ∧ ¬p ⊭ q) and paracomplete (p ⊭ q ∨ ¬q), and — unlike K3/LP — has no logical truths at all (even p → p fails, taking value N at N).

K3 and LP are re-expressed here as matrices, so this layer reproduces the existing three-valued decisions exactly (cross-checked in the tests). Build your own with TruthMatrix.from_functions().

Public API: TruthMatrix, matrix_value(), matrix_is_valid(), matrix_is_satisfiable(), matrix_entails(), and the matrices K3_MATRIX, LP_MATRIX, FDE_MATRIX. MATRICES maps the names "K3" / "LP" / "FDE" to them.

Functions

matrix_entails(premises, conclusion, matrix)

True iff every assignment designating all premises designates conclusion.

matrix_is_satisfiable(formula, matrix[, domain])

True iff formula is designated under some assignment over matrix.

matrix_is_valid(formula, matrix[, domain])

True iff formula is designated under every assignment over matrix.

matrix_value(formula, valuation, matrix[, ...])

Evaluate formula to a matrix value under valuation.

Classes

TruthMatrix(name, values, designated, neg, ...)

A finite logical matrix: values, designated values, and connective tables.
class unicode_fol_kit.semantics.matrix.TruthMatrix(name, values, designated, neg, conj, disj, impl, iff, xor)[source]

Bases: object

A finite logical matrix: values, designated values, and connective tables.

The connective tables are plain dicts (neg[v], conj[(a, b)], …) so a matrix is fully data-driven; build one directly, or — more conveniently — with from_functions() from value-level operations. ∀ / ∃ are read as the iterated conj / disj over a finite domain (a generalised min / max), so the matrix needs no separate quantifier tables.

Parameters:
name: str
values: Tuple[Hashable, ...]
designated: FrozenSet[Hashable]
neg: Dict[Hashable, Hashable]
conj: Dict[Tuple[Hashable, Hashable], Hashable]
disj: Dict[Tuple[Hashable, Hashable], Hashable]
impl: Dict[Tuple[Hashable, Hashable], Hashable]
iff: Dict[Tuple[Hashable, Hashable], Hashable]
xor: Dict[Tuple[Hashable, Hashable], Hashable]
static from_functions(name, values, designated, neg, conj, disj, impl=None)[source]

Materialise a matrix from value-level operations.

impl defaults to the material conditional ¬a ∨ b; the biconditional is (a→b) ∧ (b→a) and exclusive-or is ¬(a↔b). Every operation is checked to land back in values (a closed matrix), and every designated value to be a value, so a malformed table is caught at build time.

Parameters:
Return type:

TruthMatrix

is_designated(v)[source]

True iff v is a designated (assertible) value of this matrix.

Parameters:

v (Hashable)

Return type:

bool

unicode_fol_kit.semantics.matrix.matrix_value(formula, valuation, matrix, domain=None)[source]

Evaluate formula to a matrix value under valuation.

valuation maps each ground atom’s to_unicode_str() key to a value of matrix. Quantifiers fold conj (∀) / disj (∃) over domain (a set of constant names), generalising min/max. A missing atom key raises KeyError; a value outside the matrix raises ValueError; a modal/fuzzy/sorted/lambda node is rejected with the same message kleene_value() uses.

Parameters:
Return type:

Hashable

unicode_fol_kit.semantics.matrix.matrix_is_valid(formula, matrix, domain=None)[source]

True iff formula is designated under every assignment over matrix.

Enumerates len(matrix.values) ** n assignments of the n distinct ground atoms (after grounding quantifiers over domain). Exponential in n; capped at manyvalued.MAX_MODELS.

Parameters:
Return type:

bool

unicode_fol_kit.semantics.matrix.matrix_is_satisfiable(formula, matrix, domain=None)[source]

True iff formula is designated under some assignment over matrix.

Parameters:
Return type:

bool

unicode_fol_kit.semantics.matrix.matrix_entails(premises, conclusion, matrix, domain=None)[source]

True iff every assignment designating all premises designates conclusion.

Matrix consequence: Γ ⊨ φ holds when no assignment over matrix makes every premise designated yet the conclusion undesignated.

Parameters:
Return type:

bool