{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:02Z","timestamp":1753889702958,"version":"3.41.2"},"reference-count":28,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2010,12,22]],"date-time":"2010-12-22T00:00:00Z","timestamp":1292976000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Goedel's completeness theorem is concerned with provability, while Girard's\ntheorem in ludics (as well as full completeness theorems in game semantics) are\nconcerned with proofs. Our purpose is to look for a connection between these\ntwo disciplines. Following a previous work [3], we consider an extension of the\noriginal ludics with contraction and universal nondeterminism, which play dual\nroles, in order to capture a polarized fragment of linear logic and thus a\nconstructive variant of classical propositional logic. We then prove a\ncompleteness theorem for proofs in this extended setting: for any behaviour\n(formula) A and any design (proof attempt) P, either P is a proof of A or there\nis a model M of the orthogonal of A which defeats P. Compared with proofs of\nfull completeness in game semantics, ours exhibits a striking similarity with\nproofs of Goedel's completeness, in that it explicitly constructs a\ncountermodel essentially using Koenig's lemma, proceeds by induction on\nformulas, and implies an analogue of Loewenheim-Skolem theorem.<\/jats:p>","DOI":"10.2168\/lmcs-6(4:11)2010","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T13:29:57Z","timestamp":1316784597000},"source":"Crossref","is-referenced-by-count":2,"title":["On the meaning of logical completeness"],"prefix":"10.46298","volume":"Volume 6, Issue 4","author":[{"given":"Michele","family":"Basaldella","sequence":"first","affiliation":[]},{"given":"Kazushige","family":"Terui","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2010,12,22]]},"reference":[{"key":"10.2168\/LMCS-6(4:11)2010_Andreoli","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"10.2168\/LMCS-6(4:11)2010_Bar","unstructured":"Barendregt, H. P.: The lambda calculus: its syntax and semantics. North-Holland (1981)."},{"key":"10.2168\/LMCS-6(4:11)2010_Basaldella09","unstructured":"Basaldella, M., Faggian, C.: Ludics with repetition (exponentials, interactive types and completeness). In: LICS. (2009) 375-384."},{"key":"10.2168\/LMCS-6(4:11)2010_Bohm","unstructured":"B\u00f6hm, C.: Alcune propriet\u00e0 delle forme\\beta-\\eta-normali nel\u03bb-K-calcolo. Publicazioni dell'Istituto per le Applicazioni del Calcolo \\textbf696 (1968). Boudes, P.: Non-Uniform Hypercoherences. Electr. Notes Theor. Comput. Sci. \\textbf69 (2002) 62-82."},{"key":"10.2168\/LMCS-6(4:11)2010_BucEhr","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/mscs\/Curien98","unstructured":"Curien, P.-L.: Abstract B\u00f6hm trees. Math. Struct. in Comp. Sci. 8(6) (1998) 559-591."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/corr\/abs-cs-0501039","unstructured":"Curien, P.-L.: Introduction to linear logic and ludics, part II. Advances in Mathematics (China) 35(1) (2006) 1-44."},{"key":"10.2168\/LMCS-6(4:11)2010_Curiennote","unstructured":"Curien, P.-L.: Notes on game semantics. Manuscript (2006)."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/corr\/abs-0706-2544","unstructured":"Curien, P.-L., Herbelin, H.: Abstract machines for dialogue games. Panoramas et Synth\u00e8ses 27 (2009) 231-275."},{"key":"10.2168\/LMCS-6(4:11)2010_curmac","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Munch-Maccagnoni, G.: The duality of computation under focus. In : Proc. of IFIP TCS. (2010).","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"10.2168\/LMCS-6(4:11)2010_Dezani-Intrigila-Venturini:ICTCS-98","unstructured":"Dezani-Ciancaglini, M., Intrigila, B., Venturini-Zilli, M.: B\u00f6hm's theorem for B\u00f6hm trees. In: ICTCS'98. (1998) 1-23."},{"key":"10.2168\/LMCS-6(4:11)2010_Ehr","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.003"},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:conf\/csl\/Faggian02","unstructured":"Faggian, C.: Travelling on designs. In: CSL. (2002) 427-441."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/tcs\/Faggian06","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.042"},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:conf\/tlca\/FaggianP07","unstructured":"Faggian, C., Piccolo, M.: Ludics is a model for the finitary linear pi-calculus. In: TLCA. (2007) 148-162."},{"key":"10.2168\/LMCS-6(4:11)2010_FP09","unstructured":"Faggian, C., Piccolo, M.: Partial Orders, Event Structures, and Linear Strategies. In: TLCA. (2009) 95-111."},{"key":"10.2168\/LMCS-6(4:11)2010_Girard99b","unstructured":"Girard, J.-Y.: On the meaning of logical rules I: syntax vs. semantics. In Berger, U., Schwichtenberg, H., eds.: Computational Logic. Heidelberg Springer-Verlag (1999) 215-272."},{"key":"10.2168\/LMCS-6(4:11)2010_Girard00","unstructured":"Girard, J.-Y.: On the meaning of logical rules II: multiplicatives and additives. Foundation of Secure Computation, Berger and Schwichtenberg edts (2000) 183-212."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/mscs\/Girard01","unstructured":"Girard, J.-Y.: Locus solum: From the rules of logic to the logic of rules. Math. Struct. in Comp. Sci. 11(3) (2001) 301-506."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/iandc\/HylandO00","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/jsyml\/Lafont97","doi-asserted-by":"publisher","DOI":"10.2307\/2275637"},{"key":"10.2168\/LMCS-6(4:11)2010_LaurentThesis","unstructured":"Laurent, O.: \u00c9tude de la polarization en logique. PhD thesis, Univ. Aix-Marseille II (2002)."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:journals\/apal\/Laurent04","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.006"},{"key":"10.2168\/LMCS-6(4:11)2010_MauTh","unstructured":"Maurel, F.: Un cadre quantitatif pour la Ludique. PhD Thesis, Univ. Paris VII (2004)."},{"key":"10.2168\/LMCS-6(4:11)2010_DBLP:conf\/lpar\/MazzaP07","unstructured":"Mazza, D., Pagani, M.: The separation theorem for differential interaction nets. In: LPAR. (2007) 393-407."},{"key":"10.2168\/LMCS-6(4:11)2010_Mellies","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.016"},{"key":"10.2168\/LMCS-6(4:11)2010_Schutte56","unstructured":"Sch\u00fctte, K.: Ein System des Verkn\u00fcpfenden Schliessens. Archiv. Math. Logic Grundlagenf. 2 (1956) 55-67."},{"key":"10.2168\/LMCS-6(4:11)2010_Terui08","unstructured":"Terui, K.: Computational ludics. (2008) To appear in Theor. Comput. Sci."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1066\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1066\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:29Z","timestamp":1681243349000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1066"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,22]]},"references-count":28,"URL":"https:\/\/doi.org\/10.2168\/lmcs-6(4:11)2010","relation":{"is-same-as":[{"id-type":"arxiv","id":"1011.1625","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1011.1625","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2010,12,22]]},"article-number":"1066"}}