{"entities":{"Q1130508":{"pageid":1141257,"ns":120,"title":"Item:Q1130508","lastrevid":66849945,"modified":"2026-04-12T13:16:34Z","type":"item","id":"Q1130508","labels":{"en":{"language":"en","value":"A formal system of first-order predicate calculus with infinitely long expressions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3176037"}},"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":"Q1130508$9D0495D9-3F96-461D-8A19-7CC4569F100A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"37833533262287226c2232978fc07d5394acabc9","datavalue":{"value":{"text":"A formal system of first-order predicate calculus with infinitely long expressions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1130508$C6F3D6A3-9796-4A1A-8AEA-B2991A80D1BA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0525c5ae1fe02b55b2f0e9a8b62567f5a2f12458","datavalue":{"value":"0108.00203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130508$D7A781C0-D7B8-439D-87C6-0C97719BC470","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3a0bf1dfe04ad12e1226221d4ab68e1adf5a243","datavalue":{"value":{"entity-type":"item","numeric-id":766668,"id":"Q766668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130508$92B9144F-D8AA-43E7-B141-AE512D685D63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"057136d60f841fac35f8dec23b81e4925462b1bc","datavalue":{"value":{"entity-type":"item","numeric-id":768306,"id":"Q768306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130508$1DA7C04B-9C19-42EE-8A5B-CDBDD1867F6C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e6db4bd470edb111094f50a346a34a8ff7644b14","datavalue":{"value":{"entity-type":"item","numeric-id":176973,"id":"Q176973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1130508$2E52422B-5580-42C2-B3D2-7E84B54A2E65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f1151d44c801a909256f62362ee2b01f3c904af1","datavalue":{"value":{"time":"+1962-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":"Q1130508$C7B958CC-FEAC-4127-A311-0579A1E3B777","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"78e80e002ecfe0cfe8031a32ea02e2a730f4d4a8","datavalue":{"value":"For any fixed strongly inaccessible number \\(\\Omega_0\\) the authors consider a language whose notion of well-formed formula is defined roughly as follows:   (i) Prime formulas are predicate symbols followed by a well-ordered sequence of terms whose order-type is less than \\(\\Omega_0\\).    (ii) If \\(A\\), \\(A_\\lambda\\) are formulas for all \\(\\lambda< \\alpha <\\Omega_0\\) then \\(\\dashv A\\) and \\(\\bigvee_{\\lambda< \\alpha}A_\\lambda\\) are formulas.    (iii) If \\(A(a_0, a_1, \\ldots)\\) is a formula containing the well-ordered sequence (of type \\(< \\Omega_0\\)) \\(a_0, a_1, \\ldots\\) of distinct free variables then \\((\\exists\\) \\(x_0, x_1,\\ldots)\\) \\(A(x_0, x_1,\\ldots)\\) is a formula where \\(x_0, x_1,\\ldots\\) is a sequence of distinct bound variables.   A Gentzen-type set of rules of proof is then proposed and proven semantically complete by adapting Sch\u00fctte's method [\\textit{K. Sch\u00fctte}, Arch. Math. Logik Grundlagenforsch. 2, 55--67 (1956; Zbl 0071.00802)] for a proof of the corresponding result for first order predicate logic. This proof also gives a L\u00f6wenheim-Skolem-type theorem. The authors prove furthermore the cut-elimination theorem and Craig's interpolation theorem for their system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$851AAA2B-4CC4-4C2B-BF4F-96CBB4BB35CA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130508$A2B70DE4-0BC9-4F83-82ED-01BD4AC540D8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3df4afc3330a85c3824cddce0c8300b61475a7e3","datavalue":{"value":"3176037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130508$2BE4698F-4105-42EB-AAE1-23374B20D6F4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a250535976c55d0d83f766a663ca018f553759e","datavalue":{"value":"first-order predicate calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$816681C6-CD37-4DE4-AEDF-B8118860CC12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45837db5d91616d28a9467a7a98a897f638daaa7","datavalue":{"value":"infinitely long expressions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$67709210-8926-4ED7-8F03-A4F1708A917F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd642eae7c452120ef36463615d24a90145f1de2","datavalue":{"value":"Gentzen-type set of rules of proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$017DFBE2-3D38-46DE-9180-D27DE85CB1E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05ea7bb225dfc0f1ba88b53ac8e959b98d283c0d","datavalue":{"value":"semantic completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$86425427-EBED-4EA3-B5EC-D9E923161B78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"527469ab44a4fb0e862f1df2a860c330d63181be","datavalue":{"value":"Sch\u00fctte's method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$BE7F18B8-EA09-416A-8267-2F2A3D53B04D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0f25cad7a25dc79e00a4781379882f45724c376b","datavalue":{"value":"L\u00f6wenheim-Skolem-type theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$5AB58BFA-26BC-4E3E-9DBD-4A8794C8E8F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97cfbdd458b576a7e018dc279ea34c5cb4040b6f","datavalue":{"value":"cut-elimination theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$52BC984B-C237-43CD-8DD7-E08770D7D39D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1093f6950436e6545be25dd909b86fbd17fd071e","datavalue":{"value":"Craig's interpolation theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1130508$F1E07F52-D0FF-4726-B0A2-DBB6889A1F3D","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":"Q1130508$01488934-AE81-4853-A0C2-823862D97D9B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"919fe1226e4464d4f8d636da110b493173d65ae5","datavalue":{"value":"https://doi.org/10.2969/jmsj/01340357","type":"string"},"datatype":"url"},"type":"statement","id":"Q1130508$A7E158D4-00A9-4443-B481-B39B120366F6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"99a8b4ac1ff52d788fd10c969a753ffd6cc76d1d","datavalue":{"value":"W2018651033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130508$D2ED3C97-C32D-4AC6-B72A-3E0B2F9A759F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"75453e90341348caca4e62f30fc4b76821440a12","datavalue":{"value":"10.2969/JMSJ/01340357","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1130508$C44D0F3A-813F-492D-9E16-23B1ED5BB244","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11218fbe1f1a18f12bf4e470496b571975108524","datavalue":{"value":{"entity-type":"item","numeric-id":5722255,"id":"Q5722255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07a4009eaa1a35445cf8a647874a74184ad85fb0","datavalue":{"value":{"amount":"+0.7941739559173584","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":"Q1130508$16234E7D-D8FE-49EF-ABEC-32A777F322E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac6c80dd5eed50272b87cde60dca0b3d01259207","datavalue":{"value":{"entity-type":"item","numeric-id":5333393,"id":"Q5333393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f74ca8d1dae87d3bf4643ea14901b7ec02d09146","datavalue":{"value":{"amount":"+0.7374289035797119","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":"Q1130508$E5B44AC4-15C9-4CD9-BF5C-4BF02BF902E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40cdf0fbd9e8d32635ab7f0bb98b4632b971e66d","datavalue":{"value":{"entity-type":"item","numeric-id":5596727,"id":"Q5596727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2853c8f31f7bfefc67a2ab213232ce2615521fe5","datavalue":{"value":{"amount":"+0.7307793498039246","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":"Q1130508$821AA33B-8AED-4DA2-867E-8884FC7E1F9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b15d490d5d614fdc6287e6c580f5828c278116a6","datavalue":{"value":{"entity-type":"item","numeric-id":2639839,"id":"Q2639839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d5018f6db1896e7fa353b54b80cfc4ea1516276","datavalue":{"value":{"amount":"+0.7229081392288208","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":"Q1130508$C30058CF-5F83-4047-A60A-008FF02E74EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2edaffa804b74d87e038d748335f23a598307087","datavalue":{"value":{"entity-type":"item","numeric-id":1589838,"id":"Q1589838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b099522334e3a85e61415d99ede0d692437075b8","datavalue":{"value":{"amount":"+0.7190081477165222","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":"Q1130508$5CB1244C-8D14-49CA-9A89-26397A7E225B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A formal system of first-order predicate calculus with infinitely long expressions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_formal_system_of_first-order_predicate_calculus_with_infinitely_long_expressions"}}}}}