TB3E - B3E with T Modal


Semantics

TB3E semantics behave just like KB3E semantics.

TB3E includes the T 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

TB3E 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

TB3E includes the K3 and FDE closure rules.

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

Rules

TB3E contains all the KB3E rules plus the T 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≤TReflexive[source]
A, w0
w0Rw0

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