P. 174 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17301-17301   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	alseu-no-surprise 17301	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17269 by alseuals 17287. See als-no-surprise 17269 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- -. ( A.E! x ( ph -> ps ) /\ A.E! x ( ph -> -. ps ) )

< Previous  Wrap >