The Harmony of Identity

  • Ansten KlevEmail author


The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in a proof-theoretical manner.


Identity Natural deduction Definition 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.



The justification of =-elim given here is an adaptation to natural deduction of the justification of the corresponding rule in Martin-Löf’s type theory given in [7]. Correspondence with Per Martin-Löf pertaining to the latter work suggested to me the conception of canonical derivation that lies at the basis of the current work. While writing the paper I have been financially supported by grant nr. 17-18344Y from the Czech Science Foundation, GAČR.


  1. 1.
    Curry, H.B. (1963). Foundations of mathematical logic. New York: McGraw-Hill.Google Scholar
  2. 2.
    Curry, H.B., & Feys, R. (1958). Combinatory logic Vol. 1. Amsterdam: North-Holland.Google Scholar
  3. 3.
    Fitch, F.B. (1952). Symbolic logic. New York: The Ronald Press.Google Scholar
  4. 4.
    Gentzen, G. (1933). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431.CrossRefGoogle Scholar
  5. 5.
    Griffiths, O. (2014). Harmonious rules for identity. Review of Symbolic Logic, 7, 499–510.CrossRefGoogle Scholar
  6. 6.
    Kleene, S.C. (1952). Introduction to metamathematics. New York: Van Norstrand.Google Scholar
  7. 7.
    Klev, A. (2017). The justification of identity elimination in Martin-Löf’s type theory. Topoi. Online First.
  8. 8.
    Lemmon, E.J. (1965). Beginning logic. London: Nelson.Google Scholar
  9. 9.
    Martin-Löf, P. (1971). Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 179–216). Amsterdam: North-Holland.Google Scholar
  10. 10.
    Martin-Löf, P. (1975). About models for intuitionistic type theories and the notion of definitional equality. In Kanger, S. (Ed.) Proceedings of the third Scandinavian logic symposium (pp. 81–109). Amsterdam: North-Holland.Google Scholar
  11. 11.
    Martin-Löf, P. (1998). An intuitionistic theory of types. In Sambin, G., & Smith, J. (Eds.) Twenty-five years of constructive type theory. First published as preprint in 1972 (pp. 127–172). Oxford: Clarendon Press.Google Scholar
  12. 12.
    Milne, P. (2007). Existence, freedom, identity, and the logic of abstractionist realism. Mind, 116, 23–53.CrossRefGoogle Scholar
  13. 13.
    Prawitz, D. (1965). Natural deduction. Stockholm: Almqvist & Wiksell.Google Scholar
  14. 14.
    Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 235–307). Amsterdam: North-Holland.Google Scholar
  15. 15.
    Prawitz, D. (1973). Towards a foundation of a general proof theory. In Suppes, P., Henkin, L., Joja, A., Moisil, G.C. (Eds.) Logic, methodology and philosophy of science IV (pp. 225–250). Amsterdam: North-Holland.Google Scholar
  16. 16.
    Read, S. (2004). Identity and harmony. Analysis, 64, 113–119.CrossRefGoogle Scholar
  17. 17.
    Read, S. (2016). Harmonic inferentialism and the logic of identity. Review of Symbolic Logic, 9, 408–420.CrossRefGoogle Scholar
  18. 18.
    Schroeder-Heister, P. (2006). Validity concepts in proof-theoretic semantics. Synthese, 148, 525–571.CrossRefGoogle Scholar
  19. 19.
    Tait, W.W. (1967). Intensional interpretations of functionals of finite type. Journal of Symbolic Logic, 32, 198–212.CrossRefGoogle Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.Institute of PhilosophyCzech Academy of SciencesPragueCzech Republic

Personalised recommendations