Set-theoretic Models

Models¶

Models can be defined using Model class in mathesis.semantics.model. The class takes four arguments:

• domain: domain of objects of the model
• constants: a dictionary mapping constant symbols to objects
• predicates: a dictionary mapping predicate symbols to their extensions
• functions (Optional): a dictionary mapping function symbols to functions over the domain

In [1]:

from mathesis.grammars import BasicGrammar
from mathesis.semantics.model import Model

grammar = BasicGrammar(symbols={"conditional": "→"})

model = Model(
    domain={"a", "b", "c"},
    constants={
        "a": "a",
        "b": "b",
    },
    predicates={
        "P": {"a", "b"},
        "Q": {"a"},
        "R": {("a", "b"), ("c", "a")},
    },
)

from mathesis.grammars import BasicGrammar from mathesis.semantics.model import Model grammar = BasicGrammar(symbols={"conditional": "→"}) model = Model( domain={"a", "b", "c"}, constants={ "a": "a", "b": "b", }, predicates={ "P": {"a", "b"}, "Q": {"a"}, "R": {("a", "b"), ("c", "a")}, }, )

model.valuate() takes a formula and a variable assignment and returns the truth value of the formula in the model.

In [2]:

fml = grammar.parse("P(a) → R(x, b)")
model.valuate(fml, variable_assignment={"x": "c"})

fml = grammar.parse("P(a) → R(x, b)") model.valuate(fml, variable_assignment={"x": "c"})

Out[2]:

0

In [3]:

model.valuate(fml, variable_assignment={"x": "a"})

model.valuate(fml, variable_assignment={"x": "a"})

Out[3]:

1

model.validates() takes premises and conclusions and returns whether the model validates the inference.

In [4]:

fml = grammar.parse("∀x(∃y((Q(x)∨Q(b))→R(x, y)))")
model.validates(premises=[], conclusions=[fml])

fml = grammar.parse("∀x(∃y((Q(x)∨Q(b))→R(x, y)))") model.validates(premises=[], conclusions=[fml])

Out[4]:

True

Countermodel construction¶

WIP