# Formula¶

class `logics.classes.propositional.``Formula`(*args, **kwargs)

Class for representing propositional formulae.

The class Formula extends list. Every subformula within a Formula must also be a Formula.

• Atomic formulae contain a single string element, e.g. `Formula(['p'])`; `Formula(['A'])`; `Formula(['⊥'])`

• Molecular formulae are always written in prefix notation, e.g. `Formula(['∧', ['p'], ['~', ['q']]])`, which is read as p ∧ ~q

Note that the __init__ method of Formula will automatically turn lists within a Formula into Formula. Thus, you can write `Formula(['~', ['p']])` instead of `Formula(['~', Formula(['p'])])`

Examples

```>>> from logics.classes.propositional import Formula
>>> f = Formula(['~', ['p']])
>>> f
['p']
>>> type(f)
<class 'logics.classes.propositional.formula.Formula'>
```

Notes

Working with Formula elements directly is somewhat uncomfortable and cumbersome. You may instead want to take a look at Parsers. For random generation of formulae, see Random Formula Generators

property `is_atomic`

Returns `True` if the formula is atomic.

Will consider a formula as an atomic if it is of length 1 (so as to not have to pass a Language as parameter).

Examples

```>>> from logics.classes.propositional import Formula
>>> Formula(['p']).is_atomic
True
>>> Formula(['~', ['p']]).is_atomic
False
```
`arguments`(quantifiers=None)

Returns a list of the arguments of a molecular formula, `[]` if it is an atomic.

Examples

```>>> from logics.classes.propositional import Formula
>>> Formula(['p']).arguments()
[]
>>> Formula(['∧', ['p'], ['~', ['A']]]).arguments()
[['p'], ['~', ['A']]]
```

Notes

quantifiers parameter is necessary because of how PredicateFormula works. Leave it as `None` here.

`is_schematic`(language)

Returns `True` if the formula contains a metavariable of the language, `False` otherwise

Examples

```>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['p']).is_schematic(classical_language)
False
>>> Formula(['A']).is_schematic(classical_language)
True
>>> Formula(['∧', ['p'], ['~', ['A']]]).is_schematic(classical_language)
True
```
property `main_symbol`

Returns the first element if the formula is molecular, `None` if it is an atomic.

Examples

```>>> from logics.classes.propositional import Formula
>>> Formula(['p']).main_symbol is None
True
>>> Formula(['∧', ['p'], ['~', ['A']]]).main_symbol
'∧'
```
property `depth`

Depth of the formula.

Examples

```>>> from logics.classes.propositional import Formula
>>> Formula(['p']).depth
0
>>> Formula(['∧', ['p'], ['~', ['A']]]).depth
2
```
`is_well_formed`(language)

Shortcut for `language.is_well_formed(formula)`

property `subformulae`

Returns a list of the subformulae of the formula, without repetitions.

Examples

```>>> from logics.classes.propositional import Formula
>>> Formula(['p']).subformulae
[['p']]
>>> Formula(['∧', ['p'], ['~', ['A']]]).subformulae
[['p'], ['A'], ['~', ['A']], ['∧', ['p'], ['~', ['A']]]]
>>> Formula(["∧", ["p"], ["p"]]).subformulae  # p will only appear once
[['p'], ['∧', ['p'], ['p']]]
```
`atomics_inside`(language, prev_at=None)

Returns the set of the atomic letter strings (both propositional letters and metavariables) inside a formula. Sentential constants do not count.

Examples

```>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['∧', ['p'], ['~', ['A']]]).atomics_inside(classical_language)
{'A', 'p'}
```
`substitute`(sf_to_substitute, sf_with)

Substitutes a subformula for another subformula.

Will return a different `Formula` object, and not modify the original.

The substituted one must match exactly, for example, calling `Formula(['∧', ['p'], ['B']]).substitute` with arguments `sf_to_substitute=Formula(['∧', ['A'], ['B']])` and `sf_with=Formula(['∧', ['B'], ['B']]` will do nothing. See below for a different method that will do something with that. This method is also different from the `PredicateFormula` free variable substitution method.

Parameters
Returns

A different formula instance from the original

Return type

logics.classes.propositional.Formula

Examples

```>>> from logics.classes.propositional import Formula
>>> f = Formula(['∧', ['p'], ['~', ['A']]])
>>> f.substitute(Formula(['~', ['A']]), Formula(['~', ['p']]))
['∧', ['p'], ['~', ['p']]]
>>> f
['∧', ['p'], ['~', ['A']]]
```
`instantiate`(language, subst_dict)

Given a schematic Formula, a language and a substitution dict, returns the schema instantiated with the dict.

Will return a different Formula object, and not modify the original.

Parameters
Returns

A different formula instance from the original

Return type

logics.classes.propositional.Formula

Raises

ValueError – if some schematic propositional within the formula has no substitution assigned in the dictionary

Examples

```>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> f = Formula(['∧', ['A'], ['B']])
>>> f.instantiate(classical_language, {'A': Formula(['B']),
...                                    'B': Formula(['∧', ['~', ['B']], ['C']])})
['∧', ['B'], ['∧', ['~', ['B']], ['C']]]
>>> f
['∧', ['A'], ['B']]
>>> Formula(['∧', ['A'], ['B']]).instantiate(classical_language, {'A': Formula(['p'])})
Traceback (most recent call last):
...
ValueError: Metavariable B not present in substitution dict given
```
`schematic_substitute`(language, schema_to_substitute, schema_with)

Takes a Formula and two schematic Formula, and substitutes any subformula instance of the first schema for the corresponding instance of the second schema.

Will return a different Formula object, and not modify the original.

Parameters
Returns

A different formula instance from the original

Return type

logics.classes.propositional.Formula

Examples

```>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> f = Formula(['→', ['p'], ['→', ['p'], ['q']]])
>>> f.schematic_substitute(classical_language, Formula(['→', ['A'], ['B']]),
...                                            Formula(['∨', ['~', ['A']], ['B']]))
['∨', ['~', ['p']], ['∨', ['~', ['p']], ['q']]]
>>> f
['→', ['p'], ['→', ['p'], ['q']]]
```
`is_instance_of`(formula, language, subst_dict=None, return_subst_dict=False, order=None)

Determines if a Formula is an instance of another (tipically schematic) Formula.

For two non-schematic formulae, one is considered an instance of another iff they are equal.

Has two optional parameters:

• return_subst_dict: defaults to `False`. If True, will return the substitution dict for formula’s metavariables. See below for an example.

• subst_dict: defaults to `None`. Can be given a substitution dict if some metavariable(s) are to be interpreted in some specific way.

These parameters are useful in other modules, e.g. for checking correct instantiation of rules, where you tipically first check the conclusion, return a susbstitution dict, and use that substitution dict to check the premises of the rule. See below for some examples.

Parameters
• formula (logics.classes.propositional.Formula) – The (schematic) Formula of which we want to know if it is instance

• language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage

• subst_dict (dict, optional) – A susbstitution dict of the form `{'A': someformula, 'B': someformula}`

• return_subst_dict (bool, optional) – If True will additionally return a substitution dict.

• order (NoneType, optional) – Is for the is_instance_of method of Inference. Does nothing here, you should not alter it.

Examples

```>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['~', ['p']]).is_instance_of(Formula(['A']), classical_language)
True
>>> Formula(['~', ['p']]).is_instance_of(Formula(['∨', ['A'], ['B']]), classical_language)
False
>>> Formula(['∨', ['~', ['p']], ['q']]).is_instance_of(Formula(['∨', ['A'], ['B']]),
...                                                    classical_language)
True
```

If we give it some substitution dict beforehand:

```>>> Formula(['p']).is_instance_of(Formula(['A']), classical_language,
...                               subst_dict={'A': Formula(['q'])})
False
>>> Formula(['p']).is_instance_of(Formula(['A']), classical_language,
...                               subst_dict={'A': Formula(['p'])})
True
```

If we ask it to return the substitution dict:

```>>> Formula(['∨', ['~', ['p']], ['q']]).is_instance_of(Formula(['∨', ['A'], ['B']]),
...                                                    classical_language,
...                                                    return_subst_dict=True)
(True, {'A': ['~', ['p']], 'B': ['q']})
```