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

and the clause [[ ]] = • are omitted; further clauses are discussed later). Also

ϕ ⇔¬¬ϕ is considered to be a key equality as well.

• if [[ ϕ ]] = ◦ ⇔⊥

[[ ¬ϕ ]] = ◦ if [[ ϕ ]] = • ⊥⇔¬

[[ ϕ ]] o t h e r w i s e

[[ ϕ ]] i f [[ ϕ ]] = [[ ψ ]] ϕ ⇔ ϕ ∧ ϕ

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

[[ ϕ ∧ ψ ]] =

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

◦ otherwise

In the semantic clauses several cases may apply if and only if they agree on the
result. The semantic clauses work for classical logic and also for our logic.
We have the following standard abbreviations:

⊥≡¬ ϕ ∨ ψ ≡¬ ( ¬ϕ ∧¬ψ ) ∃υ.ϕ ≡¬∀υ.¬ϕ

The universal quantification will be introduced later (as a kind of general-

ized conjunction). A suitable abbreviation for

∀υ.ϕ

is also provided later.
As explained we have an infinite number of truth values (truth codes) in gen-
eral, but the special cases of three-valued and four-valued logics are interesting
too. In order to investigate finite truth tables we first add just [[ † ]] = as an

|

indeterminacy. We do not have ϕ ∨¬ϕ . Unfortunately we do have that ϕ ∧¬ϕ

entails ψ ∨¬ψ (try with • , ◦ and | using the truth tables and use the fact that

any entails itself). The reason for this problem is that in a sense there is not

only a single indeterminacy, but a unique one for each basic formula.
However, in many situations only two indeterminacies are ever needed, corre-
sponding to the left and right hand side of the implication. Hence we add [[

ϕ

‡ ]] =

||

as the alternative indeterminacy.

∧•◦ ||
••◦ ||
◦ ◦◦◦◦
|

∨•◦ ||
• ••••
◦•◦ ||
|

¬
•◦
◦•
|

◦ ◦ • •

| | | | |

◦◦ || • •

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

Keep in mind that truth tables are never taken as basic - they are simply
calculated from the semantic clauses taking into account also the abbreviations.

5 Implication, Biimplication, and Modality

As for conjunction and negation the motivation for the biimplication operator
↔ as defined later) is based on the few key

equalities shown to the right of the following semantic clause.

(and the implication operator →