{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:40Z","timestamp":1725664000873},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:10:40Z","timestamp":1330254640000},"page":"193-204","source":"Crossref","is-referenced-by-count":0,"title":["Weak systems of set theory related to HOL"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Forster","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Barwise, J. [1975] Admissible sets and structures, an approach to definablity theory. Springer-Verlag 1975.","DOI":"10.1007\/978-3-662-11035-5"},{"key":"13_CR2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1090\/conm\/065\/891248","volume":"65","author":"W. Buchholz","year":"1985","unstructured":"Buchholz, W. and Wainer S. [1985] Provably computable functions and the fast-growing hierarchy. Logic and Combinatorics, AMS Contemporary Mathematics v 65 pp 179\u2013198.","journal-title":"AMS Contemporary Mathematics"},{"key":"13_CR3","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A. [1940] A formulation of the simple theory of types. Journal of Symbolic Logic 5 pp. 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR4","first-page":"57","volume":"271","author":"J. Coret","year":"1970","unstructured":"Coret, J. [1970] Sur les cas stratifi\u00e9s du schema de remplacement. Comptes Rendues hebdomadaires des s\u00e9ances de l'Acad\u00e9mie des Sciences de Paris s\u00e9rie A 271 pp. 57\u201360.","journal-title":"Comptes Rendues hebdomadaires des s\u00e9ances de l'Acad\u00e9mie des Sciences de Paris s\u00e9rie A"},{"key":"13_CR5","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1002\/malq.19890350502","volume":"35","author":"T.E. Forster","year":"1989","unstructured":"Forster, T.E. [1989] A second-order theory without a (second-order) model. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik 35 pp. 285\u20136","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"13_CR6","doi-asserted-by":"crossref","first-page":"323","DOI":"10.2307\/2274922","volume":"56","author":"T.E. Forster","year":"1991","unstructured":"Forster, T.E. and Kaye, R.W. [1991] End-extensions preserving power set. Journal of Symbolic Logic 56 pp. 323\u201328.","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR7","unstructured":"Forster, T.E. and Kaye, R.W. [2???] More on the set theory KF. unpublished typescript 24pp."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Holmes, M.R. [1995] The equivalence of NF-style set theories with \u201ctangled\u201d type theories; the construction of \u03c9-models of predicative NF (and more) Journal of Symbolic Logic to appear","DOI":"10.2307\/2275515"},{"key":"13_CR9","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/BF00568059","volume":"19","author":"R.B. Jensen","year":"1969","unstructured":"Jensen, R.B. [1969] On the consistency of a slight(?) modification of Quine's NF. Synthese 19 pp. 250\u201363.","journal-title":"Synthese"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"458","DOI":"10.2307\/2274693","volume":"56","author":"R.W. Kaye","year":"1991","unstructured":"Kaye, R.W. [1991] A generalisation of Specker's theorem on typical ambiguity. Journal of Symbolic Logic 56 pp 458\u2013466","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR11","unstructured":"Kemeny, J. [1949] Type theory vs. Set theory. Ph.D.Thesis, Princeton 1949"},{"key":"13_CR12","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1002\/malq.19750210144","volume":"21","author":"J. Lake","year":"1975","unstructured":"Lake, J. [1975] Comparing Type theory and Set theory. Zeitschrift f\u00fcr Matematischer Logik 21 pp 355\u20136.","journal-title":"Zeitschrift f\u00fcr Matematischer Logik"},{"key":"13_CR13","first-page":"1965","volume":"no 57","author":"A. Levy","year":"1965","unstructured":"Levy, A. [1965] A hierarchy of formul\u00e6 in set theory. Memoirs of the American Mathematical Society no 57, 1965.","journal-title":"Memoirs of the American Mathematical Society"},{"key":"13_CR14","unstructured":"Mathias, A.R.D. [2???] Notes on MacLane Set Theory. unpublished typescript."},{"key":"13_CR15","doi-asserted-by":"crossref","first-page":"136","DOI":"10.2307\/2268946","volume":"18","author":"R. McNaughton","year":"1953","unstructured":"McNaughton, R. [1953] Some formal relative consistency proofs. Journal of Symbolic Logic 18 pp. 136\u201344.","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR16","doi-asserted-by":"crossref","first-page":"111","DOI":"10.4064\/fm-37-1-111-124","volume":"37","author":"A. Mostowski","year":"1950","unstructured":"Mostowski, A. [1950] Some impredicative definitions in the axiomatic set theory. Fundamenta Mathematic\u00e6 v 37 pp 111\u2013124.","journal-title":"Fundamenta Mathematic\u00e6"},{"key":"13_CR17","doi-asserted-by":"crossref","first-page":"87","DOI":"10.4064\/fm-37-1-87-110","volume":"37","author":"I.L. Novak","year":"1950","unstructured":"Novak, I.L. [1950] A construction of models for consistent systems. Fundamenta Mathematic\u00e6 37 pp 87\u2013110","journal-title":"Fundamenta Mathematic\u00e6"},{"key":"13_CR18","unstructured":"Quine, W.v.O. [1951] Mathematical Logic. (2nd ed.) Harvard."},{"key":"13_CR19","unstructured":"Quine, W.v.O [1966] On a application of Tarski's definition of Truth. in Selected Logic Papers pp 141\u20135"},{"key":"13_CR20","first-page":"113","volume":"15","author":"J.B. Rosser","year":"1950","unstructured":"Rosser, J.B. and Wang, H. [1950] Non-standard models for formal logics JSL 15 pp 113\u2013129","journal-title":"Non-standard models for formal logics JSL"},{"key":"13_CR21","first-page":"1026","volume":"21","author":"D. S. Scott","year":"1960","unstructured":"Scott, D. S. [1960] Review of Specker [1958]. Mathematical Reviews 21 p. 1026.","journal-title":"Mathematical Reviews"},{"key":"13_CR22","doi-asserted-by":"crossref","first-page":"21","DOI":"10.2307\/2267646","volume":"19","author":"J. R. Shoenfield","year":"1954","unstructured":"Shoenfield, J. R. [1954] A relative consistency proof Journal of Symbolic Logic 19 pp 21\u201328","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR23","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1111\/j.1746-8361.1958.tb01475.x","volume":"12","author":"E. P. Specker","year":"1958","unstructured":"Specker, E. P. [1958] Dualit\u00e4t. Dialectica 12 pp. 451\u2013465.","journal-title":"Dialectica"},{"key":"13_CR24","unstructured":"Specker, E. P. [1962] Typical ambiguity. In Logic, methodology and philosophy of science. Ed E. Nagel, Stanford."},{"key":"13_CR25","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1073\/pnas.35.3.150","volume":"35","author":"H. Wang","year":"1949","unstructured":"Wang, H. [1949] On Zermelo's and Von Neumann's axioms for set theory. Proc. N. A. S. 35 pp 150\u2013155","journal-title":"Proc. N. A. S."},{"key":"13_CR26","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1090\/S0002-9947-1952-0049136-2","volume":"72","author":"H. Wang","year":"1952","unstructured":"Wang, H. [1952] Truth definitions and consistency proofs. Transactions of the American Mathematical Society 72 pp. 243\u201375. reprinted in Wang: Survey of Mathematical Logic as ch 18","journal-title":"Transactions of the American Mathematical Society"},{"key":"13_CR27","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1093\/mind\/LXI.243.366","volume":"61","author":"H. Wang","year":"1952","unstructured":"Wang, H. [1952a] Negative types. MIND 61 pp. 366\u20138.","journal-title":"MIND"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58450-1_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:21:28Z","timestamp":1605630088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}