T - Reflexive Normal Modal Logic

T is an extension of K, with a reflexive access relation.

---

Semantics

T semantics behave just like K semantics.

Reflexivity

T adds a reflexive restriction on the access relation for models.

Reflexivity

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

Tableaux

T 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

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

The Reflexive rule applies to an open branch b when there is a node n on b with a world w but there is not a node where w accesses w (itself).

Access Rules

R≤Reflexive

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 Reflexive(tableau, /, **opts)

R≤

A, w₀

⋮

w₀Rw₀

The Reflexive rule applies to an open branch b when there is a node n on b with a world w but there is not a node where w accesses w (itself).

For a node n on an open branch b on which appears a world w for which there is no node such that world1 and world2 is w, add a node to b where world1 and world2 is w.

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.Node'>,))>}), pred=(<NodeDesignation:()>, <NodeType:((<class 'pytableaux.proof.common.Node'>,))>), ignore_ticked=False)})

Helper classes mapped to their settings.

ignore_ticked = False

(FilterHelper) Whether to ignore all ticked nodes.

ticking: bool = False

Whether this is a ticking rule.

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

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

example_nodes()

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

The rule class legend.

name: str = 'Reflexive'

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