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

The system cannot conclude L (take [[ L ]] = ◦ ,[ I ]] = ◦ ,[ J ]] =

| as a counter-

example) and neither ]] = | in both cases).

There is quite some flexibility with respect to the formalization - as an ex-
ample we consider changing

I nor ¬I (take [[ L ]] =

| ,[

I ]] =

|| ,[

J

where the logical necessity operator
expresses that the fact is “really” true. Now the previous counter-example to

θ 0 to

¬J

L
is no good and since it can be shown that there is no other counter-example, the
system concludes ). Recall that

classical logic is useless in this case study. The previous counter-example to

L (it also concludes ¬I , and of course still ¬J

¬L

J L I ◦ J ◦ I

and is ok, and there is a counter-example [[ ]] = | ,[ ]] = ,[ ]] = to .

∇

is inconsistency-tolerant
in an interesting way, but of course further investigations are needed to clarify
the potential.

We think that the case study shows that the logic

7ASequentC culus

We base the paraconsistent higher order logic ∇ on the (simply) typed λ -calculus

λ

[10] (see also [7], especially for the untyped -calculus and for the notion of

combinators which we use later).
Classical higher-order logic is often built from a very few primitives, say
equality = and the selection operator

as in Q 0 [4], but it does not seem like
we can avoid taking, say, negation, conjunction and universal quantification as
primitives for

ı

∇ . Also we prefer to extend the selection operator ı to the (global)

choice operator described later.

We use the following well-known abbreviations in order to replace negation
and conjunction by joint denial (also known as Sheffer's stroke):

ε

¬ϕ ≡ ϕ|ϕ ϕ ∧ ψ ≡¬ ( ϕ|ψ )

We also have a so-called indeterminacy generation operator ∂ as a primitive. We
use the following abbreviations:
ϕ ≡¬ϕ

ϕ ≡ ∂ ϕ ϕ ≡ ∂ ˙ ϕ ...

˙ ¨

The indeterminacy generation operator is injective and we can use it for the
natural numbers. We say much more about it later.
The truth tables in case of four truth values are the following.

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

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

=

∂
••
◦

|

• • ◦◦•◦

| | | ||

•• || ◦◦◦• ◦

|| || || ||

The truth table only displays equality = between formulas (the biimplication
operator

⇔ ), but it is applicable to any type. We have the abbreviation:

≡ ( λ x.x )=( λ x.x )

Here λ x.x is the identity function in the λ -calculus (any type for x will do).