{"entities":{"Q1813063":{"pageid":1823805,"ns":120,"title":"Item:Q1813063","lastrevid":69068742,"modified":"2026-04-13T04:23:25Z","type":"item","id":"Q1813063","labels":{"en":{"language":"en","value":"Remarks on Herbrand normal forms and Herbrand realizations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2024"}},"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":"Q1813063$3F90F601-BDF2-4B38-9189-8E1BAB7D64DB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5357bee38ecb3cae493c5bc91a8cc002e6ba2558","datavalue":{"value":{"text":"Remarks on Herbrand normal forms and Herbrand realizations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1813063$64C2EE79-BCAB-43FF-A05A-A91A0CEB39A8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"88c8bfed6f20c7907bf95492d25fa37b52ea1b09","datavalue":{"value":"0742.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$2FC040B0-3129-4581-BDA5-961CD93CEAB6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"265459f0dcb5439ddea2766caf8d54df840ac327","datavalue":{"value":"10.1007/BF01627504","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$E0CD2800-6062-4B4C-ADCD-7A6540EA74F5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3757c450e8ea3891f056e58fdb032b2670ff909f","datavalue":{"value":{"entity-type":"item","numeric-id":175049,"id":"Q175049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$C6C4A916-9838-495B-8796-16546392FC2A","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":"Q1813063$498EC51D-377F-40B0-A04C-D497EE811519","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d3f790682a6be4cc1f3210e15eebe1d6cc5ffbc2","datavalue":{"value":{"time":"+1992-06-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1813063$9E204433-673A-4355-9611-312B3A405978","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3d96b425295dc6363dea3b4f988dc173bd9b2494","datavalue":{"value":"Let \\(A^ H\\) be the Herbrand normal form of \\(A\\) and \\(A^{H,D}\\) a Herbrand realization of \\(A^ H\\). We show:   (i) There is an example of an (open) theory \\({\\mathcal T}^ +\\) with function parameters such that for some \\(A\\) not containing function parameters (1) \\({\\mathcal T}^ +\\vdash A^ H\\), \\(A^{H,D}\\), \\(\\;{\\mathcal T}^ +\\not\\vdash A\\).   (ii) Similarly for first order theories \\({\\mathcal T}\\) if the index functions used in defining \\(A^ H\\) are permitted to occur in instances of non- logical axiom schemata of \\({\\mathcal T}\\), i.e. for suitable \\({\\mathcal T}\\), \\(A\\): (2) \\({\\mathcal T}[f_ 1,\\ldots,f_ n]\\vdash A^ H\\), \\(\\;{\\mathcal T}\\not\\vdash A\\).   (iii) In fact, in (1) we can take for \\({\\mathcal T}^ +\\) the fragment \\((\\Sigma^ 0_ 1\\text{-IA})^ +\\) of second order arithmetic with induction restricted to \\(\\Sigma^ 0_ 1\\)-formulas, and in (2) we can take for \\({\\mathcal T}\\) the fragment \\((\\Sigma_ 1^{0,b}\\text{-IA})\\) of first order arithmetic with induction restricted to formulas \\(\\bigvee xA(x)\\), where \\(A\\) contains only bounded quantifiers.   (iv) On the other hand, (3) \\(PA^ 2\\vdash A^ H\\Rightarrow PA\\vdash A\\), where \\(PA^ 2\\) is the extension of first order arithmetic \\(PA\\) obtained by adding quantifiers for functions and \\(A\\in{\\mathcal L}(PA)\\). This generalizes to extensional arithmetic in the language of all finite types but not to sentences \\(A\\) with positively occurring existential quantifiers for functions.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1813063$834983D0-5E4F-4A54-B6F7-9525391AB223","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e5a9ddcfef477064bcaaf179121fdf3c5d566789","datavalue":{"value":{"entity-type":"item","numeric-id":175049,"id":"Q175049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$4C949D7A-5C35-469B-85D3-108BFA04FC0D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$D940DB3C-C9C5-432F-8B64-EB80BCC4FD40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$262DD458-53C9-4104-9F00-A00D8767F97F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$E57F7875-344B-45D5-B89B-17533C94BA5B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d6086034a4f80cffd0ddc7281474a25487ba61b7","datavalue":{"value":"2024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$86E19470-1F7B-4149-9C8C-CF0EEE213610","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8661572aaccc8ef90a52fd7944cc932d8244f9c1","datavalue":{"value":"Herbrand normal form","type":"string"},"datatype":"string"},"type":"statement","id":"Q1813063$7FEA1F8E-2680-441D-B6D0-2D192D0E7C43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0a4cc29be2c66702b46e42db9cafa46c6982c8a1","datavalue":{"value":"Herbrand realization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1813063$39FBC178-BA28-42AD-921A-ABD354EF4757","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":"Q1813063$864A98BA-A3CB-48A3-9A8D-DBA739795C80","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":"Q1813063$28C4B62D-E0F4-49CA-B234-D594B4232A30","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":"Q1813063$32E28578-E208-44D9-A57B-FDA74B005B89","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":"Q1813063$BF122510-7D81-46C5-B0DB-7AAD6E9557BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$C847C548-0237-4E31-8A0C-9B8D6B65F732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d966d8fb41a3564f4060a1b833eb768ac2e0597d","datavalue":{"value":{"entity-type":"item","numeric-id":5806808,"id":"Q5806808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$4A21DDBE-ABFF-4294-9EE7-B300001D2755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bd72dbbdbb28e49bc58fdcc6d69fc1738d5bbb0","datavalue":{"value":{"entity-type":"item","numeric-id":5552747,"id":"Q5552747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$BBB04C92-194A-408B-9CBB-80C874FFABE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e173e3f88a53b33fbc52906169cfc40c731fbc22","datavalue":{"value":{"entity-type":"item","numeric-id":2560813,"id":"Q2560813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$239D46FD-25C6-4E2E-94CE-E82593C3DDE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d71305c8d9d041668e564bf7f2f69f04f88a1b7","datavalue":{"value":{"entity-type":"item","numeric-id":3822154,"id":"Q3822154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$11719D3C-C1EF-46EF-998E-3AA50058F600","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58cc241747ec6fa1130277e3fe9cbb65e8f8d05e","datavalue":{"value":{"entity-type":"item","numeric-id":5680103,"id":"Q5680103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$54A90066-D22E-4286-AABE-092C06249738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f40bcaa8d311e4db512eab174f3dec9cd00f54c","datavalue":{"value":{"entity-type":"item","numeric-id":5537599,"id":"Q5537599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$AF6AA702-C662-4AAF-8711-14C47B07834A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82318748b8514096d13bc80763ff6e3cbefb3d9","datavalue":{"value":{"entity-type":"item","numeric-id":762484,"id":"Q762484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$65B9A5A5-0A1E-42F9-8FA0-10E95561ACBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bacb5aa102ce6c71274c34a5360472cea903ae3a","datavalue":{"value":{"entity-type":"item","numeric-id":2641297,"id":"Q2641297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1813063$891678FB-415C-4A8E-B8D6-17DF961CA8F8","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":"Q1813063$33AD9938-C5F9-43A3-A572-2F9F6CAACD97","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5176abc815be6e68c0a58ea4a649bf9031d17da4","datavalue":{"value":"https://doi.org/10.1007/bf01627504","type":"string"},"datatype":"url"},"type":"statement","id":"Q1813063$6AB3CDB0-7A2F-4DDA-8990-F87D5D99C882","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"114b65fb8b5c927b61495814e2579336fcf2a182","datavalue":{"value":"W2086046439","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1813063$31D40F0B-3AEA-477E-9C53-810C4B8EACEC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbb77c33509eb13469d047cff62be4feedf5192b","datavalue":{"value":{"entity-type":"item","numeric-id":2641297,"id":"Q2641297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b61c09ea34e796453dcedbcb90dbde91054d81d","datavalue":{"value":{"amount":"+0.8030813932418823","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":"Q1813063$C1D067C3-E9D6-4E86-B8F5-165D1CF71BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bf689db4e35822175315748c96844ad3826c6cc","datavalue":{"value":{"entity-type":"item","numeric-id":3140639,"id":"Q3140639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"489569d777721445b1750a5c1bafa6ab4c4aac9e","datavalue":{"value":{"amount":"+0.7817961573600769","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":"Q1813063$ED0367CA-84CA-453B-9B84-DA43AA742174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b45db420521eb08f46a4d86a7c19498e5668c97","datavalue":{"value":{"entity-type":"item","numeric-id":2915894,"id":"Q2915894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f16ec41e38432d9cd0b6638f235b2afa6ebafa10","datavalue":{"value":{"amount":"+0.7627431750297546","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":"Q1813063$00C447D4-24EA-4662-B86E-F22CA7B97DC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36d26d19e51029fff8c07fa8c6a01d3f2b7a0bc0","datavalue":{"value":{"entity-type":"item","numeric-id":2377353,"id":"Q2377353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61877c9b77db9da726dd875efe8df78970771951","datavalue":{"value":{"amount":"+0.7578921318054199","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":"Q1813063$7893E6B8-921E-4754-B5D8-D14B8167F9D5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Remarks on Herbrand normal forms and Herbrand realizations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Remarks_on_Herbrand_normal_forms_and_Herbrand_realizations"}}}}}