{"entities":{"Q2909619":{"pageid":2920344,"ns":120,"title":"Item:Q2909619","lastrevid":79538933,"modified":"2026-05-06T14:09:04Z","type":"item","id":"Q2909619","labels":{"en":{"language":"en","value":"Non-principal ultrafilters, program extraction and higher-order reverse mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6078206"}},"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":"Q2909619$0900A5C1-F874-4B3D-8A2C-4B662581F86D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2644092188e5cd2dd88cf7932d7affd3b080aba3","datavalue":{"value":"1269.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$98892CE6-A8B3-4385-A23D-AEBE6F7B4607","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2d955f937199a49b108fb23625a795e0f7ef7cde","datavalue":{"value":"10.1142/S021906131250002X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$55C07157-7D1A-4AF1-A251-DBC8AA61E1EE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"71b151c9da44809f650995a7f88ca4d5f5807da4","datavalue":{"value":{"entity-type":"item","numeric-id":365681,"id":"Q365681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$AAA0581D-A736-49BE-99CB-909FCBEB7EC1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7c127e90f3bdb626ec3e36ebc57f0604031b78a6","datavalue":{"value":{"entity-type":"item","numeric-id":2732505,"id":"Q2732505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$389AD953-AC49-42B1-B301-1901C5E2D0B2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a2e785076c925608e90781bb4173656a454ded85","datavalue":{"value":{"time":"+2012-09-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2909619$A3043259-CD4E-4629-B995-7C8D213D464A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1c02d7bbdaf5bd753a4ad6287e322ab1dde223d0","datavalue":{"value":"https://arxiv.org/abs/1109.4277","type":"string"},"datatype":"url"},"type":"statement","id":"Q2909619$8B49D143-19E0-48F8-B46C-7262FCCB8A13","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"13841f0b96793f178ce9a7dcac9f232220625aee","datavalue":{"value":"03B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$AA9FAB81-223F-4F84-BA52-C94B3E1D0137","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$28C5F5F9-17F6-4C9F-A835-BD365517FDBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0282342b24b585fa878a09dabeb8eb52c72be5a3","datavalue":{"value":"03F60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$621C2A68-F7F3-4475-82D5-7122E6A30F5E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c5ce001c06142dd0657e7763a547ab673134fd1a","datavalue":{"value":"6078206","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2909619$DCEDCBD3-FD7E-4ED0-8675-9196BB187D71","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06c07e461ea895d5e1f93a1913d4b00eb39ee936","datavalue":{"value":"ultrafilter","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$8FCFB093-15DB-4836-98F3-D0E9736E17BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39ece27df4663c7fd54c61ee7602b62b0604cc6a","datavalue":{"value":"conservation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$9EC56A13-053D-42BA-B5D9-962DBBE17228","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$5E863BB7-02BE-4AF1-9A8D-C32431EC9649","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"492942e689dba58f90096ed1c12c52b0f868caa6","datavalue":{"value":"functional interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$02A34032-8225-4382-AB28-659F47AD0306","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf0a0d929b9a02ed4dea0e9db58247a82b31736d","datavalue":{"value":"higher-order reverse mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$914D5DD1-EBC5-4CBE-9DD0-836CD19D25C3","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":"Q2909619$87BF16DC-8C4F-4610-A488-3D012691A5B2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f46da379b7393c7674f5add3d3bea57420eb0d58","datavalue":{"value":{"entity-type":"item","numeric-id":1128188,"id":"Q1128188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$4601ED2B-53C3-4A5F-96E5-C6D6F2938E6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ebd8070024d6244f551fde9bd0753f8070da97a","datavalue":{"value":{"entity-type":"item","numeric-id":819711,"id":"Q819711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$47019F6F-C339-4616-9B7E-499366C84107","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d357a47c04e8c031646a6927518ecdcc37982e0","datavalue":{"value":{"entity-type":"item","numeric-id":3262780,"id":"Q3262780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$69A98645-5FE9-4A84-8000-97AF0D9309BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30cc9634805ca4e1cb379f368f02a0b23d8614df","datavalue":{"value":{"entity-type":"item","numeric-id":5313381,"id":"Q5313381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$AB2277CB-35C2-4AB4-B805-29FAA6926612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aff1e3cb97846d725e4e7fa295c1ef2e5b33886f","datavalue":{"value":{"entity-type":"item","numeric-id":5479570,"id":"Q5479570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$B2659BBD-351D-4FC9-83DC-12E510BA4D15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1484ffd13476ff4e30167317b1f1955782f6b13","datavalue":{"value":{"entity-type":"item","numeric-id":1267846,"id":"Q1267846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$172E285F-11FA-40F2-8CFE-39D0EF4B5075","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77765a4477c55f314baec87f180c178599579624","datavalue":{"value":{"entity-type":"item","numeric-id":4948521,"id":"Q4948521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$273D52ED-BFB8-4253-8854-D70F0D0332B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc02835a747b01d2e5ca9dc914037e15979d0cc6","datavalue":{"value":{"entity-type":"item","numeric-id":4939397,"id":"Q4939397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$F3F1EAC4-5C1B-4CA8-8909-27E3A6A594F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f1833dffb26af37c014afbf39f35fb844fa942d","datavalue":{"value":{"entity-type":"item","numeric-id":3083144,"id":"Q3083144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$4D6A3C1B-B669-4779-AA19-FBFDE8DCC031","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80c1d6c34931d2e97e40d55144a986f53345e9d3","datavalue":{"value":{"entity-type":"item","numeric-id":5251363,"id":"Q5251363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d39eb1fced509d73e026b2f69a14ec49c872ffea","datavalue":{"value":{"amount":"+0.83675086","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$DA9E26DA-53ED-423F-9CFD-9EA4015DCA6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb798e4b4a4d369ca1c87f182afcbda7942f8909","datavalue":{"value":{"entity-type":"item","numeric-id":3159415,"id":"Q3159415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7371a548b34a8a4a5364a70959b3a71c70d758bd","datavalue":{"value":{"amount":"+0.75937176","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$9A3D04B9-D129-41E3-B52F-6B5A19429BA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f527c287dbd78f4122814039f4c3f0c3cb02688","datavalue":{"value":{"entity-type":"item","numeric-id":2304540,"id":"Q2304540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c29690373399b666191cbccfeafb5def206abb8","datavalue":{"value":{"amount":"+0.7546813","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$1B693100-3364-41F1-9168-049DF6F264D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"975c318218f9656536c8053c984cb2aee72deb75","datavalue":{"value":{"entity-type":"item","numeric-id":2878778,"id":"Q2878778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8ca089336b7fcbb0e4c542fc9ff5744fdc48fe6","datavalue":{"value":{"amount":"+0.7502196","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$5B69EE81-B26D-42FE-8E31-D084295D8534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25039b6171b2485eba382bcb26f5369f48506ee7","datavalue":{"value":{"entity-type":"item","numeric-id":3699664,"id":"Q3699664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ece7ae7625e2b34e2184ae80f56bb9e0983d06d","datavalue":{"value":{"amount":"+0.7396911","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$998D523D-AA90-41D4-B2BC-3645F3EBF84F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f4428dcbe7fbe8a9cd487de726a1dd7077efc0","datavalue":{"value":{"entity-type":"item","numeric-id":636343,"id":"Q636343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bbad002f69f2b12489f8d3c199c187a05815af0","datavalue":{"value":{"amount":"+0.7374646","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$48BC8123-69C2-42D1-BBFC-19DF48AB1150","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3db8d4624cd53d6ac98bc2e37d8bc9fabb47fb41","datavalue":{"value":{"entity-type":"item","numeric-id":2966523,"id":"Q2966523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfcc7e41b79c3d89217b0f979680f7437ac43aeb","datavalue":{"value":{"amount":"+0.73274326","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$4F80B0D1-D3F9-4783-8278-99574A9F2C19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9cb31f927016e7e06ef12bf033e414f99050c3eb","datavalue":{"value":{"entity-type":"item","numeric-id":5711887,"id":"Q5711887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e91c310d5d85ab9a28972e9c7561c185dfd8ebfd","datavalue":{"value":{"amount":"+0.73152405","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$99F1D288-9D5A-4505-960A-927423C1FC33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01ef37c0274cdf6a7c6e310bb9c6f6c94a08dbe6","datavalue":{"value":{"entity-type":"item","numeric-id":4579817,"id":"Q4579817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"706652f2f99cfcf679c95505517b99b95375481d","datavalue":{"value":{"amount":"+0.72946846","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$D74904C7-8172-411A-8685-E70B892EFC88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ea533da214356801a26c3553c733025738ddd3d","datavalue":{"value":{"entity-type":"item","numeric-id":5711891,"id":"Q5711891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb74bf3699dbd43e9e5a2932f50876e95756170b","datavalue":{"value":{"amount":"+0.7251707","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2909619$119F3215-EDE0-4150-9860-331A3EE5B69F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"59be413ad99c4bd54dde4bbf59901f7b874002c7","datavalue":{"value":{"text":"Non-principal ultrafilters, program extraction and higher-order reverse mathematics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2909619$58E59038-8F62-429C-92CC-345A49B9A4E5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6055319f3fef6d18b75d205643114c8b107133f5","datavalue":{"value":"The author studies the strength of a non-principal ultrafilter in the context of higher-order reverse mathematics. This field, as described by \\textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)], involves a generalization of second-order theories of arithmetic, such as \\(\\text{RCA}_0\\) and \\(\\text{ACA}_0\\), to corresponding theories of arithmetic in all finite types, such as \\(\\text{RCA}_0^\\omega\\) and \\(\\text{ACA}_0^\\omega\\). The author defines a principle \\(U\\), in the language of third-order arithmetic, stating the existence of a non-principal ultrafilter on the natural numbers.NEWLINENEWLINEThe main result is that, although \\(\\text{ACA}_0^\\omega + U\\) is strictly stronger than \\(\\text{ACA}_0^\\omega\\), it is \\(\\Pi^1_2\\) conservative over second-order \\(\\text{ACA}_0\\), and thus conservative over \\(\\text{PA}\\) for sentences of first-order arithmetic. The conservation results are proved as corollaries of a program extraction theorem that produces a witnessing term in G\u00f6del's system \\(T\\). Key steps include a normalization theorem due to the author and \\textit{U. Kohlenbach} [J. Symb. Log. 77, No. 3, 853--895 (2012; Zbl 1254.03112)] and an approximation result using ultrafilters on countable algebras of sets. The author states that the theorems and techniques of the paper can be applied to analyze mathematical theorems with proofs that use ultralimits and nonstandard methods that can be formalized in \\(\\text{ACA}_0^\\omega + U\\), but that the techniques of the paper do not directly address the problem of the strength of Hindman's theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2909619$495070EA-83F6-4207-950C-2A5566A41616","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"1ffd6458cf29ace8b9f78898cc3cc1cfe8fed9fa","datavalue":{"value":{"entity-type":"item","numeric-id":375888,"id":"Q375888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2909619$1FF6B805-ACAC-494E-9536-0CA8ABE8F984","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Non-principal ultrafilters, program extraction and higher-order reverse mathematics","badges":[]}}}}}