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

7.11 Other Logics

In order to investigate finite truth tables, namely the three-valued and four-
valued logics discussed in previous sections, we have the following abbreviations:

˙ ¨

†≡ ⊥‡ ≡ ⊥

We get the four-valued logic ∇ ‡ by adding the following axiom to ∇ :

∆ x ∨ x = †∨x = ‡

Likewise we get the three-valued logic ∇ † by adding the following axiom to ∇ :

∆ x ∨ x = †

But here ‡ = ⊥ due to the injection property of the indeterminacy generation.

8 Conclusions and Future Work

We have proposed a paraconsistent higher order logic ∇ ω with countably infinite

indeterminacy and described a case study (see [20, 22] for further applications).
We have presented a sequent calculus for the paraconsistent logic ∇ and

thesimpleaxiom ω turning ∇ into the ∇ ω that can serve as a foundation of

mathematics. Another axiom ∆ turns ∇ into the classical logic ∇ ∆ . We would like

to emphasize that it is not at all obvious how to get from ∇ ∆ to ∇ when the usual

axiomatics and semantics of ∇ ∆ do not deal with the axiom ∆ separately as we

do here. Corresponding to the proof-theoretical we have the model-theoretical

based on the type universes, and soundness and completeness results are to
be investigated (the latter with respect to general models of

∇

only).
We also intend to compare the paraconsistent higher order logic

∇ ω

with

work on multi-valued higher order resolution [15].

References

1. A. R. Anderson and N. D. Belnap Jr. Entailment: The Logic of Relevance and
Necessity . Princeton University Press, 1975.
2. P. B. Andrews. A reduction of the axioms for the theory of propositional types.
Fundamenta Mathematicae , 52:345-350, 1963.
3. P. B. Andrews. A Transfinite Type Theory with Type Variables . North-Holland,
1965.
4. P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth
through Proof . Academic Press, 1986.
5. P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. TPS: A
theorem proving system for classical type theory. Journal of Automated Reasoning ,
16:321-353, 1996.
6. O. Arieli and A. Avron. Bilattices and paraconsistency. In D. Batens, C. Morten-
sen, G. Priest, and J. Van-Bengedem, editors, Frontiers in Paraconsistent Logic ,
pages 11-27. Research Studies Press, 2000.