Inference¶

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

Class for propositional inferences and metainferences.

Parameters:

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)

Raises:

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

Examples

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
2
>>> i2 = Inference([], [])
>>> i2.level
1
>>> i3 = Inference([], [], level=2)
>>> i3.level
2

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

Notes

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

Examples

>>> 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.

Examples

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

is_schematic(language)¶: 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

Parameters:

sf_or_inf_to_substitute (Formula or Inference) –
sf_or_inf_with (Formula or Inference) –

Examples

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.

Parameters:

inference (logics.classes.propositional.Inference) – The (schematic) Inference 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 (bool) – If True will respect the order of the premises and conclusions in inference, if False will not.

Examples

>>> 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)
True
>>> i3 = Inference([Formula(['p'])], [Formula(['q'])])
>>> i3.is_instance_of(i2, classical_language)
False

The subst_dict and return_subst_dict parameters:

>>> i1.is_instance_of(i2, classical_language, subst_dict={'A': Formula(['q'])})
False
>>> 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)
True
>>> 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
True
>>> i6.is_instance_of(i7, classical_language, order=True)
False

associated_conditional()¶

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))

Examples

>>> 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))'

Notes

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