我很确定这不是建设性的证明。
首先,请注意
¬¬p -> (¬p -> a)
适用于完全任意的p
and a
(从¬¬p
and¬p
您首先获得虚假证明,然后通过 ex falso quodlibet 您获得 any a
)。
特别是,对于任何q
,
¬¬p -> ((¬p -> q) /\ (¬p -> ¬q)) // ("lemma")
成立(将前面的语句应用于a = q
and a = ¬q
)。
现在,如果您的原始陈述((¬p -> q) /\ (¬p -> ¬q)) -> p
是正确的,那么您可以预先组合¬¬p -> ((¬p -> q) /\ (¬p -> ¬q))
,从而获得¬¬p -> p
. 但这是双重否定消除,众所周知,这是不可建设性地证明的。
这是 Scala 3 中的完整结构(与 OCaml 有点密切相关;这里使用的语言子集应该很容易翻译成 OCaml):
type ¬[A] = A => Nothing // negation
type /\[A, B] = (A, B) // conjunction / product
type Claim[P, Q] = (¬[P] => Q) => (¬[P] => ¬[Q]) => P // your claim
type DoubleNegationElimination[P] = ¬[¬[P]] => P
/** Ex falso quodlibet. */
def efq[X]: Nothing => X = f => f
/** Lemma, as explained above. */
def lemma[P, Q](a: ¬[¬[P]]): (¬[P] => Q) /\ (¬[P] => ¬[Q]) =
val left: ¬[P] => Q = notP => efq(a(notP))
val right: ¬[P] => ¬[Q] = notP => efq(a(notP))
(left, right)
/** This shows that if you could prove your claim for any `P`, `Q`,
* then you would also be able to prove double negation elimination
* for `P`.
*/
def claimImpliesDoubleNegationElimination[P, Q](
c: Claim[P, Q]
): DoubleNegationElimination[P] =
notNotP => {
val (left, right) = lemma[P, Q](notNotP)
c(left)(right)
}
/** This is an (incomplete, because impossible) proof of the double
* negation elimination for any `P`. It is incomplete, because it
* relies on the validity of your original claim.
*/
def doubleNegationElimination[P]: DoubleNegationElimination[P] =
claimImpliesDoubleNegationElimination(claim[P, Unit])
/** There cannot be a constructive proof of this, because otherwise
* we would obtain a constructive proof of `doubleNegationElimination`.
*/
def claim[P, Q]: Claim[P, Q] = ???