Abstract
In this paper we give an analytic tableau calculus P L 1 6 for a functionally complete extension of Shramko and Wansing’s logic. The calculus is based on signed formulas and a single set of tableau rules is involved in axiomatising each of the four entailment relations ⊧ t , ⊧ f , ⊧ i , and ⊧ under consideration—the differences only residing in initial assignments of signs to formulas. Proving that two sets of formulas are in one of the first three entailment relations will in general require developing four tableaux, while proving that they are in the ⊧ relation may require six.
Similar content being viewed by others
Notes
We use the terms ‘entailment relation’ and ‘consequence relation’ purely for convenience in the case of the information entailment relation ⊧ i . Strictly more correct perhaps would be ‘necessary approximation’, a term that was used in [19] for a ‘consequence’ relation based on Belnap’s A4 lattice.
This simplicity has a pay off because it is now very easy to implement the logic. Mainly for their own amusement and instruction the authors have written a simple theorem prover 16T A P, loosely based on (the propositional part of) Beckert & Posegga’s [2] lean T A P marvel. It similarly exploits Prolog’s left-to-right depth-first evaluation mechanism, but the code unfortunately is far less concise than Beckert & Posegga’s.
References
Baaz, M., Fermüller, C., Zach, R. (1994). Elimination of cuts in first-order finite-valued logics. Journal of Information Processing and Cybernetics, 29, 333–355.
Beckert, B., & Posegga, J. (1995). lean T A P: Lean Tableau-based deduction. Journal of Automated Reasoning, 15 (3), 339–358. http://web.sec.uni-passau.de/papers/LeanTaP.pdf.
Belnap, N.D. (1976). How a computer should think. In G. Ryle (Ed.), Contemporary aspects of philosophy (pp. 30–56). Stocksfield: Oriel Press.
Belnap, N.D. (1977). A useful four-valued logic. In J. Dunn, & G. Epstein (Eds.), Modern uses of multiple-valued logic (pp. 8–37). Dordrecht: Reidel.
Kamide, N., & Wansing, H. (2009). Sequent calculi for some trilattice logics. The Review of Symbolic Logic, 2(2), 374–395.
Langholm, T. (1996). How different is partial logic? In P. Doherty (Ed.), Partiality, modality, and nonmonotonicity (pp. 3–43). Stanford: CSLI.
Muskens, R.A. (1995). Meaning and partiality. Stanford: CSLI.
Muskens, R.A. (1999). On partial and paraconsistent logics. Notre Dame Journal of Formal Logic, 40(3), 352–374.
Odintsov, S. (2009). On Axiomatizing Shramko-Wansing’s logic. Studia Logica, 91, 407–428.
Odintsov, S., & Wansing, H. (2014). The logic of generalized truth values and the logic of bilattices. In Studia Logica.
Rivieccio, U. (2013). Representation of interlaced trilattices. Journal of Applied Logic, 11, 174–189.
Rousseau, G. (1967). Sequents in many-valued logic I. Fundamenta Mathematicae, 60, 23–33.
Schröter, K. (1955). Methoden zur Axiomatisierung beliebiger Aussagen- und Prädikatenkalküle. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 1, 241–251.
Shramko, Y., & Wansing, H. (2005). Some Useful 16-Valued Logics: How a Computer Network Should Think. Journal of Philosophical Logic, 34, 121–153.
Shramko, Y., & Wansing, H. (2011). Truth and falsehood: An inquiry into generalized logical values. In Trends in logic Vol. 36: Springer.
Wansing, H. (2009). The power of Belnap: Sequent systems for S I X T E E N 3. Journal of Philosophical Logic, 39, 369–393.
Wansing, H. (2012). A non-inferentialist, anti-realistic conception of logical truth and falsity. Topoi, 31, 93–100.
Wansing, H., & Kamide, N. (2010). Intuitionistic Trilattice Logics. Journal of Logic and Computation, 20 (6), 1201–1229.
Wintein, S., & Muskens, R.A. (2012). A calculus for Belnap’s logic in which each proof consists of two trees. Logique & Analyse, 220, 643–656.
Wintein, S., & Muskens, R.A. (2014). From bi-facial truth to bi-facial proofs. Studia Logica. Online First.
Zach, R. (1993). Proof theory of finite-valued logics. Technical Report TUW-E185.2-Z.1-93. Institut für Computersprachen, Technische Universität Wien.
Acknowledgments
We would like to thank the referee for encouraging words and helpful comments. Stefan Wintein wants to thank the Netherlands Organisation for Scientific Research (NWO) for funding the project The Structure of Reality and the Reality of Structure (project leader: F. A. Muller), in which he is employed. Reinhard Muskens gratefully acknowledges NWO’s funding of his project 360-80-050, Towards Logics that Model Natural Reasoning.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Muskens, R., Wintein, S. Analytic Tableaux for all of SIXTEEN 3 . J Philos Logic 44, 473–487 (2015). https://doi.org/10.1007/s10992-014-9337-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-014-9337-3