{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T16:49:24Z","timestamp":1777481364673,"version":"3.51.4"},"reference-count":13,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    In this article we extend the algebraic theory of ordered fields [6], [8] in Mizar. We introduce extensions of orderings: if\n                    <jats:italic>E<\/jats:italic>\n                    is a field extension of\n                    <jats:italic>F<\/jats:italic>\n                    , then an ordering\n                    <jats:italic>P<\/jats:italic>\n                    of\n                    <jats:italic>F<\/jats:italic>\n                    extends to\n                    <jats:italic>E<\/jats:italic>\n                    , if there exists an ordering\n                    <jats:italic>O<\/jats:italic>\n                    of\n                    <jats:italic>E<\/jats:italic>\n                    containing\n                    <jats:italic>P<\/jats:italic>\n                    . We first prove some necessary and su cient conditions for\n                    <jats:italic>P<\/jats:italic>\n                    being extendable to\n                    <jats:italic>E<\/jats:italic>\n                    , in particular that\n                    <jats:italic>P<\/jats:italic>\n                    extends to\n                    <jats:italic>E<\/jats:italic>\n                    if and only if the set\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2023-0027_ieq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <m:mrow>\n                            <m:mi>Q<\/m:mi>\n                            <m:mi>S<\/m:mi>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:mi>E<\/m:mi>\n                            <m:mo>:<\/m:mo>\n                            <m:mo>=<\/m:mo>\n                            <m:mrow>\n                              <m:mo>{<\/m:mo>\n                              <m:mrow>\n                                <m:mo>\u2211<\/m:mo>\n                                <m:mrow>\n                                  <m:mi>a<\/m:mi>\n                                  <m:mo>*<\/m:mo>\n                                  <m:msup>\n                                    <m:mrow>\n                                      <m:mi>b<\/m:mi>\n                                    <\/m:mrow>\n                                    <m:mn>2<\/m:mn>\n                                  <\/m:msup>\n                                  <m:mo>|<\/m:mo>\n                                  <m:mi>a<\/m:mi>\n                                  <m:mo>\u2208<\/m:mo>\n                                  <m:mi>P<\/m:mi>\n                                  <m:mo>,<\/m:mo>\n                                  <m:mi>\u2009<\/m:mi>\n                                  <m:mi>\u2009<\/m:mi>\n                                  <m:mi>b<\/m:mi>\n                                  <m:mo>\u2208<\/m:mo>\n                                  <m:mi>E<\/m:mi>\n                                <\/m:mrow>\n                              <\/m:mrow>\n                              <m:mo>}<\/m:mo>\n                            <\/m:mrow>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>QS\\,\\,E: = \\left\\{ {\\sum {a*{b^2}|a \\in P,\\,\\,b \\in E} } \\right\\}<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is a preordering of\n                    <jats:italic>E<\/jats:italic>\n                    \u2013 or equivalently if and only if \u22121\n                    <jats:italic>\/<\/jats:italic>\n                    \u2209\n                    <jats:italic>QS E<\/jats:italic>\n                    . Then we show for non-square\n                    <jats:italic>a<\/jats:italic>\n                    \u2208\n                    <jats:italic>F<\/jats:italic>\n                    that\n                    <jats:italic>P<\/jats:italic>\n                    extends to\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2023-0027_ieq_002.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <m:mrow>\n                            <m:mi>F<\/m:mi>\n                            <m:mrow>\n                              <m:mo>(<\/m:mo>\n                              <m:mrow>\n                                <m:msqrt>\n                                  <m:mi>a<\/m:mi>\n                                <\/m:msqrt>\n                              <\/m:mrow>\n                              <m:mo>)<\/m:mo>\n                            <\/m:mrow>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>F\\left( {\\sqrt a } \\right)<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    if and only if\n                    <jats:italic>P<\/jats:italic>\n                    and finally that every ordering\n                    <jats:italic>P<\/jats:italic>\n                    of\n                    <jats:italic>F<\/jats:italic>\n                    extends to\n                    <jats:italic>E<\/jats:italic>\n                    if the degree of\n                    <jats:italic>E<\/jats:italic>\n                    over\n                    <jats:italic>F<\/jats:italic>\n                    is odd.\n                  <\/jats:p>","DOI":"10.2478\/forma-2023-0027","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T10:21:49Z","timestamp":1704450109000},"page":"341-352","source":"Crossref","is-referenced-by-count":0,"title":["Extensions of Orderings"],"prefix":"10.2478","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9587-8737","authenticated-orcid":false,"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[{"name":"Institute of Informatics , University of Gda\u0144sk , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2023,12,31]]},"reference":[{"key":"2026042801423943978_j_forma-2023-0027_ref_001","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026042801423943978_j_forma-2023-0027_ref_002","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Christoph Schwarzweller. Equality in computer proof-assistants. In Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin, editor, Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, volume 5 of ACSIS-Annals of Computer Science and Information Systems, pages 45\u201354. IEEE, 2015. doi:10.15439\/2015F229.","DOI":"10.15439\/2015F229"},{"key":"2026042801423943978_j_forma-2023-0027_ref_003","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of Annals of Computer Science and Information Systems, pages 363\u2013371, 2016. doi:10.15439\/2016F520.","DOI":"10.15439\/2016F520"},{"key":"2026042801423943978_j_forma-2023-0027_ref_004","doi-asserted-by":"crossref","unstructured":"Artur Korni\u0142owicz. Flexary connectives in Mizar. Computer Languages, Systems & Structures, 44:238\u2013250, December 2015. doi:10.1016\/j.cl.2015.07.002.","DOI":"10.1016\/j.cl.2015.07.002"},{"key":"2026042801423943978_j_forma-2023-0027_ref_005","unstructured":"Serge Lang. Algebra. PWN, Warszawa, 1984."},{"key":"2026042801423943978_j_forma-2023-0027_ref_006","doi-asserted-by":"crossref","unstructured":"Alexander Prestel. Lectures on Formally Real Fields. Springer-Verlag, 1984.","DOI":"10.1007\/BFb0101548"},{"key":"2026042801423943978_j_forma-2023-0027_ref_007","unstructured":"Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026042801423943978_j_forma-2023-0027_ref_008","unstructured":"Knut Radbruch. Geordnete K\u00f6rper. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026042801423943978_j_forma-2023-0027_ref_009","doi-asserted-by":"crossref","unstructured":"Piotr Rudnicki, Christoph Schwarzweller, and Andrzej Trybulec. Commutative algebra in the Mizar system. Journal of Symbolic Computation, 32(1\/2):143\u2013169, 2001. doi:10.1006\/jsco.2001.0456.","DOI":"10.1006\/jsco.2001.0456"},{"key":"2026042801423943978_j_forma-2023-0027_ref_010","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Normal extensions. Formalized Mathematics, 31(1):121\u2013130, 2023. doi:10.2478\/forma-2023-0011.","DOI":"10.2478\/forma-2023-0011"},{"key":"2026042801423943978_j_forma-2023-0027_ref_011","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Field extensions and Kronecker\u2019s construction. Formalized Mathematics, 27(3):229\u2013235, 2019. doi:10.2478\/forma-2019-0022.","DOI":"10.2478\/forma-2019-0022"},{"key":"2026042801423943978_j_forma-2023-0027_ref_012","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Ordered rings and fields. Formalized Mathematics, 25(1):63\u201372, 2017. doi:10.1515\/forma-2017-0006.","DOI":"10.1515\/forma-2017-0006"},{"key":"2026042801423943978_j_forma-2023-0027_ref_013","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller and Agnieszka Rowi\u0144ska-Schwarzweller. Quadratic extensions. Formalized Mathematics, 29(4):229\u2013240, 2021. doi:10.2478\/forma-2021-0021.","DOI":"10.2478\/forma-2021-0021"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2023-0027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:12:18Z","timestamp":1777385538000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2023-0027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":13,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,12,31]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0027"],"URL":"https:\/\/doi.org\/10.2478\/forma-2023-0027","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}