{"entities":{"Q1130232":{"pageid":1140981,"ns":120,"title":"Item:Q1130232","lastrevid":46857192,"modified":"2025-12-25T17:49:41Z","type":"item","id":"Q1130232","labels":{"en":{"language":"en","value":"Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1192478"}},"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":"Q1130232$09CBF782-623D-4538-91B0-125374704AB4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"50cf00047adf3fa269c2046fada5b83da53f730a","datavalue":{"value":{"text":"Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1130232$2A4748F9-B9B7-4CD3-9532-4B3C31F373AA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bdfb2202f84f86f76224dec4d2f4751ff0a07a88","datavalue":{"value":"0937.03067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$C16D0421-5F12-4382-8351-534CFE509DF2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c5199aa691bc5da4927d90a484fa0c33ae27338","datavalue":{"value":{"entity-type":"item","numeric-id":1130231,"id":"Q1130231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$BC2ECD6C-12EE-4D2D-9F0C-DE6C9C157516","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$F46AC588-D65F-4F50-BAFE-1837AC431F85","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"04308aed0d348814abb526d3ddeaf64fb167d343","datavalue":{"value":{"time":"+1998-11-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1130232$3783DAF4-391A-49F4-A14D-285BECABBE8B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"def4f63d56625ac5c35d57896b814d787ae11555","datavalue":{"value":"An extension of HA called TRDB (the system with Definition by Transfinite Recursion and Bar induction) is considered. It is a system designed in particular to construct the accessibility proofs for ordinal diagrams and may be considered as a modification of the system ASOD suggested by Yasugi. TRDB is a natural deduction system specified w.r.t. a certain formula \\(G\\) and a certain primitive recursive well-ordered set \\(I\\). In this paper only the case when the order type of \\(I\\) is less than \\(\\varepsilon_0\\) is studied. Main results are: strong normalization theorem for TRDB; consistency of TRDB; existence and disjunction properties.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$20731DFD-25EB-49FD-8931-349C82779A10","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$C6EB83A8-FDED-401A-9550-DB379C98E8EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$1443E9E0-A367-4762-A5CB-3C673433C412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$A770DBD1-CDC7-49BB-BA6A-F9E1DEB205F2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c00d0b0a7244f99832d10c5a58c6bf1148d0a458","datavalue":{"value":"1192478","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$432959E9-E525-43CF-8DA9-05540D1402EC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"baf5c837625e1da4bd98945a1fdab2c9aeee6d84","datavalue":{"value":"constructive arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$C50B2054-D7F2-4DB8-86B6-D2D412DAEBB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d29c7907a058ca2f5803a563e9765a72c855a696","datavalue":{"value":"recursive definitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$F79E5720-847F-4250-AD0B-B4B3DE4BBAAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$5D06AE88-8588-4CEB-81B3-987D415B3041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4108cecd289b9cafbcb28752da70c2315de2efa0","datavalue":{"value":"conservativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$F0789CEE-822C-4A91-8C14-68E9B0B0C389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd3d855058cd0bf9e0b654a9d7d73edc478bb262","datavalue":{"value":"natural deduction system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130232$F355C186-5825-408A-B269-0906A6A2BD6D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b6c848266fa72da40ff1802d3555a7d072216992","datavalue":{"value":{"entity-type":"item","numeric-id":590478,"id":"Q590478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$3CFD55BD-9A30-4031-B68E-C62F9D25F09E","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":"Q1130232$AAEAEBA6-9281-43A4-9892-4A86FFFEF4D8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8ff23e9ada9e4d229b7fdcc321a4e32239271763","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1039700743","type":"string"},"datatype":"url"},"type":"statement","id":"Q1130232$90C6CF43-C365-4747-920B-0FC6DFA40864","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"706e59f919559aaf80ce0b98e467efaaed7fb5f1","datavalue":{"value":"W1970906905","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$ACB4B2ED-3CEE-4FCC-A29A-AD5B0F29740C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$7B4255C9-7534-4992-82F6-35A2B6F090CE","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":"Q1130232$991CC954-121B-4777-85CA-5EB69D06194F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a2de9065d8148cb439d5528548f8a919de4dd59","datavalue":{"value":{"entity-type":"item","numeric-id":3770525,"id":"Q3770525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$C53BDAA4-52A8-405F-8747-EFB06B30E633","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"538a774bbda8df010e5e8d40edf18e3d45f426e0","datavalue":{"value":{"entity-type":"item","numeric-id":1124588,"id":"Q1124588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$61F94B7D-CD82-4EB9-BD66-ED07749EF7B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ad1b8f6f6df30a2e9089b2d8015d1e48306ff4","datavalue":{"value":{"entity-type":"item","numeric-id":4348037,"id":"Q4348037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130232$98FD1926-A17A-43D1-B1D4-4133A3BB9391","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c5155b4b1f9488c8dea3225014a0c6278f90fc29","datavalue":{"value":"10.1305/NDJFL/1039700743","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130232$8D3E5449-0756-4633-8903-5E34DB462B46","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98d3790d308f4eef46048b7c5e54eadf8bc34016","datavalue":{"value":{"entity-type":"item","numeric-id":5394567,"id":"Q5394567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae03fc21c5ee2a5b7a10f3bc255667194fd3115a","datavalue":{"value":{"amount":"+0.7511389851570129","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":"Q1130232$9FA1C13C-17A5-48A0-A70B-87133106D9E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7905963af015b44505496ce809c13a1a6c52306","datavalue":{"value":{"entity-type":"item","numeric-id":4348037,"id":"Q4348037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fb52d6907a8399a9aeae2b1d132189ce71d3ac1","datavalue":{"value":{"amount":"+0.7390589714050293","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":"Q1130232$B8A17DE2-2DE1-479B-BD8C-943B89494EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84cf870b60e963bde3a4f9887e8ee860d85d0c62","datavalue":{"value":{"entity-type":"item","numeric-id":3739119,"id":"Q3739119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1326b3be72eab8ab0cee087a8c4349f13b1a7434","datavalue":{"value":{"amount":"+0.7376579642295837","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":"Q1130232$31E74A08-2B4F-488E-B0F5-F99D258C7A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eed61c411ec4b693d6d36608c97770795414f4f1","datavalue":{"value":{"entity-type":"item","numeric-id":1071019,"id":"Q1071019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc39dbb4e67fa498c429f7705a0a0693928af58c","datavalue":{"value":{"amount":"+0.7310440540313721","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":"Q1130232$96AC1DC9-FAF3-4277-8BB7-572737C91194","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1130232","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1130232"}}}}}