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

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

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

•◦ ||
••◦ ||
◦◦•••
|

•◦ ||
••◦ ||
◦ ••••
|

••• ••••

• • •

|

| | | | |

••• ••••

• • •

|| || ||

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

We instead use the following abbreviations:

ϕ ψ ≡∼ϕ ∨ ψ ϕ ψ ≡ ( ϕ ψ ) ∧ ( ψ ϕ )

Although ϕ ψ does not entail ¬ψ ¬ϕ ,wedohave ϕ ϕ and ϕ ϕ ,and

this implication is very useful as we shall see in a moment.
We also use the predicate ∆ for determinacy and ∇ for indeterminacy with

the abbreviations (note that ∆ and ∇ are used for predicates and for sets of

truth codes):

∆ ϕ ≡ ( ϕ ∨¬ϕ ) ∇ϕ ≡¬ ∆ ϕ

∇
•◦
◦◦
|

∆
••
◦•
|

• ◦

• ◦

|| ||

We now come to the central abbreviations based directly on the semantic clause
above:

ϕ ↔ ψ ≡ ( ϕ = ψ ) ∧

( ϕ ψ ) ∧

( ψ ϕ ) ∧

( ¬ϕ ¬ψ ) ∧

¬ψ ¬ϕ ∧

( )

( ¬ ( ϕ = ψ ) ∧∇ϕ ∧∇ψ ⊥ )

ϕ ψ ∧ ¬ϕ ¬ψ ∧ ϕ ψ ∨ ϕ ∨ ψ ϕ ↔ ψ

We could also use ( ) ( ) ( = ∆ ∆ )for .

6 A Case Study - Continued

Recall that classical logic explodes in the presence of the formulas θ 0 ,θ 1 ,θ 2 ,θ 3

since θ 0 ,θ 1 ,θ 2 ,θ 3 entails any formula ϕ .In ∇ we have several counter-examples

as follows.
The reason why we do not have ( θ 0 ∧ θ 1 ∧ θ 2 ∧ θ 3 ) → J is that [[ L ]] = • ,

[[ is a counter-example. This can be seen from the truth tables -

the result is | which is not designated. The same counter-example also shows that
the system cannot conclude

I ]] =

| ,[

J ]] = ◦

¬L since [[ ¬L ]] = ◦ =[ J ]] and it cannot conclude J

as just explained.