Information Technology Reference
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 , LEO , HOL,
PVS, IMPS, and Isabelle (see  for further references). It should be possible
to modify some of these to our paraconsistent logic; in particular the generic
theorem prover Isabelle  already implements several object logics.
We are inspired by the notion of indeterminacy as discussed by Evans .
Even though the higher order logic
is paraconsistent some of its extensions,
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 . In the sequent
as a conjunction of a set of formulas and
as a disjunction of a set of formulas.
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
Θ, ω Γ
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
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
introduce the primitives of the paraconsistent higher order logic
the modality and implications available. Finally we present a sequent calculus
and the extensions
∇ ω ,
∇ ∆ ,
∇ † and
∇ ‡ .
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