Annals of Computer Science and Information Systems, Volume 15

DOI: http://dx.doi.org/10.15439/2018F88

Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 67–72 (2018)

Full text

Abstract. In this paper we develop a Mizar formalization of Kronecker's construction, which states that for every field $F$ and irreducible polynomial $p \in F[X]$ there exists a field extension $E$ of $F$ such that $p$ has a root over $E$. It turns out that to prove the correctness of the construction the field $F$ needs to provide a disjointness condition, namely $F \cap F[X] = \emptyset$. Surprisingly this property does not hold for arbitrary representations of a field $F$: We construct for almost every field $F$ another representation $F'$, i.e. an isomorphic copy $F'$ of $F$, not satisfying this condition. As a consequence to $F'$ our formalization of Kro\-necker's construction cannot be applied. All proofs have been carried out in the Mizar system. Based on Mizar's representation of the fields $\mathbb{Z}\_p, \mathbb{Q}$ and $\mathbb{R}$ we also have proven that $\mathbb{Z}\_p \cap \mathbb{Z}\_p[X] = \emptyset$, $\mathbb{Q} \cap \mathbb{Q}[X] = \emptyset$, and $\mathbb{R} \cap \mathbb{R}[X] = \emptyset$ respectively.

References

1. G. Bancerek, Tarski’s Classes and Ranks. Formalized Mathematics 1(3), 563–567, 1990.
2. G. Bancerek, Arithmetic of Non Negative Rational Numbers. Mizar Mathematical Library, 1998.
3. G. Bancerek et.al., Mizar: State-of-the-art and Beyond. in: M. Kerber et.al. (eds.), Proceedings of the 2015 International Conference on Intelligent Computer Mathematics, Lecture Notes in Computer Science 9150, 261–279, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_17
4. The Coq Proof Assistant. available at www.coq.inria.fr.
5. H.B. Enderton, Elements of Set Theory. Elsevier, 1977.
6. Y. Futa, H. Okazaki, and Y. Shidama, Set of Points on Elliptic Curve in Projective Coordinates. Formalized Mathematics 19(3), 131–138, 2011. http://dx.doi.org/10.2478/v10037-011-0021-6
7. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245, 2010. https://doi.org/10.6092/issn.1972-5787/1980
8. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, Equality in Computer Proof-Assistants. in: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds.), ACSIS, Vol. 5, 45–54, 2015. http://dx.doi.org/10.15439/2015F229
9. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, On Algebraic Hierarchies in Mathematical Repository of Mizar. in: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, 363–371, 2016. http://dx.doi.org/10.15439/2016F520
10. A. Grabowski and C. Schwarzweller, Translating Mathematical Vernacular into Knowledge Repositories. in: M. Kohlhase (ed.), Proceedings of the 4th International Conference on Mathematical Knowledge Management, Lecture Notes in Artificial Intelligence, 3863, 49–64, Springer Verlag, 2006.
11. A. Grabowski and C. Schwarzweller, On Duplication in Mathematical Repositories. in: S. Autexier et.al. (eds.), Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, 6167, 300-314, Springer Verlag, 2010.
12. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Four Decades of Mizar. Journal of Automated Reasoning, vol 55(3), 191–198, 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
13. J. Harrison, The HOL Light Theorem Prover. available at http://www.cl.cam.ac.uk/~jrh13/hol-light.
14. The HOL Interactive Theorem Prover. available at hol-theorem-prover. org.
15. Isabelle. available at isabelle.in.tum.de.
16. A. Korniłowicz, Quotient Rings. Formalized Mathematics 13(4), 573–576, 2005.
17. Mizar Home Page. available at www.mizar.org.
18. A. Naumowicz and A. Korniłowicz, A Brief Overview of Mizar. in: Theorem Proving in Higher Order Logics 2009, S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (eds.), Lecture Notes in Computer Science, 5674, 67–72, Springer Verlag, 2009.
19. P. Rudnicki, A. Trybulec, and C. Schwarzweller, Commutative Algebra in the Mizar System. Journal of Symbolic Computation, vol. 32(1/2), pp. 143–169, 2001. http://dx.doi.org/10.1006/jsco.2001.0456
20. C. Schwarzweller, A. Korniłowicz, and A. Rowińska-Schwarzweller, Some Algebraic Properties of Polynomial Rings. Formalized Mathematics 24(3), 227–237, 2016. http://doi.org/10.1515/forma-2016-0019
21. W.A. Trybulec, Vectors in Real Linear Space. Formalized Mathematics 1(2), 291–296, 1990.
22. A. Trybulec, A. Korniłowicz, A. Naumowicz, and K. Kuperberg, Formal Mathematics for Mathematicians. Journal of Automated Reasoning 50(2), 119–121, 2013. http://dx.doi.org/10.1007/s10817-012-9268-z
23. B. L. van der Waerden, Algebra Vol. I. 8th edition Springer Verlag 1990.
24. S. Weintraub, Galois Theory. 2nd edition Springer Verlag, 2008.
25. F. Wiedijk, Formalizing 100 Theorems. available at http://www.cs.ru.nl/~freek.