caa a22 4500 465743684 CHVBK 20180323111814.0 cr unu---uuuuu 170327e19900701xx s 000 0 eng 10.1007/BF01792983 doi (NATIONALLICENCE)springer-10.1007/BF01792983 On some formalized conservation results in arithmetic [Elektronische Daten] [P. Clote, P. Hájek, J. Paris] IΣ n andBΣ n are well known fragments of first-order arithmetic with induction and collection forΣ n formulas respectively;IΣ n 0 andBΣ n 0 are their second-order counterparts. RCA0 is the well known fragment of second-order arithmetic with recursive comprehension;WKL 0 isRCA 0 plus weak König's lemma. We first strengthen Harrington's conservation result by showing thatWKL 0 +BΣ n 0 is Π 1 1 -conservative overRCA 0 +BΣ n 0 . Then we develop some model theory inWKL 0 and illustrate the use of formalized model theory by giving a relatively simple proof of the fact thatIΣ 1 provesBΣ n+1 to be Π n+2-conservative overIΣ n . Finally, we present a proof-theoretic proof of the stronger fact that theΠ n+2 conservation result is provable already inIΔ 0 + superexp. ThusIΣ n+1 proves 1-Con (BΣ n+1) andIΔ 0 +superexp proves Con (IΣ n )↔Con(BΣ n+1). Springer-Verlag, 1990 Clote P. Department of Computer Science, Boston College, 02167, Chestnut Hill, MA, USA aut Hájek P. Institute of Mathematics CSAV, Zitna 25, CS-11567, Praha, Czechoslovakia aut Paris J. Department of Mathematics, University of Manchester, M139PL, Manchester, UK aut Archive for Mathematical Logic Springer-Verlag 30/4(1990-07-01), 201-218 0933-5846 30:4<201 1990 30 153 https://doi.org/10.1007/BF01792983 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF01792983 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Clote P. Department of Computer Science, Boston College, 02167, Chestnut Hill, MA, USA aut NATIONALLICENCE 700 1- Hájek P. Institute of Mathematics CSAV, Zitna 25, CS-11567, Praha, Czechoslovakia aut NATIONALLICENCE 700 1- Paris J. Department of Mathematics, University of Manchester, M139PL, Manchester, UK aut NATIONALLICENCE 773 0- Archive for Mathematical Logic Springer-Verlag 30/4(1990-07-01), 201-218 0933-5846 30:4<201 1990 30 153 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer