Detecting truth, just on parts

Abstract

We introduce, through a computational algebraic geometry approach, the automatic reasoning handling of propositions that are simultaneously true over some relevant collections of instances and false over some relevant collections of instances. A rigorous, algorithmic criterion is presented for detecting such cases, and its performance is exemplified through the implementation of this test within the dynamic geometry program GeoGebra. Our framework has some significant differences regarding some alternative, recent formulation of the “true on components” idea; differences and similarities between both approaches are discussed here.

1 Introduction

In this paper, we deal with a particular issue in automated proving and discovery of theorems in elementary geometry by algebraic geometry methods, namely, the case of statements that are neither valid nor their negations are valid (in some specific sense we will describe in detail below). Very roughly, the algebraic geometry approach to automated reasoning in geometry proceeds by translating a geometric statement $\{H\Rightarrow T\}$ into polynomial expressions, after adopting a coordinate system. Then, the geometric instances verifying the hypotheses H and the thesis T can be represented as the solution of a system of polynomial equations, $V(H)=\{h_1=0,\dots ,h_r=0\}$ and $V(T)=\{f=0\}$, describing the hypotheses and the thesis varieties.

Thus, when $V(H) \subseteq V(T)$ we can say that the theorem is valid, i.e.  always true, i.e. true for all instances of the hypotheses. But this fact rarely happens, even for well established theorems, because the algebraic translation of the geometric construction described by the hypotheses usually forgets explicitly excluding some degenerate cases (say, when a triangle collapses to a line, when two points defining a line become coincident, etc.) where the given statement fails. Unfortunately, many of these cases are not intuitively obvious and they are hard to detect a priori; even if detected, it happens that introducing negative hypotheses (i.e.  declaring that some geometric elements in the given statement should not verify a certain relation among them, such as the non-collinearity of the three vertices of a triangle) might involve some subtle issues, cf. [5, 8].

Thus, a delicate, but more useful, approach for automated reasoning consists in exhibiting, first, a collection of independent variables modulo H, so that no polynomial relation among them holds over the whole V(H). That is, identifying a collection of parameters describing the coordinates of the free elements in the given geometric statement. As we will show in the next section, such identification involves quite delicate issues; but let us concentrate here in providing just a rough description of the global procedure. Now, once such independent variables have been selected, the irreducible components of V(H) where these variables do not remain independent are assumed to describe degenerate instances. Thus, these components are, in some sense, negligible. Accordingly, a statement is called generally true if the thesis holds, at least, over all the non-degenerate components.

On the other hand, if over each non-degenerate component the thesis does not identically vanish, the statement is labeled as generally false: this includes the always false case, where the thesis never holds, i.e. when $\{f\ne 0\}$ over every point of V(H), and also the case when the equality $\{f = 0\}$ holds true just at some negligible set, i.e. over a degenerate component of V(H)) or over a proper subvariety of a non-degenerate component. See Fig. 1 for a graphical representation of all these terms and the relations among them. A more detailed description of this quite established terminology (with small variants) can be found, for instance, in the references [4, 12, 15].

Let us point out that it is within this more flexible concept of truth that the algebraic approach to automated theorem reasoning has shown all its capacity to verify and to discover thousands of geometric statements, either elementary or sophisticated. And, behind this success story lies the existence of algebraic methods to test the general truth or falsity of a statement without actually having to explicitly compute the decomposition of the given hypotheses variety on components, without finding which of these are degenerate or not, without verifying, one by one, over which components the thesis holds.... Thus, avoiding the use of costly primary decomposition algorithms is an implicit, but strong, restriction that the reader must keep in mind to truly understand what follows.

Fig. 1

Different types of truth for a geometry statement

It follows from the previous definition that to be generally true and to be generally false are incompatible; there can be no statement having both properties at once. On the other hand—and this is the object of interest in this paper—there are statements which happen to be, simultaneously, not generally true and not generally false. That is, statements that are both false over some non-degenerate component and that are true over some other non-degenerate component, i.e. statements that are true, just on some components. We have decided—for the better comprehension of this notion by general users of dynamic geometry programs implementing this feature, such as GeoGebra—to label such statements in a more colloquial way, as statements true on parts, false on parts. The specific framework for this concept, in the context of automated reasoning in geometry, is briefly motivated and justified in Sect. 2, where the basic definitions and other fundamental issues are precisely introduced.

It might seem, at first glance, that the true on parts, false on parts case is a useless oddity of the automated proving method, arising just in some very artificial statements without a real geometric motivation. But it is not so.

Intuitively speaking, a true on parts, false on parts situation is likely to arise when a geometric statement has some hypotheses that, under a unique algebraic formulation, yield substantially different geometric configurations. Moreover, this case usually happens when human intuition is prone to forget about the existence of all but one of such configurations. For a very simple example, let us consider that we are given two free points A, B and, then, we draw the circle c centered at A and passing through B. Let C, D be the two intersections of the circle c with the line f defined by A, B. Obviously, one of these intersection points coincide with B, say, (see Fig. 2) visually $B=C$. Now let us consider, as thesis, this equality $B=C$, and try to test its truth by using the automated reasoning tools in GeoGebra. The user might be surprised when the output of these tools is that, although the thesis is ”numerically true”, in purely symbolic terms is just true on parts, false on parts, since it is not possible, algebraically speaking, to isolate C and D without performing some kind of factorization, an option that is usually not included in the automatic reasoning programs, for its high computational cost.

Fig. 2

A simple case of true on parts, false on parts

Another example, of a different sort, could be the following (see Fig. 3). Let us consider a triangle ABC and let us project C over the line AB, yielding point E. Now, visually, it seems obvious that the lengths of the segments AE, EB, AB verify $AE+EB=AB$, but, again, since the definition of segment length involves some degree two expression, it happens that the thesis is true only for some choices of the roots of this algebraic equation, and false in the others. More in detail, assume $A=(0,0), B=(a, 0), C=(u,v), E=(u,0)$, that $x= \mathrm{length}(AE)$ is defined as $x^2=u^2$, and, likewise, $y=\mathrm{length}(AB)$ is $y^2-a^2$ and $z=\mathrm{length}(EB)$ as $z^2=(u-a)^2$. Then, the hypotheses yield a variety with eight linear components (corresponding to the different choices of signs for x, y, z) and, the thesis $x+z=y$ is true only over some of them.

Fig. 3

$AE+EB=AB$: true on parts, false on parts

Finally, as a more sophisticated example, imagine, we are dealing with some statement involving the incenter of a triangle, and we introduce its definition as the center of a circle tangent to the three sides of a triangle, we might be forgetting that we are actually considering four possible incenters (although only one of them will lie inside the given triangle), each one of them related to some irreducible component of the algebraic variety described by the hypotheses. Thus, it might happen that the considered statement holds true only for the “usual” incenter and fails on the remaining three cases.

Thus, as described rigorously in the reference [5], Sect.  3, Proposition 2 (although without explicitly providing a concrete naming for this situation), arriving to a true only on some components case means “yielding a warning sign for the need to factorize”. Luckily, such warning sign—even without actually involving algorithmic factorization, but human reflection, instead—leads to the discovery of new (surely for the user, but, sometimes, for the scientific community as well) theorems. For instance, it has already allowed one of the authors of this paper to work out some contributions, such as a converse to Varignon Theorem [2], or the generalization of the Steiner–Lehmus Theorem (cf. Example 9 in the paper [5], fully described in the reference [9]).

On the other hand, within an educational scenario, the notion of true on parts, false on parts can be particularly helpful. A student may be trying to state some conjecture and to prove it using some automated theorem prover within a dynamic geometry program. The student makes a geometric construction for the conjecture, and the program automatically (and internally) translates the construction into a collection of algebraic equations. Next, despite the apparently convincing geometric behavior of the conjecture, the student is perplexed to when the prover reports that the conjecture is not valid, and that it holds ”true on parts, false on parts”. This means the student is required to reflect more deeply in the involved algebraic-geometric dictionary issues, to understand the reasons behind the need to fix or reformulate the statement in order to be generally true.

For instance, regarding the rhombus example (see Example 3) in the last section of this paper, a student may indeed try to construct a rhombus in the given way, only to find that he/she cannot prove that its diagonals are perpendicular. Then the student may try to construct a rhombus in some other way, after reflecting about the reasons behind the apparently wrong behaviour of GeoGebra concerning this conjecture. Or: a teacher can provide one specification (a construction) of a rhombus, and ask the student to construct the rhombus ABCD, given the points A, B, C. The student provides some solution, and if it meets the teacher’s specification only ”true on parts, false on parts”, then the student knows there is something in the visually correct solution that requires further investigation on subtle algebro-geometric issues, etc. In conclusion, we think that the methodology presented in the paper clearly provides multiple learning opportunities in different scenarios like the ones we have just briefly described.

We will come back to this kind of arguments in the last section of this paper, where a general reflection on the relevance of automated reasoning tools capable of handling this subtle idea of truth (on parts!) is developed.

In summary: we think it could be quite rewarding to devote some efforts to understand better the true on parts, false on parts concept, and this is the goal of the current paper.

2 Motivation for a new framework

Some detailed, explicit examples of the true on parts, false on parts case have been already provided by one of the authors of this paper as early as 1998 in the book [10]; further examples appeared in the chapter [11] or in Sections 2.3 and 2.4. of the paper [12], reproducing in English the example, in Spanish, from the book [10]. A recent paper, specifically devoted to discuss and to present such cases is [2]. But it was not until more recently that a new terminology to describe such cases has been introduced in the reference [15], labelling as generally true on components or, simply, as true on components, those statements that are true in some, and false in some other, non-degenerate components: i.e. statements that, according to our terminology, are simultaneously true on parts, false on parts. Moreover, the reference [15] presents an algorithmic test to check this property.

Now, since the idea of true on components, or true on parts, false on parts, is based on the concepts of degeneracy and of irreducible component, it follows that both the choice of the field over which the prime decomposition is performed and the choice of the independent variables—which determine which components are to be considered as degenerate—could be essential.

Attempting to address these options, this Sect. 2 recalls some fundamental notions and argues why we have decide adopting, as our algebraic geometry framework, the consideration of statements defined over some base field K, but thinking of the associated algebraic varieties over an algebraically closed extension $K \subseteq L$. This framework, although quite classical (cf. [14]) and already quite common in the automated theorem proving context (cf. [3, 4, 12]), is more general than the one used in the paper [15]. In fact, [15] considers just one algebraically closed field, both as the base field and as field of solutions.

Moreover, we elaborate in this section a restricted—yet quite relevant—notion of non-degeneracy, by adopting always a set of independent variables of cardinal equal to the dimension of the hypotheses variety. This condition is a kind of intuitive translation of the expected fact that, for given values of the independent coordinates, the hypotheses variety contains just a finite number of configurations (as in [4], Chapter 6, Sect. 4, Definition 4; see also the Dimensionality Restriction in the book [3]; or the need, expressed in the papers [5, 12], to include the equality of the dimension and the number of free variables to obtain sound results). Again, by adopting this convention we differ from the approach in the paper [15].

Fig. 4

Another simple example

Let us first start analyzing a simple example, a modified version of the example in Sect. 3 from the reference [2]. In what follows, we identify polynomials p and polynomial equations $p=0$, as it is quite a standard “abuse of notation” in some well-spread computer algebra programs. Consider points A(0, 0), B(2, 0) in the plane and construct circles $c= (x-0)^2+(y-0)^2-3$ and $d=(x-2)^2+(y-0)^2-3$, i.e. circle c is centered at A and circle d is centered at B and both have the same radius r, where $r=\sqrt{3}$. Finally, we consider the two points of intersection of these circles, namely, E(u, v) and F(m, n) (see (Fig. 4)), so the hypotheses are

$$\begin{aligned}&(u-0)^2+(v-0)^2-3,(u-2)^2+(v-0)^2-3,\\&(m-0)^2+(n-0)^2-3, (m-2)^2+(n-0)^2-3. \end{aligned}$$

Notice that either $E=F$ or $E\ne F$ and then both points are symmetric with respect to the $X-$ axis. Finally, the thesis states the parallelism of the lines AE and BF, that is, the vanishing of the polynomial

$$\begin{aligned} (u-0)\cdot (n-0)-(v-0)\cdot (m-2). \end{aligned}$$

The ideal of hypotheses is clearly zero-dimensional, so there are no independent variables, nor degenerate components. Its primary components, over the rationals, are

$$\begin{aligned}&\langle v-n, (m-2)^2+n^2-3, (u-2)^2+v^2-3, m^2+n^2-3, u^2+v^2-3\rangle , \\&\langle v+n, (m-2)^2+n^2-3, (u-2)^2+v^2-3, m^2+n^2-3, u^2+v^2-3\rangle \end{aligned}$$

and it easy to check that the thesis is false over the first one and true over the second. This a clear, simple example of a true on components statement, arising in an elementary geometry context.

Even considering this is a very basic example of a true on parts, false on parts statement, it already allows us to emphasize different issues that motivate our choices in this paper.

First of all, it highlights the relevant role of the base field (the field of coefficients where the hypotheses and thesis equations are described, i.e. $\mathbb {Q}$, in this example). It is obvious that if we would have chosen instead, as base field, $\mathbb {Q}(\sqrt{2})$, the hypotheses ideal could have been the following precise description of the two constructed points E and F, $\left\langle u-1,v-\sqrt{2},m-1,n+\sqrt{2}\right\rangle$, clearly verifying the thesis $u\cdot n-v\cdot (m-2)$. The statement would have been a true one, then.

Moreover, even if keeping the original hypotheses ideal, it is clear that its primary decomposition depends on the coefficients field for the ring where the components are computed. A trivial example is the ideal $\left\langle x^2-2\right\rangle$, that is irreducible over $\mathbb {Q}[x]$, but has two components $\left\langle x-\sqrt{2}\right\rangle$ and $\left\langle x+\sqrt{2}\right\rangle$ over $\mathbb {Q}(\sqrt{2})[x]$. Likewise, the hypotheses ideal

$$\begin{aligned}&\left\langle (u-0)^2+(v-0)^2-3,(u-2)^2+(v-0)^2-3,\right. \\&\left. (m-0)^2+(n-0)^2-3, (m-2)^2+(n-0)^2-3\right\rangle \end{aligned}$$

has two components over $\mathbb {Q}[u,v,m,n]$, but four over $\mathbb {Q}(\sqrt{2})[u,v,m,n]$, namely,

$$\begin{aligned} \left\langle n -\alpha , v -\alpha , (m-2)^2+n^2-3, (u-2)^2+v^2-3, m^2+n^2-3, u^2+v^2-3)\right\rangle , \end{aligned}$$

considering all possible sign values for $\alpha =\sqrt{2}$. Notice that, as over $\mathbb {Q}$, the statement would also remain true on parts, false on parts over $\mathbb {Q}(\sqrt{2})$, because here the thesis would be false over two components and true over the other two.

Obviously, the idea of accepting, as input, polynomials over field extensions of the rationals, could avoid some—but not all—true on parts, false on parts cases, by allowing the user to be more specific regarding the hypotheses data, but it also implies the symbolic manipulation of quite complicated expressions and it is, in practice, not realistic.

These considerations are behind our generalized approach to the true on parts, false on parts concept, as developed in the next section, and to the extension of the Zhou–Wang–Sun test [15] to this framework, see Theorem 3.

On the other hand, the above example does not requires any discussion about the idea of degenerate components, since this concept is linked to the idea of independent parameters for our hypotheses set, and there are none in this example, as the dimension of the hypotheses variety is zero. So here all components can be thought as non-degenerate. But, in general, it is well known, since long ago, that the precise choice of a meaningful set of independent parameters and, correspondingly, the notion of degenerate components, is an involved issue. And, since the definition of true on parts, false on parts involves the truth and falsity of a statement over some non-degenerate components, both the idea of independence of parameters and of degeneracy are concepts that can not be avoided in this context.

Let us recall (cf. [4], particularly Chapter 9, Section 5, for precise definitions and basic results) that a collection of variables is considered to be independent over the hypotheses ideal if there is no polynomial in these variables alone belonging to the ideal; and that a component is labeled as degenerate if over the component the chosen independent variables verify some non-trivial relation. This notion intends to reflect the idea of free variables for our geometric statement; moreover, it is related to the concept of Hilbert Dimension (i.e. the dimension, also known as the Krull dimension) of the ideal, since this dimension coincides with the largest cardinal of a set of free variables modulo the given ideal (but notice that not every set of free variables can be enlarged to one with maximum cardinality).

There are, in general, many possible sets of independent variables for the ideal H, even concerning maximal sets of independent variables or even considering maximum-size maximal sets. For example, if $H=\left\langle x\cdot y\right\rangle$, both $\{x\}$ and $\{y\}$ are maximal and maximum-size sets of independent variables; and, if $H=\left\langle x\cdot y, ~ x\cdot z\right\rangle$, then both $\{x\}$ and $\{y, z\}$ are maximal sets of independent variables, but only the second has cardinality equal to the dimension of H.

When dealing with geometric statements, it seems logical to take as independent variables the coordinates of free points in the geometric construction we are dealing with. In most cases this “intuitively” maximal set of independent variables is maximum-size, but there are examples in which the coordinates of free points in the geometric construction do not provide a maximum-size set of independent variables. See, for instance, Example 2 in the reference [12, p. 72]: the number of coordinates of free points in the chosen geometric construction is 5, but the Hilbert dimension of H is 6.

Another typical example of the difficulties involved in handling this concept is Example 7 in the reference [5], concerning Euler’s formula regarding the radii of the inner and outer circles of a triangle with vertices $(-1,0),(1,0), (u[1],u[2])$. Here the dimension of the hypotheses variety is expected to be 2 (referring to the two coordinates of the only free vertex of the triangle), but applying the algebraic definition it turns out to be three..., unless it is explicitly required, as new hypothesis, that (u[1], u[2]) does not lie in the x-axis! This quite common problem—related, as mentioned above, to the difficult a priori control and detail of all geometric degeneracies—is already considered in the basic reference [3].

Despite of these difficulties, we think—as argued and documented in the introduction—that the closest choice reflecting, in most cases, human intuition, is that of considering a maximum-size set of independent variables as the one best related to the notion of true on parts, false on parts. The precise definition will be developed in the next Section. But we are aware that the idea of true on parts, false on parts depends on the adopted formulation of non-degeneracy in each particular case and, therefore, on the selected set of free variables for the given statement. In the following Sect. 2 we will show some precise statements and counterexamples concerning the consequences of this choice.

As a toy example, consider the following (artificial) statement: take as hypothesis set the union of the two axes in the plane, i.e. the set of points verifying $xy=0$. Its dimension is one, so we might consider that the geometry of the problem involved in this formulation requires just one free variable, say, x and, thus, we could label the x-axis as the only non-degenerate component in this problem. So, if the thesis is $y=0$, we could conclude that it is generally true, since it holds over the x-axis. But if we consider, instead, as the only non-degenerate component, the y-axis, then $y=0$ would be generally false. And if we choose to consider both x, y as two non-degenerate parameters simultaneously ruling our construction, then the thesis $y=0$ will be true on components, since it will hold on the x-axis and will be false on the y-axis.

3 Statements true on parts, false on parts

In this section we start (Sect. 3.1) detailing the specific algebro-geometric framework for our concept of true on parts, false on parts. Then, Theorem 1 of Sect. 3.2 provides a new, simpler way, of testing if a statement is true and false on parts, by just detecting if a pair of elimination ideals are zero or not. As a consequence, it is shown the somehow surprising result (cf. Corollary 1) that the notion of true on parts, false on parts does not depend on the base field being considered. Moreover, Sect. 3.2 includes an extension to our more general framework of the main result of the reference [15], by providing a direct proof (cf. Theorem 3) of the equivalence (for degenerate components of the special kind) of our test (cf. Theorem 1) and that of the paper [15], here labeled as Theorem 2. Subsection 3.3 provides some counterexamples to this equivalence (Examples 1, 2) if the mentioned degeneracy concept is not fulfilled; and shows how these examples help to explain some discrepancy, mentioned at the paper [15], with a previous result of [7].

3.1 Framework and main criterion

As above, let us consider an algebraically translated statement $\{H \Rightarrow T\}$, where H stands for the equations describing the geometric construction of the hypotheses and T describes the thesis. By abuse of notation, we will denote also by H and T the ideals generated by the polynomials involved in the equations describing the statement. In what follows we will suppose that $H=\left\langle h_1, \dots , h_r\right\rangle$ and $T=\left\langle f\right\rangle$ are the hypotheses and thesis ideals in a polynomial ring K[X], $X=\{x_{1}, \dots , x_{n}\}$, where the variables $X=\{x_{1}, \dots , x_{n}\}$ refer to the coordinates involved in the algebraic description of the hypotheses, over a base field K.

We will deal with another field L, an algebraically closed extension on K (for instance $L={{\mathbb {C}}}$ for $K={{\mathbb {Q}}}$), and the geometric instances verifying the hypotheses (respectively, the thesis) of the statement will be considered as the algebraic variety V(H) (respectively, V(T)) in the affine space $L^n$. Therefore, V(H) and V(T) are algebraic varieties of $L^n$, but defined over K. Thus, we are working here with two different fields: the one of coefficients for the algebraic description of the geometric setting and the one where the solutions of the equations are to be considered at. In fact, most elementary geometry constructions can be translated into algebraic equations with rational coefficients, while the algorithms we will consider (for its higher performance) to work with these equations are those of algebraic geometry over an algebraically closed field (i.e not over the rationals or over the reals).

In general we will suppose that $Y=\{x_{1}, \dots , x_{d}\}$ ($0\le d\le n$) is a maximum-size set of independent variables for the hypotheses ideal H, that is

• (i) $H\cap K[Y]=\left\langle 0\right\rangle$, and

• (ii) for any other set of variables $Z\subset X$ with $r>d$ elements, $H\cap K[Z]\ne \left\langle 0\right\rangle$.

Consequently, the Hilbert dimension of the hypothesis variety V(H) must be d.

Following the notation above we recall the following definitions which are usual in the literature about the algebraic geometry approach to automated reasoning in geometry [12].

Definition 1

Let $\{H \Rightarrow T\}$ be a geometric statement and fix a set $Y=\{x_{1}, \dots , x_{d}\}$ of independent variables for the hypotheses ideal H.

• The statement is generally true if the thesis f vanishes on all non-degenerate K-components of the hypotheses variety V(H).

• The statement is generally false if the thesis f vanishes on none of the non-degenerate K-components of the hypotheses variety V(H).

The related concept of “generally true on components” statements was introduced by Zhou, Wang and Sun in the paper [15] but in a slightly different, less general, context, assuming $K=L$, algebraically closed. Here we mimic this idea over our more general framework, as follows:

Definition 2

Let $\{H \Rightarrow T\}$ be a geometric statement formulated over K. The statement is labelled as true on parts, false on parts if the thesis f vanishes on some but not all non-degenerate K-components of the hypotheses variety V(H) in $L^n$. That is, if it is neither generally true nor generally false.

In the reference [12] the reader can find algorithmic criteria for the generally true and the generally false cases, by means of some elimination ideals with respect to independent variables of the free points coordinates. Moreover, in this reference it is shown how to derive, from these elimination ideals, some conditions to discover new theorems. This approach has been implemented in the widely disseminated dynamic geometry software GeoGebra [1, 6].

Here we apply these criteria to our “true on parts, false on parts” context, as follows:

Theorem 1

Let $\{H \Rightarrow T\}$ be a geometric statement and fix a maximum-size set $Y=\{x_{1}, \dots , x_{d}\}$ of independent variables for the hypotheses ideal H (i.e. $d=\dim (H)$).

• (a) The statement $\{H \Rightarrow T\}$ is generally true if and only if

  $$\begin{aligned} \left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[X,t]\cap K[Y]\ne \left\langle 0\right\rangle . \end{aligned}$$

• (b) The statement $\{H \Rightarrow T\}$ is generally false if and only if

  $$\begin{aligned} \left\langle h_1,\dots , h_r,f\right\rangle K[X]\cap K[Y]\ne \left\langle 0\right\rangle . \end{aligned}$$

Proof

The proof of (a) is quite straightforward. In fact, the ideal

$$\begin{aligned} \left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[X,t]\cap K[X] \end{aligned}$$

is usually named, in commutative algebra, as the saturation of H by f and it is well known (cf. [5], Appendix, in particular, Remark 5) that it represents the intersection of the primary components of H such that the associated primes do not contain f, i.e. such that the thesis does not hold over the corresponding irreducible component. It follows that if the intersection of this saturation with K[Y] contains a non-zero polynomial $g\in K[Y]$, then all such “failure” components must be degenerate, as they all contain g, a polynomial in the independent variables.

And, conversely, if all the prime ideals associated to the primary ideals in the saturation are degenerate, there is a non-zero polynomial $g\in K[Y]$ in each of them and, then, a power of g must be in the corresponding primary component. Thus, the product of all of these g’s is in the intersection of the primary ideals, so in the saturation, yielding

$$\begin{aligned} \left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[X,t]\cap K[Y]\ne \left\langle 0\right\rangle . \end{aligned}$$

Notice this statement is true even if the independent variables set Y is not of maximum-size.

Now, we are going to make a detailed demonstration of (b), since in the reference [12] it is just sketched as a footnote. For the “if” part of (b), suppose there is a non-zero $g\in \left\langle h_1,\dots , h_r,f\right\rangle K[X]\cap K[Y]$. Then $g=g_1 h_1+\cdots +g_r h_r+ g_{r+1} f$ for some $g_i\in K[X]$. Let W be a non-degenerate component of V(H). Then, g cannot vanish on W, because $I(W)\cap K[Y]=\left\langle 0\right\rangle$. As $h_i$ vanishes on W for all $i=1,\dots , r$, we have that f must not vanish on all W. Notice that for this part of the proof we have not used that Y is maximum-size.

For the proof of the “only if” of (b) we have to assume that $Y=\{x_{1}, \dots , x_{d}\}$ ($0< d\le n$) is a maximum-size set of independent variables for the hypotheses ideal H. Suppose that f vanishes on none of the non-degenerate components of V(H).

Take any non-degenerate component W of V(H) and let $\mathfrak {p}\subset K[X]$ be its associated prime ideal. Then, $\mathfrak {p}\cap K[Y]=\left\langle 0\right\rangle$. As f does not vanish identically on W, $\mathfrak {p}+\left\langle f\right\rangle \supsetneq \mathfrak {p}$ and $\mathfrak {p}+\left\langle f\right\rangle$ has dimension less than d, by our maximum-size of Y hypothesis. Then $\{x_{1}, \dots , x_{d}\}$ cannot be independent for $\mathfrak {p}+\left\langle f\right\rangle$. Therefore, there is a non-zero $g_W\in ( \mathfrak {p}+\left\langle f\right\rangle ) \cap K[Y]$ for each non-degenerate component W of V(H), vanishing over the intersection of this component and the thesis. For each degenerate component U of V(H) take now a polynomial $g_U\in I(U)\cap K[Y]$.

Let g be the product of all $g_W$ and all $g_U$. Then this product vanishes over all the points of V(H) where the thesis holds, because it vanishes both over all degenerate components and over the zeroes of f in the non-degenerate components. Thus $g\in \sqrt{\left\langle h_1,\dots , h_r,f\right\rangle }K[X]\cap K[Y]$ and therefore $\left\langle h_1,\dots , h_r,f\right\rangle K[X]\in K[Y]\ne \left\langle 0\right\rangle$. $\square$

Obviously, Theorem 1 provides a straightforward test for detecting if a statement is true and false on components, by simply checking if the result of performing two eliminations is zero in both cases or not. Moreover, several algorithms for elimination over algebraically closed fields, interpreted through a Gröbner basis computation, are already implemented in different computer algebra systems—including Giac, the one currently embedded in the dynamic mathematics program GeoGebra—and work satisfactorily for our purposes.

This criterion is also useful to understand an apparently contradictory fact, since we have previously emphasized the base field dependence of the primary decomposition of an ideal:

Corollary 1

Suppose that we consider some intermediate base field extension $K\subseteq K^{\prime }\subseteq L$, where L is algebraically closed. Now, although $\{H \Rightarrow T\}$ is defined over K, consider this statement as well as defined over $K^{\prime }$. Then we claim that being true on parts, false on parts over K is equivalent to being true on parts, false on parts over $K^{\prime }$, that is, the notion of true on parts, false on parts does not depend on the base field extension.

Proof

Deciding if some elimination ideal is zero or not can be achieved by computing a Gröbner basis under a certain ordering and checking if there are some elements in the basis that involve just the non-eliminated variables. But Gröbner basis computations are performed over the base field, and, thus, are independent of the field extension (i.e. it will yield the same result over K or over $K^{\prime }$). $\square$

What this result means is that, if both hypotheses and the thesis are defined over a common base field K, then the existence of some component where the thesis vanishes or where it does not vanish is independent of the choice of any field extension of K as a new base field; we can have more components over K where T vanishes, and a few less over $K^{\prime }$, and the same can happen for components where T does not vanish; but their existence over K is equivalent to their existence over $K^{\prime }$.

3.2 The Zhou-Wang-Sun framework and criterion. An equivalence result

It could seem that, since we are concluding that the field extension is not relevant in this context, the above remark directly implies that our framework is equivalent to that of the paper [15], in which it was supposed that $K=L$, algebraically closed. But things are quite subtle here. In fact, Theorem 3.1 in [15] gives a necessary and sufficient condition for a geometric statement to be generally true on components over $K=L$, but without assuming maximum-size for the set of independent variables $Y=\{x_1,\dots , x_d\}$, as we did in our Theorem 1. In what follows we will confirm that this fact is important, see Example 2, but that, otherwise, the result of the reference [15] also holds in our framework.

In order to prove this, let all the notations be the same as above. In particular, let $X=\{x_1,\dots , x_n\}$ be the set of variables representing the point coordinates involved in the algebraic description of the hypotheses ideal, suppose that $Y=\{x_1,\dots , x_d\}$ ($d\le n$) is a subset of independent variables for H, but not necessarily maximum-size, and denote by $Z=\{x_{d+1},\dots , x_n\}$ the rest of the variables. Then, we have:

Theorem 2

(Theorem 3.1 [15]) Let $L=K$ be an algebraically closed field and let $H^{\prime }=\left\langle h_1,\dots ,h_r\right\rangle K(Y)[Z]$ be the extension of H to K(Y)[Z]. Then the geometric statement $\{H\Rightarrow T\}$ is generally true on components (i.e. true on parts, false on parts) if and only if f is a non-zero zero divisor in $K(Y)[Z]/\sqrt{H^{\prime }}$.

Next we give a direct proof of the equivalence, in some specific context, between Theorems 1 and 2 ccharacterizing conditions for being generally true on components. This is achieved in a purely algebraic fashion and under some additional restrictions: namely, when considering a field K and an algebraically closed extension L and assuming that Y is a maximum-size set of independent variables.

Theorem 3

Let $\{H \Rightarrow T\}$ be a geometric statement as above and fix a maximum-size set $Y=\{x_{1}, \dots , x_{d}\}$ of independent variables for the hypotheses ideal H (i.e. $d=\dim (H)$) and let $Z=\{x_{d+1},\dots , x_n\}$ be the rest of the variables. Then,

$$\begin{aligned} \left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[X,t]\cap K[Y]=\left\langle 0\right\rangle \text { and } \left\langle h_1,\dots , h_r,f\right\rangle K[X]\cap K[Y]=\left\langle 0\right\rangle \end{aligned}$$

if and only if

$$\begin{aligned} f \text { is a non-zero zero divisor in } K(Y)[Z]/\sqrt{H^{\prime }} \text { where } H^{\prime }=\left\langle h_1,\dots ,h_r\right\rangle K(Y)[Z]. \end{aligned}$$

We need some lemmas for the proof of this theorem. For the lemmas below we assume the previous notations and the hypotheses of Theorem 3.

Lemma 1

Let $H^{\prime }$ be the extension of the hypotheses ideal H to K(Y)[Z].

• (a) The ring $K(Y)[Z]/\sqrt{H^{\prime }}$ is not zero.

• (b) $\dim _{K(Y)}(K(Y)[Z]/\sqrt{H^{\prime }})=0$.

Proof

• (a) The condition that Y is independent for H in K[Y, Z] is equivalent to say that $H^{\prime }$ is not all K(Y)[Z] (i.e. $1 \notin H^{\prime }$ and, equivalently, $1 \notin \sqrt{H^{\prime }}$)). So, the ring $K(Y)[Z]/\sqrt{H^{\prime }}$ is not zero.

• (b) Notice that the ideal H has dimension d in K[Y, Z] and Y is a set of d independent variables for H and for $\sqrt{H}$.

  For each variable $z \in Z$, we have that the variables in the set $\{Y,z\}$ are not independent for H. Then, there is a non-zero polynomial $g(Y,z)\in H\cap K[Y,z]$.

  Since $H \subset HK(Y)[Z]=H^{\prime }\subset \sqrt{H^{\prime }}$, for all $z\in Z$ there is a non-zero polynomial $g(Y,z)\in \sqrt{H^{\prime }}K(Y)[Z]\cap K(Y)[z]$ and then $\dim _{K(Y)}(K(Y)[Z]/\sqrt{H}) =0$.

$\square$

As a consequence of previous lemma we have the following corollary.

Corollary 2

Let f be a polynomial in K[Y, Z]. If $f\notin \sqrt{H^{\prime }}$, then there is a polynomial $p(t)\in K(Y)[t]$ such that $p(f)\in \sqrt{H^{\prime }}$.

Proof

Consider the primary decomposition of $\sqrt{H^{\prime }}$ in the ring K(Y)[Z]. For each associated prime $\mathfrak {p}$ of $\sqrt{H^{\prime }}$, the field of fractions of $K(Y)[Z]/\mathfrak {p}$ will be an algebraic extension of K(Y), because $K(Y)[Z]/\mathfrak {p}$ has dimension 0 over K(Y) (by the previous lemma). Thus, for each prime ideal $\mathfrak {p}$ associated to $\sqrt{H^{\prime }}$, there is a polynomial $p_{\mathfrak {p}}(t)\in K(Y)[t]$ such that $p_{\mathfrak {p}}(f)\in \mathfrak {p}$.

Take then $p(t)=\prod _{\mathfrak {p}} p_{\mathfrak {p}}(t)\in K(Y)[t]$. Then, $p(f)\in \cap \mathfrak {p}=\sqrt{H^{\prime }}$. $\square$

Lemma 2

$f\in \sqrt{H^{\prime }}$ if and only if $\left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[Y,Z,t]\cap K[Y]\ne \left\langle 0\right\rangle$

Proof

$f\in \sqrt{H^{\prime }}$ means that there is a positive integer m such that $f^m=\sum _{i=1}^r k_i^{\prime } h_i$ with $k_i^{\prime }\in K(Y)[Z]$. Equivalently, by clearing denominators, there is a positive integer m such that $g f^m=\sum _{i=1}^r k_i h_i$ where $g\in K[Y]$ and $k_i\in K[Y,Z]$ (i.e., $g f^m\in H$). That is, $g\in (H:f^\infty )\cap K[Y]$ where $(H:f^\infty )$ is the saturation of the ideal H by f.

But $(H:f^\infty )=\left\langle h_1,\dots , h_r,f\cdot t-1\right\rangle K[Y,Z,t]\cap K[Y,Z]$ (cf. [5], Appendix, Proposition 6), then $\left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[Y,Z,t]\cap K[Y]\ne \left\langle 0\right\rangle$. $\square$

Let us prove Theorem 3.

Proof

To prove the “if” part, let assume that f is a non-zero zero divisor in $K(Y)[Z]/\sqrt{H^{\prime }}$. As f is non-zero in $K(Y)[Z]/\sqrt{H^{\prime }}$, $f\notin \sqrt{H^{\prime }}$. Then, by Lemma 2, we have that

$$\begin{aligned} \left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[Y,Z,t]\cap K[Y]=\left\langle 0\right\rangle . \end{aligned}$$

Suppose also that $\left\langle h_1,\dots , h_r, f\right\rangle K[Y,Z]\cap K[Y]\ne \left\langle 0\right\rangle$, then $(\sqrt{H}+\left\langle f\right\rangle )K[Y,Z] \cap K[Y]\ne \left\langle 0\right\rangle$. Therefore, there is a polynomial $g\in K[Y]$, such that $g=k+qf$ with $k\in \sqrt{H}$ and $q\in K[Y,Z]$. Dividing by g we obtain

$$\begin{aligned} 1=\frac{k}{g}+\frac{q}{g}f \end{aligned}$$

and notice that $\frac{k}{g}\in \sqrt{H^{\prime }}K(Y)[Z]$ and $\frac{q}{g}\in K(Y)[Z]$. So, f is a unit in $K(Y)[Z]/\sqrt{H^{\prime }}$. Then, f cannot be a zero divisor in $K(Y)[Z]/\sqrt{H^{\prime }}$.

Now let us prove the “only if” part. Assume that

$$\begin{aligned}&\left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[Y,Z,t]\cap K[Y]=\left\langle 0\right\rangle \text { and }\\&\qquad \left\langle h_1,\dots , h_r, f\right\rangle K[Y,Z]\cap K[Y]=\left\langle 0\right\rangle . \end{aligned}$$

Then, by Lemma 2, $f\notin \sqrt{H^{\prime }}$ and, by Corollary 2, there is a polynomial $p(t)\in K(Y)[t]$ such that $p(f)\in \sqrt{H^{\prime }}$.

Take a polynomial $p^{\prime }\in K(Y)[t]$ of minimum degree in t with this property. Then we have two cases:

• (i) $p^{\prime }$ has an independent term in K(Y): as $p^{\prime }(f) \in \sqrt{H^{\prime }}$, take a convenient power of $p^{\prime }(f)$ and clearing denominators, we will obtain an independent term in K[Y] that will be a combination of $h_1,\dots ,h_r$ and f. Thus, $\left\langle h_1,\dots , h_r, f\right\rangle K[Y,Z]\cap K[Y]\ne \left\langle 0\right\rangle$, in contradiction with one of our hypotheses.

• (ii) $p^{\prime }$ does not have an independent term: we can take f as a common factor in $p^{\prime }(f) \in \sqrt{H^{\prime }}$, yielding $p^{\prime }(f)=f\cdot q(f) \in \sqrt{H^{\prime }}$. Moreover, q(f) cannot be in $\sqrt{H^{\prime }}$, because it has a lower degree than $p^{\prime }(t)$. Thus we will have $f\cdot q(f)=0$ in $K(Y)[X]/\sqrt{H^{\prime }}$ and q(f) non-zero in $K(Y)[X]/\sqrt{H^{\prime }}$. Therefore, f is a zero divisor in $K(Y)[X]/\sqrt{H^{\prime }}$.

$\square$

3.3 Some examples with both criteria

We have proved that the tests in the references [12, 15] for being true on components are equivalent, even in our generalized context, although requiring a maximum-size set of independent variables. Consequently, we have now a new algorithm (based on the direct application of Theorem 1) to check if a geometric statement is true on components, by merely using elimination in polynomial ideals, in contrast with the one presented in the paper [15] that requires computing a Gröbner basis over a field of fractions, and checking if f is a zero divisor of the radical of some ideal in a extended ring.

To illustrate this new test, we have chosen Example 3.8 in [15], where truth on components is checked by the zero divisor test. We apply here our test using the computer algebra system Maple 2017.0, although it can be computed in whatever system doing elimination in polynomial ideals. The computations have been performed in a few seconds.

Example 1

Let ABC be a triangle with A(0, 0), B(1, 0) and $C(u_1,u_2)$, and let $A_1BC$, $AB_1C$ and $ABC_1$ be three equilateral triangles erected on the three sides of ABC. Then, the goal is to check if the segments $B_1C_1$ and $A_1C$ have the same length, that is, $|B_1C_1|=|A_1C|$.

Taking coordinates $A_1=(x_1,x_2)$, $B_1=(x_3,x_4)$ and $C_1=(x_5,x_6)$, the hypotheses ideal is given by the following polynomials describing the equalities between the sides of the three equilateral triangles:

$$\begin{aligned} \begin{array}{ll} |AC_1|=|AB|: \;\; &{} h_1= x_5^2+x_6^2-1 \\ |BC_1|=|AB|: \;\; &{} h_2= (x_5 - 1)^2 + x_6^2- 1 \\ |CA_1|=|BC|: \;\; &{} h_3= (x_1 - u_1)^2 + (x_2 - u_2)^2 - (u_1 - 1)^2 - u_2^2 \\ |BA_1|=|BC|: \;\; &{} h_4= (x_1 - 1)^2 + x_2^2- (u_1 - 1)^2 - u_2^2 \\ |AB_1|=|AC|: \;\; &{} h_5= (x_3^2+ x_4^2) - (u_1^2+u_2^2) \\ |CB_1|=|AC|: \;\; &{} h_6= (x_3 - u_1)^2 + (x_4 - u_2)^2 - (u_1^2+ u_2^2). \end{array} \end{aligned}$$

And the thesis $|B_1C_1|=|A_1C|$ is given by the polynomial

$$\begin{aligned} f:=(x_5 - x_3)^2 + (x_6 - x_4)^2 - (x_1 - u_1)^2 - (x_2 - u_2)^2. \end{aligned}$$

The set of variables $X=\{u_1,u_2,x_1,x_2,x_3,x_4,x_5,x_6\}$ has 8 elements. By the geometric construction, the variables $\{u_1,u_2\}$ can be considered as the free variables in the hypotheses ideal H. In fact, one can check that they are even a maximum-size set of independent variables for H. In Maple, after using the package PolynomialIdeals and defining the ideal

$$\begin{aligned}&H:=\left\langle x_5^2+x_6^2-1,(x_5 - 1)^2 + x_6^2- 1,\right. \\&{(x_1 - u_1)^2 + (x_2 - u_2)^2 - (u_1 - 1)^2 - u_2^2,(x_1 - 1)^2 + x_2^2- (u_1 - 1)^2 - u_2^2},\\&{\left. (x_3^2+ x_4^2) - (u_1^2+u_2^2), (x_3 - u_1)^2 + (x_4 - u_2)^2 - (u_1^2+ u_2^2)\right\rangle }, \end{aligned}$$

we compute its Hilbert dimension (by using the command HilbertDimension(H)), yielding that it is 2 and (with the help of command MaximalIndependentSet(H)) that $\{u_1,u_2\}$ is, as expected, a maximum-size set of independent variables.

Then, we check if the statement is true on parts, false on parts, by eliminating all variables except $\{u_1,u_2\}$ in the ideals $\left\langle h_1,\dots ,h_6, f\cdot t-1\right\rangle$ and $\left\langle h_1,\dots ,h_6, f\right\rangle$.

$$\begin{aligned} \begin{array}{l} {\texttt {EliminationIdeal}\left( \left\langle x_5^2+x_6^2-1,(x_5 - 1)^2 + x_6^2- 1,\right. \right. } \\ {(x_1 - u_1)^2 + (x_2 - u_2)^2 - (u_1 - 1)^2 - u_2^2,(x_1 - 1)^2 + x_2^2- (u_1 - 1)^2 - u_2^2,}\\ {(x_3^2+ x_4^2) - (u_1^2+u_2^2), (x_3 - u_1)^2 + (x_4 - u_2)^2 - (u_1^2+ u_2^2),}\\ {\left. \left. ((x_5 - x_3)^2 + (x_6 - x_4)^2 - (x_1 - u_1)^2 - (x_2 - u_2)^2)\cdot t-1\right\rangle ,\{u_1, u_2\}\right) \!;}\\ { \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \left\langle 0\right\rangle }\\ {\texttt {EliminationIdeal}\left( \left\langle x_5^2+x_6^2-1,(x_5 - 1)^2 + x_6^2- 1,\right. \right. }\\ {(x_1 - u_1)^2 + (x_2 - u_2)^2 - (u_1 - 1)^2 - u_2^2,(x_1 - 1)^2 + x_2^2- (u_1 - 1)^2 - u_2^2,}\\ {(x_3^2+ x_4^2) - (u_1^2+u_2^2), (x_3 - u_1)^2 + (x_4 - u_2)^2 - (u_1^2+ u_2^2),}\\ {\left. \left. (x_5 - x_3)^2 + (x_6 - x_4)^2 - (x_1 - u_1)^2 - (x_2 - u_2)^2)\right\rangle ,\{u_1, u_2\}\right) \!;}\\ { \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \left\langle 0\right\rangle } \end{array} \end{aligned}$$

We obtain that both eliminations give the $\left\langle 0\right\rangle$ ideal, and we conclude, by the elimination test, that this statement is true and false on certain components, i.e. true on parts, false on parts. Intuitively, this fact is due to the different possible ways of building an equilateral triangle on the (two) sides of a given triangle (Fig. 5). And the statement is true only for some of these choices.

Fig. 5

Two different choices of building an equilateral triangle $A_1BC$ on the side BC

We would like to point out that in Example 3.8 of [15], reproduced above, the authors also consider $\{u_1,u_2\}$ as the set of choice for independent variables, which is, as previously remarked, a maximum-size set of independent variables. The following example shows that the elimination test we have presented and the zero divisor test of [15] do not agree if the number of independent variables is not maximum-size. Moreover, it explains also some pretended error detected by the authors in [15], Remark 3.6, concerning a discrepancy with the reference [7].

Example 2

Consider $H=\left\langle xy,x^2\right\rangle$ and $f=y$ in K[x, y, z]. The ideal $\left\langle xy,x^2\right\rangle K[x,y,z]$ has dimension 2 and $\{y,z\}$ is a maximum-size set of independent variables. Take, instead, $Y=\{z\}$, which is a set of independent variables, but not maximum-size. Then,

$$\begin{aligned} \left\langle xy,x^2,y\cdot t-1\right\rangle K[x,y,z,t]\cap K[z]=\left\langle 0\right\rangle \; \mathrm { and }\; \left\langle xy,x^2,y\right\rangle K[x,y,z]\cap K[z]=\left\langle 0\right\rangle . \end{aligned}$$

So if we apply the test [12] in this specific situation in which one does not consider all possible independent variables, the statement seems to be true on parts, false on parts (i.e. true on components).

But on the other hand, y is not a zero divisor in $K(z)[x,y]/\sqrt{\left\langle xy,x^2\right\rangle }$. In fact, $\sqrt{\left\langle xy,x^2\right\rangle }=(x)$, so $K(z)[x,y]/\sqrt{\left\langle xy,x^2\right\rangle }= K(z)[x,y]/(x)= K(z)[y]$ which is a domain of integrity and it does not contain zero divisors. Therefore, the statement is not true on components, according to the test [15]. Actually the statement is generally false, because y is not zero over the plane $\{x=0\}$.

Remark 1

Just by following the proof of Theorem 1, it is easy to conclude that, without any maximum-size restriction for the independent variables, it holds that to be true on components (and, thus, verifying the criteria of Theorem 2) implies the two conditions stated in Theorem 1, but not conversely, as the above example shows. So, without the maximum-size restriction, our test is just a necessary condition for a true on components situation, not a sufficient one (but it becomes sufficient for sets of independent variables of maximum-size).

4 Implementation in GeoGebra

Finally, this Sect. 4 shows some examples on how to actually deal with the concept of true on parts, false on parts, by performing our test as implemented in the dynamic geometry software GeoGebra, which deals with the concept of true on parts, false on parts since version 5.0.443.0 (10 March 2018). Thus, statements which were formerly classified as not generally true and, therefore, simply considered as false by GeoGebra, are now subject to a finer classification (for instance, some of them can now be classified as true on parts, false on parts) yielding a more accurate information to the user.

The implementation in GeoGebra of this new feature follows Theorem 1 by computing both eliminations and deciding if the “intuitively”¹ full set of independent variables is actually maximum-size, by determining the Hilbert dimension of the hypotheses ideal.² We outline the steps of this algorithm to decide the truth/falsity of a statement $\{H \Rightarrow T\}$:

• 1. First select, through the coordinates of the free points of the configuration and following the construction steps performed by the user when drawing the figure that illustrates the given statement, a set Y of independent variables. Check if they are actually algebraically independent, $H\cap K[Y]=\left\langle 0\right\rangle$.

• 2. Verify if the Hilbert’s dimension of H agrees with the cardinality of Y. If this is not the case, the user is advised to check for degenerations in the construction (END). Otherwise, continue.

• 3. Compute $\left\langle h_1,\dots , h_r, f\cdot t-1\right\rangle K[X,t]\cap K[Y]$. If it is $\ne \left\langle 0\right\rangle$, the statement is generally true (END). Otherwise, continue.

• 4. Compute $\left\langle h_1,\dots , h_r, f\right\rangle K[X]\cap K[Y]$. If it is $\ne \left\langle 0\right\rangle$, the statement is generally false (END).

• 5. Otherwise, the statement is true on parts, false on parts.

Example 3

Assume two points A and B are given. A rhombus ABDC is to be constructed, as displayed in Fig. 6, by allowing point C to be freely chosen under the restriction that the segments $AB(=m)$ and $AC(=g)$ are equal. That is, C is a circumpoint of the circle with center A and radius m, and D is an intersection of a circle c with center C and radius m, and a line h through C and parallel to m.

Fig. 6

Constructing a rhombus (an example provided by Andreas Lindner)

Now we consider the well-known statement that the diagonals of a rhombus are perpendicular, but this fact (namely, $k\perp l$) can only be observed on the component of the hypotheses variety that contains D. For the other component, where $D^{\prime }$ lies (which is the other intersection point of circle c and line h), the fact $k\parallel l$ can be detected.

To support the first glance, GeoGebra provides a numerical way to verify whether the perpendicular property is true. When comparing objects k and l by using the Relation tool in GeoGebra, after a numerical overview (Fig. 7) a symbolic proof (Fig. 8) can be achieved yielding that the statement is “true on parts, false on parts”. (The algebraic details of the proof are not visible for the user, to avoid confusion.) This kind of result can also be automatically obtained by using GeoGebra’s low-level ProveDetails[$k\perp l$] command—and also for the parallelism, the ProveDetails[$k\parallel l$] command. By getting {true, ”c”} as output we are warned that these results are true on some components only.

Fig. 7

A numerical approach for detecting truth in GeoGebra

Fig. 8

A symbolic approach for detecting truth in GeoGebra

Let us summarily consider the algebraic counterpart of this geometric construction, that is, how GeoGebra automatically sets up the input polynomials for running the described algorithm. Free points are defined with coordinates $A(v_1,v_2)$, $B(v_3,v_4)$. Since point C is defined as a point on a circle with center A and radius m (that is the segment AB), GeoGebra introduces a hidden technical point $X_1(v_5,v_6)$ to describe the vector $\overrightarrow{AB}$ by using equations

$$\begin{aligned} h_1= & {} v_{5}-v_{3}=0, \end{aligned}$$

(1)

$$\begin{aligned} h_2= & {} v_{6}-v_{4}=0, \end{aligned}$$

(2)

and then, the constrained point $C(v_7,v_8)$ is given by the equation

$$\begin{aligned} h_3=-v_{8}^{2}-v_{7}^{2}+v_{6}^{2}+v_{5}^{2}+2v_{8}v_{2}-2v_{6}v_{2}+2v_{7}v_{1}-2v_{5}v_{1}=0. \end{aligned}$$

(3)

Now line h can be described as going through C and parallel to m, by implicitly creating hidden technical point $X_2(v_9,v_{10})$ such that the parallel line joins C and $X_2$:

$$\begin{aligned} h_4= & {} v_{9}-v_{7}-v_{3}+v_{1}=0, \end{aligned}$$

(4)

$$\begin{aligned} h_5= & {} v_{10}-v_{8}-v_{4}+v_{2}=0, \end{aligned}$$

(5)

Another technical point $X_3(v_{11},v_{12})$ is introduced as a circumpoint of circle c with center C and radius m with the help of equations

$$\begin{aligned} h_6= & {} v_{11}-v_{7}-v_{3}+v_{1}=0, \end{aligned}$$

(6)

$$\begin{aligned} h_7= & {} v_{12}-v_{8}-v_{4}+v_{2}=0. \end{aligned}$$

(7)

As the final step to describe the hypotheses the intersection point $D(v_{13},v_{14})$ of line h and circle c is defined by

$$\begin{aligned} h_8= & {} v_{13}v_{10}-v_{14}v_{9}-v_{13}v_{8}+v_{9}v_{8}+v_{14}v_{7}-v_{10}v_{7}=0, \end{aligned}$$

(8)

$$\begin{aligned} h_9= & {} -v_{14}^{2}-v_{13}^{2}+v_{12}^{2}+v_{11}^{2}+2v_{14}v_{8}-2v_{12}v_{8}+2v_{13}v_{7}-2v_{11}v_{7}=0. \end{aligned}$$

(9)

The thesis equation is

$$\begin{aligned} f=v_{14}v_8+v_{13}v_7-v_{14}v_4-v_{13}v_3-v_8v_2+v_4v_2-v_7v_1+v_3v_1=0. \end{aligned}$$

(10)

Without loss of generality GeoGebra assumes that $v_1=v_2=0$. After performing these substitutions and using the notations from Theorem 1, we have

$$\begin{aligned} X= & {} \{v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},v_{11},v_{12},v_{13},v_{14}\}, \\ Y= & {} \{v_3,v_4,v_7\},\ K=\mathbb {Q}, \end{aligned}$$

and GeoGebra computes

$$\begin{aligned} \left\langle h_1,\dots , h_9, f\cdot t-1\right\rangle K[X,t]\cap K[Y] \end{aligned}$$

and

$$\begin{aligned} \left\langle h_1,\dots , h_9,f\right\rangle K[X]\cap K[Y]. \end{aligned}$$

Since both are $\left\langle 0\right\rangle$ and the computed Hilbert dimension of $\left\langle h_1,h_2,\dots ,h_9\right\rangle$ is 3, equal to |Y|, the statement is identified as “true on parts, false on parts”, because it only holds for one of the choices $D, D^{\prime }$ of the intersection of the circle c with center C and radius m, and the line h through C and parallel to m The result is computed by GeoGebra below 1 second on a modern PC.

This GeoGebra example can also be tried out online at https://www.geogebra.org/m/VeAxJHmS. Clearly, the number of used variables and equations is an overkill here, but since it is organized completely automatically by the software translating the geometry statement to an algebraic setup, it can be acceptable. Also other variables might be substituted to some concrete integer numbers, e.g. $v_3=0,v_4=1$, yielding further simplifications. Such issues should be thoroughly addressed in future versions of GeoGebra.

Let us remark that this example is just one among many others that could be worked around our rhombus construction, yielding similar results. For example, we could have conjectured that the segments AC and BD are parallel or have the same length. In these cases the reader can check, using again the Relation tool in GeoGebra, that both conjectures are “true on parts, false on parts”.

Further examples can be found in GeoGebra’s automated benchmarking database at https://tinyurl.com/provertest-566 as of 24th March, 2018. All database cells that contain the single character c refer to an identified case of true on components.

Another online resource of such theorems is available at https://www.geogebra.org/m/zbuxywqf, containing some non-trivial examples.

5 Final reflections

At first glance, it could seem that this paper deals with an algorithm for detecting geometric statements that are true on some instances and false in some others...But, indeed, surely most affirmations are like this: holding in some very particular cases, failing in most of them. What could be the interest of automatically confirming the status of such irrelevant assertions?

First of all, let us remark that we are not dealing with all statements having this bivalent condition: we are focusing on those statements such that both the set of instances where the statement holds and the set where it fails are quite large and, in many respects, geometrically meaningful. Indeed, it happens, in general, that the irreducible components of the hypotheses variety carry some special geometric significance.

Thus, as argued in Sect. 2 with references and examples, detecting a true on parts, false on parts statement provides some interesting and intriguing information on the geometry of the given problem, yielding sometimes, with the help of human intelligence, to the discovery of relevant geometric facts; and, in all cases, rising a warning sign for the human user on the need to start thinking there could be “something” relevant behind—for instance, a wrong construction of a rhombus!

For instance, at a very basic level, this true on parts, false on parts situation could point out to the need to revise some constructions steps, that could indeed have got to be improved to avoid the bivalent behavior of a given statement in the different components associated to the construction. Thus, in Example 3.7 in [15], if, instead of using circles (yielding to a a true on components conclusion), the user deals just with rotations by 90 degrees, a clearly true statement is obtained.

On the other hand, some constructions cannot be improved by choosing a different approach. For instance, Example 1 (also in [15] Example 3.8) deals with two potential constructions of equilateral triangles over each side of a given triangle, indistinguishable, at least, from the complex algebraic geometry approach. That is, in dealing with such statements the notion of “true on components” is unavoidable.

In GeoGebra’s Automated Reasoning Tools, where we have performed the examples in Sect. 4, the case true on parts, false on parts is considered as a particular case of truth (true, but on some components only, the user is warned!). We need to admit that, from a rigorous point of view, this case could also be considered as a particular kind of failure. Are the segments k and l in Fig. 6 perpendicular if D is defined as an intersection of line h and circle c? “Well, no!”—that would be the answer of a rigorous maths professor. It seems however more supporting and creative for the student (and the researcher), even if the statement is, strictly speaking, not always true, to get a partially yes-answer, mentioning that some additional hypothesis—to be discovered by the user—may be required to achieve the complete truth of the investigated statement.

Finally, we would like to emphasize that this approach, in our opinion, can also be particularly fruitful in an educational context. Automated classification of statements can be helpful in homework for self-evaluation of the student; or in automated exam correction, helping the teacher. In fact, in the previous sections we have already shown several elementary statements in Euclidean planar geometry that could be identified as “true on components”.

In our opinion, and as shown by the examples and references mentioned in Sect. 2, this subtle notion of true on parts, false on parts is both interesting for the researcher, as a powerful tool for discovery, and for the student, and can rise even when considering statements of very basic geometry. Thus, it deserves to be functional in whatever automatic geometry reasoning program aiming to be considered fully useful for researchers and students. The algorithm and implementation we have presented in this paper could be considered as a first, but already fully performing, step in this direction.