Reasoning operators

We use the following reasoning operators. These operators are part of a meta-language, because an expression like claim1 ⇒ claim2 should only result in a truth value on meta-level but not on the level of our logic.

symbol	read	write as
⇒	deduces	==>
⇐	is deduced by	<==
⇔	are equivalent	<=>

A counterexample to a claim on one variable is a value of the variable that makes the claim not hold. For instance, x = −8 is a counterexample to x + 5 ≥ 0.

Please give counterexamples to the following claims. If there are many counterexamples, you may choose yourself which one you give.

Because of a technical limitation of the current version of the tool, here it can only deal reliably with numbers from 0 to 10.
So please only use integers in the range [0, 10] as counterexamples.

x + 2 < 9 modulo 21 f_nodes 3 ok_text Correct! !(x+2 < 9) <== x = fails if x =

x² > 0 modulo 21 f_nodes 3 ok_text Correct! !(x^2 > 0) <== x = fails if x =

x² + 10 = 7x modulo 21 f_nodes 3 ok_text Correct! !(x^2 + 10 = 7x) <== x = fails if x =

x² + 10 ≠ 7x modulo 21 f_nodes 3 ok_text Correct! !(x^2 + 10 != 7x) <== x = fails if x =

A claim is correct if and only if it has no counterexamples.

A reasoning step is of one of the following three forms:

form	counterexample: a value of the variable that makes
claim1 ⇒ claim2	claim1 hold but claim2 not hold
claim1 ⇐ claim2	claim2 hold but claim1 not hold
claim1 ⇔ claim2	one of claim1 and claim2 hold, and the other not hold

Reasoning steps can be chained, like in claim1 ⇔ claim2 ⇒ claim3. (However, having both ⇒ and ⇐ in the same chain usually does not make sense.)

A reasoning step is correct if and only if it has no counterexamples.

Give counterexamples to the following reasoning steps.

Now you may use also negative numbers and numbers bigger than 10. (On the other hand, now the feedback is less easy to interpret.)

x ≥ 4  ⇒  x ≥ 7 arithmetic ok_text Correct! fail_text It is not a counterexample. only_no_yes_on f_nodes 2 hide_expr 4 <=
x = < hide_expr 7

3 ≥ 2  ⇒  3x ≥ 2x arithmetic ok_text Correct! fail_text It is not a counterexample. only_no_yes_on f_nodes 2 hide_expr 0 >
x =

x³ = 25x  ⇔  x² = 25 arithmetic ok_text Correct! fail_text It is not a counterexample. only_no_yes_on f_nodes 2 hide_expr 0 =
x =

√x = x − 2  ⇔  x = (x − 2)². arithmetic ok_text Correct! fail_text It is not a counterexample. only_no_yes_on f_nodes 1 hide_expr 1 =
x =

Are the following reasoning steps correct?

x < 0  ⇒  x² > 0 arithmetic ok_text Yes, it is correct! There are no counterexamples. fail_text If it is not correct, then there must be a counterexample. It must make #<i#>x#</i#> < 0 true and #<i#>x#</i#>#<sup#>2#</sup#> > 0 false. The only #<i#>x#</i#> that makes #<i#>x#</i#>#<sup#>2#</sup#> > 0 false is 0, but it makes also #<i#>x#</i#> < 0 false, so it is not a counterexample. only_no_yes_on hide_expr 1 = hide_expr 0
no yes

x < 0  ⇔  x² > 0 arithmetic ok_text Yes, it is not correct, because there are counterexamples! For instance, #<i#>x#</i#> = 1 makes the right hand side true but the left hand side false. fail_text What happens with positive values of #<i#>x#</i#>? only_no_yes_on hide_expr 1 = hide_expr 0
no yes

x = x − 2  ⇒  x = −123 arithmetic ok_text Yes, it is correct! There are no counterexamples, because #<i#>x#</i#> = #<i#>x#</i#> − 2 never holds. fail_text If it is not correct, then there must be a counterexample. It must make #<i#>x#</i#> = #<i#>x#</i#> − 2 true (and #<i#>x#</i#> = −123 false). No #<i#>x#</i#> makes #<i#>x#</i#> = #<i#>x#</i#> − 2 true. only_no_yes_on hide_expr 1 = hide_expr 0
no yes

Type the correct reasoning operator. If more than one is correct type the most informative one.

x > 4 modulo 21 ok_text Correct! x > 4 x ≥ 9 x ≥ 9

x = −3 modulo 21 ok_text Correct! fail_text Sorry for bad error message! The tool is not perfect. In any case, ⇒ and ⇐ are correct but not the most informative ones. x = -3 −2x = 6 -2x = 6

x = y modulo 21 ok_text Correct! x = y ax = ay a x = a y