{"entities":{"Q753810":{"pageid":755659,"ns":120,"title":"Item:Q753810","lastrevid":64157832,"modified":"2026-04-11T18:01:29Z","type":"item","id":"Q753810","labels":{"en":{"language":"en","value":"Extended bar induction in applicative theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4181326"}},"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":"Q753810$8757B98A-64E3-468F-A89A-7D33BA66FF45","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dee5d6098bb10639aa66129a2e6ba04b5237cc06","datavalue":{"value":{"text":"Extended bar induction in applicative theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q753810$E82F6354-3DC2-4949-9BEB-F683E0D204FB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4ccc0cb4775f23536656acd89e8da279602f1a8c","datavalue":{"value":"0717.03024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q753810$1B83E330-FAC9-48C2-BAC9-C1A3C22B755C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aeee7ec6a5b2907754787e905abde2e7e24dd349","datavalue":{"value":"10.1016/0168-0072(90)90047-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q753810$3DB4DE4B-FCA9-49FB-A704-3BDBEC8A20C4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"27a40f3e393f328cd4730fcb61457b79095ca391","datavalue":{"value":{"entity-type":"item","numeric-id":753808,"id":"Q753808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$E31A1097-D8D8-40EB-8487-0C2EE9AD4ABC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$7EFAF653-C846-4FF7-AEB7-2B52CA87788A","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":"Q753810$5BFEDD39-E0D5-4269-AE81-6E3D284B487A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cc5222c95acffedddcb1d9825a709ffe11e1cae8","datavalue":{"value":"This paper presents several important results of constructive mathematics on a meta-level. A sketch of the type-free theory with total application TAPP, which is an extension of APP, is given. The author shows that \\(TAPP+EAC\\) (extended axiom of choice) is conservative over HA (Heyting arithmetic) by using the method of forcing on a monoid, and that the same holds for \\(TAPP+EAC\\) with inductive definition. The author presents a novel proof of the theorem that \\(ML_ 0\\) (Martin-L\u00f6f's type theory without universes) is conservative over HA. The author studies the principle of extended bar induction (EBI), especially the arithmetical extended bar induction of type zero \\(EBI^ a_ 0\\). Extending TAPP and EL to \\(TAPP^*\\) and \\(EL^*\\) with sequence variables, the author proves that \\(TAPP^*+EBI^ a_ 0\\) and \\(EL^*+EBI^ a_ 0\\) both are arithmetically equivalent with \\(ID_ 1\\) (HA with non-iterated inductive definitions).","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$1F99BC74-4B64-4650-8D00-7DFA75CBCB56","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0a88a6971b5b4b6c7f660951ec547d3191ec51e3","datavalue":{"value":{"entity-type":"item","numeric-id":753809,"id":"Q753809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$4540A8B7-5E51-435E-92C3-29A73F380B54","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q753810$27F8DF74-7ABB-4FDA-8D26-76C40C2CE14D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"325c4e9fd01a69a2ef788213961d7bfc1ad03ce5","datavalue":{"value":"4181326","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q753810$8D92D524-CDED-47CB-9A91-98287778CEA4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0df017823f7a7af5f45c7345e5121d83a960fd7","datavalue":{"value":"total applicative theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$1CE8C182-E134-4D99-984B-B76A1EFEA47D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"880189f3ab141434ac60dc229df6c4a00e086156","datavalue":{"value":"intuitionistic arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$F3D09945-722B-4C49-BD42-574AA8DF3D2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5830bc9df856ae2559fe681dc92cebe9ada5b3da","datavalue":{"value":"constructive mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$A5C88AA9-449A-49B5-8176-F40D031817D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b5d8c97388f131003bda876a2f246e735d344591","datavalue":{"value":"type-free theory with total application","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$ADBD1D2C-18C6-4491-AA9C-3AB45D8E3D31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ebb4c059a02acfbc699b4ec679a1a1eaac3ef1a","datavalue":{"value":"TAPP","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$6858D701-25DF-4318-9A98-68A582A4F7DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4848d68088b46e5fb22a5f0d3abe31284f4b2432","datavalue":{"value":"extended axiom of choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$4C9AA0F8-87EA-4173-A51A-2A9338EDB6B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97c6b970990dab40d69357bafd674174e833bc7d","datavalue":{"value":"Heyting arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$0896600E-162B-4B43-A0F5-EF7B103E5671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"712ac19ee11ad4d22b66afe5c3977cfbf94585da","datavalue":{"value":"forcing on a monoid","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$0A70AAC5-D53E-440B-A58B-F0A2085CB66F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba29bc695092e1012b615eb49ec43774f5b5c42a","datavalue":{"value":"inductive definition","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$A48F4CC9-6A03-44C2-A243-5FDFEAB94B94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2a89517e29f96c0582e7ef59731cb72f680c7dd","datavalue":{"value":"Martin-L\u00f6f's type theory without universes","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$E66B57C9-1BCB-4C33-AA25-250BB978109B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"140f2a8dd7ae54193ee77e7667b70f1cf336acb9","datavalue":{"value":"extended bar induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q753810$2A41B695-0F15-45C9-A1B6-4F0F91FD5993","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":"Q753810$E461C805-3814-40E9-BB85-4C3510303C98","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bbb4e61d0ce5945ad5b0e933856a30f264dceb43","datavalue":{"value":"https://doi.org/10.1016/0168-0072(90)90047-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q753810$5670E053-B66C-4354-B973-8642179A00F5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d61232d1e0fc0b5f434b19ed244f1f0ca3e36f27","datavalue":{"value":"W2085036336","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q753810$26B7B951-33CB-43E0-B97E-2BFD97E9B865","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fed62f77086cc482760f4f0947cecfd1cf3885b1","datavalue":{"value":{"entity-type":"item","numeric-id":1139042,"id":"Q1139042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$0FAC6E57-B0D0-42A9-9611-E5EEB54DF2C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2e1ab8d6c4a6ea4362f203e5137d4541ef80eb","datavalue":{"value":{"entity-type":"item","numeric-id":3679172,"id":"Q3679172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$9B170831-B98B-4916-B41E-9574F369C53A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b822b85db8677253a219ea1a385eddacb5927738","datavalue":{"value":{"entity-type":"item","numeric-id":1166517,"id":"Q1166517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$03F39A48-F9B2-4E65-ACE9-BD131F6D2F66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc94f78e4d4d647f89d23291924c43b88a8d1fbf","datavalue":{"value":{"entity-type":"item","numeric-id":3029009,"id":"Q3029009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$48008B10-7698-439B-8DF8-792474D77523","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51fdc6e6c91c016e9985f506925ea38ed52ac667","datavalue":{"value":{"entity-type":"item","numeric-id":4128540,"id":"Q4128540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$40002F8E-F742-40D0-9F2A-19868D563426","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a105535a0b4cf840366405592d4900ef990604f","datavalue":{"value":{"entity-type":"item","numeric-id":3882452,"id":"Q3882452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$979FB580-8D69-4207-ABC0-A8B0520F71BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64ffae7793cb2f017658a44896cb5888b517a415","datavalue":{"value":{"entity-type":"item","numeric-id":4770943,"id":"Q4770943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$442ECDF5-BCF6-4D7B-AEA9-DAAC3D1B9899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67518660f65fbd28a63236a419c37e46f7123efe","datavalue":{"value":{"entity-type":"item","numeric-id":4140964,"id":"Q4140964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$A21F69D0-752D-48FF-8C7B-810977C5C7E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d11ad722a58de019ca546cb797582b6f9c7fc3f","datavalue":{"value":{"entity-type":"item","numeric-id":4177565,"id":"Q4177565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$AD6E75C0-A2CD-4F04-AA22-A1F3700F7DEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"967caee0f4b629b2770249b58352d882fa57e30d","datavalue":{"value":{"entity-type":"item","numeric-id":911585,"id":"Q911585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$D0E1B8D2-5132-4AA0-BFEA-9E390495103A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d5936835a9e4ba0ac0bc472068162c27a6cb583","datavalue":{"value":{"entity-type":"item","numeric-id":798316,"id":"Q798316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$CDA8E251-E860-404C-8CDB-FD6C9ECD07D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09a4e58c25b3453d9125c4c48d9600b2360c05ce","datavalue":{"value":{"entity-type":"item","numeric-id":5537358,"id":"Q5537358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$83DD08B8-138E-4468-88A7-1B95413AC785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91ba25d69cadc919d80d2b5e82a0eabcb1b50c8c","datavalue":{"value":{"entity-type":"item","numeric-id":5343325,"id":"Q5343325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$0BE562AB-B026-4D4D-804F-CEAC281FD82A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbc9c5f4d2a3665ff37b68ff31d08bc5eef515af","datavalue":{"value":{"entity-type":"item","numeric-id":5611760,"id":"Q5611760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$AD842CDB-C753-4F0E-910D-7FB2DE8360BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f69e4e3c6e6db6273645f322c23116e1ad1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3343983,"id":"Q3343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$0707EC42-EEE8-4123-9C74-D2B50231C133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dac56f2072a3893c756d692707c0c07bfe6e585","datavalue":{"value":{"entity-type":"item","numeric-id":5519134,"id":"Q5519134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$12A4FE83-5613-4C9C-86BB-A935689B484A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$A0769F69-A68D-4B5D-9213-83D504D5926C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99bdd6963dc43409b62a79b7afcf3230073a1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3887457,"id":"Q3887457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$11B87BF2-D58C-4FB0-8110-C1DD7E04EC29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20f26a27356d39f30de150c562ffeee04fbf14f0","datavalue":{"value":{"entity-type":"item","numeric-id":1099173,"id":"Q1099173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$6EA95409-79BB-4324-8FBD-0BE977DE1CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q753810$DD1C0D20-3F67-4343-A166-96C618EB0F58","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f18fd094053abb5e6d6c97c497297cfdb682bd0e","datavalue":{"value":{"entity-type":"item","numeric-id":911585,"id":"Q911585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70bb2cd3cfd15215d124de2985b35c2d06a5f1e0","datavalue":{"value":{"amount":"+0.7455907464027405","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":"Q753810$D9C75107-EE14-4AD1-84EB-FD3226B5F279","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b9889c3b95b1b19beb22295a52aaf6a8c4c4004","datavalue":{"value":{"entity-type":"item","numeric-id":5457300,"id":"Q5457300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9aaa87a86c728a5fac400ec97cc4bee54be30372","datavalue":{"value":{"amount":"+0.7380926609039307","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":"Q753810$4FB5EAF1-DD17-4478-9482-C46610D7E671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f100d5836d0242c834e014784daae9738b686670","datavalue":{"value":{"entity-type":"item","numeric-id":5244386,"id":"Q5244386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b409d87042243be91fc8ff8cf6ef6f3a1b6fe315","datavalue":{"value":{"amount":"+0.734435498714447","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":"Q753810$1823BC58-5CC0-4F80-A23F-2A80D88CC49B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11fb31218a40ef5a8f85b77a3e9032bda2daec13","datavalue":{"value":{"entity-type":"item","numeric-id":2566067,"id":"Q2566067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c199615126f7558cc2058c21fb558c48f3c81d34","datavalue":{"value":{"amount":"+0.7343512177467346","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":"Q753810$1C73D186-B848-418D-A9F8-112933836AB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9023aa54d93c82dcb1e5159f3c7a23780836cdb2","datavalue":{"value":{"entity-type":"item","numeric-id":1942040,"id":"Q1942040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77f536a5acfb6d72941e63c88fa42ab6ba646ab3","datavalue":{"value":{"amount":"+0.7292708158493042","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":"Q753810$56D1DE49-75DB-4760-ABD5-F0E188A3D3A9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extended bar induction in applicative theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extended_bar_induction_in_applicative_theories"}}}}}