Title: Some elementary examples on the need for radical membership checking in mechanical theorem proving in geometry Authors: Eugenio Roanes-Lozano, Eugenio Roanes-Macias Extended Abstract: [I] Preliminary notes An ideal of a ring is a special subset of a ring such that it is also a ring and the product of any element of the ring with an element of the subset is again in the subset. For example, the set of even numbers is an ideal of the integers. The radical of an ideal I, Rad(I), is the set of elements, alpha, such that some integer power of alpha is in I. Rad(I) is also an ideal and I is obviously contained in Rad(I). For instance, in Z, the radical of the ideal of the set of multiples of 9 is the set of multiples of 3. A basis of an ideal is a set of generators of the ideal (i.e., the elements of the ideal are the linear algebraic combinations of the elements in the basis). The ideal generated by the polynomials p_1,...,p_n is denoted . A Groebner basis of a polynomial ideal is a very special basis. Once the way the monomials have to be ordered and the order for the variables are fixed, the (reduced) Groebner basis of an ideal is unique (that is, it completely characterizes the ideal). Moreover, Buchberger's algorithm provides a method to obtain the Grobner basis of any ideal of a polynomial ring. As a consequence, checking some very complex algebraic issues turns easily decidable. For instance, checking whether two ideals of a polynomial ring are equal or not can be decided by simply comparing their (reduced) Grobner bases. An algebraic variety is the set of solutions of a system of polynomial equations (that is, the set of zeros of the ideal generated by the corresponding polynomials). We shall denote by v(I) the algebraic variety of ideal I. The ideal of an algebraic variety V, i(V), is the set of all polynomials which vanish on all the points of the set V. This set turns out to be an ideal. Hilbert's Nullstellensatz states that, if the base field is algebraically closed, i(v(I))=Rad(I). Example: v()={(0,1)} i({(0,1)})= that is: i(v())= and: =Rad() [II] Yet another preliminary note In logic, a formula F' is a tautological consequence of a formula F if every valuation that causes F to be true also causes F' to be true. This situation is denoted F |= F'. In classic Boolean logic it is equivalent to the formula F => F' being a tautology (i.e., being always true). If S is a set of polynomial equations and p is a polynomial equation (all in the same polynomial ring), what does it mean that S => p ? For instance, if we say (in C) that: x-3_{120^0}=0 => x^3-27=0 (where 3_{120^0} represents the complex number of modulus 3 and argument 120 degrees), we are thinking that all the solutions of the LHS equation satisfy the RHS equation. For example, if we say (in R^2) that: {x+y-2=0,x-y=0} => x-1=0, we are thinking that all the solutions of the LHS linear system satisfy the RHS equation. [III] About the talk proposal In his famous 1988 book ``Mechanical Geometry Theorem Proving'', Shang-Ching Chou details a method with two steps (page 78) to check whether a geometric theorem is ``generally true'' or not using Groebner bases. The adjective ``generally'' is used because there can be degenerated cases (like a triangle degenerating into a segment when its three vertices are aligned). Let us note that there is some controversy on what actually means ``generally true'', but we shall not address this topic here, as it deals with complex issues as the distinction between parameters and free variables in special cases. These are deep waters, Watson. Roughly speaking, we can describe the underlying idea as follows. Let H be the ideal describing the hypotheses polynomials and let t be the thesis polynomial. 1st Step (ideal membership): If t belongs to H, t is a linear algebraic combination of some of the elements in H. Consequently, at the points where all the polynomials in H vanish, any linear algebraic combination of these polynomials will vanish, so t will also vanish. Consequently, v(H) is a subset of v(). Therefore, according to the ideas in [II], the theorem is ``generally true''. But the 1st step is only a sufficient condition. If the base field is algebraically closed, i(v(I))=Rad(I), and it is not complicated to prove that a necessary and sufficient condition is: 2nd Step (radical membership): If t belongs to Rad(H), the theorem is ``generally true''. Chou mentions at the same page 78: ``However, for all theorems we have found in practice, H=Rad(H).'' (that is, to check the 1st step was always sufficient in practice). In his 2007 book ``Selected topics in geometry with classical vs. computer proving'', Pavel Pech shows a beautiful example (Section 8.1) where H is not equal to Rad(H), that is, checking the radical membership, not only the ideal membership, is required. This example is about the planarity of a (3D) regular skew (equilateral) pentagon. We shall begin by revisiting Pech's example using the computer algebra system Maple. Using a kind of ``reverse engineering'' we shall show how to easily find examples of theorems where to check the radical membership is required. The idea is just to construct a hypotheses ideal such that the ideal of its variety is not itself (i.e., an ideal such that it is not equal to its radical) and an adequate thesis polynomial. We shall illustrate this with trivial examples: one involving two circles and a cubic, another one involving three parabolae, another one involving two circumferences and a line,... Summarizing, Pech's example is not an isolated rare case. Moreover, there are examples so simple that can arise precisely when introducing mechanical theorem proving, so we should be careful when introducing this topic.