{"entities":{"Q1264147":{"pageid":1274897,"ns":120,"title":"Item:Q1264147","lastrevid":70031817,"modified":"2026-04-13T11:58:16Z","type":"item","id":"Q1264147","labels":{"en":{"language":"en","value":"On some formalized conservation results in arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4128807"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$662A7D0A-63AA-4CBD-BD32-C1CF1B9E069D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ad4bf6407c2811e0a15e6400a064854decad26a7","datavalue":{"value":{"text":"On some formalized conservation results in arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1264147$0142F61B-A95E-4A50-BC65-A79036239E5D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d6d23ce093ca4169a0e5082b2cc90c518cdc4ce4","datavalue":{"value":"0689.03027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$5C689E1E-347D-4B5B-A49F-37BA08287750","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a7b7051f4b4fd2ea0976c4b5dd85fd583d8dfd3f","datavalue":{"value":"10.1007/BF01792983","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$6CEE0CF7-F0B3-48CA-93D6-D322A7195C9B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$46B066F9-7005-4303-B1D3-3EAB22825C19","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1264147$EEAB435F-A3E1-4E17-B2A4-B6A5709D4931","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"736af71f3a1a915b4dc9dda4d78d222e2f2a6079","datavalue":{"value":"I\\(\\Sigma_ n\\) and \\(B\\Sigma_ n\\) are well known fragments of first-order arithmetic with induction and collection for \\(\\Sigma_ n\\) formulas respectively; \\(I\\Sigma^ 0_ n\\) and \\(B\\Sigma^ 0_ n\\) allow free second-order variables. \\(RCA_ 0\\) is the well known fragment of second- order arithmetic with recursive comprehension; \\(WKL_ 0\\) is \\(RCA_ 0\\) plus weak K\u00f6nig's lemma. We first strengthen Harrington's conservation result by showing that \\(WKL_ 0+B\\Sigma^ 0_ n\\) is \\(\\Pi^ 1_ 1\\)- conservative over \\(RCA_ 0+B\\Sigma^ 0_ n\\). Then we develop some model theory in \\(WKL_ 0\\) and illustrate the use of formalized model theory by giving a relatively simple proof of the fact that \\(I\\Sigma_ 1\\) proves \\(B\\Sigma_{n+1}\\) to be \\(\\Pi_{n+2}\\)-conservative over \\(I\\Sigma_ n\\). Finally, we present a proof-theoretic proof of the stronger fact that the \\(\\Pi_{n+2}\\) conservation result is provable already in \\(I\\Delta_ 0+\\sup er\\exp\\). Thus \\(I\\Sigma_{n+1}\\) proves \\(1\\)- Con(B\\(\\Sigma_{n+1})\\) and \\(I\\Delta_ 0+\\sup er\\exp\\) proves \\(Con(I\\Sigma_ n)\\leftrightarrow Con(B\\Sigma_{n+1})\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$CDEA40A4-C5EC-4771-8282-B256D33971E0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$CEE29C4B-79BA-4FE9-81A8-65DA11B075E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$7F80E02A-83DB-4FA2-A917-232D0A3A7FF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a22eb1f642cbb79777784e33676c61b720925aab","datavalue":{"value":"03H15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$304CCD07-FBBD-4CBD-B253-FB9E3296D411","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6bef537350d6a99250595c6e5a67c8b10bbad923","datavalue":{"value":"4128807","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$EDF349DB-BAF3-4A3A-9386-9869AB9A8829","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$7C911C5A-BFEE-4EE6-8365-131E6E80BD3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d83c0141a374ed2e054ebffd40fdcc576c0dab7","datavalue":{"value":"conservation results","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$1CF2DA65-5849-4906-9980-5F9EE5D2167D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"86883f625eb9ea1d0f9d5e4e00110dbc1e213e44","datavalue":{"value":"conservative extension","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$EAE9C799-9978-4705-9324-20186B2617C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4f2cf44b91718f77342610b1ab162b240d8995e","datavalue":{"value":"fragments of first-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$EA81A5C9-53C3-4039-9D37-DC85627A1165","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a603503db2f87cdeb7f9640fabaefa6010706904","datavalue":{"value":"fragment of second-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$3D652820-6A2E-4BEB-BF3A-8C189C8660CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73f4fd1aafbd3489f712999162cef0d128973de6","datavalue":{"value":"formalized model theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1264147$1085556E-10DC-4314-BD07-9C4145F5A3C0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"156c797a905a5f3fee298ee2b9f132ba806e98a8","datavalue":{"value":{"entity-type":"item","numeric-id":455764,"id":"Q455764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$0F590816-0ED5-448C-8D11-ABC9133CC709","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b6f60fe646c044641a88e51c899da6e67b19d59e","datavalue":{"value":{"entity-type":"item","numeric-id":195656,"id":"Q195656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$9A6CB8E0-6E86-4AD6-80D6-7E8027241D9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"44176704c420391b1ec646932fc59126c7d2f6cf","datavalue":{"value":{"entity-type":"item","numeric-id":264026,"id":"Q264026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$9BD8FC75-B04B-407B-B5B7-BD0C6CCEF09C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"af7a6817238379ba945f4c57a8ee8caebc5f2605","datavalue":{"value":{"entity-type":"item","numeric-id":455764,"id":"Q455764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$74831B18-023F-44B7-BEA2-67DE89E22666","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$47B30EC8-12DA-4497-85B9-C496E50DFAA1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a628cb64400cb3daffe7c8b3b6a4710e9daa6946","datavalue":{"value":{"entity-type":"item","numeric-id":3800030,"id":"Q3800030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$C6A936B1-FBC9-4454-BA1A-20C6E510D42B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aea8c1f5940a40e8655aa16d1c0ac9365c9d64b7","datavalue":{"value":{"entity-type":"item","numeric-id":3682484,"id":"Q3682484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$975908F3-1B53-42B5-BF16-57E588570AF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"061ecde0fd4a3494ae34993741cb7e05fda5f058","datavalue":{"value":{"entity-type":"item","numeric-id":3754621,"id":"Q3754621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$7A078361-EE5D-4D08-9FF6-3143D2718E01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f5870f15efa3f27de13ad18b4318700e6b85dd6","datavalue":{"value":{"entity-type":"item","numeric-id":4140973,"id":"Q4140973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$51C9360A-77CC-4DFD-98D9-3BEE4D04AFB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b6e4157373fd58274a40973fa66ad7b141c13cd","datavalue":{"value":{"entity-type":"item","numeric-id":3962995,"id":"Q3962995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$B4BD2616-67EA-4DDF-B2F3-135C1B13E3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"881604e64fafe5c870e7bacf59149bf554d04387","datavalue":{"value":{"entity-type":"item","numeric-id":3788005,"id":"Q3788005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$CB60A5A1-6CBB-4F8C-B587-2D01A649B0DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86108cb677c98bb6850d4621a5c75e6c35903675","datavalue":{"value":{"entity-type":"item","numeric-id":5677474,"id":"Q5677474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$C8935AF5-FDF6-4571-953F-7376A8AF9FD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67d50a6440eaa1049510fa09b2cfcd0990921ddc","datavalue":{"value":{"entity-type":"item","numeric-id":3481685,"id":"Q3481685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$9270A317-64BE-42A7-9DC9-E792743FF367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f75404b85aec9d3f8d81a90cf7f18337600389e","datavalue":{"value":{"entity-type":"item","numeric-id":3884109,"id":"Q3884109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$6EBDF6E8-238B-410E-96F6-F8EC11E90FEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f40bcaa8d311e4db512eab174f3dec9cd00f54c","datavalue":{"value":{"entity-type":"item","numeric-id":5537599,"id":"Q5537599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$91E04D14-CBDE-4015-ADBC-837AAE1E0194","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95fea0efbf7ea73b5df7afdb60be129365bfead0","datavalue":{"value":{"entity-type":"item","numeric-id":4729781,"id":"Q4729781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$C5C0E397-7CE7-4B68-85CD-CAB5C274AB91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d93c0216bb7a2404c766e146541a6f49efebe1b2","datavalue":{"value":{"entity-type":"item","numeric-id":1104318,"id":"Q1104318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$5437DCCF-0CFB-4FA1-AA18-2E5677A8F7B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98c09e51d33ea6c723b832bb0b53e6eb13bd20a9","datavalue":{"value":{"entity-type":"item","numeric-id":3951815,"id":"Q3951815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1264147$DB80333F-DAA1-440F-AB31-9DC69B2B221C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cbf202ac5e4b85bd0cff85e998d87fff373aea52","datavalue":{"value":"https://doi.org/10.1007/bf01792983","type":"string"},"datatype":"url"},"type":"statement","id":"Q1264147$C02E70B4-CCE2-4515-AFC8-E419385F5044","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"52d8f9ff9c41b9e24340e8a056158d226f7e6de4","datavalue":{"value":"W2048858873","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1264147$8695A8CE-0A95-4F58-B16A-EF46C25FAA32","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd588964afbae448a4cac58ae86e516228bf9c80","datavalue":{"value":{"entity-type":"item","numeric-id":1104318,"id":"Q1104318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d9888a71ea5091895b3885bc55f7ddf8732b267","datavalue":{"value":{"amount":"+0.8026661276817322","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1264147$D402861D-0D5B-4795-951C-879F9D986FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5596f4e7aa5c184f3689eee3edc81fa0596227e","datavalue":{"value":{"entity-type":"item","numeric-id":948908,"id":"Q948908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21c6d0f11223852d2879a0f308aedfca285ee71d","datavalue":{"value":{"amount":"+0.8006255030632019","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1264147$6A2602F4-4F27-48E0-8BE8-F84EE0A8E3B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8c0028d6c6c78955f724584e37e8c49aa588715","datavalue":{"value":{"entity-type":"item","numeric-id":1407524,"id":"Q1407524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"126636c1aa9553133d59268053e193ac87876e5b","datavalue":{"value":{"amount":"+0.7912243008613586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1264147$AC2F54C4-384D-46D2-B66D-D2A536E66536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8868a62ec8df3207496bd1c4a4eb27cf563faf1b","datavalue":{"value":{"entity-type":"item","numeric-id":2563983,"id":"Q2563983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"126636c1aa9553133d59268053e193ac87876e5b","datavalue":{"value":{"amount":"+0.7912243008613586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1264147$7464DD2B-A173-4FFA-9045-59C3207930E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44d48cc6eae7fce24a08db97a3ad4eb41ce2f1e1","datavalue":{"value":{"entity-type":"item","numeric-id":3140636,"id":"Q3140636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77f190ceace5411527323fda838423da182eb545","datavalue":{"value":{"amount":"+0.790843665599823","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1264147$1A4605E5-AD1D-46B9-97D8-32B63CC3D8F8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On some formalized conservation results in arithmetic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_some_formalized_conservation_results_in_arithmetic"}}}}}