KB3E - B3E with K Modal


Semantics

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

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 \(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

The closure rules are the same as B3E.

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

Rules

Non-modal rules for KB3E are exactly like their B3E 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
¬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