Natural Deduction for Equality: The Missing Entity

  • Ruy J. G. B. de QueirozEmail author
  • Anjolina G. de Oliveira
Part of the Trends in Logic book series (TREN, volume 39)


The conception of the very first decision procedures for first-order sentences brought about the need for giving citizenship to function symbols (e.g. Skolem functions). We argue that a closer look at proof procedures for first-order sentences with equality brings about the need for introducing (function) symbols for rewrites. This is appropriately done via the framework of labelled natural deduction which allows to formulate a proof theory for the “logical connective” of propositional equality. The basic idea is that when analysing an equality sentence into (i) proof conditions (introduction) and (ii) immediate consequences (elimination), it becomes clear that we need to bring in identifiers (i.e. function symbols) for sequences of rewrites, and this is what we claim is the missing entity in P. Martin-Löf’s equality types (both intensional and extensional). What we end up with is a formulation of what appears to be a middle ground solution to the ‘intensional’ versus ‘extensional’ dichotomy which permeates most of the work on characterizing propositional equality in natural deduction style. (Part of this material was presented at the Logical Methods in the Humanities Seminar, Stanford University, and the authors would like to thank Solomon Feferman and Grigori Mints for their comments and suggestions.)


Natural deduction Equality Labelled deduction  Equality type 


  1. 1.
    Aczel, P. H. G. (1980). Frege structures and the notions of proposition, truth and set. in J. Barwise, H.-J. Keisler, & K. Kunen (Eds.), The Kleene Symposium, Vol. 101 of Studies in logic and the foundations of mathematics (pp. 31–59). Amsterdam: North-Holland Publishing Co. (xx+425pp, 1980. Proceedings of the Symposium held in June 18–24).Google Scholar
  2. 2.
    Aczel, P. H. G. (1991). Term declaration logic and generalised composita. In Sixth Annual IEEE Symposium on Logic in Computer Science ( LICS’91) (pp. 22–30). Amsterdam: IEEE Press. Proceedings of the Symposium held July 15–18, in Amsterdam, The Netherlands.Google Scholar
  3. 3.
    Barendregt, H.P. (1984). The lambda calculus, its syntax and semantics, volume 103 of studies in logic and the foundation of mathematics. Amsterdam: North-Holland (revised edition).Google Scholar
  4. 4.
    Bishop, E. (1967). Foundations of constructive analysis. McGraw-Hill series in Higher Mathematics (xiv+371pp). New York: McGraw-Hill Book Company.Google Scholar
  5. 5.
    Chenadec, Ph. Le. (1989). On the logic of unification. Journal of Symbolic Computation, 8(1 and 2), 141–199.Google Scholar
  6. 6.
    Dummett, M. (1973). Frege: Philosophy of language (xliii+708pp, 2nd (1981) ed.). London: Duckworth.Google Scholar
  7. 7.
    Dummett, M. (1991). Frege: Philosophy of mathematics (xiii+331pp). London: Duckworth.Google Scholar
  8. 8.
    Frege, G. (1891).Funktion und Begriff. Proceedings of the Jena Medical and Scientific Society.Google Scholar
  9. 9.
    Frege G. (1893). Grundgesetze der Arithmetik. Begriffsschriftlich abgeleitet. I. Jena: Verlag von Hermann Pohle. Reprinted in volume 32 of Olms Paperbacks, Georg Olms Verlagsbuchhandlung, Hildesheim, XXXII+254pp. Partial English translation in [11].Google Scholar
  10. 10.
    Furth M. (1964). The basic laws of arithmetic. Exposition of the system (lxiv+143pp). Berkeley: University of California Press. Partial English translation of Gottlob Frege’s Grundgesetze der Arithmetik.Google Scholar
  11. 11.
    Gabbay, D. M. (1996). Labelled deductive systems. Volume I: Foundations. Oxford: Oxford University Press.Google Scholar
  12. 12.
    Gabbay, D. M., & de Queiroz, R. J. G. B. (1992). Extending the Curry-Howard interpretation to linear, relevant and other resource logics. The Journal of Simbolic Logic, 57(4), 1319–1365.CrossRefGoogle Scholar
  13. 13.
    Girard, J.-Y. (1987). Proof theory and logical complexity. Volume I of studies in proof theory (503 pp). Napoli: Bibliopolis.Google Scholar
  14. 14.
    Hilbert, D., & Bernays, P. (1934). Grundlagen der Mathematik I, volume XL of Die Grundlehren der mathematischen Wissenschaften (XII+471pp). Berlin: Verlag von Julius Springer.Google Scholar
  15. 15.
    Hilbert, D., & Bernays, P. (1939). Grundlagen der Mathematik II, volume L of Die Grundlehren der mathematischen Wissenschaften (XII+498pp). Berlin: Verlag von Julius Springer.Google Scholar
  16. 16.
    Hindley, J. R., & Seldin, J. P. (1986). Introduction to combinators and \(\lambda \) -Calculus. Cambridge: London Mathematical Society Student Texts: Cambridge University Press.Google Scholar
  17. 17.
    Howard, W. A. (1980). The formulae-as-types notion of construction. In J. R. Seldin & J. R. Hindley (Eds.), To H. B. Curry: Essays on combinatory logic lambda calculus and formalism (xxv+606pp). London: Academic Press.Google Scholar
  18. 18.
    Kleene, S. C. (1967). Mathematical logic. New York: Wiley Interscience.Google Scholar
  19. 19.
    Kreisel, G., & Tait, W. (1961). Finite definability of number theoretic functions and parametric completeness of equational calculi. Zeitschr. f Math. Logik und Grundlagen d. Math, 7, 28–38.CrossRefGoogle Scholar
  20. 20.
    Leisenring, A. C. (1969). Mathematical logic and Hilbert’s \(\varepsilon \) -Symbol, A volume of University Mathematical Series (ix+142pp). London: MacDonald Technical and Scientific.Google Scholar
  21. 21.
    Martin-Löf, P. (1975). About models for intuitionistic type theories and the notion of definitional equality. In S. Kanger (Ed.), Proceedings of the third Scandinavian logic symposium, Series studies in logic and the foundations of mathematics (pp. 81–109). Amsterdam: North-Holland.Google Scholar
  22. 22.
    Martin-Löf, P. (1975a). An intuitionistic theory of types: Predicative part. in H. E. Rose & J. C. Shepherdson (Eds.), Logic Colloquium ’73, Vol. 80 of studies in logic and the foundations of mathematics (pp. 73–118, viii+513pp). Amsterdam: North-Holland.Google Scholar
  23. 23.
    Martin-Löf, P. (1982). Constructive mathematics and computer programming. In L. J. Cohen, J. Łos, H. Pfeiffer, & K.-P. Podewski (Eds.), Logic, methodology and philosophy of science VI, Series studies in logic and the foundations of mathematics (pp. 153–175, xiii+738pp). Amsterdam: North-Holland.Google Scholar
  24. 24.
    Martin-Löf, P. (1984). Intuitionistic type theory. Series studies in proof theory (iv+91pp). Bibliopolis Naples. Notes by Giovanni Sambi of a series of lectures given in Padova, June.Google Scholar
  25. 25.
    Mitchell, J. C., & Scedrov, A. (1993). Notes on sconing and relators. In E. Boerger, et al. (Eds.), Computer science logic ’92, Selected Papers (pp. 352–378). Springer LNCS 702.Google Scholar
  26. 26.
    Montague, R. (1970). Universal grammar. Theoria, 36, 373–398.CrossRefGoogle Scholar
  27. 27.
    Nordström, B., Petersson, K., & Smith, J. M. (1990). Programming in Martin-Löf’s type theory. An introduction, Vol. 7 of The International Series of Monographs on Computer Science (x+221pp). Oxford: Clarendon Press.Google Scholar
  28. 28.
    de Oliveira, A. G. (1995). Proof transformations for labelled natural deduction via term rewriting (In Portuguese). Master’s thesis, Depto. de Informática, Universidade Federal de Pernambuco, C.P. 7851, Recife, PE 50732–970, Brasil.Google Scholar
  29. 29.
    de Oliveira, A. G., & de Queiroz, R. J. G. B. (1994). Term rewriting systems with labelled deductive systems. In Proceedings of Brazilian symposium on artificial intelligence (SBIA’94), Lecture Notes in Artificial Intelligence, Springer, pp. 59–72.Google Scholar
  30. 30.
    de Oliveira, A. G., & de Queiroz, R. J. G. B. (1999). A normalization procedure for the equational fragment of labelled natural deduction. Logic Journal of the Interest Group in Pure and Applied Logics, 7(2), 173–215.Google Scholar
  31. 31.
    de Oliveira, A. G., & de Queiroz, R. J. G. B. (2005). A new basic set of proof transformations. In S. Artemov, H. Barringer, A. Garcez, L. Lamb, & J. Woods (Eds.), We will show them! Essays in Honour of Dov Gabbay (Vol. 2, pp. 499-528). London: College Publications. ISBN 1904987125.Google Scholar
  32. 32.
    de Queiroz, R. J. G. B. (1988). A proof-theoretic account of programming and the rôle of reduction rules. Dialectica, 42(4), 265–282.CrossRefGoogle Scholar
  33. 33.
    de Queiroz, R. J. G. B. (1989). The mathematical language and its semantics: To show the consequences of a proposition is to give its meaning. In P. Weingartner & G. Schurz (Eds.), Reports of the thirteenth international Wittgenstein symposium, volume 18 of Schriftenreihe der Wittgenstein-Gesellschaft (pp. 259–266). Austria: Hölder-Pichler-Tempsky. Symposium held in Kirchberg/Wechsel.Google Scholar
  34. 34.
    de Queiroz, R. J. G. B. (1991). Meaning as grammar plus consequences. Dialectica, 45(1), 83–86.CrossRefGoogle Scholar
  35. 35.
    de Queiroz, R. J. G. B. (1992). Grundgesetze alongside Begriffsschrift. In Abstracts of Fifteenth International Wittgenstein, Symposium. pp. 15–16.Google Scholar
  36. 36.
    de Queiroz, R. J. G. B. (1994). Normalisation and language-games. Dialectica, 48(2), 83–125.CrossRefGoogle Scholar
  37. 37.
    de Queiroz, R. J. G. B. (2001). Meaning, function, purpose, usefulness, consequences—interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5), 693–734.Google Scholar
  38. 38.
    de Queiroz, R. J. G. B., & Gabbay, D. M. (1994). Equality in labelled deductive systems and the functional interpretation of propositional equality. In P. Dekker & M. Stokhof (Eds.), Proceedings of the 9th Amsterdam Colloquium (pp. 547–546)Google Scholar
  39. 39.
    de Queiroz, R. J. G. B., & Gabbay, D. M. (1993). The functional interpretation of the existential quantifier. Bulletin of the Interest Group in Pure and Applied Logics, 3(2 and 3), 243–290.Google Scholar
  40. 40.
    de Queiroz, R. J. G. B., & Gabbay, D. M. (1997). The functional interpretation of modal necessity. In de Rijke, Maarten (Ed.), Advances in intensional logic (Applied logic series) ( pp. 61–91). Dordrecht: Kluwer Academic Publishers.Google Scholar
  41. 41.
    de Queiroz, R. J. G. B., & Gabbay, D. M. (1999). Labelled natural deduction. In H. J. Ohlbach & U. Reyle (Eds.), Logic, language and reasoning. Essays in Honor of Dov Gabbay’s 50th Anniversary (pp. 173–250). Dordrecht: Kluwer Academic Publishers.Google Scholar
  42. 42.
    de Queiroz, R. J. G. B., Gabbay, D. M., & de Oliveira, A. G. (2013). The functional interpretation of non-classical logics. River Edge, NJ: Imperial College Press, World Scientific.Google Scholar
  43. 43.
    Sluga, H. (1980). Gottlob Frege. Series The Arguments of the Philosophers ( xi+203pp). London: Routledge & Kegan Paul.Google Scholar
  44. 44.
    Statman, R. (1977). Herbrand’s Theorem and Gentzen’s notion of a direct proof. In J. Barwise (Ed.), Handbook of mathematical logic. Amsterdam: North-Holland.Google Scholar
  45. 45.
    Statman, R. (1978). Bounds for proof-search and speed-up in the predicate calculus. Annals of Mathematical Logic, 15, 225–287.CrossRefGoogle Scholar
  46. 46.
    Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics: An introduction. Vol. II, Vol. 123 of Studies in logic and the foundations of mathematics (xvii+535pp). Amsterdam: North-Holland.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2014

Authors and Affiliations

  • Ruy J. G. B. de Queiroz
    • 1
    Email author
  • Anjolina G. de Oliveira
    • 1
  1. 1.Centro de InformáticaUniversidade Federal de PernambucoRecifeBrazil

Personalised recommendations