Many-Valued Semantics¶
Mixed Many-Valued Semantics¶
-
class
logics.classes.propositional.semantics.
MixedManyValuedSemantics
(language, truth_values, premise_designated_values, conclusion_designated_values, truth_function_dict, sentential_constant_values_dict, use_molecular_valuation_fast_version=False, name='MixedManyValuedSemantics object')¶ Class for many-valued semantics, which may contain different standards for premises and conclusions (e.g. ST, TS)
- Parameters
language (language: logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
truth_values (list) – A list of the truth values (which may be int, str, etc.). In the instances below I use strings.
premise_designated_values (list) – Must be a sublist of truth_values, representing the premise standard
conclusion_designated_values (list) – Must be a sublist of truth_values, representing the conclusion standard
truth_function_dict (dict) – Dict containing the logical constants (str) as keys, and n-dimensional lists as values (for constants of arity n). Will also accept any indexable (things with a __getitem__ method, e.g. numpy arrays) and any n-ary callable .
sentential_constant_values_dict (dict) – Dict containing the sentential constans (str) as keys, and their truth values (members of truth_values) as values
use_molecular_valuation_fast_version (bool, optional) – Implements a faster version of the molecular valuation function (e.g. if asked for a disjunction will return ‘1’ with one true disjunct, without evaluating the other). In counterpart, it is less general, since it assumes the Kleene truth matrices. Defaults to
False
.name (str) – Name of the system (only for prettier printing to the console)
Notes
The order of truth_values is the order in which the rows and columns will be read in the truth functions. For instance, if truth_values is
['0', 'i', '1']
, the truth function:{ # (...) '$': [[v1, v2, v3], [v4, v5, v6], [v7, v8, v9]], # (...) }
for a constant $ will be intepreted as saying that
$(‘0’, ‘0’) = v1
$(‘i’, ‘1’) = v6
$(‘1’, ‘1’) = v9
etc.
However, if truth_values is entered as
['1', 'i', '0']
, then$(‘0’, ‘0’) = v9
$(‘i’, ‘1’) = v4
$(‘1’, ‘1’) = v1
etc.
- Raises
ValueError – If the premise or conclusion designated values are not a sublist of the truth values, some logical constant of the language does not receive a truth function (or receives something that is neither a callable nor an indexible), or some sentential constant does not receive a truth value (or gets a truth value not present in truth_values)
Examples
Definition of classical logic CL
>>> from logics.instances.propositional.languages import classical_infinite_language_with_sent_constants >>> from logics.classes.propositional.semantics import MixedManyValuedSemantics >>> bivalued_truth_values = ['1', '0'] # The order is important for the lines below >>> classical_truth_functions = { ... '~': ['0', '1'], ... '∧': [ #1 #0 ... ['1', '0'], # 1 ... ['0', '0']], # 0 ... '∨': [ #1 #0 ... ['1', '1'], # 1 ... ['1', '0']], # 0 ... '→': [ #1 #0 ... ['1', '0'], # 1 ... ['1', '1']], # 0 ... '↔': [ #1 #0 ... ['1', '0'], # 1 ... ['0', '1']], # 0 ... } >>> CL = MixedManyValuedSemantics(language=classical_infinite_language_with_sent_constants, ... truth_values=bivalued_truth_values, ... premise_designated_values=['1'], ... conclusion_designated_values=['1'], ... truth_function_dict=classical_truth_functions, ... sentential_constant_values_dict= {'⊥': '0', '⊤': '1'}, ... name='CL')
Example of a non-classical 3-valued system: the many-valued system ST
>>> from logics.instances.propositional.languages import classical_infinite_language_with_sent_constants >>> from logics.classes.propositional.semantics import MixedManyValuedSemantics >>> trivalued_truth_values = ['1', 'i', '0'] # The order is important for the lines below >>> trivalued_truth_functions = { ... '~': ['0', 'i', '1'], ... '∧': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['i', 'i', '0'], # i ... ['0', '0', '0']], # 0 ... '∨': [ #1 #i #0 ... ['1', '1', '1'], # 1 ... ['1', 'i', 'i'], # i ... ['1', 'i', '0']], # 0 ... '→': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['1', 'i', 'i'], # i ... ['1', '1', '1']], # 0 ... '↔': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['i', 'i', 'i'], # i ... ['0', 'i', '1']], # 0 ... } >>> ST = MixedManyValuedSemantics(language=classical_infinite_language_with_sent_constants, ... truth_values=trivalued_truth_values, ... premise_designated_values=['1'], ... conclusion_designated_values=['1', 'i'], ... truth_function_dict=trivalued_truth_functions, ... sentential_constant_values_dict={'⊥': '0', '⊤': '1'}, ... name='ST')
Note that since both CL and ST use the Kleene truth matrices (represented above) we could also have specified
use_molecular_valuation_fast_version=True
(would have been faster than what we did). Also note that, as stated above, the values of the trivalued_truth_functions could also be callables. For example:>>> def trivalued_disjunction(val1, val2): ... if val1 == '1' or val2 == '1': ... return '1' ... elif val1 == 'i' or val2 == 'i': ... return 'i' ... return '0' >>> trivalued_truth_functions = { ... '~': ['0', 'i', '1'], ... '∧': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['i', 'i', '0'], # i ... ['0', '0', '0']], # 0 ... '∨': trivalued_disjunction ... # (...) ... }
Note that both classical logic and ST are already defined as instances in the instances modules, so there is no need to redefine them if you need them. You can just import them via:
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL, ST_mvl_semantics as ST
-
apply_truth_function
(constant, *args)¶ Gets the value of a truth function applied to a given set of arguments.
Works independently of whether the truth function for the constant is a callable or an indexible.
Examples
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL, ST_mvl_semantics as ST >>> CL.apply_truth_function('~', '0') '1' >>> CL.apply_truth_function('~', '1') '0' >>> CL.apply_truth_function('∨', '0', '1') '1' >>> ST.apply_truth_function('∨', 'i', '0') 'i'
-
valuation
(formula, atomic_valuation_dict=None)¶ Returns the valuation of a formula, given some valuations for the atomics.
- Parameters
formula (logics.classes.propositional.Formula) – The formula of which you want to know the valuation
atomic_valuation_dict (dict, optional) – A dict containing the valuations for the atomics within the formula. The keys must be strings (the atomic letters) and values are in truth_values
- Raises
KeyError – If some atomic present in formula does not get a valuation in atomic_valuation_dict
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL, ST_mvl_semantics as ST >>> CL.valuation(classical_parser.parse('p'), {'p': '1'}) '1' >>> CL.valuation(classical_parser.parse('p then q'), {'p': '1'}) Traceback (most recent call last): ... KeyError: 'Valuation for atomic q was not given in the atomic dict >>> CL.valuation(classical_parser.parse('p then q'), {'p': '1', 'q': '0'}) '0' >>> ST.valuation(classical_parser.parse('p then q'), {'p': '1', 'q': 'i'}) 'i' >>> CL.valuation(classical_parser.parse('Bottom')) # No atomic dict here '0'
-
truth_table
(formula_or_inference)¶ Returns a representation of a truth table for a formula.
Takes an instance of Formula or Inference as input, and returns 2-list where the first member is a list of subformulae (ordered by depth) and the second member is a 2-dimensional list with the valuations of those subformulae (in that order)
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.truth_table(classical_parser.parse('p')) [[['p']], [['1'], ['0']]] >>> subformulae, table = CL.truth_table(classical_parser.parse('p then q')) >>> subformulae [['p'], ['q'], ['→', ['p'], ['q']]] >>> for row in table: ... print(row) ['1', '1', '1'] ['0', '1', '1'] ['1', '0', '0'] ['0', '0', '1']
In each row above, the three values correspond to the values of p, q, and p → q respectively. Examples for inferences / metainferences:
>>> subformulae, table = CL.truth_table(classical_parser.parse('p / p')) [['p']] >>> for row in table: ... print(row) ['1'] ['0'] >>> subformulae, table = CL.truth_table(classical_parser.parse('(q / p) // (p / ~q)')) >>> subformulae [['q'], ['p'], ['~', ['q']]] >>> for row in table: ... print(row) ['1', '1', '0'] ['0', '1', '1'] ['1', '0', '0'] ['0', '0', '1']
-
satisfies
(formula_or_inference, atomic_valuation_dict=None, evaluate_premise=False)¶ Returns True if the valuation satisfies the inference / formula, False otherwise.
For formulae, being satisfied by a valuation according to a standard (i.e. a subset of truth values) means that the valuation belongs to that standard. By default formulae are evaluated using the conclusion standard of the logic.
For (meta)inferences, satisfaction is defined recursively: Γ / Δ is satisfied according to valuation v iff (if every premise is satisfied according to v then some conclusion is satisfied according to v). More intuitively, what this means is that a valuation satisfies an inference when it is not a counterexample to it (i.e. all premises in the premise standard but no conclusion in the conclusion standard)
- Parameters
formula_or_inference (logics.classes.propositional.Formula or logics.classes.propositional.Inference) – The formula or inference to evaluate for satisfaction. The inference may be of level > 1
atomic_valuation_dict (dict, optional) – A dict containing the valuations for the atomics within the formula. The keys must be strings (the atomic letters) and values are in truth_values
evaluate_premise (bool) – Formulae are evaluated by default with the conclusion standard. If evaluate_premise is True they will be evaluated with the premise standard. If you pass an inference, the correct standard will automatically be used, and you should leave the value by default
- Returns
True if the valuation satisfies the formula / inference, False otherwise
- Return type
bool
- Raises
KeyError – If some atomic present in formula does not get a valuation in atomic_valuation_dict
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL, ST_mvl_semantics as ST >>> CL.satisfies(classical_parser.parse('p'), {'p': '1'}) True >>> ST.satisfies(classical_parser.parse('p'), {'p': 'i'}) True >>> ST.satisfies(classical_parser.parse('p'), {'p': 'i'}, evaluate_premise=True) False >>> CL.satisfies(classical_parser.parse('p then q, q / p'), {'p': '1', 'q': '1'}) True >>> CL.satisfies(classical_parser.parse('p then q, q / p'), {'p': '0', 'q': '1'}) False >>> CL.satisfies(classical_parser.parse('(A / B), (B / C) // (A / C)'), ... {'A': '1', 'B': '1', 'C': '0'}) True >>> ST.satisfies(classical_parser.parse('(A / B), (B / C) // (A / C)'), ... {'A': '1', 'B': 'i', 'C': '0'}) False
-
is_locally_valid
(formula_or_inference)¶ Determines if a formula or inference is locally valid
Local validity means the following:
A formula or inference is locally valid iff it is satisfied by every valuation
For formulae, since they are evaluated by default with the conclusion standard, this is equivalent to claiming that the formula is a tautology.
For regular inferences this is the standard notion of validity for mixed logics. Since the premises and conclusions are formulae, applying the definition of satisfaction (see above) yields the following: for every valuation v, if the valuation of the premises belong to the premise standard, the valuation of some conclusion belongs to the conclusion standard
For metainferences things get more interesting. Metainferential local validity is not just “if the premises are valid, then the conclusion is valid” (that is the global notion of metainferential validity, see below). Rather, it means no valuation satisfies all the premises and none of the conclusions. So, for example, in CL, the metainference (p / q) // (r / s) is globally valid (since the premise is not valid), but locally invalid (there is a valuation that satisfies the premise but not the conclusion of the metainference, namely p=1, q=1, r=1, s=0)
- Parameters
formula_or_inference (logics.classes.propositional.Formula or logics.classes.propositional.Inference) – The formula or inference to evaluate for local validity. Inferences may be of level > 1
- Returns
True if the formula / inference is locally valid, False otherwise
- Return type
bool
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL, ST_mvl_semantics as ST >>> CL.is_locally_valid(classical_parser.parse('p or not p')) True >>> CL.is_locally_valid(classical_parser.parse('p, p then q / q')) True >>> CL.is_locally_valid(classical_parser.parse('q, p then q / p')) False >>> CL.is_locally_valid(classical_parser.parse('(p / q) // (r / s)')) False >>> CL.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) True >>> ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) False
-
is_locally_antivalid
(formula_or_inference)¶ Determines if a formula or inference is locally antivalid
Local antivalidity means the following:
A formula or inference is locally antivalid iff no valuation satisfies it
Since formulae are evaluated by default with the conclusion standard, this is equivalent to claiming that the formula is a contradiction
A (meta)inference Γ / Δ will be antivalid iff every valuation satisfies all the premises an none of the conclusions. One may think of it as an inferential equivalent of the notion of contradiction for formulae. Note that anti-vality is a stronger notion than invalidity.
The parameters and return value are similar to the method above.
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.is_locally_antivalid(classical_parser.parse('q, p then q / p')) False >>> CL.is_locally_antivalid(classical_parser.parse('p or not p / p and not p')) True
-
is_contingent
(formula_or_inference)¶ Returns True if the Formula / Inference is neither locally valid nor antivalid, False otherwise
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.is_contingent(classical_parser.parse('p')) True >>> CL.is_contingent(classical_parser.parse('p, p then q / q')) False >>> CL.is_contingent(classical_parser.parse('p or not p / p and not p')) False >>> CL.is_contingent(classical_parser.parse('q, p then q / p')) True
-
is_valid
(inference)¶ Shortcut for
is_locally_valid(inference)
-
is_antivalid
(inference)¶ Shortcut for
is_locally_antivalid(inference)
-
is_tautology
(formula)¶ Shortcut for
is_locally_valid(formula)
-
is_contradiction
(formula)¶ Shortcut for
is_locally_antivalid(formula)
-
is_globally_valid
(inference)¶ Determines if an inference is globally valid.
Global validity means:
A metainference Γ / Δ is globally valid iff (if every premise in Γ is valid, then some conclusion in Δ is valid). Note that the is valid expressions in the right conditional may be interpreted locally or globally.
This method does the following (which I think is the standard way of reading global validity):
For formulae and level 1 inferences, the is valid on the right is read locally
For metainferences (level > 1), it is read globally
Notes
Evaluating global validity of schematic metainferences can lead to (conceptual) problems, and should be avoided. For instance (A / B) // (C / D) will come out as globally valid in CL, but it may have invalid instances, e.g. (p → p / p → p) // (p → p / p ∧ ~p)
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.is_globally_valid(classical_parser.parse('(p / q) // (r / s)')) True >>> CL.is_globally_valid(classical_parser.parse('((p / p) // (p / p)) /// ((p / q) // (r / s))')) True
-
is_globally_valid2
(inference)¶ Determines if an inference is globally valid (in a second, different sense).
Same as the method above, but for inferences of level 2 and above evaluates the conditional:
If all the premises are locally valid then the conclusion is locally valid
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.is_globally_valid2(classical_parser.parse('(p / q) // (r / s)')) True >>> CL.is_globally_valid2(classical_parser.parse('((p / p) // (p / p)) /// ((p / q) // (r / s))')) False
-
is_globally_valid3
(inference)¶ Determines if an inference is globally valid (in a third, different sense).
Same as the two above but does global validity all the way down, i.e. a level 1 inference is globally valid iff if the premises globally valid (i.e. are tautologies), some conclusion is globally valid (is a tautology)
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> CL.is_globally_valid3(classical_parser.parse('(p / q)')) True >>> CL.is_globally_valid3(classical_parser.parse('(p / q) // (r / s)')) True
Instances¶
The following are predefined instances of MixedManyValuedSemantics.
-
logics.instances.propositional.many_valued_semantics.
classical_mvl_semantics
¶ Classical logic semantics (truth values are
['1', '0']
and both premise and conclusion standards are['1']
)
-
logics.instances.propositional.many_valued_semantics.
K3_mvl_semantics
¶
-
logics.instances.propositional.many_valued_semantics.
LP_mvl_semantics
¶
-
logics.instances.propositional.many_valued_semantics.
ST_mvl_semantics
¶
-
logics.instances.propositional.many_valued_semantics.
TS_mvl_semantics
¶ The above four systems share the truth values
['1', 'i', '0']
. If S denotes the standard['1']
and T denotes de standard['1', 'i']
Then K3 is the mixed system S/S, LP is the mixed system T/T, ST is the mixed system S/T and T/S is the mixed system T/S
Mixed Metainferential Semantics¶
-
class
logics.classes.propositional.semantics.
MixedMetainferentialSemantics
(*args, **kwargs)¶ Class for mixed metainferential logics, where the premises and conclusions standards are themselves mixed.
This class extends list, so you should just pass a 2-list with the mixed standards you want to combine. The given logics should have the same language and truth values, otherwise things may fail.
- Raises
ValueError – If you pass less or more than two arguments
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.classes.propositional.semantics import MixedMetainferentialSemantics >>> from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST, TS_mvl_semantics as TS >>> # TS invalidates identity (and every other inference) but validates meta-identity >>> TS.is_locally_valid(classical_parser.parse('p / p')) False >>> TS.is_locally_valid(classical_parser.parse('(p / p) // (p / p)')) True >>> # ST invalidates Cut >>> ST.is_locally_valid(classical_parser.parse('(A / B), (C / D) // (A / C)')) False >>> # ST/TS and TS/ST go empty and classical one level more >>> STTS = MixedMetainferentialSemantics([ST, TS]) >>> STTS.is_locally_valid(classical_parser.parse('(p / p) // (p / p)')) False >>> TSST = MixedMetainferentialSemantics([TS, ST]) >>> TSST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) True
Each of the two arguments of MixedMetainferentialSemantics may be 2-lists, and the __init__ method will automatically turn them into MixedMetainferentialSemantics. For example:
>>> STTS_TSST = MixedMetainferentialSemantics([[ST, TS], [TS, ST]]) >>> type(STTS_TSST[0]) <class 'logics.classes.propositional.semantics.many_valued.MixedMetainferentialSemantics'>
Instances¶
-
logics.instances.propositional.many_valued_semantics.
classical_logic_up_to_level
(n)¶ Returns a mixed metainferential system that will validate every classically valid inference and metainference up to level n. Will fail to do that for levels above.
The recursive definition of this function is as follows:
if n == 1: return ST_mvl_semantics else: return MixedMetainferentialSemantics([empty_logic_up_to_level(n-1), classical_logic_up_to_level(n-1)])
By looking at the function below, we see that, for example,
classical_logic_up_to_level(2)
the same asMixedMetainferentialSemantics([TS, ST])
, andclassical_logic_up_to_level(3)
- Parameters
n (int) – The level up to which all classical inferences and metainferences will be validated.
- Returns
Classical logic up to level n
- Return type
logics.classes.propositional.semantics.MixedMetainferentialSemantics
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import classical_logic_up_to_level >>> ST = classical_logic_up_to_level(1) >>> ST.is_locally_valid(classical_parser.parse('(A then B), (B then C) / (A then C)')) True >>> ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) False >>> TSST = classical_logic_up_to_level(2) >>> TSST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) True
In fact, we can check that:
>>> from logics.classes.propositional.semantics import MixedManyValuedSemantics >>> from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST, TS_mvl_semantics as TS >>> classical_logic_up_to_level(2) == MixedMetainferentialSemantics([TS, ST]) True >>> classical_logic_up_to_level(3) == MixedMetainferentialSemantics([[ST, TS], [TS, ST]]) True
-
logics.instances.propositional.many_valued_semantics.
empty_logic_up_to_level
(n)¶ Returns a mixed metainferential system that will validate every classically valid inference and metainference up to level n. Will fail to do that for levels above.
The recursive definition of this function is as follows:
if n == 1: return TS_mvl_semantics else: return MixedMetainferentialSemantics([classical_logic_up_to_level(n-1), empty_logic_up_to_level(n-1)])
By looking at the function above, we see that, for example,
empty_logic_up_to_level(2)
is[ST, TS]
- Parameters
n (int) – The level up to which all classical inferences and metainferences will be validated.
- Returns
The empty logic up to level n
- Return type
logics.classes.propositional.semantics.MixedMetainferentialSemantics
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import empty_logic_up_to_level >>> TS = empty_logic_up_to_level(1) >>> TS.is_locally_valid(classical_parser.parse('p / p')) False >>> TS.is_locally_valid(classical_parser.parse('(p / p) // (p / p)')) True >>> STTS = empty_logic_up_to_level(2) >>> STTS.is_locally_valid(classical_parser.parse('(p / p) // (p / p)')) False
Again, we can check that:
>>> from logics.classes.propositional.semantics import MixedManyValuedSemantics >>> from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST, TS_mvl_semantics as TS >>> empty_logic_up_to_level(2) == MixedMetainferentialSemantics([ST, TS]) True >>> empty_logic_up_to_level(3) == MixedMetainferentialSemantics([[TS, ST], [ST, TS]]) True
Union and Intersection Logics¶
-
class
logics.classes.propositional.semantics.
IntersectionLogic
(*args, **kwargs)¶ A list of logics intersected.
An inference will be valid (satisfied) iff valid (satisfied) in all of them
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST, TS_mvl_semantics as TS >>> I_TS_ST = IntersectionLogic([TS, ST]) >>> I_TS_ST.is_valid(classical_parser.parse('p / p')) # Valid in ST, invalid in TS False >>> I_TS_ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) # Valid in TS, invalid in ST False
It is also possible to put more than two systems in intersection, for example:
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> I_TS_ST_CL = IntersectionLogic([TS, ST, CL])
In this case, this system will be equal to I_TS_ST, since CL is stronger inferentially and metainferentially than both ST and TS.
-
class
logics.classes.propositional.semantics.
UnionLogic
(*args, **kwargs)¶ A list of logics put in union.
An inference will be valid (satisfied) iff valid (satisfied) in at leas one of them
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST, TS_mvl_semantics as TS >>> U_TS_ST = UnionLogic([TS, ST]) >>> U_TS_ST.is_valid(classical_parser.parse('p / p')) # Valid in ST, invalid in TS True >>> U_TS_ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) # Valid in TS, invalid in ST True
It is also possible to put more than two systems in intersection, for example:
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics as CL >>> U_TS_ST_CL = UnionLogic([TS, ST, CL])
In this case, this system will be equal to CL, since it is stronger inferentially and metainferentially than both ST and TS.