S5 - S5 Normal Modal Logic

S5 is an extension of K with a reflexive, symmetric, and transitive access relation. The access relation provides Universal Access, meaning all worlds are visible to all worlds.

Semantics 

S5 semantics behave just like K semantics.

Reflexivity 

S5 includes the reflexivity restriction of T:

Reflexivity

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

Transitivity 

S5 includes the transitivity restriction of S4:

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.

Symmetry 

S5 adds an additional symmetry restriction:

Symmetry

In every model, for each world \(w\) and each world \(w'\), if \(\langle\ w,w'\ \rangle\) is in the access relation, then so is \(\langle\ w',w\ \rangle\).

Tableaux 

S5 tableaux are constructed just like K system tableaux.

Nodes 

Nodes for bivalent modal tableaux come in two types:

A sentence-world pair like \(A, w\), indicating that \(A\) is true at \(w\).
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 node with each premise, with world \(w_0\), followed by a node with the negation of the conclusion with world \(w_0\).

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

A₁, w₀

⋮

A_n, w₀

¬B, w₀

Closure 

⊗Contradiction Closure[source]: A, w₀

⋮

¬A, w₀

⊗

⊗¬=Self Identity Closure[source]: ⋮

a ≠ a, w₀

⊗

⊗¬E!Non Existence Closure[source]: ⋮

¬E!a, w₀

⊗

Rules 

S5 contains all the K rules, the T Reflexive rule, the S4 Transitive rule, plus an additional Symmetric rule.

Access Rules

R+S4Transitive[source]: w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

R≤TReflexive[source]: A, w₀

⋮

w₀Rw₀

R⌯Symmetric[source]: w₀Rw₁

⋮

w₁Rw₀

Operator Rules

¬ Rules

¬¬KDouble Negation[source]: ¬¬A, w₀

⋮

A, w₀

∧ Rules

∧KConjunction[source]: A ∧ B, w₀

⋮

A, w₀

B, w₀

¬∧KConjunction Negated[source]: ¬(A ∧ B), w₀

⋮

¬A, w₀

¬B, w₀

∨ Rules

∨KDisjunction[source]: A ∨ B, w₀

⋮

A, w₀

B, w₀

¬∨KDisjunction Negated[source]: ¬(A ∨ B), w₀

⋮

¬A, w₀

¬B, w₀

⊃ Rules

⊃KMaterial Conditional[source]: A ⊃ B, w₀

⋮

¬A, w₀

B, w₀

¬⊃KMaterial Conditional Negated[source]: ¬(A ⊃ B), w₀

⋮

A, w₀

¬B, w₀

≡ Rules

≡KMaterial Biconditional[source]: A ≡ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬≡KMaterial Biconditional Negated[source]: ¬(A ≡ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Predicate Rules

= Rules

=KIdentity Indiscernability[source]: Fa, w₀

a = b, w₀

⋮

Fb, w₀

Quantifier Rules

∃ Rules

∃KExistential[source]: ∃xFx, w₀

⋮

Fa, w₀

¬∃KExistential Negated[source]: ¬∃xFx, w₀

⋮

∀x¬Fx, w₀

∀ Rules

∀KUniversal[source]: ∀xFx, w₀

⋮

Fa, w₀

¬∀KUniversal Negated[source]: ¬∀xFx, w₀

⋮

∃x¬Fx, w₀

Compatibility Rules

⚬ Rules

⚬KAssertion[source]: ⚬A, w₀

⋮

A, w₀

¬⚬KAssertion Negated[source]: ¬⚬A, w₀

⋮

¬A, w₀

→ Rules

→KConditional[source]: A → B, w₀

⋮

¬A, w₀

B, w₀

¬→KConditional Negated[source]: ¬(A → B), w₀

⋮

A, w₀

¬B, w₀

↔ Rules

↔KBiconditional[source]: A ↔ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬↔KBiconditional Negated[source]: ¬(A ↔ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Notes 

References 

class Rules[source]

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k.Rules.ContradictionClosure'>, <class 'pytableaux.logics.k.Rules.SelfIdentityClosure'>, <class 'pytableaux.logics.k.Rules.NonExistenceClosure'>)

class Symmetric(tableau, /, **opts)[source]

R⌯

w₀Rw₁

⋮

w₁Rw₀

For any world w appearing on a branch b, for each world w' on b, if wRw' appears on b, but w'Rw does not appear on b, then add w'Rw to b.

Parameters:: tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.WorldIndex'>: None, <class 'pytableaux.proof.helpers.AdzHelper'>: None, <class 'pytableaux.proof.helpers.FilterHelper'>: Config(filters=mappingproxy({<class 'pytableaux.proof.filters.NodeDesignation'>: <NodeDesignation:()>, <class 'pytableaux.proof.filters.NodeType'>: <NodeType:((<class 'pytableaux.proof.common.AccessNode'>,))>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.AccessNode'>,))>), ignore_ticked=True)}): Helper classes mapped to their settings.

NodeType: alias of AccessNode

ticking: bool = False: Whether this is a ticking rule.

marklegend = [(Marking.tableau, ('access', 'symmetric'))]

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

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

branching: int = 0: The number of additional branches created.

legend: tuple[tuple[str, Any], ...] = ((Marking.tableau, ('access', 'symmetric')),): The rule class legend.

name: str = 'Symmetric': The rule class name.

timer_names: Sequence[str] = qsetf({'search', 'apply'}): StopWatch names to create in timers mapping.

groups: tuple[tuple[type[Rule], ...], ...] = ((<class 'pytableaux.logics.k.Rules.IdentityIndiscernability'>, <class 'pytableaux.logics.k.Rules.Assertion'>, <class 'pytableaux.logics.k.Rules.AssertionNegated'>, <class 'pytableaux.logics.k.Rules.Conjunction'>, <class 'pytableaux.logics.k.Rules.DisjunctionNegated'>, <class 'pytableaux.logics.k.Rules.MaterialConditionalNegated'>, <class 'pytableaux.logics.k.Rules.ConditionalNegated'>, <class 'pytableaux.logics.k.Rules.DoubleNegation'>, <class 'pytableaux.logics.k.Rules.PossibilityNegated'>, <class 'pytableaux.logics.k.Rules.NecessityNegated'>, <class 'pytableaux.logics.k.Rules.ExistentialNegated'>, <class 'pytableaux.logics.k.Rules.UniversalNegated'>), (<class 'pytableaux.logics.s4.Rules.Transitive'>,), (<class 'pytableaux.logics.k.Rules.Necessity'>, <class 'pytableaux.logics.k.Rules.Possibility'>), (<class 'pytableaux.logics.t.Rules.Reflexive'>,), (<class 'pytableaux.logics.k.Rules.ConjunctionNegated'>, <class 'pytableaux.logics.k.Rules.Disjunction'>, <class 'pytableaux.logics.k.Rules.MaterialConditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditionalNegated'>, <class 'pytableaux.logics.k.Rules.Conditional'>, <class 'pytableaux.logics.k.Rules.Biconditional'>, <class 'pytableaux.logics.k.Rules.BiconditionalNegated'>), (<class 'pytableaux.logics.k.Rules.Existential'>, <class 'pytableaux.logics.k.Rules.Universal'>), (<class 'pytableaux.logics.s5.Rules.Symmetric'>,))