Formula¶

class logics.classes.predicate.PredicateFormula(*args, **kwargs)¶

Class for representing predicate formulae.

Extends the propositional class Formula, but has some differences:

Atomics are now of the form ['R', 'a', 'x']
When the terms are applied function symbols, they must come as tuples, where the first element of the tuple is the function symbol, and the following are its arguments, e.g. ['R', ('f', ('f', 'x')), 'a'] represents the formula R(f(f(x)), a)
Now we have quantified formulae of the form ['∀', 'x', PredicateFormula]
Will also accept bounded quantified formulae of the form ['∀', 'x', '∈', term, PredicateFormula]

As in Formula, the __init__ method will turn inner lists into PredicateFormula, so you can write PredicateFormula(['~', ['P', 'x']]) instead of PredicateFormula(['~', PredicateFormula(['P', 'x'])])

Examples

>>> from logics.classes.predicate import PredicateFormula

The following are examples of predicate formulae (and are well-formed for logics.instances.predicate.languages.classical_function_language):

>>> PredicateFormula(['P', 'x'])
>>> PredicateFormula(['∧', ['~', ['P', 'a']],['X', 'a']])
>>> PredicateFormula(['R', 'a', 'b'])
>>> PredicateFormula(['P', ('f', ('g', 'a', 'x'))])
>>> PredicateFormula(['∀', 'x', ['P', 'x']])
>>> PredicateFormula(['∃', 'x', ['∀', 'X', ['X', 'x']]])
>>> PredicateFormula(['∀', 'x', '∈', ('f', 'a'), ['P', 'x']])

Some properties and methods are available because we are extending Formula

>>> from logics.instances.predicate.languages import classical_function_language
>>> PredicateFormula(['P', 'x']).is_schematic(classical_function_language)
False
>>> PredicateFormula(['∧', ['P', 'x'], ['A']]).is_schematic(classical_function_language)
True
>>> PredicateFormula(['∧', ['P', 'x'], ['A']]).main_symbol
'∧'
>>> PredicateFormula(['∃', 'x', ['∀', 'X', ['X', 'x']]]).depth
2
>>> PredicateFormula(['∃', 'x', ['∀', 'X', ['X', 'x']]]).subformulae
[['X', 'x'], ['∀', 'X', ['X', 'x']], ['∃', 'x', ['∀', 'X', ['X', 'x']]]]
>>> f = PredicateFormula(['∧', ['P', 'x'], ['A']])
>>> f.substitute(PredicateFormula(['P', 'x']), PredicateFormula(['Q', 'x']))
['∧', ['Q', 'x'], ['A']]
>>> f
['∧', ['P', 'x'], ['A']]
>>> f.instantiate(classical_function_language, {'A': PredicateFormula(['P', 'a'])})
['∧', ['P', 'x'], ['P', 'a']]
>>> f2 = PredicateFormula(['∧', ['P', 'x'], ['Q', 'x']])
>>> f2.schematic_substitute(classical_function_language,
...                         PredicateFormula(['∧', ['A'], ['B']]),
...                         PredicateFormula(['∧', ['B'], ['A']]))
['∧', ['Q', 'x'], ['P', 'x']]

You can also upgrade a propositional formula into a predicate formula using the logics.utils.upgrade module. Useful especially for defining predicate systems from propositional systems (see e.g., logics.instances.predicate.natural_deduction)

>>> from logics.classes.propositional import Formula
>>> from logics.utils.upgrade import upgrade_to_predicate_formula
>>> f = Formula(['~', ['A']])
>>> type(f)
<class 'logics.classes.propositional.formula.Formula'>
>>> f2 = upgrade_to_predicate_formula(f)
>>> f2
['~', ['A']]
>>> type(f2)
<class 'logics.classes.predicate.formula.PredicateFormula'>
>>> type(f2[1])
<class 'logics.classes.predicate.formula.PredicateFormula'>
>>> type(f)  # The original is unaffected, the function returns a new entity
<class 'logics.classes.propositional.formula.Formula'>

property is_atomic¶

Same as in propositional Formula. Overriden to work with this class.

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> PredicateFormula(['P', 'x']).is_atomic
True
>>> PredicateFormula(['∧', ['~', ['P', 'a']],['X', 'a']]).is_atomic
False

arguments(quantifiers=('∀', '∃'))¶

Same as in propositional Formula. Overriden in order to accomodate quantified formulae.

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> PredicateFormula(['∧', ['P', 'x'], ['A']]).arguments()
[['P', 'x'], ['A']]
>>> PredicateFormula(['∃', 'x', ['∀', 'X', ['X', 'x']]]).arguments()
[['∀', 'X', ['X', 'x']]]
>>> PredicateFormula(['∃', 'x', '∈', 'y', ['∀', 'X', ['X', 'x']]]).arguments()
[['∀', 'X', ['X', 'x']]]

Notes

If your language uses different quantifiers, pass them as a list of strings to the quantifiers parameter.

is_schematic(language)¶

Returns True if the formula contains an (individual, predicate or sentential) metavariable of the language, False otherwise

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> from logics.instances.predicate.languages import classical_predicate_language
>>> PredicateFormula(['P', 'a']).is_schematic(classical_predicate_language)
False
>>> PredicateFormula(['P', 'α']).is_schematic(classical_predicate_language)
True
>>> PredicateFormula(['∧', ['P', 'x'], ['A']]).is_schematic(classical_predicate_language)
True

free_variables(language, term=None, _bound_variables=None)¶

Returns the set of free variables inside a predicate formula or term

if term is None will evaluate the whole formula. Otherwise, will only evaluate the term given. _bound_variables is internal and should not be altered.

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> from logics.instances.predicate.languages import classical_function_language
>>> PredicateFormula(['∀', 'X', ['X', 'x']]).free_variables(classical_function_language)
{'x'}
>>> PredicateFormula(['∀', 'x', ['X', 'x']]).free_variables(classical_function_language)
{'X'}
>>> PredicateFormula(['∃', 'x', '∈', 'y', ['∀', 'X', ['X', 'x']]]).free_variables(classical_function_language)
{'y'}
>>> PredicateFormula(['∀', 'x', ['P', ('f', 'x')]]).free_variables(classical_function_language)
set()
>>> PredicateFormula(['∀', 'x', ['P', ('f', 'x')]]).free_variables(classical_function_language, term=('f', 'x'))
{'x'}

is_closed(language)¶

Determines if a formula is closed (i.e has no free variables)

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> from logics.instances.predicate.languages import classical_function_language
>>> PredicateFormula(['∀', 'X', ['X', 'x']]).is_closed(classical_function_language)
False
>>> PredicateFormula(['∀', 'X', ['∀', 'x', ['X', 'x']]]).is_closed(classical_function_language)
True

is_open(language)¶

Determines if a formula is open (i.e. has free variables)

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> from logics.instances.predicate.languages import classical_function_language
>>> PredicateFormula(['∀', 'X', ['X', 'x']]).is_open(classical_function_language)
True
>>> PredicateFormula(['∀', 'X', ['∀', 'x', ['X', 'x']]]).is_open(classical_function_language)
False

individual_constants_inside(language, ind_cts=None)¶

Returns a set of the individual constants that the formula contains

Parameters

language (logics.classes.predicate.language.PredicateLanguage or logics.classes.predicate.language.InfinitePredicateLanguage) – A predicate language
ind_cts (NoneType) – Internal, you should not alter this value

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> from logics.instances.predicate.languages import classical_function_language
>>> PredicateFormula(['P', 'a']).individual_constants_inside(classical_function_language)
{'a'}
>>> PredicateFormula(['R', 'a', ('f', 'b')]).individual_constants_inside(classical_function_language)
{'a', 'b'}
>>> PredicateFormula(['∀', 'x', ['P', 'x']]).individual_constants_inside(classical_function_language)
set()

contains_string(string)¶

Determines if a formula constains a given language item (useful, for various things internally), excluding connectives and base language

Examples

>>> from logics.utils.parsers.predicate_parser import classical_predicate_parser as parser
>>> f = parser.parse("forall x P(x) and ~R(a, f(b))")
>>> f.contains_string('R')
True
>>> f.contains_string('a')
True
>>> f.contains_string('x')
True
>>> f.contains_string('c')
False
>>> f.contains_string('y')
False
>>> f.contains_string('f')
True
>>> f.contains_string('f(b)')  # Looks at the actual parsed formula, not the unparsed one above
False

vsubstitute(variable, substitution, quantifiers=('∀', '∃'), term=None, _bound_variables=None)¶

Variable substitution method.

Returns the PredicateFormula that results from substituting the free occurences of variable for substitution.

Parameters

variable (str) – The variable whose free occurrences you wish to substitute
substitution (str or tuple) – The term you wish to substitute it with
quantifiers (tuple of str, optional) – By default, assumes that the quantifiers are ‘∀’, ‘∃’, so that you do not have to pass a language as argument; If you have different quantifiers, you can call this differently (e.g. quantifiers = your_language.quantifiers)
term (str or tuple, optional) – if you only wish to substitute inside a term, as in the free_variables method.
_bound_variables – Internal, you should not alter its value

Examples

>>> from logics.classes.predicate import PredicateFormula
>>> PredicateFormula(['P', 'x']).vsubstitute('x', 'a')
['P', 'a']
>>> PredicateFormula(['∀', 'x', ['P', 'x']]).vsubstitute('x', 'a')
['∀', 'x', ['P', 'x']]
>>> PredicateFormula(['∧', ['P', 'x'], ['∀', 'x', ['P', 'x']]]).vsubstitute('x', 'a')
['∧', ['P', 'a'], ['∀', 'x', ['P', 'x']]]
>>> PredicateFormula(['∀', 'x', ['X', 'x']]).vsubstitute('X', 'P')
['∀', 'x', ['P', 'x']]
>>> PredicateFormula(['∀', 'X', ['X', 'a']]).vsubstitute('X', 'P')
['∀', 'X', ['X', 'a']]
>>> # The bound is not under the scope of the quantifier:
>>> PredicateFormula(['∀', 'x', '∈', ('f', 'x'), ['P', 'x']]).vsubstitute('x', 'b')
['∀', 'x', '∈', ('f', 'b'), ['P', 'x']]