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

are many ways to change the meaning of these operators there are many dif-
ferent paraconsistent logics. We present a paraconsistent higher order logic ∇

based on the (simply) typed -calculus [10, 4]. Although it is a generalization

of Lukasiewicz's three-valued logic the meaning of the logical operators is new.
The results extend the three-valued and four-valued logics first presented in [19,
20] to infinite-valued logics.
One advantage of a higher order logic is that the logic is very expressive in the
sense that most mathematical structures, functions and relations are available
(for instance arithmetic). Another advantage is that there are several automated
theorem provers for classical higher order logic, e.g. TPS [5], LEO [9], HOL,
PVS, IMPS, and Isabelle (see [23] for further references). It should be possible
to modify some of these to our paraconsistent logic; in particular the generic
theorem prover Isabelle [18] already implements several object logics.
We are inspired by the notion of indeterminacy as discussed by Evans [11].
Even though the higher order logic

λ

∇ is paraconsistent some of its extensions,

like and ∆ later for related purposes.

We also propose a sequent calculus for the paraconsistent higher order logic

∇ ∆ , are classical. We reuse the symbols ∇

∇

based on the seminal work by Muskens [17]. In the sequent Θ Γ we understand

Θ as a conjunction of a set of formulas and Γ as a disjunction of a set of formulas.

We use is an axiom which provides

countably infinite indeterminacy such that each basic formula can get its own
indeterminate truth value (or as we prefer: truth code).
As mentioned above higher order logic includes much, if not all, of ordinary
mathematics, and even though

Θ Γ as a shorthand for Θ, ω Γ ,where ω

is paraconsistent we can use it for classical
mathematics by keeping the truth values determinate. Hence we shall not con-
sider here paraconsistent mathematics. Using the standard foundation of math-
ematics (axiomatic set theory) it is possible to show that

∇

is consistent.
The essential point is that the higher-order issues and many-valued issues
complement each other in the present framework:

∇

- On the one hand we can view ∇ as a paraconsistent many-valued extension

of classical higher order logic.

- On the other hand we can view as a paraconsistent many-valued proposi-

tional logic with features from classical higher order logic.

∇

First we introduce a case study and motivate our definitions of the logical
operators. Then we describe the syntax and semantics of the typed

λ -calculus and

introduce the primitives of the paraconsistent higher order logic ,inparticular

the modality and implications available. Finally we present a sequent calculus
for

∇

∇ and the extensions ∇ ω , ∇ ∆ , ∇ † and ∇ ‡ .

2 A Case Study

Higher order logic is not really needed for the case study - propositional logic is
enough - but the purpose of the case study is mainly to illustrate the working