NH - Paraconsistent Hybrid Logic

NH is a three-valued predicate logic with values T, F, and B. It is the glutty dual of MH.


Semantics

Truth Values

Common labels for the values include:

T

1

just true

B

0.5

both true and false

F

0

just false

Designated Values

The set of designated values for NH is: { T, B }

Truth Tables

The value of a sentence with a truth-functional operator is determined by the values of its operands according to the following tables.

Negation
¬
T F
B B
F T
Conjunction
∧ T B F
T T B F
B B T F
F F F F
Disjunction
∨ T B F
T T T T
B T B B
F T B F
Conditional
→ T B F
T T T F
B T T F
F T T T

Defined Operators

The Biconditional ↔, in turn, is defined in the usual way:

A ↔ B \(:=\) (A → B) ∧ (B → A)
Biconditional
↔ T B F
T T T F
B T T F
F F F T

The Material Conditional ⊃ is definable in terms of disjunction:

A ⊃ B \(:=\) ¬A ∨ B

Likewise the Material Biconditional ≡ is defined in terms of ⊃ and ∧:

A ≡ B \(:=\) (A ⊃ B) ∧ (B ⊃ A)
Material Conditional
⊃ T B F
T T B F
B T B B
F T T T
Material Biconditional
≡ T B F
T T B F
B B T B
F F B T

Compatibility Tables

NH does not have a separate Assertion operator, but we include a table and rules for it, for cross-compatibility.

Assertion
⚬
T T
B B
F F

Predication

A sentence with predicate P with parameters \(\langle a_0, ... ,a_n\rangle\) is assigned a value as follows:

  • T iff \(\langle a_0, ... ,a_n\rangle\) is in the extension of P and not in the

    anti-extension of P.

  • F iff \(\langle a_0, ... ,a_n\rangle\) is in the anti-extension of P and not

    in the extension of P.

  • B iff \(\langle a_0, ... ,a_n\rangle\) is in both the extension and anti-extension

    of P.

Consequence

Logical Consequence is defined in terms of the set of designated values { T, B }:

Logical Consequence

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

Tableaux

NH tableaux are built similary to FDE.

Nodes

Nodes for many-value tableaux consiste of a sentence plus a designation marker: ⊕ for designated, and ⊖ for undesignated.

Trunk

To build the trunk for an argument, add a designated node for each premise, and an undesignated node for the conclusion.

To build the trunk for the argument A1 ... An ∴ B write:
A1 ⊕
⋮
An ⊕
B ⊖

Closure

⊗Gap Closure[source]
A ⊖
⋮
¬A ⊖
⊗
⊗Designation Closure[source]
A ⊕
⋮
A ⊖
⊗

Rules

In general, rules for connectives consist of four rules per connective: a designated rule, an undesignated rule, a negated designated rule, and a negated undesignated rule. The special case of negation has a total of two rules which apply to double negation only, one designated rule, and one undesignated rule.

Operator Rules

¬ Rules
¬¬⊕FDEDouble Negation Designated[source]
¬¬A ⊕
⋮
A ⊕
¬¬⊖FDEDouble Negation Undesignated[source]
¬¬A ⊖
⋮
A ⊖
∧ Rules
∧⊕FDEConjunction Designated[source]
A ∧ B ⊕
⋮
A ⊕
B ⊕
∧⊖FDEConjunction Undesignated[source]
A ∧ B ⊖
⋮
A ⊖
B ⊖
¬∧⊕Conjunction Negated Designated[source]
¬(A ∧ B) ⊕
⋮
A ⊖
B ⊖
A ⊕
¬A ⊕
¬B ⊖
B ⊕
¬B ⊕
¬A ⊖
¬∧⊖Conjunction Negated Undesignated[source]
¬(A ∧ B) ⊖
⋮
¬A ⊖
¬B ⊖
A ⊕
¬A ⊕
B ⊕
¬B ⊕
∨ Rules
∨⊕FDEDisjunction Designated[source]
A ∨ B ⊕
⋮
A ⊕
B ⊕
∨⊖FDEDisjunction Undesignated[source]
A ∨ B ⊖
⋮
A ⊖
B ⊖
¬∨⊕FDEDisjunction Negated Designated[source]
¬(A ∨ B) ⊕
⋮
¬A ⊕
¬B ⊕
¬∨⊖FDEDisjunction Negated Undesignated[source]
¬(A ∨ B) ⊖
⋮
¬A ⊖
¬B ⊖
⊃ Rules
⊃⊕FDEMaterial Conditional Designated[source]
A ⊃ B ⊕
⋮
¬A ⊕
B ⊕
⊃⊖FDEMaterial Conditional Undesignated[source]
A ⊃ B ⊖
⋮
¬A ⊖
B ⊖
¬⊃⊕Material Conditional Negated Designated[source]
¬(A ⊃ B) ⊕
⋮
A ⊕
¬B ⊕
¬⊃⊖Material Conditional Negated Undesignated[source]
¬(A ⊃ B) ⊖
⋮
A ⊖
¬B ⊖
≡ Rules
≡⊕MHMaterial Biconditional Designated[source]
A ≡ B ⊕
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊕
≡⊖MHMaterial Biconditional Undesignated[source]
A ≡ B ⊖
⋮
(A ⊃ B) ∧ (B ⊃ A) ⊖
¬≡⊕MHMaterial Biconditional Negated Designated[source]
¬(A ≡ B) ⊕
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊕
¬≡⊖MHMaterial Biconditional Negated Undesignated[source]
¬(A ≡ B) ⊖
⋮
¬((A ⊃ B) ∧ (B ⊃ A)) ⊖
→ Rules
→⊕MHConditional Designated[source]
A → B ⊕
⋮
A ⊖
B ⊕
→⊖MHConditional Undesignated[source]
A → B ⊖
⋮
A ⊕
B ⊖
¬→⊕MHConditional Negated Designated[source]
¬(A → B) ⊕
⋮
A ⊕
B ⊖
¬→⊖MHConditional Negated Undesignated[source]
¬(A → B) ⊖
⋮
A ⊖
B ⊕
↔ Rules
↔⊕MHBiconditional Designated[source]
A ↔ B ⊕
⋮
(A → B) ∧ (B → A) ⊕
↔⊖MHBiconditional Undesignated[source]
A ↔ B ⊖
⋮
(A → B) ∧ (B → A) ⊖
¬↔⊕MHBiconditional Negated Designated[source]
¬(A ↔ B) ⊕
⋮
¬((A → B) ∧ (B → A)) ⊕
¬↔⊖MHBiconditional Negated Undesignated[source]
¬(A ↔ B) ⊖
⋮
¬((A → B) ∧ (B → A)) ⊖

Compatibility Rules

⚬ Rules
⚬⊕FDEAssertion Designated[source]
⚬A ⊕
⋮
A ⊕
⚬⊖FDEAssertion Undesignated[source]
⚬A ⊖
⋮
A ⊖
¬⚬⊕FDEAssertion Negated Designated[source]
¬⚬A ⊕
⋮
¬A ⊕
¬⚬⊖FDEAssertion Negated Undesignated[source]
¬⚬A ⊖
⋮
¬A ⊖

Notes

References