S5B3E - B3E with S5 Modal


Semantics

S5B3E semantics behave just like KB3E semantics.

S5B3E 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

S5B3E 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

S5B3E includes the K3 and FDE closure rules.

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

Rules

S5B3E contains all the KB3E 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
B3EMaterial Biconditional Undesignated[source]
A ≡ B , w0
A , w0
¬A , w0
B , w0
¬B , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬K3WMaterial Biconditional Negated Designated[source]
¬(A ≡ B) , w0
¬((A ⊃ B) ∧ (B ⊃ A)) , w0
¬B3EMaterial Biconditional Negated Undesignated[source]
¬(A ≡ B) , w0
A , w0
¬A , w0
B , w0
¬B , w0
¬A , w0
¬B , w0
A , w0
B , 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
¬B3EAssertion Negated Designated[source]
¬⚬A , w0
A , w0
¬B3EAssertion Negated Undesignated[source]
¬⚬A , w0
A , w0
→ Rules
B3EConditional Designated[source]
A → B , w0
¬⚬A ∨ ⚬B , w0
B3EConditional Undesignated[source]
A → B , w0
A , w0
B , w0
¬B3EConditional Negated Designated[source]
¬(A → B) , w0
A , w0
B , w0
¬B3EConditional Negated Undesignated[source]
¬(A → B) , w0
¬(¬⚬A ∨ ⚬B) , w0
↔ Rules
B3EBiconditional Designated[source]
A ↔ B , w0
¬⚬A ∨ ⚬B , w0
¬⚬B ∨ ⚬A , w0
B3EBiconditional Undesignated[source]
A ↔ B , w0
¬⚬A ∨ ⚬B , w0
¬⚬B ∨ ⚬A , w0
¬B3EBiconditional Negated Designated[source]
¬(A ↔ B) , w0
¬(¬⚬A ∨ ⚬B) , w0
¬(¬⚬B ∨ ⚬A) , w0
¬B3EBiconditional Negated Undesignated[source]
¬(A ↔ B) , w0
A , w0
B , w0
A , w0
B , w0

Notes

References