Language¶

class logics.classes.predicate.PredicateLanguage(individual_constants=None, individual_metavariables=None, variables=None, variable_metavariables=None, quantifiers=None, metavariables=None, constant_arity_dict=None, predicate_letters=None, predicate_variables=None, function_symbols=None, sentential_constants=None, allow_predicates_as_terms=False)¶

Class for predicate languages with a finite number of predicates and individual constants.

Extends logics.classes.propositional.Language, adding some extra parameters and methods. It is safer to use single character strings for each of the parameters. In the parser you will be able to use longer strings. Needless to say, do not repeat any strings among the parameters.

Parameters:

individual_constants (list of str, optional) – A list of strings (valid letters for individual constants). Can also be a callable (a function).
individual_metavariables (list of str, optional) – A list of strings. Can be instantiated with ind cts. Are part of the metalanguage, any formula containing them is schematic. Useful for formulating rules.
variables (list of str, optional) – A list of strings (valid letters for variables). Will consider any variable + a digit a valid variable. Are part of the base language, can appear quantified over in non-schematic formulae.
variable_metavariables (list of str, optional) – Same as individual_metavariables, but can be instantiated with variables.
quantifiers (list of str, optional) – A list of strings (valid letters for quantifiers)
metavariables (list of str, optional) – A list of strings (valid letters for sentential metavariables)
constant_arity_dict (dict, optional) – a dictionary that contains str (logical cosntant symbols) as keys, and positive int (arities) as values
predicate_letters (dict, optional) – a dictionary that contains str (predicate letter symbols) as keys, and positive int (arities) as values
predicate_variables (dict, optional) – a dictionary that contains str (predicate variable symbols) as keys, and positive int (arities) as values. Will consider any variable + a digit a valid variable. Are part of the base language, , can appear quantified over in non-schematic formulae.
function_symbols (dict, optional) – a dictionary that contains str (function symbols) as keys, and positive int (arities) as values
sentential_constants (list of str, optional) – A list of strings (representing sentential constants)
allow_predicates_as_terms (bool, optional) – If true, if P is a predicate, allows one to say things like ∀x ∈ P (Formula). Defaults to False

Examples

Example language containing some of the above

>>> from logics.classes.predicate import PredicateLanguage
>>> language = PredicateLanguage(individual_constants=['a', 'b', 'c', 'd'],
...                              variables=['x', 'y', 'z'],
...                              quantifiers=['∀', '∃'],
...                              metavariables=['A', 'B', 'C'],
...                              constant_arity_dict={'~': 1, '∧': 2, '∨': 2, '→': 2, '↔': 2},
...                              predicate_letters={'P': 1, 'Q': 1, 'R': 2, 'S': 3},
...                              predicate_variables={'X': 1, 'Y': 1, 'Z': 2},
...                              sentential_constants=['⊥', '⊤'],
...                              function_symbols={'f': 1, 'g': 2})

Language of second-order arithmetic

>>> arithmetic_language = PredicateLanguage(individual_constants=['0'],
...                                         variables=['x', 'y', 'z'],
...                                         quantifiers=['∀', '∃'],
...                                         metavariables=['A', 'B', 'C'],
...                                         constant_arity_dict={'~': 1, '∧': 2, '∨': 2, '→': 2, '↔': 2},
...                                         predicate_letters={'=': 2, '>': 2, '<': 2},
...                                         predicate_variables={'X': 1, 'Y': 1, 'Z': 2},
...                                         function_symbols={'s': 1, '+': 2, '*': 2, '**': 2})

Examples of methods present because we are extending the propositional Language class

>>> arithmetic_language.constants(1)
{'~'}
>>> arithmetic_language.is_metavariable_string('A')
True
>>> from logics.classes.predicate import PredicateFormula
>>> arithmetic_language.is_well_formed(PredicateFormula(['~', ['=', ('s', '0'), '0']]))
True
>>> arithmetic_language.is_well_formed(PredicateFormula(['~', '~', ['=', ('s', '0'), '0']]))
False
>>> arithmetic_language.is_well_formed(PredicateFormula(['~', '~', ['=', ('s', '0'), '0']]), return_error=True)
(False, "['~', '~', ['=', ('s', '0'), '0']] is not well-formed: Number of arguments does not coincide with the arity of the logical constant")

Even in finite PredicateLanguage’s there is always an infinite supply of both individual and predicate variables

>>> language.is_well_formed(PredicateFormula(['P', 'x']))
True
>>> language.is_well_formed(PredicateFormula(['P', 'x23']))
True
>>> language.is_well_formed(PredicateFormula(['X', 'x23']))
True
>>> language.is_well_formed(PredicateFormula(['X1', 'x23']))
True

Parameter individual_constants can also be a callable. For instance:

>>> # The arithmetic language defined above has only '0' as its individual constant
>>> arithmetic_language.is_well_formed(PredicateFormula(['=', '0', '0']))
True
>>> arithmetic_language.is_well_formed(PredicateFormula(['=', '1', '1']))
False
>>> # To define an arithmetical language with all numerals, we can pass a function to individual_constants
>>> arithmetic_numeral_language = PredicateLanguage(individual_constants=lambda x: x.isdigit(),
...                                                 # Not the best way to do it, but simple for illustration
...                                                 variables=['x', 'y', 'z'],
...                                                 quantifiers=['∀', '∃'],
...                                                 metavariables=['A', 'B', 'C'],
...                                                 constant_arity_dict={'~': 1, '∧': 2, '∨': 2, '→': 2, '↔': 2},
...                                                 predicate_letters={'=': 2, '>': 2, '<': 2},
...                                                 predicate_variables={'X': 1, 'Y': 1, 'Z': 2},
...                                                 function_symbols={'s': 1, '+': 2, '*': 2, '**': 2})
>>> arithmetic_numeral_language.is_well_formed(PredicateFormula(['=', '0', '0']))
True
>>> arithmetic_numeral_language.is_well_formed(PredicateFormula(['=', '1', '1']))
True

predicates(arity=None)¶

Returns the set of predicates of a given arity. If arity is None, will return the set of all predicates

Examples

>>> from logics.instances.predicate.languages import classical_predicate_language
>>> classical_predicate_language.predicates(1)
{'P', 'Q'}
>>> classical_predicate_language.predicates()
{'R', 'S', 'P', 'Q'}

arity(string)¶

Overriden from the base class to include the arities of predicate letters, variables, metavariables, function symbols and quantifiers

Raises:: KeyError – If the string is not present in any of those parameters

Examples

>>> from logics.instances.predicate.languages import classical_function_language
>>> classical_function_language.arity('∀')
1
>>> classical_function_language.arity('~')
1
>>> classical_function_language.arity('∧')
2
>>> classical_function_language.arity('P')  # predicate letter
1
>>> classical_function_language.arity('Z')  # predicate variable
2
>>> classical_function_language.arity('f')  # function symbol
1
>>> classical_function_language.arity('Π')  # predicate metavariable
1

is_atomic_string(string)¶: Determines if a string is among the atomics of the language. See below for some examples.

is_metavariable_string(string)¶: Determines if a string is among the (individual/predicate/formula) metavariables of the language.

class logics.classes.predicate.InfinitePredicateLanguage(individual_constants=None, individual_metavariables=None, variables=None, variable_metavariables=None, quantifiers=None, metavariables=None, constant_arity_dict=None, predicate_letters=None, predicate_variables=None, function_symbols=None, sentential_constants=None, allow_predicates_as_terms=False)¶

Language that also considers expressions to be well-formed in case a variable, individual constant or metavariable is followed by a digit

Examples

>>> from logics.classes.predicate import InfinitePredicateLanguage, PredicateFormula
>>> language = InfinitePredicateLanguage(individual_constants=['a', 'b', 'c', 'd'],
...                                      variables=['x', 'y', 'z'],
...                                      quantifiers=['∀', '∃'],
...                                      metavariables=['A', 'B', 'C'],
...                                      constant_arity_dict={'~': 1, '∧': 2, '∨': 2, '→': 2, '↔': 2},
...                                      predicate_letters={'P': 1, 'Q': 1, 'R': 2, 'S': 3},
...                                      predicate_variables={'X': 1, 'Y': 1, 'Z': 2})
>>> language.is_well_formed(PredicateFormula(['P', 'a']))
True
>>> language.is_well_formed(PredicateFormula(['P', 'a23']))
True
>>> language.is_well_formed(PredicateFormula(['P1', 'a23']))
True
>>> language.is_well_formed(PredicateFormula(['A1']))
True

Instances¶

Abstract/logical languages:

logics.instances.predicate.languages.classical_predicate_language¶: Finite language, with constants a, b, c, d, e; Variables x, y, z; Predicate letters P (1), Q (1), R (2), S (3), M (1), N (1), T (2); Predicate variables X (1), Y (1), Z (2); Sentential constants ⊥, ⊤; Constants ~, ∧, ∨, →, ↔; Quantifiers ∀, ∃; Sentential Metavariables A, B, C; Individual Constant Metavariables α, β, γ, δ, ε and Variable Metavariables χ, ψ, ω.

logics.instances.predicate.languages.classical_infinite_predicate_language¶: InfiniteLanguage version of the above.

logics.instances.predicate.languages.classical_function_language¶: Identical to the InfiniteLanguage above, adding f (1) and g (2) function symbols.

Arithmetic languages:

logics.instances.predicate.languages.arithmetic_language¶: Identical to the arithmetic_language defined above in the examples.

logics.instances.predicate.languages.real_number_arithmetic_language¶: Similar to arithmetic_language above, but will accept any string convertible to an int or a float as constant. Also adds binary functions / and // (intuitively division and integer division).