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

of the paraconsistency. The features of first order logic and higher order logic,
including mathematical concepts, seem necessary in general.
Imagine a system that collects information on the internet - say, from news
media - about the following scenario: Agent X thinks that his supervisor hides a
secret that the public ought to know about. For simplicity we ignore all temporal
aspects and take all reports to be in present tense. We also do not take into
account a more elaborate treatment of conditionals / counterfactuals.
Assume that the following pieces of information are available:
#123 If X leaks the secret then he keeps his integrity.
#456 If X does not leak the secret then he keeps his job.
#789 If X does not keep his job then he does not keep his integrity.
#1000 X does not keep his job.
The numbers indicate that the information is collected over time and perhaps
from various sources.
Classically the information available to the system is inconsistent. This is
not entirely obvious, especially not when numerous other pieces of information
are also available to the system and when the system is operating under time
constraints. Note that the information consists of both simple facts (#1000) as
well as rules (#123, #456, #789). A straightforward formalization is as follows:

L → I θ 1

¬L → J θ 2

¬J →¬I θ 3

¬J θ 0

Here the propositional symbol L means that X leaks the secret, I that X keeps his

integrity, and J that X keeps his job. As usual → is implication, ∧ is conjunction,

and is negation.

If we use classical logic on the formulas

¬

θ 0 ,θ 1 ,θ 2 ,θ 3 the system can conclude

L , and whatever other fact or rule considered. Of course

we might try to revise the information

, ¬L , I , ¬I , J , ¬J

θ 0 ,θ 1 ,θ 2 ,θ 3 , but it is not immediately
clear what would be appropriate. In the present paper we propose to use a
paraconsistent logic ∇ such that the system can conclude only ¬J or θ 0 ,which

is reasonable (the logic ∇ is monotonic and any formula ϕ entails itself).

is an extension of classical logic in the sense that
classical reasoning is easily possible, just add the special formulas ∆

The paraconsistent logic ∇

L ,∆ I ,and

∆ behave classically.

We now turn to the motivation of the logical operators, which are to be
defined using so-called key equalities. We return to the case study in section 6.

J to the formulas θ 0 ,θ 1 ,θ 2 ,θ 3 and L , I ,and J

3 Overall Motivation

Classical logic has two truth values, namely • and ◦ (truth and falsehood), and

the designated truth value • yields the logical truths. We use the symbol for