{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T19:46:59Z","timestamp":1761767219218,"version":"3.32.0"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2023,6,27]],"date-time":"2023-06-27T00:00:00Z","timestamp":1687824000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>I discuss problems with Martin-L\u00f6f\u2019s distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-L\u00f6f\u2019s claim that all judgments of the forms <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020323000199_inline1.png\"\/><jats:tex-math>\n$a : A$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020323000199_inline2.png\"\/><jats:tex-math>\n$a = b : A$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> are analytic is unfounded. As I shall show, when <jats:italic>A<\/jats:italic> evaluates to a dependent function type <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020323000199_inline3.png\"\/><jats:tex-math>\n$(x : B) \\to C$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-L\u00f6f\u2019s original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic\u2013synthetic distinction reworked here is capable of accommodating judgments of the forms <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020323000199_inline4.png\"\/><jats:tex-math>\n$A \\&gt; \\mathsf {type}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020323000199_inline5.png\"\/><jats:tex-math>\n$A = B \\&gt; \\mathsf {type}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-L\u00f6f\u2019s position on the analytic grounding of synthetic judgments.<\/jats:p>","DOI":"10.1017\/s1755020323000199","type":"journal-article","created":{"date-parts":[[2023,6,27]],"date-time":"2023-06-27T08:26:16Z","timestamp":1687854376000},"page":"1119-1145","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["ANALYTICITY AND SYNTHETICITY IN TYPE THEORY REVISITED"],"prefix":"10.1017","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5987-7806","authenticated-orcid":false,"given":"BRUNO","family":"BENTZEN","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,6,27]]},"reference":[{"key":"S1755020323000199_r23","first-page":"203","volume-title":"Atti degli incontri di logica matematica. Scuola di Specializzazione in Logica Matematica","volume":"2","author":"Martin-L\u00f6f","year":"1985"},{"volume-title":"Reflections on Kurt G\u00f6del","year":"1990","author":"Wang","key":"S1755020323000199_r34"},{"key":"S1755020323000199_r5","doi-asserted-by":"publisher","DOI":"10.1007\/s10743-022-09323-3"},{"key":"S1755020323000199_r31","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-5137-8_3"},{"key":"S1755020323000199_r4","doi-asserted-by":"publisher","DOI":"10.1007\/s10670-020-00275-8"},{"key":"S1755020323000199_r24","doi-asserted-by":"publisher","DOI":"10.1007\/BF00484985"},{"key":"S1755020323000199_r7","unstructured":"[7] Brouwer, L. E. J. (1905\u20131907). Student notebooks. Digital transcriptions by John Kuiper. Available from: http:\/\/www.cs.ru.nl\/F.Wiedijk\/brouwer\/transcriptie.pdf."},{"key":"S1755020323000199_r1","unstructured":"[1] Allen, S. (1987). A Non-Type-Theoretic Definition of Martin-L\u00f6f\u2019s Types. Ph.D. Thesis, Cornell University."},{"key":"S1755020323000199_r28","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2021.61"},{"key":"S1755020323000199_r33","volume-title":"Constructivism in mathematics","volume":"I","author":"Troelstra","year":"1988"},{"volume-title":"Kritik der reinen Vernunft","year":"1781","author":"Kant","key":"S1755020323000199_r18"},{"key":"S1755020323000199_r11","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2021.60"},{"key":"S1755020323000199_r19","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2019.21"},{"volume-title":"Implementing Mathematics with the Nuprl Proof Development System","year":"1985","author":"Constable","key":"S1755020323000199_r10"},{"volume-title":"Logical Investigations (I\/II)","year":"1970","author":"Husserl","key":"S1755020323000199_r17"},{"key":"S1755020323000199_r22","first-page":"153","volume-title":"Logic, Methodology and Philosophy of Science, VI (Hannover, 1979)","volume":"104","author":"Martin-L\u00f6f","year":"1982"},{"key":"S1755020323000199_r26","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-0834-8_5"},{"key":"S1755020323000199_r30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-1986-9_11"},{"key":"S1755020323000199_r20","first-page":"198","volume-title":"Logic, Methodology, and the Philosophy of Science","author":"Kreisel","year":"1962"},{"key":"S1755020323000199_r15","unstructured":"[14] Harper, R. (2013). Constructive mathematics is not metamathematics. Available from: https:\/\/existentialtype.wordpress.com\/2013\/07\/10\/constructive-mathematics-is-not-meta-mathematics\/ [Online] (accessed 12 August 2022)."},{"key":"S1755020323000199_r8","unstructured":"[8] Brouwer, L. E. J. (1907). Over de Grondslagen der Wiskunde. Ph.D. Thesis, Universiteit van Amsterdam. English translation in Brouwer in 1975. Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North-Holland, pp. 13\u2013101."},{"key":"S1755020323000199_r13","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-4435-6_11"},{"key":"S1755020323000199_r2","first-page":"680","article-title":"Computational higher-dimensional type theory","author":"Angiuli","year":"2017","journal-title":"POPL \u201917: Proceedings of the 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages."},{"key":"S1755020323000199_r27","unstructured":"[26] Martin-L\u00f6f, P. (2014). Truth of empirical propositions. Transcriptions of lectures given at Leiden University on February 4, 2014. Available from: https:\/\/pml.flu.cas.cz\/uploads\/PML-Leiden04Feb14.pdf."},{"key":"S1755020323000199_r12","first-page":"116","volume-title":"Truth and Other Enigmas","author":"Dummett","year":"1978"},{"key":"S1755020323000199_r3","first-page":"179","article-title":"Sense, reference, and computation","volume":"47","author":"Bentzen","year":"2020","journal-title":"Perspectiva Filosofica"},{"key":"S1755020323000199_r6","doi-asserted-by":"publisher","DOI":"10.1080\/01445340.2023.2210908"},{"key":"S1755020323000199_r32","first-page":"59","volume-title":"Wittgenstein\u2014Towards a Re-Evaluation, Proceedings of the 14th International Wittgenstein Symposium. Kirchberg Am Wechsel, 13\u201320 August 1989","author":"Sundholm","year":"1990"},{"key":"S1755020323000199_r16","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S1755020323000199_r29","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-8311-4_25"},{"key":"S1755020323000199_r21","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S1755020323000199_r14","unstructured":"[13] Frege, G. (1884). Die Grundlagen der Arithmetik: eine logisch mathematische Untersuchung \u00fcber den Begriff der Zahl. w. Koebner."},{"key":"S1755020323000199_r25","unstructured":"[24] Martin-L\u00f6f, P. (1993). Philosophical aspects of intuitionistic type theory. Transcriptions of lectures given at Leiden University from 23 September to 16 December. Available from: https:\/\/pml.flu.cas.cz\/uploads\/PML-LeidenLectures93.pdf."}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020323000199","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,2]],"date-time":"2025-01-02T10:53:42Z","timestamp":1735815222000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020323000199\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,27]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["S1755020323000199"],"URL":"https:\/\/doi.org\/10.1017\/s1755020323000199","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"type":"print","value":"1755-0203"},{"type":"electronic","value":"1755-0211"}],"subject":[],"published":{"date-parts":[[2023,6,27]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}