{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:24:34Z","timestamp":1742912674482,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031514050"},{"type":"electronic","value":"9783031514067"}],"license":[{"start":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T00:00:00Z","timestamp":1702425600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T00:00:00Z","timestamp":1702425600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-51406-7_4","type":"book-chapter","created":{"date-parts":[[2024,4,1]],"date-time":"2024-04-01T20:18:53Z","timestamp":1712002733000},"page":"51-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["G\u00f6del\u2019s Absolute Proofs and Girard\u2019s Ludics: Mutual Insights"],"prefix":"10.1007","author":[{"given":"Gabriella","family":"Crocco","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Myriam","family":"Quatrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,13]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3), 297\u2013347.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"4_CR2","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s11225-010-9280-4","volume":"96","author":"M Antonutti-Marfori","year":"2010","unstructured":"Antonutti-Marfori, M. (2010). Informal proofs and mathematical rigour. Studia Logica, 96(2), 261\u2013272.","journal-title":"Studia Logica"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Basaldella, M., & Faggian, C. (2011). Ludics with repetitions (exponentials, interactive types and completeness). Proceedings - Symposium on Logic in Computer Science, 7(2).","DOI":"10.2168\/LMCS-7(2:13)2011"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Catta, D., & Piccolomini d\u2019Aragona, A. (2022). Game of grounds. Objects, structures, and logics. Boston studies in the philosophy and history of science (Vol. 339, pp. 259\u2013286). Springer International Publishing. 978-3-030-84705-0.","DOI":"10.1007\/978-3-030-84706-7_10"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/s11245-017-9515-3","volume":"38","author":"G Crocco","year":"2019","unstructured":"Crocco, G. (2019). Informal and absolute proofs: Some remarks from a G\u00f6delian perspective. Topoi, 38, 561\u2013575.","journal-title":"Topoi"},{"issue":"11","key":"4_CR6","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"H B Curry","year":"1934","unstructured":"Curry, H. B. (1934). Functionality in combinatory logic. Proceedings of the National Academy of Sciences of the United States of America, 20(11), 584\u2013590.","journal-title":"Proceedings of the National Academy of Sciences of the United States of America"},{"issue":"3","key":"4_CR7","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., & Schellinx, H. (1997). A deconstructive logic: linear logic. The Journal of Symbolic Logic , 62(3), 755\u2013807.","journal-title":"The Journal of Symbolic Logic"},{"issue":"4","key":"4_CR8","first-page":"1","volume":"8","author":"C Fouquer\u00e9","year":"2013","unstructured":"Fouquer\u00e9, C., & Quatrini, M. (2013). Argumentation and inference: A unified approach. Baltic International Yearbook of Cognition, Logic and Communication, 8(4), 1\u201341.","journal-title":"Baltic International Yearbook of Cognition, Logic and Communication"},{"key":"4_CR9","unstructured":"Fouquer\u00e9, C., & Quatrini, M. (2020). Study of behaviours via visitable paths. Logical Methods in Computer Science, 14(2)."},{"key":"4_CR10","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199285945.001.0001","volume-title":"Visual thinking in mathematics, an epistemological study","author":"M Giaquinto","year":"2007","unstructured":"Giaquinto M. (2007). Visual thinking in mathematics, an epistemological study. Oxford University Press."},{"key":"4_CR11","unstructured":"Girard, J.-Y. (1972). Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat, Universit\u00e9 Paris 7, Diderot."},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50, 1\u2013102","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"4_CR13","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J-Y Girard","year":"1991","unstructured":"Girard, J.-Y. (1991). A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3), 255\u2013296.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J-Y Girard","year":"1993","unstructured":"Girard, J.-Y. (1993). On the unity of logic. Annals of Pure and Applied Logic, 59(3), 201\u2013217.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"4_CR15","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J-Y Girard","year":"2001","unstructured":"Girard, J.-Y. (2001). Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3), 301\u2013506.","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR16","unstructured":"Girard, J.-Y. (2015). Transcendental syntax 1: Deterministic case. Mathematical structures in computer science. Computing with lambda-terms. A special issue dedicated to Corrado B\u00f6hm for his 90th birthday."},{"key":"4_CR17","unstructured":"Girard, J.-Y., Lafont, Y., & Taylor, P. (1990). Proofs and types. Cambridge tracts in theoretical computer science (Vol. 7). Cambridge University Press."},{"key":"4_CR18","unstructured":"G\u00f6del, K. (1936). On the length of proofs. In CW I (pp. 397\u2013398)."},{"key":"4_CR19","unstructured":"G\u00f6del, K. (1938). Lecture at Zilsel\u2019s. In CW III (pp. 87\u2013113)."},{"key":"4_CR20","unstructured":"G\u00f6del, K. (1941). In what sense is intuitionistic Logic constructive? In CW II (pp. 241\u2013251)."},{"key":"4_CR21","unstructured":"G\u00f6del, K. (1944). Russell\u2019s mathematical logic. In CW II (pp. 119\u2013141)."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"G\u00f6del, K. (1946). Remarks before the Princeton centennial conference on problems of mathematics. In CWII (pp. 150\u2013153).","DOI":"10.1093\/oso\/9780195147216.003.0009"},{"key":"4_CR23","unstructured":"G\u00f6del, K. (1958). On a hitherto unutilized extension of the finitary standpoint . In CW II (pp. 87\u2013113)."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"G\u00f6del, K. (1972). On an extension of finitary mathematics which has not yet been used. In CW II (pp. 271\u2013280).","DOI":"10.1093\/oso\/9780195147216.003.0022"},{"key":"4_CR25","unstructured":"G\u00f6del, K. (1986). In S. Feferman, J. Dawson, S. C. Kleene, G. H. Moore, R. M. Solovay, & J. van Heijenoort (Eds.), Collected works. Publications 1939\u20131936 (Vol. I). Oxford University Press."},{"key":"4_CR26","unstructured":"G\u00f6del, K. (1990). In S. Feferman, J. Dawson, S. C. Kleene, G. H. Moore, R. M. Solovay, & J. van Heijenoort (Eds.), Collected works. Publications 1938\u20131974 (Vol. II). Oxford University Press."},{"key":"4_CR27","unstructured":"G\u00f6del, K. (1995). In S. Feferman, J. Dawson, W. Goldfarb, C. Parsons, & R. M. Solovay (Eds.), Collected works. Unpublished essays and lectures (Vol. III). Oxford University Press."},{"key":"4_CR28","unstructured":"G\u00f6del, K. (2003). In S. Feferman, J. Dawson, W. Goldfarb, C. Parsons, & W. Sieg (Eds.), Collected works. Correspondence H-Z (Vol. V). Oxford Iniversity Press."},{"key":"4_CR29","volume-title":"To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479\u2013490)","author":"W Howard","year":"1980","unstructured":"Howard, W., & William, A. (1980). The formulae-as-types notion of construction [original paper manuscript from 1969]. In J. P. Seldin, J. R. Hindley (Eds.), To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479\u2013490). Academic Press."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Joinet, J.-B. (2007). Sur le temps logique. In J.-B. Joinet (Dir.), Logique, dynamique et cognition. Collection : Logique, langage, sciences, philosophie (pp. 31\u201349). Publications de la Sorbonne.","DOI":"10.4000\/books.psorbonne.299"},{"key":"4_CR31","first-page":"157","volume":"234","author":"J-B Joinet","year":"2023","unstructured":"Joinet, J.-B. (2023). Nature et logique de G. Gentzen \u00e0 J.-Y. Girard. Logique et Analyse, 234, 157\u201371. https:\/\/www.jstor.org\/stable\/26767822. Accessed 22 Feb 2023.","journal-title":"Logique et Analyse"},{"key":"4_CR32","volume-title":"G\u00f6del, Tarski and the lure of natural language","author":"J Kennedy","year":"2021","unstructured":"Kennedy, J. (2021). G\u00f6del, Tarski and the lure of natural language . Cambridge University Press."},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Leitgeb, H. (2009). On formal and informal prouvability. In $$\\emptyset $$. Linnebo, & O. Bueno (Eds.), New waves on Philosophy of mathematics. Palgrave.","DOI":"10.1057\/9780230245198_13"},{"key":"4_CR34","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199296453.001.0001","volume-title":"The philosophy of mathematical practice","author":"P Mancosu","year":"2008","unstructured":"Mancosu, P. (2008). The philosophy of mathematical practice. Oxford University Press."},{"key":"4_CR35","unstructured":"Montesi, F., & Piccolomini d\u2019Aragona, A. (2022). Prawitz\u2019s semantics and Walton\u2019s argument schemes: A tentative reading and application of Kreisel\u2019s informal rigour. In P. Cant\u00f9, B. Halimi, G. Heinzmann, & F. Patras (Eds.), Objectivity in mathematics, special issue of noesis. No\u00e9sis."},{"issue":"1","key":"4_CR36","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/philmat\/7.1.5","volume":"7","author":"Y Rav","year":"1999","unstructured":"Rav, Y. (1999). Why do we prove theorems? Philosophy of Mathematics, 7(1), 5\u201341.","journal-title":"Philosophy of Mathematics"},{"issue":"2","key":"4_CR37","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W W Tait","year":"1967","unstructured":"Tait, W. W. (1967). Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic, 32(2), 198\u2013212.","journal-title":"The Journal of Symbolic Logic"},{"issue":"20","key":"4_CR38","doi-asserted-by":"publisher","first-page":"2048","DOI":"10.1016\/j.tcs.2010.12.026","volume":"412","author":"K Terui","year":"2011","unstructured":"Terui, K. (2011). Computational ludics. Theoretical Computer Science, 412(20), 2048\u20132071.","journal-title":"Theoretical Computer Science"},{"key":"4_CR39","unstructured":"Troelstra, A. S. (1996). Introduction to G\u00f6del 58 and G\u00f6del 72. In CWII (p. 234)."},{"key":"4_CR40","unstructured":"Van Atten, M. (forthcoming). Natural constructive proofs of A via $$A\\rightarrow B$$, proof paradoxes, and impredicativity."},{"key":"4_CR41","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511753336","volume-title":"What are philosophical systems?","author":"J Vuillemin","year":"1986","unstructured":"Vuillemin, J. (1986). What are philosophical systems? Cambridge University Press"},{"key":"4_CR42","unstructured":"Vuillemin, J. (1996). Necessity or contingency: The master argument. Center for the study of language and information. Chicago University Press (First french edition, Les \u00e9ditions de minuit, 1984)."},{"key":"4_CR43","volume-title":"From mathematics to philosophy","author":"H Wang","year":"1974","unstructured":"Wang, H. (1974). From mathematics to philosophy. Routledge & Kegan Paul."},{"key":"4_CR44","volume-title":"Logical journey From G\u00f6del to philosophy","author":"H Wang","year":"1996","unstructured":"Wang, H. (1996). Logical journey From G\u00f6del to philosophy. MIT Press."}],"container-title":["Synthese Library","Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-51406-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,1]],"date-time":"2024-04-01T20:19:48Z","timestamp":1712002788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-51406-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,13]]},"ISBN":["9783031514050","9783031514067"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-51406-7_4","relation":{},"ISSN":["0166-6991","2542-8292"],"issn-type":[{"type":"print","value":"0166-6991"},{"type":"electronic","value":"2542-8292"}],"subject":[],"published":{"date-parts":[[2023,12,13]]},"assertion":[{"value":"13 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}