{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T14:57:09Z","timestamp":1780498629326,"version":"3.54.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2015,6,11]],"date-time":"2015-06-11T00:00:00Z","timestamp":1433980800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Synthese"],"published-print":{"date-parts":[[2019,7]]},"DOI":"10.1007\/s11229-015-0784-3","type":"journal-article","created":{"date-parts":[[2015,6,11]],"date-time":"2015-06-11T06:10:02Z","timestamp":1434003002000},"page":"2671-2693","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["The middle ground-ancestral logic"],"prefix":"10.1007","volume":"196","author":[{"given":"Liron","family":"Cohen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arnon","family":"Avron","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,6,11]]},"reference":[{"key":"784_CR1","doi-asserted-by":"crossref","unstructured":"Aho, A.\u00a0V., & Ullman, J.\u00a0D. (1979). Universality of data retrieval languages. In Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on principles of programming languages, (pp. 110\u2013119). ACM.","DOI":"10.1145\/567752.567763"},{"key":"784_CR2","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-94-017-0253-9_7","volume-title":"Thirty five years of automating mathematics, applied logic series","author":"A Avron","year":"2003","unstructured":"Avron, A. (2003). Transitive closure and the mechanization of mathematics. In Fairouz D. Kamareddine (Ed.), Thirty five years of automating mathematics, applied logic series (Vol. 28, pp. 149\u2013171). Netherlands: Springer."},{"key":"784_CR3","doi-asserted-by":"crossref","unstructured":"Avron, A. (2004). Formalizing set theory as it is actually used. In Mathematical knowledge management, (pp. 32\u201343). Springer.","DOI":"10.1007\/978-3-540-27818-4_3"},{"key":"784_CR4","doi-asserted-by":"crossref","unstructured":"Avron, A. (2008). A framework for formalizing set theories based on the use of static set terms. In Pillars of computer science, (pp. 87\u2013106). Springer.","DOI":"10.1007\/978-3-540-78127-1_6"},{"key":"784_CR5","unstructured":"Campbell, J. J. J. A., Dos Reis, J. C. G., Wenzel, P. S. M., & Sorge, V. (2008). Intelligent computer mathematics."},{"key":"784_CR6","first-page":"137","volume-title":"Logic, language, information, and computation, volume 8652 of lecture notes in computer science","author":"Liron Cohen","year":"2014","unstructured":"Cohen, Liron, & Avron, Arnon. (2014). Ancestral logic: A proof theoretical study. In U. Kohlenbach, et al. (Eds.), Logic, language, information, and computation, volume 8652 of lecture notes in computer science (pp. 137\u2013151). Berlin, Heidelberg: Springer."},{"key":"784_CR7","volume-title":"Implementing mathematics with the Nuprl proof development system","author":"RL Constable","year":"1986","unstructured":"Constable, R. L., Allen, S. F., Bromley, M., Cleaveland, R., Cremer, J. F., Harper, R. W., et al. (1986). Implementing mathematics with the Nuprl proof development system. Upper Saddle River: Prentice Hall."},{"key":"784_CR8","first-page":"435","volume":"203","author":"JJ Da Silva","year":"1999","unstructured":"Da Silva, J. J., D\u2019Ottaviano, I. M. L., & Sette, A. M. (1999). Translations between logics. Lecture Notes in Pure and Applied Mathematics, 203, 435\u2013448.","journal-title":"Lecture Notes in Pure and Applied Mathematics"},{"key":"784_CR9","volume-title":"On g\u00f6del\u2019s modal interpretation of the intuitionistic logic. Universal Logic: An anthology","author":"IML D\u2019Ottaviano","year":"2012","unstructured":"D\u2019Ottaviano, I. M. L., & Feitosa, H. A. (2012). On g\u00f6del\u2019s modal interpretation of the intuitionistic logic. Universal Logic: An anthology. Basel: Birkh\u00e4user."},{"key":"784_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28788-4","volume-title":"Finite model theory","author":"H-D Ebbinghaus","year":"1995","unstructured":"Ebbinghaus, H.-D., Flum, J., & Ebbinghaus, H.-D. (1995). Finite model theory (Vol. 2). New York: Springer."},{"key":"784_CR11","unstructured":"Fagin, R. (1974). Generalized first-order spectra and polynomial-time recognizable sets. In R. Karp (Ed.), SIAM-AMS Proceedings 7, (pp. 27\u201341). Immerman."},{"key":"784_CR12","unstructured":"Gentzen, G. (1969). Neue fassung des widerspruchsfreiheitsbeweises f\u00fcr die reine zahlentheorie, forschungen zur logik. 4:19\u201344. (M. E. Szabo, English Trans.). The collected work of Gerhard Gentzen, Amsterdam."},{"issue":"1","key":"784_CR13","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G. (1935). Untersuchungen \u00fcber das logische schlie\u00dfen. i. Mathematische Zeitschrift, 39(1), 176\u2013210.","journal-title":"Mathematische Zeitschrift"},{"key":"784_CR14","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BF01564760","volume":"119","author":"G Gentzen","year":"1943","unstructured":"Gentzen, G. (1943). Beweisbarkeit und unbeweisbarkeit von anfangsf\u00e4llen der transfiniten induktion in der reinen zahlentheorie. Mathematische Annalen, 119, 140\u2013161.","journal-title":"Mathematische Annalen"},{"key":"784_CR15","volume-title":"Infinistic methods","author":"L Henkin","year":"1961","unstructured":"Henkin, L. (1961). Some remarks on infinitely long formulas. In L. Henkin (Ed.), Infinistic methods. New York: Pergamon Press."},{"key":"784_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0253-9","volume-title":"Thirty five years of automating mathematics","author":"FD Kamareddine","year":"2003","unstructured":"Kamareddine, F. D. (2003). Thirty five years of automating mathematics (Vol. 28). New York: Springer."},{"issue":"1","key":"784_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267976","volume":"8","author":"RM Martin","year":"1943","unstructured":"Martin, R. M. (1943). A homogeneous system for formal logic. The Journal of Symbolic Logic, 8(1), 1\u201323.","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"784_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.2307\/2268974","volume":"14","author":"RM Martin","year":"1949","unstructured":"Martin, R. M. (1949). A note on nominalism and recursive functions. The Journal of Symbolic Logic, 14(1), 27\u201331.","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"784_CR19","doi-asserted-by":"publisher","first-page":"192","DOI":"10.2307\/2267692","volume":"17","author":"J Myhill","year":"1952","unstructured":"Myhill, J. (1952). A derivation of number theory from ancestral theory. The Journal of Symbolic Logic, 17(3), 192\u2013197.","journal-title":"The Journal of Symbolic Logic"},{"key":"784_CR20","volume-title":"Proof theory: The first step into impredicativity","author":"W Pohlers","year":"2009","unstructured":"Pohlers, W. (2009). Proof theory: The first step into impredicativity. New York: Springer."},{"key":"784_CR21","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0049-237X(08)70527-5","volume-title":"Contributions to mathematical logic, proceedings of the logic colloquium, Hannover 1966","author":"D Prawitz","year":"1968","unstructured":"Prawitz, D., & Malmn\u00e4s, P.-E. (1968). A survey of some connections between classical, intuitionistic and minimal logic. In H. Arnold Schmidt, K. Sch\u00fctte, & H. J. Thiele (Eds.), Contributions to mathematical logic, proceedings of the logic colloquium, Hannover 1966 (pp. 215\u2013229). North-Holland: North-Holland Publishing Company."},{"key":"784_CR22","unstructured":"Rudnicki, P. (1992). An overview of the mizar project. In Proceedings of the 1992 workshop on types for proofs and programs, (pp. 311\u2013330)."},{"key":"784_CR23","volume-title":"Foundations without foundationalism: A case for second-order logic","author":"S Shapiro","year":"1991","unstructured":"Shapiro, S. (1991). Foundations without foundationalism: A case for second-order logic. Oxford: Oxford University Press."},{"issue":"297","key":"784_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/analys\/68.1.1","volume":"68","author":"P Smith","year":"2008","unstructured":"Smith, P. (2008). Ancestral arithmetic and Isaacson\u2019s thesis. Analysis, 68(297), 1\u201310.","journal-title":"Analysis"},{"key":"784_CR25","volume-title":"Proof theory","author":"G Takeuti","year":"2013","unstructured":"Takeuti, G. (2013). Proof theory. Mineola: Courier Dover Publications."},{"key":"784_CR26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic proof theory number 43","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory number 43. Cambridge: Cambridge University Press."},{"issue":"4","key":"784_CR27","doi-asserted-by":"publisher","first-page":"617","DOI":"10.2307\/2269697","volume":"31","author":"M Yasuhara","year":"1966","unstructured":"Yasuhara, M. (1966). Syntactical and semantical properties of generalized quantifiers. The Journal of Symbolic Logic, 31(4), 617\u2013632.","journal-title":"The Journal of Symbolic Logic"}],"container-title":["Synthese"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11229-015-0784-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11229-015-0784-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11229-015-0784-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11229-015-0784-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T10:04:39Z","timestamp":1561457079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11229-015-0784-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,11]]},"references-count":27,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2019,7]]}},"alternative-id":["784"],"URL":"https:\/\/doi.org\/10.1007\/s11229-015-0784-3","relation":{},"ISSN":["0039-7857","1573-0964"],"issn-type":[{"value":"0039-7857","type":"print"},{"value":"1573-0964","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,11]]},"assertion":[{"value":"7 March 2014","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 May 2015","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 June 2015","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}