{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,25]],"date-time":"2023-09-25T15:53:53Z","timestamp":1695657233403},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2010,6,3]],"date-time":"2010-06-03T00:00:00Z","timestamp":1275523200000},"content-version":"unspecified","delay-in-days":2,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2010,6]]},"abstract":"<jats:p>Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum\u2013Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar St\u00e5lmarck.<\/jats:p>","DOI":"10.1017\/s175502030999030x","type":"journal-article","created":{"date-parts":[[2010,6,3]],"date-time":"2010-06-03T13:32:02Z","timestamp":1275571922000},"page":"175-227","source":"Crossref","is-referenced-by-count":8,"title":["SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS"],"prefix":"10.1017","volume":"3","author":[{"given":"PETER","family":"MILNE","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2010,6,3]]},"reference":[{"key":"S175502030999030X_ref27","volume-title":"Basic Proof Theory","author":"Troelstra","year":"1996"},{"key":"S175502030999030X_ref9","first-page":"119","article-title":"Der Minimalkalk\u00fcl, ein reduzierter intuitionistischer Formalismus","volume":"4","author":"Johansson","year":"1937","journal-title":"Compositio Mathematica"},{"key":"S175502030999030X_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00296-1"},{"key":"S175502030999030X_ref10","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1955.tb00250.x"},{"key":"S175502030999030X_ref26","doi-asserted-by":"publisher","DOI":"10.2307\/2270047"},{"key":"S175502030999030X_ref2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093870624"},{"key":"S175502030999030X_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2270260"},{"key":"S175502030999030X_ref5","volume-title":"Intuitionist Logic, Model Theory and Forcing","author":"Fitting","year":"1969"},{"key":"S175502030999030X_ref14","first-page":"30","article-title":"Untersuchungen \u00fcber den Ausagenkalk\u00fcl","volume":"23","author":"Lukasiewicz","year":"1930","journal-title":"Comptes rendues des s\u00e9ances de la Soci\u00e9t\u00e9 des Sciences et des Lettres de Varsovie"},{"key":"S175502030999030X_ref17","volume-title":"Natural Deduction: A Proof-Theoretical Study. Stockholm","author":"Prawitz","year":"1965"},{"key":"S175502030999030X_ref1","first-page":"174","article-title":"A note on the intuitionist and the classical propositional calculus","volume":"11","author":"Beth","year":"1960","journal-title":"Logique et Analyse"},{"key":"S175502030999030X_ref23","volume-title":"Natural Logic","author":"Tennant","year":"1978"},{"key":"S175502030999030X_ref18","volume-title":"Essays on Mathematical and Philosophical Logic","author":"Prawitz","year":"1979"},{"key":"S175502030999030X_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2977-2"},{"key":"S175502030999030X_ref25","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093956429"},{"key":"S175502030999030X_ref24","volume-title":"The Taming of the True","author":"Tennant","year":"1997"},{"key":"S175502030999030X_ref3","volume-title":"Foundations of Mathematical Logic","author":"Curry","year":"1963"},{"key":"S175502030999030X_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2964545"},{"key":"S175502030999030X_ref4","volume-title":"The Logical Basis of Metaphysics","author":"Dummett","year":"1991"},{"key":"S175502030999030X_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S175502030999030X_ref19","volume-title":"Formal Logic","author":"Prior","year":"1962"},{"key":"S175502030999030X_ref12","volume-title":"Existence, Truth, and Provability","author":"Leblanc","year":"1982"},{"key":"S175502030999030X_ref15","first-page":"273","volume-title":"Logical Environments","author":"Parigot","year":"1993"},{"key":"S175502030999030X_ref16","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093958754"},{"key":"S175502030999030X_ref21","doi-asserted-by":"publisher","DOI":"10.2307\/2274019"},{"key":"S175502030999030X_ref13","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19660120121"},{"key":"S175502030999030X_ref22","doi-asserted-by":"publisher","DOI":"10.2307\/2274910"},{"key":"S175502030999030X_ref20","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1968.tb00337.x"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S175502030999030X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:43:17Z","timestamp":1556480597000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S175502030999030X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["S175502030999030X"],"URL":"https:\/\/doi.org\/10.1017\/s175502030999030x","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6]]}}}