Models¶

Model¶

class logics.classes.predicate.semantics.Model¶

Class for representing classical models

Extends dict. The keys should be:

m['domain'] = {d1, ..., dn} for the domain
m['item'] = ... for the language items

Note that:

Individual constants must denote members of the domain
Monadic predicate letters must denote a set of members of the domain
n(>1)-adic predicates must denote a set of n-tuples of members of the domain
Function symbols must denote ordered pairs (len 2-tuples) consisting of ((argument1, ..., argumentn), value), where the first element is a tuple of the arguments and the second the value for those arguments.

The domain can be any iterable (useful for infinite domains, e.g. for arithmetic, use itertools.count(0)) since the domain only takes a role in a loop (as the quantifier bound in unbounded quantified formulae). Predicates and function symbols can also denote callables (predicates must return truth values). See below.

fixed_denotations¶

Class attribute (an empty dict by default). For theories that have expressions with fixed denotations (for individual constants, predicates and/or function symbols), you can subclass Model and add those default denotations here. The way to do so is to use the symbol string as a key and give an element or a callable as value. See below for some examples.

Type:: dict

Examples

A model of an abstract logical theory:

>>> from logics.classes.predicate.semantics import Model
>>> model = Model({
...     'domain': {1, 2},
...     'a': 1,
...     'b': 2,
...     'P': {1},
...     'R': {(1,1), (1,2)},
...     'f': {((1,), 2), ((2,), 1)},
...     'g': {((1, 1), 1), ((1, 2), 2), ((2, 1), 1), ((2, 2), 2)}
... })

If your theory has some expressions with fixed default denotations, you can subclass Model and specify a different fixed_denotations dict. For instance:

>>> class ArithmeticModel(Model):
...     def __init__(self, *args, **kwargs):
...         super().__init__(*args, **kwargs)
...         self.fixed_denotations.update({
...             '0': 0,
...             's': lambda x: x + 1,  # note that the denotations below are all callables
...             '+': lambda x, y: x + y,
...             '*': lambda x, y: x * y,
...             '**': lambda x, y: x ** y,
...             '=': lambda x, y: '1' if x == y else '0',
...             '>': lambda x, y: '1' if x > y else '0',
...             '<': lambda x, y: '1' if x < y else '0',
...         })

As done above, it can be better to update the fixed_denotations in the __init__ method instead of overriding it completely, since then someone else will be able to subclass ArithmeticModel without repeating the definitions of all the arithmetical fixed denotations terms.

property domain¶

Property that returns the domain of the model

Is just syntactic sugar for model['domain']

Examples

>>> from logics.classes.predicate.semantics import Model
>>> model = Model({
...     'domain': {1, 2},
...     'a': 1,
...     'P': {1},
...     'R': {(1,1), (1,2)},
... })
>>> model.domain
{1, 2}

denotation(term, free_variable_denotation_dict=None)¶

Takes a (possibly complex) term and returns its denotation

Always call model.denotation(term) instead of model[term]. The second might not work properly, especially for terms containing function symbols.

Parameters:

term (str or tuple) – A simple or complex term
free_variable_denotation_dict (dict, optional) – You can pass an asignation (a dict specifying the denotations of variables).

Raises:

logics.classes.exceptions.DenotationError – If the term given as input does not have a denotation assigned

Examples

>>> from logics.classes.predicate.semantics import Model
>>> model = Model({
...     'domain': {1, 2},
...     'a': 1,
...     'b': 2,
...     'P': {1},
...     'R': {(1,1), (1,2)},
...     'f': {((1,), 2), ((2,), 1)},
...     'g': {((1, 1), 1), ((1, 2), 2), ((2, 1), 1), ((2, 2), 2)}
... })
>>> model.denotation('a')
1
>>> model.denotation('P')
{1}
>>> model.denotation('f')
{((2,), 1), ((1,), 1)}
>>> model.denotation(('f', 'a'))
2
>>> model.denotation(('f', ('f', 'a')))
1
>>> model.denotation(('g', ('f', 'a'), ('f', 'b')))
1
>>> model.denotation('1')
Traceback (most recent call last):
...
logics.classes.exceptions.DenotationError: Term 1 does not have a denotation assigned

Giving a free variable denotation dict

>>> model.denotation(('f', 'x'))  # variable without assignment
Traceback (most recent call last):
...
logics.classes.exceptions.DenotationError: Term x does not have a denotation assigned
>>> model.denotation(('f', 'x'), {'x': 1})  # variable with assignment
2

Note that fixed denotations of the model class will be respected

>>> from logics.instances.predicate.model_subclasses import ArithmeticModel
>>> from itertools import count
>>> arithmetic_model = ArithmeticModel({'domain': count(0)})
>>> # The instance is empty except for the domain because every term has a default denotation in arithmetic
>>> arithmetic_model.denotation('0')
0
>>> arithmetic_model.denotation(('s', '0'))
1
>>> arithmetic_model.denotation(('+', ('s', '0'), ('s', '0')))
2

predicate_variable_quantification_range(variable_arity)¶

Returns the quantification range of a predicate variable as an iterator

If monadic, returns the powerset of the domain. If n-adic returns returns the powerset of D^2, etc. Note that it won’t actually return a set but an iterator (makes it much faster for computing valuations).

Examples

>>> from logics.classes.predicate.semantics import Model
>>> model = Model({'domain': {1, 2}})
>>> iter1 = model.predicate_variable_quantification_range(variable_arity=1)
>>> type(iter1)
<class 'generator'>
>>> for x in iter1:
...     print(x)
set()
{1}
{2}
{1, 2}
>>> iter2 = model.predicate_variable_quantification_range(variable_arity=2)
>>> for x in iter2:
...     print(x)
set()
{(1, 1)}
{(1, 2)}
{(2, 1)}
{(2, 2)}
{(1, 1), (1, 2)}
{(1, 1), (2, 1)}
{(1, 1), (2, 2)}
{(1, 2), (2, 1)}
{(1, 2), (2, 2)}
{(2, 1), (2, 2)}
{(1, 1), (1, 2), (2, 1)}
{(1, 1), (1, 2), (2, 2)}
{(1, 1), (2, 1), (2, 2)}
{(1, 2), (2, 1), (2, 2)}
{(1, 1), (1, 2), (2, 1), (2, 2)}

Subclasses¶

logics.instances.predicate.model_subclasses.ArithmeticModel¶: Includes fixed denotations for ‘0’, ‘s’, ‘+’, ‘*’, ‘**’, ‘=’, ‘>’, ‘<’

logics.instances.predicate.model_subclasses.RealNumberArithmeticModel¶: Includes fixed denotations for ‘+’, ‘-’, ‘*’, ‘/’, ‘//, ‘**’, ‘=’, ‘>’, ‘<’. Also extends the denotation method in order in order to return one for the numerals and floats.

Model Theory¶

class logics.classes.predicate.semantics.ModelTheory(language, truth_values, designated_value, truth_function_dict, sentential_constant_values_dict=None, use_molecular_valuation_fast_version=False, use_quantifier_fast_version=False)¶

Classical model theory

Parameters:

language (language: logics.classes.predicate.PredicateLanguage or logics.classes.predicate.InfinitePredicateLanguage) – Instance of PredicateLanguage or InfinitePredicateLanguage
truth_values (list) – A list of the truth values (which may be int, str, etc.). In the instances below I use strings.
designated_value – a member of truth_values, should be the one that represents truth
truth_function_dict (dict) – Dict containing the logical constants (str) as keys, and n-dimensional lists as values (for constants of arity n). Will also accept any indexable (things with a __getitem__ method, e.g. numpy arrays) and any n-ary callable. The clause for atomic formulae must be given with the key 'atomic', and take two parameters, for the predicate denotation and the term denotations (see below)
sentential_constant_values_dict (dict) – Dict containing the sentential constans (str) as keys, and their truth values (members of truth_values) as values
use_molecular_valuation_fast_version (bool, optional) – Implements a faster version of the molecular valuation function (e.g. if asked for a disjunction will return ‘1’ with one true disjunct, without evaluating the other). In counterpart, it is less general, since it assumes the Kleene truth matrices. Defaults to False.
use_quantifier_fast_version (bool, optional) – Same as above for quantifiers. Assumes that the universal quantifier behaves as the K3 conjunction, and the existential quantifier as the K3 disjunction. Defaults to False.

Examples

We define a model theory for second-order classical logic with 2 function symbols and sentential constants (also present as a predefined instance, see below)

>>> from logics.classes.predicate.semantics.models import ModelTheory
>>> from logics.instances.predicate.languages import classical_function_language
>>> bivalued_truth_values = ['1', '0']
>>> # The order is important for the lines below, see many-valued semantics
>>> classical_truth_functions = {
...     '~': ['0', '1'],
...     '∧': [ #1   #0
...           ['1', '0'],    # 1
...           ['0', '0']],   # 0
...     '∨': [ #1   #0
...           ['1', '1'],    # 1
...           ['1', '0']],   # 0
...     '→': [ #1   #0
...           ['1', '0'],    # 1
...           ['1', '1']],   # 0
...     '↔': [ #1   #0
...           ['1', '0'],    # 1
...           ['0', '1']],   # 0
...     '∀': lambda *args: '0' if '0' in args else '1',  # remember that the value can be a callable
...     '∃': lambda *args: '1' if '1' in args else '0',
...     'atomic': lambda pred_denotation, term_denotations: '1' if term_denotations in pred_denotation else '0'
... }
>>> model_theory = ModelTheory(language=classical_function_language,
...                            truth_values=['1', '0'],
...                            designated_value='1',
...                            truth_function_dict=classical_truth_functions,
...                            sentential_constant_values_dict={'⊥': '0', '⊤': '1'},
...                            use_molecular_valuation_fast_version=True,
...                            use_quantifier_fast_version=True)

apply_truth_function(constant, *args)¶

Gets the value of a truth function applied to a given set of arguments.

Works independently of whether the truth function for the constant is a callable or an indexible.

Examples

>>> from logics.instances.predicate.model_semantics import classical_functional_model_semantics
>>> classical_functional_model_semantics.apply_truth_function('~', '0')
'1'
>>> classical_functional_model_semantics.apply_truth_function('~', '1')
'0'
>>> classical_functional_model_semantics.apply_truth_function('∃', '0', '1', '0')
'1'
>>> classical_functional_model_semantics.apply_truth_function('∀', '0', '1', '0')
'0'
>>> classical_functional_model_semantics.apply_truth_function('atomic', {1, 2, 3}, 1)
'1'
>>> classical_functional_model_semantics.apply_truth_function('atomic', {(1, 1),(2, 1)}, (1, 2))
'0'

valuation(formula, model, free_variable_denotation_dict=None)¶

Returns the valuation of a formula, given some valuations for the atomics.

Parameters:

formula (logics.classes.predicate.PredicateFormula) – The formula of which you want to know the valuation
model (logics.classes.predicate.semantics.Model) – The model to use
free_variable_denotation_dict (dict, optional) – You can pass an asignation (a dict specifying the denotations of variables). Most often you will want to leave this as None in this method.

Raises:

logics.classes.exceptions.DenotationError – If some term or variable within the formula given as input does not have a denotation assigned in the model

Examples

>>> from logics.classes.predicate.semantics import Model
>>> from logics.utils.parsers.predicate_parser import classical_predicate_parser as parser
>>> from logics.instances.predicate.model_semantics import classical_functional_model_semantics
>>> model = Model({
...     'domain': {1, 2},
...     'a': 1,
...     'b': 2,
...     'P': {1},
...     'R': {(1,1), (1,2)},
...     'f': {((1,), 2), ((2,), 1)},
...     'g': {((1, 1), 1), ((1, 2), 2), ((2, 1), 1), ((2, 2), 2)}
... })
>>> classical_functional_model_semantics.valuation(parser.parse("P(a)"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("R(a, b)"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("R(f(a), g(f(a), b))"), model)
'0'
>>> classical_functional_model_semantics.valuation(parser.parse("exists x (P(f(x)))"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("forall X (exists x (X(f(x))))"), model)
'0'

Once again, if you have fixed denotations, the method will respect them

>>> from itertools import count
>>> from logics.instances.predicate.model_subclasses import ArithmeticModel
>>> from logics.utils.parsers.predicate_parser import arithmetic_parser
>>> from logics.instances.predicate.model_semantics import arithmetic_model_semantics
>>> arithmetic_model = ArithmeticModel({'domain': count(0)})
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) > 0"), arithmetic_model)
'1'
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) + s(0) = s(s(0))"), arithmetic_model)
'1'
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("exists x (x = s(0))"), arithmetic_model)
'1'  [Note that it returns because use_quantifier_fast_version is enabled. Otherwise it would get stuck]
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("exists x (s(x) = 0)"), arithmetic_model)
[The program freezes, as it keeps looping through the natural numbers...]

Instances¶

logics.instances.predicate.model_semantics.classical_model_semantics¶: Model theory for second-order classical logic (for the language classical_infinite_predicate_language). No function symbols.

logics.instances.predicate.model_semantics.classical_functional_model_semantics¶: Same as the above, for the language classical_function_language. Is exemplified in the class above.

logics.instances.predicate.model_semantics.arithmetic_model_semantics¶: Model theory for second-order natural-number arithmetic. For the language arithmetic_language.

logics.instances.predicate.model_semantics.realnumber_arithmetic_model_semantics¶: Model theory for second-order real-number arithmetic. For the language real_number_arithmetic_language.

Model Finder¶

class logics.utils.solvers.model_finder.ModelFinder¶

find_model(formula, sought_value, logic)¶

Given a formula, a sought thuth value and a logic, returns a Model that assigns the sought value to the formula (if it can find one)

Has an instance (logics.utils.solvers.model_finder.classical_model_finder) predefined

Parameters:

formula (logics.classes.predicate.Formula) – The Formula which must be given the sought value
sought_value (str) – The truth value that will get assigned to the formula in the model (in the predefined instances, an str)
logic (logics.classes.predicate.semantics.ModelTheory) – The model theory that the algorithm will utilize to construct a model

Returns:

A Model instance

Return type:

logics.classes.predicate.semantics.Model

Raises:

logics.classes.exceptions.SolverError – If it cannot find a model that gives the desired value to the formula

Examples

>>> from logics.utils.parsers import classical_predicate_parser
>>> from logics.utils.solvers.model_finder import classical_model_finder
>>> from logics.instances.predicate.model_semantics import classical_model_semantics
>>> f = classical_predicate_parser.parse("exists x P(x) and ~P(a)")
>>> classical_model_finder.find_model(f, "1", classical_model_semantics)
{'domain': {'1', '2'}, 'a': '1', 'P': {'2'}}
>>> classical_model_finder.find_model(f, "0", classical_model_semantics)
{'domain': {'1'}, 'a': '1', 'P': {'1'}}

Notes

Will construct a model of at most cardinality max_domain_cardinality (class param)
For now it has only been tested with classical model theory, will probably need some adjustments for non-classical model theories
For now does not work with function symbols
Will not work with open formulae