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

A Paraconsistent Higher Order Logic

Jørgen Villadsen

Computer Science, Roskilde University
Building 42.1, DK-4000 Roskilde, Denmark
[e-mail]

Abstract. Classical logic predicts that everything (thus nothing useful
at all) follows from inconsistency. A paraconsistent logic is a logic where
an inconsistency does not lead to such an explosion, and since in practice
consistency is dicult to achieve there are many potential applications
of paraconsistent logics in knowledge-based systems, logical semantics of
natural language, etc.
Higher order logics have the advantages of being expressive and with
several automated theorem provers available.Alsothetypesystemcan
be helpful.
We present a concise description of a paraconsistent higher order logic
with countably infinite indeterminacy, where each basic formula can get
its own indeterminate truth value. The meaning of the logical operators
is new and rather different from traditional many-valued logics as well
as from logics based on bilattices. Thus we try to build a bridge between
the communities of higher order logic and many-valued logic.
A case study is studied and a sequent calculus is proposed based on
recent work by Muskens.

Many non-classical logics are, at the propositional level, funny toys which work
quite good, but when one wants to extend them to higher levels to get a real
logic that would enable one to do mathematics or other more sophisticated
reasonings, sometimes dramatic troubles appear.
J.-Y. Beziau: The Future of Paraconsistent Logic
Logical Studies Online Journal 2 (1999) p. 7

A preliminary version appeared in the informal proceedings of the workshop
on Paraconsistent Computational Logic PCL 2002 (editors Hendrik Decker,
Jørgen Villadsen, Toshiharu Waragai) http://www.ruc.dk/ ~ jv/pcl.pdf

1 Introduction

Classical logic predicts that everything (thus nothing useful at all) follows from
inconsistency. A paraconsistent logic is a logic where an inconsistency does not
lead to such an explosion.
In a paraconsistent logic the meaning of some of the logical operators must
be different from classical logic in order to block the explosion, and since there

This research was partly sponsored by the IT University of Copenhagen.