S5K3W - K3W with S5 Modal


Semantics

S5K3W semantics behave just like KK3W semantics.

S5K3W includes the access relation restrictions on models of S5:

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.

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

S5K3W 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 A1 ... AnB write:
A1 , w0
An , w0
B , w0

Closure

S5K3W includes the K3 and FDE closure rules.

K3Glut Closure[source]
A , w0
¬A , w0
FDEDesignation Closure[source]
A , w0
A , w0

Rules

S5K3W contains all the KK3W rules plus the S5 access rules.

Access Rules

R+S4Transitive[source]
w0Rw1
w1Rw2
w0Rw2
R≤TReflexive[source]
A, w0
w0Rw0
R⌯S5Symmetric[source]
w0Rw1
w1Rw0

Operator Rules

¬ Rules
¬¬FDEDouble Negation Designated[source]
¬¬A , w0
A , w0
¬¬FDEDouble Negation Undesignated[source]
¬¬A , w0
A , w0
∧ Rules
FDEConjunction Designated[source]
A ∧ B , w0
A , w0
B , w0
FDEConjunction Undesignated[source]
A ∧ B , w0
A , w0
B , w0
¬K3WConjunction Negated Designated[source]
¬(A ∧ B) , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬A , w0
¬B , w0
¬K3WConjunction Negated Undesignated[source]
¬(A ∧ B) , w0
A , w0
¬A , w0
B , w0
¬B , w0
A , w0
B , w0
∨ Rules
K3WDisjunction Designated[source]
A ∨ B , w0
A , w0
¬B , w0
¬A , w0
B , w0
A , w0
B , w0
K3WDisjunction Undesignated[source]
A ∨ B , w0
A , w0
¬A , w0
B , w0
¬B , w0
¬A , w0
¬B , w0
¬FDEDisjunction Negated Designated[source]
¬(A ∨ B) , w0
¬A , w0
¬B , w0
¬K3WDisjunction Negated Undesignated[source]
¬(A ∨ B) , w0
A ∨ B , w0
A , w0
¬A , w0
B , w0
¬B , w0
⊃ Rules
K3WMaterial Conditional Designated[source]
A ⊃ B , w0
¬A ∨ B , w0
K3WMaterial Conditional Undesignated[source]
A ⊃ B , w0
¬A ∨ B , w0
¬K3WMaterial Conditional Negated Designated[source]
¬(A ⊃ B) , w0
¬(¬A ∨ B) , w0
¬K3WMaterial Conditional Negated Undesignated[source]
¬(A ⊃ B) , w0
¬(¬A ∨ B) , w0
≡ Rules
K3WMaterial Biconditional Designated[source]
A ≡ B , w0
(A ⊃ B) ∧ (B ⊃ A) , w0
K3WMaterial Biconditional Undesignated[source]
A ≡ B , w0
(A ⊃ B) ∧ (B ⊃ A) , w0
¬K3WMaterial Biconditional Negated Designated[source]
¬(A ≡ B) , w0
¬((A ⊃ B) ∧ (B ⊃ A)) , w0
¬K3WMaterial Biconditional Negated Undesignated[source]
¬(A ≡ B) , w0
¬((A ⊃ B) ∧ (B ⊃ A)) , w0

Quantifier Rules

∃ Rules
FDEExistential Designated[source]
∃xFx , w0
Fa , w0
FDEExistential Undesignated[source]
∃xFx , w0
Fa , w0
¬FDEExistential Negated Designated[source]
¬∃xFx , w0
∀x¬Fx , w0
¬FDEExistential Negated Undesignated[source]
¬∃xFx , w0
∀x¬Fx , w0
∀ Rules
FDEUniversal Designated[source]
∀xFx , w0
Fa , w0
FDEUniversal Undesignated[source]
∀xFx , w0
Fa , w0
¬FDEUniversal Negated Designated[source]
¬∀xFx , w0
∃x¬Fx , w0
¬FDEUniversal Negated Undesignated[source]
¬∀xFx , w0
∃x¬Fx , w0

Compatibility Rules

⚬ Rules
FDEAssertion Designated[source]
⚬A , w0
A , w0
FDEAssertion Undesignated[source]
⚬A , w0
A , w0
¬FDEAssertion Negated Designated[source]
¬⚬A , w0
¬A , w0
¬FDEAssertion Negated Undesignated[source]
¬⚬A , w0
¬A , w0
→ Rules
K3WConditional Designated[source]
A → B , w0
¬A ∨ B , w0
K3WConditional Undesignated[source]
A → B , w0
¬A ∨ B , w0
¬K3WConditional Negated Designated[source]
¬(A → B) , w0
¬(¬A ∨ B) , w0
¬K3WConditional Negated Undesignated[source]
¬(A → B) , w0
¬(¬A ∨ B) , w0
↔ Rules
K3WBiconditional Designated[source]
A ↔ B , w0
(A ⊃ B) ∧ (B ⊃ A) , w0
K3WBiconditional Undesignated[source]
A ↔ B , w0
(A ⊃ B) ∧ (B ⊃ A) , w0
¬K3WBiconditional Negated Designated[source]
¬(A ↔ B) , w0
¬((A ⊃ B) ∧ (B ⊃ A)) , w0
¬K3WBiconditional Negated Undesignated[source]
¬(A ↔ B) , w0
¬((A ⊃ B) ∧ (B ⊃ A)) , w0

Notes

References