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