Information Technology Reference
InDepth Information
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 threevalued logic the meaning of the logical operators is new.
The results extend the threevalued and fourvalued logics first presented in [19,
20] to infinitevalued 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 higherorder issues and manyvalued issues
complement each other in the present framework:
∇

On the one hand we can view
∇
as a paraconsistent manyvalued extension
of classical higher order logic.

On the other hand we can view
as a paraconsistent manyvalued 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
Search WWH ::
Custom Search