S4 - S4 Normal Modal Logic

S4 is an extension of K with a reflexive and transitive access relation.

---

Semantics

S4 semantics behave just like K semantics.

Reflexivity

S4 includes the reflexivity restriction of T:

Reflexivity

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

Transitivity

S4 adds an additional transitivity restriction:

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

S4 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

⊗KContradiction Closure

A, w₀

⋮

¬A, w₀

⊗

⊗¬=KSelf Identity Closure

⋮

a ≠ a, w₀

⊗

⊗¬E!KNon Existence Closure

⋮

¬E!a, w₀

⊗

Rules

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

Access Rules

R+Transitive

w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

R≤TReflexive

A, w₀

⋮

w₀Rw₀

Operator Rules

¬ Rules

¬¬KDouble Negation

¬¬A, w₀

⋮

A, w₀

∧ Rules

∧KConjunction

A ∧ B, w₀

⋮

A, w₀

B, w₀

¬∧KConjunction Negated

¬(A ∧ B), w₀

⋮

¬A, w₀

¬B, w₀

∨ Rules

∨KDisjunction

A ∨ B, w₀

⋮

A, w₀

B, w₀

¬∨KDisjunction Negated

¬(A ∨ B), w₀

⋮

¬A, w₀

¬B, w₀

⊃ Rules

⊃KMaterial Conditional

A ⊃ B, w₀

⋮

¬A, w₀

B, w₀

¬⊃KMaterial Conditional Negated

¬(A ⊃ B), w₀

⋮

A, w₀

¬B, w₀

≡ Rules

≡KMaterial Biconditional

A ≡ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬≡KMaterial Biconditional Negated

¬(A ≡ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Modal Operator Rules

◇ Rules

◇KPossibility

◇A, w₀

⋮

A, w₁

w₀Rw₁

¬◇KPossibility Negated

¬◇A, w₀

⋮

◻¬A, w₀

◻ Rules

◻KNecessity

◻A, w₀

w₀Rw₁

⋮

A, w₁

¬◻KNecessity Negated

¬◻A, w₀

⋮

◇¬A, w₀

Predicate Rules

= Rules

=KIdentity Indiscernability

Fa, w₀

a = b, w₀

⋮

Fb, w₀

Quantifier Rules

∃ Rules

∃KExistential

∃xFx, w₀

⋮

Fa, w₀

¬∃KExistential Negated

¬∃xFx, w₀

⋮

∀x¬Fx, w₀

∀ Rules

∀KUniversal

∀xFx, w₀

⋮

Fa, w₀

¬∀KUniversal Negated

¬∀xFx, w₀

⋮

∃x¬Fx, w₀

Compatibility Rules

⚬ Rules

⚬KAssertion

⚬A, w₀

⋮

A, w₀

¬⚬KAssertion Negated

¬⚬A, w₀

⋮

¬A, w₀

→ Rules

→KConditional

A → B, w₀

⋮

¬A, w₀

B, w₀

¬→KConditional Negated

¬(A → B), w₀

⋮

A, w₀

¬B, w₀

↔ Rules

↔KBiconditional

A ↔ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬↔KBiconditional Negated

¬(A ↔ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Notes

References

class Rules

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

class Transitive(tableau, /, **opts)

R+

w₀Rw₁

w₁Rw₂

⋮

w₀Rw₂

For any world w appearing on a branch b, for each world w' and for each world w'' on b, if wRw' and wRw'' appear on b, but wRw'' does not appear on b, then add wRw'' 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', 'transitive'))]

score_candidate(target, /)

example_nodes()

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

branching: int = 0

The number of additional branches created.

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

legend: tuple[tuple[str, Any], ...] = ((Marking.tableau, ('access', 'transitive')),)

The rule class legend.

name: str = 'Transitive'

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'>))