{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:32Z","timestamp":1759017932831,"version":"3.44.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Propositional inquisitive logic is the limit of its <jats:italic>n<\/jats:italic>-bounded approximations. In the predicate setting, however, this does not hold anymore, as discovered by Ciardelli and Grilletti [11], who also found complete axiomatizations of <jats:italic>n<\/jats:italic>-bounded inquisitive logics <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{InqBQ}_{n}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi>InqBQ<\/mml:mi>\n                    <mml:mi>n<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, for every fixed <jats:italic>n<\/jats:italic>. We introduce cut-free labelled sequent calculi for these logics. We illustrate the intricacies of <jats:italic>schematic validity<\/jats:italic> in such systems by showing that the well-known Casari formula is <jats:italic>atomically<\/jats:italic> valid in (a weak sublogic of) predicate inquisitive logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{InqBQ}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>InqBQ<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, fails to be schematically valid in it, and yet is schematically valid under the finite boundedness assumption. The derivations in our calculi, however, are guaranteed to be schematically valid whenever a single specific rule is not used.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_3","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:09Z","timestamp":1758969909000},"page":"39-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Inquisitive Logics: Sequent Calculi and\u00a0Schematic Validity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2240-3161","authenticated-orcid":false,"given":"Tadeusz","family":"Litak","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7780-423X","authenticated-orcid":false,"given":"Katsuhiko","family":"Sano","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s11229-008-9415-6","volume":"167","author":"S Abramsky","year":"2009","unstructured":"Abramsky, S., V\u00e4\u00e4n\u00e4nen, J.A.: From IF to BI. Synthese 167, 207\u2013230 (2009)","journal-title":"Synthese"},{"key":"3_CR2","unstructured":"Casari, E.: Intermediate logics. In: Atti degli incontri di logica matematica 1982, Universit\u00e0 di Siena, pp.\u00a0243\u2013298 (1983)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Chagrov, A.,\u00a0Zakharyaschev, M.: Modal Logic, Number\u00a035 in Oxford Logic Guides. Clarendon Press (1997)","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49, 363\u2013408 (2012). https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"J. Autom. Reason."},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-662-55665-8_36","volume-title":"Logic, Rationality, and Interaction","author":"J Chen","year":"2017","unstructured":"Chen, J., Ma, M.: Labelled sequent calculus for inquisitive logic. In: Baltag, A., Seligman, J., Yamada, T. (eds.) LORI 2017. LNCS, vol. 10455, pp. 526\u2013540. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55665-8_36"},{"key":"3_CR6","unstructured":"Church, A.: Introduction to Mathematical Logic, vol. I, 2nd edn. Princeton (1958)"},{"key":"3_CR7","unstructured":"Ciardelli, I.: Inquisitive Semantics and Intermediate Logics. Master\u2019s thesis, Institute for Logic, Language and Computation, Universiteit van Amsterdam (2009). https:\/\/eprints.illc.uva.nl\/id\/eprint\/818"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-31803-5_8","volume-title":"Dependence Logic","author":"I Ciardelli","year":"2016","unstructured":"Ciardelli, I.: Dependency as question entailment. In: Abramsky, S., Kontinen, J., V\u00e4\u00e4n\u00e4nen, J., Vollmer, H. (eds.) Dependence Logic, pp. 129\u2013181. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-31803-5_8"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s11229-016-1221-y","volume":"195","author":"I Ciardelli","year":"2018","unstructured":"Ciardelli, I.: Questions as information types. Synthese 195, 321\u2013365 (2018)","journal-title":"Synthese"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Ciardelli, I.: Inquisitive Logic: Consequence and Inference in the Realm of Questions. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-09706-5"},{"key":"3_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2022.103155","volume":"173","author":"I Ciardelli","year":"2022","unstructured":"Ciardelli, I., Grilletti, G.: Coherence in inquisitive first-order logic. Ann. Pure Appl. Logic 173, 103155 (2022)","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR12","volume-title":"Inquisitive Semantics","author":"I Ciardelli","year":"2017","unstructured":"Ciardelli, I., Groenendijk, J., Roelofsen, F.: Inquisitive Semantics. Oxford University Press, Oxford (2017)"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s10992-010-9142-6","volume":"40","author":"I Ciardelli","year":"2010","unstructured":"Ciardelli, I., Roelofsen, F.: Inquisitive logic. J. Philos. Log. 40, 55\u201394 (2010)","journal-title":"J. Philos. Log."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Curien, P.-L.,\u00a0Herbelin, H.: The duality of computation. In: Proceedings of ICFP \u201900, pp. 233\u2013243 (2000)","DOI":"10.1145\/351240.351262"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s00153-011-0254-7","volume":"51","author":"R Dyckhoff","year":"2011","unstructured":"Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. Math. Logic 51, 71\u201392 (2011)","journal-title":"Arch. Math. Logic"},{"key":"3_CR16","unstructured":"Elliger, M.O.: Formalization of (bounded) inquisitive first-order logic (2025). https:\/\/motrellin.github.io\/rocq-docs-inquisitive-logic\/"},{"key":"3_CR17","unstructured":"Elliger, M.O.: Inquisitive First-Order Logic Bounded and Mechanized. Master\u2019s thesis, FAU Erlangen-Nuremberg (2025)"},{"key":"3_CR18","first-page":"26","volume":"27","author":"L Esakia","year":"1998","unstructured":"Esakia, L.: Quantification in intuitionistic logic with provability smack. Bull. Sect. Logic 27, 26\u201328 (1998)","journal-title":"Bull. Sect. Logic"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Ferreira, G., Oliva, P.: On the relation between various negative translations. In: Berger, U., Schwichtenberg, H. (eds.) Logic, Construction, Computation, Mathematical Logic Series, vol. 3, pp. 227\u2013258. Ontos-Verlag (2012)","DOI":"10.1515\/9783110324921.227"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-662-52921-8_14","volume-title":"Logic, Language, Information, and Computation","author":"S Frittella","year":"2016","unstructured":"Frittella, S., Greco, G., Palmigiano, A., Yang, F.: A multi-type calculus for inquisitive logic. In: V\u00e4\u00e4n\u00e4nen, J., Hirvonen, \u00c5., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 215\u2013233. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-52921-8_14"},{"key":"3_CR21","unstructured":"Gabbay, D.M.,\u00a0Skvortsov, D.,\u00a0Shehtman, V.: Quantification in Nonclassical Logic, Volume I. In: Studies in Logic and the Foundations of Mathematics, vol. 153. Elsevier (2009)"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2307\/2270260","volume":"36","author":"S G\u00f6rnemann","year":"1971","unstructured":"G\u00f6rnemann, S.: A logic stronger than intuitionism. J. Symb. Logic 36, 249\u2013261 (1971)","journal-title":"J. Symb. Logic"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/s10849-021-09341-y","volume":"30","author":"G Grilletti","year":"2021","unstructured":"Grilletti, G.: Completeness for the classical antecedent fragment of inquisitive first-order logic. J. Logic Lang. Inform. 30, 725\u2013751 (2021)","journal-title":"J. Logic Lang. Inform."},{"key":"3_CR24","volume-title":"Introduction to metamathematics","author":"S Kleene","year":"1952","unstructured":"Kleene, S.: Introduction to metamathematics. North-Holland, Amsterdam-Oxford (1952)"},{"key":"3_CR25","unstructured":"Litak, T.,\u00a0Polzer, M.,\u00a0Rabenstein, U.: Negative translations and normal modality. In:\u00a0Miller, D. (ed.) Proceedings of FSCD 2017, LIPIcs, vol. 84, pp. 27:1\u201327:18 (2017). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/7741"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"1099","DOI":"10.2307\/2274476","volume":"55","author":"P Minari","year":"1990","unstructured":"Minari, P., Takano, M., Ono, H.: Intermediate predicate logics determined by ordinals. J. Symb. Logic 55, 1099\u20131124 (1990)","journal-title":"J. Symb. Logic"},{"key":"3_CR27","unstructured":"M\u00fcller, V.: On the proof theory of inquisitive logic. Master\u2019s thesis, Institute for Logic, Language and Computation, Universiteit van Amsterdam (2023). https:\/\/eprints.illc.uva.nl\/id\/eprint\/2278"},{"key":"3_CR28","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S Negri","year":"2005","unstructured":"Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34, 507\u2013544 (2005)","journal-title":"J. Philos. Log."},{"key":"3_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., Von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)"},{"key":"3_CR30","unstructured":"Ono, H.: A Study of Intermediate Predicate Logics. Ph.D. thesis, Kyoto University (1973). http:\/\/hdl.handle.net\/2433\/86490"},{"key":"3_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-023-10093-y","author":"M Rybakov","year":"2024","unstructured":"Rybakov, M., Shkatov, D.: Variations on the Kripke trick. Stud. Logica. (2024). https:\/\/doi.org\/10.1007\/s11225-023-10093-y","journal-title":"Stud. Logica."},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-18026-2_13","volume-title":"Logic and Its Applications","author":"K Sano","year":"2011","unstructured":"Sano, K.: First-order inquisitive pair logic. In: Banerjee, M., Seth, A. (eds.) ICLA 2011. LNCS (LNAI), vol. 6521, pp. 147\u2013161. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18026-2_13"},{"key":"3_CR33","unstructured":"Sano, K.,\u00a0Virtema, J.: Axiomatizing propositional dependence logics. In:\u00a0Kreutzer, S. (ed.) Proceedings of CSL, LIPIcs, pp. 292\u2013307 (2015)"},{"key":"3_CR34","unstructured":"S\u00f8rensen, M.H.,\u00a0Urzyczyn, P.: Lectures on the curry-howard isomorphism. Stud. Logic Found. Math. 149 (2006)"},{"key":"3_CR35","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"3_CR36","unstructured":"Troelstra, A.S.,\u00a0van Dalen, D.: Constructivism in mathematics: an introduction. Stud. Logic Found. Math. 121 (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:12Z","timestamp":1758969912000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}