12 February 2022

Further thoughts on supporting logic with technology

These are some further ideas on the possibilities on how integrating Tarski into GeoGebra can be fruitful in teaching logic. They reflect the latest improvements in GeoGebra Discovery. As a start, consider the command ∃a a>0. Just click on the command and it will be automatically copied and pasted in the CAS View below:

Now we will negate this: !$. You certainly noticed that GeoGebra rewrites your input a bit, but this change may improve readability.

Let us consider some examples from a secondary school textbook that may involve a bit of logic. I am going to use the Austrian textbook Mathematik verstehen 5, written by Malle et al. (Österreichische Bundesverlag Schulbuch, 2017).

(1.03) At the very beginning of the textbook we need to decide if some statements are equivalences or implications of each other. For example, the student must decide if $x\neq0\Leftrightarrow x<0\vee x>0$. Unfortunately, we need to avoid entering $x\neq0$ directly, because – this is a minor bug in the underlying CAS – this will be immediately evaluated as true. So we need a workaround: we must directly enter RealQuantifierElimination(x≠0 -> x<0∨x>0) in one turn, for one direction. For the other direction the command RealQuantifierElimination(x<0∨x>0 -> x≠0) can be used.
(1.02d) If the number 0 is not involved, we usually have a simpler method. Problem: Show that $x\ge1\Rightarrow x^2\ge1$. Is the converse of this statement true? Solution: S_1:=x>=1, S_2:=x^2>=1, RealQuantifierElimination(S_1 -> S_2) (this returns true) and RealQuantifierElimination(S_2 -> S_1) (this returns a condition to be fulfilled). The last command can be formulated as RealQuantifierElimination(∀x S_2 -> S_1) to get false.
(3.49) Find all $k\in\mathbb{R}$ such that the equation $x^2-kx+1$ has at least one solution. A possible way to solve this: We construct the polynomial $p(x)$ first: p(x):=x^2-k x+1. Then we issue RealQuantifierElimination(∃a p(a)=0).
A variant of the previous question: When are there exactly two solutions? Answer: RealQuantifierElimination(∃x_{1} (∃x_{2} ((p(x_{1})=0) ∧ (p(x_{2})=0) ∧ (x_{1}≠x_{2})))). Here the output could be further simplified.
Another variant: When are there no solutions? A possible way to get the answer: We consider the quantified equation A:=∃a p(a)=0 as statement $A$. Now we deny it: B:=!A. And finally we resolve this by using RealQuantifierElimination(B).

These simple examples show that manipulations on logic formulas can make sense already at the beginning of the secondary school. And later, if some more complicated concepts are introduced, students could already be familiar with them. Just two final examples to demonstrate the power of this tool by using negations on the definition of monotonicity and convergence:

M:=∀a (∀b (a<b -> a^2>b^2)) claims that the function $y=x^2$ monotonically increasing. How to deny this statement? Use !M.
C:=∀ε (∃N (n>N-> 1<n ε)) claims that the sequence $a_n=1/n$ converges to zero. (In fact here we consider the function $y=1/x$ at infinity.) Note that instead of the usual equality $1/n<\varepsilon$ we wrote $1 < n \varepsilon$ because the underlying system requires this format. How to deny this statement? Just use !C.

Entries on topic GeoGebra

Zoltán Kovács
Linz School of Education
Johannes Kepler University
Altenberger Strasse 69
A-4040 Linz

zoltan@geogebra.org