{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:44:11Z","timestamp":1700009051496},"reference-count":19,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2008,1,30]],"date-time":"2008-01-30T00:00:00Z","timestamp":1201651200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2008,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper provides a constructive topological semantics for non\u2010deducibility of a first order intuitionistic formula. Formal topology theory, in particular the recently introduced notion of a binary positivity predicate, and co\u2010induction are two needful tools. (\u00a9 2008 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200710026","type":"journal-article","created":{"date-parts":[[2008,1,30]],"date-time":"2008-01-30T14:16:15Z","timestamp":1201702575000},"page":"35-48","source":"Crossref","is-referenced-by-count":2,"title":["A constructive semantics for non\u2010deducibility"],"prefix":"10.1002","volume":"54","author":[{"given":"Francesco","family":"Ciraulo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2008,1,30]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"crossref","unstructured":"G.Boolos The Logic of Provability (Cambridge University Press 1995).","DOI":"10.1017\/CBO9780511625183"},{"key":"e_1_2_1_3_2","unstructured":"L. E. J.Brouwer Brouwer's Cambridge Lectures on Intuitionism (D. van Dalen ed.) (Cambridge University Press 1981)."},{"key":"e_1_2_1_4_2","unstructured":"F.Ciraulo andG.Sambin Finitary formal topologies. Submitted to Theoretical Computer Science (2007)."},{"key":"e_1_2_1_5_2","unstructured":"F.Ciraulo andG.Sambin Finiteness in a minimalistic foundation. In preparation (2007)."},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.2307\/2586694"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","unstructured":"T.Coquand andJ.Smith An application of constructive completeness. In: Types for Proof and Programs International Workshop TYPES'95 (S. Berardi and M. Coppo eds.). Lecture Notes in Computer Science 1158 pp. 46\u201384 (Springer 1996).","DOI":"10.1007\/3-540-61780-9_63"},{"key":"e_1_2_1_9_2","unstructured":"M.Dummet(with the assistance of R. Minio) Elements of Intuitionism (Clarendon Press 1977)."},{"key":"e_1_2_1_10_2","unstructured":"S. C.Kleene Introduction to Metamathematics (North\u2010Holland 1952)."},{"key":"e_1_2_1_11_2","doi-asserted-by":"crossref","unstructured":"M. E.Maietti andG.Sambin Towards a minimalist foundation for constructive mathematics. In: From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics (L. Crosilla and P. Schuster eds.) pp. 91\u2013114. Oxford Logic Guides 48 (Clarendon Press 2005).","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"e_1_2_1_12_2","unstructured":"P.Martin\u2010L\u00f6f Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua June 1980 (Bibliopolis 1984)."},{"key":"e_1_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.2307\/2267135"},{"key":"e_1_2_1_14_2","unstructured":"H.Rasiova andR.Sikorski The Mathematics of Metamathematics (PWN 1963)."},{"key":"e_1_2_1_15_2","doi-asserted-by":"crossref","unstructured":"G.Sambin Intuitionistic formal spaces \u2013 a first comunication. In: Mathematical Logic and Its Applications (D. Skordev ed.) pp. 187\u2013204 (Plenum 1987).","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.2307\/2275761"},{"key":"e_1_2_1_17_2","unstructured":"G.Sambin The Basic Picture. A Structural Basis for Constructive Topology (including two papers with P. Martin\u2010L\u00f6f and with V. Capretta). Oxford University Press to appear in 2008."},{"key":"e_1_2_1_18_2","doi-asserted-by":"crossref","unstructured":"G.Sambin andS.Valentini Building up a toolbox for Martin\u2010L\u00f6f's type theory: subset theory. In: Twenty\u2010Five Years of Constructive Type Theory. Proceedings of a congress held in Venice October 1995 (G. Sambin and J. Smith eds.) pp. 221\u2013244 (Oxford University Press 1998).","DOI":"10.1093\/oso\/9780198501275.003.0014"},{"key":"e_1_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.026"},{"key":"e_1_2_1_20_2","unstructured":"G.Takeuti Proof Theory (North\u2010Holland 1975)."}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200710026","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200710026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T17:52:50Z","timestamp":1699984370000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200710026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,30]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["10.1002\/malq.200710026"],"URL":"https:\/\/doi.org\/10.1002\/malq.200710026","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,30]]}}}