class logics.classes.propositional.Inference(premises, conclusions, level=None)

Class for propositional inferences and metainferences.

  • premises (list of Formula or list of Inference) – The premises of the inference, may be formulae, inferences or the empty list

  • conclusions (list of Formula or list of Inference) – The conclusions of the inference, may be formulae, inferences or the empty list

  • level (int, optional) – The level of the inference. Will be detected automatically if you leave it with the default value of None. Useful for building empty metainferences (of level >1)


IncorrectLevels – if the declared level of the inference does not coincide with the calculated level


Regular inferences:

>>> from logics.classes.propositional import Formula, Inference
>>> Inference([Formula(['p'])], [Formula(['q'])])  # the inference p / q
>>> Inference([Formula(['p']), Formula(['→', ['p'], ['q']])], [Formula(['q'])])  # modus ponens, p, p → q / q

Metainferences (e.g. meta-reflexivity, i.e. p / p // p / p, and an empty metainference):

>>> i1 = Inference([Inference([Formula(['p'])], [Formula(['p'])])],
...                [Inference([Formula(['p'])], [Formula(['p'])])])
>>> i1.level
>>> i2 = Inference([], [])
>>> i2.level
>>> i3 = Inference([], [], level=2)
>>> i3.level

An incorrectly declared level:

>>> Inference([Formula(['p'])], [Formula(['q'])], level=2)
Traceback (most recent call last):
logics.classes.exceptions.IncorrectLevels: Inference ([['p']] / [['q']]) has a premise of level 0 which conflicts with the declared level 2


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

property conclusion

Single conclusion of an Inference.

For single conclusion arguments, you can use inference.conclusion instead of inference.conclusions[0] If there are either more or less than one conclusions, will raise ValueError

property level

Level of a (meta)inference

0 is formula, 1 is regular inference, 2 is metainference, 3 metametainference, etc. See above for some examples.

property is_metainference

True if the level > 1, False otherwise

atomics_inside(language, prev_at=None)

Returns the set of the atomic letter strings (both propositional letters and metavariables) inside an inference.

Similar to the atomics_inside method of Formula


>>> from logics.classes.propositional import Formula, Inference
>>> from logics.instances.propositional.languages import classical_language
>>> Inference([Formula(['~', ['p']])], [Formula(['q'])]).atomics_inside(classical_language)
{'p', 'q'}
property subformulae

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


>>> from logics.classes.propositional import Formula, Inference
>>> Inference([Formula(['p'])], [Formula(['p'])]).subformulae

True if at least one Formula inside the Inference is schematic (contains a schematic Formula), False otherwise

substitute(sf_or_inf_to_substitute, sf_or_inf_with)

Substitutes either a formula or an inference for another inside an inference

The substituted formula or inference must match exactly. Does not modify the original inference. Similar to the substitute method of Formula



Substitute a formula for another:

>>> from logics.classes.propositional import Formula, Inference
>>> i1 = Inference([Formula(['p'])], [Formula(['q'])])
>>> i1.substitute(Formula(['q']), Formula(['~', ['q']]))
([['p']] / [['~', ['q']]])
>>> i1
([['p']] / [['q']])

Substitute an inference for another:

>>> i1 = Inference([Formula(['p'])], [Formula(['q'])])
>>> i1.substitute(Inference([Formula(['p'])], [Formula(['q'])]),
...               Inference([Formula(['q'])], [Formula(['p'])]))
([['q']] / [['p']])
>>> i2 = Inference([Inference([Formula(['p'])], [Formula(['q'])])],
...                [Inference([Formula(['q'])], [Formula(['p'])])])
>>> i2
([([['p']] / [['q']])] // [([['q']] / [['p']])])
>>> i2.substitute(Inference([Formula(['p'])], [Formula(['q'])]),
...               Inference([Formula(['~', ['p']])], [Formula(['~', ['q']])]))
([([['~', ['p']]] / [['~', ['q']]])] // [([['q']] / [['p']])])
is_instance_of(inference, language, subst_dict=None, return_subst_dict=False, order=False)

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

Since (until now at least) logics does not have metavariables for inferences, all it will do is check if all the premises are instances and all the conclusions are instances (recursively so if this is a metainference). For two non-schematic inferences, one is considered an instance of another iff they are equal. Similar to the is_instance_of method of Formula. The optional parameters subst_dict and return_subst_dict are as in that method.

Contains an additional parameter order. If True, the premises and conclusions of both have to be in the same order. e.g. p, q ∧ r / p will be an instance of p, A / p but not of A, p / p. If False, both are instances.



>>> from logics.classes.propositional import Formula, Inference
>>> from logics.instances.propositional.languages import classical_language
>>> i1 = Inference([Formula(['p'])], [Formula(['p'])])
>>> i2 = Inference([Formula(['A'])], [Formula(['A'])])
>>> i1.is_instance_of(i2, classical_language)
>>> i3 = Inference([Formula(['p'])], [Formula(['q'])])
>>> i3.is_instance_of(i2, classical_language)

The subst_dict and return_subst_dict parameters:

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

All the above works with any level of metainferences as well:

>>> i4 = Inference([Inference([Formula(['p'])], [Formula(['q'])])],
...                [Inference([Formula(['q'])], [Formula(['p'])])])
>>> i4
([([['p']] / [['q']])] // [([['q']] / [['p']])])
>>> i5 = Inference([Inference([Formula(['A'])], [Formula(['B'])])],
...                [Inference([Formula(['B'])], [Formula(['A'])])])
>>> i5
([([['A']] / [['B']])] // [([['B']] / [['A']])])
>>> i4.is_instance_of(i5, classical_language)
>>> i4.is_instance_of(i5, classical_language, return_subst_dict=True)
(True, {'A': ['p'], 'B': ['q']})

The order parameter:

>>> i6 = Inference([Formula(['p']), Formula(['→', ['p'], ['q']])], [Formula(['q'])])
>>> i7 = Inference([Formula(['→', ['A'], ['B']]), Formula(['A'])], [Formula(['B'])])
>>> i6.is_instance_of(i7, classical_language)  # order is False by default
>>> i6.is_instance_of(i7, classical_language, order=True)

Returns the associated conditional for an Inference

Given a level-1 Inference of the form A, B, C / D, E, F returns a Formula of the form ((A ∧ B) ∧ C) → ((D ∨ E) ∨ F)

For a metainference (A, B / C) // (D / E, F) will return the Formula ((A ∧ B) → C) → (D → (E ∨ F))


>>> from logics.utils.parsers import classical_parser
>>> inf = classical_parser.parse("p1, p2, p3 / q1, q2, q3")
>>> assoc_cond = inf.associated_conditional()
>>> classical_parser.unparse(assoc_cond)
'((p1 ∧ p2) ∧ p3) → ((q1 ∨ q2) ∨ q3)'
>>> metainf = classical_parser.parse("(p1, p2 / q1) // (r1 / s1, s2)")
>>> assoc_cond2 = metainf.associated_conditional()
>>> classical_parser.unparse(assoc_cond2)
'((p1 ∧ p2) → q1) → (r1 → (s1 ∨ s2))'


  • An inference with empty premises and conclusions will return the formula ⊥

  • An inference with empty premises and non-empty conclusions, e.g. / A, B, will return the formula A ∨ B

  • An inference with empty conclusions and non-empty premises, e.g. A, B /, will return the formula ~(A ∧ B)

  • The above clauses also work recursively (e.g. (/ A, B) // returns ~(A ∨ B); while (/) // (/) returns ⊥ → ⊥)

  • Beware because the translation may not preserve (in)validity in some systems. E.g. valid inferences of K3 will be turned into non-tautological formulae for that system (because it has no tautologies). The same may happen with ST metainferences (e.g. Cut) and its inferences