一道高中数学题

有这样一道高中数学题:

问题1. 考虑一个定义域为实数的函数f(x)f(x),如果对于任意的xRx ∈ \mathbb{R},有f(x+1)=f(x)f(x + 1)=-f(x)f(1)=2f(1) = 2,问:f(2021)f(2021)等于多少?

首先可以看到,这个问题是不宜问“周期是多少”的,因为怎么问都不严谨。如果问最小正周期的话,立刻可以给出这样的例子:

f(x)=0f(x) = 0

它毫无疑问地满足f(x+1)=f(x)f(x + 1) = -f(x),然而这个函数的最小正周期不存在。另一种选择是问周期,但周期的话无疑会导致多个答案正确。所以不如问个具体的值。

当然,问具体的值很容易被猜到答案。所以在正式考试中,这种问题还是少见的。

这里要研究的并不是题目出得好不好,而是如何把这个题目讲解给学生听。

标准讲法

这里最关键的得到周期为2这个事实。一般来说,老师会这么讲:

因为

f(x+1)=f(x)f(x + 1) = -f(x)

所以

f(x+2)=f(x+1)f(x + 2) = -f(x + 1)

所以

f(x+2)=f(x)f(x + 2) = f(x)

然而这种讲法会导致学生很迷惑,至少我当年是很迷惑的。

为什么会出现这种情况呢?我们必须首先研究一下,f(x+1)=f(x)f(x + 1) = -f(x)这个命题到底是什么意思。

对条件的翻译

f(x+1)=f(x)f(x + 1) = -f(x)中含有自由变量xx,当务之急是把自由变量消除掉。

正如我之前的博客所言,如果把f(x+1)f(x + 1)看作一个函数,那么这个函数具有隐式的λ:

λx.f(x+1)λx.f(x + 1)

这样一来,原式就被翻译为:

λx.f(x+1)=λx.f(x)λx.f(x + 1) = λx.-f(x)

可是这显然不太好用,我们不如把它翻译为一个带有全称名词的一阶公式:

x.f(x+1)=f(x)∀x.f(x+1) = -f(x)

这个翻译实际上就是所谓的I-∀,用natural deduction的方法写作:

a term u[a/x]A true x.A true Iu,0\begin{gathered} \frac{}{a \text { term }} \mathrm{u} \\ \vdots \\ \frac{[a / x] A \text { true }}{\forall x . A \text { true }} \forall_{I^{u, 0}} \end{gathered}

形式化证明

把条件翻译好以后,我们可以给出一个比较形式化的证明。

要证明的是:

f.(x.f(x+1)=f(x))(x.f(x+2)=f(x))∀ f. (∀x. f(x + 1) = -f(x)) → (∀x. f(x + 2) = f(x))

证明如下:

  1. x.f(x+1)=f(x)∀x. f(x + 1) = -f(x), HYP
  2. xx, HYP
  3. x+1x + 1, 2.
  4. f((x+1)+1)=f(x+1)f((x + 1) + 1) = -f(x + 1), 1., 3., E-∀
  5. f(x+2)=f(x+1)f(x + 2) = -f(x + 1), 4.
  6. f(x+1)=f(x)f(x + 1) = -f(x), 1. , 2., E-∀
  7. f(x+1)=f(x)-f(x + 1) = f(x), 6.
  8. f(x+2)=f(x)f(x + 2) = f(x), 7., 5.
  9. x.f(x+2)=f(x)∀x. f(x + 2) = f(x), 8., I-∀

我们这里隐式地运用了一些和实数相关的命题。这些命题并不难不严格地讲出来。难点在于如何把2.和9.使用的I-∀规则不严格地讲出来。

这个难讲是因为引入了“自由变量”xx,很多老师为了避免这个问题,改用tt来代替,但这个变量还是自由变量。自由变量的非形式化,一般会引起各种困惑和误解,这就是一个很好的例子。

结论

如果能够完全地形式化,那么这个问题并不难讲。但形式化本身是困难的。高中阶段没有讲过形式证明,这个问题出现在“函数”模块,在这之前甚至没有讲过逻辑的部分。所以,这类题目实在不宜当作练习题引入。

彩蛋:coq证明

这个命题在整数上是成立的,我们可以用coq给出一个证明:

Require Import Coq.ZArith.BinInt.

Open Scope Z_scope.

Theorem double_opp: forall x:Z, --x = x.
Proof.
  intros x.
  repeat (rewrite Z.opp_eq_mul_m1).
  rewrite <- Zmult_assoc. simpl.
  rewrite  Zmult_1_r. reflexivity.
Qed.

Theorem t:forall f:(Z -> Z), 
  (forall x, f (x + 1) = - f x) ->
  (forall x, f (x + 2) = f x).
Proof.
  intros f H1 x.
  assert (t1:forall x, f(x + 2) = - f(x + 1)).
  { intros x0. 
    assert (t2: 2 = 1 + 1). { auto. }
    rewrite -> t2. rewrite Zplus_assoc.
    apply H1. }
  rewrite t1. rewrite H1. apply double_opp.
Qed.