{"entities":{"Q923067":{"pageid":924915,"ns":120,"title":"Item:Q923067","lastrevid":65376975,"modified":"2026-04-12T02:10:43Z","type":"item","id":"Q923067","labels":{"en":{"language":"en","value":"New proof of the solvability of the elementary theory of linearly ordered sets"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4170863"}},"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":"Q923067$E43BEE98-5F5A-4CDC-8389-A70EBF7F2043","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"27ad574d2b0014b2cee339ce4797e1cb57357222","datavalue":{"value":{"text":"New proof of the solvability of the elementary theory of linearly ordered sets","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q923067$F79F975F-31E8-4F35-B719-6057C0E1F5D3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e17fccafaf20b3ff1a3984a585811193c8539b91","datavalue":{"value":"0712.03005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$416BEB25-96CA-4674-AAAA-88893F9033DE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1fdf58adee21870a11df7dfd840d712bc17f8604","datavalue":{"value":"10.1007/BF01158085","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$1DD4EB3B-C9EB-49F9-9885-FCF8D9C16132","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"00de3e6b6cfff0576fe0e1d6bc63c05579d2cb43","datavalue":{"value":{"entity-type":"item","numeric-id":173953,"id":"Q173953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923067$8AA8C0CE-446D-4D26-B79E-027ADA85EB41","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":"Q923067$05CCD51C-DB14-4935-A214-DE8A602DD0AF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fbe57cb33b1b7c4bcf3f9bf8797d0ed750dc98b0","datavalue":{"value":"The first-order theory of linearly ordered sets (LOS) is known to be decidable. Two proofs of its decidability were proposed. \\textit{H. L\u00e4uchli} and \\textit{J. Leonard} [Fundam. Math. 59, 109-116 (1966; Zbl 0156.253)] proved it by presenting a constructive description of countermodels; this proof gives no explicit upper time-bound. Rabin's proof [\\textit{M. O. Rabin}, Handbook of Mathematical Logic, Stud. Logic Found. Math. 90, 595-629 (1977; Zbl 0443.03001)] is by embedding LOS to the theory S2S of two successor functions; it gives an upper time-bound of the algorithm, and also a lower bound.    The author gives a straightforward decidability algorithm with the same upper bound as Rabin's. The idea is to associate a finite set of ``feasible projects'' to each theory T; a project is a sequence \\(T_ 0,a_ 1,T_ 1,...,a_ k,T_ k\\) of theories and constants. Then, by constructing paths in the set of all feasible projects, we either obtain a model for T or prove that T is inconsistent.","type":"string"},"datatype":"string"},"type":"statement","id":"Q923067$4FFE03F2-1B78-42A2-BDE8-60AC954E554B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$A19CC777-3A0C-4755-9E51-58CBE0FF8677","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24363e421bb7b6dfa7fe7a9b1ee54d8da8a06bf1","datavalue":{"value":"06A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$FABB33A8-84B3-414A-A471-DD4D0114C0D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$BCB2123B-1D87-40E2-BE1D-6B1B652A765F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ae634aa6c44e7229bd8eba01e7b9aada275c3737","datavalue":{"value":"4170863","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$A8448281-5960-404B-8A74-799405FB0144","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6cca8f29e9719162ae360ad8baadd922d1f8e30","datavalue":{"value":"first-order theory of linearly ordered sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q923067$5F915A15-7396-4828-BC98-0B9741EBCFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b145c7dd496fc919a38fff332a78311d2a674839","datavalue":{"value":"decidability algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q923067$BE4B5F8C-A8DF-420D-97CC-CA13AE0B200A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a878a6ace55a42ed0f1b3e5cefb54bfc6712237b","datavalue":{"value":{"entity-type":"item","numeric-id":1275007,"id":"Q1275007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923067$821E156D-1F74-4D8E-BAF2-9DDDA61EBE42","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":"Q923067$6ADB9692-4862-4FE4-B268-F253131D82D1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b54f7383e1361db9b7d8d635e3974eec1f15734d","datavalue":{"value":{"entity-type":"item","numeric-id":5536269,"id":"Q5536269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923067$658B7174-21E9-44D9-BDCA-18129DECAA16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c74e20c9157021aaf7d8167c88d779be5f8df1","datavalue":{"value":{"entity-type":"item","numeric-id":1233019,"id":"Q1233019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923067$B4AD7E74-C615-4E04-91FC-8EB4AD84E3CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8be0495d64096cf5857288714f52e73333d7204f","datavalue":{"value":"https://doi.org/10.1007/bf01158085","type":"string"},"datatype":"url"},"type":"statement","id":"Q923067$D2FF1021-E5A8-40A0-B5C8-323C2B742285","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"80f58d75a5180cfc2ff85561eaa3112a8ad7d306","datavalue":{"value":"W2075243440","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923067$57226147-E67F-4412-A979-0133545D7622","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6c58205addc674c4d8bf6232eb40acc6101d995","datavalue":{"value":{"entity-type":"item","numeric-id":1062669,"id":"Q1062669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e2a34f951dd1b7ac59e45321ebcc5be924bcaee","datavalue":{"value":{"amount":"+0.757655680179596","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":"Q923067$C5F87EC6-0ACA-4AAA-8B56-560796C06ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4f7881f86f308faed7549e24ff0faacd18739f7","datavalue":{"value":{"entity-type":"item","numeric-id":3758805,"id":"Q3758805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0787968652ef5a31e5e3aef57976a76ec944061e","datavalue":{"value":{"amount":"+0.7212997674942017","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":"Q923067$D40D912F-B1B8-440A-B2D0-6341B948108F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38ca0b1fc6919732dbb68b471a80bae2e8609924","datavalue":{"value":{"entity-type":"item","numeric-id":4395558,"id":"Q4395558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5513fc6d0e49f28609ac7940e0a38e3f02fba0f","datavalue":{"value":{"amount":"+0.7122354507446289","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":"Q923067$FB690A54-1025-4AFF-B2B9-EDB43DC0B041","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"New proof of the solvability of the elementary theory of linearly ordered sets","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/New_proof_of_the_solvability_of_the_elementary_theory_of_linearly_ordered_sets"}}}}}