A Paraconsistent Higher Order Logic - Artificial Intelligence and Symbolic Computation - page 43

• if [[ ϕ ]] = [[ ψ ]] ⇔ϕ ↔ ϕ

[[ ψ ]] i f [[ ϕ ]] = • ψ ⇔↔ψ

[[ ϕ ]] i f [[ ψ ]] = • ϕ ⇔ ϕ ↔

[[ ϕ ↔ ψ ]] =

[[ ¬ψ ]] i f [[ ϕ ]] = ◦ ¬ψ ⇔⊥↔ψ

[[ ¬ϕ ]] i f [[ ψ ]] = ◦ ¬ϕ ⇔ ϕ ↔⊥

◦ otherwise

As before, several cases may apply if and only if they agree on the result and
the semantic clause works for classical logic too.
Thesemanticclauseisanextensionoftheclauseforequality=:

•

if [[ ϕ ]] = [[ ψ ]]

[[ ϕ = ψ ]] =

◦

otherwise

We have the following abbreviations:

ϕ ⇔ ψ ≡ ϕ = ψ ϕ ⇒ ψ ≡ ϕ ⇔ ϕ ∧ ψ ϕ ≡ ϕ =

ϕ → ψ ≡ ϕ ↔ ϕ ∧ ψ ∼ϕ ≡¬ ϕ

The logical necessity operator is a so-called S5 modality.
We could also have used ( ϕ ⇒ ψ ) ∧ ( ψ ⇒ ϕ )for ϕ ⇔ ψ (using = instead of

⇔ in the definition of ⇒ ). Besides, ⇔ binds very loosely, even more loosely than

↔ does, and = binds tightly. The binding priority is the only difference between

=and ⇔ for formulas, but ⇔ and ↔ are quite different as can be seen from the

truth tables.

⇔•◦ ||
• •◦◦◦
◦ ◦•◦◦
|

⇒•◦ ||
• •◦◦◦
◦ ••••
|

••
◦◦
|

◦◦•◦ •◦•◦ ◦

◦◦◦• •◦◦• ◦

|| || ||

↔•◦ ||
••◦ ||
◦◦• ||
|

→•◦ ||
••◦ ||
◦ ••••
|

∼
•◦
◦•
|

•◦ • • •

| | | |

◦• • • •

|| || || || || || ||

We could try the following standard abbreviations:

?
→ ψ ≡¬ϕ ∨ ψ

?
↔ ψ ≡

?
→ ψ

?
→ ϕ

ϕ ϕ ( ϕ ) ∧ ( ψ )

?
→ ϕ

?
↔ ϕ

But here we have neither ϕ nor ϕ , since the diagonals differ from • at

indeterminacies.