{"entities":{"Q1766923":{"pageid":1777665,"ns":120,"title":"Item:Q1766923","lastrevid":48426259,"modified":"2026-01-04T17:06:52Z","type":"item","id":"Q1766923","labels":{"en":{"language":"en","value":"Weak theories of linear algebra"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2140314"}},"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":"Q1766923$1A6F2295-BB51-4B9A-B0F7-7B14098369FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7bf9470c51878ea6befc7dafcbfb41079d2aee53","datavalue":{"value":{"text":"Weak theories of linear algebra","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1766923$134860E1-4BA1-40FA-9CCE-D7CF65CBBE20","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ca39e2d6a0bf7b3db0dd36d31cff947f5ff3fd0f","datavalue":{"value":"1064.03037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$A9191BB3-0BFB-46FD-AC21-4284CFF48E15","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"20891ef55d2a5c027c71fa5443ab52ee86634717","datavalue":{"value":{"entity-type":"item","numeric-id":647333,"id":"Q647333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$D6659305-9D63-4094-AB90-EB65A8417AEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"06644c28854d4134a09144ca7d53b7f0310fd152","datavalue":{"value":{"entity-type":"item","numeric-id":453197,"id":"Q453197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$7192EC1C-357C-425C-A9A5-12598C6817F1","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":"Q1766923$65CD74E8-6BCB-47C8-B23E-4218B6AC66FE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"76a1c0b70526daf2b9a458bd5b057271ea98bbdf","datavalue":{"value":{"time":"+2005-03-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1766923$C2EA3DD6-B6EF-4A76-9707-777681159EC8","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"31e2a6b93c73ac238bcf3e2582b229610ebcfce6","datavalue":{"value":"Linear algebra is considered as a source for hard tautologies separating the Frege and Extended Frege propositional proof systems. In his previous works, the second author studied this problem, particularly the question of whether commutativity of matrix inverses has polysize Frege proof, by providing three weak formal theories; the first covering the basic ring properties of matrices, the second extending it with a new function to manipulate matrix powering, and the third in addition enjoying induction on formulas with bounded universal matrix quantifiers.  This paper investigates the theories in more detail. The authors give sentences separating quantified versions of these theories. The above-mentioned commutativity of inverses, which has been shown to be provable in the third theory, is shown to be provable even in such a fragment that is obtained by extending the first by allowing induction on formulas with bounded existential matrix quantifiers. The fragment is also shown to be powerful enough to interpret a weak theory \\(V^1\\) of bounded arithmetic in it and to carry out polynomial-time reasoning about matrices. Thus, for example, one can formulize the Gaussian elimination algorithm in it.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$0CF3C56D-B4C0-4048-813C-5E0002878ECA","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$7DFBACF7-3F9B-4C3A-B8B6-E676C14BC9C1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$B4EBE70D-F23E-42F4-A97E-E4E1BF9577C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$A1D821A7-D267-4E42-9BB9-1A2F0C28EB8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b06ff2ef9e04b42ff2c5c43e297cd9d734a55887","datavalue":{"value":"15A24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$02D604D1-4EBA-42F7-AB98-BEDCF8FEFC58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bdf22674356d70b9e3ec0769d180c8975ea8910e","datavalue":{"value":"15A27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$9FB880DE-BC7D-4AB2-8056-5F1B93DE7ED0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3c5f76df4ba1bf2b661eb69cf1b7f68afcaf31de","datavalue":{"value":"2140314","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$410F4520-2B1E-4709-8BFE-929956687A70","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"17ef7db62ea690b4e5062dfc499cec745f9bc958","datavalue":{"value":"linear algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$B2BC7C34-C176-4A41-82F7-AEA168BA93B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ee539f3c66b5148353f42975573a39b50c5340f","datavalue":{"value":"complexity of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$F553C9D6-9A27-4B03-8FB3-4D8B8AEB5EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"112085ac92c50d8913b25f9b12f0d850c84ba71d","datavalue":{"value":"Frege propositional proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$7BF8071D-98AB-4C31-A2E5-8F9B23C70F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ebc71b77c09281a99491dbf18aaa0d5c4bffff5","datavalue":{"value":"polysize Frege proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$2F3B2820-2BE6-4784-8EAE-7EB2D3EBEB3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ccfbdce029dcd93610c89a3c36c2dd0b5ae48527","datavalue":{"value":"polynomial time reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$0D10F16A-736D-4C56-9550-747883A8D843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bb34100c65849dd3ad123f26090599d0f281ac6","datavalue":{"value":"commutativity of matrix inverse","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$56A9D2D3-BF25-40E5-B6AC-91F3558CD032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cba2903ab2dafc050042cd489ae05396ebe51a19","datavalue":{"value":"bounded arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$F930B5D3-57C0-45FC-B814-C1DDA19198E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"872aa6ff478bd546966da21f035ad879740af27b","datavalue":{"value":"Gaussian elimination algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1766923$44C01C89-BAFF-4D38-B0C7-68C665B5AF54","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":"Q1766923$FD07CB92-C65E-4290-8CB7-EB2DE0BE3432","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ef34399f9e2f81cb2d7c4a22dbf6240513a8cca3","datavalue":{"value":"https://doi.org/10.1007/s00153-004-0249-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q1766923$441FB049-2423-4F9C-9D9E-CD991DE99F8F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"81322dff101bc57e57193d2034ef98202a4127da","datavalue":{"value":"W1987241097","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$CEE4DD42-4029-471C-9CB1-70DA1A81C477","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"33c7a78759148ce6b1abced42ef4a952f4334dd8","datavalue":{"value":{"entity-type":"item","numeric-id":794429,"id":"Q794429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$F52624B6-C16F-4BDA-BBD0-CA8AEEA523C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85cb5c2591c3b4779c32d742e1061633a99acbed","datavalue":{"value":{"entity-type":"item","numeric-id":4850545,"id":"Q4850545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$4F37FF81-3E3F-46BD-96AD-E016C2D488C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"035feb3d68e7fcb8cc1f5afc2267fb8cc293e0bf","datavalue":{"value":{"entity-type":"item","numeric-id":3794177,"id":"Q3794177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$0E707D2E-5A21-480C-9519-912B9E11F204","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b90df03a170fcc85d9f6d5af38c0866a51f22b3f","datavalue":{"value":{"entity-type":"item","numeric-id":3694688,"id":"Q3694688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$3F70AF0B-C445-4F2B-8EF7-E474358CEE99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bbc797eb347c63de3fb7afafdf69b17eb33d87c","datavalue":{"value":{"entity-type":"item","numeric-id":4003421,"id":"Q4003421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$B60BD882-1AC6-4FE6-928A-70D6BF6B11A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73f4859b896346c19dda4c5c4345766d2110894c","datavalue":{"value":{"entity-type":"item","numeric-id":1886325,"id":"Q1886325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$63CC4150-F924-49CF-9025-0415057B65D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0c45ca7e85b7fc779ac39c5df64bc8fcd404d7c","datavalue":{"value":{"entity-type":"item","numeric-id":5687325,"id":"Q5687325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1766923$2E809498-B6DA-42E5-AE01-393487C6D19D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"895eb786399cb5ebf81cf5fbc8221268c4172b24","datavalue":{"value":"10.1007/S00153-004-0249-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1766923$DB06A1DB-B797-4CE8-AEED-8E1E3692DCDE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69e8b96e9b34a3808f72ead488ca3b7947fa6bcf","datavalue":{"value":{"entity-type":"item","numeric-id":1886325,"id":"Q1886325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"193b9cc4e8874f8ba9e0667d58a74639ac221988","datavalue":{"value":{"amount":"+0.8062368631362915","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":"Q1766923$E5A024ED-3697-4C42-8CC9-E145C808A256","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b7dc5e5e540adf127a4dd9000f77502f11e4203","datavalue":{"value":{"entity-type":"item","numeric-id":5901152,"id":"Q5901152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21cce54e4f34399f93aaf4c71d71f2f3f82e5ee9","datavalue":{"value":{"amount":"+0.7867487668991089","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":"Q1766923$A7EB367D-CF80-476D-A107-8906132FB81A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73a76c54a723d94007f00f0da302e5344556a97a","datavalue":{"value":{"entity-type":"item","numeric-id":5891510,"id":"Q5891510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0eb56f3b32c5730864e864fe484996b764e1ae7e","datavalue":{"value":{"amount":"+0.7857723236083984","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":"Q1766923$193DDDE1-B1A6-44C0-A02E-FD69AB4F421E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b00f560a88229e187a9d0857824bcccd60915c1","datavalue":{"value":{"entity-type":"item","numeric-id":2581274,"id":"Q2581274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1befc8cebdbcff0cb301edde786033f1fe59e450","datavalue":{"value":{"amount":"+0.7711451053619385","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":"Q1766923$A185448D-F089-4FE6-821F-B8CD1D3AEE91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e015d4792a0df6f68d5215099472987a4105131a","datavalue":{"value":{"entity-type":"item","numeric-id":5394597,"id":"Q5394597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ed7144e4de069c60983e7265117d3373e023c5e","datavalue":{"value":{"amount":"+0.7635908722877502","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":"Q1766923$C3B18A7A-4219-4E04-9D0F-62C52952081C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1766923","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1766923"}}}}}