{"entities":{"Q920089":{"pageid":921937,"ns":120,"title":"Item:Q920089","lastrevid":65388510,"modified":"2026-04-12T02:14:40Z","type":"item","id":"Q920089","labels":{"en":{"language":"en","value":"Elementary inductive definitions in HA: From strictly positive towards monotone"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4162874"}},"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":"Q920089$58869542-20BD-4AFC-9C8D-B6EB8D0ACB0E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0e270ca9007c0cda190dffdb0b092a0b29629b48","datavalue":{"value":{"text":"Elementary inductive definitions in HA: From strictly positive towards monotone","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q920089$100BA58E-7E89-41F2-8A4E-DF0323599B96","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b6a31a3562f08d9286afed0317a51b4a765d1a10","datavalue":{"value":"0708.03029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920089$D69FD083-D473-4C39-B36C-78B6D69F647E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a14994527d5ecf7c1af7fc7618f6701c641da241","datavalue":{"value":"10.1016/0019-3577(90)90037-N","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920089$3B403974-7AC9-4C94-827A-5BEBC7B26935","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8056e242bd9114b6b7f5b12c5335e7142df0af71","datavalue":{"value":{"entity-type":"item","numeric-id":920088,"id":"Q920088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920089$37D9B65F-3BFD-4870-8585-B5F598B576BF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2e359c0e985e9b5bac2c1d59359dad9dfd6f494d","datavalue":{"value":{"entity-type":"item","numeric-id":174755,"id":"Q174755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920089$1D38BBB3-D38F-4D88-945B-CEE1FF76D7F1","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":"Q920089$6C71C265-3BC5-4184-9B31-7E4B96A0FD9A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0bf093ff7e6898c3e5e42234d0ad6a8ec8788315","datavalue":{"value":"An elementary inductive definition (e.i.d.) is given by a formula A(P,x) in the language of the intuitionistic arithmetic HA expanded with a single one-place predicate variable P, containing at most one numerical variable free, without an unbounded universal quantifier occurring in front of a positive subformula containing P, and without an unbounded existential quantifier in front of a negative subformula containing P. It has been proved classically that if A(P,x) is an e.i.d. (therefore, it is monotone), then the approximation defining its least fixed-point \\(P^ A_{\\infty}\\) closes up at or before stage \\(\\omega\\), so \\(P^ A_{\\infty}=P^ A_{\\omega}\\) \\((P^ A_{\\infty}\\) is defined by the approximation: \\(P^ A_ 0x:\\Leftrightarrow A(\\lambda x.\\perp,x),\\quad P^ A_{\\beta +1}x:\\Leftrightarrow A(P^ A_{\\beta},x),\\quad P^ A_{\\lambda}x:\\Leftrightarrow \\exists \\mu <\\lambda P^ A_{\\mu}x,\\) lim \\(\\lambda\\), \\(P^ A_{\\infty}x:\\Leftrightarrow \\exists \\mu P^ A_{\\mu}x).\\) However, intuitionistically, this is only true (in general) for strictly positive e.i.d., i.e. formulae A(P,x) built up from atomic formulae Pt, from HA-formulae \\(\\phi\\) (these do not contain P), by means of the operators \\(\\exists\\), \\(\\forall y<s\\), \\(\\wedge\\), \\(\\vee.\\)    The main result of the paper is to prove that if we extend the class of strictly positive e.i.d. by adding an operator J satisfying the conditions: (i) \\(Q\\to J(Q)\\), (ii) J(Q\\(\\wedge R)\\to J(Q)\\wedge J(R)\\), (iii) J(J(Q))\\(\\to J(Q)\\), then \\(P^ A_{\\infty}=P^ A_{\\omega +\\omega}\\) is HA-definable, i.e. the approximation closes up at or before stage \\(\\omega +\\omega\\), intuitionistically. Note that \\(\\neg \\neg\\) is such an operator J.","type":"string"},"datatype":"string"},"type":"statement","id":"Q920089$58AEBD74-5B45-4479-A5F1-9C7C0FBF414D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920089$0B93EE0E-9381-4E15-9317-EB31904B7ADF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"86133964957b402dc7c00b2cfe460216efb7f0ef","datavalue":{"value":"4162874","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920089$D682527D-182D-4CB0-841B-42AEFE7F9A83","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c49de5994ff2f4dfd4923502c90f2eece4bc505","datavalue":{"value":"elementary inductive definition","type":"string"},"datatype":"string"},"type":"statement","id":"Q920089$86B42F59-40C7-4036-A3BC-6F65B270E7F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c448f94963c9dd8e7f820d2b2639f8e7bd108f75","datavalue":{"value":"intuitionistic arithmetic HA","type":"string"},"datatype":"string"},"type":"statement","id":"Q920089$A7664B4C-DF90-44C2-94A8-4511A97567FC","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":"Q920089$8679FC3B-E692-45E6-99C1-D17C175B173D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1829d57a79fdec03bcb9e543ae58b9bda3fa26be","datavalue":{"value":{"entity-type":"item","numeric-id":3050433,"id":"Q3050433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920089$6F8580F7-319D-4E2F-8738-90760EF0C46C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a33163735a85d6128763b775f342685a8d5402f4","datavalue":{"value":{"entity-type":"item","numeric-id":5668423,"id":"Q5668423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920089$8DE7FE77-1677-47F6-B492-F55E1CCA6B90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fc0f83d5ec3109942a6da644b57709f31b1dc6","datavalue":{"value":{"entity-type":"item","numeric-id":1188522,"id":"Q1188522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920089$C47AC340-D0FA-488D-BE72-7050C4DBA527","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e98bbb3dad928742dd57875b572b75acfc21d4a","datavalue":{"value":{"entity-type":"item","numeric-id":1386672,"id":"Q1386672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fad67163105ff1329ff7bbde143706b6f780f505","datavalue":{"value":{"amount":"+0.757977306842804","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":"Q920089$9B793424-ED43-49FB-9186-5F2AB20DD6A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f6982be56b248723c76303a235ec410a82aa2a8","datavalue":{"value":{"entity-type":"item","numeric-id":2758045,"id":"Q2758045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bcec1dd8bc963d41f507a5a15c29423a17f12e4","datavalue":{"value":{"amount":"+0.7553004622459412","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":"Q920089$2605CB08-5411-459A-BAD7-AFB1CA37F75A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a62ce123c1cf42b5cfa1cc7ccf58379fc93c0b5","datavalue":{"value":{"entity-type":"item","numeric-id":688845,"id":"Q688845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ccd585889599ea12e23308cfa79434c3804d0d0","datavalue":{"value":{"amount":"+0.7543065547943115","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":"Q920089$FF10F7B7-324A-4311-BFD9-208BD0545670","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69f15e5c9ab71465b79d2ec17ced4eba42d5469f","datavalue":{"value":{"entity-type":"item","numeric-id":5486242,"id":"Q5486242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bccbd186301c2aa03e81c841ac37b5138aa95d13","datavalue":{"value":{"amount":"+0.7523510456085205","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":"Q920089$53B299BD-EBEC-47A1-B602-F295C831FDE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f90e9bc94faf1eed182284e28c42ddcf8f3554b","datavalue":{"value":{"entity-type":"item","numeric-id":3001089,"id":"Q3001089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8868a40f6e8a3318e5f08363be3707ed21b1e9d","datavalue":{"value":{"amount":"+0.7510886788368225","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":"Q920089$7CD2FFFB-6D5D-4EDF-97BF-F5C0EE6463CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Elementary inductive definitions in HA: From strictly positive towards monotone","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Elementary_inductive_definitions_in_HA:_From_strictly_positive_towards_monotone"}}}}}