{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T21:47:11Z","timestamp":1763070431070},"reference-count":6,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8412,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1991,3]]},"abstract":"<jats:p>In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)\u2014full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.<\/jats:p><jats:p>The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for \u2228 and \u2203 restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.<\/jats:p><jats:p>A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.<\/jats:p><jats:p>The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.<\/jats:p><jats:p>The notion \u201cvalidity\u201d is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to \u201cvalidity\u201d have been used earlier by Tait (convertability), Girard (r\u00e9ducibilit\u00e9) and Martin-L\u00f6f (computability).<\/jats:p><jats:p>In Prawitz [2] the N.D. system is restricted in the sense that \u2228 and \u2203 are not treated as primitive logical constants, and hence the deductions can only be seen to be \u201cnatural\u201d with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for \u2228 and \u2203 in the restricted system does not imply the normalization theorem for the full system.<\/jats:p>","DOI":"10.2307\/2274910","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:38:25Z","timestamp":1146940705000},"page":"129-149","source":"Crossref","is-referenced-by-count":38,"title":["Normalization theorems for full first order classical natural deduction"],"prefix":"10.1017","volume":"56","author":[{"given":"Gunnar","family":"St\u00e5lmarck","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200024968_ref005","first-page":"626","volume":"52","author":"Seldin","year":"1986","journal-title":"On the proof theory of the intermediate logic MH"},{"key":"S0022481200024968_ref001","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19790250102"},{"key":"S0022481200024968_ref004","first-page":"11","volume-title":"Atti del Congresso Nazionale di Logica (Montecatini, 1979)","author":"Prawitz"},{"key":"S0022481200024968_ref002","volume-title":"Natural deduction","author":"Prawitz","year":"1965"},{"key":"S0022481200024968_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"S0022481200024968_ref006","unstructured":"Statman R. [1], Structural complexity of proofs, Ph.D. thesis, Stanford University, Stanford, California, 1974."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200024968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T18:36:37Z","timestamp":1558118197000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200024968\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,3]]},"references-count":6,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,3]]}},"alternative-id":["S0022481200024968"],"URL":"https:\/\/doi.org\/10.2307\/2274910","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,3]]}}}