{"entities":{"Q1778059":{"pageid":1788801,"ns":120,"title":"Item:Q1778059","lastrevid":72540321,"modified":"2026-04-14T05:36:31Z","type":"item","id":"Q1778059","labels":{"en":{"language":"en","value":"Epsilon substitution for transfinite induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2171980"}},"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":"Q1778059$6E7B5516-0DA8-47E8-91C8-ABB2218A3D86","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5004b35ab5b16e57045f76bcb2377e8960cbc80d","datavalue":{"value":{"text":"Epsilon substitution for transfinite induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1778059$724B9128-7B8F-43AB-82DC-62E9C1010D94","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"66dfba45b398de7adadf5943a6b2b86d13ef5c8d","datavalue":{"value":"1066.03058","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$7A578C9A-220B-44F7-A87C-744358705B74","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4aea1dd36182a052ff66ff5bfa454f46b990083b","datavalue":{"value":{"entity-type":"item","numeric-id":424578,"id":"Q424578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$E7CD6A7E-3C49-4AFD-9482-18698DEFD2E5","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":"Q1778059$41C3DBF1-096E-4EBA-AD09-8FC46A6DAB80","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"883cf1b866b714c43fcf9988533850ce4229a20f","datavalue":{"value":{"time":"+2005-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1778059$ADE00E03-870D-40C5-B7BB-5C36BE4A253A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8eb3b7e80c2b2e1563a1a1ec4e37c637f809f25b","datavalue":{"value":"The systems \\(\\text{PA}+\\text{TI}(\\prec)\\) of first-order arithmetic extended by a scheme of transfinite induction on a recursive well-ordering \\(\\prec\\) (of the order type \\(\\alpha\\)) are often used in proof theory. \\textit{T. Arai} [``Epsilon substitution method for \\(\\text{ID}_{1}(\\Pi_{1}^{0}\\vee{\\Sigma} _{1}^{0})\\)'', Ann. Pure Appl. Logic 121, 163--208 (2003; Zbl 1022.03040)] outlined a schema of an \\(\\varepsilon\\)-substitution method for such systems and of a termination proof using ordinary assignment by a method of W. Ackermann. The author provides a cross-check via a termination proof using cut elimination following \\textit{G. Mints} [``Gentzen-type systems and Hilbert's epsilon substitution method. I'', in: D. Prawitz et al. (eds.), Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7--14, 1991. Amsterdam: North-Holland. Stud. Logic Found. Math. 134, 91--122 (1994; Zbl 0835.03023)]. The main new feature of the formulation by T. Arai is a possibility to assign an arbitrary value \\(n\\) satisfying \\(\\varphi[n]\\) to an \\(\\varepsilon\\)-term \\(\\varepsilon x\\varphi[x]\\), not necessarily the \\(\\prec\\)-least \\(n\\), since the latter is non-computable in general. A correction step corresponding to a critical formula \\(\\varphi[m]\\to\\varphi[\\varepsilon x\\varphi[x]]\\) may change such a value \\(n\\) to \\(m\\prec n\\).   The main new feature compared to the termination proof of Mints [loc. cit.] is the treatment of cuts corresponding to the alternative: either \\((\\varepsilon x\\varphi[x],?)\\) (that is, \\(\\forall x\\neg \\varphi[x]\\) and \\(\\varepsilon x\\varphi[x]\\) has a default value 0) or (non-default) \\(\\varepsilon x\\varphi[x]=n\\) for some \\(n\\). Redexes corresponding to this cut are situated over an \\((\\varepsilon x\\varphi[x],?)\\)-premise and called \\(H\\)-axioms. An \\(H\\)-axiom \\(A\\times H_{\\varepsilon x\\varphi[x],n}\\) corresponds to \\(\\varepsilon x\\varphi[x]=n\\). In the reviewer's paper [loc. cit.] a reduction of such a redex used only the premise of the cut corresponding to \\(\\varepsilon x \\varphi[x]=n\\). In the present treatment cut elimination in premises for many \\(m\\preceq n\\) is used in a way corresponding to the quantifier \\((\\forall m\\prec x)\\) in the progressivity condition \\(\\forall x(\\forall y\\prec x\\,\\, Px\\to Py)\\). Otherwise the schema of a proof is the same as in the reviewer's paper [loc. cit.]. For a given finite system \\(E\\) of critical \\(\\varepsilon\\)-formulas, an \\(\\omega\\)-derivation is constructed, cut-elimination theorem is proved, and it is noted that a cut-free derivation is finite and encodes a terminating \\(\\varepsilon\\)-substitution process.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$58CE20B7-14E1-46DC-B816-5131316FC98C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$E8820776-5E72-4AF7-A30F-57EC335F763E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$A8526BF1-F775-4031-88B2-7FEA4962B099","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1d718b285c20e82f5676f99c448b83e1647d5cf1","datavalue":{"value":"2171980","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$818C59E2-C174-462E-8093-6E69083515ED","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"29e85a61e7939ee6f14f83214f0f77882dcad4fc","datavalue":{"value":"first-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$84B026D0-7126-4D7B-9338-DFBC47914017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8cc87407ab9572d85505f2cace7811c9ecc29db","datavalue":{"value":"transfinite induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$53ACDB79-1D58-46CD-98C8-0345311D6B4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aca44cd05b6ae7b16fcf689051c99887666a8262","datavalue":{"value":"recursive well-ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$5C7A6E30-B182-422F-B241-32CCDB432080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"868d83768da7f63ed788dde076e4b7af4cec69c3","datavalue":{"value":"epsilon-substitution method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$BA600E2D-BCDD-4143-9328-65998AB8DFC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7d3ca4a6cbd279b42e521c34520e7efdd1df0b39","datavalue":{"value":"termination proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$C448A0ED-C43E-4DC1-B8A1-0B7EFBA61416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1778059$80EDA330-C738-4BE9-B98C-FF8E1B0107E1","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$46CD2C61-AD99-41A7-9056-763DD479DA8D","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":"Q1778059$6BD93740-BF7F-4617-9A9E-EEC07D933D24","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ac505a913b5fe2193dbe9735f409f1d2c4de2b9","datavalue":{"value":"https://doi.org/10.1007/s00153-004-0241-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q1778059$1020A1ED-D90F-4869-8D0F-46AD95432CA6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aaae8ab0ccdd913c29d1d673efaf0352a5ccbfed","datavalue":{"value":"W2061312397","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$1CBF41E7-D080-43DA-B581-6F35AAE90030","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"31291a3dd4a99b6e7b6897958f564beb936e92cd","datavalue":{"value":{"entity-type":"item","numeric-id":1399101,"id":"Q1399101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$8C44995D-C4F2-407C-BB7B-9EA0BA6E714C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"973f6bf6c69678cd9a656a7e5b366fda4d57bf05","datavalue":{"value":{"entity-type":"item","numeric-id":1407530,"id":"Q1407530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$80E9404B-820E-4B36-A6E0-DD6BA42ECA12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81cc5131b0b7964726299b118b83461f6bf3bdb2","datavalue":{"value":{"entity-type":"item","numeric-id":4325774,"id":"Q4325774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$8D645625-6343-49FB-BD6A-A67D8CCE9E64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839f84674fbc4960d57f999dfddb193181d8344e","datavalue":{"value":{"entity-type":"item","numeric-id":4941993,"id":"Q4941993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$23E6E5C1-3AE2-4EE8-8E17-FF1CBFFBDDA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82765c6652fefb7b62b485b8396ead94a739e4b9","datavalue":{"value":{"entity-type":"item","numeric-id":1908821,"id":"Q1908821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1778059$1185DEF8-891F-4CE6-A9E1-3CC48DBE8716","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"40f70771a8a9e0b8ba75b44649c5e6b0547ae42f","datavalue":{"value":"10.1007/S00153-004-0241-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1778059$C191D34E-A416-4EBA-8BE1-F934F1E3C8CB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a751f9d4e79b620673c28b4511ed3776e89bd273","datavalue":{"value":{"entity-type":"item","numeric-id":1401363,"id":"Q1401363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e49d1d0f396bc8dde42580783623a9bf483bf9e","datavalue":{"value":{"amount":"+0.8373291492462158","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":"Q1778059$298B7C32-2BE7-4B54-86D2-E1ED5A9DD354","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b4b5ea5439913743774a89ee715524f64f0fe373","datavalue":{"value":{"entity-type":"item","numeric-id":3128468,"id":"Q3128468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aec71540f4c70cfafaff9b8dbf49a1a400cf542f","datavalue":{"value":{"amount":"+0.8305031657218933","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":"Q1778059$F1A298FF-4056-4C74-BEF8-194733BB1FCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7d5ff79fb32e959dc15b5ed38278c2ea3fe7f5f","datavalue":{"value":{"entity-type":"item","numeric-id":1407530,"id":"Q1407530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aec71540f4c70cfafaff9b8dbf49a1a400cf542f","datavalue":{"value":{"amount":"+0.8305031657218933","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":"Q1778059$5B1C67F2-0DA8-4BA4-8785-63D8A4A35DD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce9c6e8e62e5587d3df40fe3ffbe7dd8008e7afb","datavalue":{"value":{"entity-type":"item","numeric-id":2566062,"id":"Q2566062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"537a4725079d50c1d49626a50bfcfa8752dfc8f9","datavalue":{"value":{"amount":"+0.8273203372955322","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":"Q1778059$A385A28A-3C0D-44E8-8C77-70F06D7A76E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d1c7427d3c71381a2d1d6b79725a7a3c51f38cf","datavalue":{"value":{"entity-type":"item","numeric-id":1399101,"id":"Q1399101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b98b02907a8c724fa4f245f84a4c380a5c7a7f8","datavalue":{"value":{"amount":"+0.8028147220611572","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":"Q1778059$C984E55A-812B-43F3-AAF8-42FC2CF75D66","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Epsilon substitution for transfinite induction","badges":[]}}}}}