KFDE - FDE with K Modal


Semantics

A KFDE frame comprises the interpretation of sentences and predicates at a world. A KFDE model comprises a non-empty collection of KFDE 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 FDE.

Consequence

Logical Consequence is defined similary as FDE, except with reference to a world:

Logical Consequence

C is a Logical Consequence of A iff all models where A has a desginated value at \(w_0\) are models where C also has a designated value at \(w_0\).

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

FDEDesignation Closure[source]
A , w0
A , w0

Rules

Non-modal rules for KFDE are exactly like their FDE 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

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
FDEConditional Designated[source]
A → B , w0
¬A , w0
B , w0
FDEConditional Undesignated[source]
A → 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
FDEBiconditional Designated[source]
A ↔ B , w0
¬A , w0
¬B , w0
B , w0
A , w0
FDEBiconditional Undesignated[source]
A ↔ B , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬FDEBiconditional Negated Designated[source]
¬(A ↔ B) , w0
A , w0
¬B , w0
¬A , w0
B , w0
¬FDEBiconditional Negated Undesignated[source]
¬(A ↔ B) , w0
¬A , w0
¬B , w0
B , w0
A , w0

Notes

  • Like FDE, there are no logical truths.

  • The standard modal operator interdefinabilities hold: ◻A¬◇¬A and ¬◻A◇¬A.

  • Modal forms of modus ponens fail, e.g. ◻(A → B), ◇A◇B.

References