TRM3 - RM3 with T Modal


Semantics

TRM3 semantics behave just like KRM3 semantics.

TRM3 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

TRM3 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

TRM3 includes the LP and FDE closure rules.

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

Rules

TRM3 contains all the KRM3 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
¬FDEConjunction Negated Designated[source]
¬(A ∧ B) , w0
¬A , w0
¬B , w0
¬FDEConjunction Negated Undesignated[source]
¬(A ∧ B) , w0
¬A , w0
¬B , w0
∨ Rules
FDEDisjunction Designated[source]
A ∨ B , w0
A , w0
B , w0
FDEDisjunction Undesignated[source]
A ∨ B , w0
A , w0
B , w0
¬FDEDisjunction Negated Designated[source]
¬(A ∨ B) , w0
¬A , w0
¬B , w0
¬FDEDisjunction Negated Undesignated[source]
¬(A ∨ B) , w0
¬A , w0
¬B , w0
⊃ Rules
FDEMaterial Conditional Designated[source]
A ⊃ B , w0
¬A , w0
B , w0
FDEMaterial Conditional Undesignated[source]
A ⊃ B , w0
¬A , w0
B , w0
¬FDEMaterial Conditional Negated Designated[source]
¬(A ⊃ B) , w0
A , w0
¬B , w0
¬FDEMaterial Conditional Negated Undesignated[source]
¬(A ⊃ B) , w0
A , w0
¬B , w0
≡ Rules
FDEMaterial Biconditional Designated[source]
A ≡ B , w0
¬A , w0
¬B , w0
B , w0
A , w0
FDEMaterial Biconditional Undesignated[source]
A ≡ B , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬FDEMaterial Biconditional Negated Designated[source]
¬(A ≡ B) , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬FDEMaterial Biconditional Negated Undesignated[source]
¬(A ≡ B) , w0
¬A , w0
¬B , w0
B , w0
A , w0
→ Rules
RM3Conditional Designated[source]
A → B , w0
A , w0
¬B , w0
A , w0
¬A , w0
B , w0
¬B , w0
RM3Conditional Undesignated[source]
A → B , w0
A , w0
B , w0
¬A , w0
¬B , w0
¬FDEConditional Negated Designated[source]
¬(A → B) , w0
A , w0
¬B , w0
¬FDEConditional Negated Undesignated[source]
¬(A → B) , w0
A , w0
¬B , w0
↔ Rules
RM3Biconditional Designated[source]
A ↔ B , w0
A , w0
B , w0
¬A , w0
¬B , w0
A , w0
¬A , w0
B , w0
¬B , w0
L3Biconditional Undesignated[source]
A ↔ B , w0
A → B , w0
B → A , w0
¬FDEBiconditional Negated Designated[source]
¬(A ↔ B) , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬RM3Biconditional Negated Undesignated[source]
¬(A ↔ 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
¬FDEAssertion Negated Designated[source]
¬⚬A , w0
¬A , w0
¬FDEAssertion Negated Undesignated[source]
¬⚬A , w0
¬A , w0

Notes

References