Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-16T15:26:21.752Z Has data issue: false hasContentIssue false

Natural 3-valued logics—characterization and proof theory

Published online by Cambridge University Press:  12 March 2014

Arnon Avron*
Affiliation:
School of Mathematical Sciences, Raymond and Beverly Sackler Faculty of Exact Sciences, Tel Aviv University, Ramat-Aviv, Tel Aviv 69978, Israel

Extract

Many-valued logics in general and 3-valued logic in particular is an old subject which had its beginning in the work of Łukasiewicz [Łuk]. Recently there is a revived interest in this topic, both for its own sake (see, for example, [Ho]), and also because of its potential applications in several areas of computer science, such as proving correctness of programs [Jo], knowledge bases [CP] and artificial intelligence [Tu]. There are, however, a huge number of 3-valued systems which logicians have studied throughout the years. The motivation behind them and their properties are not always clear, and their proof theory is frequently not well developed. This state of affairs makes both the use of 3-valued logics and doing fruitful research on them rather difficult.

Our first goal in this work is, accordingly, to identify and characterize a class of 3-valued logics which might be called natural. For this we use the general framework for characterizing and investigating logics which we have developed in [Av1]. Not many 3-valued logics appear as natural within this framework, but it turns out that those that do include some of the best known ones. These include the 3-valued logics of Łukasiewicz, Kleene and Sobociński, the logic LPF used in the VDM project, the logic RM3 from the relevance family and the paraconsistent 3-valued logic of [dCA]. Our presentation provides justifications for the introduction of certain connectives in these logics which are often regarded as ad hoc. It also shows that they are all closely related to each other. It is shown, for example, that Łukasiewicz 3-valued logic and RM3 (the strongest logic in the family of relevance logics) are in a strong sense dual to each other, and that both are derivable by the same general construction from, respectively, Kleene 3-valued logic and the 3-valued paraconsistent logic.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1991

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[AB] Anderson, A. R. and Belnap, N. D., Entailment, Vol. 1, Princeton University Press, Princeton, New Jersey, 1975.Google Scholar
[Av1] Avron, A., Simple consequence relations, LFCS Report Series ECS-LFCS-87-30, Laboratory for the Foundations of Computer Science, Edinburgh University, Edinburgh, 1987; Information and Computation (to appear).Google Scholar
[Av2] Avron, A., The semantics and proof theory of linear logic, Theoretical Computer Science, vol. 57 (1988 ), pp. 161184.CrossRefGoogle Scholar
[Av3] Avron, A., On an implication connective of RM, Notre Dame Journal of Formal Logic, vol. 27 (1986), pp. 201209.CrossRefGoogle Scholar
[Av4] Avron, A., The semantics and proof theory of relevance logics and non-trivial theories containing contradictions, Thesis, School of Mathematical Sciences, Tel-Aviv University, Tel-Aviv, 1984.Google Scholar
[Av5] Avron, A., A constructive analysis of RM, this Journal, vol. 52 (1987), pp. 939951.Google Scholar
[Av6] Avron, A., Relevant entailment: semantics and formal systems, this Journal, vol. 49 (1984), pp. 334342.Google Scholar
[BCJ] Barringer, H., Cheng, J. H., and Jones, C. B., A logic covering undefinedness in program proofs, Acta Informatica, vol. 21 (1984), pp. 251269.CrossRefGoogle Scholar
[Be1] Belnap, N. D., How a computer should think, Contemporary aspects of philosophy (Ryle, G., editor), Oriel Press, Stocksfield, England, 1977, pp. 3056.Google Scholar
[Be2] Belnap, N. D., A useful four-valued logic, Modern uses of multiple-valued logic (Epstein, G. and Dunn, J. M., editors), Reidel, Dordrecht, 1977, pp. 837.Google Scholar
[Car] Carnielli, W. A., Systematization of finite many-valued logics through the method of tableaux, this Journal, vol. 52 (1987), pp. 473493.Google Scholar
[CP] Colmerauer, A. and Pique, J. F., About natural logic, Advances in data base theory, Vol. I (Gallaire, H.et al., editors), Plenum Press, New York, 1981, pp. 343365.CrossRefGoogle Scholar
[dC] da Costa, N. C. A., Theory of inconsistent formal systems, Notre Dame Journal of Formal Logic, vol. 15(1974), pp. 497510.CrossRefGoogle Scholar
[dCA] da Costa, N. C. A. and Alves, E. H., Relations between paraconsistent logics and many-valued logic, Polish Academy of Sciences. Institute of Philosophy and Sociology. Bulletin of the Section of Logic, vol. 10(1981), pp. 185191.Google Scholar
[Du] Dunn, J. M., Relevance logic and entailment, Handbook of philosophical logic, Vol. III (Gabbay, D. and Guenthner, F., editors), Reidel, Dordrecht, 1984, pp. 117224.Google Scholar
[Ep] Epstein, R. L., The semantic foundations of logic. Vol. I: Propositional logics (to appear).Google Scholar
[Gi] Girard, J. Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1101.CrossRefGoogle Scholar
[Ho] Hodes, H., Three-valued logics: an introduction, a comparison of various logical lexica, and some philosophical remarks, Annals of Pure and Applied Logic, vol. 43 (1989), pp. 99145.CrossRefGoogle Scholar
[Jo] Jones, C. B., Systematic software development using VDM, Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar
[Łuk] Łukasiewicz, J., On 3-valued logic, Ruch Filosoficzny, vol. 5 (1920), pp. 169171; English translation, Polish logic 1920–1939 (S. McCall, editor), Oxford University Press, Oxford, 1967, pp. 15–18.Google Scholar
[MM] McCall, S. and Meyer, R. K., Pure three-valued Łukasiewiczian implication, this Journal, vol. 31 (1966), pp. 399405.Google Scholar
[Mo] Monteiro, A., Construction des algèbres de Łukasiewicz trivalentes dans les algèbres de Boole monadiques. I, Mathematica Japonka, vol. 12 (1967), pp. 123.Google Scholar
[OdC] D'Ottaviano, I. M. L. and da Costa, N. C., Sur un problème de Jaśkowski, Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, Série A, vol. 270 (1970), pp. 13491353.Google Scholar
[Pot] Pottinger, G., Uniform, cut-free formulations of T, S4 and S5 (abstract), this Journal, vol. 48 (1983), p. 900.Google Scholar
[Sc1] Scott, D., Rules and derived rules, Logical theory and semantical analysis (Stenlund, S., editor), Reidel, Dordrecht, 1974, pp. 147161.CrossRefGoogle Scholar
[Sc2] Scott, D., Completeness and axiomatizability in many-valued logic, Proceeding of the Tarski symposium, Proceeding of Symposia in Pure Mathematics, vol. 25, American Mathematical Society, Providence, Rhode Island, 1974, pp. 411435.CrossRefGoogle Scholar
[Sch] Schröter, K., Methoden zur Axiomatisierung beliebiger Aussagen- und Prädikatenkalküle, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 1 (1955), pp. 241251.CrossRefGoogle Scholar
[Se] Sette, A. M., On the propositional calculus p1, Mathematica Japonica, vol. 16(1973), pp. 173180.Google Scholar
[Sob] Sobociński, B., Axiomatization of a partial system of three-value calculus of propositions, Journal of Computing Systems, vol. 1 (1952), pp. 2355.Google Scholar
[Tu] Turner, R., Logics for artificial intelligence, Ellis Horwood Ltd., Chichester, 1984.Google Scholar
[Ur] Urquhart, A., Many-valued logic, Handbook of philosophical logic, Vol. III (Gabbay, D. and Guenthner, F., editors), Reidel, Dordrecht, 1984, pp. 71116.Google Scholar
[Wa] Wajsberg, M., Axiomatization of the 3-valued propositional calculus, Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie, Classe III, vol. 24 (1931), pp. 126148; English translation, Polish logic 1920–1939 (S. McCall, editor), Oxford University Press, Oxford, 1967, pp. 264–284.Google Scholar
[Wó] Wójcicki, R., Lectures on propositional calculi, Ossolineum, Warsaw, 1984.Google Scholar