Universal Constructions for Identity and Number

Curtis Franks

doi:10.18778/0138-0680.2026.23

Authors

Curtis Franks University of Notre Dame, Department of Philosophy, United States Author https://orcid.org/0009-0002-3486-7705

DOI:

https://doi.org/10.18778/0138-0680.2026.23

Keywords:

proof theory, universal property, Gerhardt Gentzen, identity, induction

Abstract

The scheme that Gentzen designed to specify the definitions of logical connectives has a wider reach than is usually recognized, extending naturally to terms that Gentzen did not treat explicitly, including predicate symbols. After explaining (§2) how the introduction and elimination rules of natural deduction calculi provide a relational definition of a term through a universal construction, we will describe how to provide similar constructions of, first, the binary predicate symbol for identity (§3) and, second, the monadic predicate symbol for being a natural number (§4). The main result of §3 is the interderivability of the introduction rule for identity (=I) with the law of reflexivity. This result greatly simplifies the analysis of the former rule. Further, it explains why attempts either to reject =I as unsound or to justify it only relative to specific background assumptions have systematically missed its decontextualized role in inference. In §4 we review the realization, observed by Martin-Löf and Parsons, of the principle of mathematical induction as an elimination rule (\(\mathbb{N}\)E) for the natural number predicate. Noting the universal construction underlying this realization clarifies the relationship between the induction principle and the number concept, at least when the latter is relationally specified, by resituating induction as an integral part of the very definition of the natural numbers. The common motif tying these and other results together is the fact that a term’s introduction and elimination rules are a presentation of a single concept, the term’s universal construction.

References

S. Abramsky, N. Tzevelekos, Introduction to Categories and Categorical Logic, [in:] B. Coecke (ed.), New Structures for Physics, vol. 813 of Lecture Notes in Physics, Springer, Berlin, Heidelberg (2011), pp. 3–94, DOI: https://doi.org/10.1007/978-3-642-12821-9_1.

S. Awodey, Category Theory, 2nd ed., vol. 52 of Oxford Logic Guides, Oxford University Press, Oxford (2010), paperback ISBN 978-0-19-923718-0.

G. M. Bergman, An Invitation to General Algebra and Universal Constructions, 2nd ed., Universitext, Springer, Cham (2015), DOI: https://doi.org/10.1007/978-3-319-11478-1.

W. B. Ewald, W. Sieg (eds.), David Hilbert’s Lectures on the Foundations of Arithmetic and Logic 1917–1933, vol. 3 of David Hilbert’s Lectures on the Foundations of Mathematics and Physics, 1891–1933, Springer, Berlin, Heidelberg (2013), DOI: https://doi.org/10.1007/978-3-540-69444-1.

C. Franks, The Collapse of Higher-Order Inference Rules, The Review of Symbolic Logic, (2026), pp. 1–14, DOI: https://doi.org/10.1017/S1755020326101208, first View; published online 25 June 2026.

C. Franks, Gentzen’s Logical Calculi: (the Theory Pamphlet), 1st ed., SpringerBriefs in Philosophy, Springer, Cham (2026), DOI: https://doi.org/10.1007/978-3-031-91999-2.

G. Gentzen, Untersuchungen über das logische Schließen, Ph.D. thesis, Georg-August-Universität Göttingen, Göttingen (1933), accepted as a doctoral dissertation in 1933; published in two parts in Mathematische Zeitschrift 39 (1934–1935), pp. 176–210 and 405–431, DOI: https://doi.org/10.1007/BF01201353 and DOI: https://doi.org/10.1007/BF01201363. English translation: “Investigations into Logical Deduction,” in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 68–131, DOI: https://doi.org/10.1016/S0049-237X(08)70822-X.

G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112(1) (1936), pp. 493–565, DOI: https://doi.org/10.1007/BF01565428, English translation: “The Consistency of Elementary Number Theory,” in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 132–213, DOI: https://doi.org/10.1016/S0049-237X(08)70823-1.

O. Griffiths, Harmonious Rules for Identity, The Review of Symbolic Logic, vol. 7(3) (2014), pp. 499–510, DOI: https://doi.org/10.1017/S1755020314000161.

A. Klev, The Harmony of Identity, Journal of Philosophical Logic, vol. 48(5) (2019), pp. 867–884, DOI: https://doi.org/10.1007/s10992-018-09499-0.

M. Kremer, Read on Identity and Harmony: A Friendly Correction and Simplification, Analysis, vol. 67(2) (2007), pp. 157–159, DOI: https://doi.org/10.1093/analys/67.2.157.

J. Lambek, Deductive Systems and Categories I: Syntactic Calculus and Residuated Categories, Mathematical Systems Theory, vol. 2(4) (1968), pp. 287–318, DOI: https://doi.org/10.1007/BF01703261.

J. Lambek, Deductive Systems and Categories II: Standard Constructions and Closed Categories, [in:] P. J. Hilton (ed.), Category Theory, Homology Theory and Their Applications I: Proceedings of the Conference Held at the Seattle Research Center of the Battelle Memorial Institute, June 24–July 19, 1968, Volume One, vol. 86 of Lecture Notes in Mathematics, Springer, Berlin, Heidelberg (1969), pp. 76–122, DOI: https://doi.org/10.1007/BFb0079385.

J. Lambek, P. J. Scott, Introduction to Higher-Order Categorical Logic, vol. 7 of Cambridge Studies in Advanced Mathematics, Cambridge University Press, Cambridge (1986).

F. W. Lawvere, An Elementary Theory of the Category of Sets, Proceedings of the National Academy of Sciences of the United States of America, vol. 52(6) (1964), pp. 1506–1511, DOI: https://doi.org/10.1073/pnas.52.6.1506, a longer version with commentary by the author and Colin McLarty appeared in Reprints in Theory and Applications of Categories, no. 11 (2005), pp. 1–35.

F. W. Lawvere, Adjointness in Foundations, Dialectica, vol. 23(3–4) (1969), pp. 281–296, DOI: https://doi.org/10.1111/j.1746-8361.1969.tb01194.x.

F. W. Lawvere, Quantifiers and Sheaves, [in:] Actes du Congrès International des Mathématiciens (Nice, 1970), vol. 1, Gauthier-Villars, Paris (1971), pp. 329–334, proceedings of the International Congress of Mathematicians held in Nice in 1970.

P. Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, [in:] J. E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, vol. 63 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam (1971), pp. 179–216, DOI: https://doi.org/10.1016/S0049-237X(08)70847-4.

C. Mitsch, Why Should Identity Be Logical?, The Review of Symbolic Logic, vol. 18(4) (2025), pp. 1168–1191, DOI: https://doi.org/10.1017/S1755020325100932.

C. Parsons, The Impredicativity of Induction, [in:] M. Detlefsen (ed.), Proof, Logic and Formalization, Routledge, London and New York (1992), pp. 139–161, revised and expanded version of a 1983 paper.

J. H. Poincaré, Mathematics and Logic III, [in:] W. B. Ewald (ed.), From Kant to Hilbert: A Source Book in the Foundations of Mathematics, vol. 2, Clarendon Press, Oxford (1996), pp. 1052–1071, translated by George Bruce Halsted and William Bragg Ewald. Originally published as “Les mathématiques et la logique” in Revue de Métaphysique et de Morale 14 (1906), pp. 294–317.

S. Read, Identity and Harmony, Analysis, vol. 64(2) (2004), pp. 113–119, DOI: https://doi.org/10.1093/analys/64.2.113.

S. Read, Harmonic Inferentialism and the Logic of Identity, The Review of Symbolic Logic, vol. 9(2) (2016), pp. 408–420, DOI: https://doi.org/10.1017/S1755020316000010.

P. Samuel, On Universal Mappings and Free Topological Groups, Bulletin of the American Mathematical Society, vol. 54(6) (1948), pp. 591–598, DOI: https://doi.org/10.1090/S0002-9904-1948-09052-8.

J. von Plato, Gentzen’s Proof of Normalization for Natural Deduction, Bulletin of Symbolic Logic, vol. 14(2) (2008), pp. 240–257, DOI: https://doi.org/10.2178/bsl/1208442829.