Skip to main content

Advertisement

Log in

On Different Ways of Being Equal

  • Original Research
  • Published:
Erkenntnis Aims and scope Submit manuscript

Abstract

The aim of this paper is to present a constructive solution to Frege’s puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege’s distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. See for instance Corazza and Dokič (1995); May (2001).

  2. False equality propositions have cognitive significance in our account, see Sect. 7.

  3. See Grundgesetze (Frege 1962, II, Sect. 57).

  4. The possibility should be considered that Frege did not think that providing an identity criterion for senses in Grundgesetze was important. Ruffino (1997), Duarte (2009), and Klement (2016) observed that the thesis that the reference of a sentence is a truth value was absolutely necessary to introduce Axiom IV to the system in the book. This axiom is crucial to prove that \((A \supset B) \supset (B \supset A) \supset (A = B)\), a theorem without which Frege could not show that the number of the set A equals the number of the set B iff there is a bijection from A to B (Hume’s principle). But as long as the sense and reference of an expression are not kept apart, there may be false instances of it. For example, \((1+1=2) \supset (2=2) \supset ((1+1=2)=(2=2))\) seems to be a valid instance for references, but it is false for senses according to Frege (1891). As Ruffino (1997) suggests, Frege’s sense/reference distinction may have been motivated by purely mathematical reasons, a necessary change in order to make the technical development of his logicism plausible.

  5. Klement (2002, 2016) also distinguishes three other identity criteria for senses: (4) an intermediate interpretation where the identity criterion for senses are stipulated by abstraction principles such as Frege’s infamous Axiom V and (5) a fine view according to which the sense of a closed term has as its parts only the senses of the primitive expressions forming it. In either case, (Klement 2016, Sect. 5) acknowledges that it is hard to amend the theory of sense and reference of Grundgesetze with these interpretations, given that all these identity criteria for senses give rise to problems on their own.

  6. Yet, this circular identification of constructibility with provability is now widespread in the literature. It can be traced back to Dummett’s (1975) influential reconstruction of the intuitionism of Brouwer and Heyting in terms of proof as the primitive notion, which is a result of his radical rejection of the traditional account of constructions as free mental processes given in intuition.

  7. This is certainly not a trivial question, considering that Martin-Löf (1975, 1982), the originator of both intensional and extensional traditions in type theory, has vacillated between regarding one approach as most fitting with the meaning explanations—until he finally decided adopting intensional type theory as the basis of his philosophical investigations in the late 80s. It appears this decision is inspired by a shift of viewpoint regarding the nature of constructions, which begin to be explicitly treated as proofs (Martin-Löf 1987). But, as I mentioned in Sect. 3, the failure to distinguish proof and construction can be quite problematic.

  8. The reflection rule is sometimes viewed negatively because it is responsible for “loss of knowledge”. That is, one might argue that when moving from the premise to the conclusion of the rule the proof-term p gets lost in a way that can no longer be recovered, thus going against the general requirement that in the rules for a constructive theory knowledge should never get lost Sambin and Valentini (1998). This is an interesting point, but I believe it incorrectly assumes that terms are always intended to represent proofs. In extensional type theory, terms codify realizers and we should not expect them to carry proof-theoretic information.

  9. Although there are exceptions. See Sect. 6.

  10. After completion of the present paper the author learned that Sundholm (1994) has proposed a similar type-theoretic interpretation of the equipollence principle for sentences. Sundholm’s account is based on Frege’s original formulation of the principle, so he did not provide a view for singular terms.

  11. This interpretation is often mistakenly attributed to Martin-Löf. In his actual account, a judgmental equality \(a \equiv b : A\) says of the senses of ‘a’ and ‘b’ that they are co-referential and a propositional equality \(p : a =_A b \) says of the references of ‘a’ and ‘b’ that they are equal objects (Martin-Löf 2001, pp. 14–17). I am grateful to Professor Martin-Löf for clarifying his views on the sense/reference distinction to me.

  12. See (Frege 1891, p. 29).

  13. See Ladyman and Presnell (2019); Bentzen (2020) for a more detailed discussion.

References

  • Angiuli, C., Brunerie, G., Coquand, T., Hou (Favonia), K.B., Harper, R., & Licata, D. (2019). Syntax and models of cartesian cubical type theory. URL: https://github.com/dlicata335/cart-cube. Preprint.

  • Awodey, S. (2014). Structuralism, Invariance, and Univalence. Philosophia Mathematica, 22(1), 1–11.

    Article  Google Scholar 

  • Barzan, L. (2016). A strong normalization theorem via validity for a type system with propositional equality. Master’s thesis, Università di Padova.

  • Bentzen, B. (2018). Constructive mathematics and equality. Ph.D. thesis, Sun Yat-sen University.

  • Bentzen, B. (2020). What types should not be. Philosophia Mathematica, 28(1), 60–76.

    Article  Google Scholar 

  • Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill.

    Google Scholar 

  • Bolzano, B. (1837). Wissenschaftslehre I-1V. Sulzbach: Seidel.

    Google Scholar 

  • Brouwer, L. E. J. (1907). Over de Grondslagen der Wiskunde. Ph.D. thesis, Universiteit van Amsterdam.

  • Brouwer, L. E. J. (1975). Points and spaces. In: Philosophy and Foundations of Mathematics, pp. 522–538. Elsevier.

  • Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2016). Cubical type theory: a constructive interpretation of the univalence axiom. arXiv preprint arXiv:1611.02108.

  • Corazza, E., & Dokič, J. (1995). Why is Frege’s puzzle still puzzling? In J. Biro & P. Kotatko (Eds.), Frege: Sense and Reference one hundred years later (pp. 266–290). Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  • Duarte, A. B. (2009). Lógica e aritmética na filosofia da matemática de Frege. Ph.D. thesis, PUC-Rio.

  • Dummett, M. A. (1975). Frege’s distinction between sense and reference. In: Truth and Other Enigmas, pp. 116–144. Harvard Univ. Press, Cambridge (1978). Original work published in.

  • Frege, G. (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: Nebert

  • Frege, G. (1891). Funktion und Begriff. Jena: Hermann Pohle.

    Google Scholar 

  • Frege, G. (1892). Über Sinn und Bedeutung. Zeitschrift für Philosophie und philosophische Kritik, 100, 25–50.

    Google Scholar 

  • Frege, G. (1906). A brief survey of my logical doctrines. H. Hermes, F. Kambartel, and Friedrich Kaulbach (eds and trans.). Frege: Posthumous Writings. Oxford: Basil Blackwell 1979, 197–202.

  • Frege, G. (1962). Grundgesetze der Arithmetik (I-II). Hildesheim: Georg Olms.

    Google Scholar 

  • Frege, G. (1982a). Letter to Husserl (1906). In: G. Gabriel, B. McGuinness, H. Kaal (eds.) Philosophical and mathematical correspondence. University of Chicago Press. Translated by H. Kaal

  • Frege, G. (1982b). Letter to Peano, undated (c. 1894–1896). In: G. Gabriel, B. McGuinness, H. Kaal (eds.) Philosophical and mathematical correspondence. University of Chicago Press. Translated by H. Kaal

  • Gentzen, G., & Szabo, M. (1969). The collected papers of Gerhard Gentzen. Amsterdam: North Holland.

    Google Scholar 

  • Heyting, A. (1931). Die intuitionistische Grundlegung der Mathematik. Erkenntnis, 2(1), 106–115.

    Article  Google Scholar 

  • Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice (Vol. 36, pp. 83–111)., 1995), Oxford Logic Guides New York: Oxford Univ. Press.

  • Howard, W. A. (1980). The formulae-as-types notion of construction. In J. P. Seldin & J. R. Hindley (Eds.), Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (pp. 479–490). London: Academic Press.

  • Klement, K. C. (2002). Frege and the Logic of Sense and Reference. Cambridge: Psychology Press.

    Google Scholar 

  • Klement, K. C. (2016). Grundgesetze and the sense/reference distinction. In: P.A. Ebert, M. Rossberg (eds.) Essays on Frege’s Grundgesetze. Oxford University Press

  • Kreisel, G. (1962). Foundations of intuitionistic logic. In E. Nagel, P. Suppes, & A. Tarski (Eds.), Logic, methodology, and the philosophy of science, Proceedings of the 1960 International Congress, Stanford University Press, Stanford, Calif., 1962, pp. 198–210.

  • Ladyman, J., & Presnell, S. (2019). Universes and Univalence in Homotopy Type Theory. Review of Symbolic Logic, 12(3), 426–455.

    Article  Google Scholar 

  • Martin-Löf, P. (1975). An intuitionistic theory of types: predicative part. In: H.E. Rose, J.C. Shepherdson (eds.) Logic Colloquium ’73 : Proceedings of the logic colloquium, Bristol, pp. 73–118. North-Holland, Amsterdam, New York, Oxford.

  • Martin-Löf, P. (1982). Constructive mathematics and computer programming. In: Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., vol. 104, pp. 153–175. North-Holland, Amsterdam.

  • Martin-Löf, P. (1984). Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol. 1. Bibliopolis, Naples. Notes by Giovanni Sambin.

  • Martin-Löf, P. (1987). Truth of a proposition, evidence of a judgement, validity of a proof. Synthese, 73, 407–420.

    Article  Google Scholar 

  • Martin-Löf, P. (1996). On the meanings of the logical constants and the justifications of the logical laws. Nordic J. Philos. Logic, 1(1), 11–60.

    Google Scholar 

  • Martin-Löf, P. (2001). The sense/reference distinction in constructive semantics. Paper read at Leiden (transc. by B. Jespersen).

  • May, R. (2001). Frege on identity statements. In: G.C. C. Cecchetto, M.T. Guasti (eds.) Semantic Interfaces: Reference, Anaphora, and Aspect, pp. 1–51. CSLI Publications.

  • Moschovakis, Y. N. (1994). Sense and denotation as algorithm and value. In: J. Väänänen, J. Oikkonen (eds.) Logic Colloquium ’90: Proceedings of the logic colloquium, Bristol, Lecture Notes in Logic, vol. 2, pp. 210–249. Springer-Verlag, Berlin.

  • Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm: Almqyist & Wiksell.

    Google Scholar 

  • Rodin, A. (2017). Venus homotopically. IfCoLog Journal of Logics and their Applications 4(4), 1427–1446. Special Issue Dedicated to the Memory of Grigori Mints.

  • Ruffino, M. (1997). Wahrheitswerte als gegenstände und die unterscheidung zwischen sinn und bedeutung. Kritisches Jahrbuch der Philosophie, 2, 69–118.

    Google Scholar 

  • Sambin, G., & Valentini, S. (1998). Building up a toolbox for martin-löf’s type theory: subset theory. Twenty five years of Constructive Type Theory, 36, 221.

    Google Scholar 

  • Streicher, T. (1993). Investigations into intensional type theory. Habilitiation Thesis, Ludwig Maximilian Universität.

  • Sundholm, G. (1993). Questions of Proof. Manuscrito, 16(2), 47–70.

    Google Scholar 

  • Sundholm, G. (1994). Proof-Theoretical Semantics and Fregean Identity Criteria for Propositions. The Monist, 77(3), 294–314.

    Article  Google Scholar 

  • UFP (The Univalent Foundations Program) (2013). Homotopy type theory: Univalent foundations of mathematics.

  • Tieszen, R. (1995). What is the philosophical basis of intuitionistic mathematics? Studies in Logic and the Foundations of Mathematics, 134, 579–594.

    Article  Google Scholar 

Download references

Acknowledgements

I am indebted to Jeremy Avigad, David Corfield, Ansten Klev, Andrei Rodin, Yimu Yin, Jiji Zhang, and five annonymous referees for comments on previous drafts of this paper. This work was supported by US Air Force Office of Scientific Research (AFOSR) Grant FA9550-18-1-0120. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsement, either expressed or implied, of the AFOSR or the US Government.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Bruno Bentzen.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bentzen, B. On Different Ways of Being Equal. Erkenn 87, 1809–1830 (2022). https://doi.org/10.1007/s10670-020-00275-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10670-020-00275-8

Navigation