S4GO - GO with S4 Modal

---

Semantics

The semantics for predication, quantification, and truth-functional operators are the same as GO.

Modal Operators

For modality, we reuse the crunch function from GO quantification:

Crunched Value

The crunched value of v is 1 (T) if v is 1, else 0 (F).

Possibility

The value of a possibility sentence ◻A at \(w\) is the maximum of the crunched values of its operand \(A\) at each world \(w'\) such that \(\langle\ w, w'\ \rangle\) is in \(R\).

This is in accord with interpreting the possibility operator in terms of generalized disjunction.

Necessity

The value of a necessity sentence ◻A at \(w\) is the minimum of the crunched values of its operand \(A\) at each world \(w'\) such that \(\langle\ w, w'\ \rangle\) is in \(R\).

This is in accord with interpreting the necessity operator in terms of generalized conjunction.

S4GO includes the access relation restrictions on models of S4:

Reflexivity

In every model, for each world \(w\), \(\langle\ w,w\ \rangle\) is in the access relation.

Transitivity

In every model, for each world \(w\), and each world \(w'\), for any world \(w''\) such that \(\langle\ w,w'\ \rangle\) and \(\langle\ w',w''\ \rangle\) are in the access relation, then \(\langle\ w,w''\ \rangle\) is in the access relation.

Tableaux

S4GO tableaux are constructed just like KFDE system tableaux.

Nodes

Nodes for many-valued modal tableaux come in two types:

• A node consisting of a sentence, a designation marker (⊕ or ⊖), and a world.

• An access node like \(w_1Rw_2\), indicating that the pair \(\langle\ w_1, w_2\ \rangle\) is in the access relation \(R\).

Trunk

To build the trunk for an argument, add a designated node with each premise at world \(w_0\), followed by an undesignated node with the the conclusion at world \(w_0\).

To build the trunk for the argument A₁ ... A_n ∴ B write:

A₁ ⊕, w₀

⋮

A_n ⊕, w₀

B ⊖, w₀

Closure

S4GO includes the K₃ and FDE closure rules.

⊗K₃Glut Closure

A ⊕, w₀

⋮

¬A ⊕, w₀

⊗

⊗FDEDesignation Closure

A ⊕, w₀

⋮

A ⊖, w₀

⊗

Rules

S4GO contains all the GO rules, and adds modal operator rules, as well as the S4 access rules.

Modal Operator Rules

◇ Rules

◇⊕KFDEPossibility Designated

◇A ⊕, w₀

⋮

A ⊕, w₁

w₀Rw₁

◇⊖Possibility Undesignated

◇A ⊖, w₀

⋮

¬◇A ⊕, w₀

¬◇⊕Possibility Negated Designated

¬◇A ⊕, w₀

w₀Rw₁

⋮

A ⊖, w₁

¬◇⊖Possibility Negated Undesignated

¬◇A ⊖, w₀

⋮

◇A ⊕, w₀

◻ Rules

◻⊕KFDENecessity Designated

◻A ⊕, w₀

w₀Rw₁

⋮

A ⊕, w₁

◻⊖Necessity Undesignated

◻A ⊖, w₀

⋮

¬◻A ⊕, w₀

¬◻⊕Necessity Negated Designated

¬◻A ⊕, w₀

⋮

A ⊖, w₁

w₀Rw₁

¬◻⊖Necessity Negated Undesignated

¬◻A ⊖, w₀

⋮

◻A ⊕, w₀

Access Rules

R+S4Transitive

w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

R≤TReflexive

A, w₀

⋮

w₀Rw₀

Operator Rules

⚬ Rules

⚬⊕FDEAssertion Designated

⚬A ⊕, w₀

⋮

A ⊕, w₀

⚬⊖FDEAssertion Undesignated

⚬A ⊖, w₀

⋮

A ⊖, w₀

¬⚬⊕B³_EAssertion Negated Designated

¬⚬A ⊕, w₀

⋮

A ⊖, w₀

¬⚬⊖B³_EAssertion Negated Undesignated

¬⚬A ⊖, w₀

⋮

A ⊕, w₀

¬ Rules

¬¬⊕FDEDouble Negation Designated

¬¬A ⊕, w₀

⋮

A ⊕, w₀

¬¬⊖FDEDouble Negation Undesignated

¬¬A ⊖, w₀

⋮

A ⊖, w₀

∧ Rules

∧⊕FDEConjunction Designated

A ∧ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∧⊖GOConjunction Undesignated

A ∧ B ⊖, w₀

⋮

¬(A ∧ B) ⊕, w₀

¬∧⊕GOConjunction Negated Designated

¬(A ∧ B) ⊕, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∧⊖GOConjunction Negated Undesignated

¬(A ∧ B) ⊖, w₀

⋮

A ∧ B ⊕, w₀

∨ Rules

∨⊕FDEDisjunction Designated

A ∨ B ⊕, w₀

⋮

A ⊕, w₀

B ⊕, w₀

∨⊖GODisjunction Undesignated

A ∨ B ⊖, w₀

⋮

¬(A ∨ B) ⊕, w₀

¬∨⊕GODisjunction Negated Designated

¬(A ∨ B) ⊕, w₀

⋮

A ⊖, w₀

B ⊖, w₀

¬∨⊖GODisjunction Negated Undesignated

¬(A ∨ B) ⊖, w₀

⋮

A ∨ B ⊕, w₀

⊃ Rules

⊃⊕FDEMaterial Conditional Designated

A ⊃ B ⊕, w₀

⋮

¬A ⊕, w₀

B ⊕, w₀

⊃⊖GOMaterial Conditional Undesignated

A ⊃ B ⊖, w₀

⋮

¬(A ⊃ B) ⊕, w₀

¬⊃⊕GOMaterial Conditional Negated Designated

¬(A ⊃ B) ⊕, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

¬⊃⊖GOMaterial Conditional Negated Undesignated

¬(A ⊃ B) ⊖, w₀

⋮

A ⊃ B ⊕, w₀

≡ Rules

≡⊕FDEMaterial Biconditional Designated

A ≡ B ⊕, w₀

⋮

¬A ⊕, w₀

¬B ⊕, w₀

B ⊕, w₀

A ⊕, w₀

≡⊖GOMaterial Biconditional Undesignated

A ≡ B ⊖, w₀

⋮

¬(A ≡ B) ⊕, w₀

¬≡⊕GOMaterial Biconditional Negated Designated

¬(A ≡ B) ⊕, w₀

⋮

¬A ⊖, w₀

B ⊖, w₀

A ⊖, w₀

¬B ⊖, w₀

¬≡⊖GOMaterial Biconditional Negated Undesignated

¬(A ≡ B) ⊖, w₀

⋮

A ≡ B ⊕, w₀

→ Rules

→⊕L₃Conditional Designated

A → B ⊕, w₀

⋮

¬A ∨ B ⊕, w₀

A ⊖, w₀

B ⊖, w₀

¬A ⊖, w₀

¬B ⊖, w₀

→⊖GOConditional Undesignated

A → B ⊖, w₀

⋮

¬(A → B) ⊕, w₀

¬→⊕GOConditional Negated Designated

¬(A → B) ⊕, w₀

⋮

A ⊕, w₀

B ⊖, w₀

¬A ⊖, w₀

¬B ⊕, w₀

¬→⊖GOConditional Negated Undesignated

¬(A → B) ⊖, w₀

⋮

A → B ⊕, w₀

↔ Rules

↔⊕GOBiconditional Designated

A ↔ B ⊕, w₀

⋮

A → B ⊕, w₀

B → A ⊕, w₀

↔⊖GOBiconditional Undesignated

A ↔ B ⊖, w₀

⋮

¬(A ↔ B) ⊕, w₀

¬↔⊕GOBiconditional Negated Designated

¬(A ↔ B) ⊕, w₀

⋮

¬(A → B) ⊕, w₀

¬(B → A) ⊕, w₀

¬↔⊖GOBiconditional Negated Undesignated

¬(A ↔ B) ⊖, w₀

⋮

A ↔ B ⊕, w₀

Quantifier Rules

∃ Rules

∃⊕FDEExistential Designated

∃xFx ⊕, w₀

⋮

Fa ⊕, w₀

∃⊖GOExistential Undesignated

∃xFx ⊖, w₀

⋮

¬∃xFx ⊕, w₀

¬∃⊕GOExistential Negated Designated

¬∃xFx ⊕, w₀

⋮

∀x(¬Fx ∨ ¬(Fx ∨ ¬Fx)) ⊕, w₀

¬∃⊖GOExistential Negated Undesignated

¬∃xFx ⊖, w₀

⋮

∃xFx ⊕, w₀

∀ Rules

∀⊕FDEUniversal Designated

∀xFx ⊕, w₀

⋮

Fa ⊕, w₀

∀⊖GOUniversal Undesignated

∀xFx ⊖, w₀

⋮

¬∀xFx ⊕, w₀

¬∀⊕GOUniversal Negated Designated

¬∀xFx ⊕, w₀

⋮

∃x¬Fx ⊕, w₀

Fa ⊖, w₀

¬Fa ⊖, w₀

¬∀⊖GOUniversal Negated Undesignated

¬∀xFx ⊖, w₀

⋮

∀xFx ⊕, w₀

Notes

References

• Doug Owings (2012). Indeterminacy and Logical Atoms. Ph.D. Thesis, University of Connecticut.

class Rules

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k3.Rules.GlutClosure'>, <class 'pytableaux.logics.fde.Rules.DesignationClosure'>)

class PossibilityNegatedDesignated(tableau, /, **opts)

¬◇⊕

¬◇A ⊕, w₀

w₀Rw₁

⋮

A ⊖, w₁

Parameters:

tableau (Tableau) --

static new_designation(a, /)

Same as not a.

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility(negated)>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.NodeCount'>: None, <class 'pytableaux.proof.helpers.NodesWorlds'>: None, <class 'pytableaux.proof.helpers.WorldIndex'>: None})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Possibility), (Legend.designation, True))

The rule class legend.

name: str = 'PossibilityNegatedDesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityNegatedDesignated(tableau, /, **opts)

¬◻⊕

¬◻A ⊕, w₀

⋮

A ⊖, w₁

w₀Rw₁

Parameters:

tableau (Tableau) --

static new_designation(a, /)

Same as not a.

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=True)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity(negated)>}), pred=(<NodeDesignation:(designated=True)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity(negated)>), ignore_ticked=True), <class 'pytableaux.proof.helpers.QuitFlag'>: None, <class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.AplSentCount'>: None})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = True

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Necessity), (Legend.designation, True))

The rule class legend.

name: str = 'NecessityNegatedDesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class PossibilityUndesignated(tableau, /, **opts)

◇⊖

◇A ⊖, w₀

⋮

¬◇A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Possibility), (Legend.designation, False))

The rule class legend.

name: str = 'PossibilityUndesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityUndesignated(tableau, /, **opts)

◻⊖

◻A ⊖, w₀

⋮

¬◻A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.operator, Operator.Necessity), (Legend.designation, False))

The rule class legend.

name: str = 'NecessityUndesignated'

The rule class name.

negated: bool | None = None

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class PossibilityNegatedUndesignated(tableau, /, **opts)

¬◇⊖

¬◇A ⊖, w₀

⋮

◇A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Possibility(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Possibility(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Possibility), (Legend.designation, False))

The rule class legend.

name: str = 'PossibilityNegatedUndesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (90, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

class NecessityNegatedUndesignated(tableau, /, **opts)

¬◻⊖

¬◻A ⊖, w₀

⋮

◻A ⊕, w₀

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:(designated=False)>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <class 'pytableaux.proof.filters.NodeSentence'>: <NodeSentence:operator=Necessity(negated)>}), pred=(<NodeDesignation:(designated=False)>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>, <NodeSentence:operator=Necessity(negated)>), ignore_ticked=True)})

Helper classes mapped to their settings.

NodeFilters = {<class 'pytableaux.proof.filters.NodeDesignation'>: None, <class 'pytableaux.proof.filters.NodeSentence'>: None, <class 'pytableaux.proof.filters.NodeType'>: None}

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

designation: bool | None = False

legend: tuple[tuple[str, Any], ...] = ((Legend.negated, Operator.Negation), (Legend.operator, Operator.Necessity), (Legend.designation, False))

The rule class legend.

name: str = 'NecessityNegatedUndesignated'

The rule class name.

negated: bool | None = True

operator: Operator | None = (100, 1)

predicate: Predicate | None = None

quantifier: Quantifier | None = None

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

groups: tuple[tuple[type[Rule], ...], ...] = ((<class 'pytableaux.logics.fde.Rules.AssertionDesignated'>, <class 'pytableaux.logics.fde.Rules.AssertionUndesignated'>, <class 'pytableaux.logics.b3e.Rules.AssertionNegatedDesignated'>, <class 'pytableaux.logics.b3e.Rules.AssertionNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.ConjunctionDesignated'>, <class 'pytableaux.logics.go.Rules.ConjunctionUndesignated'>, <class 'pytableaux.logics.go.Rules.ConjunctionNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.DisjunctionNegatedDesignated'>, <class 'pytableaux.logics.go.Rules.DisjunctionUndesignated'>, <class 'pytableaux.logics.go.Rules.DisjunctionNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.MaterialConditionalNegatedDesignated'>, <class 'pytableaux.logics.go.Rules.MaterialConditionalUndesignated'>, <class 'pytableaux.logics.go.Rules.MaterialConditionalNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.MaterialBiconditionalUndesignated'>, <class 'pytableaux.logics.go.Rules.MaterialBiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.ConditionalUndesignated'>, <class 'pytableaux.logics.go.Rules.ConditionalNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.BiconditionalUndesignated'>, <class 'pytableaux.logics.go.Rules.BiconditionalNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.BiconditionalDesignated'>, <class 'pytableaux.logics.go.Rules.ExistentialNegatedDesignated'>, <class 'pytableaux.logics.go.Rules.ExistentialUndesignated'>, <class 'pytableaux.logics.go.Rules.ExistentialNegatedUndesignated'>, <class 'pytableaux.logics.go.Rules.UniversalUndesignated'>, <class 'pytableaux.logics.go.Rules.UniversalNegatedUndesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationDesignated'>, <class 'pytableaux.logics.fde.Rules.DoubleNegationUndesignated'>, <class 'pytableaux.logics.s4go.Rules.PossibilityUndesignated'>, <class 'pytableaux.logics.s4go.Rules.PossibilityNegatedUndesignated'>, <class 'pytableaux.logics.s4go.Rules.NecessityUndesignated'>, <class 'pytableaux.logics.s4go.Rules.NecessityNegatedUndesignated'>), (<class 'pytableaux.logics.s4.Rules.Transitive'>,), (<class 'pytableaux.logics.kfde.Rules.NecessityDesignated'>, <class 'pytableaux.logics.s4go.Rules.PossibilityNegatedDesignated'>), (<class 'pytableaux.logics.kfde.Rules.PossibilityDesignated'>, <class 'pytableaux.logics.s4go.Rules.NecessityNegatedDesignated'>), (<class 'pytableaux.logics.t.Rules.Reflexive'>,), (<class 'pytableaux.logics.fde.Rules.DisjunctionDesignated'>, <class 'pytableaux.logics.go.Rules.ConjunctionNegatedDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialConditionalDesignated'>, <class 'pytableaux.logics.fde.Rules.MaterialBiconditionalDesignated'>, <class 'pytableaux.logics.go.Rules.MaterialBiconditionalNegatedDesignated'>, <class 'pytableaux.logics.l3.Rules.ConditionalDesignated'>, <class 'pytableaux.logics.go.Rules.ConditionalNegatedDesignated'>, <class 'pytableaux.logics.go.Rules.BiconditionalNegatedDesignated'>), (<class 'pytableaux.logics.fde.Rules.ExistentialDesignated'>,), (<class 'pytableaux.logics.go.Rules.UniversalNegatedDesignated'>,), (<class 'pytableaux.logics.fde.Rules.UniversalDesignated'>,))