Tableaus and Dual Tableaus

  • Melvin FittingEmail author
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)


In a sense, tableaus and dual tableaus are the same thing, just as tableaus and sequent calculi are the same thing. There are mathematical ideas, and there are presentations of them. For applications, representing linear operators as matrices is wonderfully helpful, but for proving results about linear operators a more abstract approach is simpler and clearer. The form of mathematical structures matters psychologically for people, though perhaps it matters little to the god of mathematics who kept Paul Erdős’s book of proofs. Tableaus work towards an obvious contradiction, dual tableaus work towards an obvious truth. Which is best? Who asks the question? That determines the answer. Here we examine the basics of tableaus and dual tableaus and their connections, looking only at the most fundamental of logics. That should be enough to make the general ideas plain.


Logic Intuitionistic logic Proof methods Tableau Dual tableau 


  1. Anellis, I. H. (1990). From semantic tableaux to Smullyan trees: A history of the development of the falsifiability tree method. Modern Logic, 1(1), 35–69.Google Scholar
  2. Beth, E. W. (1955). Semantic entailment and formal derivability. Mededelingen der Kon. Ned. Akad. v. Wet., 18, 13.Google Scholar
  3. Beth, E. W. (1956). Sematic construction of intuitionistic logic. Mededelingen der Kon. Ned. Akad. v. Wet., 19(11).Google Scholar
  4. Beth, E. W. (1959). The Foundations of Mathematics. Amsterdam: North-Holland. (Revised Edition 1964).Google Scholar
  5. Binkley, R. W. & Clark, R. L. (1967). A cancellation algorithm for elementary logic. Theoria, 33(2), 79–97.CrossRefGoogle Scholar
  6. D’Agostino, M., Gabbay, D., Hähnle, R., & Posegga, J. (Eds.). (1999). Handbook of Tableau Methods. Dordrecht: Kluwer.Google Scholar
  7. Dawson, J. & Goré, R. (2018). Machine-checked meta-theory of dual-tableaux for intuitionistic logic. In J. Golińska-Pilarek & M. Zawidzki (Eds.), Ewa Orłowska on Relational Methods in Logic and Computer Science (263–292). Outstanding Contributions to Logic. Berlin: Springer.Google Scholar
  8. Fitting, M. C. (1969). Intuitionistic Logic Model Theory and Forcing. Amsterdam: North-Holland Publishing Co.Google Scholar
  9. Fitting, M. C. (1983). Proof Methods for Modal and Intuitionistic Logics. Dordrecht: D. Reidel Publishing Co.CrossRefGoogle Scholar
  10. Gentzen, G. (1935). Untersuchungen über das logische schließen. Mathematische Zeitschrift, 39, 176–210, 405–431. (English translation as ‘Investigation into logical deduction’ in (Szabo, 1969, pp 68–131)).Google Scholar
  11. Hintikka, J. (1955). Form and content in quantification theory. Acta Philosophica Fennica, 8, 11–55.Google Scholar
  12. Indrzejczak, A. (2010). Natural Deduction, Hybrid Systems and Modal Logic. Trends in Logic. Berlin: Springer.CrossRefGoogle Scholar
  13. Lis, Z. (1960). Wynikanie semantyczne a wynikanie formalne (Logical consequence, semantic and formal). Studia Logica, 10, 39–60. (Polish, with Russian and English summaries).CrossRefGoogle Scholar
  14. Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34, 507–544.CrossRefGoogle Scholar
  15. Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.CrossRefGoogle Scholar
  16. Rasiowa, H. & Sikorski, R. (1960). On the Gentzen theorem. Fundamenta Mathematicae, 48, 57–69.CrossRefGoogle Scholar
  17. Smullyan, R. M. (1968). First-order Logic. Berlin: Springer. (Revised Edition, Dover Press, New York, 1994).CrossRefGoogle Scholar
  18. Snyder, D. P. (1971). Modal Logic and its Applications. New York: Van Nostrand.Google Scholar
  19. Szabo, M. E. (Ed.). (1969). The Collected Papers of Gerhard Gentzen. Amsterdam: North-Holland Publishing Co.Google Scholar
  20. Waaler, A. & Wallen, L. (1999). Tableaux for intuitionistic logics. In M. D’Agostino, D. M. Gabbay, R. Hähnle, & J. Posegga (Eds.), Handbook of Tableau Methods (pp. 255–296). Dordrecht: Springer.CrossRefGoogle Scholar
  21. Wang, H. (1960). Toward mechanical mathematics. IBM Journal for Research and Development, 4, 2–22. (Reprinted in Wang, H. (1963). A Survey of Mathematical Logic (pp. 224–268). Amsterdam: North-Holland).Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Department of Computer Science, Philosophy, MathematicsGraduate Center, City University of New YorkNew YorkUSA

Personalised recommendations