unicode_fol_kit.semantics.free_logic

Free logic — first-order logic without the existence assumption.

Classical FOL assumes every term denotes an existing individual, so universal instantiation ∀x φ → φ(c) and existential generalisation φ(c) → ∃x φ are valid. Free logic drops that assumption: quantifiers range only over an inner domain of existing objects E, while constants and function terms may denote an object of the wider outer domain, or fail to denote at all. An existence predicate E!(t) says “t denotes an existing object”, and the classical inference rules hold only in their guarded forms (∀x φ ∧ E!(c)) → φ(c) and (φ(c) ∧ E!(c)) → ∃x φ.

A FreeModel carries an outer domain, the existing inner subset, a (possibly partial) constant/function interpretation, and predicate tables over the outer domain. Two policies for an atom that contains a non-denoting term:

  • "negative" (default) — the atom is simply false (negative free logic; t = t then also fails when t does not denote);

  • "positive" — self-identity t = t is true for any term, while every other atom with a non-denoting term is false (the common positive-free-logic convention for identity).

Public API: FreeModel, NONDENOTING, free_satisfies(), free_holds().

Functions

free_holds(formula, model[, policy])

Convenience: free_satisfies of a closed formula (empty assignment).

free_satisfies(formula, model[, assignment, ...])

Return whether model satisfies formula under free-logic semantics.

Classes

FreeModel(outer, existing[, constants, ...])

A free-logic model: an inner existing domain inside an outer domain.
class unicode_fol_kit.semantics.free_logic.FreeModel(outer, existing, constants=<factory>, functions=<factory>, predicates=<factory>)[source]

Bases: object

A free-logic model: an inner existing domain inside an outer domain.

outer lists every object (existing or merely possible); existing is the inner domain the quantifiers range over (⊆ outer). constants maps a name to an outer element — a name absent from the map is non-denoting. functions maps (name, arity) to a partial table {argtuple: value} (a missing entry, or any non-denoting argument, makes the application non-denoting). predicates maps (name, arity) to a set of outer tuples.

Parameters:
outer: Tuple[Any, ...]
existing: FrozenSet[Any]
constants: Mapping[str, Any]
functions: Mapping[Tuple[str, int], Mapping[Tuple[Any, ...], Any]]
predicates: Mapping[Tuple[str, int], FrozenSet[Tuple[Any, ...]]]
unicode_fol_kit.semantics.free_logic.free_satisfies(formula, model, assignment=None, policy='negative')[source]

Return whether model satisfies formula under free-logic semantics.

Quantifiers range over model.existing; E!(t) is true iff t denotes an existing object; an atom with a non-denoting term is handled per policy ("negative" / "positive" — see the module docstring).

Parameters:
Return type:

bool

unicode_fol_kit.semantics.free_logic.free_holds(formula, model, policy='negative')[source]

Convenience: free_satisfies of a closed formula (empty assignment).

Parameters:
Return type:

bool