Metainferential Tableaux¶

Classes for metainferential tableaux, of the kind described in (citation needed)

Base Classes¶

class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxStandard(content, bar=False)¶

Class for a standard in metainferential tableaux (the second member of each node)

Parameters:

content (list or set or string) – Basic (level-0) indices are sets (e.g. {'1', 'i'}), higher level standards are 2-lists of lower level ones, (e.g. [{'1', 'i'}, {'1'}] -aka TS). The formulation of a system’s rules can include variables as standards (e.g. 'X'). See MetainferentialTableauxStandard.standard_variables
bar (bool, optional) – Whether the index has a bar on top or not. Defaults to False.

Notes

Note that the __init__ method of will automatically turn sets and lists within a standard into standard. Thus, you can write MetainferentialTableauxStandard([{'1'}, {'1'}]) instead of MetainferentialTableauxStandard([MetainferentialTableauxStandard({'1'}), MetainferentialTableauxStandard({'1'})])

Examples

>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard
>>> standard = MetainferentialTableauxStandard([[{'1', 'i'}, {'1'}], [{'1', 'i'}, {'1'}]], bar=True)
>>> isinstance(standard, MetainferentialTableauxStandard)
True
>>> isinstance(standard.content[0], MetainferentialTableauxStandard)
True
>>> standard.content[0].bar  # bar status is not inherited to content sub-standards
False

property level¶

Returns the level of a standard

Examples

>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard
>>> standard = MetainferentialTableauxStandard([[{'1', 'i'}, {'1'}], [{'1', 'i'}, {'1'}]])  # TS/ST
>>> standard.level
2
>>> standard.content[0].level  # TS
1
>>> standard.content[0].content[1].level  # S
0

Note that standard variables do not have a level, and will raise ValueError if their level is queried

>>> MetainferentialTableauxStandard('X').level
Traceback (most recent call last):
...
ValueError: Variable standard can have any level
>>> MetainferentialTableauxStandard(['X', {'1'}]).level
Traceback (most recent call last):
...
ValueError: Variable standard can have any level

is_instance_of(idx2, subst_dict=None, return_subst_dict=False)¶

Determines whether a standard is an instance of another standard

A MetainferentialTableauxStandard (self) is considered an instance of another (idx2) iff self and node have the same bar status, and one of the following occurs:

idx2 is a standard variable (see MetainferentialTableauxStandard.standard_variables). The default standard variables are 'W', 'X', 'Y', 'Z'
idx2 is a set (i.e. a level-0 standard) and self.content == idx2.content
idx2 is a 2-list (a level-n>0 standard) and both members of self.content are instances of both members of idx2.content, respectively

Examples

>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard
>>> simple_standard = MetainferentialTableauxStandard({'1', 'i'}, bar=False)  # T
>>> simple_standard.is_instance_of(MetainferentialTableauxStandard('X'))
True
>>> simple_standard.is_instance_of(MetainferentialTableauxStandard({'1', 'i'}))
True
>>> simple_standard.is_instance_of(MetainferentialTableauxStandard({'1'}))
False
>>> simple_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'Y']))
False

>>> complex_standard = MetainferentialTableauxStandard([{'1', 'i'}, {'1'}], bar=False)  # TS
>>> complex_standard.is_instance_of(MetainferentialTableauxStandard('X'))
True
>>> complex_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'Y']))
True
>>> complex_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'X']))
False
>>> complex_standard.is_instance_of(MetainferentialTableauxStandard([{'1'}, {'1', 'i'}]))
False

class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxNode(content, index=None, justification=None, parent=None, children=None)¶

Nodes for metainferential tableaux

Parameters:

content (logics.classes.propositional.Formula or logics.classes.propositional.Inference) – The formula or inference of the node
index (logics.classes.propositional.proof_theories.metainferntial_tableaux.MetainferentialTableauxStandard) – The standard of the node
justification (str, optional) – If the node is non-root, this parameter should contain the name of the rule by which it was obtained
parent (logics.classes.propositional.proof_theories.TableauxNode, optional) – The parent node. The root node of a tableaux has None as parent (the default value).
children (list of logics.classes.propositional.proof_theories.TableauxNode, optional) – A list of the children node. Also optional. If child nodes are specified with the parent attribute, there is no need to provide this (see the example below).

Notes

This subclasses logics.classes.propositional.proof_theories.tableaux.TableauxNode, and overrides a few methods. The functioning is almost identical

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_infinite_language as lang
>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import (
...     MetainferentialTableauxStandard, MetainferentialTableauxNode
>>> )
>>> S = MetainferentialTableauxStandard({'1'})
>>> Sbar = MetainferentialTableauxStandard({'1'}, bar=True)
>>> ST = MetainferentialTableauxStandard([{'1'}, {'1', 'i'}])
>>> XY = MetainferentialTableauxStandard(['X', 'Y'])
>>> XYbar = MetainferentialTableauxStandard(['X', 'Y'], bar=True)
>>> node1 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=ST)
>>> node2 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=XY)
>>> node3 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=XYbar)
>>> node1.is_instance_of(node2, lang)
True
>>> node1.is_instance_of(node3, lang)
False
>>> MetainferentialTableauxNode(classical_parser.parse('p'), index=S, parent=node1)
>>> MetainferentialTableauxNode(classical_parser.parse('q'), index=S, parent=node1)
>>> node1.print_tree(classical_parser)
p / q, [{'1'}, {'1', 'i'}]
├── p, {'1'}
└── q, {'1'}

Metainferential Tableaux System¶

class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxSystem(base_indexes, language, rules, closure_rules, solver=None)¶

Class for metainferential tableaux systems

Takes an extra parameter base_indexes, which should be a set. This defines what will be the valid standards. E.g. if base_indexes is {'1', 'i', '0'} then [{'1', 'i'}, {'1'}] will be a valid standard but [{'1', 'n'}, {'1'}] will not.

Notes

This subclasses logics.classes.propositional.proof_theories.tableaux.TableauxSystem, and overrides a few methods. The functioning is almost identical
Also note that the is_correct_tree method has not been implemented yet for this class.

Instances¶

logics.instances.propositional.metainferential_tableaux.CL_metainferential_tableaux_system¶: Tableaux system for every metainferential logic, of any level, using the CL (two-valued classical) schema

logics.instances.propositional.metainferential_tableaux.SK_metainferential_tableaux_system¶: Tableaux system for every metainferential logic, of any level, using the SK (three-valued strong Kleene) schema (see citation needed, examples below)

logics.instances.propositional.metainferential_tableaux.WK_metainferential_tableaux_system¶: Tableaux system for every metainferential logic, of any level, using the WK (three-valued weak Kleene) schema (see citation needed)

Metainferential Tableaux Solver¶

class logics.utils.solvers.tableaux.MetainferentialTableauxSolver¶

Solver class for many-valued metainferential systems

The default instance of the class it at logics.utils.solvers.tableaux.metainferential_tableaux_solver

The solve method takes as parameters:

inference: a logics.classes.propositional.Inference
tableaux_system: a logics.classes.propositional.proof_theories.tableaux.MetainferentialTableauxSystem
beggining_index: a list or set like [{'1', 'i'}, {'1'}]. Note that this is not a MetainferentialTableauxStandard -those are reserved for tableaux nodes.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.metainferential_tableaux import SK_metainferential_tableaux_system as sk_tableaux
>>> from logics.utils.solvers.tableaux import metainferential_tableaux_solver
>>> meta_explosion = classical_parser.parse('(/ p ∧ ~p) // (/q)')
>>> tree = metainferential_tableaux_solver.solve(
...     inference=meta_explosion,
...     tableaux_system=sk_tableaux,
...     beggining_index=[[{'1', 'i'}, {'1'}], [{'1'}, {'1', 'i'}]]  # TS/ST, closed
... )
>>> tree.print_tree(classical_parser)
(/ p ∧ ~p) // (/ q), -[[{'1', 'i'}, {'1'}], [{'1'}, {'1', 'i'}]]
└── / p ∧ ~p, [{'1', 'i'}, {'1'}] (inf0)
    └── / q, -[{'1'}, {'1', 'i'}] (inf0)
        └── p ∧ ~p, {'1'} (inf1)
            └── q, -{'1', 'i'} (inf0)
                └── p, {'1'} (R∧1)
                    └── ~p, {'1'} (R∧1)
                        └── q, {'0'} (complement)
                            └── p, {'0'} (R~1)
                                └── p, set() (intersection)
>>> sk_tableaux.tree_is_closed(tree)
True
>>> tree = metainferential_tableaux_solver.solve(
...     inference=meta_explosion,
...     tableaux_system=sk_tableaux,
...     beggining_index=[[{'1'}, {'1', 'i'}], [{'1'}, {'1', 'i'}]], # ST/ST, not closed
... )
>>> tree.print_tree(classical_parser)
(/ p ∧ ~p) // (/ q), -[[{'1'}, {'1', 'i'}], [{'1'}, {'1', 'i'}]]
└── / p ∧ ~p, [{'1'}, {'1', 'i'}] (inf0)
    └── / q, -[{'1'}, {'1', 'i'}] (inf0)
        └── p ∧ ~p, {'1', 'i'} (inf1)
            └── q, -{'1', 'i'} (inf0)
                ├── p ∧ ~p, {'1'} (singleton)
                │   └── q, {'0'} (complement)
                │       └── p, {'1'} (R∧1)
                │           └── ~p, {'1'} (R∧1)
                │               └── p, {'0'} (R~1)
                │                   └── p, set() (intersection)
                └── p ∧ ~p, {'i'} (singleton)
                    └── q, {'0'} (complement)
                        ├── p, {'1', 'i'} (R∧i)
                        │   └── ~p, {'i'} (R∧i)
                        │       ├── p, {'1'} (singleton)
                        │       │   └── p, {'i'} (R~1)
                        │       │       └── p, set() (intersection)
                        │       └── p, {'i'} (singleton)
                        └── p, {'i'} (R∧i)
                            └── ~p, {'1', 'i'} (R∧i)
                                ├── ~p, {'1'} (singleton)
                                │   └── p, {'0'} (R~1)
                                │       └── p, set() (intersection)
                                └── ~p, {'i'} (singleton)
>>> sk_tableaux.tree_is_closed(tree)
False