嘿，这个问题的核心其实是直觉主义逻辑和经典逻辑的差异——你用的那两条公理是直觉主义命题逻辑的基础公理，而你要证的$[(p→f)→f]→p$本质上是双重否定消去规则（对应经典逻辑的排中律），在直觉主义逻辑里是没法从那两条公理推出来的。你用经典完备性定理找不到矛盾很正常，因为它在经典语义下确实是重言式，得换个语义模型来验证不可证性！

你提到的经典完备性定理是针对经典命题逻辑的，它说所有经典重言式都能被经典公理系统句法推导。但你用的两条公理$p→(q→p)$和$[p→(q→r)]→[(p→q)→(p→r)]$是直觉主义命题逻辑的核心公理，而目标公式$[(p→f)→f]→p$（也就是$\neg\neg p \to p$，因为$\neg p$定义为$p→f$）是经典逻辑的定理，但不是直觉主义逻辑的定理。经典语义下它是重言式，所以用经典完备性找矛盾肯定行不通，得用直觉主义逻辑的语义模型来构造反例。

克里普克模型是直觉主义逻辑的标准语义工具，它由可能世界、可达关系和原子命题赋值组成，核心规则是真值单调性：如果一个命题在某个世界为真，那么在所有该世界可达的世界中也为真。我们构造一个极简的克里普克模型：

• 世界集合：$W = {w_0, w_1}$
• 可达关系：$w_0 \rightarrow w_1$（$w_0$能到达$w_1$，$w_1$只能到达自己）
• 原子命题赋值：
  • 在$w_0$中：$p$为假，$f$为假（$f$代表假，所以所有世界里$f$都为假）
  • 在$w_1$中：$p$为真，$f$为假

验证两条公理在模型中成立 #

1. 公理$p→(q→p)$：
   • 在$w_0$：$p$为假，蕴含式前件为假，整个式子自动为真；
   • 在$w_1$：$p$为真，不管$q$的真值如何，$q→p$都是真（后件真则蕴含式真），所以整个公理为真。
2. 公理$[p→(q→r)]→[(p→q)→(p→r)]$：
   这是蕴含的分配律，是直觉主义逻辑的核心公理，在所有克里普克模型中都有效。简单验证：假设在某个世界$w$中前件$p→(q→r)$为真，那么对所有$w$可达的$w'$，若$p$在$w'$为真，则$q→r$在$w'$为真。要证后件$(p→q)→(p→r)$在$w$为真：假设在$w$可达的$w'$中$p→q$为真，那么对$w'$可达的$w''$，若$p$在$w''$为真，则$q$在$w''$为真；结合前件，$q→r$在$w''$为真，所以$r$在$w''$为真，因此$p→r$在$w'$为真，整个后件成立。

验证目标公式在模型中不成立 #

我们看目标公式$[(p→f)→f]→p$在$w_0$中的真值：

1. 先算$\neg p = p→f$：
   • 在$w_1$中，$p$为真、$f$为假，所以$p→f$为假；
   • 在$w_0$中，因为$w_0$能到达$w_1$，而$w_1$中$p$真但$f$假，所以$p→f$在$w_0$中为假（克里普克语义中，蕴含式为真要求所有可达世界满足“前件真则后件真”，这里存在反例）。
2. 再算$\neg\neg p = (p→f)→f$：
   • 在$w_0$的所有可达世界（$w_0$和$w_1$）中，$p→f$都是假，所以“假→f”是真（前件假则蕴含式真），因此$\neg\neg p$在$w_0$中为真。
3. 最后看$\neg\neg p → p$：
   • 在$w_0$中，$\neg\neg p$为真，$p$为假，所以“真→假”的结果是假。

根据直觉主义逻辑的可靠性定理：如果一个公式能从直觉主义公理句法推导出来，那么它在所有克里普克模型中都为真。我们找到了一个克里普克模型，其中两条公理都成立，但目标公式不成立，这就证明了目标公式无法从给定的两条公理科法推导出来。

内容的提问来源于stack exchange，提问作者WhizKid