下面是一个利用形式逻辑的证明方法。

假设我们想证明：（*）x>1→∃y(Py∧(y|x))，即每个大于1的整数都有一个质因数。假设已经给定了一个有组织的信息库SF，其中首先列出的是+、·、<的性质，然后是p和|的性质。

基本的证明策略是假设该定理为假，进而尝试从最小的反例导出一个矛盾，这体现了数学归纳法原理的一个机械上方便的形式。所设想的最小反例构成一个“不明确的常项”，它不仅具有所有整数都有的普遍性质，还具有源于“它是一个反例”这个假设的特别的性质。在像（*）这样的简单情况下，援引SF中的信息并使用一些简单的真值函项演绎后，我们很快能得到一个具有矛盾性质的不明确的常项。

为了证明（*）,我们首先假设它为假，并令m为其最小反例：（1）m>1；（2）Pb→b∤m；（3）1

我们用m替换上面的a和b：（4）Pm→m∤m；（3）1

查阅SF找到P的定义性质并应用到m上：Pm↔∃x(1

用xm替换目前已得的一般陈述即（2）和（3）中的自由变项：（9）Pxm→xm∤m；（3）1

从（1）、（2）、（3）、（6-10）推导真值函项后承（先不使用SF）：（11）¬Pxm，根据（8）和（9）；（12）Pyxm，根据（7）和（10）；（13）yxm|xm，根据（7）和（10）。

现在利用SF中的信息(a|b)∧(b|c)→(a|c)：yxm|m，根据（8）和（13）。用不明确常项先替换（2）和（3）中的自由变项：（15）Pyxm→yxm∤m；（16）1

在实际编写一个机器程序之前，需要更准确地规定这个方法。但上述提纲表明，在现有机器上可以写出相当自然的程序来证明像（*）这样的定理。