KRM3 - RM3 with K Modal


Semantics

A KRM3 frame comprises the interpretation of sentences and predicates at a world. A KRM3 model comprises a non-empty collection of KRM3 frames, a world access relation R, and a set of constants (the domain).

The semantics for predication, quantification, and truth-functional operators are the same as RM3.

Consequence

Logical Consequence is defined just as in KFDE.

Logical Consequence

C is a Logical Consequence of A iff all models where A has a desginated value at w0 are models where C also has a designated value at w0.

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 w1Rw2, indicating that the pair  w1,w2  is in the access relation R.

Trunk

To build the trunk for an argument, add a designated node with each premise at world w0, followed by an undesignated node with the the conclusion at world w0.

To build the trunk for the argument A1 ... AnB write:
A1 , w0
An , w0
B , w0

Closure

The closure rules are the same as RM3.

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

Rules

Non-modal rules for KRM3 are exactly like their RM3 counterparts, with the addition of carrying over the world marker from the target node(s).

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