{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T10:44:46Z","timestamp":1774953886301,"version":"3.50.1"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,1,12]],"date-time":"2019-01-12T00:00:00Z","timestamp":1547251200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Grantov? Agentura ?esk? Republiky","doi-asserted-by":"publisher","award":["17-18344Y"],"award-info":[{"award-number":["17-18344Y"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Philos Logic"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10992-018-09499-0","type":"journal-article","created":{"date-parts":[[2019,1,11]],"date-time":"2019-01-11T22:59:29Z","timestamp":1547247569000},"page":"867-884","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["The Harmony of Identity"],"prefix":"10.1007","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1091-284X","authenticated-orcid":false,"given":"Ansten","family":"Klev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,12]]},"reference":[{"key":"9499_CR1","volume-title":"Foundations of mathematical logic","author":"HB Curry","year":"1963","unstructured":"Curry, H.B. (1963). Foundations of mathematical logic. New York: McGraw-Hill."},{"key":"9499_CR2","volume-title":"Combinatory logic, Vol. 1","author":"HB Curry","year":"1958","unstructured":"Curry, H.B., & Feys, R. (1958). Combinatory logic Vol. 1. Amsterdam: North-Holland."},{"key":"9499_CR3","volume-title":"Symbolic logic","author":"FB Fitch","year":"1952","unstructured":"Fitch, F.B. (1952). Symbolic logic. New York: The Ronald Press."},{"key":"9499_CR4","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1933","unstructured":"Gentzen, G. (1933). Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift, 39, 176\u2013210, 405\u2013431.","journal-title":"Mathematische Zeitschrift"},{"key":"9499_CR5","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1017\/S1755020314000161","volume":"7","author":"O Griffiths","year":"2014","unstructured":"Griffiths, O. (2014). Harmonious rules for identity. Review of Symbolic Logic, 7, 499\u2013510.","journal-title":"Review of Symbolic Logic"},{"key":"9499_CR6","volume-title":"Introduction to metamathematics","author":"SC Kleene","year":"1952","unstructured":"Kleene, S.C. (1952). Introduction to metamathematics. New York: Van Norstrand."},{"issue":"3","key":"9499_CR7","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/s11245-017-9509-1","volume":"38","author":"Ansten Klev","year":"2017","unstructured":"Klev, A. (2017). The justification of identity elimination in Martin-L\u00f6f\u2019s type theory. Topoi. Online First. \n                    https:\/\/doi.org\/10.1007\/s11245-017-9509-1\n                    \n                  .","journal-title":"Topoi"},{"key":"9499_CR8","volume-title":"Beginning logic","author":"EJ Lemmon","year":"1965","unstructured":"Lemmon, E.J. (1965). Beginning logic. London: Nelson."},{"key":"9499_CR9","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"Per Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, 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\u2013216). Amsterdam: North-Holland."},{"key":"9499_CR10","unstructured":"Martin-L\u00f6f, 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\u2013109). Amsterdam: North-Holland."},{"key":"9499_CR11","unstructured":"Martin-L\u00f6f, 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\u2013172). Oxford: Clarendon Press."},{"key":"9499_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1093\/mind\/fzm023","volume":"116","author":"P Milne","year":"2007","unstructured":"Milne, P. (2007). Existence, freedom, identity, and the logic of abstractionist realism. Mind, 116, 23\u201353.","journal-title":"Mind"},{"key":"9499_CR13","volume-title":"Natural deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D. (1965). Natural deduction. Stockholm: Almqvist & Wiksell."},{"key":"9499_CR14","unstructured":"Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 235\u2013307). Amsterdam: North-Holland."},{"key":"9499_CR15","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0049-237X(09)70361-1","volume-title":"Proceedings of the Fourth International Congress for Logic, Methodology and Philosophy of Science, Bucharest, 1971","author":"Dag Prawitz","year":"1973","unstructured":"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\u2013250). Amsterdam: North-Holland."},{"key":"9499_CR16","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1093\/analys\/64.2.113","volume":"64","author":"S Read","year":"2004","unstructured":"Read, S. (2004). Identity and harmony. Analysis, 64, 113\u2013119.","journal-title":"Analysis"},{"key":"9499_CR17","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1017\/S1755020316000010","volume":"9","author":"S Read","year":"2016","unstructured":"Read, S. (2016). Harmonic inferentialism and the logic of identity. Review of Symbolic Logic, 9, 408\u2013420.","journal-title":"Review of Symbolic Logic"},{"key":"9499_CR18","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","volume":"148","author":"P Schroeder-Heister","year":"2006","unstructured":"Schroeder-Heister, P. (2006). Validity concepts in proof-theoretic semantics. Synthese, 148, 525\u2013571.","journal-title":"Synthese"},{"key":"9499_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"WW Tait","year":"1967","unstructured":"Tait, W.W. (1967). Intensional interpretations of functionals of finite type. Journal of Symbolic Logic, 32, 198\u2013212.","journal-title":"Journal of Symbolic Logic"}],"container-title":["Journal of Philosophical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-018-09499-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10992-018-09499-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-018-09499-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,11]],"date-time":"2020-01-11T19:04:36Z","timestamp":1578769476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10992-018-09499-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,12]]},"references-count":19,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["9499"],"URL":"https:\/\/doi.org\/10.1007\/s10992-018-09499-0","relation":{},"ISSN":["0022-3611","1573-0433"],"issn-type":[{"value":"0022-3611","type":"print"},{"value":"1573-0433","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,12]]},"assertion":[{"value":"4 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}