.. _S5:

.. module:: pytableaux.logics.s5

**********************************
L{} - S5 Normal Modal Logic
**********************************

L{} 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.

.. contents::
    :local:
    :depth: 2

------------------------

.. _s5-semantics:

Semantics
=========

L{} semantics behave just like {@K semantics}.

Reflexivity
-----------

L{} includes the *reflexivity* restriction of {@T}:

.. include:: include/t/m.reflexivity.rst

Transitivity
------------

L{} includes the *transitivity* restriction of {@S4}:

.. include:: include/s4/m.transitivity.rst

Symmetry
--------

L{} adds an additional *symmetry* restriction:

.. include:: include/s5/m.symmetry.rst

.. _s5-system:

Tableaux
========

L{} tableaux are constructed just like {@K system} tableaux.

Nodes
-----

.. include:: include/k/nodes_blurb.rst

Trunk
-----

.. include:: include/k/trunk_blurb.rst

.. tableau::
  :build-trunk:
  :prolog:

Closure
-------

.. tableau-rules::
  :group: closure
  :titles:
  :legend:
  :doc:

.. _s5-rules:

Rules
-----

L{} contains all the {@K rules}, the {@T} Reflexive rule, the
{@S4} Transitive rule, plus an additional Symmetric rule.

.. include:: include/s5/access_rules_group.rst

.. include:: include/k/rule_groups.rst

Notes
=====

References
==========


.. cssclass:: hidden

.. autoclass:: Rules()
  :members:
  :undoc-members: