A conceptual understanding of inequalities and logic is essential for success in most of mathematics and its applications. E.g., it is indispensable for the learning of calculus because inequalities and logic are the tools that are used to express intuitive ideas about rates, changes and limits in a formal way that is required to give proofs. We show that GeoGebra and especially GeoGebra Discovery can be used to support the learning of these foundations. It will be shown that propositional logic is already supported well in GeoGebra and that support for predicate logic is realized in the experimental fork GeoGebra Discovery.
GeoGebra was oficially designated as preferred tool for learners, because of its symbolic
computation capabilities, easy syntax and free availability. As of today, various school books
include tutorials and explanatory exercises on solving problems with the help of GeoGebra’s
CAS Window (see, for example [
Accessing symbolic algorithms in most classrooms is, however, still limited to widely-known techniques only. It is quite well-accepted by teachers that a computer algebra system should be able to solve a set of linear equations, or to find the derivative or anti-derivative of a function. But it is quite surprising for many teachers that today’s algorithms are ready to automatically solve problems that contain quantifiers as well. In fact, many teachers still lack good knowledge of connecting quantified formulas and text problems. Certainly, stable computer algebra support to handle such formulas with an easy syntax and a robust backend would speed up the widespread of the required knowledge among teachers and learners as well.
Therefore, our contribution confirms the relevance of the SC 2 Project for a wider community, including schools. The new cylindrical algebraic decomposition (CAD) algorithms that came out of SC2 Project (for example, the non-uniform CAD algorithm in Tarski) already make it possible to bring robust computations of non-trivial classroom problems by exploiting the popular user interface of GeoGebra. On the other hand, there is still room for several improvements. We give some examples on possible future work in the last section of the paper.
Logical thinking and mathematics are often believed to be related, and this is supported by
several studies. Wong [23] finds correlations between deductive reasoning and mathematical
problem-solving. Cresswell and Speelman [
One of the main issues in learning propositional logic is getting used to the definition of
implication, which is not meant to represent transfer of epistemic support, but only the formal
relation between truth values. Related to this is the law of excluded middle or equivalently that
double negation on a statement is logically identical to the original statement (of course, it should
be noted that these issues are deep and that there are constructivist mathematicians that do not
accept proofs by contradiction, but for the present paper, we simply restrict ourselves to classical
logic). Durand-Guerrier and Dawkins [
Propositional logic is not enough for mathematics: only predicate logic gives the means to
deal with mathematical objects like numbers and functions and describe their properties in a
precise sense. This role of describing properties precisely and enabling correct argumentation
about them is also important beyond mathematics, e.g. in computer science. The book [
Quantifiers play an essential role in predicate logic, yet they are dificult for learners to understand correctly (see e.g. [17, 19]). In many situations in mathematics, their use can be avoided by expressing them in common language. Hence, some students view formalization as an additional burden, not as a useful concept. In a computer algebra environment, however, formalization is the way to communicate with the computer and thus this can give students a feeling for its sense. Moreover, quantifiers are essential in the definitions of many concepts, especially in rigorous calculus. Formalization can thus be seen as a modelling process: intuitive concepts are modelled in formalized language, and a computer environment can be used to validate the results. This point of view, that formalization is a kind of modelling, has been advocated in the paper [15] (Fig. 2), but shall be elaborated with another example: students easily have an intuitive understanding of what it means that a function on an interval [a, b] increases strictly, e.g. they might express this as the rule that “if x increases, so does f (x)”. However, to give proofs a formal model of this intuitive idea must be developed, namely ∀x1, x2 ∈ [a, b] : x1 < x2 ⇒ f (x1) ≤ f (x2).
Thus, we will show that technology can be used to exercise such formalisation processes. Dual to formalization is interpretation, e.g. giving meaning to a formula. Both activities are linked in the modelling cycle and both activities should be addressed in teaching.
Tarski [21] has shown that in a certain class of ordered fields, including the real numbers, the predicate logic that includes addition, multiplication, equality (=), and inequality (<), is decidable. Moreover, he showed that every formula of this language, including quantifiers, can be transformed algorithmically into an equivalent form that is free of quantifiers. The theory covers absolute values, polynomials (and with some care also rational functions) as well as powers to ifxed rational exponents, but no logarithms, exponentials or other transcendental functions.
There are diferent realizations of Tarski’s theory. The most important one is based on
CAD. Metaphorically speaking, it rests on dividing the space of possible values of variables into
components, on which each polynomial relevant in the formula at hand has the same sign. The
question as to whether a formula is true for all infinitely many numbers can thus be reduced to
the question if it is true on a finite set of sample point: one from each of these cells. Although
explaining CAD and how it leads to quantifier elimination is dificult (an attempt has been made
in [
Recently, an experimental version of GeoGebra [
As a result, it is easy to formulate statements given in predicate logic in GeoGebra Discovery. This usually means that a combination of existential and universal quantifiers can be given, that quantify an expression that consists of polynomial equations or inequalities, connected by logical operations. For example, to formalize the statement that there is no least positive number, we can use GeoGebra Discovery’s CAS Window and type the following line
¬(∃x x > 0 ∧ (∀y y > 0 → x < y)).
Now, GeoGebra Discovery preprocesses this input for Tarski, which implies a certain extent of automatic simplification and the formula ∀x (∃y (x ≤ 0 ∨ y > 0 ∧ y − x ≤ 0)) (1) is returned: it is a prenex form of the input that contains no implication operations. Finally, the command RealQuantifierElimination($) computes via a black-box CAD process the quantifier free version which is in this case simply the logical truth of the formula, i.e. it returns the answer “true”.
GeoGebra Discovery also supports visualizing CAD in two dimensions. Here, the command Plot2D(x ≤ 0 ∨ y > 0 ∧ y − x ≤ 0, "x") shows the decomposition
(A1 ∪ A2 ∪ A3 ∪ A4 ∪ A5) ∪ (B1 ∪ B2 ∪ B3) ∪ (C1 ∪ C2 ∪ C3 ∪ C4 ∪ C5) where A1 = {x < 0 ∧ y < x}, A2 = {x < 0 ∧ y = x}, A3 = {x < 0 ∧ x < y < 0}, A4 = {x < 0 ∧ y = 0}, A5 = {x < 0 ∧ 0 < y}, B1 = {x = 0 ∧ y < 0}, B2 = {x = 0 ∧ y = 0}, B3 = {x = 0 ∧ y > 0}, C1 = {0 < x ∧ y < 0}, C2 = {0 < x ∧ y = 0}, C3 = {0 < x ∧ y < x}, C4 = {0 < x ∧ y = x}, C5 = {0 < x ∧ x < y} (see Figure 1). One can easily see that the projections of these sets on the x-axes are A = {x < 0}, B = {x = 0} and C = {0 < x}, respectively. On the other hand, it is easy to read of that formula ( 1) is true because for all projected sets A, B and C, there are pre-image regions (namely, A1, A2, A3, A4, A5, B1, B2, B3, C3 and C4) such that the formula x ≤ 0 ∨ y > 0 ∧ y − x ≤ 0 yields.
In fact, the CAD approach allows the user to plot arbitrary inequalities or logical connectives of
inequalities in two variables in a faithful way. This can be, however, computationally exhausting
for formulas containing many logical operations or higher degrees of polynomials [
With this section, we start with presenting ideas how these tools can be included in teaching. Inequalities in two variables have the nice property that their solution set can be represented graphically, and standard GeoGebra can do this easily (without using a CAD, unless higher degree polynomials are present). Moreover, it ofers the possibility to combine inequalities by logical junctions such as “and”, “or”, “not”, and “implication”. For example, one may enter y > 0 ∧ x2 + y2 < 9 to get directly the graph shown in Figure 2 on the left. To get the result on the right side of Figure 2, students can come up with several solutions. What they do is modelling geometric sets within logic and set theory. Experience showed (see [16]) that such activities can be motivating even for younger students of age 15. The graphical context eased argumentation and students easily acquired logical rules such as de Morgans’ laws, the rule of double negation or the expression of implication by conjunction a → b ⇔ ¬a ∨ b. Such activities can also be combined with absolute values.
Formalization of intuitive ideas with predicate logic and understanding formulas expressed in predicate logic are dual activities that can both be exercised within GeoGebra Discovery. Let us ifrst consider two easy examples taken from assignments in actual teaching, one of each kind: 1. Interpretation: Given the real function f (x) = x3 − x interpret what the following formula means: ∀x : x > a → (∀y : x < y → f (x) < f (y)). 2. Modelling: Express that a real valued function has exactly one, resp. exactly two global maxima. Test your formalization with various polynomial functions.
The meaning of the formula in 1 is best understood when doing some rearrangement to come to the equivalent form ∀x, y : a < x ∧ x < y → f (x) < f (y). Hence, the meaning is that the function is strictly monotonically increasing on the open interval ]a, ∞[. For f (x) = x3 − x quantifier elimination will hence give the equivalent form a ≥ 1/√3 which can be used to check logical reasoning.
The second example leads to the formalizations ∃x0 ∀x : x ̸= x0 → f (x) < f (x0) resp. ∃x1 ∃x2 : x1 ̸= x2 ∧ f (x1) = f (x2) ∧ ∀x : f (x) ≤ f (x1) ∧ (f (x) = f (x1) → (x = x1 ∨ x = x2))
Figure 3 shows how the first activity can be supported with GeoGebra Discovery: In its CAS View the function f must be defined first, then the quantified statement is to be entered (which will be automatically rewritten into an equivalent prenex form), after this step a real quantifier elimination is performed, which is finally reformulated into a formula which is familiar for students.
Figure 4 gives an overview on how the second part of activity 2 can be formulated in the same software. First, we define a quartic function that fulfills the expected property. Later, we should do a counter-test with a non-example function. Syntactically, it is important that in certain parts of the input a minimal number of spaces and parentheses must be used; otherwise, the input will be misinterpreted and the user can obtain, at first sight, strange results. Here we provide a “didactic trick” to obtain some analysis on two simplified formulas that contain just two quantifiers (or just one) with the same inner formula: clearly, GeoGebra cell 5 finds the extrema at for the input function, and this is confirmed in cell 7 of the session.
It is quite clear that more complicated notions and concepts may be even more dificult to formulate and check. But, unlike other computer software that support real quantifier elimination (like Mathematica, which may be a problematic choice for students because of its commercial licensing; or like Qepcad B, which is dificult to access for non-experts), GeoGebra Discovery ofers a classroom-like syntax inside its CAS View which should already be quite well-known for many learners.
To finish, we give two advanced examples to check continuity and diferentiability.
First, we consider the function f (x) = x2/x if x ̸= 0. This has the limit 0 near 0, but, since it is undefined at 0, it is not continuous. A correct formula that checks the limit property is now ∀ε ε > 0 → (∃δ δ >
0 ∧ (∀x x ̸= 0 ∧ x < δ → x2/x < ε)).
Here we note that the software rewrites the input into the non-equivalent form ∀ε (∃δ (∀x (ε ≤ 0 ∨ δ > 0 ∧ ((x = 0) ∨ (x2(ε − x)) > 0 ∨ δ − x ≤ 0)))) to prepare it to be applicable for Tarski’s theory because divisions are disallowed. The trick here is to multiply by the square of the denominator, however, this should be done cautiously as being considered also in the original manual input. Finally, the real quantifier elimination confirms that f has a removable discontinuity at 0.
Second, we would like to compute the derivative of a rational function. In Figure 5 we collected the required steps for a simple input: a rational function of two linear formulas. Here we note that it may take quite a long time until the learners find a syntactically correct input formula. So, very importantly, proper use of implications (after universal quantifiers) and conjunctions (after existential quantifiers) cannot be avoided, that is, finding a successful solution requires solving mathematical challenges as well.
First author held a teacher training course in logic for prospective mathematics teachers in the
winter semester of 2023/2024 at The Private University College of Education of Linz, Austria.
This course was a refined version of two former courses, based on a similar content but now with
improvements. The lecture notes for this course are available at [
The students were asked to try both commands RealQuantifierElimination and Plot2D in the desktop or web version of GeoGebra Discovery, during the lectures and also for their homework assignments. Figure 6 shows the expected homework activities for the participants, 30 students, many of them having a bachelor degree already, but some of them not yet (only successfully passed exams in discrete mathematics, linear algebra and calculus). The concept of a CAD was dificult to understand for many students, this is why the lecturer decided to prolong explaining the topic, since in the planned schedule there was only two weeks reserved for these activities. 8. Feature List • Quantified formulas can be stored in variables. • Formula negation is supported. • Disjunction, conjuction and implication between two formulas is allowed. • Output expressions are automatically converted into prenex format. • Quantifiers ∀ and ∃ are available in GeoGebra’s virtual keyboards. Also, keyboard shortcuts (Alt-V and Alt-X) are supported. • Keyboard shortcuts for the negation sign (Alt-Z), disjunction (Alt-J), conjunction (Alt-K), implication (Alt-Y) and the not-equal sign (Alt-H). • Localization for the Plot2D and RealQuantifierElimination commands are available in
English (default), German, Spanish and Hungarian.
• Rational numbers and quadratic surds are accepted as input. • Rational functions are rewritten as implications before conversion to Tarski. • The Plot2D command can have a second argument: “x” or “y”. If it is set, the cylindrical algebraic decomposition will be created with respect to the given variable.
The above presentation showed that nowadays the technique of quantifier elimination is in
the reach of students and can be used to do sensible exercises in calculus. This use can build
naturally on former use of GeoGebra to exercise modelling with propositional calculus and
inequalities. In all applications the combination of two dual processes, the interpretation of
formulas and formalization of intuitive ideas, is an important didactical method that allows to
take benefits from the technical power of GeoGebra Discovery. A systematic empirical evaluation
of these benefits is, however, still to be conducted.
9.1. Connection with the SC2 Project
Teaching the concept of proofs in classrooms with the help of technology requires reliable
implementations of the used prover subsystems. In GeoGebra Discovery we use the Tarski
system for outsourcing heavy computations that require reliable and possibly fast calculations.
Also, some basic operations like parsing the input or preparing it for further operations inside
Tarski, may require additional internal programmatic techniques. Here we mention the smtlib
interface between them: for instance, the formula
(qepcad-api-call (smtlib-load ’clear "(assert (exists ((x Real)) (and (not (=
a 0) ) (= (+ (+ (* x b) c) (* (* x x) a)) 0))))") ’T)
describes the user input existence of a real root of the quadratic equation ax2 + bx + c = 0. After
performing quantifier elimination, the result a /= 0 /\ 4 a*c - bˆ2 <= 0 (which means: the
discriminant b2 − 4ac is non-negative) must be translated back to GeoGebra internals. See [
Now, we point to some possible future work. The example in Fig. 5 performs reliably if the input f is a rational function, unless the denominator is of higher degree than 1. In other cases the computation may result in a program crash due to possible lack of resources, missing optimizations in the underlying algorithms or other issues. For a reliable student experience this should be addressed in a next version of the program.
The first author was partially supported by the project “Mathematical Visualization: Foundations, Algorithms and Applications”, PID2020-113192GB-I00 from the Spanish MICINN. We thank Chris Brown for his continuous support in help using Tarski in the appropriate way for our project, and for updating it accordingly. [14] Buteau, C., Marshall, N., Jarvis, D.H., Lavicza, Z.: Integrating computer algebra systems in post-secondary mathematics education: Preliminary results of a literature review.
International Journal for Technology in Mathematics Education 16(2) (2010). [15] Oldenburg, R.: Gains and pitfalls of quantifier elimination as a teaching tool. The International Journal for Technology in Mathematics Education 22, 163–167 (2015) Retrieved June 5, 2024 from https://www.learntechlib.org/p/195004/. [16] Oldenburg, R.: Logik und Ungleichheit – ein leider exotisches Thema. In: Bender, P. (ed.)
Beiträge zum Mathematikunterricht 2018, pp. 1347–1350, WTM-Verlag (2018) [17] Selden, J., Selden, A.: Unpacking the logic of mathematical statements. Educational Studies in Mathematics 29, 123–151 (1995) doi:10.1007/BF01274210 [18] Selden, A.: Transitions and Proof and Proving at Tertiary Level. In: Hanna, G., de Villiers, M. (eds.) Proof and Proving in Mathematics Education. Springer (2012). doi:10.1007/97894-007-2129-6_17 [19] Shipman, B.: Subtleties of hidden quantifiers in implication. Teach. Math. Appl. 35(1), 41–49 (2016). doi:10.1093/teamat/hrv007 [20] Stavrou, S.: Common errors and misconceptions in mathematical proving by education undergraduates. Issues Undergrad. Math. Prep. Sch. Teach., 1–8 (2014) [21] Tarski, A.: A decision method for elementary algebra and geometry. Rand Corporation
Publication (1948). doi:10.2307/2267068 [22] Vale-Enriquez, F., Brown, C.W.: Polynomial Constraints and Unsat Cores in Tarski. In: Davenport, J. H., Kauers, M., Labahn, M., Urban, J. (eds.) Mathematical Software – ICMS 2018, LNCS, vol. 10931, pp. 466–474. (2018). doi:10.1007/978-3-319-96418-8_55 [23] Wong, T.: Is conditional reasoning related to mathematical problem solving? Developmental Science 21(5), e12644 (2017). doi:10.1111/desc.12644