Language¶

class logics.classes.propositional.Language(atomics=None, constant_arity_dict=None, sentential_constants=None, metavariables=None, context_variables=None)¶

Class for propositional languages with a finite number of atomics.

Parameters:

atomics (list of str, optional) – A list of strings (valid letters for atomics)
constant_arity_dict (dict, optional) – a dictionary that contains str (logical cosntant symbols) as keys, and positive int (arities) as values
sentential_constants (list of str, optional) – A list of strings (representing sentential constants)
metavariables (list of str, optional) – A list of strings (valid letters for atomic metavariables)
context_variables (list of str, optional) – A list of strings (representing context variables, i.e. sequences of formulae). Used mainly in sequent calculi

Notes

Do not repeat symbols among any of the parameters above. It is preferable to use single character strings for each. If you want longer strings, you will be able to use them in the parser

Examples

A propositional language containing 3 atomics, negation and conjunction, and some context variables:

>>> from logics.classes.propositional import Language
>>> language = Language(atomics=['p', 'q', 'r'],
...                     constant_arity_dict={'~': 1, '∧': 2},
...                     sentential_constants=['⊥', '⊤'],
...                     metavariables=['A', 'B', 'C'],
...                     context_variables=['Γ', 'Δ', 'Σ', 'Λ', 'Π', 'Θ'])

arity(constant)¶

Returns the arity of a logical constant.

Raises:: KeyError – If the string is not present in constant_arity_dict

Examples

>>> from logics.instances.propositional.languages import classical_language
>>> classical_language.arity('~')
1
>>> classical_language.arity('∧')
2

constants(arity=None)¶

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

Examples

>>> from logics.instances.propositional.languages import classical_language
>>> classical_language.constants(1)
{'~'}
>>> classical_language.constants()
{'∧', '→', '∨', '~', '↔'}

is_well_formed(formula, return_error=False)¶

Determines if a formula is well-formed for the Language.

Parameters:

formula (logics.classes.propositional.Formula) – an instance of Formula
return_error (bool) – If True, will return a tuple containing (bool, str). The str contains an informative message detailing why the formula is not well-formed, in case it isn’t. Otherwise the str is '' . If False (default value) the method will just return a boolean.

Examples

>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional import Formula
>>> classical_language.is_well_formed(Formula(['p']))
True
>>> classical_language.is_well_formed(Formula(['~', ['p']]))
True
>>> classical_language.is_well_formed(Formula(['~', ['~', ['p']]]))
True
>>> classical_language.is_well_formed(Formula(['~', ['~', ['p']]]), return_error=True)
(True, '')
>>> classical_language.is_well_formed(Formula(['~', '~', ['p']]))
False
>>> classical_language.is_well_formed(Formula(['~', '~', ['p']]), return_error=True)
(False, "['~', '~', ['p']] is not well-formed: Number of arguments does not coincide with the arity of the logical constant")

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

is_sentential_constant_string(string)¶: Determines if a string is among the sentential constants of the language. See below for some examples.

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

is_context_variable_string(string)¶

Determines if a string is among the context variables of the language

Examples

>>> from logics.instances.propositional.languages import classical_language_with_sent_constants
>>> classical_language_with_sent_constants.is_atomic_string('p')
True
>>> classical_language_with_sent_constants.is_atomic_string('b')
False
>>> classical_language_with_sent_constants.is_sentential_constant_string('⊥')
True
>>> classical_language_with_sent_constants.is_metavariable_string('A')
True
>>> classical_language_with_sent_constants.is_metavariable_string('F')
False
>>> classical_language_with_sent_constants.is_context_variable_string('Γ')
True

class logics.classes.propositional.InfiniteLanguage(atomics=None, constant_arity_dict=None, sentential_constants=None, metavariables=None, context_variables=None)¶

Same as Language but with an indefinite supply of atomics and metavariables.

Will consider a string in atomics + a digit a well-formed formula. Same with metavariables.

Examples

>>> from logics.classes.propositional import InfiniteLanguage
>>> infinite_language = InfiniteLanguage(atomics=['p', 'q', 'r'],
...                                      constant_arity_dict={'~': 1, '∧': 2},
...                                      sentential_constants=['⊥', '⊤'],
...                                      metavariables=['A', 'B', 'C'])

>>> infinite_language.is_atomic_string('p')
True
>>> infinite_language.is_atomic_string('p1')
True
>>> infinite_language.is_atomic_string('p234')
True
>>> infinite_language.is_metavariable_string('A')
True
>>> infinite_language.is_metavariable_string('A234')
True

>>> from logics.classes.propositional import Formula
>>> infinite_language.is_well_formed(Formula(['p']))
    True
>>> infinite_language.is_well_formed(Formula(['p234']))
    True
>>> infinite_language.is_well_formed(Formula(['~', ['p234']]))
    True

Instances¶

The following are predefined instances of Language and InfiniteLanguage.

logics.instances.propositional.languages.classical_language¶: Classical finite language. Contains atomics p, q, r, s, t, metavariables A, B, C, D constants ~, ∧, ∨, →, ↔ and context variables Γ, Δ, Σ, Λ, Π, Θ.

logics.instances.propositional.languages.classical_infinite_language¶: Same as above but with an indefinite supply of atomics and metavariables

logics.instances.propositional.languages.classical_language_with_sent_constants,
logics.instances.propositional.languages.classical_infinite_language_with_sent_constants¶: Same as the two above, adding the sentential constants ⊥, ⊤

logics.instances.propositional.languages.classical_infinite_language_noconditional¶: Same as the second, with constants ~, ∧, ∨.

logics.instances.propositional.languages.classical_infinite_language_nobiconditional¶
logics.instances.propositional.languages.classical_infinite_language_with_sent_constants_nobiconditional¶: Same as the second and fourth, with constants ~, ∧, ∨, →.

logics.instances.propositional.languages.classical_infinite_language_only_negation_conditional¶: Same as the second, with constants ~, →.

logics.instances.propositional.languages.modal_language¶: Same as classical_language but adds the unary constants □ and ◇

logics.instances.propositional.languages.modal_infinite_language¶: Same as the one immediately above, with an indefinite supply of atomics and metavariables

logics.instances.propositional.languages.modal_infinite_language_with_sent_constants¶: Same as the one immediately above, adding the sentential constants ⊥, ⊤

logics.instances.propositional.languages.LFI_language¶: Same as classical_infinite_language_with_sent_constants, adding the unary constants • and ◦, with •A intended to mean “A is inconsistent”, and ◦A “A is consistent”.